Theory DPLL_W

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: (* \htmllink{wf_dpllW} *)
  "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: (* \htmllink{dpllW_conclusive_state} *)
  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