Theory CDCL.CDCL_W_Abstract_State

theory CDCL_W_Abstract_State
imports CDCL_W_Full CDCL_W_Restart CDCL_W_Incremental

begin

section ‹Instantiation of Weidenbach's CDCL by Multisets›

text ‹We first instantiate the locale of Weidenbach's locale. Then we refine it to a 2-WL program.›

type_synonym 'v cdclW_restart_mset = "('v, 'v clause) ann_lit list ×
  'v clauses ×
  'v clauses ×
  'v clause option"

text ‹We use definition, otherwise we could not use the simplification theorems we have already
  shown.›
fun trail :: "'v cdclW_restart_mset ⇒ ('v, 'v clause) ann_lit list" where
"trail (M, _) = M"

fun init_clss :: "'v cdclW_restart_mset ⇒ 'v clauses" where
"init_clss (_, N, _) = N"

fun learned_clss :: "'v cdclW_restart_mset ⇒ 'v clauses" where
"learned_clss (_, _, U, _) = U"

fun conflicting :: "'v cdclW_restart_mset ⇒ 'v clause option" where
"conflicting (_, _, _, C) = C"

fun cons_trail :: "('v, 'v clause) ann_lit ⇒ 'v cdclW_restart_mset ⇒ 'v cdclW_restart_mset" where
"cons_trail L (M, R) = (L # M, R)"

fun tl_trail where
"tl_trail (M, R) = (tl M, R)"

fun add_learned_cls where
"add_learned_cls C (M, N, U, R) = (M, N, {#C#} + U, R)"

fun add_init_cls where
"add_init_cls C (M, N, U, R) = (M, {#C#} + N, U, R)"

fun remove_cls where
"remove_cls C (M, N, U, R) = (M, removeAll_mset C N, removeAll_mset C U, R)"

fun update_conflicting where
"update_conflicting D (M, N, U,  _) = (M, N, U, D)"

fun init_state where
"init_state N = ([], N, {#}, None)"

declare trail.simps[simp del] cons_trail.simps[simp del] tl_trail.simps[simp del]
  add_learned_cls.simps[simp del] remove_cls.simps[simp del]
  update_conflicting.simps[simp del] init_clss.simps[simp del] learned_clss.simps[simp del]
  conflicting.simps[simp del] init_state.simps[simp del]

lemmas cdclW_restart_mset_state = trail.simps cons_trail.simps tl_trail.simps add_learned_cls.simps
    remove_cls.simps update_conflicting.simps init_clss.simps learned_clss.simps
    conflicting.simps init_state.simps

definition state where
‹state S = (trail S, init_clss S, learned_clss S, conflicting S, ())›

interpretation cdclW_restart_mset: stateW_ops where
  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
  .

definition state_eq :: "'v cdclW_restart_mset ⇒ 'v cdclW_restart_mset ⇒ bool" (infix "∼m" 50) where
‹S ∼m T ⟷ state S = state T›

interpretation cdclW_restart_mset: stateW where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and
  state_eq = state_eq 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
  by unfold_locales (auto simp: cdclW_restart_mset_state state_eq_def state_def)


abbreviation backtrack_lvl :: "'v cdclW_restart_mset ⇒ nat" where
"backtrack_lvl ≡ cdclW_restart_mset.backtrack_lvl"

interpretation cdclW_restart_mset: conflict_driven_clause_learningW where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and

  state_eq = state_eq 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
  by unfold_locales

lemma cdclW_restart_mset_state_eq_eq: "state_eq = (=)"
   apply (intro ext)
   unfolding state_eq_def
   by (auto simp: cdclW_restart_mset_state state_def)


lemma clauses_def: ‹cdclW_restart_mset.clauses (M, N, U, C) = N + U›
  by (subst cdclW_restart_mset.clauses_def) (simp add: cdclW_restart_mset_state)

lemma cdclW_restart_mset_reduce_trail_to:
  "cdclW_restart_mset.reduce_trail_to F S =
    ((if length (trail S) ≥ length F
    then drop (length (trail S) - length F) (trail S)
    else []), init_clss S, learned_clss S, conflicting S)"
    (is "?S = _")
proof (induction F S rule: cdclW_restart_mset.reduce_trail_to.induct)
  case (1 F S) note IH = this
  show ?case
  proof (cases "trail S")
    case Nil
    then show ?thesis using IH by (cases S) (auto simp: cdclW_restart_mset_state)
  next
    case (Cons L M)
    then show ?thesis
      apply (cases "Suc (length M) > length F")
      subgoal
        apply (subgoal_tac "Suc (length M) - length F = Suc (length M - length F)")
        using cdclW_restart_mset.reduce_trail_to_length_ne[of S F] IH by auto
      subgoal
        using IH cdclW_restart_mset.reduce_trail_to_length_ne[of S F]
          apply (cases S)
        by (simp add: cdclW_restart_mset.trail_reduce_trail_to_drop cdclW_restart_mset_state)
      done
  qed
qed


interpretation cdclW_restart_mset: stateW_adding_init_clause where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and

  state_eq = state_eq 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 and
  add_init_cls = add_init_cls
  by unfold_locales (auto simp: state_def cdclW_restart_mset_state)


interpretation cdclW_restart_mset: conflict_driven_clause_learning_with_adding_init_clauseW where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and

  state_eq = state_eq 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 and
  add_init_cls = add_init_cls
  by unfold_locales (auto simp: state_def cdclW_restart_mset_state)

lemma full_cdclW_init_state:
  ‹full cdclW_restart_mset.cdclW_stgy (init_state {#}) S ⟷ S = init_state {#}›
  unfolding full_def rtranclp_unfold
  by (subst tranclp_unfold_begin)
     (auto simp:  cdclW_restart_mset.cdclW_stgy.simps
      cdclW_restart_mset.conflict.simps cdclW_restart_mset.cdclW_o.simps
       cdclW_restart_mset.propagate.simps cdclW_restart_mset.decide.simps
       cdclW_restart_mset.cdclW_bj.simps cdclW_restart_mset.backtrack.simps
      cdclW_restart_mset.skip.simps cdclW_restart_mset.resolve.simps
      cdclW_restart_mset_state clauses_def)

locale twl_restart_ops =
  fixes
    f :: ‹nat ⇒ nat›
begin

interpretation cdclW_restart_mset: cdclW_restart_restart_ops where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and

  state_eq = state_eq 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 and
  f = f
  by unfold_locales

end

locale twl_restart =
  twl_restart_ops f for f :: ‹nat ⇒ nat› +
  assumes
    f: ‹unbounded f›
begin

interpretation cdclW_restart_mset: cdclW_restart_restart where
  state = state and
  trail = trail and
  init_clss = init_clss and
  learned_clss = learned_clss and
  conflicting = conflicting and

  state_eq = state_eq 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 and
  f = f
  by unfold_locales (rule f)

end

context conflict_driven_clause_learningW
begin

lemma distinct_cdclW_state_alt_def:
  ‹distinct_cdclW_state S =
    ((∀T. conflicting S = Some T ⟶ distinct_mset T) ∧
     distinct_mset_mset (clauses S) ∧
     (∀L mark. Propagated L mark ∈ set (trail S) ⟶ distinct_mset mark))›
  unfolding distinct_cdclW_state_def clauses_def
  by auto
end


lemma cdclW_stgy_cdclW_init_state_empty_no_step:
  ‹cdclW_restart_mset.cdclW_stgy (init_state {#}) S ⟷ False›
  unfolding rtranclp_unfold
  by (auto simp:  cdclW_restart_mset.cdclW_stgy.simps
      cdclW_restart_mset.conflict.simps cdclW_restart_mset.cdclW_o.simps
       cdclW_restart_mset.propagate.simps cdclW_restart_mset.decide.simps
       cdclW_restart_mset.cdclW_bj.simps cdclW_restart_mset.backtrack.simps
      cdclW_restart_mset.skip.simps cdclW_restart_mset.resolve.simps
      cdclW_restart_mset_state clauses_def)

lemma cdclW_stgy_cdclW_init_state:
  ‹cdclW_restart_mset.cdclW_stgy** (init_state {#}) S ⟷ S = init_state {#}›
  unfolding rtranclp_unfold
  by (subst tranclp_unfold_begin)
    (auto simp: cdclW_stgy_cdclW_init_state_empty_no_step)


subsection ‹Restart with Replay›

text ‹
  In rather unfortunate move, we named restart with reuse of the trail ``fast restarts''
  due to the name the technique was presented first, before a reviewer pointed out that the ``fast''
  refers to the interval between two successive restarts and not to the idea that restarts are
  faster to do.
  This error is still present in various lemmas throughout the formalization.

  Anyway, the idea is that after a restart, parts of the trail are often reused (at least, for the
  VSIDS heuristic: VMTF moves too fast for that) and, therefore, it is better to not redo the
  propagations. A similar idea exists for backjump, chronological backtracking, but that technique
  is much more complicated to understand and implement properly.

TODO: fix
›
lemma after_fast_restart_replay:
  assumes
    inv: ‹cdclW_restart_mset.cdclW_all_struct_inv (M', N, U, None)› and
    stgy_invs: ‹cdclW_restart_mset.cdclW_stgy_invariant (M', N, U, None)› and
    smaller_propa: ‹cdclW_restart_mset.no_smaller_propa (M', N, U, None)› and
    kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N + U'› and
    U'_U: ‹U' ⊆# U›
  shows
    ‹cdclW_restart_mset.cdclW_stgy** ([], N, U', None) (drop (length M' - n) M', N, U', None)›
proof -
  let ?S = ‹λn. (drop (length M' - n) M', N, U', None)›
  note cdclW_restart_mset_state[simp]
  have
    M_lev: ‹cdclW_restart_mset.cdclW_M_level_inv (M', N, U, None)› and
    alien: ‹cdclW_restart_mset.no_strange_atm (M', N, U, None)› and
    confl: ‹cdclW_restart_mset.cdclW_conflicting (M', N, U, None)› and
    learned: ‹cdclW_restart_mset.cdclW_learned_clause (M', N, U, None)›
    using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+

  have smaller_confl: ‹cdclW_restart_mset.no_smaller_confl (M', N, U, None)›
    using stgy_invs unfolding cdclW_restart_mset.cdclW_stgy_invariant_def by blast
  have n_d: ‹no_dup M'›
    using M_lev unfolding cdclW_restart_mset.cdclW_M_level_inv_def by simp
  let ?L = ‹λm. M' ! (length M' - Suc m)›
  have undef_nth_Suc:
     ‹undefined_lit (drop (length M' - m) M') (lit_of (?L m))›
     if ‹m < length M'›
     for m
  proof -
    define k where
      ‹k = length M' - Suc m›
    then have Sk: ‹length M' - m = Suc k›
      using that by linarith
    have k_le_M': ‹k < length M'›
      using that unfolding k_def by linarith
    have n_d': ‹no_dup (take k M' @ ?L m # drop (Suc k) M')›
      using n_d
      apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc k›])
      apply (subst (asm) take_Suc_conv_app_nth)
       apply (rule k_le_M')
      apply (subst k_def[symmetric])
      by simp

    show ?thesis
      using n_d'
      apply (subst (asm) no_dup_append_cons)
      apply (subst (asm) k_def[symmetric])+
      apply (subst k_def[symmetric])+
      apply (subst Sk)+
      by blast
  qed

  have atm_in:
    ‹atm_of (lit_of (M' ! m)) ∈ atms_of_mm N›
    if ‹m < length M'›
    for m
    using alien that
    by (auto simp: cdclW_restart_mset.no_strange_atm_def lits_of_def)

  show ?thesis
    using kept
  proof (induction n)
    case 0
    then show ?case by simp
  next
    case (Suc m) note IH = this(1) and kept = this(2)
    consider
      (le) ‹m < length M'› |
      (ge) ‹m ≥ length M'›
      by linarith
    then show ?case
    proof (cases)
      case ge
      then show ?thesis
        using Suc by auto
    next
      case le
      define k where
        ‹k = length M' - Suc m›
      then have Sk: ‹length M' - m = Suc k›
        using le by linarith
      have k_le_M': ‹k < length M'›
        using le unfolding k_def by linarith
      have kept': ‹∀L E. Propagated L E ∈ set (drop (length M' - m) M') ⟶ E ∈# N + U'›
        using kept k_le_M' unfolding k_def[symmetric] Sk
        by (subst (asm) Cons_nth_drop_Suc[symmetric]) auto
      have M': ‹M' = take (length M' - Suc m) M' @ ?L m # trail (?S m)›
        apply (subst append_take_drop_id[symmetric, of _ ‹Suc k›])
        apply (subst take_Suc_conv_app_nth)
         apply (rule k_le_M')
        apply (subst k_def[symmetric])
        unfolding k_def[symmetric] Sk
        by auto

      have ‹cdclW_restart_mset.cdclW_stgy (?S m) (?S (Suc m))›
      proof (cases ‹?L (m)›)
        case (Decided K) note K = this
        have dec: ‹cdclW_restart_mset.decide (?S m) (?S (Suc m))›
          apply (rule cdclW_restart_mset.decide_rule[of _ ‹lit_of (?L m)›])
          subgoal by simp
          subgoal using undef_nth_Suc[of m] le by simp
          subgoal using le by (auto simp: atm_in)
          subgoal using le k_le_M' K unfolding k_def[symmetric] Sk
            by (auto simp: state_eq_def state_def Cons_nth_drop_Suc[symmetric])
          done
        have Dec: ‹M' ! k = Decided K›
          using K unfolding k_def[symmetric] Sk .

        have H: ‹D + {#L#} ∈# N + U ⟶ undefined_lit (trail (?S m)) L ⟶
            ¬ (trail (?S m)) ⊨as CNot D› for D L
          using smaller_propa unfolding cdclW_restart_mset.no_smaller_propa_def
            trail.simps clauses_def
            cdclW_restart_mset_state
          apply (subst (asm) M')
          unfolding Dec Sk k_def[symmetric]
          by (auto simp: clauses_def state_eq_def)
        have ‹D ∈# N ⟶ undefined_lit (trail (?S m)) L ⟶ L ∈# D ⟶
            ¬ (trail (?S m)) ⊨as CNot (remove1_mset L D)› and
          ‹D ∈# U' ⟶ undefined_lit (trail (?S m)) L ⟶ L ∈# D ⟶
            ¬ (trail (?S m)) ⊨as CNot (remove1_mset L D)›for D L
          using H[of ‹remove1_mset L D› L] U'_U by auto
        then have nss: ‹no_step cdclW_restart_mset.propagate (?S m)›
          by (auto simp: cdclW_restart_mset.propagate.simps clauses_def
              state_eq_def k_def[symmetric] Sk)

        have H: ‹D ∈# N + U' ⟶ ¬ (trail (?S m)) ⊨as CNot D› for D
          using smaller_confl U'_U unfolding cdclW_restart_mset.no_smaller_confl_def
            trail.simps clauses_def cdclW_restart_mset_state
          apply (subst (asm) M')
          unfolding Dec Sk k_def[symmetric]
          by (auto simp: clauses_def state_eq_def)
        then have nsc: ‹no_step cdclW_restart_mset.conflict (?S m)›
          by (auto simp: cdclW_restart_mset.conflict.simps clauses_def state_eq_def
              k_def[symmetric] Sk)
        show ?thesis
          apply (rule cdclW_restart_mset.cdclW_stgy.other')
            apply (rule nsc)
           apply (rule nss)
          apply (rule cdclW_restart_mset.cdclW_o.decide)
          apply (rule dec)
          done
      next
        case K: (Propagated K C)
        have Propa: ‹M' ! k = Propagated K C›
          using K unfolding k_def[symmetric] Sk .
        have
          M_C: ‹trail (?S m) ⊨as CNot (remove1_mset K C)› and
          K_C: ‹K ∈# C›
          using confl unfolding cdclW_restart_mset.cdclW_conflicting_def trail.simps
          by (subst (asm)(3) M'; auto simp: k_def[symmetric] Sk Propa)+
        have [simp]: ‹k - min (length M') k = 0›
          unfolding k_def by auto
        have C_N_U: ‹C ∈# N + U'›
          using learned kept unfolding cdclW_restart_mset.cdclW_learned_clause_alt_def Sk
            k_def[symmetric] cdclW_restart_mset.reasons_in_clauses_def
          apply (subst (asm)(4)M')
          apply (subst (asm)(10)M')
          unfolding K
          by (auto simp: K k_def[symmetric] Sk Propa clauses_def)
        have ‹cdclW_restart_mset.propagate (?S m) (?S (Suc m))›
          apply (rule cdclW_restart_mset.propagate_rule[of _ C K])
          subgoal by simp
          subgoal using C_N_U by (simp add: clauses_def)
          subgoal using K_C .
          subgoal using M_C .
          subgoal using undef_nth_Suc[of m] le K by (simp add: k_def[symmetric] Sk)
          subgoal
            using le k_le_M' K unfolding k_def[symmetric] Sk
            by (auto simp: state_eq_def
                state_def Cons_nth_drop_Suc[symmetric])
          done
        then show ?thesis
          by (rule cdclW_restart_mset.cdclW_stgy.propagate')
      qed
      then show ?thesis
        using IH[OF kept'] by simp
    qed
  qed
qed

lemma after_fast_restart_replay_no_stgy:
  assumes
    inv: ‹cdclW_restart_mset.cdclW_all_struct_inv (M', N, U, None)› and
    kept: ‹∀L E. Propagated L E ∈ set (drop (length M' - n) M') ⟶ E ∈# N + U'› and
    U'_U: ‹U' ⊆# U›
  shows
    ‹cdclW_restart_mset.cdclW** ([], N, U', None) (drop (length M' - n) M', N, U', None)›
proof -
  let ?S = ‹λn. (drop (length M' - n) M', N, U', None)›
  note cdclW_restart_mset_state[simp]
  have
    M_lev: ‹cdclW_restart_mset.cdclW_M_level_inv (M', N, U, None)› and
    alien: ‹cdclW_restart_mset.no_strange_atm (M', N, U, None)› and
    confl: ‹cdclW_restart_mset.cdclW_conflicting (M', N, U, None)› and
    learned: ‹cdclW_restart_mset.cdclW_learned_clause (M', N, U, None)›
    using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+

  have n_d: ‹no_dup M'›
    using M_lev unfolding cdclW_restart_mset.cdclW_M_level_inv_def by simp
  let ?L = ‹λm. M' ! (length M' - Suc m)›
  have undef_nth_Suc:
     ‹undefined_lit (drop (length M' - m) M') (lit_of (?L m))›
     if ‹m < length M'›
     for m
  proof -
    define k where
      ‹k = length M' - Suc m›
    then have Sk: ‹length M' - m = Suc k›
      using that by linarith
    have k_le_M': ‹k < length M'›
      using that unfolding k_def by linarith
    have n_d': ‹no_dup (take k M' @ ?L m # drop (Suc k) M')›
      using n_d
      apply (subst (asm) append_take_drop_id[symmetric, of _ ‹Suc k›])
      apply (subst (asm) take_Suc_conv_app_nth)
       apply (rule k_le_M')
      apply (subst k_def[symmetric])
      by simp

    show ?thesis
      using n_d'
      apply (subst (asm) no_dup_append_cons)
      apply (subst (asm) k_def[symmetric])+
      apply (subst k_def[symmetric])+
      apply (subst Sk)+
      by blast
  qed

  have atm_in:
    ‹atm_of (lit_of (M' ! m)) ∈ atms_of_mm N›
    if ‹m < length M'›
    for m
    using alien that
    by (auto simp: cdclW_restart_mset.no_strange_atm_def lits_of_def)

  show ?thesis
    using kept
  proof (induction n)
    case 0
    then show ?case by simp
  next
    case (Suc m) note IH = this(1) and kept = this(2)
    consider
      (le) ‹m < length M'› |
      (ge) ‹m ≥ length M'›
      by linarith
    then show ?case
    proof cases
      case ge
      then show ?thesis
        using Suc by auto
    next
      case le
      define k where
        ‹k = length M' - Suc m›
      then have Sk: ‹length M' - m = Suc k›
        using le by linarith
      have k_le_M': ‹k < length M'›
        using le unfolding k_def by linarith
      have kept': ‹∀L E. Propagated L E ∈ set (drop (length M' - m) M') ⟶ E ∈# N + U'›
        using kept k_le_M' unfolding k_def[symmetric] Sk
        by (subst (asm) Cons_nth_drop_Suc[symmetric]) auto
      have M': ‹M' = take (length M' - Suc m) M' @ ?L m # trail (?S m)›
        apply (subst append_take_drop_id[symmetric, of _ ‹Suc k›])
        apply (subst take_Suc_conv_app_nth)
         apply (rule k_le_M')
        apply (subst k_def[symmetric])
        unfolding k_def[symmetric] Sk
        by auto

      have ‹cdclW_restart_mset.cdclW (?S m) (?S (Suc m))›
      proof (cases ‹?L (m)›)
        case (Decided K) note K = this
        have dec: ‹cdclW_restart_mset.decide (?S m) (?S (Suc m))›
          apply (rule cdclW_restart_mset.decide_rule[of _ ‹lit_of (?L m)›])
          subgoal by simp
          subgoal using undef_nth_Suc[of m] le by simp
          subgoal using le by (auto simp: atm_in)
          subgoal using le k_le_M' K unfolding k_def[symmetric] Sk
            by (auto simp: state_eq_def state_def Cons_nth_drop_Suc[symmetric])
          done
        have Dec: ‹M' ! k = Decided K›
          using K unfolding k_def[symmetric] Sk .

        show ?thesis
          apply (rule cdclW_restart_mset.cdclW.intros(3))
          apply (rule cdclW_restart_mset.cdclW_o.decide)
          apply (rule dec)
          done
      next
        case K: (Propagated K C)
        have Propa: ‹M' ! k = Propagated K C›
          using K unfolding k_def[symmetric] Sk .
        have
          M_C: ‹trail (?S m) ⊨as CNot (remove1_mset K C)› and
          K_C: ‹K ∈# C›
          using confl unfolding cdclW_restart_mset.cdclW_conflicting_def trail.simps
          by (subst (asm)(3) M'; auto simp: k_def[symmetric] Sk Propa)+
        have [simp]: ‹k - min (length M') k = 0›
          unfolding k_def by auto
        have C_N_U: ‹C ∈# N + U'›
          using learned kept unfolding cdclW_restart_mset.cdclW_learned_clause_alt_def Sk
            k_def[symmetric] cdclW_restart_mset.reasons_in_clauses_def
          apply (subst (asm)(4)M')
          apply (subst (asm)(10)M')
          unfolding K
          by (auto simp: K k_def[symmetric] Sk Propa clauses_def)
        have ‹cdclW_restart_mset.propagate (?S m) (?S (Suc m))›
          apply (rule cdclW_restart_mset.propagate_rule[of _ C K])
          subgoal by simp
          subgoal using C_N_U by (simp add: clauses_def)
          subgoal using K_C .
          subgoal using M_C .
          subgoal using undef_nth_Suc[of m] le K by (simp add: k_def[symmetric] Sk)
          subgoal
            using le k_le_M' K unfolding k_def[symmetric] Sk
            by (auto simp: state_eq_def
                state_def Cons_nth_drop_Suc[symmetric])
          done
        then show ?thesis
          by (rule cdclW_restart_mset.cdclW.intros)
      qed
      then show ?thesis
        using IH[OF kept'] by simp
    qed
  qed
qed

lemma (in conflict_driven_clause_learningW) cdclW_stgy_new_learned_in_all_simple_clss:
  assumes
    st: ‹cdclW_stgy** R S› and
    invR: ‹cdclW_all_struct_inv R›
  shows ‹set_mset (learned_clss S) ⊆ simple_clss (atms_of_mm (init_clss S))›
proof
  fix C
  assume C: ‹C ∈# learned_clss S›
  have invS: ‹cdclW_all_struct_inv S›
    using rtranclp_cdclW_stgy_cdclW_all_struct_inv[OF st invR] .
  then have dist: ‹distinct_cdclW_state S› and alien: ‹no_strange_atm S›
    unfolding cdclW_all_struct_inv_def by fast+
  have ‹atms_of C ⊆ atms_of_mm (init_clss S)›
    using alien C unfolding no_strange_atm_def
    by (auto dest!: multi_member_split)
  moreover have ‹distinct_mset C›
    using dist C unfolding distinct_cdclW_state_def distinct_mset_set_def
    by (auto dest: in_diffD)
  moreover have ‹¬ tautology C›
    using invS C unfolding cdclW_all_struct_inv_def
    by (auto dest: in_diffD)
  ultimately show ‹C ∈ simple_clss (atms_of_mm (init_clss S))›
    unfolding simple_clss_def
    by clarify
qed

end