Theory 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 trail⇩N⇩O⇩T where
"trail⇩N⇩O⇩T 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 state⇩W ⊆ dpll_state_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λC S. remove_cls C S"
  by unfold_locales

sublocale state⇩W ⊆ dpll_state where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λC S. remove_cls C S"
  by unfold_locales (auto simp: map_tl o_def)

context state⇩W
begin
declare state_simp⇩N⇩O⇩T[simp del]
end


subsection ‹Inclusion of Weidendenbch's CDCL without Strategy›

sublocale conflict_driven_clause_learning⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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_learning⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn_proxy where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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 = inv⇩N⇩O⇩T
  by unfold_locales

sublocale conflict_driven_clause_learning⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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 = inv⇩N⇩O⇩T
proof (unfold_locales, goal_cases)
  case 2
  then show ?case using cdcl⇩N⇩O⇩T_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 ‹inv⇩N⇩O⇩T S› ‹convert_trail_from_W (trail S) = F' @ Decided K # F›
      unfolding inv⇩N⇩O⇩T_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 ‹inv⇩N⇩O⇩T S› unfolding inv⇩N⇩O⇩T_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_eq⇩N⇩O⇩T_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. decide⇩N⇩O⇩T S T ∨ propagate⇩N⇩O⇩T S T ∨ backjump_l S T"
    using decide⇩N⇩O⇩T.intros[of S L] by auto
qed


context conflict_driven_clause_learning⇩W
begin
text ‹Notations are lost while proving locale inclusion:›
notation state_eq⇩N⇩O⇩T (infix "∼⇩N⇩O⇩T" 50)

subsection ‹Additional Lemmas between NOT and W states›
lemma trail⇩W_eq_reduce_trail_to⇩N⇩O⇩T_eq:
  "trail S = trail T ⟹ trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
proof (induction F S arbitrary: T rule: reduce_trail_to⇩N⇩O⇩T.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_to⇩N⇩O⇩T F (tl_trail S)) = trail (reduce_trail_to⇩N⇩O⇩T F (tl_trail T))"
    using IH by (metis (no_types) trail_tl_trail)
  then show "trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
    using tr by (metis (no_types) reduce_trail_to⇩N⇩O⇩T.elims)
qed

lemma trail_reduce_trail_to⇩N⇩O⇩T_add_learned_cls:
"no_dup (trail S) ⟹
  trail (reduce_trail_to⇩N⇩O⇩T M (add_learned_cls D S)) = trail (reduce_trail_to⇩N⇩O⇩T M S)"
 by (rule trail⇩W_eq_reduce_trail_to⇩N⇩O⇩T_eq) simp

lemma reduce_trail_to⇩N⇩O⇩T_reduce_trail_convert:
  "reduce_trail_to⇩N⇩O⇩T C S = reduce_trail_to (convert_trail_from_NOT C) S"
  apply (induction C S rule: reduce_trail_to⇩N⇩O⇩T.induct)
  apply (subst reduce_trail_to⇩N⇩O⇩T.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_to⇩N⇩O⇩T_map[simp]:
  "reduce_trail_to⇩N⇩O⇩T (map f M) S = reduce_trail_to⇩N⇩O⇩T M S"
  by (rule reduce_trail_to⇩N⇩O⇩T_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 cdcl⇩W_merge} (with merging) in
  NOT's @{const cdcl⇩N⇩O⇩T_merged_bj_learn}.›
lemma cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn:
  assumes
    inv: "cdcl⇩W_all_struct_inv S" and
    cdcl⇩W_restart: "cdcl⇩W_merge S T"
  shows "cdcl⇩N⇩O⇩T_merged_bj_learn S T
    ∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
  using cdcl⇩W_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 "propagate⇩N⇩O⇩T S T"
    using H CL T undef M_C by (auto simp: state_eq⇩N⇩O⇩T_def clauses_def simp del: state_simp)
  then show ?case
    using cdcl⇩N⇩O⇩T_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 "decide⇩N⇩O⇩T S T"
    apply (rule decide⇩N⇩O⇩T.decide⇩N⇩O⇩T)
       using undef_L apply (simp; fail)
     using atm_L inv apply (auto simp: cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def; fail)
    using T undef_L unfolding state_eq⇩N⇩O⇩T_def by (auto simp: clauses_def)
  then show ?case using cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T 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 "forget⇩N⇩O⇩T S T"
    apply (rule forget⇩N⇩O⇩T.forget⇩N⇩O⇩T)
       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_eq⇩N⇩O⇩T_def clauses_def ac_simps)
  then show ?case using cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T by blast
next
  case (fw_conflict S T U) note confl = this(1) and bj = this(2) and inv = this(3)
  obtain C⇩S CT where
    confl_T: "conflicting T = Some CT" and
    CT: "CT = C⇩S" and
    C⇩S: "C⇩S ∈# clauses S" and
    tr_S_C⇩S: "trail S ⊨as CNot C⇩S"
    using confl by (elim conflictE) auto
  have inv_T: "cdcl⇩W_all_struct_inv T"
    using cdcl⇩W_restart.simps cdcl⇩W_all_struct_inv_inv confl inv by blast
  then have "cdcl⇩W_M_level_inv T"
    unfolding cdcl⇩W_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_cdcl⇩W_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 cdcl⇩W_merge U"
      by (auto simp: cdcl⇩W_merge.simps elim: rulesE)
    ultimately show ?thesis by blast
  next
    case bt note s_or_r = this(1) and bt = this(2)
    have "cdcl⇩W_restart⇧*⇧* T T'"
      using s_or_r mono_rtranclp[of skip_or_resolve cdcl⇩W_restart]
        rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart
      by blast
    then have "cdcl⇩W_M_level_inv T'"
      using rtranclp_cdcl⇩W_restart_consistent_inv ‹cdcl⇩W_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 "cdcl⇩W_restart⇧*⇧* T T'"
      using rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart s_or_r by blast
    have inv_T': "cdcl⇩W_all_struct_inv T'"
      using ‹cdcl⇩W_restart⇧*⇧* T T'› inv_T rtranclp_cdcl⇩W_all_struct_inv_inv by blast
    have inv_U: "cdcl⇩W_all_struct_inv U"
      using cdcl⇩W_merge_restart_cdcl⇩W_restart confl fw_r_conflict inv local.bj
      rtranclp_cdcl⇩W_all_struct_inv_inv by blast

    have [simp]: "init_clss S = init_clss T'"
      using ‹cdcl⇩W_restart⇧*⇧* T T'› cdcl⇩W_restart_init_clss confl cdcl⇩W_all_struct_inv_def conflict
      inv by (metis rtranclp_cdcl⇩W_restart_init_clss)
    then have atm_L: "atm_of L ∈ atms_of_mm (clauses S)"
      using inv_T' confl_T' unfolding cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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_to⇩N⇩O⇩T M1 S) = M1"
      using M1_M2 confl by (subst reduce_trail_to⇩N⇩O⇩T_reduce_trail_convert)
      (auto simp: comp_def elim: rulesE)
    have "every_mark_is_a_conflict U"
      using inv_U unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def
              cdcl⇩W_M_level_inv_def apply (auto simp: state_eq⇩N⇩O⇩T_def
                trail_reduce_trail_to⇩N⇩O⇩T_add_learned_cls; fail)[]
            using C⇩S apply (auto; fail)[]
           using tr_S_C⇩S apply (simp; fail)

          using undef_L apply (auto; fail)[]
         using atm_L apply (simp add: trail_reduce_trail_to⇩N⇩O⇩T_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 cdcl⇩W_all_struct_inv_def
      distinct_cdcl⇩W_state_def by (auto simp: cdcl⇩W_M_level_inv_decomp backjump_l_cond_def
          dest: multi_member_split)
    then show ?thesis using cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l by fast
  qed
qed

abbreviation cdcl⇩N⇩O⇩T_restart where
"cdcl⇩N⇩O⇩T_restart ≡ restart_ops.cdcl⇩N⇩O⇩T_raw_restart cdcl⇩N⇩O⇩T restart"

lemma cdcl⇩W_merge_restart_is_cdcl⇩N⇩O⇩T_merged_bj_learn_restart_no_step:
  assumes
    inv: "cdcl⇩W_all_struct_inv S" and
    cdcl⇩W_restart:"cdcl⇩W_merge_restart S T"
  shows "cdcl⇩N⇩O⇩T_restart⇧*⇧* S T ∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
proof -
  consider
    (fw) "cdcl⇩W_merge S T" |
    (fw_r) "restart S T"
    using cdcl⇩W_restart by (meson cdcl⇩W_merge_restart.simps cdcl⇩W_rf.cases fw_conflict fw_decide fw_forget
      fw_propagate)
  then show ?thesis
  proof cases
    case fw
    then have IH: "cdcl⇩N⇩O⇩T_merged_bj_learn S T ∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
      using inv cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn by blast
    have invS: "inv⇩N⇩O⇩T S"
      using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
    have ff2: "cdcl⇩N⇩O⇩T⇧+⇧+ S T ⟶ cdcl⇩N⇩O⇩T⇧*⇧* 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 "cdcl⇩N⇩O⇩T ≤ cdcl⇩N⇩O⇩T_restart"
      by (auto simp: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.simps)
    then show ?thesis
      using ff3 ff2 IH cdcl⇩N⇩O⇩T_merged_bj_learn_is_tranclp_cdcl⇩N⇩O⇩T
        rtranclp_mono[of cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_restart] invS predicate2D by blast
  next
    case fw_r
    then show ?thesis by (blast intro: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.intros)
  qed
qed

abbreviation μ⇩F⇩W :: "'st ⇒ nat" where
"μ⇩F⇩W S ≡ (if no_step cdcl⇩W_merge S then 0 else 1+μ⇩C⇩D⇩C⇩L'_merged (set_mset (init_clss S)) S)"

lemma cdcl⇩W_merge_μ⇩F⇩W_decreasing:
  assumes
    inv: "cdcl⇩W_all_struct_inv S" and
    fw: "cdcl⇩W_merge S T"
  shows "μ⇩F⇩W T < μ⇩F⇩W S"
proof -
  let ?A = "init_clss S"
  have atm_clauses: "atms_of_mm (clauses S) ⊆ atms_of_mm ?A"
    using inv unfolding cdcl⇩W_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 cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def by auto
  have n_d: "no_dup (trail S)"
    using inv unfolding cdcl⇩W_all_struct_inv_def by (auto simp: cdcl⇩W_M_level_inv_decomp)
  have [simp]: "¬ no_step cdcl⇩W_merge S"
    using fw by auto
  have [simp]: "init_clss S = init_clss T"
    using cdcl⇩W_merge_restart_cdcl⇩W_restart[of S T] inv rtranclp_cdcl⇩W_restart_init_clss
    unfolding cdcl⇩W_all_struct_inv_def
    by (meson cdcl⇩W_merge.simps cdcl⇩W_merge_restart.simps cdcl⇩W_rf.simps fw)
  consider
    (merged) "cdcl⇩N⇩O⇩T_merged_bj_learn S T"  |
    (n_s) "no_step cdcl⇩W_merge T"
    using cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn inv fw by blast
  then show ?thesis
  proof cases
    case merged
    then show ?thesis
      using cdcl⇩N⇩O⇩T_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_cdcl⇩W_merge: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}"
  apply (rule wfP_if_measure[of _ _ "μ⇩F⇩W"])
  using cdcl⇩W_merge_μ⇩F⇩W_decreasing by blast

lemma tranclp_cdcl⇩W_merge_cdcl⇩W_merge_trancl:
  "{(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge⇧+⇧+ S T}
  ⊆ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}⇧+"
proof -
  have "(T, S) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}⇧+"
    if inv: "cdcl⇩W_all_struct_inv S" and "cdcl⇩W_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 "cdcl⇩W_all_struct_inv T"
        using st by (meson inv rtranclp_cdcl⇩W_all_struct_inv_inv
          rtranclp_cdcl⇩W_merge_rtranclp_cdcl⇩W_restart tranclp_into_rtranclp)
      then have "(U, T) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}⇧+"
        using s by auto
      then show ?case using IH by auto
    qed
  then show ?thesis by auto
qed

lemma wf_tranclp_cdcl⇩W_merge: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge⇧+⇧+ S T}"
  apply (rule wf_subset)
    apply (rule wf_trancl)
    using wf_cdcl⇩W_merge apply simp
  using tranclp_cdcl⇩W_merge_cdcl⇩W_merge_trancl by simp

lemma wf_cdcl⇩W_bj_all_struct: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_bj S T}"
  apply (rule wfP_if_measure[of "λ_. True"
      _ "λT. length (trail T) + (if conflicting T = None then 0 else 1)", simplified])
  using cdcl⇩W_bj_measure by (simp add: cdcl⇩W_all_struct_inv_def)

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

lemma trancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart:
  assumes "cdcl⇩W⇧+⇧+ S V" and inv: "cdcl⇩W_M_level_inv S" and "conflicting S = None"
  shows "(cdcl⇩W_merge⇧+⇧+ S V ∧ conflicting V = None)
    ∨ (∃T U. cdcl⇩W_merge⇧*⇧* S T ∧ conflicting V ≠ None ∧ conflict T U ∧ cdcl⇩W_bj⇧*⇧* U V)"
  using assms
proof induction
  case base
  then show ?case using cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart by blast
next
  case (step U V) note st = this(1) and cdcl⇩W = this(2) and IH = this(3)[OF this(4-)] and
    confl[simp] = this(5) and inv = this(4)
  from cdcl⇩W
  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 cdcl⇩W_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 "cdcl⇩W_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 cdcl⇩W_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: cdcl⇩W_bj.simps)
      then show ?thesis
      proof cases
        case s_or_r
        have f1: "cdcl⇩W_bj⇧+⇧+ U V"
          by (simp add: local.bj tranclp.r_into_trancl)
        obtain T T' :: 'st where
          f2: "cdcl⇩W_merge⇧+⇧+ S U
                ∨ cdcl⇩W_merge⇧*⇧* S T ∧ conflicting U ≠ None
                  ∧ conflict T T' ∧ cdcl⇩W_bj⇧*⇧* T' U"
          using IH confl by (meson bj rtranclp.intros(1)
              rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj
              rtranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_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
          "cdcl⇩W_merge⇧*⇧* S T" and
          "conflicting U ≠ None" and
          "conflict T T'" and
          "cdcl⇩W_bj⇧*⇧* T' U"
          using IH confl by (meson bj rtranclp.intros(1)
              rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj
              rtranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_restart)
        have invU: "cdcl⇩W_M_level_inv U"
          using inv rtranclp_cdcl⇩W_restart_consistent_inv step.hyps(1)
          by (meson ‹cdcl⇩W_bj⇧*⇧* T' U› ‹cdcl⇩W_merge⇧*⇧* S T› ‹conflict T T'›
              cdcl⇩W_restart_consistent_inv conflict rtranclp_cdcl⇩W_bj_rtranclp_cdcl⇩W_restart
              rtranclp_cdcl⇩W_merge_rtranclp_cdcl⇩W_restart)
        then have "conflicting V = None"
          using ‹backtrack U V› inv by (auto elim: backtrackE
              simp: cdcl⇩W_M_level_inv_decomp)
        have "full cdcl⇩W_bj T' V"
          apply (rule rtranclp_fullI[of cdcl⇩W_bj T' U V])
          using ‹cdcl⇩W_bj⇧*⇧* T' U› apply fast
          using ‹backtrack U V› backtrack_is_full1_cdcl⇩W_bj invU unfolding full1_def full_def
          by blast
        then show ?thesis
          using cdcl⇩W_merge.fw_conflict[of T T' V] ‹conflict T T'›
            ‹cdcl⇩W_merge⇧*⇧* S T› ‹conflicting V = None› by auto
      qed
    qed
  qed
qed

lemma wf_cdcl⇩W: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W S T}"
  unfolding wf_iff_no_infinite_down_chain
proof clarify
  fix f :: "nat ⇒ 'st"
  assume "∀i. (f (Suc i), f i) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W S T}"
  then have f: "⋀i. (f (Suc i), f i) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W S T}"
    by blast
  {
    fix f :: "nat ⇒ 'st"
    assume
      f: "(f (Suc i), f i) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W S T}" and
      confl: "conflicting (f i) ≠ None" for i
    have "(f (Suc i), f i) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_bj S T}" for i
      using f[of i] confl[of i] by (auto simp: cdcl⇩W.simps cdcl⇩W_o.simps cdcl⇩W_rf.simps
        elim!: rulesE)
    then have False
      using wf_cdcl⇩W_bj_all_struct unfolding wf_iff_no_infinite_down_chain by blast
  } note no_infinite_conflict = this

  have st: "cdcl⇩W⇧+⇧+ (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 ⟹ cdcl⇩W⇧+⇧+ (f i) (f j)" for i j :: nat
    using st[of i "j - i - 1"] by auto

  obtain i⇩b where i⇩b: "conflicting (f i⇩b) = None"
    using f no_infinite_conflict by blast

  define i⇩0 where i⇩0: "i⇩0 = Max {i⇩0. ∀i < i⇩0. conflicting (f i) ≠ None}"
  have "finite {i⇩0. ∀i < i⇩0. conflicting (f i) ≠ None}"
  proof -
    have "{i⇩0. ∀i < i⇩0. conflicting (f i) ≠ None} ⊆ {0..i⇩b}"
      using i⇩b 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 "{i⇩0. ∀i < i⇩0. conflicting (f i) ≠ None} ≠ {}"
    by auto
  ultimately have "i⇩0 ∈ {i⇩0. ∀i < i⇩0. conflicting (f i) ≠ None}"
    using Max_in[of "{i⇩0. ∀i<i⇩0. conflicting (f i) ≠ None}"] unfolding i⇩0 by fast
  then have confl_i⇩0: "conflicting (f i⇩0) = None"
  proof -
    have f1: "∀n<i⇩0. conflicting (f n) ≠ None"
      using ‹i⇩0 ∈ {i⇩0. ∀i<i⇩0. conflicting (f i) ≠ None}› by blast
    have "Suc i⇩0 ∉ {n. ∀na<n. conflicting (f na) ≠ None}"
      by (metis (lifting) Max_ge ‹finite {i⇩0. ∀i<i⇩0. conflicting (f i) ≠ None}›
          i⇩0 lessI not_le)
    then have "∃n<Suc i⇩0. conflicting (f n) = None"
      by fastforce
    then show "conflicting (f i⇩0) = None"
      using f1 by (metis le_less less_Suc_eq_le)
  qed
  have "∀i < i⇩0. conflicting (f i) ≠ None"
    using ‹i⇩0 ∈ {i⇩0. ∀i < i⇩0. 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 "cdcl⇩W_merge (?f j) (?f (Suc j))" for j :: nat
      using f[of "i+j+1"] confl that by (auto dest!: cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart)
    then have "(?f (Suc j), ?f j) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}"
      for j :: nat
      using f[of "i+j+1"] by auto
    then show False
      using wf_cdcl⇩W_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 "cdcl⇩W_bj (?f j) (?f (Suc j))" for j :: nat
      using f[of "i+j+1"] confl that by (auto simp: cdcl⇩W.simps cdcl⇩W_o.simps elim: rulesE)

    then have "(?f (Suc j), ?f j) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_bj S T}"
      for j :: nat
      using f[of "i+j+1"] by auto
    then show False
      using wf_cdcl⇩W_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 i⇩0 (λ_ i. LEAST j. j > i ∧ conflicting (f j) = None)"
  have g_0: "g 0 = i⇩0"
    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 > i⇩0 ∧ 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_i⇩0)
  have [simp]: "cdcl⇩W_M_level_inv (f i)" "cdcl⇩W_all_struct_inv (f i)" for i :: nat
    using f[of i] by (auto simp: cdcl⇩W_all_struct_inv_def)
  let ?fg = "λi. (f (g i))"
  have "∀i < Suc j. (f (g (Suc i)), f (g i)) ∈ {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge⇧+⇧+ S T}"
    for j :: nat
  proof (induction j)
    case 0
    have "cdcl⇩W⇧+⇧+ (?fg 0) (?fg 1)"
      using g_increasing[of 0] by (simp add: st)
    then show ?case by (auto dest!: trancl_cdcl⇩W_conflicting_true_cdcl⇩W_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 "cdcl⇩W_all_struct_inv (f ?i)"
      by auto
    ultimately have "cdcl⇩W⇧+⇧+ (f ?i) (f ?j)"
      using g_increasing by (simp add: st)
    then have "cdcl⇩W_merge⇧+⇧+ (f ?i) (f ?j)"
      by (auto dest!: trancl_cdcl⇩W_conflicting_true_cdcl⇩W_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). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge⇧+⇧+ S T}"
    by blast
  then show False
    using wf_tranclp_cdcl⇩W_merge unfolding wf_iff_no_infinite_down_chain by fast
qed

lemma wf_cdcl⇩W_stgy:
  ‹wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_stgy S T}›
  by (rule wf_subset[OF wf_cdcl⇩W]) (auto dest: cdcl⇩W_stgy_cdcl⇩W)

end


subsection ‹Inclusion of Weidendenbch's CDCL with Strategy›

context conflict_driven_clause_learning⇩W
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 inv⇩N⇩O⇩T_stgy where
"inv⇩N⇩O⇩T_stgy S ≡ conflicting S = None ∧ cdcl⇩W_all_struct_inv S ∧ no_smaller_propa S ∧
  cdcl⇩W_stgy_invariant S ∧ propagated_clauses_clauses S"

interpretation cdcl⇩W_with_strategy: cdcl⇩N⇩O⇩T_merge_bj_learn_ops where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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 cdcl⇩W_with_strategy: cdcl⇩N⇩O⇩T_merge_bj_learn_proxy where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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 = inv⇩N⇩O⇩T_stgy
  by unfold_locales

lemma cdcl⇩W_with_strategy_cdcl⇩N⇩O⇩T_merged_bj_learn_conflict:
  assumes
    "cdcl⇩W_with_strategy.cdcl⇩N⇩O⇩T_merged_bj_learn S T"
    "conflicting S = None"
  shows
    "conflicting T = None"
  using assms
  apply (cases rule: cdcl⇩W_with_strategy.cdcl⇩N⇩O⇩T_merged_bj_learn.cases;
    elim cdcl⇩W_with_strategy.forget⇩N⇩O⇩TE cdcl⇩W_with_strategy.propagate⇩N⇩O⇩TE
    cdcl⇩W_with_strategy.decide⇩N⇩O⇩TE rulesE
    cdcl⇩W_with_strategy.backjump_lE backjumpE)
  apply (auto elim!: rulesE simp: comp_def)
  done

lemma cdcl⇩W_with_strategy_no_forget⇩N⇩O⇩T[iff]: "cdcl⇩W_with_strategy.forget⇩N⇩O⇩T S T ⟷ False"
  by (auto elim: cdcl⇩W_with_strategy.forget⇩N⇩O⇩TE)

lemma cdcl⇩W_with_strategy_cdcl⇩N⇩O⇩T_merged_bj_learn_cdcl⇩W_stgy:
  assumes
    "cdcl⇩W_with_strategy.cdcl⇩N⇩O⇩T_merged_bj_learn S V"
  shows
    "cdcl⇩W_stgy⇧*⇧* S V"
  using assms
proof (cases rule: cdcl⇩W_with_strategy.cdcl⇩N⇩O⇩T_merged_bj_learn.cases)
  case cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T
  then show ?thesis
    apply (elim cdcl⇩W_with_strategy.decide⇩N⇩O⇩TE)
    using cdcl⇩W_stgy.other'[of S V] cdcl⇩W_o.decide[of S V] by blast
next
  case cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T
  then show ?thesis
    using cdcl⇩W_stgy.propagate' by (blast elim: cdcl⇩W_with_strategy.propagate⇩N⇩O⇩TE)
next
  case cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T
  then show ?thesis
    by blast
next
  case cdcl⇩N⇩O⇩T_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 cdcl⇩W_with_strategy.backjump_lE) blast
  have "cdcl⇩W_bj⇧*⇧* T U"
    using full mono_rtranclp[of skip_or_resolve cdcl⇩W_bj] unfolding full_def
    by (blast elim: skip_or_resolve.cases)
  moreover have "cdcl⇩W_bj U V" and "no_step cdcl⇩W_bj V"
    using bt by (auto dest: backtrack_no_cdcl⇩W_bj)
  ultimately have "full1 cdcl⇩W_bj T V"
    unfolding full1_def by auto
  then have "cdcl⇩W_stgy⇧*⇧* T V"
    using cdcl⇩W_s'.bj'[of T V] cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy[of T V] by blast
  then show ?thesis
    using confl cdcl⇩W_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 cdcl⇩W_bj_cdcl⇩W_stgy: ‹cdcl⇩W_bj S T ⟹ cdcl⇩W_stgy S T›
  by (rule cdcl⇩W_stgy.other') (auto simp: cdcl⇩W_bj.simps cdcl⇩W_o.simps elim!: rulesE)

lemma cdcl⇩W_restart_propagated_clauses_clauses:
  ‹cdcl⇩W_restart S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  by (induction rule: cdcl⇩W_restart_all_induct) (auto simp: propagated_clauses_clauses_def
      in_get_all_mark_of_propagated_in_trail simp: state_prop)

lemma rtranclp_cdcl⇩W_restart_propagated_clauses_clauses:
  ‹cdcl⇩W_restart⇧*⇧* S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  by (induction rule: rtranclp_induct) (auto simp: cdcl⇩W_restart_propagated_clauses_clauses)

lemma rtranclp_cdcl⇩W_stgy_propagated_clauses_clauses:
  ‹cdcl⇩W_stgy⇧*⇧* S T ⟹ propagated_clauses_clauses S ⟹ propagated_clauses_clauses T›
  using rtranclp_cdcl⇩W_restart_propagated_clauses_clauses[of S T]
    rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart by blast

lemma conflicting_clause_bt_lvl_gt_0_backjump:
  assumes
    inv: ‹inv⇩N⇩O⇩T_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 cdcl⇩W_stgy_invariant_def cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_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 ‹cdcl⇩W_stgy⇧*⇧* ?T U›
    using s_o_r by induction
      (auto simp: skip_or_resolve.simps dest!: cdcl⇩W_bj.intros cdcl⇩W_bj_cdcl⇩W_stgy)
  then have ‹cdcl⇩W_stgy⇧*⇧* S U›
    using confl_S_T by (auto dest!: cdcl⇩W_stgy.intros)
  then have
    inv_U: ‹cdcl⇩W_all_struct_inv U› and
    no_smaller_U: ‹no_smaller_propa U› and
    inv_stgy_U: ‹cdcl⇩W_stgy_invariant U›
    using inv rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv rtranclp_cdcl⇩W_stgy_no_smaller_propa
    rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant by blast+
  show ?thesis
  proof (cases C')
    case (add L D)
    then obtain V where ‹cdcl⇩W_stgy U V›
      using conflicting_no_false_can_do_step[of U C'] C' inv_U inv_stgy_U
      unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_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: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_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: ‹cdcl⇩W_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!: cdcl⇩W_bj.intros cdcl⇩W_bj_cdcl⇩W_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: ‹cdcl⇩W_stgy⇧*⇧* S (f k)› if ‹k < j› for k
      using confl_S_T that st_f_T[of k] by (auto dest!: cdcl⇩W_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, hide_lams) ‹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: ‹cdcl⇩W_all_struct_inv (f l)› and
      no_smaller_f_l: ‹no_smaller_propa (f l)› and
      inv_stgy_f_l: ‹cdcl⇩W_stgy_invariant (f l)› and
      propa_cls_f_l: ‹propagated_clauses_clauses (f l)›
      using inv st_f_s_k[OF ‹l < j›] rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv[of S "f l"]
        rtranclp_cdcl⇩W_stgy_no_smaller_propa[of S "f l"]
        rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant[of S "f l"]
        rtranclp_cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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: ‹cdcl⇩W_all_struct_inv S›
  shows ‹cdcl⇩W_with_strategy.backjump_l S V›
proof -
  have inv_U: ‹cdcl⇩W_all_struct_inv U›
    by (metis cdcl⇩W_stgy.conflict' cdcl⇩W_stgy_cdcl⇩W_all_struct_inv
        conf full full_def inv rtranclp_cdcl⇩W_all_struct_inv_inv
        rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart)
  then have inv_V: ‹cdcl⇩W_all_struct_inv V›
    by (metis backtrack bt cdcl⇩W_bj_cdcl⇩W_stgy cdcl⇩W_stgy_cdcl⇩W_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_eq⇩N⇩O⇩T_def
    by (auto simp del: state_simp dest!: state_simp(1))
  ultimately have V': ‹V ∼⇩N⇩O⇩T
    cons_trail (Propagated L dummy_cls) (reduce_trail_to⇩N⇩O⇩T M1 (add_learned_cls ?D' S))›
    using V T M tr_T_S[symmetric] M' clss_T_U[symmetric] unfolding state_eq⇩N⇩O⇩T_def
    by (auto simp del: state_simp
        simp: trail_reduce_trail_to⇩N⇩O⇩T_drop drop_map drop_tl clss_T_S)
  have ‹no_dup (trail V)›
    using inv_V V unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_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 cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
     apply simp_all
     using inv_V V not_tautology_mono[OF D_D'] distinct_mset_mono[OF D_D']
     unfolding cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
    by (auto simp: subset_mset_trans_add_mset)
  show ?thesis
    apply (rule cdcl⇩W_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 cdcl⇩W_with_strategy_propagate⇩N⇩O⇩T_propagate_iff[iff]:
  ‹cdcl⇩W_with_strategy.propagate⇩N⇩O⇩T 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 cdcl⇩W_with_strategy.propagate⇩N⇩O⇩T[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_eq⇩N⇩O⇩T_def clauses_def)
qed


interpretation cdcl⇩W_with_strategy: cdcl⇩N⇩O⇩T_merge_bj_learn where
  trail = "λS. convert_trail_from_W (trail S)" and
  clauses⇩N⇩O⇩T = clauses and
  prepend_trail = "λL S. cons_trail (convert_ann_lit_from_NOT L) S" and
  tl_trail = "λS. tl_trail S" and
  add_cls⇩N⇩O⇩T = "λC S. add_learned_cls C S" and
  remove_cls⇩N⇩O⇩T = "λ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 = inv⇩N⇩O⇩T_stgy
proof (unfold_locales, goal_cases)
  case (2 S T)
  then show ?case
    using cdcl⇩W_with_strategy_cdcl⇩N⇩O⇩T_merged_bj_learn_cdcl⇩W_stgy[of S T]
    cdcl⇩W_with_strategy_cdcl⇩N⇩O⇩T_merged_bj_learn_conflict[of S T]
    rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv rtranclp_cdcl⇩W_stgy_no_smaller_propa
    rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant rtranclp_cdcl⇩W_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 ‹inv⇩N⇩O⇩T_stgy S› unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_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 ‹inv⇩N⇩O⇩T_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 ‹inv⇩N⇩O⇩T_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(cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_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 cdcl⇩W_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 cdcl⇩W_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 ∼⇩N⇩O⇩T cons_trail (Decided L) S›
    by (simp add: state_eq⇩N⇩O⇩T_def del: state_simp)
  ultimately show "∃T. cdcl⇩W_with_strategy.decide⇩N⇩O⇩T S T ∨
    cdcl⇩W_with_strategy.propagate⇩N⇩O⇩T S T ∨
    cdcl⇩W_with_strategy.backjump_l S T"
    using cdcl⇩W_with_strategy.decide⇩N⇩O⇩T.intros[of S L "cons_trail (Decided L) S"]
    by auto
qed

thm cdcl⇩W_with_strategy.full_cdcl⇩N⇩O⇩T_merged_bj_learn_final_state

end

end