theory DPLL_W imports Entailment_Definition.Partial_Herbrand_Interpretation Entailment_Definition.Partial_Annotated_Herbrand_Interpretation Weidenbach_Book_Base.Wellfounded_More begin section ‹Weidenbach's DPLL› subsection ‹Rules› type_synonym 'a dpll⇩W_ann_lit = "('a, unit) ann_lit" type_synonym 'a dpll⇩W_ann_lits = "('a, unit) ann_lits" type_synonym 'v dpll⇩W_state = "'v dpll⇩W_ann_lits × 'v clauses" abbreviation trail :: "'v dpll⇩W_state ⇒ 'v dpll⇩W_ann_lits" where "trail ≡ fst" abbreviation clauses :: "'v dpll⇩W_state ⇒ 'v clauses" where "clauses ≡ snd" inductive dpll⇩W :: "'v dpll⇩W_state ⇒ 'v dpll⇩W_state ⇒ bool" where propagate: "add_mset L C ∈# clauses S ⟹ trail S ⊨as CNot C ⟹ undefined_lit (trail S) L ⟹ dpll⇩W S (Propagated L () # trail S, clauses S)" | decided: "undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_mm (clauses S) ⟹ dpll⇩W S (Decided L # trail S, clauses S)" | backtrack: "backtrack_split (trail S) = (M', L # M) ⟹ is_decided L ⟹ D ∈# clauses S ⟹ trail S ⊨as CNot D ⟹ dpll⇩W S (Propagated (- (lit_of L)) () # M, clauses S)" subsection ‹Invariants› lemma dpll⇩W_distinct_inv: assumes "dpll⇩W S S'" and "no_dup (trail S)" shows "no_dup (trail S')" using assms proof (induct rule: dpll⇩W.induct) case (decided L S) then show ?case using defined_lit_map by force next case (propagate C L S) then show ?case using defined_lit_map by force next case (backtrack S M' L M D) note extracted = this(1) and no_dup = this(5) show ?case using no_dup backtrack_split_list_eq[of "trail S", symmetric] unfolding extracted by (auto dest: no_dup_appendD) qed lemma dpll⇩W_consistent_interp_inv: assumes "dpll⇩W S S'" and "consistent_interp (lits_of_l (trail S))" and "no_dup (trail S)" shows "consistent_interp (lits_of_l (trail S'))" using assms proof (induct rule: dpll⇩W.induct) case (backtrack S M' L M D) note extracted = this(1) and decided = this(2) and D = this(4) and cons = this(5) and no_dup = this(6) have no_dup': "no_dup M" by (metis (no_types) backtrack_split_list_eq distinct.simps(2) distinct_append extracted list.simps(9) map_append no_dup snd_conv no_dup_def) then have "insert (lit_of L) (lits_of_l M) ⊆ lits_of_l (trail S)" using backtrack_split_list_eq[of "trail S", symmetric] unfolding extracted by auto then have cons: "consistent_interp (insert (lit_of L) (lits_of_l M))" using consistent_interp_subset cons by blast moreover have undef: "undefined_lit M (lit_of L)" using no_dup backtrack_split_list_eq[of "trail S", symmetric] unfolding extracted by force moreover have "lit_of L ∉ lits_of_l M" using undef by (auto simp: Decided_Propagated_in_iff_in_lits_of_l) ultimately show ?case by simp qed (auto intro: consistent_add_undefined_lit_consistent) lemma dpll⇩W_vars_in_snd_inv: assumes "dpll⇩W S S'" and "atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (clauses S)" shows "atm_of ` (lits_of_l (trail S')) ⊆ atms_of_mm (clauses S')" using assms proof (induct rule: dpll⇩W.induct) case (backtrack S M' L M D) then have "atm_of (lit_of L) ∈ atms_of_mm (clauses S)" using backtrack_split_list_eq[of "trail S", symmetric] by auto moreover have "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" using backtrack(5) by simp then have "⋀xb. xb ∈ set M ⟹ atm_of (lit_of xb) ∈ atms_of_mm (clauses S)" using backtrack_split_list_eq[symmetric, of "trail S"] backtrack.hyps(1) unfolding lits_of_def by auto ultimately show ?case by (auto simp : lits_of_def) qed (auto simp: in_plus_implies_atm_of_on_atms_of_ms) lemma atms_of_ms_lit_of_atms_of: "atms_of_ms (unmark ` c) = atm_of ` lit_of ` c" unfolding atms_of_ms_def using image_iff by force text ‹\cwref{dpll:sound:model}{theorem 2.8.3 page 86}› lemma dpll⇩W_propagate_is_conclusion: assumes "dpll⇩W S S'" and "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" shows "all_decomposition_implies_m (clauses S') (get_all_ann_decomposition (trail S'))" using assms proof (induct rule: dpll⇩W.induct) case (decided L S) then show ?case unfolding all_decomposition_implies_def by simp next case (propagate L C S) note inS = this(1) and cnot = this(2) and IH = this(4) and undef = this(3) and atms_incl = this(5) let ?I = "set (map unmark (trail S)) ∪ set_mset (clauses S)" have "?I ⊨p add_mset L C" by (auto simp add: inS) moreover have "?I ⊨ps CNot C" using true_annots_true_clss_cls cnot by fastforce ultimately have "?I ⊨p {#L#}" using true_clss_cls_plus_CNot[of ?I L C] inS by blast { assume "get_all_ann_decomposition (trail S) = []" then have ?case by blast } moreover { assume n: "get_all_ann_decomposition (trail S) ≠ []" have 1: "⋀a b. (a, b) ∈ set (tl (get_all_ann_decomposition (trail S))) ⟹ (unmark_l a ∪ set_mset (clauses S)) ⊨ps unmark_l b" using IH unfolding all_decomposition_implies_def by (fastforce simp add: list.set_sel(2) n) moreover have 2: "⋀a c. hd (get_all_ann_decomposition (trail S)) = (a, c) ⟹ (unmark_l a ∪ set_mset (clauses S)) ⊨ps (unmark_l c)" by (metis IH all_decomposition_implies_cons_pair all_decomposition_implies_single list.collapse n) moreover have 3: "⋀a c. hd (get_all_ann_decomposition (trail S)) = (a, c) ⟹ (unmark_l a ∪ set_mset (clauses S)) ⊨p {#L#}" proof - fix a c assume h: "hd (get_all_ann_decomposition (trail S)) = (a, c)" have h': "trail S = c @ a" using get_all_ann_decomposition_decomp h by blast have I: "set (map unmark a) ∪ set_mset (clauses S) ∪ unmark_l c ⊨ps CNot C" using ‹?I ⊨ps CNot C› unfolding h' by (simp add: Un_commute Un_left_commute) have "atms_of_ms (CNot C) ⊆ atms_of_ms (set (map unmark a) ∪ set_mset (clauses S))" and "atms_of_ms (unmark_l c) ⊆ atms_of_ms (set (map unmark a) ∪ set_mset (clauses S))" using atms_incl cnot apply (auto simp: atms_of_def dest!: true_annots_CNot_all_atms_defined; fail)[] using inS atms_of_atms_of_ms_mono atms_incl by (fastforce simp: h') then have "unmark_l a ∪ set_mset (clauses S) ⊨ps CNot C" using true_clss_clss_left_right[OF _ I] h "2" by auto then show "unmark_l a ∪ set_mset (clauses S) ⊨p {#L#}" using inS true_clss_cls_plus_CNot true_clss_clss_in_imp_true_clss_cls union_trus_clss_clss by blast qed ultimately have ?case by (cases "hd (get_all_ann_decomposition (trail S))") (auto simp: all_decomposition_implies_def) } ultimately show ?case by auto next case (backtrack S M' L M D) note extracted = this(1) and decided = this(2) and D = this(3) and cnot = this(4) and cons = this(4) and IH = this(5) and atms_incl = this(6) have S: "trail S = M' @ L # M" using backtrack_split_list_eq[of "trail S"] unfolding extracted by auto have M': "∀l ∈ set M'. ¬is_decided l" using extracted backtrack_split_fst_not_decided[of _ "trail S"] by simp have n: "get_all_ann_decomposition (trail S) ≠ []" by auto then have "all_decomposition_implies_m (clauses S) ((L # M, M') # tl (get_all_ann_decomposition (trail S)))" by (metis (no_types) IH extracted get_all_ann_decomposition_backtrack_split list.exhaust_sel) then have 1: "unmark_l (L # M) ∪ set_mset (clauses S) ⊨ps(λa.{#lit_of a#}) ` set M'" by simp moreover have "unmark_l (L # M) ∪ unmark_l M' ⊨ps CNot D" by (metis (mono_tags, lifting) S Un_commute cons image_Un set_append true_annots_true_clss_clss) then have 2: "unmark_l (L # M) ∪ set_mset (clauses S) ∪ unmark_l M' ⊨ps CNot D" by (metis (no_types, lifting) Un_assoc Un_left_commute true_clss_clss_union_l_r) ultimately have "set (map unmark (L # M)) ∪ set_mset (clauses S) ⊨ps CNot D" using true_clss_clss_left_right by fastforce then have "set (map unmark (L # M)) ∪ set_mset (clauses S) ⊨p {#}" by (metis (mono_tags, lifting) D Un_def mem_Collect_eq true_clss_clss_contradiction_true_clss_cls_false) then have IL: "unmark_l M ∪ set_mset (clauses S) ⊨p {#-lit_of L#}" using true_clss_clss_false_left_right by auto show ?case unfolding S all_decomposition_implies_def proof fix x P level assume x: "x ∈ set (get_all_ann_decomposition (fst (Propagated (- lit_of L) P # M, clauses S)))" let ?M' = "Propagated (- lit_of L) P # M" let ?hd = "hd (get_all_ann_decomposition ?M')" let ?tl = "tl (get_all_ann_decomposition ?M')" have "x = ?hd ∨ x ∈ set ?tl" using x by (cases "get_all_ann_decomposition ?M'") auto moreover { assume x': "x ∈ set ?tl" have L': "Decided (lit_of L) = L" using decided by (cases L, auto) have "x ∈ set (get_all_ann_decomposition (M' @ L # M))" using x' get_all_ann_decomposition_except_last_choice_equal[of M' "lit_of L" P M] L' by (metis (no_types) M' list.set_sel(2) tl_Nil) then have "case x of (Ls, seen) ⇒ unmark_l Ls ∪ set_mset (clauses S) ⊨ps unmark_l seen" using decided IH by (cases L) (auto simp add: S all_decomposition_implies_def) } moreover { assume x': "x = ?hd" have tl: "tl (get_all_ann_decomposition (M' @ L # M)) ≠ []" proof - have f1: "⋀ms. length (get_all_ann_decomposition (M' @ ms)) = length (get_all_ann_decomposition ms)" by (simp add: M' get_all_ann_decomposition_remove_undecided_length) have "Suc (length (get_all_ann_decomposition M)) ≠ Suc 0" by blast then show ?thesis using f1[of ‹L # M›] decided by (cases ‹get_all_ann_decomposition (M' @ L # M)›; cases L) auto qed obtain M0' M0 where L0: "hd (tl (get_all_ann_decomposition (M' @ L # M))) = (M0, M0')" by (cases "hd (tl (get_all_ann_decomposition (M' @ L # M)))") have x'': "x = (M0, Propagated (-lit_of L) P # M0')" unfolding x' using get_all_ann_decomposition_last_choice tl M' L0 by (smt is_decided_ex_Decided lit_of.simps(1) local.decided old.unit.exhaust) obtain l_get_all_ann_decomposition where "get_all_ann_decomposition (trail S) = (L # M, M') # (M0, M0') # l_get_all_ann_decomposition" using get_all_ann_decomposition_backtrack_split extracted by (metis (no_types) L0 S hd_Cons_tl n tl) then have "M = M0' @ M0" using get_all_ann_decomposition_hd_hd by fastforce then have IL': "unmark_l M0 ∪ set_mset (clauses S) ∪ unmark_l M0' ⊨ps {{#- lit_of L#}}" using IL by (simp add: Un_commute Un_left_commute image_Un) moreover have H: "unmark_l M0 ∪ set_mset (clauses S) ⊨ps unmark_l M0'" using IH x'' unfolding all_decomposition_implies_def by (metis (no_types, lifting) L0 S list.set_sel(1) list.set_sel(2) old.prod.case tl tl_Nil) ultimately have "case x of (Ls, seen) ⇒ unmark_l Ls ∪ set_mset (clauses S) ⊨ps unmark_l seen" using true_clss_clss_left_right unfolding x'' by auto } ultimately show "case x of (Ls, seen) ⇒ unmark_l Ls ∪ set_mset (snd (?M', clauses S)) ⊨ps unmark_l seen" unfolding snd_conv by blast qed qed text ‹\cwref{dpll:sound:propLits:valuation}{theorem 2.8.4 page 86}› theorem dpll⇩W_propagate_is_conclusion_of_decided: assumes "dpll⇩W S S'" and "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" shows "set_mset (clauses S') ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set (trail S')} ⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition (trail S')))" using all_decomposition_implies_trail_is_implied[OF dpll⇩W_propagate_is_conclusion[OF assms]] . text ‹\cwref{dpll:sound:propLits:unsat}{theorem 2.8.5 page 86}› lemma only_propagated_vars_unsat: assumes decided: "∀x ∈ set M. ¬ is_decided x" and DN: "D ∈ N" and D: "M ⊨as CNot D" and inv: "all_decomposition_implies N (get_all_ann_decomposition M)" and atm_incl: "atm_of ` lits_of_l M ⊆ atms_of_ms N" shows "unsatisfiable N" proof (rule ccontr) assume "¬ unsatisfiable N" then obtain I where I: "I ⊨s N" and cons: "consistent_interp I" and tot: "total_over_m I N" unfolding satisfiable_def by auto then have I_D: "I ⊨ D" using DN unfolding true_clss_def by auto have l0: "{{#lit_of L#} |L. is_decided L ∧ L ∈ set M} = {}" using decided by auto have "atms_of_ms (N ∪ unmark_l M) = atms_of_ms N" using atm_incl unfolding atms_of_ms_def lits_of_def by auto then have "total_over_m I (N ∪ unmark ` (set M))" using tot unfolding total_over_m_def by auto then have "I ⊨s unmark ` (set M)" using all_decomposition_implies_propagated_lits_are_implied[OF inv] cons I unfolding true_clss_clss_def l0 by auto then have IM: "I ⊨s unmark_l M" by auto { fix K assume "K ∈# D" then have "-K ∈ lits_of_l M" by (auto split: if_split_asm intro: allE[OF D[unfolded true_annots_def Ball_def], of "{#-K#}"]) then have "-K ∈ I" using IM true_clss_singleton_lit_of_implies_incl by fastforce } then have "¬ I ⊨ D" using cons unfolding true_cls_def consistent_interp_def by auto then show False using I_D by blast qed lemma dpll⇩W_same_clauses: assumes "dpll⇩W S S'" shows "clauses S = clauses S'" using assms by (induct rule: dpll⇩W.induct, auto) lemma rtranclp_dpll⇩W_inv: assumes "rtranclp dpll⇩W S S'" and inv: "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and atm_incl: "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" and "consistent_interp (lits_of_l (trail S))" and "no_dup (trail S)" shows "all_decomposition_implies_m (clauses S') (get_all_ann_decomposition (trail S'))" and "atm_of ` lits_of_l (trail S') ⊆ atms_of_mm (clauses S')" and "clauses S = clauses S'" and "consistent_interp (lits_of_l (trail S'))" and "no_dup (trail S')" using assms proof (induct rule: rtranclp_induct) case base show "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" and "clauses S = clauses S" and "consistent_interp (lits_of_l (trail S))" and "no_dup (trail S)" using assms by auto next case (step S' S'') note dpll⇩WStar = this(1) and IH = this(3,4,5,6,7) and dpll⇩W = this(2) moreover assume inv: "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and atm_incl: "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" and cons: "consistent_interp (lits_of_l (trail S))" and "no_dup (trail S)" ultimately have decomp: "all_decomposition_implies_m (clauses S') (get_all_ann_decomposition (trail S'))" and atm_incl': "atm_of ` lits_of_l (trail S') ⊆ atms_of_mm (clauses S')" and snd: "clauses S = clauses S'" and cons': "consistent_interp (lits_of_l (trail S'))" and no_dup': "no_dup (trail S')" by blast+ show "clauses S = clauses S''" using dpll⇩W_same_clauses[OF dpll⇩W] snd by metis show "all_decomposition_implies_m (clauses S'') (get_all_ann_decomposition (trail S''))" using dpll⇩W_propagate_is_conclusion[OF dpll⇩W] decomp atm_incl' by auto show "atm_of ` lits_of_l (trail S'') ⊆ atms_of_mm (clauses S'')" using dpll⇩W_vars_in_snd_inv[OF dpll⇩W] atm_incl atm_incl' by auto show "no_dup (trail S'')" using dpll⇩W_distinct_inv[OF dpll⇩W] no_dup' dpll⇩W by auto show "consistent_interp (lits_of_l (trail S''))" using cons' no_dup' dpll⇩W_consistent_interp_inv[OF dpll⇩W] by auto qed definition "dpll⇩W_all_inv S ≡ (all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S)) ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S) ∧ consistent_interp (lits_of_l (trail S)) ∧ no_dup (trail S))" lemma dpll⇩W_all_inv_dest[dest]: assumes "dpll⇩W_all_inv S" shows "all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))" and "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" and "consistent_interp (lits_of_l (trail S)) ∧ no_dup (trail S)" using assms unfolding dpll⇩W_all_inv_def lits_of_def by auto lemma rtranclp_dpll⇩W_all_inv: assumes "rtranclp dpll⇩W S S'" and "dpll⇩W_all_inv S" shows "dpll⇩W_all_inv S'" using assms rtranclp_dpll⇩W_inv[OF assms(1)] unfolding dpll⇩W_all_inv_def lits_of_def by blast lemma dpll⇩W_all_inv: assumes "dpll⇩W S S'" and "dpll⇩W_all_inv S" shows "dpll⇩W_all_inv S'" using assms rtranclp_dpll⇩W_all_inv by blast lemma rtranclp_dpll⇩W_inv_starting_from_0: assumes "rtranclp dpll⇩W S S'" and inv: "trail S = []" shows "dpll⇩W_all_inv S'" proof - have "dpll⇩W_all_inv S" using assms unfolding all_decomposition_implies_def dpll⇩W_all_inv_def by auto then show ?thesis using rtranclp_dpll⇩W_all_inv[OF assms(1)] by blast qed lemma dpll⇩W_can_do_step: assumes "consistent_interp (set M)" and "distinct M" and "atm_of ` (set M) ⊆ atms_of_mm N" shows "rtranclp dpll⇩W ([], N) (map Decided M, N)" using assms proof (induct M) case Nil then show ?case by auto next case (Cons L M) then have "undefined_lit (map Decided M) L" unfolding defined_lit_def consistent_interp_def by auto moreover have "atm_of L ∈ atms_of_mm N" using Cons.prems(3) by auto ultimately have "dpll⇩W (map Decided M, N) (map Decided (L # M), N)" using dpll⇩W.decided by auto moreover have "consistent_interp (set M)" and "distinct M" and "atm_of ` set M ⊆ atms_of_mm N" using Cons.prems unfolding consistent_interp_def by auto ultimately show ?case using Cons.hyps by auto qed definition "conclusive_dpll⇩W_state (S:: 'v dpll⇩W_state) ⟷ (trail S ⊨asm clauses S ∨ ((∀L ∈ set (trail S). ¬is_decided L) ∧ (∃C ∈# clauses S. trail S ⊨as CNot C)))" text ‹\cwref{prop:prop:dpllcomplete}{theorem 2.8.7 page 87}› lemma dpll⇩W_strong_completeness: assumes "set M ⊨sm N" and "consistent_interp (set M)" and "distinct M" and "atm_of ` (set M) ⊆ atms_of_mm N" shows "dpll⇩W⇧*⇧* ([], N) (map Decided M, N)" and "conclusive_dpll⇩W_state (map Decided M, N)" proof - show "rtranclp dpll⇩W ([], N) (map Decided M, N)" using dpll⇩W_can_do_step assms by auto have "map Decided M ⊨asm N" using assms(1) true_annots_decided_true_cls by auto then show "conclusive_dpll⇩W_state (map Decided M, N)" unfolding conclusive_dpll⇩W_state_def by auto qed text ‹\cwref{prop:prop:dpllsound}{theorem 2.8.6 page 86}› lemma dpll⇩W_sound: assumes "rtranclp dpll⇩W ([], N) (M, N)" and "∀S. ¬dpll⇩W (M, N) S" shows "M ⊨asm N ⟷ satisfiable (set_mset N)" (is "?A ⟷ ?B") proof let ?M'= "lits_of_l M" assume ?A then have "?M' ⊨sm N" by (simp add: true_annots_true_cls) moreover have "consistent_interp ?M'" using rtranclp_dpll⇩W_inv_starting_from_0[OF assms(1)] by auto ultimately show ?B by auto next assume ?B show ?A proof (rule ccontr) assume n: "¬ ?A" have "(∃L. undefined_lit M L ∧ atm_of L ∈ atms_of_mm N) ∨ (∃D∈#N. M ⊨as CNot D)" proof - obtain D :: "'a clause" where D: "D ∈# N" and "¬ M ⊨a D" using n unfolding true_annots_def Ball_def by auto then have "(∃L. undefined_lit M L ∧ atm_of L ∈ atms_of D) ∨ M ⊨as CNot D" unfolding true_annots_def Ball_def CNot_def true_annot_def using atm_of_lit_in_atms_of true_annot_iff_decided_or_true_lit true_cls_def by (smt mem_Collect_eq union_single_eq_member) then show ?thesis by (metis Bex_def D atms_of_atms_of_ms_mono rev_subsetD) qed moreover { assume "∃L. undefined_lit M L ∧ atm_of L ∈ atms_of_mm N" then have False using assms(2) decided by fastforce } moreover { assume "∃D∈#N. M ⊨as CNot D" then obtain D where DN: "D ∈# N" and MD: "M ⊨as CNot D" by auto { assume "∀l ∈ set M. ¬ is_decided l" moreover have "dpll⇩W_all_inv ([], N)" using assms unfolding all_decomposition_implies_def dpll⇩W_all_inv_def by auto ultimately have "unsatisfiable (set_mset N)" using only_propagated_vars_unsat[of M D "set_mset N"] DN MD rtranclp_dpll⇩W_all_inv[OF assms(1)] by force then have False using ‹?B› by blast } moreover { assume l: "∃l ∈ set M. is_decided l" then have False using backtrack[of "(M, N)" _ _ _ D ] DN MD assms(2) backtrack_split_some_is_decided_then_snd_has_hd[OF l] by (metis backtrack_split_snd_hd_decided fst_conv list.distinct(1) list.sel(1) snd_conv) } ultimately have False by blast } ultimately show False by blast qed qed subsection ‹Termination› definition "dpll⇩W_mes M n = map (λl. if is_decided l then 2 else (1::nat)) (rev M) @ replicate (n - length M) 3" lemma length_dpll⇩W_mes: assumes "length M ≤ n" shows "length (dpll⇩W_mes M n) = n" using assms unfolding dpll⇩W_mes_def by auto lemma distinctcard_atm_of_lit_of_eq_length: assumes "no_dup S" shows "card (atm_of ` lits_of_l S) = length S" using assms by (induct S) (auto simp add: image_image lits_of_def no_dup_def) lemma Cons_lexn_iff: shows ‹(x # xs, y # ys) ∈ lexn R n ⟷ (length (x # xs) = n ∧ length (y # ys) = n ∧ ((x,y) ∈ R ∨ (x = y ∧ (xs, ys) ∈ lexn R (n - 1))))› unfolding lexn_conv apply (rule iffI; clarify) subgoal for xys xa ya xs' ys' by (cases xys) (auto simp: lexn_conv) subgoal by (auto 5 5 simp: lexn_conv simp del: append_Cons simp: append_Cons[symmetric]) done declare append_same_lexn[simp] prepend_same_lexn[simp] Cons_lexn_iff[simp] declare lexn.simps(2)[simp del] lemma dpll⇩W_card_decrease: assumes dpll: "dpll⇩W S S'" and [simp]: "length (trail S') ≤ card vars" and "length (trail S) ≤ card vars" shows "(dpll⇩W_mes (trail S') (card vars), dpll⇩W_mes (trail S) (card vars)) ∈ lexn less_than (card vars)" using assms proof (induct rule: dpll⇩W.induct) case (propagate C L S) then have m: "card vars - length (trail S) = Suc (card vars - Suc (length (trail S)))" by fastforce then show ‹(dpll⇩W_mes (trail (Propagated C () # trail S, clauses S)) (card vars), dpll⇩W_mes (trail S) (card vars)) ∈ lexn less_than (card vars)› unfolding dpll⇩W_mes_def by auto next case (decided S L) have m: "card vars - length (trail S) = Suc (card vars - Suc (length (trail S)))" using decided.prems[simplified] using Suc_diff_le by fastforce then show ‹(dpll⇩W_mes (trail (Decided L # trail S, clauses S)) (card vars), dpll⇩W_mes (trail S) (card vars)) ∈ lexn less_than (card vars)› unfolding dpll⇩W_mes_def by auto next case (backtrack S M' L M D) moreover have S: "trail S = M' @ L # M" using backtrack.hyps(1) backtrack_split_list_eq[of "trail S"] by auto ultimately show ‹(dpll⇩W_mes (trail (Propagated (- lit_of L) () # M, clauses S)) (card vars), dpll⇩W_mes (trail S) (card vars)) ∈ lexn less_than (card vars)› using backtrack_split_list_eq[of "trail S"] unfolding dpll⇩W_mes_def by fastforce qed text ‹\cwref{prop:prop:dpllterminating}{theorem 2.8.8 page 87}› lemma dpll⇩W_card_decrease': assumes dpll: "dpll⇩W S S'" and atm_incl: "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm (clauses S)" and no_dup: "no_dup (trail S)" shows "(dpll⇩W_mes (trail S') (card (atms_of_mm (clauses S'))), dpll⇩W_mes (trail S) (card (atms_of_mm (clauses S)))) ∈ lex less_than" proof - have "finite (atms_of_mm (clauses S))" unfolding atms_of_ms_def by auto then have 1: "length (trail S) ≤ card (atms_of_mm (clauses S))" using distinctcard_atm_of_lit_of_eq_length[OF no_dup] atm_incl card_mono by metis moreover { have no_dup': "no_dup (trail S')" using dpll dpll⇩W_distinct_inv no_dup by blast have SS': "clauses S' = clauses S" using dpll by (auto dest!: dpll⇩W_same_clauses) have atm_incl': "atm_of ` lits_of_l (trail S') ⊆ atms_of_mm (clauses S')" using atm_incl dpll dpll⇩W_vars_in_snd_inv[OF dpll] by force have "finite (atms_of_mm (clauses S'))" unfolding atms_of_ms_def by auto then have 2: "length (trail S') ≤ card (atms_of_mm (clauses S))" using distinctcard_atm_of_lit_of_eq_length[OF no_dup'] atm_incl' card_mono SS' by metis } ultimately have "(dpll⇩W_mes (trail S') (card (atms_of_mm (clauses S))), dpll⇩W_mes (trail S) (card (atms_of_mm (clauses S)))) ∈ lexn less_than (card (atms_of_mm (clauses S)))" using dpll⇩W_card_decrease[OF assms(1), of "atms_of_mm (clauses S)"] by blast then have "(dpll⇩W_mes (trail S') (card (atms_of_mm (clauses S))), dpll⇩W_mes (trail S) (card (atms_of_mm (clauses S)))) ∈ lex less_than" unfolding lex_def by auto then show "(dpll⇩W_mes (trail S') (card (atms_of_mm (clauses S'))), dpll⇩W_mes (trail S) (card (atms_of_mm (clauses S)))) ∈ lex less_than" using dpll⇩W_same_clauses[OF assms(1)] by auto qed lemma wf_lexn: "wf (lexn {(a, b). (a::nat) < b} (card (atms_of_mm (clauses S))))" proof - have m: "{(a, b). a < b} = measure id" by auto show ?thesis apply (rule wf_lexn) unfolding m by auto qed lemma wf_dpll⇩W: "wf {(S', S). dpll⇩W_all_inv S ∧ dpll⇩W S S'}" apply (rule wf_wf_if_measure'[OF wf_lex_less, of _ _ "λS. dpll⇩W_mes (trail S) (card (atms_of_mm (clauses S)))"]) using dpll⇩W_card_decrease' by fast lemma dpll⇩W_tranclp_star_commute: "{(S', S). dpll⇩W_all_inv S ∧ dpll⇩W S S'}⇧+ = {(S', S). dpll⇩W_all_inv S ∧ tranclp dpll⇩W S S'}" (is "?A = ?B") proof { fix S S' assume "(S, S') ∈ ?A" then have "(S, S') ∈ ?B" by (induct rule: trancl.induct, auto) } then show "?A ⊆ ?B" by blast { fix S S' assume "(S, S') ∈ ?B" then have "dpll⇩W⇧+⇧+ S' S" and "dpll⇩W_all_inv S'" by auto then have "(S, S') ∈ ?A" proof (induct rule: tranclp.induct) case r_into_trancl then show ?case by (simp_all add: r_into_trancl') next case (trancl_into_trancl S S' S'') then have "(S', S) ∈ {a. case a of (S', S) ⇒ dpll⇩W_all_inv S ∧ dpll⇩W S S'}⇧+" by blast moreover have "dpll⇩W_all_inv S'" using rtranclp_dpll⇩W_all_inv[OF tranclp_into_rtranclp[OF trancl_into_trancl.hyps(1)]] trancl_into_trancl.prems by auto ultimately have "(S'', S') ∈ {(pa, p). dpll⇩W_all_inv p ∧ dpll⇩W p pa}⇧+" using ‹dpll⇩W_all_inv S'› trancl_into_trancl.hyps(3) by blast then show ?case using ‹(S', S) ∈ {a. case a of (S', S) ⇒ dpll⇩W_all_inv S ∧ dpll⇩W S S'}⇧+› by auto qed } then show "?B ⊆ ?A" by blast qed lemma wf_dpll⇩W_tranclp: "wf {(S', S). dpll⇩W_all_inv S ∧ dpll⇩W⇧+⇧+ S S'}" unfolding dpll⇩W_tranclp_star_commute[symmetric] by (simp add: wf_dpll⇩W wf_trancl) lemma wf_dpll⇩W_plus: "wf {(S', ([], N))| S'. dpll⇩W⇧+⇧+ ([], N) S'}" (is "wf ?P") apply (rule wf_subset[OF wf_dpll⇩W_tranclp, of ?P]) unfolding dpll⇩W_all_inv_def by auto subsection ‹Final States› text ‹Proposition 2.8.1: final states are the normal forms of @{term dpll⇩W}› lemma dpll⇩W_no_more_step_is_a_conclusive_state: assumes "∀S'. ¬dpll⇩W S S'" shows "conclusive_dpll⇩W_state S" proof - have vars: "∀s ∈ atms_of_mm (clauses S). s ∈ atm_of ` lits_of_l (trail S)" proof (rule ccontr) assume "¬ (∀s∈atms_of_mm (clauses S). s ∈ atm_of ` lits_of_l (trail S))" then obtain L where L_in_atms: "L ∈ atms_of_mm (clauses S)" and L_notin_trail: "L ∉ atm_of ` lits_of_l (trail S)" by metis obtain L' where L': "atm_of L' = L" by (meson literal.sel(2)) then have "undefined_lit (trail S) L'" unfolding Decided_Propagated_in_iff_in_lits_of_l by (metis L_notin_trail atm_of_uminus imageI) then show False using dpll⇩W.decided assms(1) L_in_atms L' by blast qed show ?thesis proof (rule ccontr) assume not_final: "¬ ?thesis" then have "¬ trail S ⊨asm clauses S" and "(∃L∈set (trail S). is_decided L) ∨ (∀C∈#clauses S. ¬trail S ⊨as CNot C)" unfolding conclusive_dpll⇩W_state_def by auto moreover { assume "∃L∈set (trail S). is_decided L" then obtain L M' M where L: "backtrack_split (trail S) = (M', L # M)" using backtrack_split_some_is_decided_then_snd_has_hd by blast obtain D where "D ∈# clauses S" and "¬ trail S ⊨a D" using ‹¬ trail S ⊨asm clauses S› unfolding true_annots_def by auto then have "∀s∈atms_of_ms {D}. s ∈ atm_of ` lits_of_l (trail S)" using vars unfolding atms_of_ms_def by auto then have "trail S ⊨as CNot D" using all_variables_defined_not_imply_cnot[of D] ‹¬ trail S ⊨a D› by auto moreover have "is_decided L" using L by (metis backtrack_split_snd_hd_decided list.distinct(1) list.sel(1) snd_conv) ultimately have False using assms(1) dpll⇩W.backtrack L ‹D ∈# clauses S› ‹trail S ⊨as CNot D› by blast } moreover { assume tr: "∀C∈#clauses S. ¬trail S ⊨as CNot C" obtain C where C_in_cls: "C ∈# clauses S" and trC: "¬ trail S ⊨a C" using ‹¬ trail S ⊨asm clauses S› unfolding true_annots_def by auto have "∀s∈atms_of_ms {C}. s ∈ atm_of ` lits_of_l (trail S)" using vars ‹C ∈# clauses S› unfolding atms_of_ms_def by auto then have "trail S ⊨as CNot C" by (meson C_in_cls tr trC all_variables_defined_not_imply_cnot) then have False using tr C_in_cls by auto } ultimately show False by blast qed qed lemma dpll⇩W_conclusive_state_correct: assumes "dpll⇩W⇧*⇧* ([], N) (M, N)" and "conclusive_dpll⇩W_state (M, N)" shows "M ⊨asm N ⟷ satisfiable (set_mset N)" (is "?A ⟷ ?B") proof let ?M'= "lits_of_l M" assume ?A then have "?M' ⊨sm N" by (simp add: true_annots_true_cls) moreover have "consistent_interp ?M'" using rtranclp_dpll⇩W_inv_starting_from_0[OF assms(1)] by auto ultimately show ?B by auto next assume ?B show ?A proof (rule ccontr) assume n: "¬ ?A" have no_mark: "∀L∈set M. ¬ is_decided L" "∃C ∈# N. M ⊨as CNot C" using n assms(2) unfolding conclusive_dpll⇩W_state_def by auto moreover obtain D where DN: "D ∈# N" and MD: "M ⊨as CNot D" using no_mark by auto ultimately have "unsatisfiable (set_mset N)" using only_propagated_vars_unsat rtranclp_dpll⇩W_all_inv[OF assms(1)] unfolding dpll⇩W_all_inv_def by force then show False using ‹?B› by blast qed qed lemma dpll⇩W_trail_after_step1: assumes ‹dpll⇩W S T› shows ‹∃K' M1 M2' M2''. (rev (trail T) = rev (trail S) @ M2' ∧ M2' ≠ []) ∨ (rev (trail S) = M1 @ Decided (-K') # M2' ∧ rev (trail T) = M1 @ Propagated K' () # M2'' ∧ Suc (length M1) ≤ length (trail S))› using assms apply (induction S T rule: dpll⇩W.induct) subgoal for L C T by auto subgoal by auto subgoal for S M' L M D using backtrack_split_snd_hd_decided[of ‹trail S›] backtrack_split_list_eq[of ‹trail S›, symmetric] apply - apply (rule exI[of _ ‹-lit_of L›], rule exI[of _ ‹rev M›], rule exI[of _ ‹rev M'›], rule exI[of _ ‹[]›]) by (cases L) auto done lemma tranclp_dpll⇩W_trail_after_step: assumes ‹dpll⇩W⇧+⇧+ S T› shows ‹∃K' M1 M2' M2''. (rev (trail T) = rev (trail S) @ M2' ∧ M2' ≠ []) ∨ (rev (trail S) = M1 @ Decided (-K') # M2' ∧ rev (trail T) = M1 @ Propagated K' () # M2'' ∧ Suc (length M1) ≤ length (trail S))› using assms(1) proof (induction rule: tranclp_induct) case (base y) then show ?case by (auto dest!: dpll⇩W_trail_after_step1) next case (step y z) then consider (1) M2' where ‹rev (DPLL_W.trail y) = rev (DPLL_W.trail S) @ M2'› ‹M2' ≠ []› | (2) K' M1 M2' M2'' where ‹rev (DPLL_W.trail S) = M1 @ Decided (- K') # M2'› ‹rev (DPLL_W.trail y) = M1 @ Propagated K' () # M2''› and ‹Suc (length M1) ≤ length (trail S)› by blast then show ?case proof cases case (1 M2') consider (a) M2' where ‹rev (DPLL_W.trail z) = rev (DPLL_W.trail y) @ M2'› ‹M2' ≠ []› | (b) K'' M1' M2'' M2''' where ‹rev (DPLL_W.trail y) = M1' @ Decided (- K'') # M2''› ‹rev (DPLL_W.trail z) = M1' @ Propagated K'' () # M2'''› and ‹Suc (length M1') ≤ length (trail y)› using dpll⇩W_trail_after_step1[OF step(2)] by blast then show ?thesis proof cases case a then show ?thesis using 1 by auto next case b have H: ‹rev (DPLL_W.trail S) @ M2' = M1' @ Decided (- K'') # M2'' ⟹ length M1' ≠ length (DPLL_W.trail S) ⟹ length M1' < Suc (length (DPLL_W.trail S)) ⟹ rev (DPLL_W.trail S) = M1' @ Decided (- K'') # drop (Suc (length M1')) (rev (DPLL_W.trail S))› apply (drule arg_cong[of _ _ ‹take (length (trail S))›]) by (auto simp: take_Cons') show ?thesis using b 1 apply - apply (rule exI[of _ ‹K''›]) apply (rule exI[of _ ‹M1'›]) apply (rule exI[of _ ‹if length (trail S) ≤ length M1' then drop (length (DPLL_W.trail S)) (rev (DPLL_W.trail z)) else drop (Suc (length M1')) (rev (DPLL_W.trail S))›]) apply (cases ‹length (trail S) < length M1'›) subgoal apply auto by (simp add: append_eq_append_conv_if) apply (cases ‹length M1' = length (trail S)›) subgoal by auto subgoal using H apply (clarsimp simp: ) done done qed next case (2 K'' M1' M2'' M2''') consider (a) M2' where ‹rev (DPLL_W.trail z) = rev (DPLL_W.trail y) @ M2'› ‹M2' ≠ []› | (b) K'' M1' M2'' M2''' where ‹rev (DPLL_W.trail y) = M1' @ Decided (- K'') # M2''› ‹rev (DPLL_W.trail z) = M1' @ Propagated K'' () # M2'''› and ‹Suc (length M1') ≤ length (trail y)› using dpll⇩W_trail_after_step1[OF step(2)] by blast then show ?thesis proof cases case a then show ?thesis using 2 by auto next case (b K''' M1'' M2'''' M2''''') have [iff]: ‹M1' @ Propagated K'' () # M2''' = M1'' @ Decided (- K''') # M2'''' ⟷ (∃N1''. M1'' = M1' @ Propagated K'' () # N1'' ∧ M2''' = N1'' @ Decided (- K''') # M2'''')› if ‹length M1' < length M1''› using that apply (auto simp: append_eq_append_conv_if) by (metis (no_types, lifting) Cons_eq_append_conv append_take_drop_id drop_eq_Nil leD) have [iff]: ‹M1' @ Propagated K'' () # M2''' = M1'' @ Decided (- K''') # M2'''' ⟷ (∃N1''. M1' = M1'' @ Decided (- K''') # N1'' ∧ M2'''' = N1'' @ Propagated K'' () # M2''')› if ‹¬length M1' < length M1''› using that apply (auto simp: append_eq_append_conv_if) by (metis (no_types, lifting) Cons_eq_append_conv append_take_drop_id drop_eq_Nil le_eq_less_or_eq) show ?thesis using b 2 apply - apply (rule exI[of _ ‹if length M1' < length M1'' then K'' else K'''›]) apply (rule exI[of _ ‹if length M1' < length M1'' then M1' else M1''›]) apply (cases ‹length (trail S) < min (length M1') (length M1'')›) subgoal by auto apply (cases ‹min (length M1') (length M1'') = length (trail S)›) subgoal by auto subgoal by (auto simp: ) done qed qed qed text ‹ This theorem is an important (although rather obvious) property: the model induced by trails are not repeated. › lemma tranclp_dpll⇩W_no_dup_trail: assumes ‹dpll⇩W⇧+⇧+ S T› and ‹dpll⇩W_all_inv S› shows ‹set (trail S) ≠ set (trail T)› proof - have [simp]: ‹A = B ∪ A ⟷ B ⊆ A› for A B by auto have [simp]: ‹rev (trail U) = xs ⟷trail U = rev xs› for xs U by auto have ‹dpll⇩W_all_inv T› by (metis assms(1) assms(2) reflclp_tranclp rtranclp_dpll⇩W_all_inv sup2CI) then have n_d: ‹no_dup (trail S)› ‹no_dup (trail T)› using assms unfolding dpll⇩W_all_inv_def by (auto dest: no_dup_imp_distinct) have [simp]: ‹no_dup (rev M2' @ DPLL_W.trail S) ⟹ dpll⇩W_all_inv S ⟹ set M2' ⊆ set (DPLL_W.trail S) ⟷ M2' = []› for M2' by (cases M2' rule: rev_cases) (auto simp: undefined_notin) show ?thesis using n_d tranclp_dpll⇩W_trail_after_step[OF assms(1)] assms(2) apply auto by (metis (no_types, lifting) Un_insert_right insertI1 list.simps(15) lit_of.simps(1,2) n_d(1) no_dup_cannot_not_lit_and_uminus set_append set_rev) qed end