Theory CDCL_NOT

theory CDCL_NOT
imports
  Weidenbach_Book_Base.WB_List_More
  Weidenbach_Book_Base.Wellfounded_More
  Entailment_Definition.Partial_Annotated_Herbrand_Interpretation
  CDCL_WNOT_Measure
begin

section ‹NOT's CDCL›

subsection ‹Auxiliary Lemmas and Measure›

text ‹We define here some more simplification rules, or rules that have been useful as help
  for some tactic›

lemma atms_of_uminus_lit_atm_of_lit_of:
  ‹atms_of {# -lit_of x. x ∈# A#} = atm_of ` (lit_of ` (set_mset A))›
  unfolding atms_of_def by (auto simp add: Fun.image_comp)

lemma atms_of_ms_single_image_atm_of_lit_of:
  ‹atms_of_ms (unmark_s A) = atm_of ` (lit_of ` A)›
  unfolding atms_of_ms_def by auto


subsection ‹Initial Definitions›

subsubsection ‹The State›

text ‹We define here an abstraction over operation on the state we are manipulating.›
locale dpll_state_ops =
  fixes
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st›
begin
abbreviation stateNOT :: ‹'st ⇒ ('v, unit) ann_lit list × 'v clauses› where
‹stateNOT S ≡ (trail S, clausesNOT S)›
end

text ‹NOT's state is basically a pair composed of the trail (i.e.\ the candidate model) and the
  set of clauses. We abstract this state to convert this state to other states. like Weidenbach's
  five-tuple.›
locale dpll_state =
  dpll_state_ops
    trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT ― ‹related to the state›
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  assumes
    prepend_trailNOT:
      ‹stateNOT (prepend_trail L st) = (L # trail st, clausesNOT st)› and
    tl_trailNOT:
      ‹stateNOT (tl_trail st) = (tl (trail st), clausesNOT st)› and
    add_clsNOT:
      ‹stateNOT (add_clsNOT C st) = (trail st, add_mset C (clausesNOT st))› and
    remove_clsNOT:
      ‹stateNOT (remove_clsNOT C st) = (trail st, removeAll_mset C (clausesNOT st))›
begin
lemma
  trail_prepend_trail[simp]:
    ‹trail (prepend_trail L st) = L # trail st›
    and
  trail_tl_trailNOT[simp]: ‹trail (tl_trail st) = tl (trail st)› and
  trail_add_clsNOT[simp]: ‹trail (add_clsNOT C st) = trail st› and
  trail_remove_clsNOT[simp]: ‹trail (remove_clsNOT C st) = trail st› and

  clauses_prepend_trail[simp]:
    ‹clausesNOT (prepend_trail L st) = clausesNOT st›
    and
  clauses_tl_trail[simp]: ‹clausesNOT (tl_trail st) = clausesNOT st› and
  clauses_add_clsNOT[simp]:
    ‹clausesNOT (add_clsNOT C st) = add_mset C (clausesNOT st)› and
  clauses_remove_clsNOT[simp]:
    ‹clausesNOT (remove_clsNOT C st) = removeAll_mset C (clausesNOT st)›
  using prepend_trailNOT[of L st] tl_trailNOT[of st] add_clsNOT[of C st] remove_clsNOT[of C st]
  by (cases ‹stateNOT st›; auto)+

text ‹We define the following function doing the backtrack in the trail:›
function reduce_trail_toNOT :: ‹'a list ⇒ 'st ⇒ 'st› where
‹reduce_trail_toNOT F S =
  (if length (trail S) = length F ∨ trail S = [] then S else reduce_trail_toNOT F (tl_trail S))›
  by fast+
termination by (relation ‹measure (λ(_, S). length (trail S))›) auto

declare reduce_trail_toNOT.simps[simp del]

text ‹Then we need several lemmas about the @{term reduce_trail_toNOT}.›
lemma
  shows
  reduce_trail_toNOT_Nil[simp]: ‹trail S = [] ⟹ reduce_trail_toNOT F S = S› and
  reduce_trail_toNOT_eq_length[simp]: ‹length (trail S) = length F ⟹ reduce_trail_toNOT F S = S›
  by (auto simp: reduce_trail_toNOT.simps)

lemma reduce_trail_toNOT_length_ne[simp]:
  ‹length (trail S) ≠ length F ⟹ trail S ≠ [] ⟹
    reduce_trail_toNOT F S = reduce_trail_toNOT F (tl_trail S)›
  by (auto simp: reduce_trail_toNOT.simps)

lemma trail_reduce_trail_toNOT_length_le:
  assumes ‹length F > length (trail S)›
  shows ‹trail (reduce_trail_toNOT F S) = []›
  using assms by (induction F S rule: reduce_trail_toNOT.induct)
    (subst reduce_trail_toNOT.simps, simp add: less_imp_diff_less )

lemma trail_reduce_trail_toNOT_Nil[simp]:
  ‹trail (reduce_trail_toNOT [] S) = []›
  by (induction "[]" S rule: reduce_trail_toNOT.induct)
    (subst reduce_trail_toNOT.simps, simp add: less_imp_diff_less )


lemma clauses_reduce_trail_toNOT_Nil:
  ‹clausesNOT (reduce_trail_toNOT [] S) = clausesNOT S›
  by (induction ‹[]› S rule: reduce_trail_toNOT.induct)
  (simp add: less_imp_diff_less reduce_trail_toNOT.simps)

lemma trail_reduce_trail_toNOT_drop:
  ‹trail (reduce_trail_toNOT F S) =
    (if length (trail S) ≥ length F
    then drop (length (trail S) - length F) (trail S)
    else [])›
  apply (induction F S rule: reduce_trail_toNOT.induct)
  apply (rename_tac F S, case_tac ‹trail S›)
   apply auto[]
  apply (rename_tac list, case_tac ‹Suc (length list) > length F›)
   prefer 2 apply simp
  apply (subgoal_tac ‹Suc (length list) - length F = Suc (length list - length F)›)
   apply simp
  apply simp
  done

lemma reduce_trail_toNOT_skip_beginning:
  assumes ‹trail S = F' @ F›
  shows ‹trail (reduce_trail_toNOT F S) = F›
  using assms by (auto simp: trail_reduce_trail_toNOT_drop)

lemma reduce_trail_toNOT_clauses[simp]:
  ‹clausesNOT (reduce_trail_toNOT F S) = clausesNOT S›
  by (induction F S rule: reduce_trail_toNOT.induct)
  (simp add: less_imp_diff_less reduce_trail_toNOT.simps)

lemma trail_eq_reduce_trail_toNOT_eq:
  ‹trail S = trail T ⟹ trail (reduce_trail_toNOT F S) = trail (reduce_trail_toNOT F T)›
  apply (induction F S arbitrary: T rule: reduce_trail_toNOT.induct)
  by (metis trail_tl_trailNOT reduce_trail_toNOT_eq_length reduce_trail_toNOT_length_ne
    reduce_trail_toNOT_Nil)

lemma trail_reduce_trail_toNOT_add_clsNOT[simp]:
  ‹no_dup (trail S) ⟹
    trail (reduce_trail_toNOT F (add_clsNOT C S)) = trail (reduce_trail_toNOT F S)›
  by (rule trail_eq_reduce_trail_toNOT_eq) simp

lemma reduce_trail_toNOT_trail_tl_trail_decomp[simp]:
  ‹trail S = F' @ Decided K # F ⟹
     trail (reduce_trail_toNOT F (tl_trail S)) = F›
  apply (rule reduce_trail_toNOT_skip_beginning[of _ ‹tl (F' @ Decided K # [])›])
  by (cases F') (auto simp add:tl_append reduce_trail_toNOT_skip_beginning)

lemma reduce_trail_toNOT_length:
  ‹length M = length M' ⟹ reduce_trail_toNOT M S = reduce_trail_toNOT M' S›
  apply (induction M S rule: reduce_trail_toNOT.induct)
  by (simp add: reduce_trail_toNOT.simps)

abbreviation trail_weight where
‹trail_weight S ≡ map ((λl. 1 + length l) o snd) (get_all_ann_decomposition (trail S))›

text ‹As we are defining abstract states, the Isabelle equality about them is too strong: we want
  the weaker equivalence stating that two states are equal if they cannot be distinguished, i.e.\
  given the getter @{term trail} and @{term clausesNOT} do not distinguish them.›

definition state_eqNOT :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) where
‹S ∼ T ⟷ trail S = trail T ∧ clausesNOT S = clausesNOT T›

lemma state_eqNOT_ref[intro, simp]:
  ‹S ∼ S›
  unfolding state_eqNOT_def by auto

lemma state_eqNOT_sym:
  ‹S ∼ T ⟷ T ∼ S›
  unfolding state_eqNOT_def by auto

lemma state_eqNOT_trans:
  ‹S ∼ T ⟹ T ∼ U ⟹ S ∼ U›
  unfolding state_eqNOT_def by auto

lemma
  shows
    state_eqNOT_trail: ‹S ∼ T ⟹ trail S = trail T› and
    state_eqNOT_clauses: ‹S ∼ T ⟹ clausesNOT S = clausesNOT T›
  unfolding state_eqNOT_def by auto

lemmas state_simpNOT[simp] = state_eqNOT_trail state_eqNOT_clauses

lemma reduce_trail_toNOT_state_eqNOT_compatible:
  assumes ST: ‹S ∼ T›
  shows ‹reduce_trail_toNOT F S ∼ reduce_trail_toNOT F T›
proof -
  have ‹clausesNOT (reduce_trail_toNOT F S) = clausesNOT (reduce_trail_toNOT F T)›
    using ST by auto
  moreover have ‹trail (reduce_trail_toNOT F S) = trail (reduce_trail_toNOT F T)›
    using trail_eq_reduce_trail_toNOT_eq[of S T F] ST by auto
  ultimately show ?thesis by (auto simp del: state_simpNOT simp: state_eqNOT_def)
qed

end ― ‹End on locale @{locale dpll_state}.›


subsubsection ‹Definition of the Transitions›

text ‹Each possible is in its own locale.›
locale propagate_ops =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  fixes
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool›
begin
inductive propagateNOT :: ‹'st ⇒ 'st ⇒ bool› where
propagateNOT[intro]: ‹add_mset L C ∈# clausesNOT S ⟹ trail S ⊨as CNot C
    ⟹ undefined_lit (trail S) L
    ⟹ propagate_conds (Propagated L ()) S T
    ⟹ T ∼ prepend_trail (Propagated L ()) S
    ⟹ propagateNOT S T›
inductive_cases propagateNOTE[elim]: ‹propagateNOT S T›

end

locale decide_ops =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  fixes
    decide_conds :: ‹'st ⇒ 'st ⇒ bool›
begin
inductive decideNOT :: ‹'st ⇒ 'st ⇒ bool› where
decideNOT[intro]:
  ‹undefined_lit (trail S) L ⟹
  atm_of L ∈ atms_of_mm (clausesNOT S) ⟹
  T ∼ prepend_trail (Decided L) S ⟹
  decide_conds S T ⟹
  decideNOT S T›

inductive_cases decideNOTE[elim]: ‹decideNOT S S'›
end

locale backjumping_ops =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  fixes
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool›
begin

inductive backjump where
‹trail S = F' @ Decided K # F
   ⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_toNOT F S)
   ⟹ C ∈# clausesNOT S
   ⟹ trail S ⊨as CNot C
   ⟹ undefined_lit F L
   ⟹ atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))
   ⟹ clausesNOT S ⊨pm add_mset L C'
   ⟹ F ⊨as CNot C'
   ⟹ backjump_conds C C' L S T
   ⟹ backjump S T›
inductive_cases backjumpE: ‹backjump S T›

text ‹The condition @{term ‹atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›}
  is not implied by the the condition @{term ‹clausesNOT S ⊨pm add_mset L C'›} (no negation).›
end


subsection ‹DPLL with Backjumping›

locale dpll_with_backjumping_ops =
  propagate_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT propagate_conds +
  decide_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT decide_conds +
  backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT backjump_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› +
  assumes
    bj_can_jump:
      ‹⋀S C F' K F L.
        inv S ⟹
        trail S = F' @ Decided K # F ⟹
        C ∈# clausesNOT S ⟹
        trail S ⊨as CNot C ⟹
        undefined_lit F L ⟹
        atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (F' @ Decided K # F)) ⟹
        clausesNOT S ⊨pm add_mset L C' ⟹
        F ⊨as CNot C' ⟹
        ¬no_step backjump S› and
    can_propagate_or_decide_or_backjump:
      ‹atm_of L ∈ atms_of_mm (clausesNOT S) ⟹
      undefined_lit (trail S) L ⟹
      satisfiable (set_mset (clausesNOT S)) ⟹
      inv S ⟹
      no_dup (trail S) ⟹
      ∃T. decideNOT S T ∨ propagateNOT S T ∨ backjump S T›
begin

text ‹We cannot add a like condition @{term ‹atms_of C' ⊆ atms_of_ms N›} to ensure that we
  can backjump even if the last decision variable has disappeared from the set of clauses.

  The part of the condition @{term ‹atm_of L ∈ atm_of ` (lits_of_l (F' @ Decided K # F))›} is
  important, otherwise you are not sure that you can backtrack.›

subsubsection ‹Definition›

text ‹We define dpll with backjumping:›
inductive dpll_bj :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
bj_decideNOT: ‹decideNOT S S' ⟹ dpll_bj S S'› |
bj_propagateNOT: ‹propagateNOT S S' ⟹ dpll_bj S S'› |
bj_backjump: ‹backjump S S' ⟹ dpll_bj S S'›

lemmas dpll_bj_induct = dpll_bj.induct[split_format(complete)]
thm dpll_bj_induct[OF dpll_with_backjumping_ops_axioms]
lemma dpll_bj_all_induct[consumes 2, case_names decideNOT propagateNOT backjump]:
  fixes S T :: ‹'st›
  assumes
    ‹dpll_bj S T› and
    ‹inv S›
    ‹⋀L T. undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_mm (clausesNOT S)
      ⟹ T ∼ prepend_trail (Decided L) S
      ⟹ P S T› and
    ‹⋀C L T. add_mset L C ∈# clausesNOT S ⟹ trail S ⊨as CNot C ⟹ undefined_lit (trail S) L
      ⟹ T ∼ prepend_trail (Propagated L ()) S
      ⟹ P S T› and
    ‹⋀C F' K F L C' T. C ∈# clausesNOT S ⟹ F' @ Decided K # F ⊨as CNot C
      ⟹ trail S = F' @ Decided K # F
      ⟹ undefined_lit F L
      ⟹ atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (F' @ Decided K # F))
      ⟹ clausesNOT S ⊨pm add_mset L C'
      ⟹ F ⊨as CNot C'
      ⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_toNOT F S)
      ⟹ P S T›
  shows ‹P S T›
  apply (induct T rule: dpll_bj_induct[OF local.dpll_with_backjumping_ops_axioms])
     apply (rule assms(1))
    using assms(3) apply blast
   apply (elim propagateNOTE) using assms(4) apply blast
  apply (elim backjumpE) using assms(5) ‹inv S› by simp


subsubsection ‹Basic properties›

paragraph ‹First, some better suited induction principle›
lemma dpll_bj_clauses:
  assumes ‹dpll_bj S T› and ‹inv S›
  shows ‹clausesNOT S = clausesNOT T›
  using assms by (induction rule: dpll_bj_all_induct) auto

paragraph ‹No duplicates in the trail›
lemma dpll_bj_no_dup:
  assumes ‹dpll_bj S T› and ‹inv S›
  and ‹no_dup (trail S)›
  shows ‹no_dup (trail T)›
  using assms by (induction rule: dpll_bj_all_induct)
  (auto simp add: defined_lit_map reduce_trail_toNOT_skip_beginning dest: no_dup_appendD)

paragraph ‹Valuations›
lemma dpll_bj_sat_iff:
  assumes ‹dpll_bj S T› and ‹inv S›
  shows ‹I ⊨sm clausesNOT S ⟷ I ⊨sm clausesNOT T›
  using assms by (induction rule: dpll_bj_all_induct) auto

paragraph ‹Clauses›
lemma dpll_bj_atms_of_ms_clauses_inv:
  assumes
    ‹dpll_bj S T› and
    ‹inv S›
  shows ‹atms_of_mm (clausesNOT S) = atms_of_mm (clausesNOT T)›
  using assms by (induction rule: dpll_bj_all_induct) auto

lemma dpll_bj_atms_in_trail:
  assumes
    ‹dpll_bj S T› and
    ‹inv S› and
    ‹atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (clausesNOT S)›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ atms_of_mm (clausesNOT S)›
  using assms by (induction rule: dpll_bj_all_induct)
  (auto simp: in_plus_implies_atm_of_on_atms_of_ms reduce_trail_toNOT_skip_beginning)

lemma dpll_bj_atms_in_trail_in_set:
  assumes ‹dpll_bj S T›and
    ‹inv S› and
  ‹atms_of_mm (clausesNOT S) ⊆ A› and
  ‹atm_of ` (lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A›
  using assms by (induction rule: dpll_bj_all_induct)
  (auto simp: in_plus_implies_atm_of_on_atms_of_ms)

lemma dpll_bj_all_decomposition_implies_inv:
  assumes
    ‹dpll_bj S T› and
    inv: ‹inv S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
  using assms(1,2)
proof (induction rule:dpll_bj_all_induct)
  case decideNOT
  then show ?case using decomp by auto
next
  case (propagateNOT C L T) note propa = this(1) and undef = this(3) and T = this(4)
  let ?M' = ‹trail (prepend_trail (Propagated L ()) S)›
  let ?N = ‹clausesNOT S›
  obtain a y l where ay: ‹get_all_ann_decomposition ?M' = (a, y) # l›
    by (cases ‹get_all_ann_decomposition ?M'›) fastforce+
  then have M': ‹?M' = y @ a› using get_all_ann_decomposition_decomp[of ?M'] by auto
  have M: ‹get_all_ann_decomposition (trail S) = (a, tl y) # l›
    using ay undef by (cases ‹ get_all_ann_decomposition (trail S)›) auto
  have y0: ‹y = (Propagated L ()) # (tl y)›
    using ay undef by (auto simp add: M)
  from arg_cong[OF this, of set] have y[simp]: ‹set y = insert (Propagated L ()) (set (tl y))›
    by simp
  have tr_S: ‹trail S = tl y @ a›
    using arg_cong[OF M', of tl] y0 M get_all_ann_decomposition_decomp by force
  have a_Un_N_M: ‹unmark_l a ∪ set_mset ?N ⊨ps unmark_l (tl y)›
    using decomp ay unfolding all_decomposition_implies_def by (simp add: M)+

  moreover have ‹unmark_l a ∪ set_mset ?N ⊨p {#L#}› (is ‹?I ⊨p _›)
  proof (rule true_clss_cls_plus_CNot)
    show ‹?I ⊨p add_mset L C›
      using propa propagateNOT.prems by (auto dest!: true_clss_clss_in_imp_true_clss_cls)
  next
    have ‹unmark_l ?M' ⊨ps CNot C›
      using ‹trail S ⊨as CNot C› undef by (auto simp add: true_annots_true_clss_clss)
    have a1: ‹unmark_l a ∪ unmark_l (tl y) ⊨ps CNot C›
      using propagateNOT.hyps(2) tr_S true_annots_true_clss_clss
      by (force simp add: image_Un sup_commute)
    then have ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨ps unmark_l a ∪ unmark_l (tl y)›
      using a_Un_N_M true_clss_clss_def by blast
    then show ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨ps CNot C›
      using a1 by (meson true_clss_clss_left_right true_clss_clss_union_and
          true_clss_clss_union_l_r)
  qed
  ultimately have ‹unmark_l a ∪ set_mset ?N ⊨ps unmark_l ?M'›
    unfolding M' by (auto simp add: all_in_true_clss_clss image_Un)
  then show ?case
    using decomp T M undef unfolding ay all_decomposition_implies_def by (auto simp add: ay)
next
  case (backjump C F' K F L D T) note confl = this(2) and tr = this(3) and undef = this(4) and
    L = this(5) and N_C = this(6) and vars_D = this(5) and T = this(8)
  have decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition F)›
    using decomp unfolding tr all_decomposition_implies_def
    by (metis (no_types, lifting) get_all_ann_decomposition.simps(1)
      get_all_ann_decomposition_never_empty hd_Cons_tl insert_iff list.sel(3) list.set(2)
      tl_get_all_ann_decomposition_skip_some)

  obtain a b li where F: ‹get_all_ann_decomposition F = (a, b) # li›
    by (cases ‹get_all_ann_decomposition F›) auto
  have ‹F = b @ a›
    using get_all_ann_decomposition_decomp[of F a b] F by auto
  have a_N_b:‹unmark_l a ∪ set_mset (clausesNOT S) ⊨ps unmark_l b›
    using decomp unfolding all_decomposition_implies_def by (auto simp add: F)

  have F_D: ‹unmark_l F ⊨ps CNot D›
    using ‹F ⊨as CNot D› by (simp add: true_annots_true_clss_clss)
  then have ‹unmark_l a ∪ unmark_l b ⊨ps CNot D›
    unfolding ‹F = b @ a› by (simp add: image_Un sup.commute)
  have a_N_CNot_D: ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨ps CNot D ∪ unmark_l b›
    apply (rule true_clss_clss_left_right)
    using a_N_b F_D unfolding ‹F = b @ a› by (auto simp add: image_Un ac_simps)

  have a_N_D_L: ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨p add_mset L D›
    by (simp add: N_C)
  have ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨p {#L#}›
    using a_N_D_L a_N_CNot_D by (blast intro: true_clss_cls_plus_CNot)
  then show ?case
    using decomp T tr undef unfolding all_decomposition_implies_def by (auto simp add: F)
qed


subsubsection ‹Termination›

paragraph ‹Using a proper measure›
lemma length_get_all_ann_decomposition_append_Decided:
  ‹length (get_all_ann_decomposition (F' @ Decided K # F)) =
    length (get_all_ann_decomposition F')
    + length (get_all_ann_decomposition (Decided K # F))
    - 1›
  by (induction F' rule: ann_lit_list_induct) auto

lemma take_length_get_all_ann_decomposition_decided_sandwich:
  ‹take (length (get_all_ann_decomposition F))
      (map (f o snd) (rev (get_all_ann_decomposition (F' @ Decided K # F))))
      =
     map (f o snd) (rev (get_all_ann_decomposition F))
    ›
proof (induction F' rule: ann_lit_list_induct)
  case Nil
  then show ?case by auto
next
  case (Decided K)
  then show ?case by (simp add: length_get_all_ann_decomposition_append_Decided)
next
  case (Propagated L m F') note IH = this(1)
  obtain a b l where F': ‹get_all_ann_decomposition (F' @ Decided K # F) = (a, b) # l›
    by (cases ‹get_all_ann_decomposition (F' @ Decided K # F)›) auto
  have ‹length (get_all_ann_decomposition F) - length l = 0›
    using length_get_all_ann_decomposition_append_Decided[of F' K F]
    unfolding F' by (cases ‹get_all_ann_decomposition F'›) auto
  then show ?case
    using IH by (simp add: F')
qed

lemma length_get_all_ann_decomposition_length:
  ‹length (get_all_ann_decomposition M) ≤ 1 + length M›
  by (induction M rule: ann_lit_list_induct) auto

lemma length_in_get_all_ann_decomposition_bounded:
  assumes i:‹i ∈ set (trail_weight S)›
  shows ‹i ≤ Suc (length (trail S))›
proof -
  obtain a b where
    ‹(a, b) ∈ set (get_all_ann_decomposition (trail S))› and
    ib: ‹i = Suc (length b)›
    using i by auto
  then obtain c where ‹trail S = c @ b @ a›
    using get_all_ann_decomposition_exists_prepend' by metis
  from arg_cong[OF this, of length] show ?thesis using i ib by auto
qed


paragraph ‹Well-foundedness›
text ‹The bounds are the following:
  ▪ @{term ‹1+card (atms_of_ms A)›}: @{term ‹card (atms_of_ms A)›} is an upper bound on the length
  of the list. As @{term get_all_ann_decomposition} appends an possibly empty couple at the end,
  adding one is needed.
  ▪ @{term ‹2+card (atms_of_ms A)›}: @{term ‹card (atms_of_ms A)›} is an upper bound on the number
  of elements, where adding one is necessary for the same reason as for the bound on the list, and
  one is needed to have a strict bound.
  ›
abbreviation unassigned_lit :: ‹'b clause set ⇒ 'a list ⇒ nat› where
  ‹unassigned_lit N M ≡ card (atms_of_ms N) - length M›

lemma dpll_bj_trail_mes_increasing_prop:
  fixes M :: ‹('v, unit) ann_lits › and N :: ‹'v clauses›
  assumes
    ‹dpll_bj S T› and
    ‹inv S› and
    NA: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    MA: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite A›
  shows ‹μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
    > μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)›
  using assms(1,2)
proof (induction rule: dpll_bj_all_induct)
  case (propagateNOT C L T) note CLN = this(1) and MC = this(2) and undef_L = this(3) and T = this(4)
  have incl: ‹atm_of ` lits_of_l (Propagated L () # trail S) ⊆ atms_of_ms A›
    using propagateNOT dpll_bj_atms_in_trail_in_set bj_propagateNOT NA MA CLN
    by (auto simp: in_plus_implies_atm_of_on_atms_of_ms)

  have no_dup: ‹no_dup (Propagated L () # trail S)›
    using defined_lit_map n_d undef_L by auto
  obtain a b l where M: ‹get_all_ann_decomposition (trail S) = (a, b) # l›
    by (cases ‹get_all_ann_decomposition (trail S)›) auto
  have b_le_M: ‹length b ≤ length (trail S)›
    using get_all_ann_decomposition_decomp[of ‹trail S›] by (simp add: M)
  have ‹finite (atms_of_ms A)› using finite by simp

  then have ‹length (Propagated L () # trail S) ≤ card (atms_of_ms A)›
    using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of_l[OF no_dup]
    by (simp add: card_mono)
  then have latm: ‹unassigned_lit A b = Suc (unassigned_lit A (Propagated L () # b))›
    using b_le_M by auto
  then show ?case using T undef_L by (auto simp: latm M μC_cons)
next
  case (decideNOT L) note undef_L = this(1) and MC = this(2) and T = this(3)
  have incl: ‹atm_of ` lits_of_l (Decided L # (trail S)) ⊆ atms_of_ms A›
    using dpll_bj_atms_in_trail_in_set bj_decideNOT decideNOT.decideNOT[OF decideNOT.hyps] NA MA MC
    by auto

  have no_dup: ‹no_dup (Decided L # (trail S))›
    using defined_lit_map n_d undef_L by auto
  obtain a b l where M: ‹get_all_ann_decomposition (trail S) = (a, b) # l›
    by (cases ‹get_all_ann_decomposition (trail S)›) auto

  then have ‹length (Decided L # (trail S)) ≤ card (atms_of_ms A)›
    using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of_l[OF no_dup]
    by (simp add: card_mono)
  show ?case using T undef_L by (simp add: μC_cons)
next
  case (backjump C F' K F L C' T) note undef_L = this(4) and MC = this(1) and tr_S = this(3) and
    L = this(5) and T = this(8)
  have incl: ‹atm_of ` lits_of_l (Propagated L () # F) ⊆ atms_of_ms A›
    using dpll_bj_atms_in_trail_in_set NA MA L by (auto simp: tr_S)

  have no_dup: ‹no_dup (Propagated L () # F)›
    using defined_lit_map n_d undef_L tr_S by (auto dest: no_dup_appendD)
  obtain a b l where M: ‹get_all_ann_decomposition (trail S) = (a, b) # l›
    by (cases ‹get_all_ann_decomposition (trail S)›) auto
  have b_le_M: ‹length b ≤ length (trail S)›
    using get_all_ann_decomposition_decomp[of ‹trail S›] by (simp add: M)
  have fin_atms_A: ‹finite (atms_of_ms A)› using finite by simp

  then have F_le_A: ‹length (Propagated L () # F) ≤ card (atms_of_ms A)›
    using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of_l[OF no_dup]
    by (simp add: card_mono)
  have tr_S_le_A: ‹length (trail S) ≤ card (atms_of_ms A)›
    using n_d MA by (metis fin_atms_A card_mono no_dup_length_eq_card_atm_of_lits_of_l)
  obtain a b l where F: ‹get_all_ann_decomposition F = (a, b) # l›
    by (cases ‹get_all_ann_decomposition F›) auto
  then have ‹F = b @ a›
    using get_all_ann_decomposition_decomp[of ‹Propagated L () # F› a
      ‹Propagated L () # b›] by simp
  then have latm: ‹unassigned_lit A b = Suc (unassigned_lit A (Propagated L () # b))›
     using F_le_A by simp
  obtain rem where
    rem:‹map (λa. Suc (length (snd a))) (rev (get_all_ann_decomposition (F' @ Decided K # F)))
    = map (λa. Suc (length (snd a))) (rev (get_all_ann_decomposition F)) @ rem›
    using take_length_get_all_ann_decomposition_decided_sandwich[of F ‹λa. Suc (length a)› F' K]
    unfolding o_def by (metis append_take_drop_id)
  then have rem: ‹map (λa. Suc (length (snd a)))
      (get_all_ann_decomposition (F' @ Decided K # F))
    = rev rem @ map (λa. Suc (length (snd a))) ((get_all_ann_decomposition F))›
    by (simp add: rev_map[symmetric] rev_swap)
  have ‹length (rev rem @ map (λa. Suc (length (snd a))) (get_all_ann_decomposition F))
          ≤ Suc (card (atms_of_ms A))›
    using arg_cong[OF rem, of length] tr_S_le_A
    length_get_all_ann_decomposition_length[of ‹F' @ Decided K # F›] tr_S by auto
  moreover {
    { fix i :: nat and xs :: ‹'a list›
      have ‹i < length xs ⟹ length xs - Suc i < length xs›
        by auto
      then have H: ‹i<length xs ⟹ rev xs ! i ∈ set xs›
        using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
    } note H = this
    have ‹∀i<length rem. rev rem ! i < card (atms_of_ms A) + 2›
      using tr_S_le_A length_in_get_all_ann_decomposition_bounded[of _ S] unfolding tr_S
      by (force simp add: o_def rem dest!: H intro: length_get_all_ann_decomposition_length) }
  ultimately show ?case
    using μC_bounded[of ‹rev rem› ‹card (atms_of_ms A)+2› ‹unassigned_lit A l›] T undef_L
    by (simp add: rem μC_append μC_cons F tr_S)
qed

lemma dpll_bj_trail_mes_decreasing_prop:
  assumes dpll: ‹dpll_bj S T› and inv: ‹inv S› and
  N_A: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
  M_A: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
  nd: ‹no_dup (trail S)› and
  fin_A: ‹finite A›
  shows ‹(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
               - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
            < (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
               - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)›
proof -
  let ?b = ‹2+card (atms_of_ms A)›
  let ?s = ‹1+card (atms_of_ms A)›
  let ?μ = ‹μC ?s ?b›
  have M'_A: ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
    by (meson M_A N_A dpll dpll_bj_atms_in_trail_in_set inv)
  have nd': ‹no_dup (trail T)›
    using ‹dpll_bj S T› dpll_bj_no_dup nd inv by blast
  { fix i :: nat and xs :: ‹'a list›
    have ‹i < length xs ⟹ length xs - Suc i < length xs›
      by auto
    then have H: ‹i<length xs ⟹ xs ! i ∈ set xs›
      using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
  } note H = this

  have l_M_A: ‹length (trail S) ≤ card (atms_of_ms A)›
    by (simp add: fin_A M_A card_mono no_dup_length_eq_card_atm_of_lits_of_l nd)
  have l_M'_A: ‹length (trail T) ≤ card (atms_of_ms A)›
    by (simp add: fin_A M'_A card_mono no_dup_length_eq_card_atm_of_lits_of_l nd')
  have l_trail_weight_M: ‹length (trail_weight T) ≤ 1+card (atms_of_ms A)›
     using l_M'_A length_get_all_ann_decomposition_length[of ‹trail T›] by auto
  have bounded_M: ‹∀i<length (trail_weight T). (trail_weight T)! i < card (atms_of_ms A) + 2›
    using length_in_get_all_ann_decomposition_bounded[of _ T] l_M'_A
    by (metis (no_types, lifting) H Nat.le_trans add_2_eq_Suc' not_le not_less_eq_eq)

  from dpll_bj_trail_mes_increasing_prop[OF dpll inv N_A M_A nd fin_A]
  have ‹μC ?s ?b (trail_weight S) < μC ?s ?b (trail_weight T)› by simp
  moreover from μC_bounded[OF bounded_M l_trail_weight_M]
    have ‹μC ?s ?b (trail_weight T) ≤ ?b ^ ?s› by auto
  ultimately show ?thesis by linarith
qed

lemma wf_dpll_bj: (*  \htmllink{wf_dpll_bj} *)
  assumes fin: ‹finite A›
  shows ‹wf {(T, S). dpll_bj S T
    ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S) ∧ inv S}›
  (is ‹wf ?A›)
proof (rule wf_bounded_measure[of _
        ‹λ_. (2 + card (atms_of_ms A))^(1 + card (atms_of_ms A))›
        ‹λS. μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)›])
  fix a b :: ‹'st›
  let ?b = ‹2+card (atms_of_ms A)›
  let ?s = ‹1+card (atms_of_ms A)›
  let ?μ = ‹μC ?s ?b›
  assume ab: ‹(b, a) ∈ ?A›

  have fin_A: ‹finite (atms_of_ms A)›
    using fin by auto
  have
    dpll_bj: ‹dpll_bj a b› and
    N_A: ‹atms_of_mm (clausesNOT a) ⊆ atms_of_ms A› and
    M_A: ‹atm_of ` lits_of_l (trail a) ⊆ atms_of_ms A› and
    nd: ‹no_dup (trail a)› and
    inv: ‹inv a›
    using ab by auto

  have M'_A: ‹atm_of ` lits_of_l (trail b) ⊆ atms_of_ms A›
    by (meson M_A N_A ‹dpll_bj a b› dpll_bj_atms_in_trail_in_set inv)
  have nd': ‹no_dup (trail b)›
    using ‹dpll_bj a b› dpll_bj_no_dup nd inv by blast
  { fix i :: nat and xs :: ‹'a list›
    have ‹i < length xs ⟹ length xs - Suc i < length xs›
      by auto
    then have H: ‹i<length xs ⟹ xs ! i ∈ set xs›
      using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
  } note H = this

  have l_M_A: ‹length (trail a) ≤ card (atms_of_ms A)›
    by (simp add: fin_A M_A card_mono no_dup_length_eq_card_atm_of_lits_of_l nd)
  have l_M'_A: ‹length (trail b) ≤ card (atms_of_ms A)›
    by (simp add: fin_A M'_A card_mono no_dup_length_eq_card_atm_of_lits_of_l nd')
  have l_trail_weight_M: ‹length (trail_weight b) ≤ 1+card (atms_of_ms A)›
     using l_M'_A length_get_all_ann_decomposition_length[of ‹trail b›] by auto
  have bounded_M: ‹∀i<length (trail_weight b). (trail_weight b)! i < card (atms_of_ms A) + 2›
    using length_in_get_all_ann_decomposition_bounded[of _ b] l_M'_A
    by (metis (no_types, lifting) Nat.le_trans One_nat_def Suc_1 add.right_neutral add_Suc_right
      le_imp_less_Suc less_eq_Suc_le nth_mem)

  from dpll_bj_trail_mes_increasing_prop[OF dpll_bj inv N_A M_A nd fin]
  have ‹μC ?s ?b (trail_weight a) < μC ?s ?b (trail_weight b)› by simp
  moreover from μC_bounded[OF bounded_M l_trail_weight_M]
    have ‹μC ?s ?b (trail_weight b) ≤ ?b ^ ?s› by auto
  ultimately show ‹?b ^ ?s ≤ ?b ^ ?s ∧
           μC ?s ?b (trail_weight b) ≤ ?b ^ ?s ∧
           μC ?s ?b (trail_weight a) < μC ?s ?b (trail_weight b)›
    by blast
qed

paragraph ‹Alternative termination proof›

abbreviation DPLL_mesW where
  ‹DPLL_mesW A M ≡
    map (λL. if is_decided L then 2::nat else 1) (rev M) @ replicate (card A - length M) 3›

lemma distinctcard_atm_of_lit_of_eq_length:
  assumes "no_dup S"
  shows "card (atm_of ` lits_of_l S) = length S"
  using assms by (induct S) (auto simp add: image_image lits_of_def no_dup_def)

lemma dpll_bj_trail_mes_decreasing_less_than:
  assumes dpll: ‹dpll_bj S T› and inv: ‹inv S› and
    N_A: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    M_A: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    nd: ‹no_dup (trail S)› and
    fin_A: ‹finite A›
  shows ‹(DPLL_mesW (atms_of_ms A) (trail T), DPLL_mesW (atms_of_ms A) (trail S)) ∈
    lexn less_than (card ((atms_of_ms A)))›
  using assms(1,2)
proof (induction rule: dpll_bj_all_induct)
  case (decideNOT L T)
  define n where
    ‹n = card (atms_of_ms A) - card (atm_of ` lits_of_l (trail S))›

  have [simp]: ‹length (trail S) = card (atm_of ` lits_of_l (trail S))›
    using nd by (auto simp: no_dup_def lits_of_def image_image dest: distinct_card)
  have ‹atm_of L ∉ atm_of ` lits_of_l (trail S)›
    by (metis decideNOT.hyps(1) defined_lit_map imageE in_lits_of_l_defined_litD)

  have ‹card (atms_of_ms A) > card (atm_of ` lits_of_l (trail S))›
    by (metis N_A ‹atm_of L ∉ atm_of ` lits_of_l (trail S)› atms_of_ms_finite card_seteq decideNOT.hyps(2)
        M_A fin_A not_le subsetCE)
  then have
    n_0: ‹n > 0› and
    n_Suc: ‹card (atms_of_ms A) - Suc (card (atm_of ` lits_of_l (trail S))) = n - 1›
    unfolding n_def by auto

  show ?case
    using fin_A decideNOT n_0 unfolding state_eqNOT_trail[OF decideNOT(3)]
    by (cases n) (auto simp: prepend_same_lexn n_def[symmetric] n_Suc lexn_Suc
        simp del: state_simpNOT lexn.simps)
next
  case (propagateNOT C L T) note C = this(1) and undef = this(3) and T = this(3)
  then have ‹card (atms_of_ms A) > length (trail S)›
  proof -
    have f7: "atm_of L ∈ atms_of_ms A"
      using N_A C in_m_in_literals by blast
    have "undefined_lit (trail S) (- L)"
      using undef by auto
    then show ?thesis
      using f7 nd fin_A M_A undef by (metis atm_of_in_atm_of_set_in_uminus atms_of_ms_finite
          card_seteq in_lits_of_l_defined_litD leI no_dup_length_eq_card_atm_of_lits_of_l)
  qed
  then show ?case
    using fin_A unfolding state_eqNOT_trail[OF propagateNOT(4)]
    by (cases ‹card (atms_of_ms A) - length (trail S)›)
      (auto simp: prepend_same_lexn lexn_Suc
        simp del: state_simpNOT lexn.simps)
next
  case (backjump C F' K F L C' T) note tr_S = this(3)
  have ‹trail (reduce_trail_toNOT F S) = F›
    by (simp add: tr_S)
  have ‹no_dup F›
    using nd tr_S by (auto dest: no_dup_appendD)
  then have card_A_F: ‹card (atms_of_ms A) > length F›
    using distinctcard_atm_of_lit_of_eq_length[of ‹trail S›] card_mono[OF _ M_A] fin_A nd tr_S
    by auto
  have ‹no_dup (F' @ F)›
    using nd tr_S by (auto dest: no_dup_appendD)
  then have ‹no_dup F'›
    apply (subst (asm) no_dup_rev[symmetric])
    using nd tr_S by (auto dest: no_dup_appendD)
  then have card_A_F': ‹card (atms_of_ms A) > length F' + length F›
    using distinctcard_atm_of_lit_of_eq_length[of ‹trail S›] card_mono[OF _ M_A] fin_A nd tr_S
    by auto
  show ?case
    using card_A_F card_A_F'
    unfolding state_eqNOT_trail[OF backjump(8)]
    by (cases ‹card (atms_of_ms A) - length F›)
      (auto simp: tr_S prepend_same_lexn lexn_Suc simp del: state_simpNOT lexn.simps)
qed

lemma
  assumes fin[simp]: ‹finite A›
  shows ‹wf {(T, S). dpll_bj S T
    ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S) ∧ inv S}›
    (is ‹wf ?A›)
  unfolding conj_commute[of ‹dpll_bj _ _›]
  apply (rule wf_wf_if_measure'[of _ _ _  ‹λS. DPLL_mesW ((atms_of_ms A)) (trail S)›])
   apply (rule wf_lexn)
   apply (rule wf_less_than)
  by (rule dpll_bj_trail_mes_decreasing_less_than; use fin in simp)


subsubsection ‹Normal Forms›

text ‹
  We prove that given a normal form of DPLL, with some structural invariants, then either @{term N}
  is satisfiable and the built valuation @{term M} is a model; or @{term N} is unsatisfiable.

  Idea of the proof: We have to prove tat @{term ‹satisfiable N›}, @{term ‹¬M⊨as N›}
  and there is no remaining step is incompatible.
  ▸ The @{term decide} rule tells us that every variable in @{term N} has a value.
  ▸ The assumption @{term ‹¬M⊨as N›} implies that there is conflict.
  ▸ There is at least one decision in the trail (otherwise, @{term M} would be a model of the set
    of clauses @{term N}).
  ▸ Now if we build the clause with all the decision literals of the trail, we can apply the
  @{term backjump} rule.

  The assumption are saying that we have a finite upper bound @{term A} for the literals, that we
  cannot do any step @{term ‹no_step dpll_bj S›}›
theorem dpll_backjump_final_state:
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    ‹no_dup (trail S)› and
    ‹finite A› and
    inv: ‹inv S› and
    n_d: ‹no_dup (trail S)› and
    n_s: ‹no_step dpll_bj S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT S))
    ∨ (trail S ⊨asm clausesNOT S ∧ satisfiable (set_mset (clausesNOT S)))›
proof -
  let ?N = ‹set_mset (clausesNOT S)›
  let ?M = ‹trail S›
  consider
      (sat) ‹satisfiable ?N› and ‹?M ⊨as ?N›
    | (sat') ‹satisfiable ?N› and ‹¬ ?M ⊨as ?N›
    | (unsat) ‹unsatisfiable ?N›
    by auto
  then show ?thesis
    proof cases
      case sat' note sat = this(1) and M = this(2)
      obtain C where ‹C ∈ ?N› and ‹¬?M ⊨a C› using M unfolding true_annots_def by auto
      obtain I :: ‹'v literal set› where
        ‹I ⊨s ?N› and
        cons: ‹consistent_interp I› and
        tot: ‹total_over_m I ?N› and
        atm_I_N: ‹atm_of `I ⊆ atms_of_ms ?N›
        using sat unfolding satisfiable_def_min by auto
      let ?I = ‹I ∪ {P| P. P ∈ lits_of_l ?M ∧ atm_of P ∉ atm_of ` I}›
      let ?O = ‹{unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
      have cons_I': ‹consistent_interp ?I›
        using cons using ‹no_dup ?M› unfolding consistent_interp_def
        by (auto simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set lits_of_def
          dest!: no_dup_cannot_not_lit_and_uminus)
      have tot_I': ‹total_over_m ?I (?N ∪ unmark_l ?M)›
        using tot atm_I_N unfolding total_over_m_def total_over_set_def
        by (fastforce simp: image_iff lits_of_def)
      have ‹{P |P. P ∈ lits_of_l ?M ∧ atm_of P ∉ atm_of ` I} ⊨s ?O›
        using ‹I⊨s ?N› atm_I_N by (auto simp add: atm_of_eq_atm_of true_clss_def lits_of_def)
      then have I'_N: ‹?I ⊨s ?N ∪ ?O›
        using ‹I⊨s ?N› true_clss_union_increase by force
      have tot': ‹total_over_m ?I (?N∪?O)›
        using atm_I_N tot unfolding total_over_m_def total_over_set_def
        by (force simp: lits_of_def elim!: is_decided_ex_Decided)

      have atms_N_M: ‹atms_of_ms ?N ⊆ atm_of ` lits_of_l ?M›
      proof (rule ccontr)
        assume ‹¬ ?thesis›
        then obtain l :: 'v where
          l_N: ‹l ∈ atms_of_ms ?N› and
          l_M: ‹l ∉ atm_of ` lits_of_l ?M›
          by auto
        have ‹undefined_lit ?M (Pos l)›
          using l_M by (metis Decided_Propagated_in_iff_in_lits_of_l
              atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1))
        then show False
          using l_N n_s can_propagate_or_decide_or_backjump[of ‹Pos l› S] inv n_d sat
          by (auto dest: dpll_bj.intros)
      qed
      have ‹?M ⊨as CNot C›
        apply (rule all_variables_defined_not_imply_cnot)
        using ‹C ∈ set_mset (clausesNOT S)› ‹¬ trail S ⊨a C›
           atms_N_M by (auto dest: atms_of_atms_of_ms_mono)
      have ‹∃l ∈ set ?M. is_decided l›
        proof (rule ccontr)
          let ?O = ‹{unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
          have θ[iff]: ‹⋀I. total_over_m I (?N ∪ ?O ∪ unmark_l ?M)
            ⟷ total_over_m I (?N ∪unmark_l ?M)›
            unfolding total_over_set_def total_over_m_def atms_of_ms_def by blast
          assume ‹¬ ?thesis›
          then have [simp]:‹{unmark L |L. is_decided L ∧ L ∈ set ?M}
            = {unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
            by auto
          then have ‹?N ∪ ?O ⊨ps unmark_l ?M›
            using all_decomposition_implies_propagated_lits_are_implied[OF decomp] by auto

          then have ‹?I ⊨s unmark_l ?M›
            using cons_I' I'_N tot_I' ‹?I ⊨s ?N ∪ ?O› unfolding θ true_clss_clss_def by blast
          then have ‹lits_of_l ?M ⊆ ?I›
            unfolding true_clss_def lits_of_def by auto
          then have ‹?M ⊨as ?N›
            using I'_N ‹C ∈ ?N› ‹¬ ?M ⊨a C› cons_I' atms_N_M
            by (meson ‹trail S ⊨as CNot C› consistent_CNot_not rev_subsetD sup_ge1 true_annot_def
              true_annots_def true_cls_mono_set_mset_l true_clss_def)
          then show False using M by fast
        qed
      from List.split_list_first_propE[OF this] obtain K :: ‹'v literal› and
        F F' :: ‹('v, unit) ann_lits› where
        M_K: ‹?M = F' @ Decided K # F› and
        nm: ‹∀f∈set F'. ¬is_decided f›
        by (metis (full_types) is_decided_ex_Decided old.unit.exhaust)
      let ?K = ‹Decided K :: ('v, unit) ann_lit›
      have ‹?K ∈ set ?M›
        unfolding M_K by auto
      let ?C = ‹image_mset lit_of {#L∈#mset ?M. is_decided L ∧ L≠?K#} :: 'v clause›
      let ?C' = ‹set_mset (image_mset (λL::'v literal. {#L#}) (?C + unmark ?K))›
      have ‹?N ∪ {unmark L |L. is_decided L ∧ L ∈ set ?M} ⊨ps unmark_l ?M›
        using all_decomposition_implies_propagated_lits_are_implied[OF decomp] .
      moreover have C': ‹?C' = {unmark L |L. is_decided L ∧ L ∈ set ?M}›
        unfolding M_K by standard force+
      ultimately have N_C_M: ‹?N ∪ ?C' ⊨ps unmark_l ?M›
        by auto
      have N_M_False: ‹?N ∪ (λL. unmark L) ` (set ?M) ⊨ps {{#}}›
        unfolding true_clss_clss_def true_annots_def Ball_def true_annot_def
      proof (intro allI impI)
        fix LL :: "'v literal set"
        assume
          tot: ‹total_over_m LL (set_mset (clausesNOT S) ∪ unmark_l (trail S) ∪ {{#}})› and
          cons: ‹consistent_interp LL› and
          LL: ‹LL ⊨s set_mset (clausesNOT S) ∪ unmark_l (trail S)›
        have ‹total_over_m LL (CNot C)›
          by (metis ‹C ∈# clausesNOT S› insert_absorb tot total_over_m_CNot_toal_over_m
              total_over_m_insert total_over_m_union)
        then have "total_over_m LL (unmark_l (trail S) ∪ CNot C)"
            using tot by force
          then show "LL ⊨s {{#}}"
            using tot cons LL
            by (metis (no_types) ‹C ∈# clausesNOT S› ‹trail S ⊨as CNot C› consistent_CNot_not
                true_annots_true_clss_clss true_clss_clss_def true_clss_def true_clss_union)
      qed
      have ‹undefined_lit F K› using ‹no_dup ?M› unfolding M_K by (auto simp: defined_lit_map)
      moreover {
        have ‹?N ∪ ?C' ⊨ps {{#}}›
          proof -
            have A: ‹?N ∪ ?C' ∪ unmark_l ?M = ?N ∪ unmark_l ?M›
              unfolding M_K by auto
            show ?thesis
              using true_clss_clss_left_right[OF N_C_M, of ‹{{#}}›] N_M_False unfolding A by auto
          qed
        have ‹?N ⊨p image_mset uminus ?C + {#-K#}›
          unfolding true_clss_cls_def true_clss_clss_def total_over_m_def
          proof (intro allI impI)
            fix I
            assume
              tot: ‹total_over_set I (atms_of_ms (?N ∪ {image_mset uminus ?C+ {#- K#}}))› and
              cons: ‹consistent_interp I› and
              ‹I ⊨s ?N›
            have ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
              using cons tot unfolding consistent_interp_def by (cases K) auto
            have ‹ {a ∈ set (trail S). is_decided a ∧ a ≠ Decided K} =
              set (trail S) ∩ {L. is_decided L ∧ L ≠ Decided K}›
             by auto
            then have tot': ‹total_over_set I
               (atm_of ` lit_of ` (set ?M ∩ {L. is_decided L ∧ L ≠ Decided K}))›
              using tot by (auto simp add: atms_of_uminus_lit_atm_of_lit_of)
            { fix x :: ‹('v, unit) ann_lit›
              assume
                a3: ‹lit_of x ∉ I› and
                a1: ‹x ∈ set ?M› and
                a4: ‹is_decided x› and
                a5: ‹x ≠ Decided K›
              then have ‹Pos (atm_of (lit_of x)) ∈ I ∨ Neg (atm_of (lit_of x)) ∈ I›
                using a5 a4 tot' a1 unfolding total_over_set_def atms_of_s_def by blast
              moreover have f6: ‹Neg (atm_of (lit_of x)) = - Pos (atm_of (lit_of x))›
                by simp
              ultimately have ‹- lit_of x ∈ I›
                using f6 a3 by (metis (no_types) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
                  literal.sel(1))
            } note H = this

            have ‹¬I ⊨s ?C'›
              using ‹?N ∪ ?C' ⊨ps {{#}}› tot cons ‹I ⊨s ?N›
              unfolding true_clss_clss_def total_over_m_def
              by (simp add: atms_of_uminus_lit_atm_of_lit_of atms_of_ms_single_image_atm_of_lit_of)
            then show ‹I ⊨ image_mset uminus ?C + {#- K#}›
              unfolding true_clss_def true_cls_def using ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
              by (auto dest!: H)
          qed }
      moreover have ‹F ⊨as CNot (image_mset uminus ?C)›
        using nm unfolding true_annots_def CNot_def M_K by (auto simp add: lits_of_def)
      ultimately have False
        using bj_can_jump[of S F' K F C ‹-K›
          ‹image_mset uminus (image_mset lit_of {# L :# mset ?M. is_decided L ∧ L ≠ Decided K#})›]
          ‹C∈?N› n_s ‹?M ⊨as CNot C› bj_backjump inv ‹no_dup (trail S)› sat
          unfolding M_K by auto
        then show ?thesis by fast
    qed auto
qed

end ― ‹End of the locale @{locale dpll_with_backjumping_ops}.›

locale dpll_with_backjumping =
  dpll_with_backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT inv
    decide_conds backjump_conds propagate_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool›
  +
  assumes dpll_bj_inv: ‹⋀S T. dpll_bj S T ⟹ inv S ⟹ inv T›
begin

lemma rtranclp_dpll_bj_inv:
  assumes ‹dpll_bj** S T› and ‹inv S›
  shows ‹inv T›
  using assms by (induction rule: rtranclp_induct)
    (auto simp add: dpll_bj_no_dup intro: dpll_bj_inv)

lemma rtranclp_dpll_bj_no_dup:
  assumes ‹dpll_bj** S T› and ‹inv S›
  and ‹no_dup (trail S)›
  shows ‹no_dup (trail T)›
  using assms by (induction rule: rtranclp_induct)
  (auto simp add: dpll_bj_no_dup dest: rtranclp_dpll_bj_inv dpll_bj_inv)

lemma rtranclp_dpll_bj_atms_of_ms_clauses_inv:
  assumes
    ‹dpll_bj** S T› and ‹inv S›
  shows ‹atms_of_mm (clausesNOT S) = atms_of_mm (clausesNOT T)›
  using assms by (induction rule: rtranclp_induct)
    (auto dest: rtranclp_dpll_bj_inv dpll_bj_atms_of_ms_clauses_inv)

lemma rtranclp_dpll_bj_atms_in_trail:
  assumes
    ‹dpll_bj** S T› and
    ‹inv S› and
    ‹atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (clausesNOT S)›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ atms_of_mm (clausesNOT T)›
  using assms apply (induction rule: rtranclp_induct)
  using dpll_bj_atms_in_trail dpll_bj_atms_of_ms_clauses_inv rtranclp_dpll_bj_inv by auto

lemma rtranclp_dpll_bj_sat_iff:
  assumes ‹dpll_bj** S T› and ‹inv S›
  shows ‹I ⊨sm clausesNOT S ⟷ I ⊨sm clausesNOT T›
  using assms by (induction rule: rtranclp_induct)
    (auto dest!: dpll_bj_sat_iff simp: rtranclp_dpll_bj_inv)

lemma rtranclp_dpll_bj_atms_in_trail_in_set:
  assumes
    ‹dpll_bj** S T› and
    ‹inv S›
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of ` (lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A›
  using assms by (induction rule: rtranclp_induct)
  (auto dest: rtranclp_dpll_bj_inv
    simp: dpll_bj_atms_in_trail_in_set rtranclp_dpll_bj_atms_of_ms_clauses_inv rtranclp_dpll_bj_inv)

lemma rtranclp_dpll_bj_all_decomposition_implies_inv:
  assumes
    ‹dpll_bj** S T› and
    ‹inv S›
    ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
  using assms by (induction rule: rtranclp_induct)
    (auto intro: dpll_bj_all_decomposition_implies_inv simp: rtranclp_dpll_bj_inv)

lemma rtranclp_dpll_bj_inv_incl_dpll_bj_inv_trancl:
  ‹{(T, S). dpll_bj++ S T
    ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S) ∧ inv S}
     ⊆ {(T, S). dpll_bj S T ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A
        ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧ no_dup (trail S) ∧ inv S}+›
    (is ‹?A ⊆ ?B+›)
proof standard
  fix x
  assume x_A: ‹x ∈ ?A›
  obtain S T::‹'st› where
    x[simp]: ‹x = (T, S)› by (cases x) auto
  have
    ‹dpll_bj++ S T› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    ‹no_dup (trail S)› and
     ‹inv S›
    using x_A by auto
  then show ‹x ∈ ?B+› unfolding x
    proof (induction rule: tranclp_induct)
      case base
      then show ?case by auto
    next
      case (step T U) note step = this(1) and ST = this(2) and IH = this(3)[OF this(4-7)]
        and N_A = this(4) and M_A = this(5) and nd = this(6) and inv = this(7)

      have [simp]: ‹atms_of_mm (clausesNOT S) = atms_of_mm (clausesNOT T)›
        using step rtranclp_dpll_bj_atms_of_ms_clauses_inv tranclp_into_rtranclp inv by fastforce
      have ‹no_dup (trail T)›
        using local.step nd rtranclp_dpll_bj_no_dup tranclp_into_rtranclp inv by fastforce
      moreover have ‹atm_of ` (lits_of_l (trail T)) ⊆ atms_of_ms A›
        by (metis inv M_A N_A local.step rtranclp_dpll_bj_atms_in_trail_in_set
          tranclp_into_rtranclp)
      moreover have ‹inv T›
         using inv local.step rtranclp_dpll_bj_inv tranclp_into_rtranclp by fastforce
      ultimately have ‹(U, T) ∈ ?B› using ST N_A M_A inv by auto
      then show ?case using IH by (rule trancl_into_trancl2)
    qed
qed

lemma wf_tranclp_dpll_bj:
  assumes fin: ‹finite A›
  shows ‹wf {(T, S). dpll_bj++ S T
    ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S) ∧ inv S}›
  using wf_trancl[OF wf_dpll_bj[OF fin]] rtranclp_dpll_bj_inv_incl_dpll_bj_inv_trancl
  by (rule wf_subset)

lemma dpll_bj_sat_ext_iff:
  ‹dpll_bj S T ⟹ inv S ⟹ I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  by (simp add: dpll_bj_clauses)

lemma rtranclp_dpll_bj_sat_ext_iff:
  ‹dpll_bj** S T ⟹ inv S ⟹ I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  by (induction rule: rtranclp_induct) (simp_all add: rtranclp_dpll_bj_inv dpll_bj_sat_ext_iff)

theorem full_dpll_backjump_final_state:
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    full: ‹full dpll_bj S T› and
    atms_S: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    ‹finite A› and
    inv: ‹inv S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT S))
  ∨ (trail T ⊨asm clausesNOT S ∧ satisfiable (set_mset (clausesNOT S)))›
proof -
  have st: ‹dpll_bj** S T› and ‹no_step dpll_bj T›
    using full unfolding full_def by fast+
  moreover have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    using atms_S inv rtranclp_dpll_bj_atms_of_ms_clauses_inv st by blast
  moreover have ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
     using atms_S atms_trail inv rtranclp_dpll_bj_atms_in_trail_in_set st by auto
  moreover have ‹no_dup (trail T)›
    using n_d inv rtranclp_dpll_bj_no_dup st by blast
  moreover have inv: ‹inv T›
    using inv rtranclp_dpll_bj_inv st by blast
  moreover
    have decomp: ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
      using ‹inv S› decomp rtranclp_dpll_bj_all_decomposition_implies_inv st by blast
  ultimately have ‹unsatisfiable (set_mset (clausesNOT T))
    ∨ (trail T ⊨asm clausesNOT T ∧ satisfiable (set_mset (clausesNOT T)))›
    using ‹finite A› dpll_backjump_final_state by force
  then show ?thesis
    by (meson ‹inv S› rtranclp_dpll_bj_sat_iff satisfiable_carac st true_annots_true_cls)
qed

corollary full_dpll_backjump_final_state_from_init_state: (* \htmllink{full_dpll_backjump_final_state_from_init_state}*)
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    full: ‹full dpll_bj S T› and
    ‹trail S = []› and
    ‹clausesNOT S = N› and
    ‹inv S›
  shows ‹unsatisfiable (set_mset N) ∨ (trail T ⊨asm N ∧ satisfiable (set_mset N))›
  using assms full_dpll_backjump_final_state[of S T ‹set_mset N›] by auto

lemma tranclp_dpll_bj_trail_mes_decreasing_prop:
  assumes dpll: ‹dpll_bj++ S T› and inv: ‹inv S› and
  N_A: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
  M_A: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
  n_d: ‹no_dup (trail S)› and
  fin_A: ‹finite A›
  shows ‹(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
               - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
            < (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
               - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)›
  using dpll
proof induction
  case base
  then show ?case
    using N_A M_A n_d dpll_bj_trail_mes_decreasing_prop fin_A inv by blast
next
  case (step T U) note st = this(1) and dpll = this(2) and IH = this(3)
  have ‹atms_of_mm (clausesNOT S) = atms_of_mm (clausesNOT T)›
    using rtranclp_dpll_bj_atms_of_ms_clauses_inv by (metis dpll_bj_clauses dpll_bj_inv inv st
      tranclpD)
  then have N_A': ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
     using N_A by auto
  moreover have M_A': ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
    by (meson M_A N_A inv rtranclp_dpll_bj_atms_in_trail_in_set st dpll
      tranclp.r_into_trancl tranclp_into_rtranclp tranclp_trans)
  moreover have nd: ‹no_dup (trail T)›
    by (metis inv n_d rtranclp_dpll_bj_no_dup st tranclp_into_rtranclp)
  moreover have ‹inv T›
    by (meson dpll dpll_bj_inv inv rtranclp_dpll_bj_inv st tranclp_into_rtranclp)
  ultimately show ?case
    using IH dpll_bj_trail_mes_decreasing_prop[of T U A] dpll fin_A by linarith
qed

end ― ‹End of the locale @{locale dpll_with_backjumping}.›


subsection ‹CDCL›

text ‹In this section we will now define the conflict driven clause learning above DPLL: we first
  introduce the rules learn and forget, and the add these rules to the DPLL calculus.›

subsubsection ‹Learn and Forget›

text ‹Learning adds a new clause where all the literals are already included in the clauses.›
locale learn_ops =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  fixes
    learn_conds :: ‹'v clause ⇒ 'st ⇒ bool›
begin

inductive learn :: ‹'st ⇒ 'st ⇒ bool› where
learnNOT_rule: ‹clausesNOT S ⊨pm C ⟹
  atms_of C ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S)) ⟹
  learn_conds C S ⟹
  T ∼ add_clsNOT C S ⟹
  learn S T›
inductive_cases learnNOTE: ‹learn S T›

lemma learn_μC_stable:
  assumes ‹learn S T› and ‹no_dup (trail S)›
  shows ‹μC A B (trail_weight S) = μC A B (trail_weight T)›
  using assms by (auto elim: learnNOTE)
end

text ‹Forget removes an information that can be deduced from the context (e.g.\ redundant clauses,
  tautologies)›
locale forget_ops =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› +
  fixes
    forget_conds :: ‹'v clause ⇒ 'st ⇒ bool›
begin

inductive forgetNOT :: ‹'st ⇒ 'st ⇒ bool› where
forgetNOT:
  ‹removeAll_mset C(clausesNOT S) ⊨pm C ⟹
  forget_conds C S ⟹
  C ∈# clausesNOT S ⟹
  T ∼ remove_clsNOT C S ⟹

  forgetNOT S T›
inductive_cases forgetNOTE: ‹forgetNOT S T›

lemma forget_μC_stable:
  assumes ‹forgetNOT S T›
  shows ‹μC A B (trail_weight S) = μC A B (trail_weight T)›
  using assms by (auto elim!: forgetNOTE)
end

locale learn_and_forgetNOT =
  learn_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT learn_conds +
  forget_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT forget_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    learn_conds forget_conds :: ‹'v clause ⇒ 'st ⇒ bool›
begin
inductive learn_and_forgetNOT :: ‹'st ⇒ 'st ⇒ bool›
where
lf_learn: ‹learn S T ⟹ learn_and_forgetNOT S T› |
lf_forget: ‹forgetNOT S T ⟹ learn_and_forgetNOT S T›
end


subsubsection ‹Definition of CDCL›

locale conflict_driven_clause_learning_ops =
  dpll_with_backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    inv decide_conds backjump_conds propagate_conds +
  learn_and_forgetNOT trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT learn_conds
    forget_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    learn_conds forget_conds :: ‹'v clause ⇒ 'st ⇒ bool›
begin

inductive cdclNOT :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
c_dpll_bj: ‹dpll_bj S S' ⟹ cdclNOT S S'› |
c_learn: ‹learn S S' ⟹ cdclNOT S S'› |
c_forgetNOT: ‹forgetNOT S S' ⟹ cdclNOT S S'›

lemma cdclNOT_all_induct[consumes 1, case_names dpll_bj learn forgetNOT]:
  fixes S T :: ‹'st›
  assumes ‹cdclNOT S T› and
    dpll: ‹⋀T. dpll_bj S T ⟹ P S T› and
    learning:
      ‹⋀C T. clausesNOT S ⊨pm C ⟹
      atms_of C ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S)) ⟹
      T ∼ add_clsNOT C S ⟹
      P S T› and
    forgetting: ‹⋀C T. removeAll_mset C (clausesNOT S) ⊨pm C ⟹
      C ∈# clausesNOT S ⟹
      T ∼ remove_clsNOT C S ⟹
      P S T›
  shows ‹P S T›
  using assms(1) by (induction rule: cdclNOT.induct)
  (auto intro: assms(2, 3, 4) elim!: learnNOTE forgetNOTE)+

lemma cdclNOT_no_dup:
  assumes
    ‹cdclNOT S T› and
    ‹inv S› and
    ‹no_dup (trail S)›
  shows ‹no_dup (trail T)›
  using assms by (induction rule: cdclNOT_all_induct) (auto intro: dpll_bj_no_dup)

paragraph ‹Consistency of the trail›
lemma cdclNOT_consistent:
  assumes
    ‹cdclNOT S T› and
    ‹inv S› and
    ‹no_dup (trail S)›
  shows ‹consistent_interp (lits_of_l (trail T))›
  using cdclNOT_no_dup[OF assms] distinct_consistent_interp by fast

text ‹The subtle problem here is that tautologies can be removed, meaning that some variable can
  disappear of the problem. It is also means that some variable of the trail might not be present
  in the clauses anymore.›
lemma cdclNOT_atms_of_ms_clauses_decreasing:
  assumes ‹cdclNOT S T›and ‹inv S›
  shows ‹atms_of_mm (clausesNOT T) ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›
  using assms by (induction rule: cdclNOT_all_induct)
    (auto dest!: dpll_bj_atms_of_ms_clauses_inv set_mp simp add: atms_of_ms_def Union_eq)

lemma cdclNOT_atms_in_trail:
  assumes ‹cdclNOT S T›and ‹inv S›
  and ‹atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (clausesNOT S)›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ atms_of_mm (clausesNOT S)›
  using assms by (induction rule: cdclNOT_all_induct) (auto simp add: dpll_bj_atms_in_trail)

lemma cdclNOT_atms_in_trail_in_set:
  assumes
    ‹cdclNOT S T› and ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of ` (lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A›
  using assms
  by (induction rule: cdclNOT_all_induct)
     (simp_all add: dpll_bj_atms_in_trail_in_set dpll_bj_atms_of_ms_clauses_inv)

lemma cdclNOT_all_decomposition_implies:
  assumes ‹cdclNOT S T› and ‹inv S› and
    ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows
    ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
  using assms(1,2,3)
proof (induction rule: cdclNOT_all_induct)
  case dpll_bj
  then show ?case
     using dpll_bj_all_decomposition_implies_inv by blast
next
  case learn
  then show ?case by (auto simp add: all_decomposition_implies_def)
next
  case (forgetNOT C T) note cls_C = this(1) and C = this(2) and T = this(3) and inv = this(4) and
    decomp = this(5)
  show ?case
    unfolding all_decomposition_implies_def Ball_def
    proof (intro allI, clarify)
      fix a b
      assume ‹(a, b) ∈ set (get_all_ann_decomposition (trail T))›
      then have ‹unmark_l a ∪ set_mset (clausesNOT S) ⊨ps unmark_l b›
        using decomp T by (auto simp add: all_decomposition_implies_def)
      moreover
        have a1:‹C ∈ set_mset (clausesNOT S)›
          using C by blast
        have ‹clausesNOT T = clausesNOT (remove_clsNOT C S)›
         using T state_eqNOT_clauses by blast
        then have ‹set_mset (clausesNOT T) ⊨ps set_mset (clausesNOT S)›
          using a1 by (metis (no_types) clauses_remove_clsNOT cls_C insert_Diff order_refl
          set_mset_minus_replicate_mset(1) true_clss_clss_def true_clss_clss_insert)
      ultimately show ‹unmark_l a ∪ set_mset (clausesNOT T)
        ⊨ps unmark_l b›
        using true_clss_clss_generalise_true_clss_clss by blast
    qed
qed

paragraph ‹Extension of models›
lemma cdclNOT_bj_sat_ext_iff:
  assumes ‹cdclNOT S T›and ‹inv S›
  shows ‹I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  using assms
proof (induction rule:cdclNOT_all_induct)
  case dpll_bj
  then show ?case by (simp add: dpll_bj_clauses)
next
  case (learn C T) note T = this(3)
  { fix J
    assume
      ‹I ⊨sextm clausesNOT S› and
      ‹I ⊆ J› and
      tot: ‹total_over_m J (set_mset (add_mset C (clausesNOT S)))› and
      cons: ‹consistent_interp J›
    then have ‹J ⊨sm clausesNOT S› unfolding true_clss_ext_def by auto

    moreover
      with ‹clausesNOT S⊨pm C› have ‹J ⊨ C›
        using tot cons unfolding true_clss_cls_def by auto
    ultimately have ‹J ⊨sm {#C#} + clausesNOT S› by auto
  }
  then have H: ‹I ⊨sextm (clausesNOT S) ⟹ I ⊨sext insert C (set_mset (clausesNOT S))›
    unfolding true_clss_ext_def by auto
  show ?case
    apply standard
      using T apply (auto simp add: H)[]
    using T apply simp
    by (metis Diff_insert_absorb insert_subset subsetI subset_antisym
      true_clss_ext_decrease_right_remove_r)
next
  case (forgetNOT C T) note cls_C = this(1) and T = this(3)
  { fix J
    assume
      ‹I ⊨sext set_mset (clausesNOT S) - {C}› and
      ‹I ⊆ J› and
      tot: ‹total_over_m J (set_mset (clausesNOT S))› and
      cons: ‹consistent_interp J›
    then have ‹J ⊨s set_mset (clausesNOT S) - {C}›
      unfolding true_clss_ext_def by (meson Diff_subset total_over_m_subset)

    moreover
      with cls_C have ‹J ⊨ C›
        using tot cons unfolding true_clss_cls_def
        by (metis Un_commute forgetNOT.hyps(2) insert_Diff insert_is_Un order_refl
          set_mset_minus_replicate_mset(1))
    ultimately have ‹J ⊨sm (clausesNOT S)› by (metis insert_Diff_single true_clss_insert)
  }
  then have H: ‹I ⊨sext set_mset (clausesNOT S) - {C} ⟹ I ⊨sextm (clausesNOT S)›
    unfolding true_clss_ext_def by blast
  show ?case using T by (auto simp: true_clss_ext_decrease_right_remove_r H)
qed

end ― ‹End of the locale @{locale conflict_driven_clause_learning_ops}.›

subsubsection ‹CDCL with invariant›
locale conflict_driven_clause_learning =
  conflict_driven_clause_learning_ops +
  assumes cdclNOT_inv: ‹⋀S T. cdclNOT S T ⟹ inv S ⟹ inv T›
begin
sublocale dpll_with_backjumping
  apply unfold_locales
  using cdclNOT.simps cdclNOT_inv by auto

lemma rtranclp_cdclNOT_inv:
  ‹cdclNOT** S T ⟹ inv S ⟹ inv T›
  by (induction rule: rtranclp_induct) (auto simp add: cdclNOT_inv)

lemma rtranclp_cdclNOT_no_dup:
  assumes ‹cdclNOT** S T› and ‹inv S›
  and ‹no_dup (trail S)›
  shows ‹no_dup (trail T)›
  using assms by (induction rule: rtranclp_induct) (auto intro: cdclNOT_no_dup rtranclp_cdclNOT_inv)

lemma rtranclp_cdclNOT_trail_clauses_bound:
  assumes
    cdcl: ‹cdclNOT** S T› and
    inv: ‹inv S› and
    atms_clauses_S: ‹atms_of_mm (clausesNOT S) ⊆ A› and
    atms_trail_S: ‹atm_of `(lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A ∧ atms_of_mm (clausesNOT T) ⊆ A›
  using cdcl
proof (induction rule: rtranclp_induct)
  case base
  then show ?case using atms_clauses_S atms_trail_S by simp
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)
  have ‹inv T› using inv st rtranclp_cdclNOT_inv by blast
   have ‹atms_of_mm (clausesNOT U) ⊆ A›
    using cdclNOT_atms_of_ms_clauses_decreasing[OF cdclNOT] IH ‹inv T› by fast
  moreover
    have ‹atm_of `(lits_of_l (trail U)) ⊆ A›
      using cdclNOT_atms_in_trail_in_set[OF cdclNOT, of A]
      by (meson atms_trail_S atms_clauses_S IH ‹inv T› cdclNOT )
  ultimately show ?case by fast
qed

lemma rtranclp_cdclNOT_all_decomposition_implies:
  assumes ‹cdclNOT** S T› and ‹inv S› and ‹no_dup (trail S)› and
    ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows
    ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
  using assms by (induction)
  (auto intro: rtranclp_cdclNOT_inv cdclNOT_all_decomposition_implies rtranclp_cdclNOT_no_dup)

lemma rtranclp_cdclNOT_bj_sat_ext_iff:
  assumes ‹cdclNOT** S T›and ‹inv S›
  shows ‹I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  using assms apply (induction rule: rtranclp_induct)
  using cdclNOT_bj_sat_ext_iff by (auto intro: rtranclp_cdclNOT_inv rtranclp_cdclNOT_no_dup)

definition cdclNOT_NOT_all_inv where
‹cdclNOT_NOT_all_inv A S ⟷ (finite A ∧ inv S ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A
    ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧ no_dup (trail S))›

lemma cdclNOT_NOT_all_inv:
  assumes ‹cdclNOT** S T› and ‹cdclNOT_NOT_all_inv A S›
  shows ‹cdclNOT_NOT_all_inv A T›
  using assms unfolding cdclNOT_NOT_all_inv_def
  by (simp add: rtranclp_cdclNOT_inv rtranclp_cdclNOT_no_dup rtranclp_cdclNOT_trail_clauses_bound)

(* is the same as learn_and_forgetNOT *)
abbreviation learn_or_forget where
‹learn_or_forget S T ≡ learn S T ∨ forgetNOT S T›

lemma rtranclp_learn_or_forget_cdclNOT:
  ‹learn_or_forget** S T ⟹ cdclNOT** S T›
  using rtranclp_mono[of learn_or_forget cdclNOT] by (blast intro: cdclNOT.c_learn cdclNOT.c_forgetNOT)

lemma learn_or_forget_dpll_μC:
  assumes
    l_f: ‹learn_or_forget** S T› and
    dpll: ‹dpll_bj T U› and
    inv: ‹cdclNOT_NOT_all_inv A S›
  shows ‹(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
      - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight U)
    < (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
      - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)›
     (is ‹?μ U < ?μ S›)
proof -
  have ‹?μ S = ?μ T›
    using l_f
    proof (induction)
      case base
      then show ?case by simp
    next
      case (step T U)
      moreover then have ‹no_dup (trail T)›
        using rtranclp_cdclNOT_no_dup[of S T] cdclNOT_NOT_all_inv_def inv
        rtranclp_learn_or_forget_cdclNOT by auto
      ultimately show ?case
        using forget_μC_stable learn_μC_stable inv unfolding cdclNOT_NOT_all_inv_def by presburger
    qed
  moreover have ‹cdclNOT_NOT_all_inv A T›
     using rtranclp_learn_or_forget_cdclNOT cdclNOT_NOT_all_inv l_f inv by blast
  ultimately show ?thesis
    using dpll_bj_trail_mes_decreasing_prop[of T U A, OF dpll] finite
    unfolding cdclNOT_NOT_all_inv_def by presburger
qed

lemma infinite_cdclNOT_exists_learn_and_forget_infinite_chain: (* \htmlink{infinite_cdcl_NOT_exists_learn_and_forget_infinite_chain} *)
  assumes
    ‹⋀i. cdclNOT (f i) (f(Suc i))› and
    inv: ‹cdclNOT_NOT_all_inv A (f 0)›
  shows ‹∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))›
  using assms
proof (induction ‹(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
    - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight (f 0))›
    arbitrary: f
    rule: nat_less_induct_case)
  case (Suc n) note IH = this(1) and μ = this(2) and cdclNOT = this(3) and inv = this(4)
  consider
    (dpll_end) ‹∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))›
    | (dpll_more) ‹¬(∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i)))›
    by blast
  then show ?case
  proof cases
    case dpll_end
    then show ?thesis by auto
  next
    case dpll_more
    then have j: ‹∃i. ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))›
      by blast
    obtain i where
      i_learn_forget: ‹¬learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))› and
      ‹∀k<i. learn_or_forget (f k) (f (Suc k))›
    proof -
      obtain i0 where ‹¬ learn (f i0) (f (Suc i0)) ∧ ¬forgetNOT (f i0) (f (Suc i0))›
        using j by auto
      then have ‹{i. i≤i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))} ≠ {}›
        by auto
      let ?I = ‹{i. i≤i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))}›
      let ?i = ‹Min ?I›
      have ‹finite ?I›
        by auto
      have ‹¬ learn (f ?i) (f (Suc ?i)) ∧ ¬forgetNOT (f ?i) (f (Suc ?i))›
        using Min_in[OF ‹finite ?I› ‹?I ≠ {}›] by auto
      moreover have ‹∀k<?i. learn_or_forget (f k) (f (Suc k))›
        using Min.coboundedI[of ‹{i. i ≤ i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬ forgetNOT (f i)
            (f (Suc i))}›, simplified]
        by (meson ‹¬ learn (f i0) (f (Suc i0)) ∧ ¬ forgetNOT (f i0) (f (Suc i0))› less_imp_le
            dual_order.trans not_le)
      ultimately show ?thesis using that by blast
    qed
    define g where ‹g = (λn. f (n + Suc i))›
    have ‹dpll_bj (f i) (g 0)›
      using i_learn_forget cdclNOT cdclNOT.cases unfolding g_def by auto
    {
      fix j
      assume ‹j ≤ i›
      then have ‹learn_or_forget** (f 0) (f j)›
        apply (induction j)
         apply simp
        by (metis (no_types, lifting) Suc_leD Suc_le_lessD rtranclp.simps
            ‹∀k<i. learn (f k) (f (Suc k)) ∨ forgetNOT (f k) (f (Suc k))›)
    }
    then have ‹learn_or_forget** (f 0) (f i)› by blast
    then have ‹(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
      - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight (g 0))
      < (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
      - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight (f 0))›
      using learn_or_forget_dpll_μC[of ‹f 0› ‹f i› ‹g 0› A] inv ‹dpll_bj (f i) (g 0)›
      unfolding cdclNOT_NOT_all_inv_def by linarith

    moreover have cdclNOT_i: ‹cdclNOT** (f 0) (g 0)›
      using rtranclp_learn_or_forget_cdclNOT[of ‹f 0› ‹f i›] ‹learn_or_forget** (f 0) (f i)›
        cdclNOT[of i] unfolding g_def by auto
    moreover have ‹⋀i. cdclNOT (g i) (g (Suc i))›
      using cdclNOT g_def by auto
    moreover have ‹cdclNOT_NOT_all_inv A (g 0)›
      using inv cdclNOT_i rtranclp_cdclNOT_trail_clauses_bound g_def cdclNOT_NOT_all_inv by auto
    ultimately obtain j where j: ‹⋀i. i≥j ⟹ learn_or_forget (g i) (g (Suc i))›
      using IH unfolding μ[symmetric] by presburger
    show ?thesis
    proof
      {
        fix k
        assume ‹k ≥ j + Suc i›
        then have ‹learn_or_forget (f k) (f (Suc k))›
          using j[of ‹k-Suc i›] unfolding g_def by auto
      }
      then show ‹∀k≥j+Suc i. learn_or_forget (f k) (f (Suc k))›
        by auto
    qed
  qed
next
  case 0 note H = this(1) and cdclNOT = this(2) and inv = this(3)
  show ?case
  proof (rule ccontr)
    assume ‹¬ ?case›
    then have j: ‹∃i. ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))›
      by blast
    obtain i where
      ‹¬learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))› and
      ‹∀k<i. learn_or_forget (f k) (f (Suc k))›
    proof -
      obtain i0 where ‹¬ learn (f i0) (f (Suc i0)) ∧ ¬forgetNOT (f i0) (f (Suc i0))›
        using j by auto
      then have ‹{i. i≤i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))} ≠ {}›
        by auto
      let ?I = ‹{i. i≤i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forgetNOT (f i) (f (Suc i))}›
      let ?i = ‹Min ?I›
      have ‹finite ?I›
        by auto
      have ‹¬ learn (f ?i) (f (Suc ?i)) ∧ ¬forgetNOT (f ?i) (f (Suc ?i))›
        using Min_in[OF ‹finite ?I› ‹?I ≠ {}›] by auto
      moreover have ‹∀k<?i. learn_or_forget (f k) (f (Suc k))›
        using Min.coboundedI[of ‹{i. i ≤ i0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬ forgetNOT (f i)
            (f (Suc i))}›, simplified]
        by (meson ‹¬ learn (f i0) (f (Suc i0)) ∧ ¬ forgetNOT (f i0) (f (Suc i0))› less_imp_le
            dual_order.trans not_le)
      ultimately show ?thesis using that by blast
    qed
    have ‹dpll_bj (f i) (f (Suc i))›
      using ‹¬ learn (f i) (f (Suc i)) ∧ ¬ forgetNOT (f i) (f (Suc i))› cdclNOT cdclNOT.cases
      by blast
    {
      fix j
      assume ‹j ≤ i›
      then have ‹learn_or_forget** (f 0) (f j)›
        apply (induction j)
         apply simp
        by (metis (no_types, lifting) Suc_leD Suc_le_lessD rtranclp.simps
            ‹∀k<i. learn (f k) (f (Suc k)) ∨ forgetNOT (f k) (f (Suc k))›)
    }
    then have ‹learn_or_forget** (f 0) (f i)› by blast

    then show False
      using learn_or_forget_dpll_μC[of ‹f 0› ‹f i› ‹f (Suc i)› A] inv 0
        ‹dpll_bj (f i) (f (Suc i))› unfolding cdclNOT_NOT_all_inv_def by linarith
  qed
qed

lemma wf_cdclNOT_no_learn_and_forget_infinite_chain:
  assumes
    no_infinite_lf: ‹⋀f j. ¬ (∀i≥j. learn_or_forget (f i) (f (Suc i)))›
  shows ‹wf {(T, S). cdclNOT S T ∧ cdclNOT_NOT_all_inv A S}›
    (is ‹wf {(T, S). cdclNOT S T ∧ ?inv S}›)
  unfolding wf_iff_no_infinite_down_chain
proof (rule ccontr)
  assume ‹¬ ¬ (∃f. ∀i. (f (Suc i), f i) ∈ {(T, S). cdclNOT S T ∧ ?inv S})›
  then obtain f where
    ‹∀i. cdclNOT (f i) (f (Suc i)) ∧ ?inv (f i)›
    by fast
  then have ‹∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))›
    using infinite_cdclNOT_exists_learn_and_forget_infinite_chain[of f] by meson
  then show False using no_infinite_lf by blast
qed

lemma inv_and_tranclp_cdcl_NOT_tranclp_cdclNOT_and_inv:
  ‹cdclNOT++ S T ∧ cdclNOT_NOT_all_inv A S ⟷ (λS T. cdclNOT S T ∧ cdclNOT_NOT_all_inv A S)++ S T›
  (is ‹?A ∧ ?I ⟷ ?B›)
proof
  assume ‹?A ∧ ?I›
  then have ?A and ?I by blast+
  then show ?B
    apply induction
      apply (simp add: tranclp.r_into_trancl)
    by (subst tranclp.simps) (auto intro: cdclNOT_NOT_all_inv tranclp_into_rtranclp)
next
  assume ?B
  then have ?A by induction auto
  moreover have ?I using ‹?B› tranclpD by fastforce
  ultimately show ‹?A ∧ ?I› by blast
qed

lemma wf_tranclp_cdclNOT_no_learn_and_forget_infinite_chain:
  assumes
    no_infinite_lf: ‹⋀f j. ¬ (∀i≥j. learn_or_forget (f i) (f (Suc i)))›
  shows ‹wf {(T, S). cdclNOT++ S T ∧ cdclNOT_NOT_all_inv A S}›
  using wf_trancl[OF wf_cdclNOT_no_learn_and_forget_infinite_chain[OF no_infinite_lf]]
  apply (rule wf_subset)
  by (auto simp: trancl_set_tranclp inv_and_tranclp_cdcl_NOT_tranclp_cdclNOT_and_inv)

lemma cdclNOT_final_state:
  assumes
    n_s: ‹no_step cdclNOT S› and
    inv: ‹cdclNOT_NOT_all_inv A S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT S))
    ∨ (trail S ⊨asm clausesNOT S ∧ satisfiable (set_mset (clausesNOT S)))›
proof -
  have n_s': ‹no_step dpll_bj S›
    using n_s by (auto simp: cdclNOT.simps)
  show ?thesis
    apply (rule dpll_backjump_final_state[of S A])
    using inv decomp n_s' unfolding cdclNOT_NOT_all_inv_def by auto
qed

lemma full_cdclNOT_final_state:
  assumes
    full: ‹full cdclNOT S T› and
    inv: ‹cdclNOT_NOT_all_inv A S› and
    n_d: ‹no_dup (trail S)› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT T))
    ∨ (trail T ⊨asm clausesNOT T ∧ satisfiable (set_mset (clausesNOT T)))›
proof -
  have st: ‹cdclNOT** S T› and n_s: ‹no_step cdclNOT T›
    using full unfolding full_def by blast+
  have n_s': ‹cdclNOT_NOT_all_inv A T›
    using cdclNOT_NOT_all_inv inv st by blast
  moreover have ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
    using cdclNOT_NOT_all_inv_def decomp inv rtranclp_cdclNOT_all_decomposition_implies st by auto
  ultimately show ?thesis
    using cdclNOT_final_state n_s by blast
qed

end ― ‹End of the locale @{locale conflict_driven_clause_learning}.›


subsubsection ‹Termination›

text ‹To prove termination we need to restrict learn and forget. Otherwise we could forget and
  relearn the exact same clause over and over. A first idea is to forbid removing clauses that
  can be used to backjump. This does not change the rules of the calculus. A second idea is to
  ``merge'' backjump and learn: that way, though closer to implementation, needs a change of the
  rules, since the backjump-rule learns the clause used to backjump.›

subsubsection ‹Restricting learn and forget›

locale conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt =
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT +
  conflict_driven_clause_learning trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    inv decide_conds backjump_conds propagate_conds
  ‹λC S. distinct_mset C ∧ ¬tautology C ∧ learn_restrictions C S ∧
    (∃F K d F' C' L. trail S = F' @ Decided K # F ∧ C = add_mset L C' ∧ F ⊨as CNot C'
      ∧ add_mset L C' ∉# clausesNOT S)›
  ‹λC S. ¬(∃F' F K d L. trail S = F' @ Decided K # F ∧ F ⊨as CNot (remove1_mset L C))
    ∧ forget_restrictions C S›
    for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    learn_restrictions forget_restrictions :: ‹'v clause ⇒ 'st ⇒ bool›
begin

lemma cdclNOT_learn_all_induct[consumes 1, case_names dpll_bj learn forgetNOT]:
  fixes S T :: ‹'st›
  assumes ‹cdclNOT S T› and
    dpll: ‹⋀T. dpll_bj S T ⟹ P S T› and
    learning:
      ‹⋀C F K F' C' L T. clausesNOT S ⊨pm C ⟹
        atms_of C ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S)) ⟹
        distinct_mset C ⟹
        ¬ tautology C ⟹
        learn_restrictions C S ⟹
        trail S = F' @ Decided K # F ⟹
        C = add_mset L C' ⟹
        F ⊨as CNot C' ⟹
        add_mset L C' ∉# clausesNOT S ⟹
        T ∼ add_clsNOT C S ⟹
        P S T› and
    forgetting: ‹⋀C T. removeAll_mset C (clausesNOT S) ⊨pm C ⟹
      C ∈# clausesNOT S ⟹
      ¬(∃F' F K L. trail S = F' @ Decided K # F ∧ F ⊨as CNot (C - {#L#})) ⟹
      T ∼ remove_clsNOT C S ⟹
      forget_restrictions C S ⟹
      P S T›
    shows ‹P S T›
  using assms(1)
  apply (induction rule: cdclNOT.induct)
    apply (auto dest: assms(2) simp add: learn_ops_axioms)[]
   apply (auto elim!: learn_ops.learn.cases[OF learn_ops_axioms] dest: assms(3))[]
  apply (auto elim!: forget_ops.forgetNOT.cases[OF forget_ops_axioms] dest!: assms(4))
  done

lemma rtranclp_cdclNOT_inv:
  ‹cdclNOT** S T ⟹ inv S ⟹ inv T›
  apply (induction rule: rtranclp_induct)
   apply simp
  using cdclNOT_inv unfolding conflict_driven_clause_learning_def
  conflict_driven_clause_learning_axioms_def by blast

lemma learn_always_simple_clauses:
  assumes
    learn: ‹learn S T› and
    n_d: ‹no_dup (trail S)›
  shows ‹set_mset (clausesNOT T - clausesNOT S)
    ⊆ simple_clss (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
proof
  fix C assume C: ‹C ∈ set_mset (clausesNOT T - clausesNOT S)›
  have ‹distinct_mset C› ‹¬tautology C› using learn C n_d by (elim learnNOTE; auto)+
  then have ‹C ∈ simple_clss (atms_of C)›
    using distinct_mset_not_tautology_implies_in_simple_clss by blast
  moreover have ‹atms_of C ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S)›
    using learn C n_d by (elim learnNOTE) (auto simp: atms_of_ms_def atms_of_def image_Un
      true_annots_CNot_all_atms_defined)
  moreover have ‹finite (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
     by auto
  ultimately show ‹C ∈ simple_clss (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
    using simple_clss_mono by (metis (no_types) insert_subset mk_disjoint_insert)
qed

definition ‹conflicting_bj_clss S ≡
   {C+{#L#} |C L. C+{#L#} ∈# clausesNOT S ∧ distinct_mset (C+{#L#})
   ∧ ¬tautology (C+{#L#})
     ∧ (∃F' K F. trail S = F' @ Decided K # F ∧ F ⊨as CNot C)}›

lemma conflicting_bj_clss_remove_clsNOT[simp]:
  ‹conflicting_bj_clss (remove_clsNOT C S) = conflicting_bj_clss S - {C}›
  unfolding conflicting_bj_clss_def by fastforce

lemma conflicting_bj_clss_remove_clsNOT'[simp]:
  ‹T ∼ remove_clsNOT C S ⟹ conflicting_bj_clss T = conflicting_bj_clss S - {C}›
  unfolding conflicting_bj_clss_def by fastforce

lemma conflicting_bj_clss_add_clsNOT_state_eq:
  assumes
    T: ‹T ∼ add_clsNOT C' S› and
    n_d: ‹no_dup (trail S)›
  shows ‹conflicting_bj_clss T
    = conflicting_bj_clss S
      ∪ (if ∃C L. C' = add_mset L C ∧ distinct_mset (add_mset L C) ∧ ¬tautology (add_mset L C)
     ∧ (∃F' K d F. trail S = F' @ Decided K # F ∧ F ⊨as CNot C)
     then {C'} else {})›
proof -
  define P where ‹P = (λC L T. distinct_mset (add_mset L C) ∧ ¬ tautology (add_mset L C) ∧
    (∃F' K F. trail T = F' @ Decided K # F ∧ F ⊨as CNot C))›
  have conf: ‹⋀T. conflicting_bj_clss T = {add_mset L C |C L. add_mset L C ∈# clausesNOT T ∧ P C L T}›
    unfolding conflicting_bj_clss_def P_def by auto
  have P_S_T: ‹⋀C L. P C L T = P C L S›
    using T n_d unfolding P_def by auto
  have P: ‹conflicting_bj_clss T = {add_mset L C |C L. add_mset L C ∈# clausesNOT S ∧ P C L T} ∪
     {add_mset L C |C L. add_mset L C ∈# {#C'#} ∧ P C L T}›
    using T n_d unfolding conf by auto
  moreover have ‹{add_mset L C |C L. add_mset L C ∈# clausesNOT S ∧ P C L T} = conflicting_bj_clss S›
    using T n_d unfolding P_def conflicting_bj_clss_def by auto
  moreover have ‹{add_mset L C |C L. add_mset L C ∈# {#C'#} ∧ P C L T} =
    (if ∃C L. C' = add_mset L C ∧ P C L S then {C'} else {})›
    using n_d T by (force simp: P_S_T)
  ultimately show ?thesis unfolding P_def by presburger
qed

lemma conflicting_bj_clss_add_clsNOT:
  ‹no_dup (trail S) ⟹
  conflicting_bj_clss (add_clsNOT C' S)
    = conflicting_bj_clss S
      ∪ (if ∃C L. C' = C +{#L#}∧ distinct_mset (C+{#L#}) ∧ ¬tautology (C+{#L#})
     ∧ (∃F' K d F. trail S = F' @ Decided K # F ∧ F ⊨as CNot C)
     then {C'} else {})›
  using conflicting_bj_clss_add_clsNOT_state_eq by auto

lemma conflicting_bj_clss_incl_clauses:
   ‹conflicting_bj_clss S ⊆ set_mset (clausesNOT S)›
  unfolding conflicting_bj_clss_def by auto

lemma finite_conflicting_bj_clss[simp]:
  ‹finite (conflicting_bj_clss S)›
  using conflicting_bj_clss_incl_clauses[of S] rev_finite_subset by blast

lemma learn_conflicting_increasing:
  ‹no_dup (trail S) ⟹ learn S T ⟹ conflicting_bj_clss S ⊆ conflicting_bj_clss T›
  apply (elim learnNOTE)
  by (subst conflicting_bj_clss_add_clsNOT_state_eq[of T]) auto

abbreviation ‹conflicting_bj_clss_yet b S ≡
  3 ^ b - card (conflicting_bj_clss S)›

abbreviation μL :: ‹nat ⇒ 'st ⇒ nat × nat› where
  ‹μL b S ≡ (conflicting_bj_clss_yet b S, card (set_mset (clausesNOT S)))›

lemma do_not_forget_before_backtrack_rule_clause_learned_clause_untouched:
  assumes ‹forgetNOT S T›
  shows ‹conflicting_bj_clss S = conflicting_bj_clss T›
  using assms apply (elim forgetNOTE)
  apply rule
   apply (subst conflicting_bj_clss_remove_clsNOT'[of T], simp)
   apply (fastforce simp: conflicting_bj_clss_def remove1_mset_add_mset_If split: if_splits)
  apply fastforce
  done

lemma forget_μL_decrease:
  assumes forgetNOT: ‹forgetNOT S T›
  shows ‹(μL b T, μL b S) ∈ less_than <*lex*> less_than›
proof -
  have ‹card (set_mset (clausesNOT S)) > 0›
    using forgetNOT by (elim forgetNOTE) (auto simp: size_mset_removeAll_mset_le_iff card_gt_0_iff)
  then have ‹card (set_mset (clausesNOT T)) < card (set_mset (clausesNOT S))›
    using forgetNOT by (elim forgetNOTE) (auto simp: size_mset_removeAll_mset_le_iff)
  then show ?thesis
    unfolding do_not_forget_before_backtrack_rule_clause_learned_clause_untouched[OF forgetNOT]
    by auto
qed

lemma set_condition_or_split:
   ‹{a. (a = b ∨ Q a) ∧ S a} = (if S b then {b} else {}) ∪ {a. Q a ∧ S a}›
  by auto

lemma set_insert_neq:
  ‹A ≠ insert a A ⟷ a ∉ A›
  by auto

lemma learn_μL_decrease:
  assumes learnST: ‹learn S T› and n_d: ‹no_dup (trail S)› and
   A: ‹atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S) ⊆ A› and
   fin_A: ‹finite A›
  shows ‹(μL (card A) T, μL (card A) S) ∈ less_than <*lex*> less_than›
proof -
  have [simp]: ‹(atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))
    = (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
    using learnST n_d by (elim learnNOTE) auto

  then have ‹card (atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))
    = card (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
    by (auto intro!: card_mono)
  then have 3: ‹(3::nat) ^ card (atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))
    = 3 ^ card (atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S))›
    by (auto intro: power_mono)
  moreover have ‹conflicting_bj_clss S ⊆ conflicting_bj_clss T›
    using learnST n_d by (simp add: learn_conflicting_increasing)
  moreover have ‹conflicting_bj_clss S ≠ conflicting_bj_clss T›
    using learnST
    proof (elim learnNOTE, goal_cases)
      case (1 C) note clss_S = this(1) and atms_C = this(2) and inv = this(3) and T = this(4)
      then obtain F K F' C' L where
        tr_S: ‹trail S = F' @ Decided K # F› and
        C: ‹C = add_mset L C'› and
        F: ‹F ⊨as CNot C'› and
        C_S:‹add_mset L C' ∉# clausesNOT S›
        by blast
      moreover have ‹distinct_mset C› ‹¬ tautology C› using inv by blast+
      ultimately have ‹add_mset L C' ∈ conflicting_bj_clss T›
        using T n_d unfolding conflicting_bj_clss_def by fastforce
      moreover have ‹add_mset L C' ∉ conflicting_bj_clss S›
        using C_S unfolding conflicting_bj_clss_def by auto
      ultimately show ?case by blast
    qed
  moreover have fin_T: ‹finite (conflicting_bj_clss T)›
    using learnST by induction (auto simp add: conflicting_bj_clss_add_clsNOT )
  ultimately have ‹card (conflicting_bj_clss T) ≥ card (conflicting_bj_clss S)›
    using card_mono by blast

  moreover
    have fin': ‹finite (atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))›
      by auto
    have 1:‹atms_of_ms (conflicting_bj_clss T) ⊆ atms_of_mm (clausesNOT T)›
      unfolding conflicting_bj_clss_def atms_of_ms_def by auto
    have 2: ‹⋀x. x∈ conflicting_bj_clss T ⟹ ¬ tautology x ∧ distinct_mset x›
      unfolding conflicting_bj_clss_def by auto
    have T: ‹conflicting_bj_clss T
    ⊆ simple_clss (atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))›
      by standard (meson 1 2 fin' ‹finite (conflicting_bj_clss T)› simple_clss_mono
        distinct_mset_set_def simplified_in_simple_clss subsetCE sup.coboundedI1)
  moreover
    then have #: ‹3 ^ card (atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T))
        ≥ card (conflicting_bj_clss T)›
      by (meson Nat.le_trans simple_clss_card simple_clss_finite card_mono fin')
    have ‹atms_of_mm (clausesNOT T) ∪ atm_of ` lits_of_l (trail T) ⊆ A›
      using learnNOTE[OF learnST] A by simp
    then have ‹3 ^ (card A) ≥ card (conflicting_bj_clss T)›
      using # fin_A by (meson simple_clss_card simple_clss_finite
        simple_clss_mono calculation(2) card_mono dual_order.trans)
  ultimately show ?thesis
    using psubset_card_mono[OF fin_T ]
    unfolding less_than_iff lex_prod_def by clarify
      (meson ‹conflicting_bj_clss S ≠ conflicting_bj_clss T›
        ‹conflicting_bj_clss S ⊆ conflicting_bj_clss T›
        diff_less_mono2 le_less_trans not_le psubsetI)
qed

text ‹We have to assume the following:
  ▪ @{term ‹inv S›}: the invariant holds in the inital state.
  ▪ @{term A} is a (finite @{term ‹finite A›}) superset of the literals in the trail
  @{term ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A›}
  and in the clauses @{term ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A›}. This can the the set of all
  the literals in the starting set of clauses.
  ▪ @{term ‹no_dup (trail S)›}: no duplicate in the trail. This is invariant along the path.›
definition μCDCL where
‹μCDCL A T ≡ ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
               - μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T),
            conflicting_bj_clss_yet (card (atms_of_ms A)) T, card (set_mset (clausesNOT T)))›
lemma cdclNOT_decreasing_measure:
  assumes
    ‹cdclNOT S T› and
    inv: ‹inv S› and
    atm_clss: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atm_lits: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    fin_A: ‹finite A›
  shows ‹(μCDCL A T, μCDCL A S)
            ∈ less_than <*lex*> (less_than <*lex*> less_than)›
  using assms(1)
proof induction
  case (c_dpll_bj T)
  from dpll_bj_trail_mes_decreasing_prop[OF this(1) inv atm_clss atm_lits n_d fin_A]
  show ?case unfolding μCDCL_def
    by (meson in_lex_prod less_than_iff)
next
  case (c_learn T) note learn = this(1)
  then have S: ‹trail S = trail T›
    using inv atm_clss atm_lits n_d fin_A
    by (elim learnNOTE) auto
  show ?case
    using learn_μL_decrease[OF learn n_d, of ‹atms_of_ms A›] atm_clss atm_lits fin_A n_d
    unfolding S μCDCL_def by auto
next
  case (c_forgetNOT T) note forgetNOT = this(1)
  have ‹trail S = trail T› using forgetNOT by induction auto
  then show ?case
    using forget_μL_decrease[OF forgetNOT] unfolding μCDCL_def by auto
qed

lemma wf_cdclNOT_restricted_learning:
  assumes ‹finite A›
  shows ‹wf {(T, S).
    (atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S)
    ∧ inv S)
    ∧ cdclNOT S T }›
  by (rule wf_wf_if_measure'[of ‹less_than <*lex*> (less_than <*lex*> less_than)›])
     (auto intro: cdclNOT_decreasing_measure[OF _ _ _ _ _ assms])

definition μC' :: ‹'v clause set ⇒ 'st ⇒ nat› where
‹μC' A T ≡ μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)›

definition μCDCL' :: ‹'v clause set ⇒ 'st ⇒ nat› where
‹μCDCL' A T ≡
  ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A T) * (1+ 3^card (atms_of_ms A)) * 2
  + conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2
  + card (set_mset (clausesNOT T))›

lemma cdclNOT_decreasing_measure':
  assumes
    ‹cdclNOT S T› and
    inv: ‹inv S› and
    atms_clss: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    fin_A: ‹finite A›
  shows ‹μCDCL' A T < μCDCL' A S›
  using assms(1)
proof (induction rule: cdclNOT_learn_all_induct)
  case (dpll_bj T)
  then have ‹(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A T
    < (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A S›
    using dpll_bj_trail_mes_decreasing_prop fin_A inv n_d atms_clss atms_trail
    unfolding μC'_def by blast
  then have XX: ‹((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A T) + 1
    ≤ (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A S›
    by auto
  from mult_le_mono1[OF this, of ‹1 + 3 ^ card (atms_of_ms A)›]
  have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A T) *
      (1 + 3 ^ card (atms_of_ms A)) + (1 + 3 ^ card (atms_of_ms A))
    ≤ ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A S)
      * (1 + 3 ^ card (atms_of_ms A))›
    unfolding Nat.add_mult_distrib
    by presburger
  moreover
    have cl_T_S: ‹clausesNOT T = clausesNOT S›
      using dpll_bj.hyps inv dpll_bj_clauses by auto
    have ‹conflicting_bj_clss_yet (card (atms_of_ms A)) S < 1+ 3 ^ card (atms_of_ms A)›
    by simp
  ultimately have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A T)
      * (1 + 3 ^ card (atms_of_ms A)) + conflicting_bj_clss_yet (card (atms_of_ms A)) T
    < ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A S) *(1 + 3 ^ card (atms_of_ms A))›
    by linarith
  then have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A T)
        * (1 + 3 ^ card (atms_of_ms A))
      + conflicting_bj_clss_yet (card (atms_of_ms A)) T
    < ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A S)
        * (1 + 3 ^ card (atms_of_ms A))
      + conflicting_bj_clss_yet (card (atms_of_ms A)) S›
    by linarith
  then have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A T)
      * (1 + 3 ^ card (atms_of_ms A)) * 2
    + conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2
    < ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A S)
      * (1 + 3 ^ card (atms_of_ms A)) * 2
    + conflicting_bj_clss_yet (card (atms_of_ms A)) S * 2›
    by linarith
  then show ?case unfolding μCDCL'_def cl_T_S by presburger
next
  case (learn C F' K F C' L T) note clss_S_C = this(1) and atms_C = this(2) and dist = this(3)
    and tauto = this(4) and learn_restr = this(5) and tr_S = this(6) and C' = this(7) and
    F_C = this(8) and C_new = this(9) and T = this(10)
  have ‹insert C (conflicting_bj_clss S) ⊆ simple_clss (atms_of_ms A)›
    proof -
      have ‹C ∈ simple_clss (atms_of_ms A)›
        using C'
        by (metis (no_types, opaque_lifting) Un_subset_iff simple_clss_mono
          contra_subsetD dist distinct_mset_not_tautology_implies_in_simple_clss
          dual_order.trans atms_C atms_clss atms_trail tauto)
      moreover have ‹conflicting_bj_clss S ⊆ simple_clss (atms_of_ms A)›
        proof
          fix x :: ‹'v clause›
          assume ‹x ∈ conflicting_bj_clss S›
          then have ‹x ∈# clausesNOT S ∧ distinct_mset x ∧ ¬ tautology x›
            unfolding conflicting_bj_clss_def by blast
          then show ‹x ∈ simple_clss (atms_of_ms A)›
            by (meson atms_clss atms_of_atms_of_ms_mono atms_of_ms_finite simple_clss_mono
              distinct_mset_not_tautology_implies_in_simple_clss fin_A finite_subset
              set_rev_mp)
        qed
      ultimately show ?thesis
        by auto
    qed
  then have ‹card (insert C (conflicting_bj_clss S)) ≤ 3 ^ (card (atms_of_ms A))›
    by (meson Nat.le_trans atms_of_ms_finite simple_clss_card simple_clss_finite
      card_mono fin_A)
  moreover have [simp]: ‹card (insert C (conflicting_bj_clss S))
    = Suc (card ((conflicting_bj_clss S)))›
    by (metis (no_types) C' C_new card_insert_if conflicting_bj_clss_incl_clauses contra_subsetD
      finite_conflicting_bj_clss)
  moreover have [simp]: ‹conflicting_bj_clss (add_clsNOT C S) = conflicting_bj_clss S ∪ {C}›
    using dist tauto F_C by (subst conflicting_bj_clss_add_clsNOT[OF n_d]) (force simp: C' tr_S n_d)
  ultimately have [simp]: ‹conflicting_bj_clss_yet (card (atms_of_ms A)) S
    = Suc (conflicting_bj_clss_yet (card (atms_of_ms A)) (add_clsNOT C S))›
      by simp
  have 1: ‹clausesNOT T = clausesNOT (add_clsNOT C S)› using T by auto
  have 2: ‹conflicting_bj_clss_yet (card (atms_of_ms A)) T
    = conflicting_bj_clss_yet (card (atms_of_ms A)) (add_clsNOT C S)›
    using T unfolding conflicting_bj_clss_def by auto
  have 3: ‹μC' A T = μC' A (add_clsNOT C S)›
    using T unfolding μC'_def by auto
  have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A (add_clsNOT C S))
    * (1 + 3 ^ card (atms_of_ms A)) * 2
    = ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A S)
    * (1 + 3 ^ card (atms_of_ms A)) * 2›
      using n_d unfolding μC'_def by auto
  moreover
    have ‹conflicting_bj_clss_yet (card (atms_of_ms A)) (add_clsNOT C S)
        * 2
      + card (set_mset (clausesNOT (add_clsNOT C S)))
      < conflicting_bj_clss_yet (card (atms_of_ms A)) S * 2
      + card (set_mset (clausesNOT S))›
      by (simp add: C' C_new n_d)
  ultimately show ?case unfolding μCDCL'_def 1 2 3 by presburger
next
  case (forgetNOT C T) note T = this(4)
  have [simp]: ‹μC' A (remove_clsNOT C S) = μC' A S›
    unfolding μC'_def by auto
  have ‹forgetNOT S T›
    apply (rule forgetNOT.intros) using forgetNOT by auto
  then have ‹conflicting_bj_clss T = conflicting_bj_clss S›
    using do_not_forget_before_backtrack_rule_clause_learned_clause_untouched by blast
  moreover have ‹card (set_mset (clausesNOT T)) < card (set_mset (clausesNOT S))›
    by (metis T card_Diff1_less clauses_remove_clsNOT finite_set_mset forgetNOT.hyps(2)
      order_refl set_mset_minus_replicate_mset(1) state_eqNOT_clauses)
  ultimately show ?case unfolding μCDCL'_def
    using T ‹μC' A (remove_clsNOT C S) = μC' A S› by (metis (no_types) add_le_cancel_left
      μC'_def not_le state_eqNOT_trail)
qed

lemma cdclNOT_clauses_bound:
  assumes
    ‹cdclNOT S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ A› and
    n_d: ‹no_dup (trail S)› and
    fin_A[simp]: ‹finite A›
  shows ‹set_mset (clausesNOT T) ⊆ set_mset (clausesNOT S) ∪ simple_clss A›
  using assms
proof (induction rule: cdclNOT_learn_all_induct)
  case dpll_bj
  then show ?case using dpll_bj_clauses by simp
next
  case forgetNOT
  then show ?case using clauses_remove_clsNOT unfolding state_eqNOT_def by auto
next
  case (learn C F K d F' C' L) note atms_C = this(2) and dist = this(3) and tauto = this(4) and
  T = this(10) and atms_clss_S = this(12) and atms_trail_S = this(13)
  have ‹atms_of C ⊆ A›
    using atms_C atms_clss_S atms_trail_S by fast
  then have ‹simple_clss (atms_of C) ⊆ simple_clss A›
    by (simp add: simple_clss_mono)
  then have ‹C ∈ simple_clss A›
    using finite dist tauto by (auto dest: distinct_mset_not_tautology_implies_in_simple_clss)
  then show ?case using T n_d by auto
qed

lemma rtranclp_cdclNOT_clauses_bound:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite A›
  shows ‹set_mset (clausesNOT T) ⊆ set_mset (clausesNOT S) ∪ simple_clss A›
  using assms(1-5)
proof induction
  case base
  then show ?case by simp
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)[OF this(4-7)] and
    inv = this(4) and atms_clss_S = this(5) and atms_trail_S = this(6) and finite_cls_S = this(7)
  have ‹inv T›
    using rtranclp_cdclNOT_inv st inv by blast
  moreover have ‹atms_of_mm (clausesNOT T) ⊆ A› and ‹atm_of ` lits_of_l (trail T) ⊆ A›
    using rtranclp_cdclNOT_trail_clauses_bound[OF st] inv atms_clss_S atms_trail_S n_d by auto
  moreover have ‹no_dup (trail T)›
   using rtranclp_cdclNOT_no_dup[OF st ‹inv S› n_d] by simp
  ultimately have ‹set_mset (clausesNOT U) ⊆ set_mset (clausesNOT T) ∪ simple_clss A›
    using cdclNOT finite n_d by (auto simp: cdclNOT_clauses_bound)
  then show ?case using IH by auto
qed

lemma rtranclp_cdclNOT_card_clauses_bound:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite A›
  shows ‹card (set_mset (clausesNOT T)) ≤ card (set_mset (clausesNOT S)) + 3 ^ (card A)›
  using rtranclp_cdclNOT_clauses_bound[OF assms] finite by (meson Nat.le_trans
    simple_clss_card simple_clss_finite card_Un_le card_mono finite_UnI
    finite_set_mset nat_add_left_cancel_le)

lemma rtranclp_cdclNOT_card_clauses_bound':
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite A›
  shows ‹card {C|C. C ∈# clausesNOT T ∧ (tautology C ∨ ¬distinct_mset C)}
    ≤ card {C|C. C∈# clausesNOT S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card A)›
    (is ‹card ?T ≤ card ?S + _›)
  using rtranclp_cdclNOT_clauses_bound[OF assms] finite
proof -
  have ‹?T ⊆ ?S ∪ simple_clss A›
    using rtranclp_cdclNOT_clauses_bound[OF assms] by force
  then have ‹card ?T ≤ card (?S ∪ simple_clss A)›
    using finite by (simp add: assms(5) simple_clss_finite card_mono)
  then show ?thesis
    by (meson le_trans simple_clss_card card_Un_le local.finite nat_add_left_cancel_le)
qed

lemma rtranclp_cdclNOT_card_simple_clauses_bound:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    NA: ‹atms_of_mm (clausesNOT S) ⊆ A› and
    MA: ‹atm_of ` (lits_of_l (trail S)) ⊆ A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite A›
  shows ‹card (set_mset (clausesNOT T))
  ≤ card {C. C ∈# clausesNOT S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card A)›
    (is ‹card ?T ≤ card ?S + _›)
  using rtranclp_cdclNOT_clauses_bound[OF assms] finite
proof -
  have ‹⋀x. x ∈# clausesNOT T ⟹ ¬ tautology x ⟹ distinct_mset x ⟹ x ∈ simple_clss A›
    using rtranclp_cdclNOT_clauses_bound[OF assms] by (metis (no_types, opaque_lifting) Un_iff NA
      atms_of_atms_of_ms_mono simple_clss_mono contra_subsetD subset_trans
      distinct_mset_not_tautology_implies_in_simple_clss)
  then have ‹set_mset (clausesNOT T) ⊆ ?S ∪ simple_clss A›
    using rtranclp_cdclNOT_clauses_bound[OF assms] by auto
  then have ‹card(set_mset (clausesNOT T)) ≤ card (?S ∪ simple_clss A)›
    using finite by (simp add: assms(5) simple_clss_finite card_mono)
  then show ?thesis
    by (meson le_trans simple_clss_card card_Un_le local.finite nat_add_left_cancel_le)
qed

definition μCDCL'_bound :: ‹'v clause set ⇒ 'st ⇒ nat› where
‹μCDCL'_bound A S =
  ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))) * (1 + 3 ^ card (atms_of_ms A)) * 2
     + 2*3 ^ (card (atms_of_ms A))
     + card {C. C ∈# clausesNOT S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card (atms_of_ms A))›

lemma μCDCL'_bound_reduce_trail_toNOT[simp]:
  ‹μCDCL'_bound A (reduce_trail_toNOT M S) = μCDCL'_bound A S›
  unfolding μCDCL'_bound_def by auto

lemma rtranclp_cdclNOT_μCDCL'_bound_reduce_trail_toNOT:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite (atms_of_ms A)› and
    U: ‹U ∼ reduce_trail_toNOT M T›
  shows ‹μCDCL' A U ≤ μCDCL'_bound A S›
proof -
  have ‹ ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A U)
    ≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))›
    by auto
  then have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A U)
        * (1 + 3 ^ card (atms_of_ms A)) * 2
    ≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) * (1 + 3 ^ card (atms_of_ms A)) * 2›
    using mult_le_mono1 by blast
  moreover
    have ‹conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2 ≤ 2 * 3 ^ card (atms_of_ms A)›
      by linarith
  moreover have ‹card (set_mset (clausesNOT U))
      ≤ card {C. C ∈# clausesNOT S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ card (atms_of_ms A)›
    using rtranclp_cdclNOT_card_simple_clauses_bound[OF assms(1-6)] U by auto
  ultimately show ?thesis
    unfolding μCDCL'_def μCDCL'_bound_def by linarith
qed

lemma rtranclp_cdclNOT_μCDCL'_bound:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    finite: ‹finite (atms_of_ms A)›
  shows ‹μCDCL' A T ≤ μCDCL'_bound A S›
proof -
  have ‹μCDCL' A (reduce_trail_toNOT (trail T) T) = μCDCL' A T›
    unfolding μCDCL'_def μC'_def conflicting_bj_clss_def by auto
  then show ?thesis using rtranclp_cdclNOT_μCDCL'_bound_reduce_trail_toNOT[OF assms, of _ ‹trail T›]
    state_eqNOT_ref by fastforce
qed

lemma rtranclp_μCDCL'_bound_decreasing:
  assumes
    ‹cdclNOT** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    finite[simp]: ‹finite (atms_of_ms A)›
  shows ‹μCDCL'_bound A T ≤ μCDCL'_bound A S›
proof -
  have ‹{C. C ∈# clausesNOT T ∧ (tautology C ∨ ¬ distinct_mset C)}
    ⊆ {C. C ∈# clausesNOT S ∧ (tautology C ∨ ¬ distinct_mset C)}› (is ‹?T ⊆ ?S›)
    proof (rule Set.subsetI)
      fix C assume ‹C ∈ ?T›
      then have C_T: ‹C ∈# clausesNOT T› and t_d: ‹tautology C ∨ ¬ distinct_mset C›
        by auto
      then have ‹C ∉ simple_clss (atms_of_ms A)›
        by (auto dest: simple_clssE)
      then show ‹C ∈ ?S›
        using C_T rtranclp_cdclNOT_clauses_bound[OF assms] t_d by force
    qed
  then have ‹card {C. C ∈# clausesNOT T ∧ (tautology C ∨ ¬ distinct_mset C)} ≤
    card {C. C ∈# clausesNOT S ∧ (tautology C ∨ ¬ distinct_mset C)}›
    by (simp add: card_mono)
  then show ?thesis
    unfolding μCDCL'_bound_def by auto
qed

end ― ‹End of the locale @{locale conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt}.›


subsection ‹CDCL with Restarts›

subsubsection‹Definition›

locale restart_ops =
  fixes
    cdclNOT :: ‹'st ⇒ 'st ⇒ bool› and
    restart :: ‹'st ⇒ 'st ⇒ bool›
begin
inductive cdclNOT_raw_restart :: ‹'st ⇒ 'st ⇒ bool› where
‹cdclNOT S T ⟹ cdclNOT_raw_restart S T› |
‹restart S T ⟹ cdclNOT_raw_restart S T›

end

locale conflict_driven_clause_learning_with_restarts =
  conflict_driven_clause_learning trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    inv decide_conds backjump_conds propagate_conds learn_conds forget_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    learn_conds forget_conds :: ‹'v clause ⇒ 'st ⇒ bool›
begin

lemma cdclNOT_iff_cdclNOT_raw_restart_no_restarts:
  ‹cdclNOT S T ⟷ restart_ops.cdclNOT_raw_restart cdclNOT (λ_ _. False) S T›
  (is ‹?C S T ⟷ ?R S T›)
proof
  fix S T
  assume ‹?C S T›
  then show ‹?R S T› by (simp add: restart_ops.cdclNOT_raw_restart.intros(1))
next
  fix S T
  assume ‹?R S T›
  then show ‹?C S T›
    apply (cases rule: restart_ops.cdclNOT_raw_restart.cases)
    using ‹?R S T› by fast+
qed

lemma cdclNOT_cdclNOT_raw_restart:
  ‹cdclNOT S T ⟹ restart_ops.cdclNOT_raw_restart cdclNOT restart S T›
  by (simp add: restart_ops.cdclNOT_raw_restart.intros(1))
end


subsubsection ‹Increasing restarts›

paragraph ‹Definition›

text ‹
  We define our increasing restart very abstractly: the predicate (called @{term cdclNOT}) does not
  have to be a CDCL calculus. We just need some assuptions to prove termination:
  ▪ a function @{term f} that is strictly monotonic. The first step is actually only used as a
  restart to clean the state (e.g. to ensure that the trail is empty). Then we assume that
  @{term ‹f n ≥ 1›} for @{term ‹n ≥ 1›}: it means that between two consecutive
  restarts, at least one step will be done. This is necessary to avoid sequence. like: full --
  restart -- full -- ...
  ▪ a measure @{term μ}: it should decrease under the assumptions @{term bound_inv}, whenever a
  @{term cdclNOT} or a @{term restart} is done. A parameter is given to @{term μ}: for conflict-
  driven clause learning, it is an upper-bound of the clauses. We are assuming that such a bound
  can be found after a restart whenever the invariant holds.
  ▪ we also assume that the measure decrease after any @{term cdclNOT} step.
  ▪ an invariant on the states @{term cdclNOT_inv} that also holds after restarts.
  ▪ it is ∗‹not required› that the measure decrease with respect to restarts, but the measure has to
  be bound by some function @{term μ_bound} taking the same parameter as @{term μ} and the initial
  state of the considered @{term cdclNOT} chain.›
locale cdclNOT_increasing_restarts_ops =
  restart_ops cdclNOT restart for
    restart :: ‹'st ⇒ 'st ⇒ bool› and
    cdclNOT :: ‹'st ⇒ 'st ⇒ bool› +
  fixes
    f :: ‹nat ⇒ nat› and
    bound_inv :: ‹'bound ⇒ 'st ⇒ bool› and
    μ :: ‹'bound ⇒ 'st ⇒ nat› and
    cdclNOT_inv :: ‹'st ⇒ bool› and
    μ_bound :: ‹'bound ⇒ 'st ⇒ nat›
  assumes
    f: ‹unbounded f› and
    f_ge_1: ‹⋀n. n≥1 ⟹ f n ≠ 0› and
    bound_inv: ‹⋀A S T. cdclNOT_inv S ⟹ bound_inv A S ⟹ cdclNOT S T ⟹ bound_inv A T› and
    cdclNOT_measure: ‹⋀A S T. cdclNOT_inv S ⟹ bound_inv A S ⟹ cdclNOT S T ⟹ μ A T < μ A S› and
    measure_bound2: ‹⋀A T U. cdclNOT_inv T ⟹ bound_inv A T ⟹ cdclNOT** T U
       ⟹ μ A U ≤ μ_bound A T› and
    measure_bound4: ‹⋀A T U. cdclNOT_inv T ⟹ bound_inv A T ⟹ cdclNOT** T U
       ⟹ μ_bound A U ≤ μ_bound A T› and
    cdclNOT_restart_inv: ‹⋀A U V. cdclNOT_inv U ⟹ restart U V ⟹ bound_inv A U ⟹ bound_inv A V›
      and
    exists_bound: ‹⋀R S. cdclNOT_inv R ⟹ restart R S ⟹ ∃A. bound_inv A S› and
    cdclNOT_inv: ‹⋀S T. cdclNOT_inv S ⟹ cdclNOT S T ⟹ cdclNOT_inv T› and
    cdclNOT_inv_restart: ‹⋀S T. cdclNOT_inv S ⟹ restart S T ⟹ cdclNOT_inv T›
begin

lemma cdclNOT_cdclNOT_inv:
  assumes
    ‹(cdclNOT^^n) S T› and
    ‹cdclNOT_inv S›
  shows ‹cdclNOT_inv T›
  using assms by (induction n arbitrary: T) (auto intro:bound_inv cdclNOT_inv)

lemma cdclNOT_bound_inv:
  assumes
    ‹(cdclNOT^^n) S T› and
    ‹cdclNOT_inv S›
    ‹bound_inv A S›
  shows ‹bound_inv A T›
  using assms by (induction n arbitrary: T) (auto intro:bound_inv cdclNOT_cdclNOT_inv)

lemma rtranclp_cdclNOT_cdclNOT_inv:
  assumes
    ‹cdclNOT** S T› and
    ‹cdclNOT_inv S›
  shows ‹cdclNOT_inv T›
  using assms by induction (auto intro: cdclNOT_inv)

lemma rtranclp_cdclNOT_bound_inv:
  assumes
    ‹cdclNOT** S T› and
    ‹bound_inv A S› and
    ‹cdclNOT_inv S›
  shows ‹bound_inv A T›
  using assms by induction (auto intro:bound_inv rtranclp_cdclNOT_cdclNOT_inv)

lemma cdclNOT_comp_n_le:
  assumes
    ‹(cdclNOT^^(Suc n)) S T› and
    ‹bound_inv A S›
    ‹cdclNOT_inv S›
  shows ‹μ A T < μ A S - n›
  using assms
proof (induction n arbitrary: T)
  case 0
  then show ?case using cdclNOT_measure by auto
next
  case (Suc n) note IH = this(1)[OF _ this(3) this(4)] and S_T = this(2) and b_inv = this(3) and
  c_inv = this(4)
  obtain U :: 'st where S_U: ‹(cdclNOT^^(Suc n)) S U› and U_T: ‹cdclNOT U T› using S_T by auto
  then have ‹μ A U < μ A S - n› using IH[of U] by simp
  moreover
    have ‹bound_inv A U›
      using S_U b_inv cdclNOT_bound_inv c_inv by blast
    then have ‹μ A T < μ A U› using cdclNOT_measure[OF _ _ U_T] S_U c_inv cdclNOT_cdclNOT_inv by auto
  ultimately show ?case by linarith
qed

lemma wf_cdclNOT:
  ‹wf {(T, S). cdclNOT S T ∧ cdclNOT_inv S ∧ bound_inv A S}› (is ‹wf ?A›)
  apply (rule wfP_if_measure2[of _ _ ‹μ A›])
  using cdclNOT_comp_n_le[of 0 _ _ A] by auto

lemma rtranclp_cdclNOT_measure:
  assumes
    ‹cdclNOT** S T› and
    ‹bound_inv A S› and
    ‹cdclNOT_inv S›
  shows ‹μ A T ≤ μ A S›
  using assms
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step T U) note IH = this(3)[OF this(4) this(5)] and st = this(1) and cdclNOT = this(2) and
    b_inv = this(4) and c_inv = this(5)
  have ‹bound_inv A T›
    by (meson cdclNOT_bound_inv rtranclp_imp_relpowp st step.prems)
  moreover have ‹cdclNOT_inv T›
    using c_inv rtranclp_cdclNOT_cdclNOT_inv st by blast
  ultimately have ‹μ A U < μ A T› using cdclNOT_measure[OF _ _ cdclNOT] by auto
  then show ?case using IH by linarith
qed

lemma cdclNOT_comp_bounded:
  assumes
    ‹bound_inv A S› and ‹cdclNOT_inv S› and ‹m ≥ 1+μ A S›
  shows ‹¬(cdclNOT ^^ m) S T›
  using assms cdclNOT_comp_n_le[of ‹m-1› S T A] by fastforce

text ‹
  ▪ @{term ‹m > f n›} ensures that at least one step has been done.›
inductive cdclNOT_restart where
restart_step: ‹(cdclNOT^^m) S T ⟹ m ≥ f n ⟹ restart T U
  ⟹ cdclNOT_restart (S, n) (U, Suc n)› |
restart_full: ‹full1 cdclNOT S T ⟹ cdclNOT_restart (S, n) (T, Suc n)›

lemmas cdclNOT_with_restart_induct = cdclNOT_restart.induct[split_format(complete),
  OF cdclNOT_increasing_restarts_ops_axioms]

lemma cdclNOT_restart_cdclNOT_raw_restart:
  ‹cdclNOT_restart S T ⟹ cdclNOT_raw_restart** (fst S) (fst T)›
proof (induction rule: cdclNOT_restart.induct)
  case (restart_step m S T n U)
  then have ‹cdclNOT** S T› by (meson relpowp_imp_rtranclp)
  then have ‹cdclNOT_raw_restart** S T› using cdclNOT_raw_restart.intros(1)
    rtranclp_mono[of cdclNOT cdclNOT_raw_restart] by blast
  moreover have ‹cdclNOT_raw_restart T U›
    using ‹restart T U› cdclNOT_raw_restart.intros(2) by blast
  ultimately show ?case by auto
next
  case (restart_full S T)
  then have ‹cdclNOT** S T› unfolding full1_def by auto
  then show ?case using cdclNOT_raw_restart.intros(1)
    rtranclp_mono[of cdclNOT cdclNOT_raw_restart] by auto
qed

lemma cdclNOT_with_restart_bound_inv:
  assumes
    ‹cdclNOT_restart S T› and
    ‹bound_inv A (fst S)› and
    ‹cdclNOT_inv (fst S)›
  shows ‹bound_inv A (fst T)›
  using assms apply (induction rule: cdclNOT_restart.induct)
    prefer 2 apply (metis rtranclp_unfold fstI full1_def rtranclp_cdclNOT_bound_inv)
  by (metis cdclNOT_bound_inv cdclNOT_cdclNOT_inv cdclNOT_restart_inv fst_conv)

lemma cdclNOT_with_restart_cdclNOT_inv:
  assumes
    ‹cdclNOT_restart S T› and
    ‹cdclNOT_inv (fst S)›
  shows ‹cdclNOT_inv (fst T)›
  using assms apply induction
    apply (metis cdclNOT_cdclNOT_inv cdclNOT_inv_restart fst_conv)
   apply (metis fstI full_def full_unfold rtranclp_cdclNOT_cdclNOT_inv)
  done

lemma rtranclp_cdclNOT_with_restart_cdclNOT_inv:
  assumes
    ‹cdclNOT_restart** S T› and
    ‹cdclNOT_inv (fst S)›
  shows ‹cdclNOT_inv (fst T)›
  using assms by induction (auto intro: cdclNOT_with_restart_cdclNOT_inv)

lemma rtranclp_cdclNOT_with_restart_bound_inv:
  assumes
    ‹cdclNOT_restart** S T› and
    ‹cdclNOT_inv (fst S)› and
    ‹bound_inv A (fst S)›
  shows ‹bound_inv A (fst T)›
  using assms apply induction
   apply (simp add: cdclNOT_cdclNOT_inv cdclNOT_with_restart_bound_inv)
  using cdclNOT_with_restart_bound_inv rtranclp_cdclNOT_with_restart_cdclNOT_inv by blast

lemma cdclNOT_with_restart_increasing_number:
  ‹cdclNOT_restart S T ⟹ snd T = 1 + snd S›
  by (induction rule: cdclNOT_restart.induct) auto
end

locale cdclNOT_increasing_restarts =
  cdclNOT_increasing_restarts_ops restart cdclNOT f bound_inv μ cdclNOT_inv μ_bound +
  dpll_state trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    f :: ‹nat ⇒ nat› and
    restart :: ‹'st ⇒ 'st ⇒ bool› and
    bound_inv :: ‹'bound ⇒ 'st ⇒ bool› and
    μ :: ‹'bound ⇒ 'st ⇒ nat› and
    cdclNOT :: ‹'st ⇒ 'st ⇒ bool› and
    cdclNOT_inv :: ‹'st ⇒ bool› and
    μ_bound :: ‹'bound ⇒ 'st ⇒ nat› +
  assumes
    measure_bound: ‹⋀A T V n. cdclNOT_inv T ⟹ bound_inv A T
      ⟹ cdclNOT_restart (T, n) (V, Suc n) ⟹ μ A V ≤ μ_bound A T› and
    cdclNOT_raw_restart_μ_bound:
      ‹cdclNOT_restart (T, a) (V, b) ⟹ cdclNOT_inv T ⟹ bound_inv A T
        ⟹ μ_bound A V ≤ μ_bound A T›
begin

lemma rtranclp_cdclNOT_raw_restart_μ_bound:
  ‹cdclNOT_restart** (T, a) (V, b) ⟹ cdclNOT_inv T ⟹ bound_inv A T
    ⟹ μ_bound A V ≤ μ_bound A T›
  apply (induction rule: rtranclp_induct2)
   apply simp
  by (metis cdclNOT_raw_restart_μ_bound dual_order.trans fst_conv
    rtranclp_cdclNOT_with_restart_bound_inv rtranclp_cdclNOT_with_restart_cdclNOT_inv)

lemma cdclNOT_raw_restart_measure_bound:
  ‹cdclNOT_restart (T, a) (V, b) ⟹ cdclNOT_inv T ⟹ bound_inv A T
    ⟹ μ A V ≤ μ_bound A T›
  apply (cases rule: cdclNOT_restart.cases)
     apply simp
    using measure_bound relpowp_imp_rtranclp apply fastforce
   by (metis full_def full_unfold measure_bound2 prod.inject)

lemma rtranclp_cdclNOT_raw_restart_measure_bound:
  ‹cdclNOT_restart** (T, a) (V, b) ⟹ cdclNOT_inv T ⟹ bound_inv A T
    ⟹ μ A V ≤ μ_bound A T›
  apply (induction rule: rtranclp_induct2)
    apply (simp add: measure_bound2)
  by (metis dual_order.trans fst_conv measure_bound2 r_into_rtranclp rtranclp.rtrancl_refl
    rtranclp_cdclNOT_with_restart_bound_inv rtranclp_cdclNOT_with_restart_cdclNOT_inv
    rtranclp_cdclNOT_raw_restart_μ_bound)

lemma wf_cdclNOT_restart:
  ‹wf {(T, S). cdclNOT_restart S T ∧ cdclNOT_inv (fst S)}› (is ‹wf ?A›)
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g where
    g: ‹⋀i. cdclNOT_restart (g i) (g (Suc i))› and
    cdclNOT_inv_g: ‹⋀i. cdclNOT_inv (fst (g i))›
    unfolding wf_iff_no_infinite_down_chain by fast

  have snd_g: ‹⋀i. snd (g i) = i + snd (g 0)›
    apply (induct_tac i)
      apply simp
      by (metis Suc_eq_plus1_left add.commute add.left_commute
        cdclNOT_with_restart_increasing_number g)
  then have snd_g_0: ‹⋀i. i > 0 ⟹ snd (g i) = i + snd (g 0)›
    by blast
  have unbounded_f_g: ‹unbounded (λi. f (snd (g i)))›
    using f unfolding bounded_def by (metis add.commute f less_or_eq_imp_le snd_g
      not_bounded_nat_exists_larger not_le le_iff_add)

  { fix i
    have H: ‹⋀T Ta m. (cdclNOT ^^ m) T Ta ⟹ no_step cdclNOT T ⟹ m = 0›
      apply (case_tac m) by simp (meson relpowp_E2)
    have ‹∃ T m. (cdclNOT ^^ m) (fst (g i)) T ∧ m ≥ f (snd (g i))›
      using g[of i] apply (cases rule: cdclNOT_restart.cases)
        apply auto[]
      using g[of ‹Suc i›] f_ge_1 apply (cases rule: cdclNOT_restart.cases)
      apply (auto simp add: full1_def full_def dest: H dest: tranclpD)
      using H Suc_leI leD by blast
  } note H = this
  obtain A where ‹bound_inv A (fst (g 1))›
    using g[of 0] cdclNOT_inv_g[of 0] apply (cases rule: cdclNOT_restart.cases)
      apply (metis One_nat_def cdclNOT_inv exists_bound fst_conv relpowp_imp_rtranclp
        rtranclp_induct)
      using H[of 1] unfolding full1_def by (metis One_nat_def Suc_eq_plus1 diff_is_0_eq' diff_zero
        f_ge_1 fst_conv le_add2 relpowp_E2 snd_conv)
  let ?j = ‹μ_bound A (fst (g 1)) + 1›
  obtain j where
    j: ‹f (snd (g j)) > ?j› and ‹j > 1›
    using unbounded_f_g not_bounded_nat_exists_larger by blast
  {
     fix i j
     have cdclNOT_with_restart: ‹j ≥ i ⟹ cdclNOT_restart** (g i) (g j)›
       apply (induction j)
         apply simp
       by (metis g le_Suc_eq rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl)
  } note cdclNOT_restart = this
  have ‹cdclNOT_inv (fst (g (Suc 0)))›
    by (simp add: cdclNOT_inv_g)
  have ‹cdclNOT_restart** (fst (g 1), snd (g 1)) (fst (g j), snd (g j))›
    using ‹j> 1› by (simp add: cdclNOT_restart)
  have ‹μ A (fst (g j)) ≤ μ_bound A (fst (g 1))›
    apply (rule rtranclp_cdclNOT_raw_restart_measure_bound)
    using ‹cdclNOT_restart** (fst (g 1), snd (g 1)) (fst (g j), snd (g j))› apply blast
        apply (simp add: cdclNOT_inv_g)
       using ‹bound_inv A (fst (g 1))› apply simp
    done
  then have ‹μ A (fst (g j)) ≤ ?j›
    by auto
  have inv: ‹bound_inv A (fst (g j))›
    using ‹bound_inv A (fst (g 1))› ‹cdclNOT_inv (fst (g (Suc 0)))›
    ‹cdclNOT_restart** (fst (g 1), snd (g 1)) (fst (g j), snd (g j))›
    rtranclp_cdclNOT_with_restart_bound_inv by auto
  obtain T m where
    cdclNOT_m: ‹(cdclNOT ^^ m) (fst (g j)) T› and
    f_m: ‹f (snd (g j)) ≤ m›
    using H[of j] by blast
  have ‹?j < m›
    using f_m j Nat.le_trans by linarith

  then show False
    using ‹μ A (fst (g j)) ≤ μ_bound A (fst (g 1))›
    cdclNOT_comp_bounded[OF inv cdclNOT_inv_g, of ] cdclNOT_inv_g cdclNOT_m
    ‹?j < m› by auto
qed

lemma cdclNOT_restart_steps_bigger_than_bound:
  assumes
    ‹cdclNOT_restart S T› and
    ‹bound_inv A (fst S)› and
    ‹cdclNOT_inv (fst S)› and
    ‹f (snd S) > μ_bound A (fst S)›
  shows ‹full1 cdclNOT (fst S) (fst T)›
  using assms
proof (induction rule: cdclNOT_restart.induct)
  case restart_full
  then show ?case by auto
next
  case (restart_step m S T n U) note st = this(1) and f = this(2) and bound_inv = this(4) and
    cdclNOT_inv = this(5) and μ = this(6)
  then obtain m' where m: ‹m = Suc m'› by (cases m) auto
  have ‹μ A S - m' = 0›
    using f bound_inv cdclNOT_inv μ m rtranclp_cdclNOT_raw_restart_measure_bound by fastforce
  then have False using cdclNOT_comp_n_le[of m' S T A] restart_step unfolding m by simp
  then show ?case by fast
qed

lemma rtranclp_cdclNOT_with_inv_inv_rtranclp_cdclNOT:
  assumes
    inv: ‹cdclNOT_inv S› and
    binv: ‹bound_inv A S›
  shows ‹(λS T. cdclNOT S T ∧ cdclNOT_inv S ∧ bound_inv A S)** S T ⟷ cdclNOT** S T›
    (is ‹?A** S T ⟷ ?B** S T›)
  apply (rule iffI)
    using rtranclp_mono[of ?A ?B] apply blast
  apply (induction rule: rtranclp_induct)
    using inv binv apply simp
  by (metis (mono_tags, lifting) binv inv rtranclp.simps rtranclp_cdclNOT_bound_inv
    rtranclp_cdclNOT_cdclNOT_inv)

lemma no_step_cdclNOT_restart_no_step_cdclNOT:
  assumes
    n_s: ‹no_step cdclNOT_restart S› and
    inv: ‹cdclNOT_inv (fst S)› and
    binv: ‹bound_inv A (fst S)›
  shows ‹no_step cdclNOT (fst S)›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain T where T: ‹cdclNOT (fst S) T›
    by blast
  then obtain U where U: ‹full (λS T. cdclNOT S T ∧ cdclNOT_inv S ∧ bound_inv A S) T U›
     using wf_exists_normal_form_full[OF wf_cdclNOT, of A T] by auto
  moreover have inv_T: ‹cdclNOT_inv T›
    using ‹cdclNOT (fst S) T› cdclNOT_inv inv by blast
  moreover have b_inv_T: ‹bound_inv A T›
    using ‹cdclNOT (fst S) T› binv bound_inv inv by blast
  ultimately have ‹full cdclNOT T U›
    using rtranclp_cdclNOT_with_inv_inv_rtranclp_cdclNOT rtranclp_cdclNOT_bound_inv
    rtranclp_cdclNOT_cdclNOT_inv unfolding full_def by blast
  then have ‹full1 cdclNOT (fst S) U›
    using T full_fullI by metis
  then show False by (metis n_s prod.collapse restart_full)
qed

end

subsection ‹Merging backjump and learning›
locale cdclNOT_merge_bj_learn_ops =
  decide_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT decide_conds +
  forget_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT forget_conds +
  propagate_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT propagate_conds
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    forget_conds :: ‹'v clause ⇒ 'st ⇒ bool› +
  fixes backjump_l_cond :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool›
begin

text ‹We have a new backjump that combines the backjumping on the trail and the learning of the
  used clause (called @{term C''} below)›
inductive backjump_l where
backjump_l: ‹trail S = F' @ Decided K # F
   ⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_toNOT F (add_clsNOT C'' S))
   ⟹ C ∈# clausesNOT S
   ⟹ trail S ⊨as CNot C
   ⟹ undefined_lit F L
   ⟹ atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))
   ⟹ clausesNOT S ⊨pm add_mset L C'
   ⟹ C'' = add_mset L C'
   ⟹ F ⊨as CNot C'
   ⟹ backjump_l_cond C C' L S T
   ⟹ backjump_l S T›

text ‹Avoid (meaningless) simplification in the theorem generated by ‹inductive_cases›:›
declare reduce_trail_toNOT_length_ne[simp del] Set.Un_iff[simp del] Set.insert_iff[simp del]
inductive_cases backjump_lE: ‹backjump_l S T›
thm backjump_lE
declare reduce_trail_toNOT_length_ne[simp] Set.Un_iff[simp] Set.insert_iff[simp]

inductive cdclNOT_merged_bj_learn :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdclNOT_merged_bj_learn_decideNOT: ‹decideNOT S S' ⟹ cdclNOT_merged_bj_learn S S'› |
cdclNOT_merged_bj_learn_propagateNOT: ‹propagateNOT S S' ⟹ cdclNOT_merged_bj_learn S S'› |
cdclNOT_merged_bj_learn_backjump_l: ‹backjump_l S S' ⟹ cdclNOT_merged_bj_learn S S'› |
cdclNOT_merged_bj_learn_forgetNOT: ‹forgetNOT S S' ⟹ cdclNOT_merged_bj_learn S S'›

lemma cdclNOT_merged_bj_learn_no_dup_inv:
  ‹cdclNOT_merged_bj_learn S T ⟹ no_dup (trail S) ⟹ no_dup (trail T)›
  apply (induction rule: cdclNOT_merged_bj_learn.induct)
      using defined_lit_map apply fastforce
    using defined_lit_map apply fastforce
   apply (force simp: defined_lit_map elim!: backjump_lE dest: no_dup_appendD)[]
  using forgetNOT.simps apply (auto; fail)
  done
end

locale cdclNOT_merge_bj_learn_proxy =
  cdclNOT_merge_bj_learn_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    decide_conds propagate_conds forget_conds
    ‹λC C' L' S T. backjump_l_cond C C' L' S T
    ∧ distinct_mset C' ∧ L' ∉# C' ∧ ¬tautology (add_mset L' C')›
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    forget_conds :: ‹'v clause ⇒ 'st ⇒ bool› and
    backjump_l_cond :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› +
  fixes
    inv :: ‹'st ⇒ bool›
begin

abbreviation backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool›
  where
‹backjump_conds ≡ λC C' L' S T. distinct_mset C' ∧ L' ∉# C' ∧ ¬tautology (add_mset L' C')›

sublocale backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  backjump_conds
  by standard

end

locale cdclNOT_merge_bj_learn =
  cdclNOT_merge_bj_learn_proxy trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    decide_conds propagate_conds forget_conds backjump_l_cond inv
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    forget_conds :: ‹'v clause ⇒ 'st ⇒ bool› and
    backjump_l_cond :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    inv :: ‹'st ⇒ bool› +
  assumes
     bj_merge_can_jump:
     ‹⋀S C F' K F L.
       inv S
       ⟹ trail S = F' @ Decided K # F
       ⟹ C ∈# clausesNOT S
       ⟹ trail S ⊨as CNot C
       ⟹ undefined_lit F L
       ⟹ atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (F' @ Decided K # F))
       ⟹ clausesNOT S ⊨pm add_mset L C'
       ⟹ F ⊨as CNot C'
       ⟹ ¬no_step backjump_l S› and
     cdcl_merged_inv: ‹⋀S T. cdclNOT_merged_bj_learn S T ⟹ inv S ⟹ inv T›  and
     can_propagate_or_decide_or_backjump_l:
       ‹atm_of L ∈ atms_of_mm (clausesNOT S) ⟹
       undefined_lit (trail S) L ⟹
       inv S ⟹
       satisfiable (set_mset (clausesNOT S)) ⟹
       ∃T. decideNOT S T ∨ propagateNOT S T ∨ backjump_l S T›
begin

lemma backjump_no_step_backjump_l:
  ‹backjump S T ⟹ inv S ⟹ ¬no_step backjump_l S›
  apply (elim backjumpE)
  apply (rule bj_merge_can_jump)
    apply auto[7]
  by blast

lemma tautology_single_add:
  ‹tautology (L + {#a#}) ⟷ tautology L ∨ -a ∈# L›
  unfolding tautology_decomp by (cases a) auto

lemma backjump_l_implies_exists_backjump:
  assumes bj: ‹backjump_l S T› and ‹inv S› and n_d: ‹no_dup (trail S)›
  shows ‹∃U. backjump S U›
proof -
  obtain C F' K F L C' where
    tr: ‹trail S = F' @ Decided K # F› and
    C: ‹C ∈# clausesNOT S› and
    T: ‹T ∼ prepend_trail (Propagated L ()) (reduce_trail_toNOT F (add_clsNOT (add_mset L C') S))› and
    tr_C: ‹trail S ⊨as CNot C› and
    undef: ‹undefined_lit F L› and
    L: ‹atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
    S_C_L: ‹clausesNOT S ⊨pm add_mset L C'› and
    F_C': ‹F ⊨as CNot C'› and
    cond: ‹backjump_l_cond C C' L S T› and
    dist: ‹distinct_mset (add_mset L C')› and
    taut: ‹¬ tautology (add_mset L C')›
    using bj by (elim backjump_lE) force
  have ‹L ∉# C'›
    using dist by auto
  show ?thesis
    using backjump.intros[OF tr _ C tr_C undef L S_C_L F_C'] cond dist taut
    by auto
qed

text ‹Without additional knowledge on @{term backjump_l_cond}, it is impossible to have the same
  invariant.›
sublocale dpll_with_backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
  inv decide_conds backjump_conds propagate_conds
proof (unfold_locales, goal_cases)
  case 1
  { fix S S'
    assume bj: ‹backjump_l S S'›
    then obtain F' K F L C' C D where
      S': ‹S' ∼ prepend_trail (Propagated L ()) (reduce_trail_toNOT F (add_clsNOT D S))›
        and
      tr_S: ‹trail S = F' @ Decided K # F› and
      C: ‹C ∈# clausesNOT S› and
      tr_S_C: ‹trail S ⊨as CNot C› and
      undef_L: ‹undefined_lit F L› and
      atm_L:
       ‹atm_of L ∈ insert (atm_of K) (atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l F' ∪ lits_of_l F))›
       and
      cls_S_C': ‹clausesNOT S ⊨pm add_mset L C'› and
      F_C': ‹F ⊨as CNot C'› and
      dist: ‹distinct_mset (add_mset L C')› and
      not_tauto: ‹¬ tautology (add_mset L C')› and
      cond: ‹backjump_l_cond C C' L S S'›
      ‹D = add_mset L C'›
      by (elim backjump_lE) simp
    interpret backjumping_ops trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    backjump_conds
      by unfold_locales
    have ‹∃T. backjump S T›
      apply rule
      apply (rule backjump.intros)
               using tr_S apply simp
              apply (rule state_eqNOT_ref)
             using C apply simp
            using tr_S_C apply simp
          using undef_L apply simp
         using atm_L tr_S apply simp
        using cls_S_C' apply simp
       using F_C' apply simp
      using dist not_tauto cond by simp
    }
  then show ?case using 1 bj_merge_can_jump by meson
next
  case 2
  then show ?case
    using can_propagate_or_decide_or_backjump_l backjump_l_implies_exists_backjump by blast
qed

sublocale conflict_driven_clause_learning_ops trail clausesNOT prepend_trail tl_trail add_clsNOT
  remove_clsNOT inv decide_conds backjump_conds propagate_conds
  ‹λC _. distinct_mset C ∧ ¬tautology C›
  forget_conds
  by unfold_locales

lemma backjump_l_learn_backjump:
  assumes bt: ‹backjump_l S T› and inv: ‹inv S›
  shows ‹∃C' L D. learn S (add_clsNOT D S)
    ∧ D = add_mset L C'
    ∧ backjump (add_clsNOT D S) T
    ∧ atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›
proof -
   obtain C F' K F L l C' D where
     tr_S: ‹trail S = F' @ Decided K # F› and
     T: ‹T ∼ prepend_trail (Propagated L l) (reduce_trail_toNOT F (add_clsNOT D S))› and
     C_cls_S: ‹C ∈# clausesNOT S› and
     tr_S_CNot_C: ‹trail S ⊨as CNot C› and
     undef: ‹undefined_lit F L› and
     atm_L: ‹atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
     clss_C: ‹clausesNOT S ⊨pm D› and
     D: ‹D = add_mset L C'›
     ‹F ⊨as CNot C'› and
     distinct: ‹distinct_mset D› and
     not_tauto: ‹¬ tautology D› and
     cond: ‹backjump_l_cond C C' L S T›
     using bt inv by (elim backjump_lE) simp
   have atms_C': ‹atms_of C' ⊆ atm_of ` (lits_of_l F)›
     by (metis D(2) atms_of_def image_subsetI true_annots_CNot_all_atms_defined)
   then have ‹atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›
     using atm_L tr_S by auto
   moreover have learn: ‹learn S (add_clsNOT D S)›
     apply (rule learn.intros)
         apply (rule clss_C)
       using atms_C' atm_L D apply (fastforce simp add: tr_S in_plus_implies_atm_of_on_atms_of_ms)
     apply standard
      apply (rule distinct)
      apply (rule not_tauto)
      apply simp
     done
   moreover have bj: ‹backjump (add_clsNOT D S) T›
     apply (rule backjump.intros[of _ _ _ _ _ L C C'])
     using ‹F ⊨as CNot C'› C_cls_S tr_S_CNot_C undef T distinct not_tauto D cond
     by (auto simp: tr_S state_eqNOT_def simp del: state_simpNOT)
   ultimately show ?thesis using D by blast
qed

lemma backjump_l_backjump_learn:
  assumes bt: ‹backjump_l S T› and inv: ‹inv S›
  shows ‹∃C' L D S'. backjump S S'
    ∧ learn S' T
    ∧ D = (add_mset L C')
    ∧ T ∼ add_clsNOT D S'
    ∧ atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))
    ∧ clausesNOT S ⊨pm D›
proof -
   obtain C F' K F L l C' D where
     tr_S: ‹trail S = F' @ Decided K # F› and
     T: ‹T ∼ prepend_trail (Propagated L l) (reduce_trail_toNOT F (add_clsNOT D S))› and
     C_cls_S: ‹C ∈# clausesNOT S› and
     tr_S_CNot_C: ‹trail S ⊨as CNot C› and
     undef: ‹undefined_lit F L› and
     atm_L: ‹atm_of L ∈ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
     clss_C: ‹clausesNOT S ⊨pm D› and
     D: ‹D = add_mset L C'›
     ‹F ⊨as CNot C'› and
     distinct: ‹distinct_mset D› and
     not_tauto: ‹¬ tautology D› and
     cond: ‹backjump_l_cond C C' L S T›
     using bt inv by (elim backjump_lE) simp
   let ?S' = ‹prepend_trail (Propagated L ()) (reduce_trail_toNOT F S)›
   have atms_C': ‹atms_of C' ⊆ atm_of ` (lits_of_l F)›
     by (metis D(2) atms_of_def image_subsetI true_annots_CNot_all_atms_defined)
   then have ‹atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›
     using atm_L tr_S by auto
   moreover have learn: ‹learn ?S' T›
     apply (rule learn.intros)
         using clss_C apply auto[]
       using atms_C' atm_L D apply (fastforce simp add: tr_S in_plus_implies_atm_of_on_atms_of_ms)
     apply standard
      apply (rule distinct)
      apply (rule not_tauto)
      using T apply (auto simp: tr_S state_eqNOT_def simp del: state_simpNOT)
     done
   moreover have bj: ‹backjump S (prepend_trail (Propagated L ()) (reduce_trail_toNOT F S))›
     apply (rule backjump.intros[of S F' K F _ L])
     using ‹F ⊨as CNot C'› C_cls_S tr_S_CNot_C undef T distinct not_tauto D cond clss_C atm_L
     by (auto simp: tr_S)
   moreover have ‹T ∼ (add_clsNOT D ?S')›
     using T by (auto simp: tr_S state_eqNOT_def simp del: state_simpNOT)
   ultimately show ?thesis
     using D clss_C by blast
qed

lemma cdclNOT_merged_bj_learn_is_tranclp_cdclNOT:
  ‹cdclNOT_merged_bj_learn S T ⟹ inv S ⟹ cdclNOT++ S T›
proof (induction rule: cdclNOT_merged_bj_learn.induct)
  case (cdclNOT_merged_bj_learn_decideNOT T)
  then have ‹cdclNOT S T›
    using bj_decideNOT cdclNOT.simps by fastforce
  then show ?case by auto
next
  case (cdclNOT_merged_bj_learn_propagateNOT T)
  then have ‹cdclNOT S T›
    using bj_propagateNOT cdclNOT.simps by fastforce
  then show ?case by auto
next
   case (cdclNOT_merged_bj_learn_forgetNOT T)
   then have ‹cdclNOT S T›
     using c_forgetNOT by blast
   then show ?case by auto
next
   case (cdclNOT_merged_bj_learn_backjump_l T) note bt = this(1) and inv = this(2)
   obtain C' :: ‹'v clause› and L :: ‹'v literal› and D :: ‹'v clause› where
     f3: ‹learn S (add_clsNOT D S) ∧
       backjump (add_clsNOT D S) T ∧
       atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S)› and
     D: ‹D = add_mset L C'›
     using backjump_l_learn_backjump[OF bt inv] by blast
   then have f4: ‹cdclNOT S (add_clsNOT D S)›
     using c_learn by blast
   have ‹cdclNOT (add_clsNOT D S) T›
     using f3 bj_backjump c_dpll_bj by blast
   then show ?case
     using f4 by (meson tranclp.r_into_trancl tranclp.trancl_into_trancl)
qed

lemma rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv:
  ‹cdclNOT_merged_bj_learn** S T ⟹ inv S ⟹ cdclNOT** S T ∧ inv T›
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)[OF this(4-)] and
    inv = this(4)
  have ‹cdclNOT** T U›
    using cdclNOT_merged_bj_learn_is_tranclp_cdclNOT[OF cdclNOT] IH
     inv by auto
  then have ‹cdclNOT** S U› using IH by fastforce
  moreover have ‹inv U› using IH cdclNOT cdcl_merged_inv inv by blast
  ultimately show ?case using st by fast
qed

lemma rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT:
  ‹cdclNOT_merged_bj_learn** S T ⟹ inv S ⟹ cdclNOT** S T›
  using rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv by blast

lemma rtranclp_cdclNOT_merged_bj_learn_inv:
  ‹cdclNOT_merged_bj_learn** S T ⟹ inv S ⟹ inv T›
  using rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv by blast

lemma rtranclp_cdclNOT_merged_bj_learn_no_dup_inv:
  ‹cdclNOT_merged_bj_learn** S T ⟹ no_dup (trail S) ⟹ no_dup (trail T)›
  by (induction rule: rtranclp_induct) (auto simp: cdclNOT_merged_bj_learn_no_dup_inv)

definition μC' :: ‹'v clause set ⇒ 'st ⇒ nat› where
‹μC' A T ≡ μC (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)›

definition μCDCL'_merged :: ‹'v clause set ⇒ 'st ⇒ nat› where
‹μCDCL'_merged A T ≡
  ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μC' A T) * 2 + card (set_mset (clausesNOT T))›

lemma cdclNOT_decreasing_measure':
  assumes
    ‹cdclNOT_merged_bj_learn S T› and
    inv: ‹inv S› and
    atm_clss: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atm_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    fin_A: ‹finite A›
  shows ‹μCDCL'_merged A T < μCDCL'_merged A S›
  using assms(1)
proof induction
  case (cdclNOT_merged_bj_learn_decideNOT T)
  have ‹clausesNOT S = clausesNOT T›
    using cdclNOT_merged_bj_learn_decideNOT.hyps by auto
  moreover have
    ‹(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
       - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
     < (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
       - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)›
    apply (rule dpll_bj_trail_mes_decreasing_prop)
    using cdclNOT_merged_bj_learn_decideNOT fin_A atm_clss atm_trail n_d inv
    by (simp_all add: bj_decideNOT cdclNOT_merged_bj_learn_decideNOT.hyps)
  ultimately show ?case
    unfolding μCDCL'_merged_def μC'_def by simp
next
  case (cdclNOT_merged_bj_learn_propagateNOT T)
  have ‹clausesNOT S = clausesNOT T›
    using cdclNOT_merged_bj_learn_propagateNOT.hyps
    by (simp add: bj_propagateNOT inv dpll_bj_clauses)
  moreover have
    ‹(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
       - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
     < (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
       - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)›
    apply (rule dpll_bj_trail_mes_decreasing_prop)
    using inv n_d atm_clss atm_trail fin_A by (simp_all add: bj_propagateNOT
      cdclNOT_merged_bj_learn_propagateNOT.hyps)
  ultimately show ?case
    unfolding μCDCL'_merged_def μC'_def by simp
next
  case (cdclNOT_merged_bj_learn_forgetNOT T)
  have ‹card (set_mset (clausesNOT T)) < card (set_mset (clausesNOT S))›
    using ‹forgetNOT S T› by (metis card_Diff1_less clauses_remove_clsNOT finite_set_mset
      forgetNOT.cases linear set_mset_minus_replicate_mset(1) state_eqNOT_def)
  moreover
    have ‹trail S = trail T›
      using ‹forgetNOT S T› by (auto elim: forgetNOTE)
    then have
      ‹(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
        - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
 = (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
        - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)›
       by auto
  ultimately show ?case
    unfolding μCDCL'_merged_def μC'_def by simp
next
  case (cdclNOT_merged_bj_learn_backjump_l T) note bj_l = this(1)
  obtain C' L D S' where
    learn: ‹learn S' T› and
    bj: ‹backjump S S'› and
    atms_C: ‹atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
    D: ‹D = add_mset L C'› and
    T: ‹T ∼ add_clsNOT D S'›
    using bj_l inv backjump_l_backjump_learn [of S] n_d atm_clss atm_trail by blast
  have card_T_S: ‹card (set_mset (clausesNOT T)) ≤ 1+ card (set_mset (clausesNOT S))›
    using bj_l inv by (force elim!: backjump_lE simp: card_insert_if)
  have tr_S_T: ‹trail_weight S' = trail_weight T›
    using T by auto
  have
    ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
      - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S'))
    < ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
      - μC (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A))
           (trail_weight S))›
    apply (rule dpll_bj_trail_mes_decreasing_prop)
         using bj bj_backjump apply blast
        using inv apply blast
       using atms_C atm_clss atm_trail D apply (simp add: n_d; fail)
      using atm_trail n_d apply (simp; fail)
     apply (simp add: n_d; fail)
    using fin_A apply (simp; fail)
    done
  then show ?case
    using card_T_S unfolding μCDCL'_merged_def μC'_def tr_S_T by linarith
qed

lemma wf_cdclNOT_merged_bj_learn:
  assumes
    fin_A: ‹finite A›
  shows ‹wf {(T, S).
    (inv S ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S))
    ∧ cdclNOT_merged_bj_learn S T}›
  apply (rule wfP_if_measure[of _ _ ‹μCDCL'_merged A›])
  using cdclNOT_decreasing_measure' fin_A by simp

lemma in_atms_neg_defined: ‹x ∈ atms_of C' ⟹ F ⊨as CNot C' ⟹ x ∈ atm_of ` lits_of_l F›
  by (metis (no_types, lifting) atms_of_def imageE true_annots_CNot_all_atms_defined)

lemma cdclNOT_merged_bj_learn_atms_of_ms_clauses_decreasing:
  assumes ‹cdclNOT_merged_bj_learn S T›and ‹inv S›
  shows ‹atms_of_mm (clausesNOT T) ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))›
  using assms
  apply (induction rule: cdclNOT_merged_bj_learn.induct)
      prefer 4 apply (auto dest!: dpll_bj_atms_of_ms_clauses_inv set_mp
        simp add: atms_of_ms_def Union_eq
        elim!: decideNOTE propagateNOTE forgetNOTE)[3]
  apply (elim backjump_lE)
  by (auto dest!: in_atms_neg_defined simp del:)

lemma cdclNOT_merged_bj_learn_atms_in_trail_in_set:
  assumes
    ‹cdclNOT_merged_bj_learn S T› and ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ A› and
    ‹atm_of ` (lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A›
  using assms
  apply (induction rule: cdclNOT_merged_bj_learn.induct)
      apply (meson bj_decideNOT dpll_bj_atms_in_trail_in_set)
     apply (meson bj_propagateNOT dpll_bj_atms_in_trail_in_set)
    defer
    apply (metis forgetNOTE state_eqNOT_trail trail_remove_clsNOT)
  by (metis (no_types, lifting) backjump_l_backjump_learn bj_backjump dpll_bj_atms_in_trail_in_set
      state_eqNOT_trail trail_add_clsNOT)

lemma rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound:
  assumes
    cdcl: ‹cdclNOT_merged_bj_learn** S T› and
    inv: ‹inv S› and
    atms_clauses_S: ‹atms_of_mm (clausesNOT S) ⊆ A› and
    atms_trail_S: ‹atm_of `(lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A ∧ atms_of_mm (clausesNOT T) ⊆ A›
  using cdcl
proof (induction rule: rtranclp_induct)
  case base
  then show ?case using atms_clauses_S atms_trail_S by simp
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)
  have ‹inv T› using inv st rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv by blast
  then have ‹atms_of_mm (clausesNOT U) ⊆ A›
    using cdclNOT_merged_bj_learn_atms_of_ms_clauses_decreasing cdclNOT IH ‹inv T› by fast
  moreover
    have ‹atm_of `(lits_of_l (trail U)) ⊆ A›
      using cdclNOT_merged_bj_learn_atms_in_trail_in_set[of _ _ A] ‹inv T› cdclNOT step.IH by auto
  ultimately show ?case by fast
qed

lemma cdclNOT_merged_bj_learn_trail_clauses_bound:
  assumes
    cdcl: ‹cdclNOT_merged_bj_learn S T› and
    inv: ‹inv S› and
    atms_clauses_S: ‹atms_of_mm (clausesNOT S) ⊆ A› and
    atms_trail_S: ‹atm_of `(lits_of_l (trail S)) ⊆ A›
  shows ‹atm_of ` (lits_of_l (trail T)) ⊆ A ∧ atms_of_mm (clausesNOT T) ⊆ A›
  using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[of S T] assms by auto

lemma tranclp_cdclNOT_cdclNOT_tranclp:
  assumes
    ‹cdclNOT_merged_bj_learn++ S T› and
    inv: ‹inv S› and
    atm_clss: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atm_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    fin_A[simp]: ‹finite A›
  shows ‹(T, S) ∈ {(T, S).
    (inv S ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S))
    ∧ cdclNOT_merged_bj_learn S T}+› (is ‹_ ∈ ?P+›)
  using assms(1)
proof (induction rule: tranclp_induct)
  case base
  then show ?case using n_d atm_clss atm_trail inv by auto
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)
  have st: ‹cdclNOT_merged_bj_learn** S T›
    using [[simp_trace]]
    by (simp add: rtranclp_unfold st)
  have ‹cdclNOT** S T›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT)
    using st cdclNOT inv n_d atm_clss atm_trail inv by auto
  have ‹inv T›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_inv)
      using inv st cdclNOT n_d atm_clss atm_trail inv by auto
  moreover have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st inv atm_clss atm_trail]
    by fast
  moreover have ‹atm_of ` (lits_of_l (trail T))⊆ atms_of_ms A›
    using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st inv atm_clss atm_trail]
    by fast
  moreover have ‹no_dup (trail T)›
    using rtranclp_cdclNOT_merged_bj_learn_no_dup_inv[OF st n_d] by fast
  ultimately have ‹(U, T) ∈ ?P›
    using cdclNOT by auto
  then show ?case using IH by (simp add: trancl_into_trancl2)
qed

lemma wf_tranclp_cdclNOT_merged_bj_learn:
  assumes ‹finite A›
  shows ‹wf {(T, S).
    (inv S ∧ atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A
    ∧ no_dup (trail S))
    ∧ cdclNOT_merged_bj_learn++ S T}›
  apply (rule wf_subset)
   apply (rule wf_trancl[OF wf_cdclNOT_merged_bj_learn])
   using assms apply simp
  using tranclp_cdclNOT_cdclNOT_tranclp[OF _ _ _ _ _ ‹finite A›] by auto

lemma cdclNOT_merged_bj_learn_final_state:
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    n_s: ‹no_step cdclNOT_merged_bj_learn S› and
    atms_S: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    ‹finite A› and
    inv: ‹inv S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT S))
    ∨ (trail S ⊨asm clausesNOT S ∧ satisfiable (set_mset (clausesNOT S)))›
proof -
  let ?N = ‹set_mset (clausesNOT S)›
  let ?M = ‹trail S›
  consider
      (sat) ‹satisfiable ?N› and ‹?M ⊨as ?N›
    | (sat') ‹satisfiable ?N› and ‹¬ ?M ⊨as ?N›
    | (unsat) ‹unsatisfiable ?N›
    by auto
  then show ?thesis
    proof cases
      case sat' note sat = this(1) and M = this(2)
      obtain C where ‹C ∈ ?N› and ‹¬?M ⊨a C› using M unfolding true_annots_def by auto
      obtain I :: ‹'v literal set› where
        ‹I ⊨s ?N› and
        cons: ‹consistent_interp I› and
        tot: ‹total_over_m I ?N› and
        atm_I_N: ‹atm_of `I ⊆ atms_of_ms ?N›
        using sat unfolding satisfiable_def_min by auto
      let ?I = ‹I ∪ {P| P. P ∈ lits_of_l ?M ∧ atm_of P ∉ atm_of ` I}›
      let ?O = ‹{unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
      have cons_I': ‹consistent_interp ?I›
        using cons using ‹no_dup ?M› unfolding consistent_interp_def
        by (auto simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set lits_of_def
          dest!: no_dup_cannot_not_lit_and_uminus)
      have tot_I': ‹total_over_m ?I (?N ∪ unmark_l ?M)›
        using tot atms_of_s_def unfolding total_over_m_def total_over_set_def
        by (fastforce simp: image_iff)
      have ‹{P |P. P ∈ lits_of_l ?M ∧ atm_of P ∉ atm_of ` I} ⊨s ?O›
        using ‹I⊨s ?N› atm_I_N by (auto simp add: atm_of_eq_atm_of true_clss_def lits_of_def)
      then have I'_N: ‹?I ⊨s ?N ∪ ?O›
        using ‹I⊨s ?N› true_clss_union_increase by force
      have tot': ‹total_over_m ?I (?N∪?O)›
        using atm_I_N tot unfolding total_over_m_def total_over_set_def
        by (force simp: lits_of_def elim!: is_decided_ex_Decided)

      have atms_N_M: ‹atms_of_ms ?N ⊆ atm_of ` lits_of_l ?M›
        proof (rule ccontr)
          assume ‹¬ ?thesis›
          then obtain l :: 'v where
            l_N: ‹l ∈ atms_of_ms ?N› and
            l_M: ‹l ∉ atm_of ` lits_of_l ?M›
            by auto
          have ‹undefined_lit ?M (Pos l)›
            using l_M by (metis Decided_Propagated_in_iff_in_lits_of_l
              atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1))
          then show False
            using can_propagate_or_decide_or_backjump_l[of ‹Pos l› S] l_N
            cdclNOT_merged_bj_learn_decideNOT n_s inv sat
            by (auto dest!: cdclNOT_merged_bj_learn.intros)
        qed

      have ‹?M ⊨as CNot C›
      apply (rule all_variables_defined_not_imply_cnot)
        using atms_N_M ‹C ∈ ?N› ‹¬ ?M ⊨a C› atms_of_atms_of_ms_mono[OF ‹C ∈ ?N›]
        by (auto dest: atms_of_atms_of_ms_mono)
      have ‹∃l ∈ set ?M. is_decided l›
        proof (rule ccontr)
          let ?O = ‹{unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
          have θ[iff]: ‹⋀I. total_over_m I (?N ∪ ?O ∪ unmark_l ?M)
            ⟷ total_over_m I (?N ∪unmark_l ?M)›
            unfolding total_over_set_def total_over_m_def atms_of_ms_def by blast
          assume ‹¬ ?thesis›
          then have [simp]:‹{unmark L |L. is_decided L ∧ L ∈ set ?M}
   = {unmark L |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}›
            by auto
          then have ‹?N ∪ ?O ⊨ps unmark_l ?M›
            using all_decomposition_implies_propagated_lits_are_implied[OF decomp] by auto

          then have ‹?I ⊨s unmark_l ?M›
            using cons_I' I'_N tot_I' ‹?I ⊨s ?N ∪ ?O› unfolding θ true_clss_clss_def by blast
          then have ‹lits_of_l ?M ⊆ ?I›
            unfolding true_clss_def lits_of_def by auto
          then have ‹?M ⊨as ?N›
            using I'_N ‹C ∈ ?N› ‹¬ ?M ⊨a C› cons_I' atms_N_M
            by (meson ‹trail S ⊨as CNot C› consistent_CNot_not rev_subsetD sup_ge1 true_annot_def
              true_annots_def true_cls_mono_set_mset_l true_clss_def)
          then show False using M by fast
        qed
      from List.split_list_first_propE[OF this] obtain K :: ‹'v literal› and d :: unit and
        F F' :: ‹('v, unit) ann_lits› where
        M_K: ‹?M = F' @ Decided K # F› and
        nm: ‹∀f∈set F'. ¬is_decided f›
        by (metis (full_types) is_decided_ex_Decided old.unit.exhaust)
      let ?K = ‹Decided K::('v, unit) ann_lit›
      have ‹?K ∈ set ?M›
        unfolding M_K by auto
      let ?C = ‹image_mset lit_of {#L∈#mset ?M. is_decided L ∧ L≠?K#} :: 'v clause›
      let ?C' = ‹set_mset (image_mset (λL::'v literal. {#L#}) (?C + unmark ?K))›
      have ‹?N ∪ {unmark L |L. is_decided L ∧ L ∈ set ?M} ⊨ps unmark_l ?M›
        using all_decomposition_implies_propagated_lits_are_implied[OF decomp] .
      moreover have C': ‹?C' = {unmark L |L. is_decided L ∧ L ∈ set ?M}›
        unfolding M_K apply standard
          apply force
        by auto
      ultimately have N_C_M: ‹?N ∪ ?C' ⊨ps unmark_l ?M›
        by auto
      have N_M_False: ‹?N ∪ (λL. unmark L) ` (set ?M) ⊨ps {{#}}›
        unfolding true_clss_clss_def true_annots_def Ball_def true_annot_def
      proof (intro allI impI)
        fix LL :: "'v literal set"
        assume
          tot: ‹total_over_m LL (set_mset (clausesNOT S) ∪ unmark_l (trail S) ∪ {{#}})› and
          cons: ‹consistent_interp LL› and
          LL: ‹LL ⊨s set_mset (clausesNOT S) ∪ unmark_l (trail S)›
        have ‹total_over_m LL (CNot C)›
          by (metis ‹C ∈# clausesNOT S› insert_absorb tot total_over_m_CNot_toal_over_m
              total_over_m_insert total_over_m_union)
        then have "total_over_m LL (unmark_l (trail S) ∪ CNot C)"
          using tot by force
        then show "LL ⊨s {{#}}"
          using tot cons LL
          by (metis (no_types) ‹C ∈# clausesNOT S› ‹trail S ⊨as CNot C› consistent_CNot_not
              true_annots_true_clss_clss true_clss_clss_def true_clss_def true_clss_union)
      qed

      have ‹undefined_lit F K› using ‹no_dup ?M› unfolding M_K by (auto simp: defined_lit_map)
      moreover {
        have ‹?N ∪ ?C' ⊨ps {{#}}›
          proof -
            have A: ‹?N ∪ ?C' ∪ unmark_l ?M = ?N ∪ unmark_l ?M›
              unfolding M_K by auto
            show ?thesis
              using true_clss_clss_left_right[OF N_C_M, of ‹{{#}}›] N_M_False unfolding A by auto
          qed
        have ‹?N ⊨p image_mset uminus ?C + {#-K#}›
          unfolding true_clss_cls_def true_clss_clss_def total_over_m_def
          proof (intro allI impI)
            fix I
            assume
              tot: ‹total_over_set I (atms_of_ms (?N ∪ {image_mset uminus ?C+ {#- K#}}))› and
              cons: ‹consistent_interp I› and
              ‹I ⊨s ?N›
            have ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
              using cons tot unfolding consistent_interp_def by (cases K) auto
            have ‹{a ∈ set (trail S). is_decided a ∧ a ≠ Decided K} =
             set (trail S) ∩ {L. is_decided L ∧ L ≠ Decided K}›
             by auto
            then have tot': ‹total_over_set I
               (atm_of ` lit_of ` (set ?M ∩ {L. is_decided L ∧ L ≠ Decided K}))›
              using tot by (auto simp add: atms_of_uminus_lit_atm_of_lit_of)
            { fix x :: ‹('v, unit) ann_lit›
              assume
                a3: ‹lit_of x ∉ I› and
                a1: ‹x ∈ set ?M› and
                a4: ‹is_decided x› and
                a5: ‹x ≠ Decided K›
              then have ‹Pos (atm_of (lit_of x)) ∈ I ∨ Neg (atm_of (lit_of x)) ∈ I›
                using a5 a4 tot' a1 unfolding total_over_set_def atms_of_s_def by blast
              moreover have f6: ‹Neg (atm_of (lit_of x)) = - Pos (atm_of (lit_of x))›
                by simp
              ultimately have ‹- lit_of x ∈ I›
                using f6 a3 by (metis (no_types) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
                  literal.sel(1))
            } note H = this

            have ‹¬I ⊨s ?C'›
              using ‹?N ∪ ?C' ⊨ps {{#}}› tot cons ‹I ⊨s ?N›
              unfolding true_clss_clss_def total_over_m_def
              by (simp add: atms_of_uminus_lit_atm_of_lit_of atms_of_ms_single_image_atm_of_lit_of)
            then show ‹I ⊨ image_mset uminus ?C + {#- K#}›
              unfolding true_clss_def true_cls_def Bex_def
              using ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
              by (auto dest!: H)
          qed }
      moreover have ‹F ⊨as CNot (image_mset uminus ?C)›
        using nm unfolding true_annots_def CNot_def M_K by (auto simp add: lits_of_def)
      ultimately have False
        using bj_merge_can_jump[of S F' K F C ‹-K›
          ‹image_mset uminus (image_mset lit_of {# L :# mset ?M. is_decided L ∧ L ≠ Decided K#})›]
          ‹C∈?N› n_s ‹?M ⊨as CNot C› bj_backjump inv sat unfolding M_K
          by (auto simp: cdclNOT_merged_bj_learn.simps)
        then show ?thesis by fast
    qed auto
qed

lemma cdclNOT_merged_bj_learn_all_decomposition_implies:
  assumes ‹cdclNOT_merged_bj_learn S T› and inv: ‹inv S›
    ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows
    ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
    using assms
proof (induction rule: cdclNOT_merged_bj_learn.induct)
  case (cdclNOT_merged_bj_learn_backjump_l T) note bj_l = this(1)
  obtain C' L D S' where
    learn: ‹learn S' T› and
    bj: ‹backjump S S'› and
    atms_C: ‹atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
    D: ‹D = add_mset L C'› and
    T: ‹T ∼ add_clsNOT D S'›
    using bj_l inv backjump_l_backjump_learn [of S] by blast
  have ‹all_decomposition_implies_m (clausesNOT S') (get_all_ann_decomposition (trail S'))›
    using bj bj_backjump dpll_bj_clauses inv(1) inv(2)
    by (fastforce simp: dpll_bj_all_decomposition_implies_inv)
  then show ?case
    using T by (auto simp: all_decomposition_implies_insert_single)
qed (auto simp: dpll_bj_all_decomposition_implies_inv cdclNOT_all_decomposition_implies
    dest!: dpll_bj.intros cdclNOT.intros)

lemma rtranclp_cdclNOT_merged_bj_learn_all_decomposition_implies:
  assumes ‹cdclNOT_merged_bj_learn** S T› and inv: ‹inv S›
    ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows
    ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
  using assms
  apply (induction rule: rtranclp_induct)
    apply simp
  using cdclNOT_merged_bj_learn_all_decomposition_implies
    rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv by blast

lemma full_cdclNOT_merged_bj_learn_final_state:
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    full: ‹full cdclNOT_merged_bj_learn S T› and
    atms_S: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    ‹finite A› and
    inv: ‹inv S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT T))
    ∨ (trail T ⊨asm clausesNOT T ∧ satisfiable (set_mset (clausesNOT T)))›
proof -
  have st: ‹cdclNOT_merged_bj_learn** S T› and n_s: ‹no_step cdclNOT_merged_bj_learn T›
    using full unfolding full_def by blast+
  then have st': ‹cdclNOT** S T›
    using inv rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv n_d by auto
  have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A› and ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st inv atms_S atms_trail] by blast+
  moreover have ‹no_dup (trail T)›
    using rtranclp_cdclNOT_merged_bj_learn_no_dup_inv inv n_d st by blast
  moreover have ‹inv T›
    using rtranclp_cdclNOT_merged_bj_learn_inv inv st by blast
  moreover have ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
    using rtranclp_cdclNOT_merged_bj_learn_all_decomposition_implies inv st decomp n_d by blast
  ultimately show ?thesis
    using cdclNOT_merged_bj_learn_final_state[of T A] ‹finite A› n_s by fast
qed

end

subsection ‹Instantiations›
text ‹In this section, we instantiate the previous locales to ensure that the assumption are not
  contradictory.›
locale cdclNOT_with_backtrack_and_restarts =
  conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt
    trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    inv decide_conds backjump_conds propagate_conds learn_restrictions forget_restrictions
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    inv :: ‹'st ⇒ bool› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    backjump_conds :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    learn_restrictions forget_restrictions :: ‹'v clause ⇒ 'st ⇒ bool›
    +
  fixes f :: ‹nat ⇒ nat›
  assumes
    unbounded: ‹unbounded f› and f_ge_1: ‹⋀n. n ≥ 1 ⟹ f n ≥ 1› and
    inv_restart:‹⋀S T. inv S ⟹ T ∼ reduce_trail_toNOT ([]::'a list) S ⟹ inv T›
begin

lemma bound_inv_inv:
  assumes
    ‹inv S› and
    n_d: ‹no_dup (trail S)› and
    atms_clss_S_A: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail_S_A:‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    ‹finite A› and
    cdclNOT: ‹cdclNOT S T›
  shows
    ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A› and
    ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A› and
    ‹finite A›
proof -
  have ‹cdclNOT S T›
    using ‹inv S› cdclNOT by linarith
  then have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` lits_of_l (trail S)›
    using ‹inv S›
    by (meson conflict_driven_clause_learning_ops.cdclNOT_atms_of_ms_clauses_decreasing
      conflict_driven_clause_learning_ops_axioms n_d)
  then show ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    using atms_clss_S_A atms_trail_S_A by blast
next
  show ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
    by (meson ‹inv S› atms_clss_S_A atms_trail_S_A cdclNOT cdclNOT_atms_in_trail_in_set n_d)
next
  show ‹finite A›
    using ‹finite A› by simp
qed

sublocale cdclNOT_increasing_restarts_ops ‹λS T. T ∼ reduce_trail_toNOT ([]::'a list) S› cdclNOT f
  ‹λA S. atms_of_mm (clausesNOT S) ⊆ atms_of_ms A ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧
  finite A›
  μCDCL' ‹λS. inv S ∧ no_dup (trail S)›
  μCDCL'_bound
  apply unfold_locales
           apply (simp add: unbounded)
          using f_ge_1 apply force
         using bound_inv_inv apply meson
        apply (rule cdclNOT_decreasing_measure'; simp)
        apply (rule rtranclp_cdclNOT_μCDCL'_bound; simp)
       apply (rule rtranclp_μCDCL'_bound_decreasing; simp)
      apply auto[]
    apply auto[]
   using cdclNOT_inv cdclNOT_no_dup apply blast
  using inv_restart apply auto[]
  done

lemma cdclNOT_with_restart_μCDCL'_le_μCDCL'_bound:
  assumes
    cdclNOT: ‹cdclNOT_restart (T, a) (V, b)› and
    cdclNOT_inv:
      ‹inv T›
      ‹no_dup (trail T)› and
    bound_inv:
      ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
      ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
      ‹finite A›
  shows ‹μCDCL' A V ≤ μCDCL'_bound A T›
  using cdclNOT_inv bound_inv
proof (induction rule: cdclNOT_with_restart_induct[OF cdclNOT])
  case (1 m S T n U) note U = this(3)
  show ?case
    apply (rule rtranclp_cdclNOT_μCDCL'_bound_reduce_trail_toNOT[of S T])
         using ‹(cdclNOT ^^ m) S T› apply (fastforce dest!: relpowp_imp_rtranclp)
        using 1 by auto
next
  case (2 S T n) note full = this(2)
  show ?case
    apply (rule rtranclp_cdclNOT_μCDCL'_bound)
    using full 2 unfolding full1_def by force+
qed

lemma cdclNOT_with_restart_μCDCL'_bound_le_μCDCL'_bound:
  assumes
    cdclNOT: ‹cdclNOT_restart (T, a) (V, b)› and
    cdclNOT_inv:
      ‹inv T›
      ‹no_dup (trail T)› and
    bound_inv:
      ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
      ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
      ‹finite A›
  shows ‹μCDCL'_bound A V ≤ μCDCL'_bound A T›
  using cdclNOT_inv bound_inv
proof (induction rule: cdclNOT_with_restart_induct[OF cdclNOT])
  case (1 m S T n U) note U = this(3)
  have ‹μCDCL'_bound A T ≤ μCDCL'_bound A S›
     apply (rule rtranclp_μCDCL'_bound_decreasing)
         using ‹(cdclNOT ^^ m) S T› apply (fastforce dest: relpowp_imp_rtranclp)
        using 1 by auto
  then show ?case using U unfolding μCDCL'_bound_def by auto
next
  case (2 S T n) note full = this(2)
  show ?case
    apply (rule rtranclp_μCDCL'_bound_decreasing)
    using full 2 unfolding full1_def by force+
qed

sublocale cdclNOT_increasing_restarts _ _ _ _ _ _
    f
   (* restart *) ‹λS T. T ∼ reduce_trail_toNOT ([]::'a list) S›
   (* bound_inv *)‹λA S. atms_of_mm (clausesNOT S) ⊆ atms_of_ms A
     ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧ finite A›
   μCDCL' cdclNOT
   (* inv *) ‹λS. inv S ∧ no_dup (trail S)›
   μCDCL'_bound
  apply unfold_locales
   using cdclNOT_with_restart_μCDCL'_le_μCDCL'_bound apply simp
  using cdclNOT_with_restart_μCDCL'_bound_le_μCDCL'_bound apply simp
  done

lemma cdclNOT_restart_all_decomposition_implies:
  assumes ‹cdclNOT_restart S T› and
    ‹inv (fst S)› and
    ‹no_dup (trail (fst S))›
    ‹all_decomposition_implies_m (clausesNOT (fst S)) (get_all_ann_decomposition (trail (fst S)))›
  shows
    ‹all_decomposition_implies_m (clausesNOT (fst T)) (get_all_ann_decomposition (trail (fst T)))›
  using assms apply (induction)
  using rtranclp_cdclNOT_all_decomposition_implies by (auto dest!: tranclp_into_rtranclp
    simp: full1_def)

lemma rtranclp_cdclNOT_restart_all_decomposition_implies:
  assumes ‹cdclNOT_restart** S T› and
    inv: ‹inv (fst S)› and
    n_d: ‹no_dup (trail (fst S))› and
    decomp:
      ‹all_decomposition_implies_m (clausesNOT (fst S)) (get_all_ann_decomposition (trail (fst S)))›
  shows
    ‹all_decomposition_implies_m (clausesNOT (fst T)) (get_all_ann_decomposition (trail (fst T)))›
  using assms(1)
proof (induction rule: rtranclp_induct)
  case base
  then show ?case using decomp by simp
next
  case (step T u) note st = this(1) and r = this(2) and IH = this(3)
  have ‹inv (fst T)›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv[OF st] inv n_d by blast
  moreover have ‹no_dup (trail (fst T))›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv[OF st] inv n_d by blast
  ultimately show ?case
    using cdclNOT_restart_all_decomposition_implies r IH n_d by fast
qed

lemma cdclNOT_restart_sat_ext_iff:
  assumes
    st: ‹cdclNOT_restart S T› and
    n_d: ‹no_dup (trail (fst S))› and
    inv: ‹inv (fst S)›
  shows ‹I ⊨sextm clausesNOT (fst S) ⟷ I ⊨sextm clausesNOT (fst T)›
  using assms
proof (induction)
  case (restart_step m S T n U)
  then show ?case
    using rtranclp_cdclNOT_bj_sat_ext_iff n_d by (fastforce dest!: relpowp_imp_rtranclp)
next
  case restart_full
  then show ?case using rtranclp_cdclNOT_bj_sat_ext_iff unfolding full1_def
  by (fastforce dest!: tranclp_into_rtranclp)
qed

lemma rtranclp_cdclNOT_restart_sat_ext_iff:
  fixes S T :: ‹'st × nat›
  assumes
    st: ‹cdclNOT_restart** S T› and
    n_d: ‹no_dup (trail (fst S))› and
    inv: ‹inv (fst S)›
  shows ‹I ⊨sextm clausesNOT (fst S) ⟷ I ⊨sextm clausesNOT (fst T)›
  using st
proof (induction)
  case base
  then show ?case by simp
next
  case (step T U) note st = this(1) and r = this(2) and IH = this(3)
  have ‹inv (fst T)›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv[OF st] inv n_d by blast+
  moreover have ‹no_dup (trail (fst T))›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv rtranclp_cdclNOT_no_dup st inv n_d by blast
  ultimately show ?case
    using cdclNOT_restart_sat_ext_iff[OF r] IH by blast
qed

theorem full_cdclNOT_restart_backjump_final_state:
  fixes A :: ‹'v clause set› and S T :: ‹'st›
  assumes
    full: ‹full cdclNOT_restart (S, n) (T, m)› and
    atms_S: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A› and
    n_d: ‹no_dup (trail S)› and
    fin_A[simp]: ‹finite A› and
    inv: ‹inv S› and
    decomp: ‹all_decomposition_implies_m (clausesNOT S) (get_all_ann_decomposition (trail S))›
  shows ‹unsatisfiable (set_mset (clausesNOT S))
    ∨ (lits_of_l (trail T) ⊨sextm clausesNOT S ∧ satisfiable (set_mset (clausesNOT S)))›
proof -
  have st: ‹cdclNOT_restart** (S, n) (T, m)› and
    n_s: ‹no_step cdclNOT_restart (T, m)›
    using full unfolding full_def by fast+
  have binv_T: ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_with_restart_bound_inv[OF st, of A] inv n_d atms_S atms_trail
    by auto
  moreover have inv_T: ‹no_dup (trail T)› ‹inv T›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv[OF st] inv n_d by auto
  moreover have ‹all_decomposition_implies_m (clausesNOT T) (get_all_ann_decomposition (trail T))›
    using rtranclp_cdclNOT_restart_all_decomposition_implies[OF st] inv n_d
    decomp by auto
  ultimately have T: ‹unsatisfiable (set_mset (clausesNOT T))
    ∨ (trail T ⊨asm clausesNOT T ∧ satisfiable (set_mset (clausesNOT T)))›
    using no_step_cdclNOT_restart_no_step_cdclNOT[of ‹(T, m)› A] n_s
    cdclNOT_final_state[of T A] unfolding cdclNOT_NOT_all_inv_def by auto
  have eq_sat_S_T:‹⋀I. I ⊨sextm clausesNOT S ⟷ I ⊨sextm clausesNOT T›
    using rtranclp_cdclNOT_restart_sat_ext_iff[OF st] inv n_d atms_S
        atms_trail by auto
  have cons_T: ‹consistent_interp (lits_of_l (trail T))›
    using inv_T(1) distinct_consistent_interp by blast
  consider
      (unsat) ‹unsatisfiable (set_mset (clausesNOT T))›
    | (sat) ‹trail T ⊨asm clausesNOT T› and ‹satisfiable (set_mset (clausesNOT T))›
    using T by blast
  then show ?thesis
    proof cases
      case unsat
      then have ‹unsatisfiable (set_mset (clausesNOT S))›
        using eq_sat_S_T consistent_true_clss_ext_satisfiable true_clss_imp_true_cls_ext
        unfolding satisfiable_def by blast
      then show ?thesis by fast
    next
      case sat
      then have ‹lits_of_l (trail T) ⊨sextm clausesNOT S›
        using rtranclp_cdclNOT_restart_sat_ext_iff[OF st] inv n_d atms_S
        atms_trail by (auto simp: true_clss_imp_true_cls_ext true_annots_true_cls)
      moreover then have ‹satisfiable (set_mset (clausesNOT S))›
          using cons_T consistent_true_clss_ext_satisfiable by blast
      ultimately show ?thesis by blast
    qed
qed
end ― ‹End of the locale @{locale cdclNOT_with_backtrack_and_restarts}.›

text ‹The restart does only reset the trail, contrary to Weidenbach's version where
  forget and restart are always combined. But there is a forget rule.›
locale cdclNOT_merge_bj_learn_with_backtrack_restarts =
  cdclNOT_merge_bj_learn trail clausesNOT prepend_trail tl_trail add_clsNOT remove_clsNOT
    decide_conds propagate_conds forget_conds
    ‹λC C' L' S T. distinct_mset C' ∧ L' ∉# C' ∧ backjump_l_cond C C' L' S T› inv
  for
    trail :: ‹'st ⇒ ('v, unit) ann_lits› and
    clausesNOT :: ‹'st ⇒ 'v clauses› and
    prepend_trail :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒'st› and
    add_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_clsNOT :: ‹'v clause ⇒ 'st ⇒ 'st› and
    decide_conds :: ‹'st ⇒ 'st ⇒ bool› and
    propagate_conds :: ‹('v, unit) ann_lit ⇒ 'st ⇒ 'st ⇒ bool› and
    inv :: ‹'st ⇒ bool› and
    forget_conds :: ‹'v clause ⇒ 'st ⇒ bool› and
    backjump_l_cond :: ‹'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool›
    +
  fixes f :: ‹nat ⇒ nat›
  assumes
    unbounded: ‹unbounded f› and f_ge_1: ‹⋀n. n ≥ 1 ⟹ f n ≥ 1› and
    inv_restart:‹⋀S T. inv S ⟹ T ∼ reduce_trail_toNOT [] S ⟹ inv T›
begin

definition not_simplified_cls :: ‹'b clause multiset ⇒ 'b clauses›
where
‹not_simplified_cls A ≡ {#C ∈# A. C ∉ simple_clss (atms_of_mm A)#}›

lemma not_simplified_cls_tautology_distinct_mset:
  ‹not_simplified_cls A = {#C ∈# A. tautology C ∨ ¬distinct_mset C#}›
  unfolding not_simplified_cls_def by (rule filter_mset_cong) (auto simp: simple_clss_def)

lemma simple_clss_or_not_simplified_cls:
  assumes ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹x ∈# clausesNOT S› and ‹finite A›
  shows ‹x ∈ simple_clss (atms_of_ms A) ∨ x ∈# not_simplified_cls (clausesNOT S)›
proof -
  consider
      (simpl) ‹¬tautology x› and ‹distinct_mset x›
    | (n_simp) ‹tautology x ∨ ¬distinct_mset x›
    by auto
  then show ?thesis
    proof cases
      case simpl
      then have ‹x ∈ simple_clss (atms_of_ms A)›
        by (meson assms atms_of_atms_of_ms_mono atms_of_ms_finite simple_clss_mono
          distinct_mset_not_tautology_implies_in_simple_clss finite_subset
          subsetCE)
      then show ?thesis by blast
    next
      case n_simp
      then have ‹x ∈# not_simplified_cls (clausesNOT S)›
        using ‹x ∈# clausesNOT S› unfolding not_simplified_cls_tautology_distinct_mset by auto
      then show ?thesis by blast
    qed
qed

lemma cdclNOT_merged_bj_learn_clauses_bound:
  assumes
    ‹cdclNOT_merged_bj_learn S T› and
    inv: ‹inv S› and
    atms_clss: ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    fin_A[simp]: ‹finite A›
  shows ‹set_mset (clausesNOT T) ⊆ set_mset (not_simplified_cls (clausesNOT S))
    ∪ simple_clss (atms_of_ms A)›
  using assms(1-4)
proof (induction rule: cdclNOT_merged_bj_learn.induct)
  case cdclNOT_merged_bj_learn_decideNOT
  then show ?case using dpll_bj_clauses by (force dest!: simple_clss_or_not_simplified_cls)
next
  case cdclNOT_merged_bj_learn_propagateNOT
  then show ?case using dpll_bj_clauses by (force dest!: simple_clss_or_not_simplified_cls)
next
  case cdclNOT_merged_bj_learn_forgetNOT
  then show ?case using clauses_remove_clsNOT unfolding state_eqNOT_def
    by (force elim!: forgetNOTE dest: simple_clss_or_not_simplified_cls)
next
  case (cdclNOT_merged_bj_learn_backjump_l T) note bj = this(1) and inv = this(2) and
    atms_clss = this(3) and atms_trail = this(4)

  have st: ‹cdclNOT_merged_bj_learn** S T›
    using bj inv cdclNOT_merged_bj_learn.simps by blast+
  have ‹atm_of `(lits_of_l (trail T)) ⊆ atms_of_ms A› and ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st] inv atms_trail atms_clss
    by auto

  obtain F' K F L l C' C D where
    tr_S: ‹trail S = F' @ Decided K # F› and
    T: ‹T ∼ prepend_trail (Propagated L l) (reduce_trail_toNOT F (add_clsNOT D S))› and
    ‹C ∈# clausesNOT S› and
    ‹trail S ⊨as CNot C› and
    undef: ‹undefined_lit F L› and
    ‹clausesNOT S ⊨pm add_mset L C'› and
    ‹F ⊨as CNot C'› and
    D: ‹D = add_mset L C'› and
    dist: ‹distinct_mset (add_mset L C')› and
    tauto: ‹¬ tautology (add_mset L C')› and
    ‹backjump_l_cond C C' L S T›
    using ‹backjump_l S T› apply (elim backjump_lE) by auto

  have ‹atms_of C' ⊆ atm_of ` (lits_of_l F)›
    using ‹F ⊨as CNot C'› by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
      atms_of_def image_subset_iff in_CNot_implies_uminus(2))
  then have ‹atms_of (C'+{#L#}) ⊆ atms_of_ms A›
    using T ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A› tr_S undef by auto
  then have ‹simple_clss (atms_of (add_mset L C')) ⊆ simple_clss (atms_of_ms A)›
    apply - by (rule simple_clss_mono) (simp_all)
  then have ‹add_mset L C' ∈ simple_clss (atms_of_ms A)›
    using distinct_mset_not_tautology_implies_in_simple_clss[OF dist tauto]
    by auto
  then show ?case
    using T inv atms_clss undef tr_S D by (force dest!: simple_clss_or_not_simplified_cls)
qed

lemma cdclNOT_merged_bj_learn_not_simplified_decreasing:
  assumes ‹cdclNOT_merged_bj_learn S T›
  shows ‹not_simplified_cls (clausesNOT T) ⊆# not_simplified_cls (clausesNOT S)›
  using assms apply induction
  prefer 4
  unfolding not_simplified_cls_tautology_distinct_mset apply (auto elim!: backjump_lE forgetNOTE)[3]
  by (elim backjump_lE) auto

lemma rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing:
  assumes ‹cdclNOT_merged_bj_learn** S T›
  shows ‹not_simplified_cls (clausesNOT T) ⊆# not_simplified_cls (clausesNOT S)›
  using assms apply induction
    apply simp
   by (drule cdclNOT_merged_bj_learn_not_simplified_decreasing) auto

lemma rtranclp_cdclNOT_merged_bj_learn_clauses_bound:
  assumes
    ‹cdclNOT_merged_bj_learn** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    finite[simp]: ‹finite A›
  shows ‹set_mset (clausesNOT T) ⊆ set_mset (not_simplified_cls (clausesNOT S))
    ∪ simple_clss (atms_of_ms A)›
  using assms(1-4)
proof induction
  case base
  then show ?case by (auto dest!: simple_clss_or_not_simplified_cls)
next
  case (step T U) note st = this(1) and cdclNOT = this(2) and IH = this(3)[OF this(4-6)] and
    inv = this(4) and atms_clss_S = this(5) and atms_trail_S = this(6)
  have st': ‹cdclNOT** S T›
    using inv rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv st by blast
  have ‹inv T›
    using inv rtranclp_cdclNOT_merged_bj_learn_inv st by blast
  moreover
    have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A› and
      ‹atm_of ` lits_of_l (trail T) ⊆ atms_of_ms A›
      using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st] inv atms_clss_S
        atms_trail_S by blast+
  ultimately have ‹set_mset (clausesNOT U)
    ⊆ set_mset (not_simplified_cls (clausesNOT T)) ∪ simple_clss (atms_of_ms A)›
    using cdclNOT finite cdclNOT_merged_bj_learn_clauses_bound
    by (auto intro!: cdclNOT_merged_bj_learn_clauses_bound)
  moreover have ‹set_mset (not_simplified_cls (clausesNOT T))
    ⊆ set_mset (not_simplified_cls (clausesNOT S))›
    using rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing[OF st] by auto
  ultimately show ?case using IH inv atms_clss_S
    by (auto dest!: simple_clss_or_not_simplified_cls)
qed

abbreviation μCDCL'_bound where
‹μCDCL'_bound A T ≡ ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))) * 2
     + card (set_mset (not_simplified_cls(clausesNOT T)))
     + 3 ^ card (atms_of_ms A)›

lemma rtranclp_cdclNOT_merged_bj_learn_clauses_bound_card:
  assumes
    ‹cdclNOT_merged_bj_learn** S T› and
    ‹inv S› and
    ‹atms_of_mm (clausesNOT S) ⊆ atms_of_ms A› and
    ‹atm_of `(lits_of_l (trail S)) ⊆ atms_of_ms A› and
    finite: ‹finite A›
  shows ‹μCDCL'_merged A T ≤ μCDCL'_bound A S›
proof -
  have ‹set_mset (clausesNOT T) ⊆ set_mset (not_simplified_cls(clausesNOT S))
    ∪ simple_clss (atms_of_ms A)›
    using rtranclp_cdclNOT_merged_bj_learn_clauses_bound[OF assms] .
  moreover have ‹card (set_mset (not_simplified_cls(clausesNOT S))
      ∪ simple_clss (atms_of_ms A))
    ≤ card (set_mset (not_simplified_cls(clausesNOT S))) + 3 ^ card (atms_of_ms A)›
    by (meson Nat.le_trans atms_of_ms_finite simple_clss_card card_Un_le finite
      nat_add_left_cancel_le)
  ultimately have ‹card (set_mset (clausesNOT T))
    ≤ card (set_mset (not_simplified_cls(clausesNOT S))) + 3 ^ card (atms_of_ms A)›
    by (meson Nat.le_trans atms_of_ms_finite simple_clss_finite card_mono
      finite_UnI finite_set_mset local.finite)
  moreover have ‹((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μC' A T) * 2
    ≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) * 2›
    by auto
  ultimately show ?thesis unfolding μCDCL'_merged_def by auto
qed

sublocale cdclNOT_increasing_restarts_ops ‹λS T. T ∼ reduce_trail_toNOT ([]::'a list) S›
   cdclNOT_merged_bj_learn f
   (* bound_inv *)‹λA S. atms_of_mm (clausesNOT S) ⊆ atms_of_ms A
     ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧ finite A›
   μCDCL'_merged
   (* inv *) ‹λS. inv S ∧ no_dup (trail S)›
   μCDCL'_bound
   apply unfold_locales
              using unbounded apply simp
             using f_ge_1 apply force
            using cdclNOT_merged_bj_learn_trail_clauses_bound apply meson
           apply (simp add: cdclNOT_decreasing_measure')
          using rtranclp_cdclNOT_merged_bj_learn_clauses_bound_card apply blast
          apply (drule rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing)
          apply (auto simp: card_mono set_mset_mono)[]
       apply simp
      apply auto[]
     using cdclNOT_merged_bj_learn_no_dup_inv cdcl_merged_inv apply blast
    apply (auto simp: inv_restart)[]
    done

lemma cdclNOT_restart_μCDCL'_merged_le_μCDCL'_bound:
  assumes
    ‹cdclNOT_restart T V›
    ‹inv (fst T)› and
    ‹no_dup (trail (fst T))› and
    ‹atms_of_mm (clausesNOT (fst T)) ⊆ atms_of_ms A› and
    ‹atm_of ` lits_of_l (trail (fst T)) ⊆ atms_of_ms A› and
    ‹finite A›
  shows ‹μCDCL'_merged A (fst V) ≤ μCDCL'_bound A (fst T)›
  using assms
proof induction
  case (restart_full S T n)
  show ?case
    unfolding fst_conv
    apply (rule rtranclp_cdclNOT_merged_bj_learn_clauses_bound_card)
    using restart_full unfolding full1_def by (force dest!: tranclp_into_rtranclp)+
next
  case (restart_step m S T n U) note st = this(1) and U = this(3) and inv = this(4) and
    n_d = this(5) and atms_clss = this(6) and atms_trail = this(7) and finite = this(8)
  then have st': ‹cdclNOT_merged_bj_learn** S T›
    by (blast dest: relpowp_imp_rtranclp)
  then have st'': ‹cdclNOT** S T›
    using inv n_d apply - by (rule rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT) auto
  have ‹inv T›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_inv)
      using inv st' n_d by auto
  then have ‹inv U›
    using U by (auto simp: inv_restart)
  have ‹atms_of_mm (clausesNOT T) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_merged_bj_learn_trail_clauses_bound[OF st'] inv atms_clss atms_trail n_d
    by simp
  then have ‹atms_of_mm (clausesNOT U) ⊆ atms_of_ms A›
    using U by simp
  have ‹not_simplified_cls (clausesNOT U) ⊆# not_simplified_cls (clausesNOT T)›
    using ‹U ∼ reduce_trail_toNOT [] T› by auto
  moreover have ‹not_simplified_cls (clausesNOT T) ⊆# not_simplified_cls (clausesNOT S)›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing)
    using ‹(cdclNOT_merged_bj_learn ^^ m) S T› by (auto dest!: relpowp_imp_rtranclp)
  ultimately have U_S: ‹not_simplified_cls (clausesNOT U) ⊆# not_simplified_cls (clausesNOT S)›
    by auto

  have ‹(set_mset (clausesNOT U))
    ⊆ set_mset (not_simplified_cls (clausesNOT U)) ∪ simple_clss (atms_of_ms A)›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_clauses_bound)
         apply simp
        using ‹inv U› apply simp
       using ‹atms_of_mm (clausesNOT U) ⊆ atms_of_ms A› apply simp
      using U apply simp
    using finite apply simp
    done
  then have f1: ‹card (set_mset (clausesNOT U)) ≤ card (set_mset (not_simplified_cls (clausesNOT U))
    ∪ simple_clss (atms_of_ms A))›
    by (simp add: simple_clss_finite card_mono local.finite)

  moreover have ‹set_mset (not_simplified_cls (clausesNOT U)) ∪ simple_clss (atms_of_ms A)
    ⊆ set_mset (not_simplified_cls (clausesNOT S)) ∪ simple_clss (atms_of_ms A)›
    using U_S by auto
  then have f2:
    ‹card (set_mset (not_simplified_cls (clausesNOT U)) ∪ simple_clss (atms_of_ms A))
      ≤ card (set_mset (not_simplified_cls (clausesNOT S)) ∪ simple_clss (atms_of_ms A))›
    by (simp add: simple_clss_finite card_mono local.finite)

  moreover have ‹card (set_mset (not_simplified_cls (clausesNOT S))
      ∪ simple_clss (atms_of_ms A))
    ≤ card (set_mset (not_simplified_cls (clausesNOT S))) + card (simple_clss (atms_of_ms A))›
    using card_Un_le by blast
  moreover have ‹card (simple_clss (atms_of_ms A)) ≤ 3 ^ card (atms_of_ms A)›
    using atms_of_ms_finite simple_clss_card local.finite by blast
  ultimately have ‹card (set_mset (clausesNOT U))
    ≤ card (set_mset (not_simplified_cls (clausesNOT S))) + 3 ^ card (atms_of_ms A)›
    by linarith
  then show ?case unfolding μCDCL'_merged_def by auto
qed

lemma cdclNOT_restart_μCDCL'_bound_le_μCDCL'_bound:
  assumes
    ‹cdclNOT_restart T V› and
    ‹no_dup (trail (fst T))› and
    ‹inv (fst T)› and
    fin: ‹finite A›
  shows ‹μCDCL'_bound A (fst V) ≤ μCDCL'_bound A (fst T)›
  using assms(1-3)
proof induction
  case (restart_full S T n)
  have ‹not_simplified_cls (clausesNOT T) ⊆# not_simplified_cls (clausesNOT S)›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing)
    using ‹full1 cdclNOT_merged_bj_learn S T› unfolding full1_def
    by (auto dest: tranclp_into_rtranclp)
  then show ?case by (auto simp: card_mono set_mset_mono)
next
  case (restart_step m S T n U) note st = this(1) and U = this(3) and n_d = this(4) and
    inv = this(5)
  then have st': ‹cdclNOT_merged_bj_learn** S T›
    by (blast dest: relpowp_imp_rtranclp)
  then have st'': ‹cdclNOT** S T›
    using inv n_d apply - by (rule rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT) auto
  have ‹inv T›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_inv)
      using inv st' n_d by auto
  then have ‹inv U›
    using U by (auto simp: inv_restart)
  have ‹not_simplified_cls (clausesNOT U) ⊆# not_simplified_cls (clausesNOT T)›
    using ‹U ∼ reduce_trail_toNOT [] T› by auto
  moreover have ‹not_simplified_cls (clausesNOT T) ⊆# not_simplified_cls (clausesNOT S)›
    apply (rule rtranclp_cdclNOT_merged_bj_learn_not_simplified_decreasing)
    using ‹(cdclNOT_merged_bj_learn ^^ m) S T› by (auto dest!: relpowp_imp_rtranclp)
  ultimately have U_S: ‹not_simplified_cls (clausesNOT U) ⊆# not_simplified_cls (clausesNOT S)›
    by auto
  then show ?case by (auto simp: card_mono set_mset_mono)
qed


sublocale cdclNOT_increasing_restarts _ _ _ _ _ _ f
   ‹λS T. T ∼ reduce_trail_toNOT ([]::'a list) S›
   (* bound_inv *)‹λA S. atms_of_mm (clausesNOT S) ⊆ atms_of_ms A
     ∧ atm_of ` lits_of_l (trail S) ⊆ atms_of_ms A ∧ finite A›
   μCDCL'_merged cdclNOT_merged_bj_learn
   (* inv *) ‹λS. inv S ∧ no_dup (trail S)›
   ‹λA T. ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))) * 2
     + card (set_mset (not_simplified_cls(clausesNOT T)))
     + 3 ^ card (atms_of_ms A)›
   apply unfold_locales
     using cdclNOT_restart_μCDCL'_merged_le_μCDCL'_bound apply force
    using cdclNOT_restart_μCDCL'_bound_le_μCDCL'_bound by fastforce

lemma true_clss_ext_decrease_right_insert: ‹I ⊨sext insert C (set_mset M) ⟹ I ⊨sextm M›
  by (metis Diff_insert_absorb insert_absorb true_clss_ext_decrease_right_remove_r)

lemma true_clss_ext_decrease_add_implied:
  assumes ‹M ⊨pm C›
  shows ‹I⊨sext insert C (set_mset M) ⟷ I⊨sextm M›
proof -
  { fix J
    assume
      ‹I ⊨sextm M› and
      ‹I ⊆ J› and
      tot: ‹total_over_m J (set_mset ({#C#} + M))› and
      cons: ‹consistent_interp J›
    then have ‹J ⊨sm M› unfolding true_clss_ext_def by auto

    moreover
      with ‹M ⊨pm C› have ‹J ⊨ C›
        using tot cons unfolding true_clss_cls_def by auto
    ultimately have ‹J ⊨sm {#C#} + M› by auto
  }
  then have H: ‹I ⊨sextm M ⟹ I ⊨sext insert C (set_mset M)›
    unfolding true_clss_ext_def by auto
  then show ?thesis
    by (auto simp: true_clss_ext_decrease_right_insert)
qed

lemma cdclNOT_merged_bj_learn_bj_sat_ext_iff:
  assumes ‹cdclNOT_merged_bj_learn S T› and inv: ‹inv S›
  shows ‹I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  using assms
proof (induction rule: cdclNOT_merged_bj_learn.induct)
  case (cdclNOT_merged_bj_learn_backjump_l T) note bj_l = this(1)
  obtain C' L D S' where
    learn: ‹learn S' T› and
    bj: ‹backjump S S'› and
    atms_C: ‹atms_of (add_mset L C') ⊆ atms_of_mm (clausesNOT S) ∪ atm_of ` (lits_of_l (trail S))› and
    D: ‹D = add_mset L C'› and
    T: ‹T ∼ add_clsNOT D S'› and
    clss_D: ‹clausesNOT S ⊨pm D›
    using bj_l inv backjump_l_backjump_learn [of S] by blast
  have [simp]: ‹clausesNOT S' = clausesNOT S›
    using bj by (auto elim: backjumpE)
  have ‹(I ⊨sextm clausesNOT S) ⟷ (I ⊨sextm clausesNOT S')›
    using bj bj_backjump dpll_bj_clauses inv by fastforce
  then show ?case
    using clss_D T by (auto simp: true_clss_ext_decrease_add_implied)
qed (auto simp: cdclNOT_bj_sat_ext_iff
    dest!: dpll_bj.intros cdclNOT.intros)

lemma rtranclp_cdclNOT_merged_bj_learn_bj_sat_ext_iff:
  assumes ‹cdclNOT_merged_bj_learn** S T›and ‹inv S›
  shows ‹I⊨sextm clausesNOT S ⟷ I⊨sextm clausesNOT T›
  using assms apply (induction rule: rtranclp_induct)
    apply simp
  using cdclNOT_merged_bj_learn_bj_sat_ext_iff
    rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv by blast

lemma cdclNOT_restart_eq_sat_iff:
  assumes
    ‹cdclNOT_restart S T› and
    inv: ‹inv (fst S)›
  shows ‹I⊨sextm clausesNOT (fst S) ⟷ I ⊨sextm clausesNOT (fst T)›
  using assms
proof (induction rule: cdclNOT_restart.induct)
  case (restart_full S T n)
  then have ‹cdclNOT_merged_bj_learn** S T ›
    by (simp add: tranclp_into_rtranclp full1_def)
  then show ?case
    using rtranclp_cdclNOT_merged_bj_learn_bj_sat_ext_iff restart_full.prems by auto
next
  case (restart_step m S T n U)
  then have ‹cdclNOT_merged_bj_learn** S T›
    by (auto simp: tranclp_into_rtranclp full1_def dest!: relpowp_imp_rtranclp)
  then have ‹I ⊨sextm clausesNOT S ⟷ I ⊨sextm clausesNOT T›
    using rtranclp_cdclNOT_merged_bj_learn_bj_sat_ext_iff restart_step.prems by auto
  moreover have ‹I ⊨sextm clausesNOT T ⟷ I ⊨sextm clausesNOT U›
    using restart_step.hyps(3) by auto
  ultimately show ?case by auto
qed

lemma rtranclp_cdclNOT_restart_eq_sat_iff:
  assumes
    ‹cdclNOT_restart** S T› and
    inv: ‹inv (fst S)› and n_d: ‹no_dup(trail (fst S))›
  shows ‹I⊨sextm clausesNOT (fst S) ⟷ I ⊨sextm clausesNOT (fst T)›
  using assms(1)
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step T U) note st = this(1) and cdcl = this(2) and IH = this(3)
  have ‹inv (fst T)› and ‹no_dup (trail (fst T))›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv using st inv n_d by blast+
  then have ‹I⊨sextm clausesNOT (fst T) ⟷ I ⊨sextm clausesNOT (fst U)›
    using cdclNOT_restart_eq_sat_iff cdcl by blast
  then show ?case using IH by blast
qed

lemma cdclNOT_restart_all_decomposition_implies_m:
  assumes
    ‹cdclNOT_restart S T› and
    inv: ‹inv (fst S)› and n_d: ‹no_dup(trail (fst S))› and
    ‹all_decomposition_implies_m (clausesNOT (fst S))
      (get_all_ann_decomposition (trail (fst S)))›
  shows ‹all_decomposition_implies_m (clausesNOT (fst T))
      (get_all_ann_decomposition (trail (fst T)))›
  using assms
proof induction
  case (restart_full S T n) note full = this(1) and inv = this(2) and n_d = this(3) and
    decomp = this(4)
  have st: ‹cdclNOT_merged_bj_learn** S T› and
    n_s: ‹no_step cdclNOT_merged_bj_learn T›
    using full unfolding full1_def by (fast dest: tranclp_into_rtranclp)+
  have st': ‹cdclNOT** S T›
    using inv rtranclp_cdclNOT_merged_bj_learn_is_rtranclp_cdclNOT_and_inv st n_d by auto
  have ‹inv T›
    using rtranclp_cdclNOT_cdclNOT_inv[OF st] inv n_d by auto
  then show ?case
    using rtranclp_cdclNOT_merged_bj_learn_all_decomposition_implies[OF _ _ decomp] st inv by auto
next
  case (restart_step m S T n U) note st = this(1) and U = this(3) and inv = this(4) and
    n_d = this(5) and decomp = this(6)
  show ?case using U by auto
qed

lemma rtranclp_cdclNOT_restart_all_decomposition_implies_m:
  assumes
    ‹cdclNOT_restart** S T› and
    inv: ‹inv (fst S)› and n_d: ‹no_dup(trail (fst S))› and
    decomp: ‹all_decomposition_implies_m (clausesNOT (fst S))
      (get_all_ann_decomposition (trail (fst S)))›
  shows ‹all_decomposition_implies_m (clausesNOT (fst T))
      (get_all_ann_decomposition (trail (fst T)))›
  using assms
proof induction
  case base
  then show ?case using decomp by simp
next
  case (step T U) note st = this(1) and cdcl = this(2) and IH = this(3)[OF this(4-)] and
    inv = this(4) and n_d = this(5) and decomp = this(6)
  have ‹inv (fst T)› and ‹no_dup (trail (fst T))›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv using st inv n_d by blast+
  then show ?case
    using cdclNOT_restart_all_decomposition_implies_m[OF cdcl] IH by auto
qed

lemma full_cdclNOT_restart_normal_form:
  assumes
    full: ‹full cdclNOT_restart S T› and
    inv: ‹inv (fst S)› and n_d: ‹no_dup(trail (fst S))› and
    decomp: ‹all_decomposition_implies_m (clausesNOT (fst S))
      (get_all_ann_decomposition (trail (fst S)))› and
    atms_cls: ‹atms_of_mm (clausesNOT (fst S)) ⊆ atms_of_ms A› and
    atms_trail: ‹atm_of ` lits_of_l (trail (fst S)) ⊆ atms_of_ms A› and
    fin: ‹finite A›
  shows ‹unsatisfiable (set_mset (clausesNOT (fst S)))
    ∨ lits_of_l (trail (fst T)) ⊨sextm clausesNOT (fst S) ∧
       satisfiable (set_mset (clausesNOT (fst S)))›
proof -
  have inv_T: ‹inv (fst T)› and n_d_T: ‹no_dup (trail (fst T))›
    using rtranclp_cdclNOT_with_restart_cdclNOT_inv using full inv n_d unfolding full_def by blast+
  moreover have
    atms_cls_T: ‹atms_of_mm (clausesNOT (fst T)) ⊆ atms_of_ms A› and
    atms_trail_T: ‹atm_of ` lits_of_l (trail (fst T)) ⊆ atms_of_ms A›
    using rtranclp_cdclNOT_with_restart_bound_inv[of S T A] full atms_cls atms_trail fin inv n_d
    unfolding full_def by blast+
  ultimately have ‹no_step cdclNOT_merged_bj_learn (fst T)›
    apply -
    apply (rule no_step_cdclNOT_restart_no_step_cdclNOT[of _ A])
       using full unfolding full_def apply simp
      apply simp
    using fin apply simp
    done
  moreover have ‹all_decomposition_implies_m (clausesNOT (fst T))
    (get_all_ann_decomposition (trail (fst T)))›
    using rtranclp_cdclNOT_restart_all_decomposition_implies_m[of S T] inv n_d decomp
    full unfolding full_def by auto
  ultimately have ‹unsatisfiable (set_mset (clausesNOT (fst T)))
    ∨ trail (fst T) ⊨asm clausesNOT (fst T) ∧ satisfiable (set_mset (clausesNOT (fst T)))›
    apply -
    apply (rule cdclNOT_merged_bj_learn_final_state)
    using atms_cls_T atms_trail_T fin n_d_T fin inv_T by blast+
  then consider
      (unsat) ‹unsatisfiable (set_mset (clausesNOT (fst T)))›
    | (sat) ‹trail (fst T) ⊨asm clausesNOT (fst T)› and ‹satisfiable (set_mset (clausesNOT (fst T)))›
    by auto
  then show ‹unsatisfiable (set_mset (clausesNOT (fst S)))
    ∨ lits_of_l (trail (fst T)) ⊨sextm clausesNOT (fst S) ∧
       satisfiable (set_mset (clausesNOT (fst S)))›
    proof cases
      case unsat
      then have ‹unsatisfiable (set_mset (clausesNOT (fst S)))›
        unfolding satisfiable_def apply auto
        using rtranclp_cdclNOT_restart_eq_sat_iff[of S T ] full inv n_d
        consistent_true_clss_ext_satisfiable true_clss_imp_true_cls_ext
        unfolding satisfiable_def full_def by blast
      then show ?thesis by blast
    next
      case sat
      then have ‹lits_of_l (trail (fst T)) ⊨sextm clausesNOT (fst T)›
        using true_clss_imp_true_cls_ext by (auto simp: true_annots_true_cls)
      then have ‹lits_of_l (trail (fst T)) ⊨sextm clausesNOT (fst S)›
        using rtranclp_cdclNOT_restart_eq_sat_iff[of S T] full inv n_d unfolding full_def by blast
      moreover then have ‹satisfiable (set_mset (clausesNOT (fst S)))›
        using consistent_true_clss_ext_satisfiable distinct_consistent_interp n_d_T by fast
      ultimately show ?thesis by fast
    qed
qed

corollary full_cdclNOT_restart_normal_form_init_state:
  assumes
    init_state: ‹trail S = []› ‹clausesNOT S = N› and
    full: ‹full cdclNOT_restart (S, 0) T› and
    inv: ‹inv S›
  shows ‹unsatisfiable (set_mset N)
    ∨ lits_of_l (trail (fst T)) ⊨sextm N ∧ satisfiable (set_mset N)›
  using full_cdclNOT_restart_normal_form[of ‹(S, 0)› T] assms by auto

end ― ‹End of locale @{locale cdclNOT_merge_bj_learn_with_backtrack_restarts}.›

end