Theory CDCL_W_BnB

theory CDCL_W_BnB
  imports CDCL.CDCL_W_Abstract_State
begin

section CDCL Extensions

text 
  A counter-example for the original version from the book has been found (see below). There is no
  simple fix, except taking complete models.

  Based on Dominik Zimmer's thesis, we later reduced the problem of finding partial models to
  finding total models. We later switched to the more elegant dual rail encoding (thanks to the
  reviewer).


subsection Optimisations

notation image_mset (infixr `# 90)

text The initial version was supposed to work on partial models directly. I found a counterexample
while writing the proof:

\nitpicking{

\shortrules{Propagate}{$(M;N;U;k;\top;O)$}{$(ML^{C\lor L};N;U;k;\top;O)$}

provided $C\lor L\in (N\cup U)$, $M\models \neg C$, $L$ is undefined in $M$.

\bigskip
\shortrules{Decide}{$(M;N;U;k;\top;O)$}{$(ML^{k+1};N;U;k+1;\top;O)$}

provided $L$ is undefined in $M$, contained in $N$.

\bigskip
\shortrules{ConflSat}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;D;O)$}

provided $D\in (N\cup U)$ and $M\models \neg D$.

\bigskip
\shortrules{ConflOpt}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;\neg M;O)$}

provided $O\neq\epsilon$ and $\operatorname{cost}(M) \geq \operatorname{cost}(O)$.

\bigskip
\shortrules{Skip}{$(ML^{C\lor L};N;U;k;D;O)$}{$(M;N;U;k;D;O)$}

provided $D\not\in\{\top,\bot\}$ and $\neg L$ does not occur in $D$.


\bigskip
\shortrules{Resolve}{$(ML^{C\lor L};N;U;k;D\lor-(L);O)$}{$(M;N;U;k;D\lor C;O)$}

provided $D$ is of level $k$.

\bigskip
\shortrules{Backtrack}{$(M_1K^{i+1}M_2;N;U;k;D\lor L;O)$}{$(M_1L^{D\vee L};N;U\cup\{D\lor L\};i;
  \top;O)$}

provided $L$ is of level $k$ and $D$ is of level $i$.

\bigskip
\shortrules{Improve}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;\top;M)$}

provided $M\models N$ and $O=\epsilon$ or $\operatorname{cost}(M)<\operatorname{cost}(O)$.
}
{This calculus does not always find the model with minimum cost. Take for example the following
  cost function:
\[\operatorname{cost}: \left\{
\begin{array}{c@ {\rightarrow}c}
P & 3\\
\neg P & 1\\
Q & 1\\
\neg Q & 1\\
\end{array}
 \right.\]
and the clauses $N = \{P\lor Q\}$. We can then do the following transitions:


$(\epsilon, N, \varnothing, \top, \infty)$

\shortrules{Decide}{}{$(P^1, N, \varnothing, \top, \infty)$}

\shortrules{Improve}{}{$(P^1, N, \varnothing, \top, (P, 3))$}

\shortrules{conflictOpt}{}{$(P^1, N, \varnothing, \neg P, (P, 3))$}

\shortrules{backtrack}{}{$({\neg P}^{\neg P}, N, \{\neg P\}, \top, (P, 3))$}

\shortrules{propagate}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, \top, (P, 3))$}

\shortrules{improve}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, \top, (\neg P\, Q, 2))$}

\shortrules{conflictOpt}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, P \lor \neg Q, (\neg P\,
  Q, 2))$}

\shortrules{resolve}{}{$({\neg P}^{\neg P}, N, \{\neg P\}, P, (\neg P\, Q, 2))$}

\shortrules{resolve}{}{$(\epsilon, N, \{\neg P\}, \bot, (\neg P\, Q, 3))$}


However, the optimal model is $Q$.
}


text 
  The idea of the proof (explained of the example of the optimising CDCL) is the following:

   We start with a calculus OCDCL on term(M, N, U, D, Op).

   This extended to a state term(M, N + all_models_of_higher_cost, U, D, Op).

   Each transition step of OCDCL is mapped to a step in CDCL over the abstract state. The abstract
    set of clauses might be unsatisfiable, but we only use it to prove the invariants on the
    state. Only adding clause cannot be mapped to a transition over the abstract state, but adding
    clauses does not break the invariants (as long as the additional clauses do not contain
    duplicate literals).

   The last proofs are done over CDCLopt.

We abstract about how the optimisation is done in the locale below: We define a calculus
termcdcl_bnb (for branch-and-bounds). It is parametrised by how the conflicting clauses are
generated and the improvement criterion.

We later instantiate it with the optimisation calculus from Weidenbach's book.



subsubsection Helper libraries

definition model_on :: 'v partial_interp  'v clauses  bool where
model_on I N  consistent_interp I  atm_of ` I  atms_of_mm N


subsubsection CDCL BNB

locale conflict_driven_clause_learning_with_adding_init_clause_bnbW_no_state =
  stateW_no_state
    state_eq state
    ― ‹functions for the state:
      ― ‹access functions:
    trail init_clss learned_clss conflicting
      ― ‹changing state:
    cons_trail tl_trail add_learned_cls remove_cls
    update_conflicting

      ― ‹get state:
    init_state
  for
    state_eq :: 'st  'st  bool (infix  50) and
    state :: 'st  ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
      'a × 'b and
    trail :: 'st  ('v, 'v clause) ann_lits and
    init_clss :: 'st  'v clauses and
    learned_clss :: 'st  'v clauses and
    conflicting :: 'st  'v clause option and

    cons_trail :: ('v, 'v clause) ann_lit  'st  'st and
    tl_trail :: 'st  'st and
    add_learned_cls :: 'v clause  'st  'st and
    remove_cls :: 'v clause  'st  'st and
    update_conflicting :: 'v clause option  'st  'st and

    init_state :: 'v clauses  'st +
  fixes
    update_weight_information :: ('v, 'v clause) ann_lits  'st  'st and
    is_improving_int :: ('v, 'v clause) ann_lits  ('v, 'v clause) ann_lits  'v clauses  'a  bool and
    conflicting_clauses :: 'v clauses  'a  'v clauses and
    weight :: 'st  'a
begin

abbreviation is_improving where
  is_improving M M' S  is_improving_int M M' (init_clss S) (weight S)

definition additional_info' :: 'st  'b where
additional_info' S = (λ(_, _, _, _, _, D). D) (state S)

definition conflicting_clss :: 'st  'v literal multiset multiset where
conflicting_clss S = conflicting_clauses (init_clss S) (weight S)

text While it would more be natural to add an sublocale with the extended version clause set,
  this actually causes a loop in the hierarchy structure (although with different parameters).
  Therefore, adding theorems (e.g. defining an inductive predicate) causes a loop.

definition abs_state
  :: 'st  ('v, 'v clause) ann_lit list × 'v clauses × 'v clauses × 'v clause option
where
  abs_state S = (trail S, init_clss S + conflicting_clss S, learned_clss S,
    conflicting S)

end

locale conflict_driven_clause_learning_with_adding_init_clause_bnbW_ops =
  conflict_driven_clause_learning_with_adding_init_clause_bnbW_no_state
    state_eq state
    ― ‹functions for the state:
      ― ‹access functions:
    trail init_clss learned_clss conflicting
      ― ‹changing state:
    cons_trail tl_trail add_learned_cls remove_cls
    update_conflicting

      ― ‹get state:
    init_state
      ― ‹Adding a clause:
    update_weight_information is_improving_int conflicting_clauses weight
  for
    state_eq :: 'st  'st  bool (infix  50) and
    state :: "'st  ('v, 'v clause) ann_lits × 'v clauses × 'v clauses ×  'v clause option ×
      'a × 'b" and
    trail :: 'st  ('v, 'v clause) ann_lits and
    init_clss :: 'st  'v clauses and
    learned_clss :: 'st  'v clauses and
    conflicting :: 'st  'v clause option and

    cons_trail :: ('v, 'v clause) ann_lit  'st  'st and
    tl_trail :: 'st  'st and
    add_learned_cls :: 'v clause  'st  'st and
    remove_cls :: 'v clause  'st  'st and
    update_conflicting :: 'v clause option  'st  'st and

    init_state :: 'v clauses  'st and
    update_weight_information :: ('v, 'v clause) ann_lits  'st  'st and
    is_improving_int :: "('v, 'v clause) ann_lits  ('v, 'v clause) ann_lits  'v clauses 
      'a  bool" and
    conflicting_clauses :: 'v clauses  'a  'v clauses and
    weight :: 'st  'a +
  assumes
    state_prop':
      state S = (trail S, init_clss S, learned_clss S, conflicting S, weight S, additional_info' S)
    and
    update_weight_information:
       state S = (M, N, U, C, w, other) 
          w'. state (update_weight_information T S) = (M, N, U, C, w', other) and
    atms_of_conflicting_clss:
      atms_of_mm (conflicting_clss S)  atms_of_mm (init_clss S) and
    distinct_mset_mset_conflicting_clss:
      distinct_mset_mset (conflicting_clss S) and
    conflicting_clss_update_weight_information_mono:
      cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  is_improving M M' S 
        conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)
    and
    conflicting_clss_update_weight_information_in:
      is_improving M M' S  
        negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)
begin

paragraph Conversion to CDCL
sublocale conflict_driven_clause_learningW where
  state_eq = state_eq and
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and
  cons_trail = cons_trail and
  tl_trail = tl_trail and
  add_learned_cls = add_learned_cls and
  remove_cls = remove_cls and
  update_conflicting = update_conflicting and
  init_state = init_state
  apply unfold_locales
  unfolding additional_info'_def additional_info_def by (auto simp: state_prop')

paragraph Overall simplification on states
declare reduce_trail_to_skip_beginning[simp]

lemma state_eq_weight[state_simp, simp]: S  T  weight S = weight T
  apply (drule state_eq_state)
  apply (subst (asm) state_prop')+
  by simp


lemma conflicting_clause_state_eq[state_simp, simp]:
  S  T  conflicting_clss S = conflicting_clss T
  unfolding conflicting_clss_def by auto

lemma
  weight_cons_trail[simp]:
    weight (cons_trail L S) = weight S and
  weight_update_conflicting[simp]:
    weight (update_conflicting C S) = weight S and
  weight_tl_trail[simp]:
    weight (tl_trail S) = weight S and
  weight_add_learned_cls[simp]:
    weight (add_learned_cls D S) = weight S
  using cons_trail[of S _ _ L] update_conflicting[of S] tl_trail[of S] add_learned_cls[of S]
  by (auto simp: state_prop')

lemma update_weight_information_simp[simp]:
  trail (update_weight_information C S) = trail S
  init_clss (update_weight_information C S) = init_clss S
  learned_clss (update_weight_information C S) = learned_clss S
  clauses (update_weight_information C S) = clauses S
  backtrack_lvl (update_weight_information C S) = backtrack_lvl S
  conflicting (update_weight_information C S) = conflicting S
  using update_weight_information[of S] unfolding clauses_def
  by (subst (asm) state_prop', subst (asm) state_prop'; force)+

lemma
  conflicting_clss_cons_trail[simp]: conflicting_clss (cons_trail K S) = conflicting_clss S and
  conflicting_clss_tl_trail[simp]: conflicting_clss (tl_trail S) = conflicting_clss S and
  conflicting_clss_add_learned_cls[simp]:
    conflicting_clss (add_learned_cls D S) = conflicting_clss S and
  conflicting_clss_update_conflicting[simp]:
    conflicting_clss (update_conflicting E S) = conflicting_clss S
  unfolding conflicting_clss_def by auto

lemma conflicting_abs_state_conflicting[simp]:
    CDCL_W_Abstract_State.conflicting (abs_state S) = conflicting S and
  clauses_abs_state[simp]:
    cdclW_restart_mset.clauses (abs_state S) = clauses S + conflicting_clss S and
  abs_state_tl_trail[simp]:
    abs_state (tl_trail S) = CDCL_W_Abstract_State.tl_trail (abs_state S) and
  abs_state_add_learned_cls[simp]:
    abs_state (add_learned_cls C S) = CDCL_W_Abstract_State.add_learned_cls C (abs_state S) and
  abs_state_update_conflicting[simp]:
    abs_state (update_conflicting D S) = CDCL_W_Abstract_State.update_conflicting D (abs_state S)
  by (auto simp: conflicting.simps abs_state_def cdclW_restart_mset.clauses_def
    init_clss.simps learned_clss.simps clauses_def tl_trail.simps
    add_learned_cls.simps update_conflicting.simps)

lemma sim_abs_state_simp: S  T  abs_state S = abs_state T
  by (auto simp: abs_state_def)

lemma reduce_trail_to_update_weight_information[simp]:
  trail (reduce_trail_to M (update_weight_information M' S)) = trail (reduce_trail_to M S)
  unfolding trail_reduce_trail_to_drop by auto

lemma additional_info_weight_additional_info': additional_info S = (weight S, additional_info' S)
  using state_prop[of S] state_prop'[of S] by auto

lemma
  weight_reduce_trail_to[simp]: weight (reduce_trail_to M S) = weight S and
  additional_info'_reduce_trail_to[simp]: additional_info' (reduce_trail_to M S) = additional_info' S
  using additional_info_reduce_trail_to[of M S] unfolding additional_info_weight_additional_info'
  by auto

lemma conflicting_clss_reduce_trail_to[simp]:
  conflicting_clss (reduce_trail_to M S) = conflicting_clss S
  unfolding conflicting_clss_def by auto

lemma trail_trail [simp]:
  CDCL_W_Abstract_State.trail (abs_state S) = trail S
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma [simp]:
  CDCL_W_Abstract_State.trail (cdclW_restart_mset.reduce_trail_to M (abs_state S)) =
     trail (reduce_trail_to M S)
  by (auto simp: trail_reduce_trail_to_drop
    cdclW_restart_mset.trail_reduce_trail_to_drop)

lemma abs_state_cons_trail[simp]:
    abs_state (cons_trail K S) = CDCL_W_Abstract_State.cons_trail K (abs_state S) and
  abs_state_reduce_trail_to[simp]:
    abs_state (reduce_trail_to M S) = cdclW_restart_mset.reduce_trail_to M (abs_state S)
  subgoal by (auto simp: abs_state_def cons_trail.simps)
  subgoal by (induction rule: reduce_trail_to_induct)
       (auto simp: reduce_trail_to.simps cdclW_restart_mset.reduce_trail_to.simps)
  done


lemma learned_clss_learned_clss[simp]:
    CDCL_W_Abstract_State.learned_clss (abs_state S) = learned_clss S
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma state_eq_init_clss_abs_state[state_simp, simp]:
  S  T  CDCL_W_Abstract_State.init_clss (abs_state S) = CDCL_W_Abstract_State.init_clss (abs_state T)
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma
  init_clss_abs_state_update_conflicting[simp]:
    CDCL_W_Abstract_State.init_clss (abs_state (update_conflicting (Some D) S)) =
       CDCL_W_Abstract_State.init_clss (abs_state S) and
  init_clss_abs_state_cons_trail[simp]:
    CDCL_W_Abstract_State.init_clss (abs_state (cons_trail K S)) =
      CDCL_W_Abstract_State.init_clss (abs_state S)
  by (auto simp: abs_state_def cdclW_restart_mset_state)


paragraph CDCL with branch-and-bound

inductive conflict_opt :: 'st  'st  bool for S T :: 'st where
conflict_opt_rule:
  conflict_opt S T
  if
    negate_ann_lits (trail S) ∈# conflicting_clss S
    conflicting S = None
    T  update_conflicting (Some (negate_ann_lits (trail S))) S

inductive_cases conflict_optE: conflict_opt S T

inductive improvep :: 'st  'st  bool for S :: 'st where
improve_rule:
  improvep S T
  if
    is_improving (trail S) M' S and
    conflicting S = None and
    T  update_weight_information M' S

inductive_cases improveE: improvep S T

lemma invs_update_weight_information[simp]:
  no_strange_atm (update_weight_information C S) = (no_strange_atm S)
  cdclW_M_level_inv (update_weight_information C S) = cdclW_M_level_inv S
  distinct_cdclW_state (update_weight_information C S) = distinct_cdclW_state S
  cdclW_conflicting (update_weight_information C S) = cdclW_conflicting S
  cdclW_learned_clause (update_weight_information C S) = cdclW_learned_clause S
  unfolding no_strange_atm_def cdclW_M_level_inv_def distinct_cdclW_state_def cdclW_conflicting_def
    cdclW_learned_clause_alt_def cdclW_all_struct_inv_def by auto

lemma conflict_opt_cdclW_all_struct_inv:
  assumes conflict_opt S T and
    inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
  using assms atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
  by (induction rule: conflict_opt.cases)
    (auto simp add: cdclW_restart_mset.no_strange_atm_def
        cdclW_restart_mset.cdclW_M_level_inv_def
        cdclW_restart_mset.distinct_cdclW_state_def cdclW_restart_mset.cdclW_conflicting_def
        cdclW_restart_mset.cdclW_learned_clause_alt_def cdclW_restart_mset.cdclW_all_struct_inv_def
        true_annots_true_cls_def_iff_negation_in_model
        in_negate_trial_iff cdclW_restart_mset_state cdclW_restart_mset.clauses_def
        distinct_mset_mset_conflicting_clss abs_state_def
      intro!: true_clss_cls_in)

lemma improve_cdclW_all_struct_inv:
  assumes improvep S T and
    inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
  using assms atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
proof (induction rule: improvep.cases)
  case (improve_rule M' T)
  moreover have all_decomposition_implies
     (set_mset (init_clss S)  set_mset (conflicting_clss S)  set_mset (learned_clss S))
     (get_all_ann_decomposition (trail S)) 
    all_decomposition_implies
     (set_mset (init_clss S)  set_mset (conflicting_clss (update_weight_information M' S)) 
      set_mset (learned_clss S))
     (get_all_ann_decomposition (trail S))
      apply (rule all_decomposition_implies_mono)
      using improve_rule conflicting_clss_update_weight_information_mono[of S trail S M'] inv
      by (auto dest: multi_member_split)
   ultimately show ?case
      using conflicting_clss_update_weight_information_mono[of S trail S M']
      by (auto 6 2 simp add: cdclW_restart_mset.no_strange_atm_def
            cdclW_restart_mset.cdclW_M_level_inv_def
            cdclW_restart_mset.distinct_cdclW_state_def cdclW_restart_mset.cdclW_conflicting_def
            cdclW_restart_mset.cdclW_learned_clause_alt_def cdclW_restart_mset.cdclW_all_struct_inv_def
            true_annots_true_cls_def_iff_negation_in_model
            in_negate_trial_iff cdclW_restart_mset_state cdclW_restart_mset.clauses_def
            image_Un distinct_mset_mset_conflicting_clss abs_state_def
          simp del: append_assoc
          dest: no_dup_appendD consistent_interp_unionD)
qed

text termcdclW_restart_mset.cdclW_stgy_invariant is too restrictive:
  termcdclW_restart_mset.no_smaller_confl is needed but does not hold(at least, if cannot
  ensure that conflicts are found as soon as possible).
lemma improve_no_smaller_conflict:
  assumes improvep S T and
    no_smaller_confl S
  shows no_smaller_confl T and conflict_is_false_with_level T
  using assms apply (induction rule: improvep.induct)
  unfolding cdclW_restart_mset.cdclW_stgy_invariant_def
  by (auto simp: cdclW_restart_mset_state no_smaller_confl_def cdclW_restart_mset.clauses_def
      exists_lit_max_level_in_negate_ann_lits)

lemma conflict_opt_no_smaller_conflict:
  assumes conflict_opt S T and
    no_smaller_confl S
  shows no_smaller_confl T and conflict_is_false_with_level T
  using assms by (induction rule: conflict_opt.induct)
    (auto simp: cdclW_restart_mset_state no_smaller_confl_def cdclW_restart_mset.clauses_def
      exists_lit_max_level_in_negate_ann_lits cdclW_restart_mset.cdclW_stgy_invariant_def)

fun no_confl_prop_impr where
  no_confl_prop_impr S 
    no_step propagate S  no_step conflict S

text We use a slighlty generalised form of backtrack to make conflict clause minimisation possible.
inductive obacktrack :: 'st  'st  bool for S :: 'st where
obacktrack_rule: 
  conflicting S = Some (add_mset L D) 
  (Decided K # M1, M2)  set (get_all_ann_decomposition (trail S)) 
  get_level (trail S) L = backtrack_lvl S 
  get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') 
  get_maximum_level (trail S) D'  i 
  get_level (trail S) K = i + 1 
  D' ⊆# D 
  clauses S + conflicting_clss S ⊨pm add_mset L D' 
  T  cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None S))) 
  obacktrack S T

inductive_cases obacktrackE: obacktrack S T

inductive cdcl_bnb_bj :: 'st  'st  bool where
skip: skip S S'  cdcl_bnb_bj S S' |
resolve: resolve S S'  cdcl_bnb_bj S S' |
backtrack: obacktrack S S'  cdcl_bnb_bj S S'

inductive_cases cdcl_bnb_bjE: cdcl_bnb_bj S T

inductive ocdclW_o :: 'st  'st  bool for S :: 'st where
decide: decide S S'  ocdclW_o S S' |
bj: cdcl_bnb_bj S S'  ocdclW_o S S'

inductive cdcl_bnb :: 'st  'st  bool for S :: 'st where
cdcl_conflict: conflict S S'  cdcl_bnb S S' |
cdcl_propagate: propagate S S'  cdcl_bnb S S' |
cdcl_improve: improvep S S'  cdcl_bnb S S' |
cdcl_conflict_opt: conflict_opt S S'  cdcl_bnb S S' |
cdcl_other': ocdclW_o S S'  cdcl_bnb S S'

inductive cdcl_bnb_stgy :: 'st  'st  bool for S :: 'st where
cdcl_bnb_conflict: conflict S S'  cdcl_bnb_stgy S S' |
cdcl_bnb_propagate: propagate S S'  cdcl_bnb_stgy S S' |
cdcl_bnb_improve: improvep S S'  cdcl_bnb_stgy S S' |
cdcl_bnb_conflict_opt: conflict_opt S S'  cdcl_bnb_stgy S S' |
cdcl_bnb_other': ocdclW_o S S'  no_confl_prop_impr S  cdcl_bnb_stgy S S'

lemma ocdclW_o_induct[consumes 1, case_names decide skip resolve backtrack]:
  fixes S :: 'st
  assumes cdclW_restart: ocdclW_o S T and
    decideH: "L T. conflicting S = None  undefined_lit (trail S) L  
      atm_of L  atms_of_mm (init_clss S) 
      T  cons_trail (Decided L) S 
      P S T" and
    skipH: "L C' M E T.
      trail S = Propagated L C' # M 
      conflicting S = Some E 
      -L ∉# E  E  {#} 
      T  tl_trail S 
      P S T" and
    resolveH: "L E M D T.
      trail S = Propagated L E # M 
      L ∈# E 
      hd_trail S = Propagated L E 
      conflicting S = Some D 
      -L ∈# D 
      get_maximum_level (trail S) ((remove1_mset (-L) D)) = backtrack_lvl S 
      T  update_conflicting
        (Some (resolve_cls L D E)) (tl_trail S) 
      P S T" and
    backtrackH: "L D K i M1 M2 T D'.
      conflicting S = Some (add_mset L D) 
      (Decided K # M1, M2)  set (get_all_ann_decomposition (trail S)) 
      get_level (trail S) L = backtrack_lvl S 
      get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') 
      get_maximum_level (trail S) D'  i 
      get_level (trail S) K = i+1 
      D' ⊆# D 
      clauses S + conflicting_clss S ⊨pm add_mset L D' 
      T  cons_trail (Propagated L (add_mset L D'))
            (reduce_trail_to M1
              (add_learned_cls (add_mset L D')
                (update_conflicting None S))) 
       P S T"
  shows P S T
  using cdclW_restart apply (induct T rule: ocdclW_o.induct)
  subgoal using assms(2) by (auto elim: decideE; fail)
  subgoal apply (elim cdcl_bnb_bjE skipE resolveE obacktrackE)
    apply (frule skipH; simp; fail)
    apply (cases trail S; auto elim!: resolveE intro!: resolveH; fail)
    apply (frule backtrackH; simp; fail)
    done
  done

lemma obacktrack_backtrackg: obacktrack S T  backtrackg S T
  unfolding obacktrack.simps backtrackg.simps
  by blast


subsubsection Pluging into normal CDCL

lemma cdcl_bnb_no_more_init_clss:
  cdcl_bnb S S'  init_clss S = init_clss S'
  by (induction rule: cdcl_bnb.cases)
    (auto simp: improvep.simps conflict.simps propagate.simps
      conflict_opt.simps ocdclW_o.simps obacktrack.simps skip.simps resolve.simps cdcl_bnb_bj.simps
      decide.simps)

lemma rtranclp_cdcl_bnb_no_more_init_clss:
  cdcl_bnb** S S'  init_clss S = init_clss S'
  by (induction rule: rtranclp_induct)
    (auto dest: cdcl_bnb_no_more_init_clss)

lemma conflict_opt_conflict:
  conflict_opt S T  cdclW_restart_mset.conflict (abs_state S) (abs_state T)
  by (induction rule: conflict_opt.cases)
    (auto intro!: cdclW_restart_mset.conflict_rule[of _ negate_ann_lits (trail S)]
      simp: cdclW_restart_mset.clauses_def cdclW_restart_mset_state
      true_annots_true_cls_def_iff_negation_in_model abs_state_def
      in_negate_trial_iff)

lemma conflict_conflict:
  conflict S T  cdclW_restart_mset.conflict (abs_state S) (abs_state T)
  by (induction rule: conflict.cases)
    (auto intro!: cdclW_restart_mset.conflict_rule
      simp: clauses_def cdclW_restart_mset.clauses_def cdclW_restart_mset_state
      true_annots_true_cls_def_iff_negation_in_model abs_state_def
      in_negate_trial_iff)


lemma propagate_propagate:
  propagate S T  cdclW_restart_mset.propagate (abs_state S) (abs_state T)
  by (induction rule: propagate.cases)
    (auto intro!: cdclW_restart_mset.propagate_rule
      simp: clauses_def cdclW_restart_mset.clauses_def cdclW_restart_mset_state
        true_annots_true_cls_def_iff_negation_in_model abs_state_def
        in_negate_trial_iff)

lemma decide_decide:
  decide S T  cdclW_restart_mset.decide (abs_state S) (abs_state T)
  by (induction rule: decide.cases)
    (auto intro!: cdclW_restart_mset.decide_rule
      simp: clauses_def cdclW_restart_mset.clauses_def cdclW_restart_mset_state
        true_annots_true_cls_def_iff_negation_in_model abs_state_def
        in_negate_trial_iff)

lemma skip_skip:
  skip S T  cdclW_restart_mset.skip (abs_state S) (abs_state T)
  by (induction rule: skip.cases)
    (auto intro!: cdclW_restart_mset.skip_rule
      simp: clauses_def cdclW_restart_mset.clauses_def cdclW_restart_mset_state
        true_annots_true_cls_def_iff_negation_in_model abs_state_def
        in_negate_trial_iff)

lemma resolve_resolve:
  resolve S T  cdclW_restart_mset.resolve (abs_state S) (abs_state T)
  by (induction rule: resolve.cases)
    (auto intro!: cdclW_restart_mset.resolve_rule
      simp: clauses_def cdclW_restart_mset.clauses_def cdclW_restart_mset_state
        true_annots_true_cls_def_iff_negation_in_model abs_state_def
        in_negate_trial_iff)

lemma backtrack_backtrack:
  obacktrack S T  cdclW_restart_mset.backtrack (abs_state S) (abs_state T)
proof (induction rule: obacktrack.cases)
  case (obacktrack_rule L D K M1 M2 D' i T)
  have H: set_mset (init_clss S)  set_mset (learned_clss S)
     set_mset (init_clss S)  set_mset (conflicting_clss S)  set_mset (learned_clss S)
    by auto
  have [simp]: cdclW_restart_mset.reduce_trail_to M1
       (trail S, init_clss S + conflicting_clss S, add_mset D (learned_clss S), None) =
    (M1, init_clss S + conflicting_clss S, add_mset D (learned_clss S), None) for D
    using obacktrack_rule by (auto simp add: cdclW_restart_mset_reduce_trail_to
        cdclW_restart_mset_state)
  show ?case
    using obacktrack_rule
    by (auto intro!: cdclW_restart_mset.backtrack.intros
        simp: cdclW_restart_mset_state abs_state_def clauses_def cdclW_restart_mset.clauses_def
          ac_simps)
qed

lemma ocdclW_o_all_rules_induct[consumes 1, case_names decide backtrack skip resolve]:
  fixes S T :: 'st
  assumes
    ocdclW_o S T and
    T. decide S T  P S T and
    T. obacktrack S T  P S T and
    T. skip S T  P S T and
    T. resolve S T  P S T
  shows P S T
  using assms by (induct T rule: ocdclW_o.induct) (auto simp: cdcl_bnb_bj.simps)

lemma cdclW_o_cdclW_o:
  ocdclW_o S S'  cdclW_restart_mset.cdclW_o (abs_state S) (abs_state S')
  apply (induction rule: ocdclW_o_all_rules_induct)
     apply (simp add: cdclW_restart_mset.cdclW_o.simps decide_decide; fail)
    apply (blast dest: backtrack_backtrack)
   apply (blast dest: skip_skip)
  by (blast dest: resolve_resolve)

lemma cdcl_bnb_stgy_all_struct_inv:
  assumes cdcl_bnb S T and cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
  using assms
proof (induction rule: cdcl_bnb.cases)
  case (cdcl_conflict S')
  then show ?case
    by (blast dest: conflict_conflict cdclW_restart_mset.cdclW_stgy.intros
      intro: cdclW_restart_mset.cdclW_stgy_cdclW_all_struct_inv)
next
  case (cdcl_propagate S')
  then show ?case
    by (blast dest: propagate_propagate cdclW_restart_mset.cdclW_stgy.intros
      intro: cdclW_restart_mset.cdclW_stgy_cdclW_all_struct_inv)
next
  case (cdcl_improve S')
  then show ?case
    using improve_cdclW_all_struct_inv by blast
next
  case (cdcl_conflict_opt S')
  then show ?case
    using conflict_opt_cdclW_all_struct_inv by blast
next
  case (cdcl_other' S')
  then show ?case
    by (meson cdclW_restart_mset.cdclW_all_struct_inv_inv cdclW_restart_mset.other cdclW_o_cdclW_o)
qed

lemma rtranclp_cdcl_bnb_stgy_all_struct_inv:
  assumes cdcl_bnb** S T and cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
  using assms by induction (auto dest: cdcl_bnb_stgy_all_struct_inv)


lemma cdcl_bnb_stgy_cdclW_or_improve:
  assumes cdcl_bnb S T and cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows (λS T. cdclW_restart_mset.cdclW (abs_state S) (abs_state T)  improvep S T) S T
  using assms
  apply (induction rule: cdcl_bnb.cases)
  apply (auto dest!: propagate_propagate conflict_conflict
    intro: cdclW_restart_mset.cdclW.intros simp add: cdclW_restart_mset.W_conflict conflict_opt_conflict
      cdclW_o_cdclW_o cdclW_restart_mset.W_other)
  done


lemma rtranclp_cdcl_bnb_stgy_cdclW_or_improve:
  assumes rtranclp cdcl_bnb S T and cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows (λS T. cdclW_restart_mset.cdclW (abs_state S) (abs_state T)  improvep S T)** S T
  using assms
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_bnb_stgy_cdclW_or_improve[of T U] rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T]
    by (smt rtranclp_unfold tranclp_unfold_end)
  done

lemma eq_diff_subset_iff: A = B + (A -B)  B ⊆# A
  by (metis mset_subset_eq_add_left subset_mset.add_diff_inverse)

lemma cdcl_bnb_conflicting_clss_mono:
  cdcl_bnb S T  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  
   conflicting_clss S ⊆# conflicting_clss T
  by (auto simp: cdcl_bnb.simps ocdclW_o.simps improvep.simps cdcl_bnb_bj.simps
    obacktrack.simps conflict_opt.simps conflicting_clss_update_weight_information_mono elim!: rulesE)


lemma cdcl_or_improve_cdclD:
  assumes cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    cdcl_bnb S T
  shows N.
      cdclW_restart_mset.cdclW** (trail S, init_clss S + N, learned_clss S, conflicting S) (abs_state T) 
      CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N
proof -
  have inv_T: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
    using assms(1) assms(2) cdcl_bnb_stgy_all_struct_inv by blast
  consider
     improvep S T |
     cdclW_restart_mset.cdclW (abs_state S) (abs_state T)
     using cdcl_bnb_stgy_cdclW_or_improve[of S T] assms by blast
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      using assms cdcl_bnb_stgy_cdclW_or_improve[of S T]
     unfolding abs_state_def cdcl_bnb_no_more_init_clss[of S T, OF assms(2)]
     by (auto simp: improvep.simps cdclW_restart_mset_state eq_diff_subset_iff)
  next
    case 2
    let ?S' = (trail S, init_clss S + (conflicting_clss S) + (conflicting_clss T - conflicting_clss S),
      learned_clss S, conflicting S)
    let ?S'' = (trail S, init_clss S + conflicting_clss T, learned_clss S, conflicting S)
    let ?T' = (trail T, init_clss T + (conflicting_clss T) + (conflicting_clss T - conflicting_clss S),
      learned_clss T, conflicting T)
    have subs: conflicting_clss S ⊆# conflicting_clss T
       using cdcl_bnb_conflicting_clss_mono[of S T] assms by fast
    then have H[simp]: set_mset (conflicting_clss T + (conflicting_clss T -
             conflicting_clss S)) = set_mset (conflicting_clss T)
        apply (auto simp flip: multiset_diff_union_assoc[OF subs])
        apply (subst (asm) multiset_diff_union_assoc[OF subs] set_mset_union)+
        apply (auto dest: in_diffD)
        apply (subst multiset_diff_union_assoc[OF subs] set_mset_union)+
        apply (auto dest: in_diffD)
        done
    have [simp]: set_mset (init_clss T + conflicting_clss T + conflicting_clss T -
             conflicting_clss S) = set_mset (init_clss T + conflicting_clss T)
        by (subst multiset_diff_union_assoc, (rule subs))
          (simp only: H ac_simps, subst set_mset_union, subst H, simp)
    have cdclW_restart_mset.cdclW_all_struct_inv ?T'
      by (rule cdclW_restart_mset.cdclW_all_struct_inv_clauses_cong[OF inv_T])
        (auto simp: cdclW_restart_mset_state eq_diff_subset_iff abs_state_def subs)
    then have cdclW_restart_mset.cdclW ?S' ?T'
      using 2 cdclW_restart_mset.cdclW_enlarge_clauses[of abs_state S abs_state T ?S' conflicting_clss T - conflicting_clss S {#}]
      by (auto simp: cdclW_restart_mset_state abs_state_def subs)
    then have cdclW_restart_mset.cdclW ?S'' (abs_state T)
      using cdclW_restart_mset.cdclW_clauses_cong[of ?S' ?T' ?S'']
       cdclW_restart_mset.cdclW_learnel_clss_mono[of ?S' ?T']
      cdclW_restart_mset.cdclW_restart_init_clss[OF cdclW_restart_mset.cdclW_cdclW_restart, of ?S' ?T']
      unfolding abs_state_def cdcl_bnb_no_more_init_clss[of S T, OF assms(2)]
      by (auto simp: cdclW_restart_mset_state abs_state_def subs)

    then show ?thesis
      by (auto intro!: exI[of _ conflicting_clss T] simp: abs_state_def init_clss.simps
        cdcl_bnb_no_more_init_clss[of S T, OF assms(2)])
  qed
qed

lemma rtranclp_cdcl_or_improve_cdclD:
  assumes cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    cdcl_bnb** S T
  shows N.
      cdclW_restart_mset.cdclW** (trail S, init_clss S + N, learned_clss S, conflicting S) (abs_state T) 
      CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N
  using assms(2,1)
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by (auto intro!: exI[of _ {#}] simp: abs_state_def init_clss.simps)
next
  case (step T U)
  then obtain N where
    st: cdclW_restart_mset.cdclW** (trail S, init_clss S + N, learned_clss S, conflicting S)
         (abs_state T) and
   eq: CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N
    by auto
  obtain N' where
    st': cdclW_restart_mset.cdclW** (trail T, init_clss T + N', learned_clss T, conflicting T)
         (abs_state U) and
   eq': CDCL_W_Abstract_State.init_clss (abs_state U) = init_clss T + N'
     using cdcl_or_improve_cdclD[of T U] rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T] step
     by (auto simp: cdclW_restart_mset_state)
  have inv_T: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
    using rtranclp_cdcl_bnb_stgy_all_struct_inv step.hyps(1) step.prems by blast
  have [simp]: init_clss S = init_clss T init_clss T = init_clss U
     using rtranclp_cdcl_bnb_no_more_init_clss[OF step(1)] cdcl_bnb_no_more_init_clss[OF step(2)]
     by fast+
  then have N ⊆# N'
    using eq eq' inv_T cdcl_bnb_conflicting_clss_mono[of T U] step
    by (auto simp: abs_state_def init_clss.simps)

  let ?S = (trail S, init_clss S + N, learned_clss S, conflicting S)
  let ?S' = (trail S, (init_clss S + N) + (N' - N), learned_clss S, conflicting S)
  let ?T' = (trail T, init_clss T + (conflicting_clss T) + (N' - N), learned_clss T, conflicting T)
  have cdclW_restart_mset.cdclW** ?S' ?T'
    using st eq cdclW_restart_mset.rtranclp_cdclW_enlarge_clauses[of ?S' ?S N' - N {#} abs_state T]
    by (auto simp: cdclW_restart_mset_state abs_state_def)
  moreover have init_clss T + (conflicting_clss T) + (N' - N) = init_clss T + N'
    using eq eq' N ⊆# N'
    by (auto simp: abs_state_def init_clss.simps)

  ultimately have
    cdclW_restart_mset.cdclW** (trail S, init_clss S + N', learned_clss S, conflicting S)
          (abs_state U)
    using eq' st' N ⊆# N' unfolding abs_state_def
    by auto
  then show ?case
    using eq' st' by (auto intro!: exI[of _ N'])
qed

definition cdcl_bnb_struct_invs :: 'st  bool where
cdcl_bnb_struct_invs S 
   atms_of_mm (conflicting_clss S)  atms_of_mm (init_clss S)

lemma cdcl_bnb_cdcl_bnb_struct_invs:
  cdcl_bnb S T  cdcl_bnb_struct_invs S  cdcl_bnb_struct_invs T
  using atms_of_conflicting_clss[of update_weight_information _ S] apply -
  by (induction rule: cdcl_bnb.induct)
    (force simp: improvep.simps conflict.simps propagate.simps
      conflict_opt.simps ocdclW_o.simps obacktrack.simps skip.simps resolve.simps
      cdcl_bnb_bj.simps decide.simps cdcl_bnb_struct_invs_def)+

lemma rtranclp_cdcl_bnb_cdcl_bnb_struct_invs:
  cdcl_bnb** S T  cdcl_bnb_struct_invs S  cdcl_bnb_struct_invs T
  by (induction rule: rtranclp_induct) (auto dest: cdcl_bnb_cdcl_bnb_struct_invs)

lemma cdcl_bnb_stgy_cdcl_bnb: cdcl_bnb_stgy S T  cdcl_bnb S T
  by (auto simp: cdcl_bnb_stgy.simps intro: cdcl_bnb.intros)

lemma rtranclp_cdcl_bnb_stgy_cdcl_bnb: cdcl_bnb_stgy** S T  cdcl_bnb** S T
  by (induction rule: rtranclp_induct)
   (auto dest: cdcl_bnb_stgy_cdcl_bnb)

text The following does not hold, because we cannot guarantee the absence of conflict of
  smaller level after termimprove and termconflict_opt.
lemma cdcl_bnb_all_stgy_inv:
  assumes cdcl_bnb S T and cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    cdclW_restart_mset.cdclW_stgy_invariant (abs_state S)
  shows cdclW_restart_mset.cdclW_stgy_invariant (abs_state T)
  oops

lemma skip_conflict_is_false_with_level:
  assumes skip S T and
    struct_inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    confl_inv:conflict_is_false_with_level S
  shows conflict_is_false_with_level T
  using assms
proof induction
  case (skip_rule L C' M D T) note tr_S = this(1) and D = this(2) and T = this(5)
  have conflicting: cdclW_conflicting S and
    lev: cdclW_M_level_inv S
    using struct_inv unfolding cdclW_conflicting_def cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_M_level_inv_def cdclW_restart_mset.cdclW_conflicting_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  obtain La where
    La ∈# D and
    get_level (Propagated L C' # M) La = backtrack_lvl S
    using skip_rule confl_inv by auto
  moreover {
    have atm_of La  atm_of L
    proof (rule ccontr)
      assume ¬ ?thesis
      then have La: La = L using La ∈# D - L ∉# D
        by (auto simp add: atm_of_eq_atm_of)
      have Propagated L C' # M ⊨as CNot D
        using conflicting tr_S D unfolding cdclW_conflicting_def by auto
      then have -L  lits_of_l M
        using La ∈# D in_CNot_implies_uminus(2)[of L D Propagated L C' # M] unfolding La
        by auto
      then show False using lev tr_S unfolding cdclW_M_level_inv_def consistent_interp_def by auto
    qed
    then have get_level (Propagated L C' # M) La = get_level M La by auto
  }
  ultimately show ?case using D tr_S T by auto
qed

lemma propagate_conflict_is_false_with_level:
  assumes propagate S T and
    struct_inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    confl_inv:conflict_is_false_with_level S
  shows conflict_is_false_with_level T
  using assms by (induction rule: propagate.induct) auto

lemma cdclW_o_conflict_is_false_with_level:
  assumes cdclW_o S T and
    struct_inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    confl_inv: conflict_is_false_with_level S
  shows conflict_is_false_with_level T
  apply (rule cdclW_o_conflict_is_false_with_level_inv[of S T])
  subgoal using assms by auto
  subgoal using struct_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_M_level_inv_def cdclW_restart_mset.cdclW_M_level_inv_def
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  subgoal using assms by auto
  subgoal using struct_inv unfolding distinct_cdclW_state_def
      cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset.distinct_cdclW_state_def
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  subgoal using struct_inv unfolding cdclW_conflicting_def
      cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset.cdclW_conflicting_def
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  done

lemma cdclW_o_no_smaller_confl:
  assumes cdclW_o S T and
    struct_inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    confl_inv: no_smaller_confl S and
    lev: conflict_is_false_with_level S and
    n_s: no_confl_prop_impr S
  shows no_smaller_confl T
  apply (rule cdclW_o_no_smaller_confl_inv[of S T])
  subgoal using assms by (auto dest!:cdclW_o_cdclW_o)[]
  subgoal using n_s by auto
  subgoal using struct_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_M_level_inv_def cdclW_restart_mset.cdclW_M_level_inv_def
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  subgoal using lev by fast
  subgoal using confl_inv unfolding distinct_cdclW_state_def
      cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset.distinct_cdclW_state_def
      cdclW_restart_mset.no_smaller_confl_def
    by (auto simp: abs_state_def cdclW_restart_mset_state clauses_def)
  done

declare cdclW_restart_mset.conflict_is_false_with_level_def [simp del]

lemma improve_conflict_is_false_with_level:
  assumes improvep S T and conflict_is_false_with_level S
  shows conflict_is_false_with_level T
  using assms
  by induction (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
        abs_state_def cdclW_restart_mset_state in_negate_trial_iff Bex_def negate_ann_lits_empty_iff
        intro!: exI[of _ -lit_of (hd M)])

declare conflict_is_false_with_level_def[simp del]

lemma cdclW_M_level_inv_cdclW_M_level_inv[iff]:
  cdclW_restart_mset.cdclW_M_level_inv (abs_state S) = cdclW_M_level_inv S
  by (auto simp: cdclW_restart_mset.cdclW_M_level_inv_def
      cdclW_M_level_inv_def cdclW_restart_mset_state)

lemma obacktrack_state_eq_compatible:
  assumes
    bt: obacktrack S T and
    SS': S  S' and
    TT': T  T'
  shows obacktrack S' T'
proof -
  obtain D L K i M1 M2 D' where
    conf: conflicting S = Some (add_mset L D) and
    decomp: (Decided K # M1, M2)  set (get_all_ann_decomposition (trail S)) and
    lev: get_level (trail S) L = backtrack_lvl S and
    max: get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') and
    max_D: get_maximum_level (trail S) D'  i and
    lev_K: get_level (trail S) K = Suc i and
    D'_D: D' ⊆# D and
    NU_DL: clauses S + conflicting_clss S ⊨pm add_mset L D' and
    T: "T  cons_trail (Propagated L (add_mset L D'))
                (reduce_trail_to M1
                  (add_learned_cls (add_mset L D')
                    (update_conflicting None S)))"
    using bt by (elim obacktrackE) force
  let ?D = add_mset L D
  let ?D' = add_mset L D'
  have D': conflicting S' = Some ?D
    using SS' conf by (cases conflicting S') auto

  have T'_S: "T'  cons_trail (Propagated L ?D')
     (reduce_trail_to M1 (add_learned_cls ?D'
     (update_conflicting None S)))"
    using T TT' state_eq_sym state_eq_trans by blast
  have T': "T'  cons_trail (Propagated L ?D')
     (reduce_trail_to M1 (add_learned_cls ?D'
     (update_conflicting None S')))"
    apply (rule state_eq_trans[OF T'_S])
    by (auto simp: cons_trail_state_eq reduce_trail_to_state_eq add_learned_cls_state_eq
        update_conflicting_state_eq SS')
  show ?thesis
    apply (rule obacktrack_rule[of _ L D K M1 M2 D' i])
    subgoal by (rule D')
    subgoal using TT' decomp SS' by auto
    subgoal using lev TT'  SS' by auto
    subgoal using max TT' SS' by auto
    subgoal using max_D TT' SS' by auto
    subgoal using lev_K TT' SS' by auto
    subgoal by (rule D'_D)
    subgoal using NU_DL TT' SS' by auto
    subgoal by (rule T')
    done
qed

lemma ocdclW_o_no_smaller_confl_inv:
  fixes S S' :: 'st
  assumes
    ocdclW_o S S' and
    n_s: no_step conflict S and
    lev: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    max_lev: conflict_is_false_with_level S and
    smaller: no_smaller_confl S
  shows no_smaller_confl S'
  using assms(1,2) unfolding no_smaller_confl_def
proof (induct rule: ocdclW_o_induct)
  case (decide L T) note confl = this(1) and undef = this(2) and T = this(4)
  have [simp]: clauses T = clauses S
    using T undef by auto
  show ?case
  proof (intro allI impI)
    fix M'' K M' Da
    assume trail T = M'' @ Decided K # M' and D: Da ∈# local.clauses T
    then have "trail S = tl M'' @ Decided K # M'
         (M'' = []  Decided K # M' = Decided L # trail S)"
      using T undef by (cases M'') auto
    moreover {
      assume trail S = tl M'' @ Decided K # M'
      then have ¬M' ⊨as CNot Da
        using D T undef confl smaller unfolding no_smaller_confl_def smaller by fastforce
    }
    moreover {
      assume Decided K # M' = Decided L # trail S
      then have ¬M' ⊨as CNot Da using smaller D confl T n_s by (auto simp: conflict.simps)
    }
    ultimately show ¬M' ⊨as CNot Da by fast
  qed
next
  case resolve
  then show ?case using smaller max_lev unfolding no_smaller_confl_def by auto
next
  case skip
  then show ?case using smaller max_lev unfolding no_smaller_confl_def by auto
next
  case (backtrack L D K i M1 M2 T D') note confl = this(1) and decomp = this(2) and
    T = this(9)
  obtain c where M: trail S = c @ M2 @ Decided K # M1
    using decomp by auto

  show ?case
  proof (intro allI impI)
    fix M ia K' M' Da
    assume trail T = M' @ Decided K' # M
    then have M1 = tl M' @ Decided K' # M
      using T decomp lev by (cases M') (auto simp: cdclW_M_level_inv_decomp)
    let ?D' = add_mset L D'
    let ?S' = "(cons_trail (Propagated L ?D')
                  (reduce_trail_to M1 (add_learned_cls ?D' (update_conflicting None S))))"
    assume D: Da ∈# clauses T
    moreover{
      assume Da ∈# clauses S
      then have ¬M ⊨as CNot Da using M1 = tl M' @ Decided K' # M M confl smaller
        unfolding no_smaller_confl_def by auto
    }
    moreover {
      assume Da: Da = add_mset L D'
      have ¬M ⊨as CNot Da
      proof (rule ccontr)
        assume ¬ ?thesis
        then have -L  lits_of_l M
          unfolding Da by (simp add: in_CNot_implies_uminus(2))
        then have -L  lits_of_l (Propagated L D # M1)
          using UnI2 M1 = tl M' @ Decided K' # M
          by auto
        moreover {
          have obacktrack S ?S'
            using obacktrack_rule[OF backtrack.hyps(1-8) T] obacktrack_state_eq_compatible[of S T S] T
            by force
          then have cdcl_bnb S ?S'
            by (auto dest!: cdcl_bnb_bj.intros ocdclW_o.intros intro: cdcl_bnb.intros)
          then have cdclW_restart_mset.cdclW_all_struct_inv (abs_state ?S')
            using cdcl_bnb_stgy_all_struct_inv[of S, OF _ lev] by fast
          then have cdclW_restart_mset.cdclW_M_level_inv (abs_state ?S')
            by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
          then have no_dup (Propagated L D # M1)
            using decomp lev unfolding cdclW_restart_mset.cdclW_M_level_inv_def by auto
        }
        ultimately show False
          using Decided_Propagated_in_iff_in_lits_of_l defined_lit_map
          by (auto simp: no_dup_def)
      qed
    }
    ultimately show ¬M ⊨as CNot Da
      using T decomp lev unfolding cdclW_M_level_inv_def by fastforce
  qed
qed

lemma cdcl_bnb_stgy_no_smaller_confl:
  assumes cdcl_bnb_stgy S T and
    cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    no_smaller_confl S and
    conflict_is_false_with_level S
  shows no_smaller_confl T
  using assms
proof (induction rule: cdcl_bnb_stgy.cases)
  case (cdcl_bnb_other' S')
  show ?case
    by (rule ocdclW_o_no_smaller_confl_inv)
     (use cdcl_bnb_other' in auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
qed (auto intro: conflict_no_smaller_confl_inv propagate_no_smaller_confl_inv;
  auto simp: no_smaller_confl_def improvep.simps conflict_opt.simps)+

lemma ocdclW_o_conflict_is_false_with_level_inv:
  assumes
    ocdclW_o S S' and
    lev: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    confl_inv: conflict_is_false_with_level S
  shows conflict_is_false_with_level S'
  using assms(1,2)
proof (induct rule: ocdclW_o_induct)
  case (resolve L C M D T) note tr_S = this(1) and confl = this(4) and LD = this(5) and T = this(7)

  have resolve S T
    using resolve.intros[of S L C D T] resolve
    by auto
  then have cdclW_restart_mset.resolve (abs_state S) (abs_state T)
    by (simp add: resolve_resolve)
  moreover have cdclW_restart_mset.conflict_is_false_with_level (abs_state S)
    using confl_inv
    by (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
      conflict_is_false_with_level_def abs_state_def cdclW_restart_mset_state)
  ultimately have cdclW_restart_mset.conflict_is_false_with_level (abs_state T)
    using cdclW_restart_mset.cdclW_o_conflict_is_false_with_level_inv[of abs_state S abs_state T]
    lev confl_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    by (auto dest!: cdclW_restart_mset.cdclW_o.intros
      cdclW_restart_mset.cdclW_bj.intros)
  then show ?case
    by (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
      conflict_is_false_with_level_def abs_state_def cdclW_restart_mset_state)
next
  case (skip L C' M D T) note tr_S = this(1) and D = this(2) and T = this(5)
  have cdclW_restart_mset.skip (abs_state S) (abs_state T)
     using skip.intros[of S L C' M D T] skip by (simp add: skip_skip)
  moreover have cdclW_restart_mset.conflict_is_false_with_level (abs_state S)
    using confl_inv
    by (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
      conflict_is_false_with_level_def abs_state_def cdclW_restart_mset_state)
  ultimately have cdclW_restart_mset.conflict_is_false_with_level (abs_state T)
    using  cdclW_restart_mset.cdclW_o_conflict_is_false_with_level_inv[of abs_state S abs_state T]
    lev confl_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    by (auto dest!: cdclW_restart_mset.cdclW_o.intros cdclW_restart_mset.cdclW_bj.intros)
  then show ?case
    by (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
      conflict_is_false_with_level_def abs_state_def cdclW_restart_mset_state)
next
  case backtrack
  then show ?case
    by (auto split: if_split_asm simp: cdclW_M_level_inv_decomp lev conflict_is_false_with_level_def)
qed (auto simp: conflict_is_false_with_level_def)


lemma cdcl_bnb_stgy_conflict_is_false_with_level:
  assumes cdcl_bnb_stgy S T and
    cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    no_smaller_confl S and
    conflict_is_false_with_level S
  shows conflict_is_false_with_level T
  using assms
proof (induction rule: cdcl_bnb_stgy.cases)
  case (cdcl_bnb_conflict S')
  then show ?case
    using conflict_conflict_is_false_with_level
    by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
next
  case (cdcl_bnb_propagate S')
  then show ?case
    using propagate_conflict_is_false_with_level
    by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
next
  case (cdcl_bnb_improve S')
  then show ?case
    using improve_conflict_is_false_with_level by blast
next
  case (cdcl_bnb_conflict_opt S')
  then show ?case
    using conflict_opt_no_smaller_conflict(2) by blast
next
  case (cdcl_bnb_other' S')
  show ?case
    apply (rule ocdclW_o_conflict_is_false_with_level_inv)
    using cdcl_bnb_other' by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
qed

lemma decided_cons_eq_append_decide_cons: Decided L # MM = M' @ Decided K # M 
  (M'  []  hd M' = Decided L  MM = tl M' @ Decided K # M) 
  (M' = []  L = K  MM = M)
  by (cases M') auto

lemma either_all_false_or_earliest_decomposition:
  shows (K K'. L = K' @ K  ¬P K) 
      (L' L''. L = L'' @ L'  P L'  (K K'. L' = K' @ K  K'  []  ¬P K))
  apply (induction L)
  subgoal by auto
  subgoal for a
    by (metis append_Cons append_Nil list.sel(3) tl_append2)
  done

lemma trail_is_improving_Ex_improve:
  assumes confl: conflicting S = None and
    imp: is_improving (trail S) M' S
  shows Ex (improvep S)
  using assms
  by (auto simp: improvep.simps intro!: exI)

definition cdcl_bnb_stgy_inv :: 'st  bool where
  cdcl_bnb_stgy_inv S  conflict_is_false_with_level S  no_smaller_confl S

lemma cdcl_bnb_stgy_invD:
  shows cdcl_bnb_stgy_inv S  cdclW_stgy_invariant S
  unfolding cdclW_stgy_invariant_def cdcl_bnb_stgy_inv_def
  by auto

lemma cdcl_bnb_stgy_stgy_inv:
  cdcl_bnb_stgy S T  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) 
    cdcl_bnb_stgy_inv S  cdcl_bnb_stgy_inv T
  using cdclW_stgy_cdclW_stgy_invariant[of S T]
     cdcl_bnb_stgy_conflict_is_false_with_level cdcl_bnb_stgy_no_smaller_confl
  unfolding cdcl_bnb_stgy_inv_def
  by blast

lemma rtranclp_cdcl_bnb_stgy_stgy_inv:
  cdcl_bnb_stgy** S T  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) 
    cdcl_bnb_stgy_inv S  cdcl_bnb_stgy_inv T
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_bnb_stgy_stgy_inv rtranclp_cdcl_bnb_stgy_all_struct_inv
      rtranclp_cdcl_bnb_stgy_cdcl_bnb by blast
  done

lemma cdcl_bnb_cdclW_learned_clauses_entailed_by_init:
  assumes
    cdcl_bnb S T and
    entailed: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state S) and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state T)
  using assms(1)
proof (induction rule: cdcl_bnb.cases)
  case (cdcl_conflict S')
  then show ?case
    using entailed
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
        elim!: conflictE)
next
  case (cdcl_propagate S')
  then show ?case
    using entailed
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
        elim!: propagateE)
next
  case (cdcl_improve S')
  moreover have set_mset (CDCL_W_Abstract_State.init_clss (abs_state S)) 
    set_mset (CDCL_W_Abstract_State.init_clss (abs_state (update_weight_information M' S)))
       if is_improving M M' S for M M'
    using that conflicting_clss_update_weight_information_mono[OF all_struct]
    by (auto simp: abs_state_def cdclW_restart_mset_state)
  ultimately show ?case
    using entailed
    by (fastforce simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
        elim!: improveE intro: true_clss_clss_subsetI)
next
  case (cdcl_other' S') note T = this(1) and o = this(2)
  show ?case
    apply (rule cdclW_restart_mset.cdclW_learned_clauses_entailed[of abs_state S])
    subgoal using o unfolding T by (blast dest: cdclW_o_cdclW_o cdclW_restart_mset.other)
    subgoal using all_struct unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast
    subgoal using entailed by fast
    done
next
  case (cdcl_conflict_opt S')
  then show ?case
    using entailed
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
        elim!: conflict_optE)
qed

lemma rtranclp_cdcl_bnb_cdclW_learned_clauses_entailed_by_init:
  assumes
    cdcl_bnb** S T and
    entailed: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state S) and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state T)
  using assms by (induction rule: rtranclp_induct)
   (auto intro: cdcl_bnb_cdclW_learned_clauses_entailed_by_init
      rtranclp_cdcl_bnb_stgy_all_struct_inv)

lemma atms_of_init_clss_conflicting_clss2[simp]:
  atms_of_mm (init_clss S)  atms_of_mm (conflicting_clss S) = atms_of_mm (init_clss S)
  using atms_of_conflicting_clss[of S] by blast

lemma no_strange_atm_no_strange_atm[simp]:
  cdclW_restart_mset.no_strange_atm (abs_state S) = no_strange_atm S
  using atms_of_conflicting_clss[of S]
  unfolding cdclW_restart_mset.no_strange_atm_def no_strange_atm_def
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma cdclW_conflicting_cdclW_conflicting[simp]:
  cdclW_restart_mset.cdclW_conflicting (abs_state S) = cdclW_conflicting S
  unfolding cdclW_restart_mset.cdclW_conflicting_def cdclW_conflicting_def
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma distinct_cdclW_state_distinct_cdclW_state:
  cdclW_restart_mset.distinct_cdclW_state (abs_state S)  distinct_cdclW_state S
  unfolding cdclW_restart_mset.distinct_cdclW_state_def distinct_cdclW_state_def
  by (auto simp: abs_state_def cdclW_restart_mset_state)

lemma obacktrack_imp_backtrack:
  obacktrack S T  cdclW_restart_mset.backtrack (abs_state S) (abs_state T)
  by (elim obacktrackE, rule_tac D=D and L=L and K=K in cdclW_restart_mset.backtrack.intros)
    (auto elim!: obacktrackE simp: cdclW_restart_mset.backtrack.simps sim_abs_state_simp)

lemma backtrack_imp_obacktrack:
  cdclW_restart_mset.backtrack (abs_state S) T  Ex (obacktrack S)
  by (elim cdclW_restart_mset.backtrackE, rule exI,
       rule_tac D=D and L=L and K=K in obacktrack.intros)
    (auto simp: cdclW_restart_mset.backtrack.simps obacktrack.simps)

lemma cdclW_same_weight: cdclW S U  weight S = weight U
  by (induction rule: cdclW.induct)
    (auto simp: improvep.simps cdclW.simps
        propagate.simps sim_abs_state_simp abs_state_def cdclW_restart_mset_state
        clauses_def conflict.simps cdclW_o.simps decide.simps cdclW_bj.simps
        skip.simps resolve.simps backtrack.simps)

lemma ocdclW_o_same_weight: ocdclW_o S U  weight S = weight U
  by (induction rule: ocdclW_o.induct)
    (auto simp: improvep.simps cdclW.simps cdcl_bnb_bj.simps
        propagate.simps sim_abs_state_simp abs_state_def cdclW_restart_mset_state
        clauses_def conflict.simps cdclW_o.simps decide.simps cdclW_bj.simps
        skip.simps resolve.simps obacktrack.simps)

text This is a proof artefact: it is easier to reason on termimprovep when the set of
  initial clauses is fixed (here by termN). The next theorem shows that the conclusion
  is equivalent to not fixing the set of clauses.
lemma wf_cdcl_bnb: (* \htmllink{wf_cdcl_bnb} *)
  assumes improve: S T. improvep S T  init_clss S = N  (ν (weight T), ν (weight S))  R and
    wf_R: wf R
  shows wf {(T, S). cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  cdcl_bnb S T 
      init_clss S = N}
    (is wf ?A)
proof -
  let ?R = {(T, S). (ν (weight T), ν (weight S))  R}

  have wf {(T, S).  cdclW_restart_mset.cdclW_all_struct_inv S  cdclW_restart_mset.cdclW S T}
    by (rule cdclW_restart_mset.wf_cdclW)
  from wf_if_measure_f[OF this, of abs_state]
  have wf: wf {(T, S).  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) 
      cdclW_restart_mset.cdclW (abs_state S) (abs_state T)  weight S = weight T}
    (is wf ?CDCL)
    by (rule wf_subset) auto
  have wf (?R  ?CDCL)
    apply (rule wf_union_compatible)
    subgoal by (rule wf_if_measure_f[OF wf_R, of λx. ν (weight x)])
    subgoal by (rule wf)
    subgoal by (auto simp: cdclW_same_weight)
    done

  moreover have ?A  ?R  ?CDCL
    by (auto dest: cdclW.intros cdclW_restart_mset.W_propagate cdclW_restart_mset.W_other
          conflict_conflict propagate_propagate decide_decide improve conflict_opt_conflict
          cdclW_o_cdclW_o cdclW_restart_mset.W_conflict W_conflict cdclW_o.intros cdclW.intros
          cdclW_o_cdclW_o
        simp: cdclW_same_weight cdcl_bnb.simps ocdclW_o_same_weight
        elim: conflict_optE)
  ultimately show ?thesis
    by (rule wf_subset)
qed

corollary wf_cdcl_bnb_fixed_iff:
  shows (N. wf {(T, S). cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  cdcl_bnb S T
        init_clss S = N}) 
     wf {(T, S). cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  cdcl_bnb S T}
    (is (N. wf (?A N))  wf ?B)
proof
  assume wf ?B
  then show N. wf (?A N)
    by (intro allI, rule wf_subset) auto
next
  assume N. wf (?A N)
  show wf ?B
    unfolding wf_iff_no_infinite_down_chain
  proof
    assume f. i. (f (Suc i), f i)  ?B
    then obtain f where f: (f (Suc i), f i)  ?B for i
      by blast
    then have cdclW_restart_mset.cdclW_all_struct_inv (abs_state (f n)) for n
      by (induction n) auto
    with f have st: cdcl_bnb** (f 0) (f n) for n
      apply (induction n)
      subgoal by auto
      subgoal by (subst rtranclp_unfold,subst tranclp_unfold_end)
         auto
      done
    let ?N = init_clss (f 0)
    have N: init_clss (f n) = ?N for n
      using st[of n] by (auto dest: rtranclp_cdcl_bnb_no_more_init_clss)
    have (f (Suc i), f i)  ?A ?N for i
      using f N by auto
    with N. wf (?A N) show False
      unfolding wf_iff_no_infinite_down_chain by blast
  qed
qed

text The following is a slightly more restricted version of the theorem, because it makes it possible
to add some specific invariant, which can be useful when the proof of the decreasing is complicated.

lemma wf_cdcl_bnb_with_additional_inv:
  assumes improve: S T. improvep S T  P S  init_clss S = N  (ν (weight T), ν (weight S))  R and
    wf_R: wf R and
    S T. cdcl_bnb S T  P S  init_clss S = N  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  P T
  shows wf {(T, S). cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)  cdcl_bnb S T  P S 
      init_clss S = N}
    (is wf ?A)
proof -
  let ?R = {(T, S). (ν (weight T), ν (weight S))  R}

  have wf {(T, S).  cdclW_restart_mset.cdclW_all_struct_inv S  cdclW_restart_mset.cdclW S T}
    by (rule cdclW_restart_mset.wf_cdclW)
  from wf_if_measure_f[OF this, of abs_state]
  have wf: wf {(T, S).  cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) 
      cdclW_restart_mset.cdclW (abs_state S) (abs_state T)  weight S = weight T}
    (is wf ?CDCL)
    by (rule wf_subset) auto
  have wf (?R  ?CDCL)
    apply (rule wf_union_compatible)
    subgoal by (rule wf_if_measure_f[OF wf_R, of λx. ν (weight x)])
    subgoal by (rule wf)
    subgoal by (auto simp: cdclW_same_weight)
    done

  moreover have ?A  ?R  ?CDCL
    using assms(3) cdcl_bnb.intros(3)
    by (auto dest: cdclW.intros cdclW_restart_mset.W_propagate cdclW_restart_mset.W_other
          conflict_conflict propagate_propagate decide_decide improve conflict_opt_conflict
          cdclW_o_cdclW_o cdclW_restart_mset.W_conflict W_conflict cdclW_o.intros cdclW.intros
          cdclW_o_cdclW_o
        simp: cdclW_same_weight cdcl_bnb.simps ocdclW_o_same_weight
        elim: conflict_optE)
  ultimately show ?thesis
    by (rule wf_subset)
qed


lemma conflict_is_false_with_level_abs_iff:
  cdclW_restart_mset.conflict_is_false_with_level (abs_state S) 
    conflict_is_false_with_level S
  by (auto simp: cdclW_restart_mset.conflict_is_false_with_level_def
    conflict_is_false_with_level_def)

lemma decide_abs_state_decide:
  cdclW_restart_mset.decide (abs_state S) T  cdcl_bnb_struct_invs S  Ex(decide S)
  apply (cases rule: cdclW_restart_mset.decide.cases, assumption)
  subgoal for L
    apply (rule exI)
    apply (rule decide.intros[of _ L])
    by (auto simp: cdcl_bnb_struct_invs_def abs_state_def cdclW_restart_mset_state)
  done

lemma cdcl_bnb_no_conflicting_clss_cdclW:
  assumes cdcl_bnb S T and conflicting_clss T = {#}
  shows cdclW_restart_mset.cdclW (abs_state S) (abs_state T)  conflicting_clss S = {#}
  using assms
  by (auto simp: cdcl_bnb.simps conflict_opt.simps improvep.simps ocdclW_o.simps
      cdcl_bnb_bj.simps
    dest: conflict_conflict propagate_propagate decide_decide skip_skip resolve_resolve
      backtrack_backtrack
    intro: cdclW_restart_mset.W_conflict cdclW_restart_mset.W_propagate cdclW_restart_mset.W_other
    dest: conflicting_clss_update_weight_information_in
    elim: conflictE propagateE decideE skipE resolveE improveE obacktrackE)

lemma rtranclp_cdcl_bnb_no_conflicting_clss_cdclW:
  assumes cdcl_bnb** S T and conflicting_clss T = {#}
  shows cdclW_restart_mset.cdclW** (abs_state S) (abs_state T)  conflicting_clss S = {#}
  using assms
  by (induction rule: rtranclp_induct)
     (fastforce dest: cdcl_bnb_no_conflicting_clss_cdclW)+

lemma conflict_abs_ex_conflict_no_conflicting:
  assumes cdclW_restart_mset.conflict (abs_state S) T and conflicting_clss S = {#}
  shows T. conflict S T
  using assms by (auto simp: conflict.simps cdclW_restart_mset.conflict.simps abs_state_def
    cdclW_restart_mset_state clauses_def cdclW_restart_mset.clauses_def)

lemma propagate_abs_ex_propagate_no_conflicting:
  assumes cdclW_restart_mset.propagate (abs_state S) T and conflicting_clss S = {#}
  shows T. propagate S T
  using assms by (auto simp: propagate.simps cdclW_restart_mset.propagate.simps abs_state_def
    cdclW_restart_mset_state clauses_def cdclW_restart_mset.clauses_def)

lemma cdcl_bnb_stgy_no_conflicting_clss_cdclW_stgy:
  assumes cdcl_bnb_stgy S T and conflicting_clss T = {#}
  shows cdclW_restart_mset.cdclW_stgy (abs_state S) (abs_state T)
proof -
  have conflicting_clss S = {#}
    using cdcl_bnb_no_conflicting_clss_cdclW[of S T] assms
    by (auto dest: cdcl_bnb_stgy_cdcl_bnb)
  then show ?thesis
    using assms
    by (auto 7 5 simp: cdcl_bnb_stgy.simps conflict_opt.simps ocdclW_o.simps
        cdcl_bnb_bj.simps
      dest: conflict_conflict propagate_propagate decide_decide skip_skip resolve_resolve
        backtrack_backtrack
      dest: cdclW_restart_mset.cdclW_stgy.intros cdclW_restart_mset.cdclW_o.intros
      dest: conflicting_clss_update_weight_information_in
        conflict_abs_ex_conflict_no_conflicting
        propagate_abs_ex_propagate_no_conflicting
      intro: cdclW_restart_mset.cdclW_stgy.intros(3)
      elim: improveE)
qed

lemma rtranclp_cdcl_bnb_stgy_no_conflicting_clss_cdclW_stgy:
  assumes cdcl_bnb_stgy** S T and conflicting_clss T = {#}
  shows cdclW_restart_mset.cdclW_stgy** (abs_state S) (abs_state T)
  using assms apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_bnb_no_conflicting_clss_cdclW[of T U, OF cdcl_bnb_stgy_cdcl_bnb]
    by (auto dest: cdcl_bnb_stgy_no_conflicting_clss_cdclW_stgy)
  done


context
  assumes can_always_improve:
     S. trail S ⊨asm clauses S  no_step conflict_opt S 
       conflicting S = None 
       cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) 
       total_over_m (lits_of_l (trail S)) (set_mset (clauses S))  Ex (improvep S)
begin

text The following theorems states a non-obvious (and slightly subtle) property: The fact that there
  is no conflicting cannot be shown without additional assumption. However, the assumption that every
  model leads to an improvements implies that we end up with a conflict.
lemma no_step_cdcl_bnb_cdclW:
  assumes
    ns: no_step cdcl_bnb S and
    struct_invs: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
  shows no_step cdclW_restart_mset.cdclW (abs_state S)
proof -
  have ns_confl: no_step skip S  no_step resolve S  no_step obacktrack S and
    ns_nc: no_step conflict S no_step propagate S no_step improvep S no_step conflict_opt S
      no_step decide S
    using ns
    by (auto simp: cdcl_bnb.simps ocdclW_o.simps cdcl_bnb_bj.simps)
  have alien: cdclW_restart_mset.no_strange_atm (abs_state S)
    using struct_invs unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+

  have False if st: T. cdclW_restart_mset.cdclW (abs_state S) T
  proof (cases conflicting S = None)
    case True
    have total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))
      using ns_nc True apply - apply (rule ccontr)
      by (force simp: decide.simps total_over_m_def total_over_set_def
        Decided_Propagated_in_iff_in_lits_of_l)
    then have tot: total_over_m (lits_of_l (trail S)) (set_mset (clauses S))
      using alien unfolding cdclW_restart_mset.no_strange_atm_def
      by (auto simp: total_over_set_atm_of total_over_m_def clauses_def
        abs_state_def init_clss.simps learned_clss.simps trail.simps)
    then have trail S ⊨asm clauses S
      using ns_nc True unfolding true_annots_def apply -
      apply clarify
      subgoal for C
        using all_variables_defined_not_imply_cnot[of C trail S]
        by (fastforce simp: conflict.simps total_over_set_atm_of
        dest: multi_member_split)
      done
    from can_always_improve[OF this] have False
      using ns_nc True struct_invs tot by blast
    then show ?thesis
      by blast
  next
    case False
    have nss: no_step cdclW_restart_mset.skip (abs_state S)
       no_step cdclW_restart_mset.resolve (abs_state S)
       no_step cdclW_restart_mset.backtrack (abs_state S)
      using ns_confl by (force simp: cdclW_restart_mset.skip.simps skip.simps
        cdclW_restart_mset.resolve.simps resolve.simps
        dest: backtrack_imp_obacktrack)+
    then show ?thesis
      using that False by (auto simp: cdclW_restart_mset.cdclW.simps
        cdclW_restart_mset.propagate.simps cdclW_restart_mset.conflict.simps
        cdclW_restart_mset.cdclW_o.simps cdclW_restart_mset.decide.simps
        cdclW_restart_mset.cdclW_bj.simps)
  qed
  then show ?thesis by blast
qed


lemma no_step_cdcl_bnb_stgy:
  assumes
    n_s: no_step cdcl_bnb S and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    stgy_inv: cdcl_bnb_stgy_inv S
  shows conflicting S = None  conflicting S = Some {#}
proof (rule ccontr)
  assume ¬ ?thesis
  then obtain D where conflicting S = Some D and D  {#}
    by auto
  moreover have no_step cdclW_restart_mset.cdclW_stgy (abs_state S)
    using no_step_cdcl_bnb_cdclW[OF n_s all_struct]
    cdclW_restart_mset.cdclW_stgy_cdclW by blast
  moreover have le: cdclW_restart_mset.cdclW_learned_clause (abs_state S)
    using all_struct unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast
  ultimately show False
    using cdclW_restart_mset.conflicting_no_false_can_do_step[of abs_state S] all_struct stgy_inv le
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def cdcl_bnb_stgy_inv_def
    by (force dest: distinct_cdclW_state_distinct_cdclW_state
      simp: conflict_is_false_with_level_abs_iff)
qed

lemma no_step_cdcl_bnb_stgy_empty_conflict: (* \htmllink{no_step_cdcl_bnb_stgy_empty_conflict} *)
  assumes
    n_s: no_step cdcl_bnb S and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    stgy_inv: cdcl_bnb_stgy_inv S
  shows conflicting S = Some {#}
proof (rule ccontr)
  assume H: ¬ ?thesis
  have all_struct': cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)
    by (simp add: all_struct)
  have le: cdclW_restart_mset.cdclW_learned_clause (abs_state S)
    using all_struct
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def cdcl_bnb_stgy_inv_def
    by auto
  have conflicting S = None  conflicting S = Some {#}
    using no_step_cdcl_bnb_stgy[OF n_s all_struct' stgy_inv] .
  then have confl: conflicting S = None
    using H by blast
  have no_step cdclW_restart_mset.cdclW_stgy (abs_state S)
    using no_step_cdcl_bnb_cdclW[OF n_s all_struct]
    cdclW_restart_mset.cdclW_stgy_cdclW by blast
  then have entail: trail S ⊨asm clauses S
    using confl cdclW_restart_mset.cdclW_stgy_final_state_conclusive2[of abs_state S]
      all_struct stgy_inv le
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def cdcl_bnb_stgy_inv_def
    by (auto simp: conflict_is_false_with_level_abs_iff)
  have total_over_m (lits_of_l (trail S)) (set_mset (clauses S))
    using cdclW_restart_mset.no_step_cdclW_total[OF no_step_cdcl_bnb_cdclW, of S] all_struct n_s confl
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    by auto
  with can_always_improve entail confl all_struct
  show False
    using n_s by (auto simp: cdcl_bnb.simps)
qed

lemma full_cdcl_bnb_stgy_no_conflicting_clss_unsat: (* \htmllink{full_cdcl_bnb_stgy_no_conflicting_clss_unsat} *)
  assumes
    full: full cdcl_bnb_stgy S T and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    stgy_inv: cdcl_bnb_stgy_inv S and
    ent_init: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state S) and
    [simp]: conflicting_clss T = {#}
  shows unsatisfiable (set_mset (init_clss S))
proof -
  have ns: no_step cdcl_bnb_stgy T and
    st: cdcl_bnb_stgy** S T and
    st': cdcl_bnb** S T and
    ns': no_step cdcl_bnb T
    using full unfolding full_def apply (blast dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)+
    using full unfolding full_def
    by (metis cdcl_bnb.simps cdcl_bnb_conflict cdcl_bnb_conflict_opt cdcl_bnb_improve
      cdcl_bnb_other' cdcl_bnb_propagate no_confl_prop_impr.elims(3))
  have struct_T: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
  have [simp]: conflicting_clss S = {#}
    using rtranclp_cdcl_bnb_no_conflicting_clss_cdclW[OF st'] by auto
  have cdclW_restart_mset.cdclW_stgy** (abs_state S) (abs_state T)
    using rtranclp_cdcl_bnb_stgy_no_conflicting_clss_cdclW_stgy[OF st] by auto
  then have full cdclW_restart_mset.cdclW_stgy (abs_state S) (abs_state T)
    using no_step_cdcl_bnb_cdclW[OF ns' struct_T] unfolding full_def
    by (auto dest: cdclW_restart_mset.cdclW_stgy_cdclW)
  moreover have cdclW_restart_mset.no_smaller_confl (state_butlast S)
    using stgy_inv ent_init
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def conflict_is_false_with_level_abs_iff
      cdcl_bnb_stgy_inv_def conflict_is_false_with_level_abs_iff
      cdclW_restart_mset.cdclW_stgy_invariant_def
    by (auto simp: abs_state_def cdclW_restart_mset_state cdcl_bnb_stgy_inv_def
      no_smaller_confl_def cdclW_restart_mset.no_smaller_confl_def clauses_def
      cdclW_restart_mset.clauses_def)
  ultimately have "conflicting T = Some {#}  unsatisfiable (set_mset (init_clss S))
     conflicting T = None  trail T ⊨asm init_clss S"
    using cdclW_restart_mset.full_cdclW_stgy_inv_normal_form[of abs_state S abs_state T] all_struct
      stgy_inv ent_init
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def conflict_is_false_with_level_abs_iff
      cdcl_bnb_stgy_inv_def conflict_is_false_with_level_abs_iff
      cdclW_restart_mset.cdclW_stgy_invariant_def
    by (auto simp: abs_state_def cdclW_restart_mset_state cdcl_bnb_stgy_inv_def)
  moreover have cdcl_bnb_stgy_inv T
    using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
  ultimately show ?thesis
    using no_step_cdcl_bnb_stgy_empty_conflict[OF ns' struct_T] by auto

qed


lemma ocdclW_o_no_smaller_propa:
  assumes ocdclW_o S T and
    inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    smaller_propa: no_smaller_propa S and
    n_s: no_confl_prop_impr S
  shows no_smaller_propa T
  using assms(1)
proof cases
  case decide
  show ?thesis
    unfolding no_smaller_propa_def
  proof clarify
    fix M K M' D L
    assume
      tr: trail T = M' @ Decided K # M and
      D: D+{#L#} ∈# clauses T and
      undef: undefined_lit M L and
      M: M ⊨as CNot D
    then have Ex (propagate S)
      apply (cases M')
      using propagate_rule[of S D+{#L#} L cons_trail (Propagated L (D + {#L#})) S]
        smaller_propa decide
      by (auto simp: no_smaller_propa_def elim!: rulesE)
    then show False
      using n_s unfolding no_confl_prop_impr.simps by blast
  qed
next
  case bj
  then show ?thesis
  proof cases
    case skip
    then show ?thesis
      using assms no_smaller_propa_tl[of S T]
      by (auto simp: cdcl_bnb_bj.simps ocdclW_o.simps obacktrack.simps elim!: rulesE)
  next
    case resolve
    then show ?thesis
      using assms no_smaller_propa_tl[of S T]
      by (auto simp: cdcl_bnb_bj.simps ocdclW_o.simps obacktrack.simps elim!: rulesE)
  next
    case backtrack
    have inv_T: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
      using cdclW_restart_mset.cdclW_stgy_cdclW_all_struct_inv inv assms(1)
      using cdcl_bnb_stgy_all_struct_inv cdcl_other' by blast
    obtain D D' :: 'v clause and K L :: 'v literal and
      M1 M2 :: ('v, 'v clause) ann_lit list and i :: nat where
      conflicting S = Some (add_mset L D) and
      decomp: (Decided K # M1, M2)  set (get_all_ann_decomposition (trail S)) and
      get_level (trail S) L = backtrack_lvl S and
      get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') and
      i: get_maximum_level (trail S) D'  i and
      lev_K: get_level (trail S) K = i + 1 and
      D_D': D' ⊆# D and
      T: "T  cons_trail (Propagated L (add_mset L D'))
          (reduce_trail_to M1
            (add_learned_cls (add_mset L D')
              (update_conflicting None S)))"
      using backtrack by (auto elim!: obacktrackE)
    let ?D' = add_mset L D'
    have [simp]: trail (reduce_trail_to M1 S) = M1
      using decomp by auto
    obtain M'' c where M'': trail S = M'' @ tl (trail T) and c: M'' = c @ M2 @ [Decided K]
      using decomp T by auto
    have M1: M1 = tl (trail T) and tr_T: trail T = Propagated L ?D' # M1
      using decomp T by auto
    have lev_inv: cdclW_restart_mset.cdclW_M_level_inv (abs_state S)
      using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by auto
    then have lev_inv_T: cdclW_restart_mset.cdclW_M_level_inv (abs_state T)
      using inv_T unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by auto
    have n_d: no_dup (trail S)
      using lev_inv unfolding cdclW_restart_mset.cdclW_M_level_inv_def
      by (auto simp: abs_state_def trail.simps)
    have n_d_T: no_dup (trail T)
      using lev_inv_T unfolding cdclW_restart_mset.cdclW_M_level_inv_def
      by (auto simp: abs_state_def trail.simps)

    have i_lvl: i = backtrack_lvl T
      using no_dup_append_in_atm_notin[of c @ M2 Decided K # tl (trail T) K]
      n_d lev_K unfolding c M'' by (auto simp: image_Un tr_T)

    from backtrack show ?thesis
      unfolding no_smaller_propa_def
    proof clarify
      fix M K' M' E' L'
      assume
        tr: trail T = M' @ Decided K' # M and
        E: E'+{#L'#} ∈# clauses T and
        undef: undefined_lit M L' and
        M: M ⊨as CNot E'
      have False if D: add_mset L D' = add_mset L' E' and M_D: M ⊨as CNot E'
      proof -
        have i  0
          using i_lvl tr T by auto
        moreover {
          have M1 ⊨as CNot D'
            using inv_T tr_T unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
            cdclW_restart_mset.cdclW_conflicting_def
            by (force simp: abs_state_def trail.simps conflicting.simps)
          then have get_maximum_level M1 D' = i
            using T i n_d D_D' unfolding M'' tr_T
            by (subst (asm) get_maximum_level_skip_beginning)
              (auto dest: defined_lit_no_dupD dest!: true_annots_CNot_definedD) }
        ultimately obtain L_max where
          L_max_in: L_max ∈# D' and
          lev_L_max: get_level M1 L_max = i
          using i get_maximum_level_exists_lit_of_max_level[of D' M1]
          by (cases D') auto
        have count_dec_M: count_decided M < i
          using T i_lvl unfolding tr by auto
        have - L_max  lits_of_l M
        proof (rule ccontr)
          assume ¬ ?thesis
          then have undefined_lit (M' @ [Decided K']) L_max
            using n_d_T unfolding tr
            by (auto dest: in_lits_of_l_defined_litD dest: defined_lit_no_dupD simp: atm_of_eq_atm_of)
          then have get_level (tl M' @ Decided K' # M) L_max < i
            apply (subst get_level_skip)
             apply (cases M'; auto simp add: atm_of_eq_atm_of lits_of_def; fail)
            using count_dec_M count_decided_ge_get_level[of M L_max] by auto
          then show False
            using lev_L_max tr unfolding tr_T by (auto simp: propagated_cons_eq_append_decide_cons)
        qed
        moreover have - L  lits_of_l M
        proof (rule ccontr)
          define MM where MM = tl M'
          assume ¬ ?thesis
          then have - L  lits_of_l (M' @ [Decided K'])
            using n_d_T unfolding tr by (auto simp: lits_of_def no_dup_def)
          have undefined_lit (M' @ [Decided K']) L
            apply (rule no_dup_uminus_append_in_atm_notin)
            using n_d_T ¬ - L  lits_of_l M unfolding tr by auto
          moreover have M' = Propagated L ?D' # MM
            using tr_T MM_def by (metis hd_Cons_tl propagated_cons_eq_append_decide_cons tr)
          ultimately show False
            by simp
        qed
        moreover have L_max ∈# D'  L ∈# D'
          using D L_max_in by (auto split: if_splits)
        ultimately show False
          using M_D D by (auto simp: true_annots_true_cls true_clss_def add_mset_eq_add_mset)
      qed
      then show False
        using M'' smaller_propa tr undef M T E
        by (cases M') (auto simp: no_smaller_propa_def trivial_add_mset_remove_iff elim!: rulesE)
    qed
  qed
qed

lemma ocdclW_no_smaller_propa:
  assumes cdcl_bnb_stgy S T and
    inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    smaller_propa: no_smaller_propa S and
    n_s: no_confl_prop_impr S
  shows no_smaller_propa T
  using assms
  apply (cases)
  subgoal by (auto)
  subgoal by (auto)
  subgoal by (auto elim!: improveE simp: no_smaller_propa_def)
  subgoal by (auto elim!: conflict_optE simp: no_smaller_propa_def)
  subgoal using ocdclW_o_no_smaller_propa by fast
  done


text Unfortunately, we cannot reuse the proof we have alrealy done.
lemma ocdclW_no_relearning:
  assumes cdcl_bnb_stgy S T and
    inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    smaller_propa: no_smaller_propa S and
    n_s: no_confl_prop_impr S and
    dist: distinct_mset (clauses S)
  shows distinct_mset (clauses T)
  using assms(1)
proof cases
  case cdcl_bnb_conflict
  then show ?thesis using dist by (auto elim: rulesE)
next
  case cdcl_bnb_propagate
  then show ?thesis using dist by (auto elim: rulesE)
next
  case cdcl_bnb_improve
  then show ?thesis using dist by (auto elim: improveE)
next
  case cdcl_bnb_conflict_opt
  then show ?thesis using dist by (auto elim: conflict_optE)
next
  case cdcl_bnb_other'
  then show ?thesis
  proof cases
    case decide
    then show ?thesis using dist by (auto elim: rulesE)
  next
    case bj
    then show ?thesis
    proof cases
      case skip
      then show ?thesis using dist by (auto elim: rulesE)
    next
      case resolve
      then show ?thesis using dist by (auto elim: rulesE)
    next
      case backtrack
      have smaller_propa: M K M' D L.
        trail S = M' @ Decided K # M 
        D + {#L#} ∈# clauses S  undefined_lit M L  ¬ M ⊨as CNot D
        using smaller_propa unfolding no_smaller_propa_def by fast
      have inv: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
        using inv
        using cdclW_restart_mset.cdclW_stgy_cdclW_all_struct_inv inv assms(1)
        using cdcl_bnb_stgy_all_struct_inv cdcl_other' backtrack ocdclW_o.intros
        cdcl_bnb_bj.intros
        by blast
      then have n_d: no_dup (trail T) and
        ent: L mark a b.
          a @ Propagated L mark # b = trail T 
           b ⊨as CNot (remove1_mset L mark)  L ∈# mark
        unfolding cdclW_restart_mset.cdclW_M_level_inv_def
          cdclW_restart_mset.cdclW_all_struct_inv_def
           cdclW_restart_mset.cdclW_conflicting_def
        by (auto simp: abs_state_def trail.simps)
      show ?thesis
      proof (rule ccontr)
        assume H: ¬?thesis
        obtain D D' :: 'v clause and K L :: 'v literal and
          M1 M2 :: ('v, 'v clause) ann_lit list and i :: nat where
          conflicting S = Some (add_mset L D) and
          decomp: (Decided K # M1, M2)  set (get_all_ann_decomposition (trail S)) and
          get_level (trail S) L = backtrack_lvl S and
          get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') and
          i: get_maximum_level (trail S) D'  i and
          lev_K: get_level (trail S) K = i + 1 and
          D_D': D' ⊆# D and
          T: "T  cons_trail (Propagated L (add_mset L D'))
              (reduce_trail_to M1
                (add_learned_cls (add_mset L D')
                  (update_conflicting None S)))"
          using backtrack by (auto elim!: obacktrackE)
        from H T dist have LD': add_mset L D' ∈# clauses S
          by auto
        have ¬M1 ⊨as CNot D'
          using get_all_ann_decomposition_exists_prepend[OF decomp] apply (elim exE)
          by (rule smaller_propa[of _ @ M2 K M1 D' L])
            (use n_d T decomp LD' in auto)
        moreover have M1 ⊨as CNot D'
          using ent[of [] L add_mset L D' M1] T decomp by auto
        ultimately show False
          ..
      qed
    qed
  qed
qed


lemma full_cdcl_bnb_stgy_unsat:
  assumes
    st: full cdcl_bnb_stgy S T and
    all_struct: cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) and
    opt_struct: cdcl_bnb_struct_invs S and
    stgy_inv: cdcl_bnb_stgy_inv S
  shows
    unsatisfiable (set_mset (clauses T + conflicting_clss T))
proof -
  have ns: no_step cdcl_bnb_stgy T and
    st: cdcl_bnb_stgy** S T and
    st': cdcl_bnb** S T
    using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  have ns': no_step cdcl_bnb T
    by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
  have struct_T: cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
  have stgy_T: cdcl_bnb_stgy_inv T
    using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
  have confl: conflicting T = Some {#}
    using no_step_cdcl_bnb_stgy_empty_conflict[OF ns' struct_T stgy_T] .

  have cdclW_restart_mset.cdclW_learned_clause (abs_state T) and
    alien: cdclW_restart_mset.no_strange_atm (abs_state T)
    using struct_T unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+
  then have ent': set_mset (clauses T + conflicting_clss T) ⊨p {#}
    using confl unfolding cdclW_restart_mset.cdclW_learned_clause_alt_def
    by auto
  then show unsatisfiable (set_mset (clauses T + conflicting_clss T))
     unfolding true_clss_cls_def satisfiable_def by auto

qed

end

lemma cdcl_bnb_reasons_in_clauses:
  cdcl_bnb S T  reasons_in_clauses S  reasons_in_clauses T
  by (auto simp: cdcl_bnb.simps reasons_in_clauses_def ocdclW_o.simps
        cdcl_bnb_bj.simps get_all_mark_of_propagated_tl_proped
    elim!: rulesE improveE conflict_optE obacktrackE
    dest!: in_set_tlD get_all_ann_decomposition_exists_prepend)


lemma cdcl_bnb_pow2_n_learned_clauses:
  assumes distinct_mset_mset N
    cdcl_bnb** (init_state N) T
  shows size (learned_clss T)  2 ^ (card (atms_of_mm N))
proof -
  have H: cdclW_restart_mset.cdclW_all_struct_inv (abs_state (init_state N))
    using assms apply (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def
     cdclW_restart_mset.distinct_cdclW_state_def cdclW_restart_mset.cdclW_learned_clause_def
     cdclW_restart_mset.reasons_in_clauses_def)
    using assms by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def
     distinct_mset_mset_conflicting_clss
     cdclW_restart_mset.distinct_cdclW_state_def abs_state_def init_clss.simps)
  then obtain Na where Na:  cdclW_restart_mset.cdclW**
        (trail (init_state N), init_clss (init_state N) + Na,
         learned_clss (init_state N), conflicting (init_state N))
        (abs_state T) 
       CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss (init_state N) + Na
    using rtranclp_cdcl_or_improve_cdclD[OF H assms(2)] by auto
  moreover have cdclW_restart_mset.cdclW_all_struct_inv ([], N + Na, {#}, None)
    using assms Na rtranclp_cdcl_bnb_no_more_init_clss[OF assms(2)]
    apply (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def
     cdclW_restart_mset.distinct_cdclW_state_def cdclW_restart_mset.cdclW_learned_clause_def
     cdclW_restart_mset.reasons_in_clauses_def)
    using assms by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset_state
     distinct_mset_mset_conflicting_clss cdclW_restart_mset.no_strange_atm_def cdclW_restart_mset.cdclW_M_level_inv_def
     cdclW_restart_mset.cdclW_conflicting_def
     cdclW_restart_mset.distinct_cdclW_state_def abs_state_def init_clss.simps)
  ultimately show ?thesis
    using rtranclp_cdcl_bnb_no_more_init_clss[OF assms(2)]
    cdclW_restart_mset.cdcl_pow2_n_learned_clauses2[of N + Na abs_state T]
    by (auto simp: init_state.simps abs_state_def cdclW_restart_mset_state)
qed
end

end