Theory CDCL.CDCL_WNOT

theory CDCL_WNOT
imports CDCL_NOT CDCL_W_Merge
begin

section ‹Link between Weidenbach's and NOT's CDCL›
subsection ‹Inclusion of the states›
declare upt.simps(2)[simp del]

fun convert_ann_lit_from_W where
"convert_ann_lit_from_W (Propagated L _) = Propagated L ()" |
"convert_ann_lit_from_W (Decided L) = Decided L"

abbreviation convert_trail_from_W ::
  "('v, 'mark) ann_lits
    ⇒ ('v, unit) ann_lits" where
"convert_trail_from_W ≡ map convert_ann_lit_from_W"

lemma lits_of_l_convert_trail_from_W[simp]:
  "lits_of_l (convert_trail_from_W M) = lits_of_l M"
  by (induction rule: ann_lit_list_induct) simp_all

lemma lit_of_convert_trail_from_W[simp]:
  "lit_of (convert_ann_lit_from_W L) = lit_of L"
  by (cases L) auto

lemma no_dup_convert_from_W[simp]:
  "no_dup (convert_trail_from_W M) ⟷ no_dup M"
  by (auto simp: comp_def no_dup_def)

lemma convert_trail_from_W_true_annots[simp]:
  "convert_trail_from_W M ⊨as C ⟷ M ⊨as C"
  by (auto simp: true_annots_true_cls image_image lits_of_def)

lemma defined_lit_convert_trail_from_W[simp]:
  "defined_lit (convert_trail_from_W S) = defined_lit S"
  by (auto simp: defined_lit_map image_comp intro!: ext)

lemma is_decided_convert_trail_from_W[simp]:
  ‹is_decided (convert_ann_lit_from_W L) = is_decided L›
  by (cases L) auto

lemma count_decided_conver_Trail_from_W[simp]:
  ‹count_decided (convert_trail_from_W M) = count_decided M›
  unfolding count_decided_def by (auto simp: comp_def)

text ‹The values @{term "0::nat"} and @{term "{#}"} are dummy values.›
consts dummy_cls :: 'cls
fun convert_ann_lit_from_NOT
  :: "('v, 'mark) ann_lit ⇒ ('v, 'cls) ann_lit" where
"convert_ann_lit_from_NOT (Propagated L _) = Propagated L dummy_cls" |
"convert_ann_lit_from_NOT (Decided L) = Decided L"

abbreviation convert_trail_from_NOT where
"convert_trail_from_NOT ≡ map convert_ann_lit_from_NOT"

lemma undefined_lit_convert_trail_from_NOT[simp]:
  "undefined_lit (convert_trail_from_NOT F) L ⟷ undefined_lit F L"
  by (induction F rule: ann_lit_list_induct) (auto simp: defined_lit_map)

lemma lits_of_l_convert_trail_from_NOT:
  "lits_of_l (convert_trail_from_NOT F) = lits_of_l F"
  by (induction F rule: ann_lit_list_induct) auto

lemma convert_trail_from_W_from_NOT[simp]:
  "convert_trail_from_W (convert_trail_from_NOT M) = M"
  by (induction rule: ann_lit_list_induct) auto

lemma convert_trail_from_W_convert_lit_from_NOT[simp]:
  "convert_ann_lit_from_W (convert_ann_lit_from_NOT L) = L"
  by (cases L) auto

abbreviation trailNOT where
"trailNOT S ≡ convert_trail_from_W (fst S)"

lemma undefined_lit_convert_trail_from_W[iff]:
  "undefined_lit (convert_trail_from_W M) L ⟷ undefined_lit M L"
  by (auto simp: defined_lit_map image_comp)

lemma lit_of_convert_ann_lit_from_NOT[iff]:
  "lit_of (convert_ann_lit_from_NOT L) = lit_of L"
  by (cases L) auto

sublocale stateW ⊆ dpll_state_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S"
  by unfold_locales

sublocale stateW ⊆ dpll_state where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S"
  by unfold_locales (auto simp: map_tl o_def)

context stateW
begin
declare state_simpNOT[simp del]
end


subsection ‹Inclusion of Weidendenbch's CDCL without Strategy›

sublocale conflict_driven_clause_learningW ⊆ cdclNOT_merge_bj_learn_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = "λ_ _. True" and
  propagate_conds = "λ_ _ _. True" and
  forget_conds =  "λ_ S. conflicting S = None" and
  backjump_l_cond = "λC C' L' S T. backjump_l_cond C C' L' S T
    ∧ distinct_mset C' ∧ L' ∉# C' ∧ ¬tautology (add_mset L' C')"
  by unfold_locales

sublocale conflict_driven_clause_learningW ⊆ cdclNOT_merge_bj_learn_proxy where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = "λ_ _. True" and
  propagate_conds = "λ_ _ _. True" and
  forget_conds =  "λ_ S. conflicting S = None" and
  backjump_l_cond = backjump_l_cond and
  inv = invNOT
  by unfold_locales

sublocale conflict_driven_clause_learningW ⊆ cdclNOT_merge_bj_learn where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = "λ_ _. True" and
  propagate_conds = "λ_ _ _. True" and
  forget_conds =  "λ_ S. conflicting S = None" and
  backjump_l_cond = backjump_l_cond and
  inv = invNOT
proof (unfold_locales, goal_cases)
  case 2
  then show ?case using cdclNOT_merged_bj_learn_no_dup_inv by (auto simp: comp_def)
next
  case (1 C' S C F' K F L)
    let ?C' = "remdups_mset C'"
    have "L ∉# C'"
      using ‹F ⊨as CNot C'› ‹undefined_lit F L› Decided_Propagated_in_iff_in_lits_of_l
      in_CNot_implies_uminus(2) by fast
    then have dist: "distinct_mset ?C'" "L ∉# C'"
      by simp_all

    have "no_dup F"
      using ‹invNOT S› ‹convert_trail_from_W (trail S) = F' @ Decided K # F›
      unfolding invNOT_def by (metis no_dup_appendD no_dup_cons no_dup_convert_from_W)
    then have "consistent_interp (lits_of_l F)"
      using distinct_consistent_interp by blast
    then have "¬ tautology C'"
      using ‹F ⊨as CNot C'› consistent_CNot_not_tautology true_annots_true_cls by blast
    then have taut: "¬ tautology (add_mset L ?C')"
      using ‹F ⊨as CNot C'› ‹undefined_lit F L› by (metis CNot_remdups_mset
          Decided_Propagated_in_iff_in_lits_of_l in_CNot_uminus tautology_add_mset
          tautology_remdups_mset true_annot_singleton true_annots_def)

    have f2: "no_dup (convert_trail_from_W (trail S))"
      using ‹invNOT S› unfolding invNOT_def by (simp add: o_def)
    have f3: "atm_of L ∈ atms_of_mm (clauses S)
      ∪ atm_of ` lits_of_l (convert_trail_from_W (trail S))"
      using ‹convert_trail_from_W (trail S) = F' @ Decided K # F›
        ‹atm_of L ∈ atms_of_mm (clauses S) ∪ atm_of ` lits_of_l (F' @ Decided K # F)› by auto
    have f4: "clauses S ⊨pm add_mset L ?C'"
      by (metis "1"(7) dist(2) remdups_mset_singleton_sum true_clss_cls_remdups_mset)
    have "F ⊨as CNot ?C'"
      by (simp add: ‹F ⊨as CNot C'›)
    have "Ex (backjump_l S)"
      apply standard
      apply (rule backjump_l.intros[of _ _ _ _ _ L "add_mset L ?C'" _ ?C'])
      using f4 f3 f2 ‹¬ tautology (add_mset L ?C')›
        1 taut dist ‹F ⊨as CNot (remdups_mset C')›
        state_eqNOT_ref unfolding backjump_l_cond_def set_mset_remdups_mset by blast+
    then show ?case
      by blast
next
  case (3 L S)
  then show "∃T. decideNOT S T ∨ propagateNOT S T ∨ backjump_l S T"
    using decideNOT.intros[of S L] by auto
qed


context conflict_driven_clause_learningW
begin
text ‹Notations are lost while proving locale inclusion:›
notation state_eqNOT (infix "∼NOT" 50)

subsection ‹Additional Lemmas between NOT and W states›
lemma trailW_eq_reduce_trail_toNOT_eq:
  "trail S = trail T ⟹ trail (reduce_trail_toNOT F S) = trail (reduce_trail_toNOT F T)"
proof (induction F S arbitrary: T rule: reduce_trail_toNOT.induct)
  case (1 F S T) note IH = this(1) and tr = this(2)
  then have "[] = convert_trail_from_W (trail S)
    ∨ length F = length (convert_trail_from_W (trail S))
    ∨ trail (reduce_trail_toNOT F (tl_trail S)) = trail (reduce_trail_toNOT F (tl_trail T))"
    using IH by (metis (no_types) trail_tl_trail)
  then show "trail (reduce_trail_toNOT F S) = trail (reduce_trail_toNOT F T)"
    using tr by (metis (no_types) reduce_trail_toNOT.elims)
qed

lemma trail_reduce_trail_toNOT_add_learned_cls:
"no_dup (trail S) ⟹
  trail (reduce_trail_toNOT M (add_learned_cls D S)) = trail (reduce_trail_toNOT M S)"
 by (rule trailW_eq_reduce_trail_toNOT_eq) simp

lemma reduce_trail_toNOT_reduce_trail_convert:
  "reduce_trail_toNOT C S = reduce_trail_to (convert_trail_from_NOT C) S"
  apply (induction C S rule: reduce_trail_toNOT.induct)
  apply (subst reduce_trail_toNOT.simps, subst reduce_trail_to.simps)
  by auto

lemma reduce_trail_to_map[simp]:
  "reduce_trail_to (map f M) S = reduce_trail_to M S"
  by (rule reduce_trail_to_length) simp

lemma reduce_trail_toNOT_map[simp]:
  "reduce_trail_toNOT (map f M) S = reduce_trail_toNOT M S"
  by (rule reduce_trail_toNOT_length) simp

lemma skip_or_resolve_state_change:
  assumes "skip_or_resolve** S T"
  shows
    "∃M. trail S = M @ trail T ∧ (∀m ∈ set M. ¬is_decided m)"
    "clauses S = clauses T"
    "backtrack_lvl S = backtrack_lvl T"
    "init_clss S = init_clss T"
    "learned_clss S = learned_clss T"
  using assms
proof (induction rule: rtranclp_induct)
  case base
  case 1 show ?case by simp
  case 2 show ?case by simp
  case 3 show ?case by simp
  case 4 show ?case by simp
  case 5 show ?case by simp
next
  case (step T U) note st = this(1) and s_o_r = this(2) and IH = this(3) and IH' = this(3-)

  case 2 show ?case using IH' s_o_r by (auto elim!: rulesE simp: skip_or_resolve.simps)
  case 3 show ?case using IH' s_o_r by (cases ‹trail T›) (auto elim!: rulesE simp: skip_or_resolve.simps)
  case 1 show ?case
    using s_o_r IH by (cases "trail T") (auto elim!: rulesE simp: skip_or_resolve.simps)
  case 4 show ?case
    using s_o_r IH' by (cases "trail T") (auto elim!: rulesE simp: skip_or_resolve.simps)
  case 5 show ?case
    using s_o_r IH' by (cases "trail T") (auto elim!: rulesE simp: skip_or_resolve.simps)
qed


subsection ‹Inclusion of Weidenbach's CDCL in NOT's CDCL›

text ‹This lemma shows the inclusion of Weidenbach's CDCL @{const cdclW_merge} (with merging) in
  NOT's @{const cdclNOT_merged_bj_learn}.›
lemma cdclW_merge_is_cdclNOT_merged_bj_learn:
  assumes
    inv: "cdclW_all_struct_inv S" and
    cdclW_restart: "cdclW_merge S T"
  shows "cdclNOT_merged_bj_learn S T
    ∨ (no_step cdclW_merge T ∧ conflicting T ≠ None)"
  using cdclW_restart inv
proof induction
  case (fw_propagate S T) note propa = this(1)
  then obtain M N U L C where
    H: "state_butlast S = (M, N, U, None)" and
    CL: "C + {#L#} ∈# clauses S" and
    M_C: "M ⊨as CNot C" and
    undef: "undefined_lit (trail S) L" and
    T: "state_butlast T = (Propagated L (C + {#L#}) # M, N, U, None)"
    by (auto elim: propagate_high_levelE)
  have "propagateNOT S T"
    using H CL T undef M_C by (auto simp: state_eqNOT_def clauses_def simp del: state_simp)
  then show ?case
    using cdclNOT_merged_bj_learn.intros(2) by blast
next
  case (fw_decide S T) note dec = this(1) and inv = this(2)
  then obtain L where
    undef_L: "undefined_lit (trail S) L" and
    atm_L: "atm_of L ∈ atms_of_mm (init_clss S)" and
    T: "T ∼ cons_trail (Decided L) S"
    by (auto elim: decideE)
  have "decideNOT S T"
    apply (rule decideNOT.decideNOT)
       using undef_L apply (simp; fail)
     using atm_L inv apply (auto simp: cdclW_all_struct_inv_def no_strange_atm_def clauses_def; fail)
    using T undef_L unfolding state_eqNOT_def by (auto simp: clauses_def)
  then show ?case using cdclNOT_merged_bj_learn_decideNOT by blast
next
  case (fw_forget S T) note rf = this(1) and inv = this(2)
  then obtain C where
     S: "conflicting S = None" and
     C_le: "C ∈# learned_clss S" and
     "¬(trail S) ⊨asm clauses S" and
     "C ∉ set (get_all_mark_of_propagated (trail S))" and
     C_init: "C ∉# init_clss S" and
     T: "T ∼ remove_cls C S" and
     S_C: ‹removeAll_mset C (clauses S) ⊨pm C›
    by (auto elim: forgetE)
  have "forgetNOT S T"
    apply (rule forgetNOT.forgetNOT)
       using S_C apply blast
      using S apply simp
     using C_init C_le apply (simp add: clauses_def)
    using T C_le C_init by (auto simp: Un_Diff state_eqNOT_def clauses_def ac_simps)
  then show ?case using cdclNOT_merged_bj_learn_forgetNOT by blast
next
  case (fw_conflict S T U) note confl = this(1) and bj = this(2) and inv = this(3)
  obtain CS CT where
    confl_T: "conflicting T = Some CT" and
    CT: "CT = CS" and
    CS: "CS ∈# clauses S" and
    tr_S_CS: "trail S ⊨as CNot CS"
    using confl by (elim conflictE) auto
  have inv_T: "cdclW_all_struct_inv T"
    using cdclW_restart.simps cdclW_all_struct_inv_inv confl inv by blast
  then have "cdclW_M_level_inv T"
    unfolding cdclW_all_struct_inv_def by auto
  then consider
    (no_bt) "skip_or_resolve** T U" |
    (bt) T' where "skip_or_resolve** T T'" and "backtrack T' U"
    using bj rtranclp_cdclW_bj_skip_or_resolve_backtrack unfolding full_def by meson
  then show ?case
  proof cases
    case no_bt
    then have "conflicting U ≠ None"
      using confl by (induction rule: rtranclp_induct)
      (auto simp: skip_or_resolve.simps elim!: rulesE)
    moreover then have "no_step cdclW_merge U"
      by (auto simp: cdclW_merge.simps elim: rulesE)
    ultimately show ?thesis by blast
  next
    case bt note s_or_r = this(1) and bt = this(2)
    have "cdclW_restart** T T'"
      using s_or_r mono_rtranclp[of skip_or_resolve cdclW_restart]
        rtranclp_skip_or_resolve_rtranclp_cdclW_restart
      by blast
    then have "cdclW_M_level_inv T'"
      using rtranclp_cdclW_restart_consistent_inv ‹cdclW_M_level_inv T› by blast
    then obtain M1 M2 i D L K D' where
      confl_T': "conflicting T' = Some (add_mset L D)" and
      M1_M2:"(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail T'))" and
      "get_level (trail T') K = i+1"
      "get_level (trail T') L = backtrack_lvl T'" and
      "get_level (trail T') L = get_maximum_level (trail T') (add_mset L D')" and
      "get_maximum_level (trail T') D' = i" and
      U: "U ∼ cons_trail (Propagated L (add_mset L D'))
               (reduce_trail_to M1
                    (add_learned_cls (add_mset L D')
                      (update_conflicting None T')))" and
      D_D': ‹D' ⊆# D› and
      T'_L_D': ‹clauses T' ⊨pm add_mset L D'›
      using bt by (auto elim: backtrackE)
    let ?D' = ‹add_mset L D'›
    have [simp]: "clauses S = clauses T"
      using confl by (auto elim: rulesE)
    have [simp]: "clauses T = clauses T'"
      using s_or_r
    proof (induction)
      case base
      then show ?case by simp
    next
      case (step U V) note st = this(1) and s_o_r = this(2) and IH = this(3)
      have "clauses U = clauses V"
        using s_o_r by (auto simp: skip_or_resolve.simps elim: rulesE)
      then show ?case using IH by auto
    qed
    have "cdclW_restart** T T'"
      using rtranclp_skip_or_resolve_rtranclp_cdclW_restart s_or_r by blast
    have inv_T': "cdclW_all_struct_inv T'"
      using ‹cdclW_restart** T T'› inv_T rtranclp_cdclW_all_struct_inv_inv by blast
    have inv_U: "cdclW_all_struct_inv U"
      using cdclW_merge_restart_cdclW_restart confl fw_r_conflict inv local.bj
      rtranclp_cdclW_all_struct_inv_inv by blast

    have [simp]: "init_clss S = init_clss T'"
      using ‹cdclW_restart** T T'› cdclW_restart_init_clss confl cdclW_all_struct_inv_def conflict
      inv by (metis rtranclp_cdclW_restart_init_clss)
    then have atm_L: "atm_of L ∈ atms_of_mm (clauses S)"
      using inv_T' confl_T' unfolding cdclW_all_struct_inv_def no_strange_atm_def
      clauses_def
      by (simp add: atms_of_def image_subset_iff)
    obtain M where tr_T: "trail T = M @ trail T'"
      using s_or_r skip_or_resolve_state_change by meson
    obtain M' where
      tr_T': "trail T' = M' @ Decided K # tl (trail U)" and
      tr_U: "trail U = Propagated L ?D' # tl (trail U)"
      using U M1_M2 inv_T' unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def
      by fastforce
    define M'' where "M'' ≡ M @ M'"
    have tr_T: "trail S = M'' @ Decided K # tl (trail U)"
      using tr_T tr_T' confl unfolding M''_def by (auto elim: rulesE)
    have "init_clss T' + learned_clss S ⊨pm ?D'"
      using inv_T' confl_T' ‹clauses S = clauses T› ‹clauses T = clauses T'› T'_L_D'
      unfolding cdclW_all_struct_inv_def cdclW_learned_clause_alt_def clauses_def by auto
    have "reduce_trail_to (convert_trail_from_NOT (convert_trail_from_W M1)) S =
      reduce_trail_to M1 S"
      by (rule reduce_trail_to_length) simp
    moreover have "trail (reduce_trail_to M1 S) = M1"
      apply (rule reduce_trail_to_skip_beginning[of _ "M @ _ @ M2 @ [Decided K]"])
      using confl M1_M2 ‹trail T = M @ trail T'›
        apply (auto dest!: get_all_ann_decomposition_exists_prepend
          elim!: conflictE)
        by (rule sym) auto
    ultimately have [simp]: "trail (reduce_trail_toNOT M1 S) = M1"
      using M1_M2 confl by (subst reduce_trail_toNOT_reduce_trail_convert)
      (auto simp: comp_def elim: rulesE)
    have "every_mark_is_a_conflict U"
      using inv_U unfolding cdclW_all_struct_inv_def cdclW_conflicting_def by simp
    then have U_D: "tl (trail U) ⊨as CNot D'"
      by (subst tr_U, subst (asm) tr_U) fastforce
    have undef_L: "undefined_lit (tl (trail U)) L"
      using U M1_M2 inv_U unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def
      by (auto simp: lits_of_def defined_lit_map)
    have "backjump_l S U"
      apply (rule backjump_l[of _ _ _ _ _ L ?D' _ "D'"])
               using tr_T apply (simp; fail)
              using U M1_M2 confl M1_M2 inv_T' inv unfolding cdclW_all_struct_inv_def
              cdclW_M_level_inv_def apply (auto simp: state_eqNOT_def
                trail_reduce_trail_toNOT_add_learned_cls; fail)[]
            using CS apply (auto; fail)[]
           using tr_S_CS apply (simp; fail)

          using undef_L apply (auto; fail)[]
         using atm_L apply (simp add: trail_reduce_trail_toNOT_add_learned_cls; fail)
        using ‹init_clss T' + learned_clss S ⊨pm ?D'› unfolding clauses_def
        apply (simp; fail)
       apply (simp; fail)
      apply (metis U_D convert_trail_from_W_true_annots)
      using inv_T' inv_U U confl_T' undef_L M1_M2 unfolding cdclW_all_struct_inv_def
      distinct_cdclW_state_def by (auto simp: cdclW_M_level_inv_decomp backjump_l_cond_def
          dest: multi_member_split)
    then show ?thesis using cdclNOT_merged_bj_learn_backjump_l by fast
  qed
qed

abbreviation cdclNOT_restart where
"cdclNOT_restart ≡ restart_ops.cdclNOT_raw_restart cdclNOT restart"

lemma cdclW_merge_restart_is_cdclNOT_merged_bj_learn_restart_no_step:
  assumes
    inv: "cdclW_all_struct_inv S" and
    cdclW_restart:"cdclW_merge_restart S T"
  shows "cdclNOT_restart** S T ∨ (no_step cdclW_merge T ∧ conflicting T ≠ None)"
proof -
  consider
    (fw) "cdclW_merge S T" |
    (fw_r) "restart S T"
    using cdclW_restart by (meson cdclW_merge_restart.simps cdclW_rf.cases fw_conflict fw_decide fw_forget
      fw_propagate)
  then show ?thesis
  proof cases
    case fw
    then have IH: "cdclNOT_merged_bj_learn S T ∨ (no_step cdclW_merge T ∧ conflicting T ≠ None)"
      using inv cdclW_merge_is_cdclNOT_merged_bj_learn by blast
    have invS: "invNOT S"
      using inv unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by auto
    have ff2: "cdclNOT++ S T ⟶ cdclNOT** S T"
      by (meson tranclp_into_rtranclp)
    have ff3: "no_dup (convert_trail_from_W (trail S))"
      using invS by (simp add: comp_def)
    have "cdclNOT ≤ cdclNOT_restart"
      by (auto simp: restart_ops.cdclNOT_raw_restart.simps)
    then show ?thesis
      using ff3 ff2 IH cdclNOT_merged_bj_learn_is_tranclp_cdclNOT
        rtranclp_mono[of cdclNOT cdclNOT_restart] invS predicate2D by blast
  next
    case fw_r
    then show ?thesis by (blast intro: restart_ops.cdclNOT_raw_restart.intros)
  qed
qed

abbreviation μFW :: "'st ⇒ nat" where
"μFW S ≡ (if no_step cdclW_merge S then 0 else 1+μCDCL'_merged (set_mset (init_clss S)) S)"

lemma cdclW_merge_μFW_decreasing:
  assumes
    inv: "cdclW_all_struct_inv S" and
    fw: "cdclW_merge S T"
  shows "μFW T < μFW S"
proof -
  let ?A = "init_clss S"
  have atm_clauses: "atms_of_mm (clauses S) ⊆ atms_of_mm ?A"
    using inv unfolding cdclW_all_struct_inv_def no_strange_atm_def clauses_def by auto
  have atm_trail: "atm_of ` lits_of_l (trail S) ⊆ atms_of_mm ?A"
    using inv unfolding cdclW_all_struct_inv_def no_strange_atm_def clauses_def by auto
  have n_d: "no_dup (trail S)"
    using inv unfolding cdclW_all_struct_inv_def by (auto simp: cdclW_M_level_inv_decomp)
  have [simp]: "¬ no_step cdclW_merge S"
    using fw by auto
  have [simp]: "init_clss S = init_clss T"
    using cdclW_merge_restart_cdclW_restart[of S T] inv rtranclp_cdclW_restart_init_clss
    unfolding cdclW_all_struct_inv_def
    by (meson cdclW_merge.simps cdclW_merge_restart.simps cdclW_rf.simps fw)
  consider
    (merged) "cdclNOT_merged_bj_learn S T"  |
    (n_s) "no_step cdclW_merge T"
    using cdclW_merge_is_cdclNOT_merged_bj_learn inv fw by blast
  then show ?thesis
  proof cases
    case merged
    then show ?thesis
      using cdclNOT_decreasing_measure'[OF _ _ atm_clauses, of T] atm_trail n_d
      by (auto split: if_split simp: comp_def image_image lits_of_def)
  next
    case n_s
    then show ?thesis by simp
  qed
qed

lemma wf_cdclW_merge: "wf {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge S T}"
  apply (rule wfP_if_measure[of _ _ "μFW"])
  using cdclW_merge_μFW_decreasing by blast

lemma tranclp_cdclW_merge_cdclW_merge_trancl:
  "{(T, S). cdclW_all_struct_inv S ∧ cdclW_merge++ S T}
  ⊆ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge S T}+"
proof -
  have "(T, S) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge S T}+"
    if inv: "cdclW_all_struct_inv S" and "cdclW_merge++ S T"
    for S T :: 'st
    using that(2)
    proof (induction rule: tranclp_induct)
      case base
      then show ?case using inv by auto
    next
      case (step T U) note st = this(1) and s = this(2) and IH = this(3)
      have "cdclW_all_struct_inv T"
        using st by (meson inv rtranclp_cdclW_all_struct_inv_inv
          rtranclp_cdclW_merge_rtranclp_cdclW_restart tranclp_into_rtranclp)
      then have "(U, T) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge S T}+"
        using s by auto
      then show ?case using IH by auto
    qed
  then show ?thesis by auto
qed

lemma wf_tranclp_cdclW_merge: "wf {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge++ S T}"
  apply (rule wf_subset)
    apply (rule wf_trancl)
    using wf_cdclW_merge apply simp
  using tranclp_cdclW_merge_cdclW_merge_trancl by simp

lemma wf_cdclW_bj_all_struct: "wf {(T, S). cdclW_all_struct_inv S ∧ cdclW_bj S T}"
  apply (rule wfP_if_measure[of "λ_. True"
      _ "λT. length (trail T) + (if conflicting T = None then 0 else 1)", simplified])
  using cdclW_bj_measure by (simp add: cdclW_all_struct_inv_def)

lemma cdclW_conflicting_true_cdclW_merge_restart:
  assumes "cdclW S V" and confl: "conflicting S = None"
  shows "(cdclW_merge S V ∧ conflicting V = None) ∨ (conflicting V ≠ None ∧ conflict S V)"
  using assms
proof (induction rule: cdclW.induct)
  case W_propagate
  then show ?case by (auto intro: cdclW_merge.intros elim: rulesE)
next
  case (W_conflict S')
  then show ?case by (auto intro: cdclW_merge.intros elim: rulesE)
next
  case W_other
  then show ?case
  proof cases
    case decide
    then show ?thesis
      by (auto intro: cdclW_merge.intros elim: rulesE)
  next
    case bj
    then show ?thesis
      using confl by (auto simp: cdclW_bj.simps elim: rulesE)
  qed
qed

lemma trancl_cdclW_conflicting_true_cdclW_merge_restart:
  assumes "cdclW++ S V" and inv: "cdclW_M_level_inv S" and "conflicting S = None"
  shows "(cdclW_merge++ S V ∧ conflicting V = None)
    ∨ (∃T U. cdclW_merge** S T ∧ conflicting V ≠ None ∧ conflict T U ∧ cdclW_bj** U V)"
  using assms
proof induction
  case base
  then show ?case using cdclW_conflicting_true_cdclW_merge_restart by blast
next
  case (step U V) note st = this(1) and cdclW = this(2) and IH = this(3)[OF this(4-)] and
    confl[simp] = this(5) and inv = this(4)
  from cdclW
  show ?case
  proof (cases)
    case W_propagate
    moreover have "conflicting U = None" and "conflicting V = None"
      using W_propagate by (auto elim: propagateE)
    ultimately show ?thesis using IH cdclW_merge.fw_propagate[of U V] by auto
  next
    case W_conflict
    moreover have confl_U: "conflicting U = None" and confl_V: "conflicting V ≠ None"
      using W_conflict by (auto elim!: conflictE)
    moreover have "cdclW_merge** S U"
      using IH confl_U by auto
    ultimately show ?thesis using IH by auto
  next
    case W_other
    then show ?thesis
    proof cases
      case decide
      then show ?thesis using IH cdclW_merge.fw_decide[of U V] by (auto elim: decideE)
    next
      case bj
      then consider
        (s_or_r) "skip_or_resolve U V" |
        (bt) "backtrack U V"
        by (auto simp: cdclW_bj.simps)
      then show ?thesis
      proof cases
        case s_or_r
        have f1: "cdclW_bj++ U V"
          by (simp add: local.bj tranclp.r_into_trancl)
        obtain T T' :: 'st where
          f2: "cdclW_merge++ S U
                ∨ cdclW_merge** S T ∧ conflicting U ≠ None
                  ∧ conflict T T' ∧ cdclW_bj** T' U"
          using IH confl by (meson bj rtranclp.intros(1)
              rtranclp_cdclW_merge_restart_no_step_cdclW_bj
              rtranclp_cdclW_merge_tranclp_cdclW_merge_restart)
        have "conflicting V ≠ None ∧ conflicting U ≠ None"
          using ‹skip_or_resolve U V›
          by (auto simp: skip_or_resolve.simps elim!: skipE resolveE)
        then show ?thesis
          by (metis (full_types) IH f1 rtranclp_trans tranclp_into_rtranclp)
      next
        case bt
        then have "conflicting U ≠ None" by (auto elim: backtrackE)
        then obtain T T' where
          "cdclW_merge** S T" and
          "conflicting U ≠ None" and
          "conflict T T'" and
          "cdclW_bj** T' U"
          using IH confl by (meson bj rtranclp.intros(1)
              rtranclp_cdclW_merge_restart_no_step_cdclW_bj
              rtranclp_cdclW_merge_tranclp_cdclW_merge_restart)
        have invU: "cdclW_M_level_inv U"
          using inv rtranclp_cdclW_restart_consistent_inv step.hyps(1)
          by (meson ‹cdclW_bj** T' U› ‹cdclW_merge** S T› ‹conflict T T'›
              cdclW_restart_consistent_inv conflict rtranclp_cdclW_bj_rtranclp_cdclW_restart
              rtranclp_cdclW_merge_rtranclp_cdclW_restart)
        then have "conflicting V = None"
          using ‹backtrack U V› inv by (auto elim: backtrackE
              simp: cdclW_M_level_inv_decomp)
        have "full cdclW_bj T' V"
          apply (rule rtranclp_fullI[of cdclW_bj T' U V])
          using ‹cdclW_bj** T' U› apply fast
          using ‹backtrack U V› backtrack_is_full1_cdclW_bj invU unfolding full1_def full_def
          by blast
        then show ?thesis
          using cdclW_merge.fw_conflict[of T T' V] ‹conflict T T'›
            ‹cdclW_merge** S T› ‹conflicting V = None› by auto
      qed
    qed
  qed
qed

lemma wf_cdclW: "wf {(T, S). cdclW_all_struct_inv S ∧ cdclW S T}"
  unfolding wf_iff_no_infinite_down_chain
proof clarify
  fix f :: "nat ⇒ 'st"
  assume "∀i. (f (Suc i), f i) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW S T}"
  then have f: "⋀i. (f (Suc i), f i) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW S T}"
    by blast
  {
    fix f :: "nat ⇒ 'st"
    assume
      f: "(f (Suc i), f i) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW S T}" and
      confl: "conflicting (f i) ≠ None" for i
    have "(f (Suc i), f i) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_bj S T}" for i
      using f[of i] confl[of i] by (auto simp: cdclW.simps cdclW_o.simps cdclW_rf.simps
        elim!: rulesE)
    then have False
      using wf_cdclW_bj_all_struct unfolding wf_iff_no_infinite_down_chain by blast
  } note no_infinite_conflict = this

  have st: "cdclW++ (f i) (f (Suc (i+j)))" for i j :: nat
    proof (induction j)
      case 0
      then show ?case using f by auto
    next
      case (Suc j)
      then show ?case using f [of "i+j+1"] by auto
    qed
  have st: "i < j ⟹ cdclW++ (f i) (f j)" for i j :: nat
    using st[of i "j - i - 1"] by auto

  obtain ib where ib: "conflicting (f ib) = None"
    using f no_infinite_conflict by blast

  define i0 where i0: "i0 = Max {i0. ∀i < i0. conflicting (f i) ≠ None}"
  have "finite {i0. ∀i < i0. conflicting (f i) ≠ None}"
  proof -
    have "{i0. ∀i < i0. conflicting (f i) ≠ None} ⊆ {0..ib}"
      using ib by (metis (mono_tags, lifting) atLeast0AtMost atMost_iff mem_Collect_eq not_le
          subsetI)
    then show ?thesis
      by (simp add: finite_subset)
  qed
  moreover have "{i0. ∀i < i0. conflicting (f i) ≠ None} ≠ {}"
    by auto
  ultimately have "i0 ∈ {i0. ∀i < i0. conflicting (f i) ≠ None}"
    using Max_in[of "{i0. ∀i<i0. conflicting (f i) ≠ None}"] unfolding i0 by fast
  then have confl_i0: "conflicting (f i0) = None"
  proof -
    have f1: "∀n<i0. conflicting (f n) ≠ None"
      using ‹i0 ∈ {i0. ∀i<i0. conflicting (f i) ≠ None}› by blast
    have "Suc i0 ∉ {n. ∀na<n. conflicting (f na) ≠ None}"
      by (metis (lifting) Max_ge ‹finite {i0. ∀i<i0. conflicting (f i) ≠ None}›
          i0 lessI not_le)
    then have "∃n<Suc i0. conflicting (f n) = None"
      by fastforce
    then show "conflicting (f i0) = None"
      using f1 by (metis le_less less_Suc_eq_le)
  qed
  have "∀i < i0. conflicting (f i) ≠ None"
    using ‹i0 ∈ {i0. ∀i < i0. conflicting (f i) ≠ None}› by blast

  have not_conflicting_none: False if confl: "∀x>i. conflicting (f x) = None" for i :: nat
  proof -
    let ?f = "λj. f (i + j+1)"
    have "cdclW_merge (?f j) (?f (Suc j))" for j :: nat
      using f[of "i+j+1"] confl that by (auto dest!: cdclW_conflicting_true_cdclW_merge_restart)
    then have "(?f (Suc j), ?f j) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge S T}"
      for j :: nat
      using f[of "i+j+1"] by auto
    then show False
      using wf_cdclW_merge unfolding wf_iff_no_infinite_down_chain by fast
  qed

  have not_conflicting: False if confl: "∀x>i. conflicting (f x) ≠ None" for i :: nat
  proof -
    let ?f = "λj. f (Suc (i + j))"
    have confl: "conflicting (f x) ≠ None" if "x > i" for x :: nat
      using confl that by auto
    have [iff]: "¬propagate (?f j) S" "¬decide (?f j) S" "¬conflict (?f j) S"
      for j :: nat and S :: 'st
      using confl[of "i+j+1"] by (auto elim!: rulesE)
    have [iff]: "¬ backtrack (f (Suc (i + j))) (f (Suc (Suc (i + j))))" for j :: nat
      using confl[of "i+j+2"] by (auto elim!: rulesE)
    have "cdclW_bj (?f j) (?f (Suc j))" for j :: nat
      using f[of "i+j+1"] confl that by (auto simp: cdclW.simps cdclW_o.simps elim: rulesE)

    then have "(?f (Suc j), ?f j) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_bj S T}"
      for j :: nat
      using f[of "i+j+1"] by auto
    then show False
      using wf_cdclW_bj_all_struct unfolding wf_iff_no_infinite_down_chain by fast
  qed

  then have [simp]: "∃x>i. conflicting (f x) = None" for i :: nat
    by meson
  have "{j. j > i ∧ conflicting (f j) ≠ None} ≠ {}" for i :: nat
    using not_conflicting_none by (rule ccontr) auto

  define g where g: "g = rec_nat i0 (λ_ i. LEAST j. j > i ∧ conflicting (f j) = None)"
  have g_0: "g 0 = i0"
    unfolding g by auto
  have g_Suc: "g (Suc i) = (LEAST j. j > g i ∧ conflicting (f j) = None)" for i
    unfolding g by auto
  have g_prop:"g (Suc i) > g i ∧ conflicting (f (g (Suc i))) = None" for i
  proof (cases i)
    case 0
    then show ?thesis
      using LeastI_ex[of "λj. j > i0 ∧ conflicting (f j) = None"]
      by (auto simp: g)[]
  next
    case (Suc i')
    then show ?thesis
      apply (subst g_Suc, subst g_Suc)
      using LeastI_ex[of "λj. j > g (Suc i') ∧ conflicting (f j) = None"]
      by auto
  qed
  then have g_increasing: "g (Suc i) > g i" for i :: nat by simp
  have confl_f_G[simp]: "conflicting (f (g i)) = None" for i :: nat
    by (cases i) (auto simp: g_prop g_0 confl_i0)
  have [simp]: "cdclW_M_level_inv (f i)" "cdclW_all_struct_inv (f i)" for i :: nat
    using f[of i] by (auto simp: cdclW_all_struct_inv_def)
  let ?fg = "λi. (f (g i))"
  have "∀i < Suc j. (f (g (Suc i)), f (g i)) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge++ S T}"
    for j :: nat
  proof (induction j)
    case 0
    have "cdclW++ (?fg 0) (?fg 1)"
      using g_increasing[of 0] by (simp add: st)
    then show ?case by (auto dest!: trancl_cdclW_conflicting_true_cdclW_merge_restart)
  next
    case (Suc j) note IH = this(1)
    let ?i = "g (Suc j)"
    let ?j = "g (Suc (Suc j))"
    have "conflicting (f ?i) = None"
      by auto
    moreover have "cdclW_all_struct_inv (f ?i)"
      by auto
    ultimately have "cdclW++ (f ?i) (f ?j)"
      using g_increasing by (simp add: st)
    then have "cdclW_merge++ (f ?i) (f ?j)"
      by (auto dest!: trancl_cdclW_conflicting_true_cdclW_merge_restart)
    then show ?case using IH not_less_less_Suc_eq by auto
  qed
  then have "∀i. (f (g (Suc i)), f (g i)) ∈ {(T, S). cdclW_all_struct_inv S ∧ cdclW_merge++ S T}"
    by blast
  then show False
    using wf_tranclp_cdclW_merge unfolding wf_iff_no_infinite_down_chain by fast
qed

lemma wf_cdclW_stgy:
  ‹wf {(T, S). cdclW_all_struct_inv S ∧ cdclW_stgy S T}›
  by (rule wf_subset[OF wf_cdclW]) (auto dest: cdclW_stgy_cdclW)

end


subsection ‹Inclusion of Weidendenbch's CDCL with Strategy›

context conflict_driven_clause_learningW
begin
abbreviation propagate_conds where
"propagate_conds ≡ λ_. propagate"

abbreviation (input) decide_conds where
"decide_conds S T ≡ decide S T ∧ no_step conflict S ∧ no_step propagate S"

abbreviation backjump_l_conds_stgy :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" where
"backjump_l_conds_stgy C C' L S V ≡
  (∃T U. conflict S T ∧ full skip_or_resolve T U ∧ conflicting T = Some C ∧
    mark_of (hd_trail V) = add_mset L C' ∧ backtrack U V)"

abbreviation invNOT_stgy where
"invNOT_stgy S ≡ conflicting S = None ∧ cdclW_all_struct_inv S ∧ no_smaller_propa S ∧
  cdclW_stgy_invariant S ∧ propagated_clauses_clauses S"

interpretation cdclW_with_strategy: cdclNOT_merge_bj_learn_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = decide_conds and
  propagate_conds = propagate_conds and
  forget_conds =  "λ_ _. False" and
  backjump_l_cond = "λC C' L' S T. backjump_l_conds_stgy C C' L' S T
    ∧ distinct_mset C' ∧ L' ∉# C' ∧ ¬tautology (add_mset L' C')"
  by unfold_locales

interpretation cdclW_with_strategy: cdclNOT_merge_bj_learn_proxy where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = decide_conds and
  propagate_conds = propagate_conds and
  forget_conds =  "λ_ _. False" and
  backjump_l_cond = backjump_l_conds_stgy and
  inv = invNOT_stgy
  by unfold_locales

lemma cdclW_with_strategy_cdclNOT_merged_bj_learn_conflict:
  assumes
    "cdclW_with_strategy.cdclNOT_merged_bj_learn S T"
    "conflicting S = None"
  shows
    "conflicting T = None"
  using assms
  apply (cases rule: cdclW_with_strategy.cdclNOT_merged_bj_learn.cases;
    elim cdclW_with_strategy.forgetNOTE cdclW_with_strategy.propagateNOTE
    cdclW_with_strategy.decideNOTE rulesE
    cdclW_with_strategy.backjump_lE backjumpE)
  apply (auto elim!: rulesE simp: comp_def)
  done

lemma cdclW_with_strategy_no_forgetNOT[iff]: "cdclW_with_strategy.forgetNOT S T ⟷ False"
  by (auto elim: cdclW_with_strategy.forgetNOTE)

lemma cdclW_with_strategy_cdclNOT_merged_bj_learn_cdclW_stgy:
  assumes
    "cdclW_with_strategy.cdclNOT_merged_bj_learn S V"
  shows
    "cdclW_stgy** S V"
  using assms
proof (cases rule: cdclW_with_strategy.cdclNOT_merged_bj_learn.cases)
  case cdclNOT_merged_bj_learn_decideNOT
  then show ?thesis
    apply (elim cdclW_with_strategy.decideNOTE)
    using cdclW_stgy.other'[of S V] cdclW_o.decide[of S V] by blast
next
  case cdclNOT_merged_bj_learn_propagateNOT
  then show ?thesis
    using cdclW_stgy.propagate' by (blast elim: cdclW_with_strategy.propagateNOTE)
next
  case cdclNOT_merged_bj_learn_forgetNOT
  then show ?thesis
    by blast
next
  case cdclNOT_merged_bj_learn_backjump_l
  then obtain T U where
    confl: "conflict S T" and
    full: "full skip_or_resolve T U" and
    bt: "backtrack U V"
    by (elim cdclW_with_strategy.backjump_lE) blast
  have "cdclW_bj** T U"
    using full mono_rtranclp[of skip_or_resolve cdclW_bj] unfolding full_def
    by (blast elim: skip_or_resolve.cases)
  moreover have "cdclW_bj U V" and "no_step cdclW_bj V"
    using bt by (auto dest: backtrack_no_cdclW_bj)
  ultimately have "full1 cdclW_bj T V"
    unfolding full1_def by auto
  then have "cdclW_stgy** T V"
    using cdclW_s'.bj'[of T V] cdclW_s'_is_rtranclp_cdclW_stgy[of T V] by blast
  then show ?thesis
    using confl cdclW_stgy.conflict'[of S T] by auto
qed

lemma rtranclp_transition_function:
  ‹R** a b ⟹ ∃f j. (∀i<j. R (f i) (f (Suc i))) ∧ f 0 = a ∧ f j = b›
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step b c) note st = this(1) and R = this(2) and IH = this(3)
  from IH obtain f j where
    i: ‹∀i<j. R (f i) (f (Suc i))› and
    a: ‹f 0 = a› and
    b: ‹f j = b›
    by auto
  let ?f = ‹f(Suc j := c)›

  have
    i: ‹∀i<Suc j. R (?f i) (?f (Suc i))› and
    a: ‹?f 0 = a› and
    b: ‹?f (Suc j) = c›
    using i a b R by auto
  then show ?case by blast
qed

lemma cdclW_bj_cdclW_stgy: ‹cdclW_bj S T ⟹ cdclW_stgy S T›
  by (rule cdclW_stgy.other') (auto simp: cdclW_bj.simps cdclW_o.simps elim!: rulesE)

lemma cdclW_restart_propagated_clauses_clauses:
  ‹cdclW_restart S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  by (induction rule: cdclW_restart_all_induct) (auto simp: propagated_clauses_clauses_def
      in_get_all_mark_of_propagated_in_trail simp: state_prop)

lemma rtranclp_cdclW_restart_propagated_clauses_clauses:
  ‹cdclW_restart** S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  by (induction rule: rtranclp_induct) (auto simp: cdclW_restart_propagated_clauses_clauses)

lemma rtranclp_cdclW_stgy_propagated_clauses_clauses:
  ‹cdclW_stgy** S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  using rtranclp_cdclW_restart_propagated_clauses_clauses[of S T]
    rtranclp_cdclW_stgy_rtranclp_cdclW_restart by blast

lemma conflicting_clause_bt_lvl_gt_0_backjump:
  assumes
    inv: ‹invNOT_stgy S› and
    C: ‹C ∈# clauses S› and
    tr_C: ‹trail S ⊨as CNot C› and
    bt: ‹backtrack_lvl S > 0›
  shows ‹∃ T U V. conflict S T ∧ full skip_or_resolve T U ∧ backtrack U V›
proof -
  let ?T = "update_conflicting (Some C) S"
  have confl_S_T: "conflict S ?T"
    using C tr_C inv by (auto intro!: conflict_rule)
  have count: "count_decided (trail S) > 0"
    using inv bt unfolding cdclW_stgy_invariant_def cdclW_all_struct_inv_def cdclW_M_level_inv_def
    by auto
  have ‹(∃K M'. trail S = M' @ Decided K # M) ⟹ D ∈# clauses S ⟹ ¬ M ⊨as CNot D› for M D
    using inv C tr_C unfolding cdclW_stgy_invariant_def no_smaller_confl_def
    by auto
  from this[OF _ C ] have C_ne: ‹C ≠ {#}›
    using tr_C bt count by (fastforce simp: filter_empty_conv in_set_conv_decomp count_decided_def
        elim!: is_decided_ex_Decided)

  obtain U where
    U: ‹full skip_or_resolve ?T U›
    by (meson wf_exists_normal_form_full wf_skip_or_resolve)
  then have s_o_r: "skip_or_resolve** ?T U"
    unfolding full_def by blast
  then obtain C' where C': ‹conflicting U = Some C'›
    by (induction rule: rtranclp_induct) (auto simp: skip_or_resolve.simps elim: rulesE)
  have ‹cdclW_stgy** ?T U›
    using s_o_r by induction
      (auto simp: skip_or_resolve.simps dest!: cdclW_bj.intros cdclW_bj_cdclW_stgy)
  then have ‹cdclW_stgy** S U›
    using confl_S_T by (auto dest!: cdclW_stgy.intros)
  then have
    inv_U: ‹cdclW_all_struct_inv U› and
    no_smaller_U: ‹no_smaller_propa U› and
    inv_stgy_U: ‹cdclW_stgy_invariant U›
    using inv rtranclp_cdclW_stgy_cdclW_all_struct_inv rtranclp_cdclW_stgy_no_smaller_propa
    rtranclp_cdclW_stgy_cdclW_stgy_invariant by blast+
  show ?thesis
  proof (cases C')
    case (add L D)
    then obtain V where ‹cdclW_stgy U V›
      using conflicting_no_false_can_do_step[of U C'] C' inv_U inv_stgy_U
      unfolding cdclW_all_struct_inv_def cdclW_stgy_invariant_def
      by (auto simp del: conflict_is_false_with_level_def)
    then have ‹backtrack U V›
      using C' U unfolding full_def
      by (auto simp: cdclW_stgy.simps cdclW_o.simps cdclW_bj.simps elim: rulesE)
    then show ?thesis
      using U confl_S_T by blast
  next
    case [simp]: empty
    obtain f j where
      f_s_o_r: ‹i<j ⟹ skip_or_resolve (f i) (f (Suc i))› and
      f_0: ‹f 0 = ?T› and
      f_j: ‹f j = U› for i
      using rtranclp_transition_function[OF s_o_r] by blast
    have j_0: ‹j ≠ 0›
      using C' f_j C_ne f_0 by (cases j) auto

    have bt_lvl_f_l: ‹backtrack_lvl (f k) = backtrack_lvl (f 0)› if ‹k ≤ j› for k
      using that
    proof (induction k)
      case 0
      then show ?case by (simp add: f_0)
    next
      case (Suc k)
      then have ‹backtrack_lvl (f (Suc k)) = backtrack_lvl (f k)›
        apply (cases ‹k < j›; cases ‹trail (f k)›)
        using f_s_o_r[of k] apply (auto simp: skip_or_resolve.simps elim!: rulesE)[2]
        by (auto simp: skip_or_resolve.simps elim!: rulesE simp del: local.state_simp)
      then show ?case
        using f_s_o_r[of k] Suc by simp
    qed

    have st_f: ‹cdclW_stgy** ?T (f k)› if ‹k < j› for k
      using that
    proof (induction k)
      case 0
      then show ?case by (simp add: f_0)
    next
      case (Suc k)
      then show ?case
        apply (cases ‹k < j›)
        using f_s_o_r[of k] apply (auto simp: skip_or_resolve.simps
            dest!: cdclW_bj.intros cdclW_bj_cdclW_stgy)[]
        using f_s_o_r[of "j - 1"] j_0 by (simp del: local.state_simp)
    qed note st_f_T = this(1)
    have st_f_s_k: ‹cdclW_stgy** S (f k)› if ‹k < j› for k
      using confl_S_T that st_f_T[of k] by (auto dest!: cdclW_stgy.intros)
    have f_confl: "conflicting (f k) ≠ None" if ‹k ≤ j› for k
      using that f_s_o_r[of k] f_j C'
      by (auto simp: skip_or_resolve.simps le_eq_less_or_eq elim!: rulesE)
    have ‹size (the (conflicting (f j))) = 0›
      using f_j C' by simp
    moreover have ‹size (the (conflicting (f 0))) > 0›
      using C_ne f_0 by (cases C) auto
    then have ‹∃x∈set [0..<Suc j]. 0 < size (the (conflicting (f x)))›
      by force
    ultimately obtain ys l zs where
      ‹[0..<Suc j] = ys @ l # zs› and
      ‹0 < size (the (conflicting (f l)))› and
      ‹∀z∈set zs. ¬ 0 < size (the (conflicting (f z)))›
      using split_list_last_prop[of "[0..<Suc j]" "λi. size (the (conflicting (f i))) > 0"]
      by blast
    moreover have ‹l < j›
      by (metis C' Suc_le_lessD ‹C' = {#}› append1_eq_conv append_cons_eq_upt_length_i_end
          calculation(1) calculation(2) f_j le_eq_less_or_eq neq0_conv option.sel
          size_eq_0_iff_empty upt_Suc)
    ultimately have ‹size (the (conflicting (f (Suc l)))) = 0›
      by (metis (no_types, opaque_lifting) ‹size (the (conflicting (f j))) = 0› append1_eq_conv
          append_cons_eq_upt_length_i_end less_eq_nat.simps(1) list.exhaust list.set_intros(1)
          neq0_conv upt_Suc upt_eq_Cons_conv)
    then have confl_Suc_l: ‹conflicting (f (Suc l)) = Some {#}›
      using f_confl[of "Suc l"] ‹l < j›  by (cases ‹conflicting (f (Suc l))›) auto
    let ?T' = ‹f l›
    let ?T'' = ‹f (Suc l)›
    have res: ‹resolve ?T' ?T''›
      using confl_Suc_l ‹0 < size (the (conflicting (f l)))› f_s_o_r[of l] ‹l < j›
      by (auto simp: skip_or_resolve.simps elim: rulesE)
    then have confl_T': ‹size (the (conflicting (f l))) = 1›
      using confl_Suc_l by (auto elim!: rulesE
          simp: Diff_eq_empty_iff_mset subset_eq_mset_single_iff)

    then have "size (mark_of (hd (trail ?T'))) = 1" and hd_t'_dec:"¬is_decided (hd (trail ?T'))"
      and tr_T'_ne: ‹trail ?T' ≠ []›
      using res C' confl_Suc_l
      by (auto elim!: resolveE simp: Diff_eq_empty_iff_mset subset_eq_mset_single_iff)
    then obtain L where L: "mark_of (hd (trail ?T')) = {#L#}"
      by (cases "hd (trail ?T')"; cases "mark_of (hd (trail ?T'))") auto
    have
      inv_f_l: ‹cdclW_all_struct_inv (f l)› and
      no_smaller_f_l: ‹no_smaller_propa (f l)› and
      inv_stgy_f_l: ‹cdclW_stgy_invariant (f l)› and
      propa_cls_f_l: ‹propagated_clauses_clauses (f l)›
      using inv st_f_s_k[OF ‹l < j›] rtranclp_cdclW_stgy_cdclW_all_struct_inv[of S "f l"]
        rtranclp_cdclW_stgy_no_smaller_propa[of S "f l"]
        rtranclp_cdclW_stgy_cdclW_stgy_invariant[of S "f l"]
        rtranclp_cdclW_stgy_propagated_clauses_clauses
      by blast+

    have hd_T': ‹hd (trail ?T') = Propagated L {#L#}›
      using inv_f_l L tr_T'_ne hd_t'_dec unfolding cdclW_all_struct_inv_def cdclW_conflicting_def
      by (cases "trail ?T'"; cases "(hd (trail ?T'))") force+
    let ?D = "mark_of (hd (trail ?T'))"
    have ‹get_level (trail (f l)) L = 0›
      using propagate_single_literal_clause_get_level_is_0[of "f l" L]
        propa_cls_f_l no_smaller_f_l hd_T' inv_f_l
      unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def
      by (cases ‹trail (f l)›) auto
    then have ‹count_decided (trail ?T') = 0›
      using hd_T' by (cases ‹trail (f l)›) auto
    then have ‹backtrack_lvl ?T' = 0›
      using inv_f_l unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def
      by auto
    then show ?thesis
      using bt bt_lvl_f_l[of l] ‹l < j› confl_S_T by (auto simp: f_0 elim: rulesE)
  qed
qed

lemma conflict_full_skip_or_resolve_backtrack_backjump_l:
  assumes
    conf: ‹conflict S T› and
    full: ‹full skip_or_resolve T U› and
    bt: ‹backtrack U V› and
    inv: ‹cdclW_all_struct_inv S›
  shows ‹cdclW_with_strategy.backjump_l S V›
proof -
  have inv_U: ‹cdclW_all_struct_inv U›
    by (metis cdclW_stgy.conflict' cdclW_stgy_cdclW_all_struct_inv
        conf full full_def inv rtranclp_cdclW_all_struct_inv_inv
        rtranclp_skip_or_resolve_rtranclp_cdclW_restart)
  then have inv_V: ‹cdclW_all_struct_inv V›
    by (metis backtrack bt cdclW_bj_cdclW_stgy cdclW_stgy_cdclW_all_struct_inv)
  obtain C where
    C_S: ‹C ∈# clauses S› and
    S_Not_C: ‹trail S ⊨as CNot C› and
    tr_T_S: ‹trail T = trail S› and
    T: ‹T ∼ update_conflicting (Some C) S› and
    clss_T_S: ‹clauses T = clauses S›
    using conf by (auto elim: rulesE)
  have s_o_r: ‹skip_or_resolve** T U›
    using full unfolding full_def by blast
  then have
    ‹∃M. trail T = M @ trail U› and
    bt_T_U: ‹backtrack_lvl T = backtrack_lvl U› and
    bt_lvl_T_U: ‹backtrack_lvl T = backtrack_lvl U› and
    clss_T_U: ‹clauses T = clauses U› and
    init_T_U: ‹init_clss T = init_clss U› and
    learned_T_U: ‹learned_clss T = learned_clss U›
    using skip_or_resolve_state_change[of T U] by blast+
  then obtain M where M: ‹trail T = M @ trail U›
    by blast
  obtain D D' :: "'v clause" and K L :: "'v literal" and
    M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat where
    confl_D: "conflicting U = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail U))" and
    lev_L_U: "get_level (trail U) L = backtrack_lvl U" and
    max_D_L_U: "get_level (trail U) L = get_maximum_level (trail U) (add_mset L D')" and
    i: "get_maximum_level (trail U) D' ≡ i" and
    lev_K_U: "get_level (trail U) K = i + 1" and
    V: "V ∼ cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None U)))" and
    U_L_D': ‹clauses U ⊨pm add_mset L D'› and
    D_D': ‹D' ⊆# D›
    using bt by (auto elim!: rulesE)
  let ?D' = ‹add_mset L D'›
  obtain M' where M': ‹trail U = M' @ M2 @ Decided K # M1›
    using decomp by auto
  have ‹clauses V = {#?D'#} + clauses U›
    using V by auto
  moreover have ‹trail V = (Propagated L ?D') # trail (reduce_trail_to M1 U)›
    using V T M tr_T_S[symmetric] M' clss_T_U[symmetric] unfolding state_eqNOT_def
    by (auto simp del: state_simp dest!: state_simp(1))
  ultimately have V': ‹V ∼NOT
    cons_trail (Propagated L dummy_cls) (reduce_trail_toNOT M1 (add_learned_cls ?D' S))›
    using V T M tr_T_S[symmetric] M' clss_T_U[symmetric] unfolding state_eqNOT_def
    by (auto simp del: state_simp
        simp: trail_reduce_trail_toNOT_drop drop_map drop_tl clss_T_S)
  have ‹no_dup (trail V)›
    using inv_V V unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by blast
  then have undef_L: ‹undefined_lit M1 L›
    using V decomp by (auto simp: defined_lit_map)

  have ‹atm_of L ∈ atms_of_mm (init_clss V)›
    using inv_V V decomp unfolding cdclW_all_struct_inv_def no_strange_atm_def by auto
  moreover have init_clss_VU_S: ‹init_clss V = init_clss S›
    ‹init_clss U = init_clss S›‹learned_clss U = learned_clss S›
    using T V init_T_U learned_T_U by auto
  ultimately have atm_L: ‹atm_of L ∈ atms_of_mm (clauses S)›
    by (auto simp: clauses_def)



  have ‹distinct_mset ?D'› and ‹¬ tautology ?D'›
     using inv_U confl_D decomp D_D' unfolding cdclW_all_struct_inv_def distinct_cdclW_state_def
     apply simp_all
     using inv_V V not_tautology_mono[OF D_D'] distinct_mset_mono[OF D_D']
     unfolding cdclW_all_struct_inv_def
     apply (auto simp add: tautology_add_mset)
    done
  have ‹L ∉# D'›
    using ‹distinct_mset ?D'› by (auto simp: not_in_iff)
  have bj: ‹backjump_l_conds_stgy C D' L S V›
    apply (rule exI[of _ T], rule exI[of _ U])
    using ‹distinct_mset ?D'› ‹¬ tautology ?D'› conf full bt confl_D
      ‹L ∉# D'› V T
    by (auto)

  have M1_D': "M1 ⊨as CNot D'"
    using backtrack_M1_CNot_D'[of U D' ‹i› K M1 M2 L ‹add_mset L D› V ‹Propagated L (add_mset L D')›]
      inv_U confl_D decomp lev_L_U max_D_L_U i lev_K_U V U_L_D' D_D'
    unfolding cdclW_all_struct_inv_def cdclW_conflicting_def cdclW_M_level_inv_def
    by (auto simp: subset_mset_trans_add_mset)
  show ?thesis
    apply (rule cdclW_with_strategy.backjump_l.intros[of S _ K
          "convert_trail_from_W M1" _ L _ C D'])
             apply (simp add: tr_T_S[symmetric] M' M; fail)
            using V' apply (simp; fail)
           using C_S apply (simp; fail)
          using S_Not_C apply (simp; fail)
         using undef_L apply (simp; fail)
        using atm_L apply (simp; fail)
       using U_L_D' init_clss_VU_S apply (simp add: clauses_def; fail)
      apply (simp; fail)
     using M1_D' apply (simp; fail)
    using bj ‹distinct_mset ?D'› ‹¬ tautology ?D'› by auto
qed

lemma is_decided_o_convert_ann_lit_from_W[simp]:
  ‹is_decided o convert_ann_lit_from_W = is_decided›
  apply (rule ext)
  apply (rename_tac x, case_tac x)
  apply (auto simp: comp_def)
  done

lemma cdclW_with_strategy_propagateNOT_propagate_iff[iff]:
  ‹cdclW_with_strategy.propagateNOT S T ⟷ propagate S T› (is "?NOT ⟷ ?W")
proof (rule iffI)
  assume ?NOT
  then show ?W by auto
next
  assume ?W
  then obtain E L where
    ‹conflicting S = None› and
    E: ‹E ∈# clauses S› and
    LE: ‹L ∈# E› and
    tr_E: ‹trail S ⊨as CNot (remove1_mset L E)› and
    undef: ‹undefined_lit (trail S) L› and
    T: ‹T ∼ cons_trail (Propagated L E) S›
    by (auto elim!: propagateE)
  show ?NOT
    apply (rule cdclW_with_strategy.propagateNOT[of L ‹remove1_mset L E›])
        using LE E apply (simp; fail)
       using tr_E apply (simp; fail)
      using undef apply (simp; fail)
     using ‹?W› apply (simp; fail)
    using T by (simp add: state_eqNOT_def clauses_def)
qed


interpretation cdclW_with_strategy: cdclNOT_merge_bj_learn where
  trail = "λS. convert_trail_from_W (trail S)" and
  clausesNOT = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_clsNOT = "λC S. add_learned_cls C S" and
  remove_clsNOT = "λC S. remove_cls C S" and
  decide_conds = decide_conds and
  propagate_conds = propagate_conds and
  forget_conds =  "λ_ _. False" and
  backjump_l_cond = backjump_l_conds_stgy and
  inv = invNOT_stgy
proof (unfold_locales, goal_cases)
  case (2 S T)
  then show ?case
    using cdclW_with_strategy_cdclNOT_merged_bj_learn_cdclW_stgy[of S T]
    cdclW_with_strategy_cdclNOT_merged_bj_learn_conflict[of S T]
    rtranclp_cdclW_stgy_cdclW_all_struct_inv rtranclp_cdclW_stgy_no_smaller_propa
    rtranclp_cdclW_stgy_cdclW_stgy_invariant rtranclp_cdclW_stgy_propagated_clauses_clauses
    by blast
next
  case (1 C' S C F' K F L)
  have ‹count_decided (convert_trail_from_W (trail S)) > 0›
    unfolding ‹convert_trail_from_W (trail S) = F' @ Decided K # F› by simp
  then have ‹count_decided (trail S) > 0›
    by simp
  then have ‹backtrack_lvl S > 0›
    using ‹invNOT_stgy S› unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by auto
  have "∃T U V. conflict S T ∧ full skip_or_resolve T U ∧ backtrack U V"
    apply (rule conflicting_clause_bt_lvl_gt_0_backjump)
       using ‹invNOT_stgy S› apply (auto; fail)[]
      using ‹C ∈# clauses S› apply (simp; fail)
     using ‹convert_trail_from_W (trail S) ⊨as CNot C› apply (simp; fail)
    using ‹backtrack_lvl S > 0› by (simp; fail)
  then show ?case
    using conflict_full_skip_or_resolve_backtrack_backjump_l ‹invNOT_stgy S› by blast
next
  case (3 L S) note atm = this(1,2) and inv = this(3) and sat = this(4)
  moreover have ‹Ex(cdclW_with_strategy.backjump_l S)› if ‹conflict S T› for T
  proof -
    have ‹∃C. C ∈# clauses S ∧ trail S ⊨as CNot C›
      using that by (auto elim: rulesE)
    then obtain C where ‹C ∈# clauses S› and ‹trail S ⊨as CNot C› by blast
    have ‹backtrack_lvl S > 0›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then have ‹backtrack_lvl S = 0›
        by simp
      then have ‹count_decided (trail S) = 0›
        using inv unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by simp
      then have ‹get_all_ann_decomposition (trail S) = [([], trail S)]›
        by (auto simp: filter_empty_conv no_decision_get_all_ann_decomposition count_decided_0_iff)
      then have ‹set_mset (clauses S) ⊨ps unmark_l (trail S)›
        using 3(3) unfolding cdclW_all_struct_inv_def by auto
      obtain I where
        consistent: ‹consistent_interp I› and
        I_S: ‹I ⊨m clauses S› and
        tot: ‹total_over_m I (set_mset (clauses S))›
        using sat by (auto simp: satisfiable_def)
      have ‹total_over_m I (set_mset (clauses S)) ∧ total_over_m I (unmark_l (trail S))›
        using tot inv unfolding cdclW_all_struct_inv_def no_strange_atm_def
        by (auto simp: clauses_def total_over_set_def total_over_m_def)
      then have ‹I ⊨s unmark_l (trail S)›
        using ‹set_mset (clauses S) ⊨ps unmark_l (trail S)› consistent I_S
        unfolding true_clss_clss_def clauses_def
        by auto

      have ‹I ⊨s CNot C›
        by (meson ‹trail S ⊨as CNot C› ‹I ⊨s unmark_l (trail S)› set_mp true_annots_true_cls
            true_cls_def true_clss_def true_clss_singleton_lit_of_implies_incl true_lit_def)
      moreover have ‹I ⊨ C›
        using ‹C ∈# clauses S› and ‹I ⊨m clauses S› unfolding true_cls_mset_def by auto
      ultimately show False
        using consistent consistent_CNot_not by blast
    qed
    then show ?thesis
      using conflicting_clause_bt_lvl_gt_0_backjump[of S C]
        conflict_full_skip_or_resolve_backtrack_backjump_l[of S]
        ‹C ∈# clauses S› ‹trail S ⊨as CNot C› inv by fast
  qed
  moreover {
    have atm: ‹atms_of_mm (clauses S) = atms_of_mm (init_clss S)›
      using 3(3) unfolding cdclW_all_struct_inv_def no_strange_atm_def
      by (auto simp: clauses_def)
    have ‹decide S (cons_trail (Decided L) S)›
      apply (rule decide_rule)
      using 3 by (auto simp: atm) }
  moreover have ‹cons_trail (Decided L) S ∼NOT cons_trail (Decided L) S›
    by (simp add: state_eqNOT_def del: state_simp)
  ultimately show "∃T. cdclW_with_strategy.decideNOT S T ∨
    cdclW_with_strategy.propagateNOT S T ∨
    cdclW_with_strategy.backjump_l S T"
    using cdclW_with_strategy.decideNOT.intros[of S L "cons_trail (Decided L) S"]
    by auto
qed

thm cdclW_with_strategy.full_cdclNOT_merged_bj_learn_final_state

end

end