Theory IsaSAT_Literals

theory IsaSAT_Literals imports More_Sepref.WB_More_Refinement "Word_Lib.Many_More" Watched_Literals.Watched_Literals_Watch_List Entailment_Definition.Partial_Herbrand_Interpretation Isabelle_LLVM.Bits_Natural begin chapter ‹Refinement of Literals› section ‹Literals as Natural Numbers› subsection ‹Definition› lemma Pos_div2_iff: ‹Pos ((bb :: nat) div 2) = b ⟷ is_pos b ∧ (bb = 2 * atm_of b ∨ bb = 2 * atm_of b + 1)› by (cases b) auto lemma Neg_div2_iff: ‹Neg ((bb :: nat) div 2) = b ⟷ is_neg b ∧ (bb = 2 * atm_of b ∨ bb = 2 * atm_of b + 1)› by (cases b) auto text ‹ Modeling typ‹nat literal› via the transformation associating term‹2*n› or term‹2*n+1› has some advantages over the transformation to positive or negative integers: 0 is not an issue. It is also a bit faster according to Armin Biere. › fun nat_of_lit :: ‹nat literal ⇒ nat› where ‹nat_of_lit (Pos L) = 2*L› | ‹nat_of_lit (Neg L) = 2*L + 1› lemma nat_of_lit_def: ‹nat_of_lit L = (if is_pos L then 2 * atm_of L else 2 * atm_of L + 1)› by (cases L) auto fun literal_of_nat :: ‹nat ⇒ nat literal› where ‹literal_of_nat n = (if even n then Pos (n div 2) else Neg (n div 2))› lemma lit_of_nat_nat_of_lit[simp]: ‹literal_of_nat (nat_of_lit L) = L› by (cases L) auto lemma nat_of_lit_lit_of_nat[simp]: ‹nat_of_lit (literal_of_nat n) = n› by auto lemma atm_of_lit_of_nat: ‹atm_of (literal_of_nat n) = n div 2› by auto text ‹There is probably a more ``closed'' form from the following theorem, but it is unclear if that is useful or not.› lemma uminus_lit_of_nat: ‹- (literal_of_nat n) = (if even n then literal_of_nat (n+1) else literal_of_nat (n-1))› by (auto elim!: oddE) lemma literal_of_nat_literal_of_nat_eq[iff]: ‹literal_of_nat x = literal_of_nat xa ⟷ x = xa› by auto presburger+ definition nat_lit_rel :: ‹(nat × nat literal) set› where ‹nat_lit_rel = br literal_of_nat (λ_. True)› lemma ex_literal_of_nat: ‹∃bb. b = literal_of_nat bb› by (cases b) (auto simp: nat_of_lit_def split: if_splits; presburger; fail)+ subsection ‹Lifting to annotated literals› fun pair_of_ann_lit :: ‹('a, 'b) ann_lit ⇒ 'a literal × 'b option› where ‹pair_of_ann_lit (Propagated L D) = (L, Some D)› | ‹pair_of_ann_lit (Decided L) = (L, None)› fun ann_lit_of_pair :: ‹'a literal × 'b option ⇒ ('a, 'b) ann_lit› where ‹ann_lit_of_pair (L, Some D) = Propagated L D› | ‹ann_lit_of_pair (L, None) = Decided L› lemma ann_lit_of_pair_alt_def: ‹ann_lit_of_pair (L, D) = (if D = None then Decided L else Propagated L (the D))› by (cases D) auto lemma ann_lit_of_pair_pair_of_ann_lit: ‹ann_lit_of_pair (pair_of_ann_lit L) = L› by (cases L) auto lemma pair_of_ann_lit_ann_lit_of_pair: ‹pair_of_ann_lit (ann_lit_of_pair L) = L› by (cases L; cases ‹snd L›) auto lemma literal_of_neq_eq_nat_of_lit_eq_iff: ‹literal_of_nat b = L ⟷ b = nat_of_lit L› by (auto simp del: literal_of_nat.simps) lemma nat_of_lit_eq_iff[iff]: ‹nat_of_lit xa = nat_of_lit x ⟷ x = xa› apply (cases x; cases xa) by auto presburger+ definition ann_lit_rel:: ‹('a × nat) set ⇒ ('b × nat option) set ⇒ (('a × 'b) × (nat, nat) ann_lit) set› where ann_lit_rel_internal_def: ‹ann_lit_rel R R' = {(a, b). ∃c d. (fst a, c) ∈ R ∧ (snd a, d) ∈ R' ∧ b = ann_lit_of_pair (literal_of_nat c, d)}› section ‹Conflict Clause› definition the_is_empty where ‹the_is_empty D = Multiset.is_empty (the D)› section ‹Atoms with bound› definition unat32_max :: nat where ‹unat32_max ≡ 2^32-1› definition unat64_max :: nat where ‹unat64_max ≡ 2^64-1› definition snat32_max :: nat where ‹snat32_max ≡ 2^31-1› definition snat64_max :: nat where ‹snat64_max ≡ 2^63-1› lemma li_unat32_maxdiv2_le_unit32_max: ‹a ≤ unat32_max div 2 + 1 ⟹ a ≤ unat32_max› by (auto simp: unat32_max_def) lemma unat64_max_uint_def: ‹unat (-1 :: 64 Word.word) = unat64_max› proof - have ‹unat (-1 :: 64 Word.word) = unat (- Numeral1 :: 64 Word.word)› unfolding numeral.numeral_One .. also have ‹… = unat64_max› unfolding unat_bintrunc_neg apply (simp add: unat64_max_def) apply (subst numeral_eq_Suc; subst semiring_bit_operations_class.mask_Suc_exp; simp)+ done finally show ?thesis . qed section ‹Operations with set of atoms.› context fixes 𝒜_i_n :: ‹nat multiset› begin abbreviation D₀ :: ‹(nat × nat literal) set› where ‹D₀ ≡ (λL. (nat_of_lit L, L)) ` set_mset (ℒ_a_l_l 𝒜_i_n)› text ‹ The following lemma was necessary at some point to prove the existence of a watch list. › lemma ex_list_watched: fixes W :: ‹nat literal ⇒ 'a list› shows ‹∃aa. ∀x∈#ℒ_a_l_l 𝒜_i_n. nat_of_lit x < length aa ∧ aa ! nat_of_lit x = W x› (is ‹∃aa. ?P aa›) proof - define D' where ‹D' = D₀› define ℒ_a_l_l' where ‹ℒ_a_l_l' = ℒ_a_l_l› define D'' where ‹D'' = mset_set (snd ` D')› let ?f = ‹(λL a. a[nat_of_lit L:= W L])› interpret comp_fun_commute ?f apply standard apply (case_tac ‹y = x›) apply (solves simp) apply (intro ext) apply (subst (asm) lit_of_nat_nat_of_lit[symmetric]) apply (subst (asm)(3) lit_of_nat_nat_of_lit[symmetric]) apply (clarsimp simp only: comp_def intro!: list_update_swap) done define aa where ‹aa ≡ fold_mset ?f (replicate (1+Max (nat_of_lit ` snd ` D')) []) (mset_set (snd ` D'))› have length_fold: ‹length (fold_mset (λL a. a[nat_of_lit L := W L]) l M) = length l› for l M by (induction M) auto have length_aa: ‹length aa = Suc (Max (nat_of_lit ` snd ` D'))› unfolding aa_def D''_def[symmetric] by (simp add: length_fold) have H: ‹x ∈# ℒ_a_l_l' ⟹ length l ≥ Suc (Max (nat_of_lit ` set_mset (ℒ_a_l_l'))) ⟹ fold_mset (λL a. a[nat_of_lit L := W L]) l (remdups_mset (ℒ_a_l_l')) ! nat_of_lit x = W x› for x l ℒ_a_l_l' unfolding ℒ_a_l_l'_def[symmetric] apply (induction ℒ_a_l_l' arbitrary: l) subgoal by simp subgoal for xa Ls l apply (case_tac ‹(nat_of_lit ` set_mset Ls) = {}›) apply (solves simp) apply (auto simp: less_Suc_eq_le length_fold) done done have H': ‹aa ! nat_of_lit x = W x› if ‹x ∈# ℒ_a_l_l 𝒜_i_n› for x using that unfolding aa_def D'_def by (auto simp: D'_def image_image remdups_mset_def[symmetric] less_Suc_eq_le intro!: H) have ‹?P aa› by (auto simp: D'_def image_image remdups_mset_def[symmetric] less_Suc_eq_le length_aa H') then show ?thesis by blast qed text ‹The following two definitions are very important in practise for the invariants for the SAT solver.› definition isasat_input_bounded where [simp]: ‹isasat_input_bounded = (∀L ∈# ℒ_a_l_l 𝒜_i_n. nat_of_lit L ≤ unat32_max)› definition isasat_input_nempty where [simp]: ‹isasat_input_nempty = (set_mset 𝒜_i_n ≠ {})› definition isasat_input_bounded_nempty where ‹isasat_input_bounded_nempty = (isasat_input_bounded ∧ isasat_input_nempty)› section ‹Set of atoms with bound› context assumes in_ℒ_a_l_l_less_unat32_max: ‹isasat_input_bounded› begin lemma in_ℒ_a_l_l_less_unat32_max': ‹L ∈# ℒ_a_l_l 𝒜_i_n ⟹ nat_of_lit L ≤ unat32_max› using in_ℒ_a_l_l_less_unat32_max by auto lemma in_𝒜_i_n_less_than_unat32_max_div_2: ‹L ∈# 𝒜_i_n ⟹ L ≤ unat32_max div 2› using in_ℒ_a_l_l_less_unat32_max'[of ‹Neg L›] unfolding Ball_def atms_of_ℒ_a_l_l_𝒜_i_n in_ℒ_a_l_l_atm_of_in_atms_of_iff by (auto simp: unat32_max_def) lemma simple_clss_size_upper_div2': assumes lits: ‹literals_are_in_ℒ_i_n 𝒜_i_n C› and dist: ‹distinct_mset C› and tauto: ‹¬tautology C› and in_ℒ_a_l_l_less_unat32_max: ‹∀L ∈# ℒ_a_l_l 𝒜_i_n. nat_of_lit L < unat32_max - 1› shows ‹size C ≤ unat32_max div 2› proof - let ?C = ‹atm_of `# C› have ‹distinct_mset ?C› proof (rule ccontr) assume ‹¬ ?thesis› then obtain K where ‹¬count (atm_of `# C) K ≤ Suc 0› unfolding distinct_mset_count_less_1 by auto then have ‹count (atm_of `# C) K ≥ 2› by auto then obtain L L' C' where C: ‹C = {#L, L'#} + C'› and L_L': ‹atm_of L = atm_of L'› by (auto dest!: count_image_mset_multi_member_split_2) then show False using dist tauto by (auto simp: atm_of_eq_atm_of tautology_add_mset) qed then have card: ‹size ?C = card (set_mset ?C)› using distinct_mset_size_eq_card by blast have size: ‹size ?C = size C› using dist tauto by (induction C) (auto simp: tautology_add_mset) have m: ‹set_mset ?C ⊆ {0..<unat32_max div 2}› proof fix L assume ‹L ∈ set_mset ?C› then have ‹L ∈ atms_of (ℒ_a_l_l 𝒜_i_n)› using lits by (auto simp: literals_are_in_ℒ_i_n_def atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff) then have ‹Pos L ∈# (ℒ_a_l_l 𝒜_i_n)› using lits by (auto simp: in_ℒ_a_l_l_atm_of_in_atms_of_iff) then have ‹nat_of_lit (Pos L) < unat32_max - 1› using in_ℒ_a_l_l_less_unat32_max by (auto simp: atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff) then have ‹L < unat32_max div 2› by (auto simp: atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff unat32_max_def) then show ‹L ∈ {0..<unat32_max div 2}› by (auto simp: atm_of_lit_in_atms_of unat32_max_def in_all_lits_of_m_ain_atms_of_iff subset_iff) qed moreover have ‹card … = unat32_max div 2› by auto ultimately have ‹card (set_mset ?C) ≤ unat32_max div 2› using card_mono[OF _ m] by auto then show ?thesis unfolding card[symmetric] size . qed lemma simple_clss_size_upper_div2: assumes lits: ‹literals_are_in_ℒ_i_n 𝒜_i_n C› and dist: ‹distinct_mset C› and tauto: ‹¬tautology C› shows ‹size C ≤ 1 + unat32_max div 2› proof - let ?C = ‹atm_of `# C› have ‹distinct_mset ?C› proof (rule ccontr) assume ‹¬ ?thesis› then obtain K where ‹¬count (atm_of `# C) K ≤ Suc 0› unfolding distinct_mset_count_less_1 by auto then have ‹count (atm_of `# C) K ≥ 2› by auto then obtain L L' C' where C: ‹C = {#L, L'#} + C'› and L_L': ‹atm_of L = atm_of L'› by (auto dest!: count_image_mset_multi_member_split_2) then show False using dist tauto by (auto simp: atm_of_eq_atm_of tautology_add_mset) qed then have card: ‹size ?C = card (set_mset ?C)› using distinct_mset_size_eq_card by blast have size: ‹size ?C = size C› using dist tauto by (induction C) (auto simp: tautology_add_mset) have m: ‹set_mset ?C ⊆ {0..unat32_max div 2}› proof fix L assume ‹L ∈ set_mset ?C› then have ‹L ∈ atms_of (ℒ_a_l_l 𝒜_i_n)› using lits by (auto simp: literals_are_in_ℒ_i_n_def atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff) then have ‹Neg L ∈# (ℒ_a_l_l 𝒜_i_n)› using lits by (auto simp: in_ℒ_a_l_l_atm_of_in_atms_of_iff) then have ‹nat_of_lit (Neg L) ≤ unat32_max› using in_ℒ_a_l_l_less_unat32_max by (auto simp: atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff) then have ‹L ≤ unat32_max div 2› by (auto simp: atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff subset_iff unat32_max_def) then show ‹L ∈ {0 .. unat32_max div 2}› by (auto simp: atm_of_lit_in_atms_of unat32_max_def in_all_lits_of_m_ain_atms_of_iff subset_iff) qed moreover have ‹card … = 1 + unat32_max div 2› by auto ultimately have ‹card (set_mset ?C) ≤ 1 + unat32_max div 2› using card_mono[OF _ m] by auto then show ?thesis unfolding card[symmetric] size . qed lemma clss_size_unat32_max: assumes lits: ‹literals_are_in_ℒ_i_n 𝒜_i_n C› and dist: ‹distinct_mset C› shows ‹size C ≤ unat32_max + 2› proof - let ?posC = ‹filter_mset is_pos C› let ?negC = ‹filter_mset is_neg C› have C: ‹C = ?posC + ?negC› apply (subst multiset_partition[of _ is_pos]) by auto have ‹literals_are_in_ℒ_i_n 𝒜_i_n ?posC› by (rule literals_are_in_ℒ_i_n_mono[OF lits]) auto moreover have ‹distinct_mset ?posC› by (rule distinct_mset_mono[OF _dist]) auto ultimately have pos: ‹size ?posC ≤ 1 + unat32_max div 2› by (rule simple_clss_size_upper_div2) (auto simp: tautology_decomp) have ‹literals_are_in_ℒ_i_n 𝒜_i_n ?negC› by (rule literals_are_in_ℒ_i_n_mono[OF lits]) auto moreover have ‹distinct_mset ?negC› by (rule distinct_mset_mono[OF _dist]) auto ultimately have neg: ‹size ?negC ≤ 1 + unat32_max div 2› by (rule simple_clss_size_upper_div2) (auto simp: tautology_decomp) show ?thesis apply (subst C) apply (subst size_union) using pos neg by linarith qed lemma clss_size_upper: assumes lits: ‹literals_are_in_ℒ_i_n 𝒜_i_n C› and dist: ‹distinct_mset C› and in_ℒ_a_l_l_less_unat32_max: ‹∀L ∈# ℒ_a_l_l 𝒜_i_n. nat_of_lit L < unat32_max - 1› shows ‹size C ≤ unat32_max› proof - let ?A = ‹remdups_mset (atm_of `# C)› have [simp]: ‹distinct_mset (poss ?A)› ‹distinct_mset (negs ?A)› by (simp_all add: distinct_image_mset_inj inj_on_def) have ‹C ⊆# poss ?A + negs ?A› apply (rule distinct_subseteq_iff[THEN iffD1]) subgoal by (auto simp: dist distinct_mset_add disjunct_not_in) subgoal apply rule using literal.exhaust_sel by (auto simp: image_iff ) done have [simp]: ‹literals_are_in_ℒ_i_n 𝒜_i_n (poss ?A)› ‹literals_are_in_ℒ_i_n 𝒜_i_n (negs ?A)› using lits by (auto simp: literals_are_in_ℒ_i_n_negs_remdups_mset literals_are_in_ℒ_i_n_poss_remdups_mset) have ‹¬ tautology (poss ?A)› ‹¬ tautology (negs ?A)› by (auto simp: tautology_decomp) then have ‹size (poss ?A) ≤ unat32_max div 2› and ‹size (negs ?A) ≤ unat32_max div 2› using simple_clss_size_upper_div2'[of ‹poss ?A›] simple_clss_size_upper_div2'[of ‹negs ?A›] in_ℒ_a_l_l_less_unat32_max by auto then have ‹size C ≤ unat32_max div 2 + unat32_max div 2› using ‹C ⊆# poss (remdups_mset (atm_of `# C)) + negs (remdups_mset (atm_of `# C))› size_mset_mono by fastforce then show ?thesis by (auto simp: unat32_max_def) qed lemma assumes lits: ‹literals_are_in_ℒ_i_n_trail 𝒜_i_n M› and n_d: ‹no_dup M› shows literals_are_in_ℒ_i_n_trail_length_le_unat32_max: ‹length M ≤ Suc (unat32_max div 2)› and literals_are_in_ℒ_i_n_trail_count_decided_unat32_max: ‹count_decided M ≤ Suc (unat32_max div 2)› and literals_are_in_ℒ_i_n_trail_get_level_unat32_max: ‹get_level M L ≤ Suc (unat32_max div 2)› proof - have ‹length M = card (atm_of ` lits_of_l M)› using no_dup_length_eq_card_atm_of_lits_of_l[OF n_d] . moreover have ‹atm_of ` lits_of_l M ⊆ set_mset 𝒜_i_n› using lits unfolding literals_are_in_ℒ_i_n_trail_atm_of by auto ultimately have ‹length M ≤ card (set_mset 𝒜_i_n)› by (simp add: card_mono) moreover { have ‹set_mset 𝒜_i_n ⊆ {0 ..< (unat32_max div 2) + 1}› using in_𝒜_i_n_less_than_unat32_max_div_2 by (fastforce simp: in_ℒ_a_l_l_atm_of_in_atms_of_iff Ball_def atms_of_ℒ_a_l_l_𝒜_i_n unat32_max_def) from subset_eq_atLeast0_lessThan_card[OF this] have ‹card (set_mset 𝒜_i_n) ≤ unat32_max div 2 + 1› . } ultimately show ‹length M ≤ Suc (unat32_max div 2)› by linarith moreover have ‹count_decided M ≤ length M› unfolding count_decided_def by auto ultimately show ‹count_decided M ≤ Suc (unat32_max div 2)› by simp then show ‹get_level M L ≤ Suc (unat32_max div 2)› using count_decided_ge_get_level[of M L] by simp qed lemma length_trail_unat32_max_div2: fixes M :: ‹(nat, 'b) ann_lits› assumes M_ℒ_a_l_l: ‹∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜_i_n› and n_d: ‹no_dup M› shows ‹length M ≤ unat32_max div 2 + 1› proof - have dist_atm_M: ‹distinct_mset {#atm_of (lit_of x). x ∈# mset M#}› using n_d by (metis distinct_mset_mset_distinct mset_map no_dup_def) have incl: ‹atm_of `# lit_of `# mset M ⊆# remdups_mset (atm_of `# ℒ_a_l_l 𝒜_i_n)› apply (subst distinct_subseteq_iff[THEN iffD1]) using assms dist_atm_M by (auto 5 5 simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def no_dup_distinct atm_of_eq_atm_of) have inj_on: ‹inj_on nat_of_lit (set_mset (remdups_mset (ℒ_a_l_l 𝒜_i_n)))› by (auto simp: inj_on_def) have H: ‹xa ∈# ℒ_a_l_l 𝒜_i_n ⟹ atm_of xa ≤ unat32_max div 2› for xa using in_ℒ_a_l_l_less_unat32_max by (cases xa) (auto simp: unat32_max_def) have ‹remdups_mset (atm_of `# ℒ_a_l_l 𝒜_i_n) ⊆# mset [0..< 1 + (unat32_max div 2)]› apply (subst distinct_subseteq_iff[THEN iffD1]) using H distinct_image_mset_inj[OF inj_on] by (force simp del: literal_of_nat.simps simp: distinct_mset_mset_set dest: le_neq_implies_less)+ note _ = size_mset_mono[OF this] moreover have ‹size (nat_of_lit `# remdups_mset (ℒ_a_l_l 𝒜_i_n)) = size (remdups_mset (ℒ_a_l_l 𝒜_i_n))› by simp ultimately have 2: ‹size (remdups_mset (atm_of `# (ℒ_a_l_l 𝒜_i_n))) ≤ 1 + unat32_max div 2› by auto from size_mset_mono[OF incl] have 1: ‹length M ≤ size (remdups_mset (atm_of `# (ℒ_a_l_l 𝒜_i_n)))› unfolding unat32_max_def count_decided_def by (auto simp del: length_filter_le) with 2 show ?thesis by (auto simp: unat32_max_def) qed end end section ‹Instantion for code generation› instantiation literal :: (default) default begin definition default_literal where ‹default_literal = Pos default› instance by standard end instantiation fmap :: (type, type) default begin definition default_fmap where ‹default_fmap = fmempty› instance by standard end subsection ‹Literals as Natural Numbers› definition propagated where ‹propagated L C = (L, Some C)› definition decided where ‹decided L = (L, None)› definition uminus_lit_imp :: ‹nat ⇒ nat› where ‹uminus_lit_imp L = L XOR 1› lemma uminus_lit_imp_uminus: ‹(RETURN o uminus_lit_imp, RETURN o uminus) ∈ nat_lit_rel →_f ⟨nat_lit_rel⟩nres_rel› unfolding bitXOR_1_if_mod_2 uminus_lit_imp_def by (intro frefI nres_relI) (auto simp: uminus_lit_imp_def case_prod_beta p2rel_def br_def nat_lit_rel_def split: option.splits, presburger) subsection ‹State Conversion› subsubsection ‹Functions and Types:› subsubsection ‹More Operations› subsection ‹Code Generation› subsubsection ‹More Operations› definition literals_to_update_wl_empty :: ‹nat twl_st_wl ⇒ bool› where ‹literals_to_update_wl_empty = (λ(M, N, D, NE, UE, Q, W). Q = {#})› lemma in_nat_list_rel_list_all2_in_set_iff: ‹(a, aa) ∈ nat_lit_rel ⟹ list_all2 (λx x'. (x, x') ∈ nat_lit_rel) b ba ⟹ a ∈ set b ⟷ aa ∈ set ba› apply (subgoal_tac ‹length b = length ba›) subgoal apply (rotate_tac 2) apply (induction b ba rule: list_induct2) apply (solves simp) apply (auto simp: p2rel_def nat_lit_rel_def br_def, presburger)[] done subgoal using list_all2_lengthD by auto done definition is_decided_wl where ‹is_decided_wl L ⟷ snd L = None› definition get_maximum_level_remove where ‹get_maximum_level_remove M D L = get_maximum_level M (remove1_mset L D)› lemma in_list_all2_ex_in: ‹a ∈ set xs ⟹ list_all2 R xs ys ⟹ ∃b ∈ set ys. R a b› apply (subgoal_tac ‹length xs = length ys›) apply (rotate_tac 2) apply (induction xs ys rule: list_induct2) apply ((solves auto)+)[2] using list_all2_lengthD by blast definition find_decomp_wl_imp :: ‹(nat, nat) ann_lits ⇒ nat clause ⇒ nat literal ⇒ (nat, nat) ann_lits nres› where ‹find_decomp_wl_imp = (λM₀ D L. do { let lev = get_maximum_level M₀ (remove1_mset (-L) D); let k = count_decided M₀; (_, M) ← WHILE_T⇗λ(j, M). j = count_decided M ∧ j ≥ lev ∧ (M = [] ⟶ j = lev) ∧ (∃M'. M₀ = M' @ M ∧ (j = lev ⟶ M' ≠ [] ∧ is_decided (last M')))⇖ (λ(j, M). j > lev) (λ(j, M). do { ASSERT(M ≠ []); if is_decided (hd M) then RETURN (j-1, tl M) else RETURN (j, tl M)} ) (k, M₀); RETURN M })› lemma ex_decomp_get_ann_decomposition_iff: ‹(∃M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)) ⟷ (∃M2. M = M2 @ Decided K # M1)› using get_all_ann_decomposition_ex by fastforce lemma count_decided_tl_if: ‹M ≠ [] ⟹ count_decided (tl M) = (if is_decided (hd M) then count_decided M - 1 else count_decided M)› by (cases M) auto lemma count_decided_butlast: ‹count_decided (butlast xs) = (if is_decided (last xs) then count_decided xs - 1 else count_decided xs)› by (cases xs rule: rev_cases) (auto simp: count_decided_def) definition find_decomp_wl' where ‹find_decomp_wl' = (λ(M::(nat, nat) ann_lits) (D::nat clause) (L::nat literal). SPEC(λM1. ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧ get_level M K = get_maximum_level M (D - {#-L#}) + 1))› definition get_conflict_wl_is_None :: ‹nat twl_st_wl ⇒ bool› where ‹get_conflict_wl_is_None = (λ(M, N, D, NE, UE, Q, W). is_None D)› lemma get_conflict_wl_is_None: ‹get_conflict_wl S = None ⟷ get_conflict_wl_is_None S› by (cases S) (auto simp: get_conflict_wl_is_None_def split: option.splits) lemma hd_decided_count_decided_ge_1: ‹x ≠ [] ⟹ is_decided (hd x) ⟹ Suc 0 ≤ count_decided x› by (cases x) auto definition (in -) find_decomp_wl_imp' :: ‹(nat, nat) ann_lits ⇒ nat clause_l list ⇒ nat ⇒ nat clause ⇒ nat clauses ⇒ nat clauses ⇒ nat lit_queue_wl ⇒ (nat literal ⇒ nat watched) ⇒ _ ⇒ (nat, nat) ann_lits nres› where ‹find_decomp_wl_imp' = (λM N U D NE UE W Q L. find_decomp_wl_imp M D L)› definition is_decided_hd_trail_wl where ‹is_decided_hd_trail_wl S = is_decided (hd (get_trail_wl S))› definition is_decided_hd_trail_wll :: ‹nat twl_st_wl ⇒ bool nres› where ‹is_decided_hd_trail_wll = (λ(M, N, D, NE, UE, Q, W). RETURN (is_decided (hd M)) )› lemma Propagated_eq_ann_lit_of_pair_iff: ‹Propagated x21 x22 = ann_lit_of_pair (a, b) ⟷ x21 = a ∧ b = Some x22› by (cases b) auto lemma set_mset_all_lits_of_mm_atms_of_ms_iff: ‹set_mset (all_lits_of_mm A) = set_mset (ℒ_a_l_l 𝒜) ⟷ atms_of_ms (set_mset A) = atms_of (ℒ_a_l_l 𝒜)› by (force simp add: atms_of_s_def in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def atms_of_ℒ_a_l_l_𝒜_i_n atms_of_def atm_of_eq_atm_of uminus_𝒜_i_n_iff eq_commute[of ‹set_mset (all_lits_of_mm _)› ‹set_mset (ℒ_a_l_l _)›] dest: multi_member_split) section ‹Polarities› type_synonym tri_bool = ‹bool option› definition UNSET :: ‹tri_bool› where [simp]: ‹UNSET = None› definition SET_FALSE :: ‹tri_bool› where [simp]: ‹SET_FALSE = Some False› definition SET_TRUE :: ‹tri_bool› where [simp]: ‹SET_TRUE = Some True› definition (in -) tri_bool_eq :: ‹tri_bool ⇒ tri_bool ⇒ bool› where ‹tri_bool_eq = (=)› end