Theory Watched_Literals_Transition_System_Restart

theory Watched_Literals_Transition_System_Restart
imports Watched_Literals_Transition_System
theory Watched_Literals_Transition_System_Restart
  imports Watched_Literals_Transition_System
begin


text ‹
  Unlike the basic CDCL, it does not make any sense to fully restart the trail:
  the part propagated at level 0 (only the part due to unit clauses) has to be kept.
  Therefore, we allow fast restarts (i.e. a restart where part of the trail is reused).

  There are two cases:
    ▪ either the trail is strictly decreasing;
    ▪ or it is kept and the number of clauses is strictly decreasing.

  This ensures that ∗‹something› changes to prove termination.

  In practice, there are two types of restarts that are done:
    ▪ First, a restart can be done to enforce that the SAT solver goes more into the direction
      expected by the decision heuristics.
    ▪ Second, a full restart can be done to simplify inprocessing and garbage collection of the memory:
      instead of properly updating the trail, we restart the search. This is not necessary (i.e.,
      glucose and minisat do not do it), but it simplifies the proofs by allowing to move clauses
      without taking care of updating references in the trail. Moreover, as this happens ``rarely''
      (around once every few thousand conflicts), it should not matter too much.

  Restarts are the ``local search'' part of all modern SAT solvers.
›

inductive cdcl_twl_restart :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
restart_trail:
   ‹cdcl_twl_restart (M, N, U, None, NE, UE, {#}, Q)
        (M', N', U', None, NE + clauses NE', UE + clauses UE', {#}, {#})›
  if
    ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#clause E. L ∈ lits_of_l M' ∧ get_level M' L = 0›
    ‹∀L E. Propagated L E ∈ set M' ⟶ E ∈# clause `# (N + U') + NE + UE + clauses UE'› |
restart_clauses:
   ‹cdcl_twl_restart (M, N, U, None, NE, UE, {#}, Q)
      (M, N', U', None, NE + clauses NE', UE + clauses UE', {#}, Q)›
  if
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#clause E. L ∈ lits_of_l M ∧ get_level M L = 0›
    ‹∀L E. Propagated L E ∈ set M ⟶ E ∈# clause `# (N + U') + NE + UE + clauses UE'›

inductive_cases cdcl_twl_restartE: ‹cdcl_twl_restart S T›


lemma cdcl_twl_restart_cdclW_stgy:
  assumes
    ‹cdcl_twl_restart S V› and
    ‹twl_struct_invs S› and
    ‹twl_stgy_invs S›
  shows
    ‹∃T. cdclW_restart_mset.restart (stateW_of S) T ∧ cdclW_restart_mset.cdclW_stgy** T (stateW_of V) ∧
      cdclW_restart_mset.cdclW_restart** (stateW_of S) (stateW_of V)›
  using assms
proof (induction rule: cdcl_twl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE Q)
  note decomp = this(1) and learned = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and inv = this(6) and stgy_invs = this(7)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?T = ‹([], clause `# N + NE, clause `# U' + UE + clauses UE', None)›
  let ?V = ‹(M', N, U', None, NE, UE + clauses UE', {#}, {#})›
  have restart: ‹cdclW_restart_mset.restart (stateW_of ?S) ?T›
    using learned
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of ?S)›  and
    smaller_propa:
      ‹cdclW_restart_mset.no_smaller_propa (stateW_of ?S)›
    using inv unfolding twl_struct_invs_def by fast+
  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW_stgy** ?T
      (drop (length M - length M') M, clause `# N + NE, clause `# U' + UE + clauses UE', None)› for n
    apply (rule after_fast_restart_replay[of M ‹clause `# N + NE› ‹clause `# U+UE› _
          ‹clause `# U' + UE +clauses UE'›])
    subgoal using struct_invs by simp
    subgoal using stgy_invs unfolding twl_stgy_invs_def by simp
    subgoal using smaller_propa by simp
    subgoal using kept unfolding drop_M_M' by (auto simp add: ac_simps)
    subgoal using learned
     by (auto simp: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
    done
  then have st: ‹cdclW_restart_mset.cdclW_stgy** ?T (stateW_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  moreover have ‹cdclW_restart_mset.cdclW_restart** (stateW_of ?S) (stateW_of ?V)›
    using restart st
    by (auto dest!: cdclW_restart_mset.cdclW_rf.intros cdclW_restart_mset.cdclW_restart.intros
          cdclW_restart_mset.rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  ultimately show ?case
    using restart unfolding N stateW_of.simps image_mset_union add.assoc
      add.commute[of ‹clauses NE'›]
    by fast
next
  case (restart_clauses U' UE' U N N' NE' M NE UE Q)
  note learned = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    inv = this(5) and stgy_invs = this(6)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?T = ‹([], clause `# N + NE, clause `# U' + UE + clauses UE', None)›
  let ?V = ‹(M, N, U', None, NE, UE + clauses UE', {#}, {#})›
  have restart: ‹cdclW_restart_mset.restart (stateW_of ?S) ?T›
    using learned
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro!: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of (M, N, U, None, NE, UE, {#}, Q))›  and
    smaller_propa:
      ‹cdclW_restart_mset.no_smaller_propa (stateW_of (M, N, U, None, NE, UE, {#}, Q))›
    using inv unfolding twl_struct_invs_def by fast+

  have ‹cdclW_restart_mset.cdclW_stgy** ?T
      (drop (length M - length M) M, clause `# N + NE, clause `# U' + UE+ clauses UE', None)› for n
    apply (rule after_fast_restart_replay[of M ‹clause `# N + NE› ‹clause `# U+UE› _
          ‹clause `# U' + UE + clauses UE'›])
    subgoal using struct_invs by simp
    subgoal using stgy_invs unfolding twl_stgy_invs_def by simp
    subgoal using smaller_propa by simp
    subgoal using kept by (auto simp add: ac_simps)
    subgoal using learned
     by (auto simp: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
    done
  then have st: ‹cdclW_restart_mset.cdclW_stgy** ?T (stateW_of ?V)›
    by (simp add: ac_simps)
  moreover have ‹cdclW_restart_mset.cdclW_restart** (stateW_of ?S) (stateW_of ?V)›
    using restart st
    by (auto dest!: cdclW_restart_mset.cdclW_rf.intros cdclW_restart_mset.cdclW_restart.intros
          cdclW_restart_mset.rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  ultimately show ?case
    using restart unfolding N stateW_of.simps image_mset_union add.assoc
      add.commute[of ‹clauses NE'›]
    by fast
qed

lemma cdcl_twl_restart_cdclW:
  assumes
    ‹cdcl_twl_restart S V› and
    ‹twl_struct_invs S›
  shows
    ‹∃T. cdclW_restart_mset.restart (stateW_of S) T ∧ cdclW_restart_mset.cdclW** T (stateW_of V)›
  using assms
proof (induction rule: cdcl_twl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE Q)
  note decomp = this(1) and learned = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and inv = this(6)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?T = ‹([], clause `# N + NE, clause `# U' + UE + clauses UE', None)›
  let ?V = ‹(M', N, U', None, NE, UE + clauses UE', {#}, {#})›
  have restart: ‹cdclW_restart_mset.restart (stateW_of ?S) ?T›
    using learned
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of (M, N, U, None, NE, UE, {#}, Q))›  and
    smaller_propa:
      ‹cdclW_restart_mset.no_smaller_propa (stateW_of (M, N, U, None, NE, UE, {#}, Q))›
    using inv unfolding twl_struct_invs_def by fast+
  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW** ?T
      (drop (length M - length M') M, clause `# N + NE, clause `# U' + UE+ clauses UE', None)› for n
    apply (rule after_fast_restart_replay_no_stgy[of M ‹clause `# N + NE› ‹clause `# U+UE› _
          ‹clause `# U' + UE + clauses UE'›])
    subgoal using struct_invs by simp
    subgoal using kept unfolding drop_M_M' by (auto simp add: ac_simps)
    subgoal using learned
     by (auto simp: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
    done
  then have st: ‹cdclW_restart_mset.cdclW** ?T (stateW_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  then show ?case
    using restart by (auto simp: ac_simps N)
next
  case (restart_clauses U' UE' U N N' NE' M NE UE Q)
  note learned = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    inv = this(5)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?T = ‹([], clause `# N + NE, clause `# U' + UE + clauses UE', None)›
  let ?V = ‹(M, N, U', None, NE, UE + clauses UE', {#}, {#})›
  have restart: ‹cdclW_restart_mset.restart (stateW_of ?S) ?T›
    using learned
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of ?S)›  and
    smaller_propa:
      ‹cdclW_restart_mset.no_smaller_propa (stateW_of ?S)›
    using inv unfolding twl_struct_invs_def by fast+
  have ‹cdclW_restart_mset.cdclW** ?T
      (drop (length M - length M) M, clause `# N + NE, clause `# U' + UE+ clauses UE', None)› for n
    apply (rule after_fast_restart_replay_no_stgy[of M ‹clause `# N + NE› ‹clause `# U+UE› _
          ‹clause `# U' + UE+ clauses UE'›])
    subgoal using struct_invs by simp
    subgoal using kept by (auto simp add: ac_simps)
    subgoal
     using learned by (auto simp: image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
    done
  then have st: ‹cdclW_restart_mset.cdclW** ?T (stateW_of ?V)›
    by (simp add: ac_simps)
  then show ?case
    using restart by (auto simp: ac_simps N)
qed

lemma cdcl_twl_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_restart S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  using assms
proof (induction rule: cdcl_twl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE Q)
  note decomp = this(1) and learned' = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and inv = this(6)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?S' = ‹(M', N', U', None, NE+ clauses NE', UE + clauses UE', {#}, {#})›
  have learned: ‹U' ⊆# U›
    using learned' by (rule mset_le_decr_left1)
  have
    twl_st_inv: ‹twl_st_inv ?S› and
    ‹valid_enqueued ?S› and
    struct_inv: ‹cdclW_restart_mset.cdclW_all_struct_inv
      (stateW_of ?S)› and
    smaller: ‹cdclW_restart_mset.no_smaller_propa
      (stateW_of ?S)› and
    ‹twl_st_exception_inv ?S› and
    no_dup_q: ‹no_duplicate_queued ?S› and
    dist: ‹distinct_queued ?S› and
    ‹confl_cands_enqueued ?S› and
    ‹propa_cands_enqueued ?S› and
    ‹get_conflict ?S ≠ None ⟶
     clauses_to_update ?S = {#} ∧
     literals_to_update ?S = {#}› and
    unit: ‹entailed_clss_inv ?S› and
    to_upd: ‹clauses_to_update_inv ?S› and
    past: ‹past_invs ?S›
    using inv unfolding twl_struct_invs_def by clarify+
  have
    ex: ‹(∀C∈#N + U. twl_lazy_update M' C ∧
           watched_literals_false_of_max_level M' C ∧
           twl_exception_inv (M', N, U, None, NE, UE, {#}, {#}) C)› and
     conf_cands: ‹confl_cands_enqueued (M', N, U, None, NE, UE, {#}, {#})› and
     propa_cands: ‹propa_cands_enqueued (M', N, U, None, NE, UE, {#}, {#})› and
     clss_to_upd: ‹clauses_to_update_inv (M', N, U, None, NE, UE, {#}, {#})›
     using past get_all_ann_decomposition_exists_prepend[OF decomp] unfolding past_invs.simps
     by force+

   have excp_inv: ‹twl_st_exception_inv (M', N, U, None, NE, UE, {#}, {#})›
     using ex unfolding twl_st_exception_inv.simps by blast+
   have twl_st_inv': ‹twl_st_inv (M', N, U, None, NE, UE, {#}, {#})›
     using ex learned twl_st_inv
     unfolding twl_st_exception_inv.simps twl_st_inv.simps
     by auto
   have n_d: ‹no_dup M›
     using struct_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
       cdclW_restart_mset.cdclW_M_level_inv_def by (auto simp: trail.simps)
   obtain M3 where
     M: ‹M = M3 @ M2 @ Decided K # M'›
     using decomp by blast
   define M3' where ‹M3' = M3 @ M2›
   then have M3': ‹M = M3' @ Decided K # M'›
     unfolding M by auto
   have entailed_clss_inv: ‹entailed_clss_inv ?S'›
     unfolding entailed_clss_inv.simps
   proof
     fix C
     assume ‹C ∈# NE + clauses NE' + (UE + clauses UE')›
     moreover have ‹L ∈ lits_of_l M ∧ get_level M L = 0 ⟹L ∈ lits_of_l M' ∧ get_level M' L = 0›
       for L
       using n_d
       by (cases ‹undefined_lit M3' L›)
         (auto simp: M3' atm_of_eq_atm_of get_level_cons_if
           dest: in_lits_of_l_defined_litD split: if_splits)
     ultimately obtain L where
       lev_L: ‹get_level M' L = 0›
       ‹L ∈ lits_of_l M'› and
       C: ‹L ∈# C›
       using unit has_true by auto blast+
     then have ‹L ∈ lits_of_l M'›
       apply (cases ‹defined_lit M3' L›)
       using n_d unfolding M3' by (auto simp: get_level_cons_if split: if_splits
           dest: in_lits_of_l_defined_litD)
     moreover have ‹get_level M' L = 0›
       apply (cases ‹defined_lit M3' L›)
       using n_d lev_L unfolding M3' by (auto simp: get_level_cons_if split: if_splits
           dest: in_lits_of_l_defined_litD)
     ultimately show ‹∃L. L ∈# C ∧
             (None = None ∨ 0 < count_decided M' ⟶
              get_level M' L = 0 ∧ L ∈ lits_of_l M')›
       using C by blast
   qed
   have a: ‹N ⊆# N› and NN': ‹N' ⊆# N› using N by auto
   have past_invs: ‹past_invs ?S'›
     unfolding past_invs.simps
   proof (intro conjI impI allI)
     fix M1 M2 K'
     assume H:‹M' = M2 @ Decided K' # M1›
     let ?U = ‹(M1, N, U, None, NE, UE, {#}, {#})›
     let ?U' = ‹(M1, N', U', None, NE+clauses NE', UE+clauses UE', {#}, {#})›
     have ‹M = (M3' @ Decided K # M2) @ Decided K' # M1›
       using H M3' by simp
     then have
       1: ‹∀C∈#N + U.
           twl_lazy_update M1 C ∧
           watched_literals_false_of_max_level M1 C ∧
           twl_exception_inv ?U C› and
       2: ‹confl_cands_enqueued ?U› and
       3: ‹propa_cands_enqueued ?U› and
       4: ‹clauses_to_update_inv ?U›
       using past unfolding past_invs.simps by blast+
     show ‹∀C∈#N' + U'.
          twl_lazy_update M1 C ∧
          watched_literals_false_of_max_level M1 C ∧
          twl_exception_inv ?U' C›
       using 1 learned twl_st_exception_inv_mono[OF learned NN', of M1 None NE ‹UE›
          ‹{#}› ‹{#}› ‹NE+clauses NE'› ‹UE+clauses UE'›] N by auto
     show ‹confl_cands_enqueued ?U'›
       using confl_cands_enqueued_mono[OF learned NN' 2] .
     show ‹propa_cands_enqueued ?U'›
       using propa_cands_enqueued_mono[OF learned NN' 3] .
     show ‹clauses_to_update_inv ?U'›
       using 4 learned by (auto simp add: filter_mset_empty_conv N)
   qed
   have clss_to_upd: ‹clauses_to_update_inv ?S'›
     using clss_to_upd learned by (auto simp add: filter_mset_empty_conv N)

   have [simp]: ‹cdclW_restart_mset.cdclW ≤ cdclW_restart_mset.cdclW_restart›
     using cdclW_restart_mset.cdclW_cdclW_restart by blast

   obtain T' where
     res: ‹cdclW_restart_mset.restart (stateW_of ?S) T'› and
     res': ‹cdclW_restart_mset.cdclW** T' (stateW_of ?S')›
     using cdcl_twl_restart_cdclW[OF cdcl_twl_restart.restart_trail[OF restart_trail(1-5)] inv]
     by (auto simp: ac_simps N)
   then have ‹cdclW_restart_mset.cdclW_restart** (stateW_of ?S)
       (stateW_of ?S')›
     using rtranclp_mono[of cdclW_restart_mset.cdclW cdclW_restart_mset.cdclW_restart]
       cdclW_restart_mset.cdclW_cdclW_restart
     by (auto dest!: cdclW_restart_mset.cdclW_restart.intros
         cdclW_restart_mset.cdclW_rf.intros)
   from cdclW_restart_mset.rtranclp_cdclW_all_struct_inv_inv[OF this struct_inv]
   have struct_inv':
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of (M', N', U', None, NE+ clauses NE', UE+ clauses UE', {#}, {#}))›
     by (auto simp: ac_simps N)
   have smaller':
     ‹cdclW_restart_mset.no_smaller_propa (stateW_of (M', N', U', None, NE+ clauses NE', UE+ clauses UE', {#}, {#}))›
     using smaller mset_subset_eqD[OF learned']
     apply (auto simp: cdclW_restart_mset.no_smaller_propa_def M3' cdclW_restart_mset_state
         clauses_def ac_simps N) (* TODO Proof *)
     apply (metis Cons_eq_appendI append_assoc image_eqI)
     apply (metis Cons_eq_appendI append_assoc image_eqI)
     done

   show ?case
    unfolding twl_struct_invs_def
    apply (intro conjI)
    subgoal using twl_st_inv_mono[OF learned NN' twl_st_inv'] by (auto simp: ac_simps N)
    subgoal by simp
    subgoal by (rule struct_inv')
    subgoal by (rule smaller')
    subgoal using twl_st_exception_inv_mono[OF learned NN' excp_inv] .
    subgoal using no_dup_q by auto
    subgoal using dist by auto
    subgoal using confl_cands_enqueued_mono[OF learned NN' conf_cands] .
    subgoal using propa_cands_enqueued_mono[OF learned NN' propa_cands] .
    subgoal by simp
    subgoal by (rule entailed_clss_inv)
    subgoal by (rule clss_to_upd)
    subgoal by (rule past_invs)
    done
next
  case (restart_clauses U' UE' U N N' NE' M NE UE Q)
  note learned' = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    invs = this(5)
  let ?S = ‹(M, N, U, None, NE, UE, {#}, Q)›
  let ?T = ‹(M, N', U', None, NE+clauses NE', UE + clauses UE', {#}, Q)›
  have learned: ‹U' ⊆# U›
    using learned' by (rule mset_le_decr_left1)
  have
    twl_st_inv: ‹twl_st_inv ?S› and
    valid: ‹valid_enqueued ?S› and
    struct_inv: ‹cdclW_restart_mset.cdclW_all_struct_inv
      (stateW_of ?S)› and
    smaller: ‹cdclW_restart_mset.no_smaller_propa
      (stateW_of ?S)› and
    excp_inv: ‹twl_st_exception_inv ?S› and
    no_dup_q: ‹no_duplicate_queued ?S› and
    dist: ‹distinct_queued ?S› and
    confl_cands: ‹confl_cands_enqueued ?S› and
    propa_cands: ‹propa_cands_enqueued ?S› and
    ‹get_conflict ?S ≠ None ⟶
     clauses_to_update ?S = {#} ∧
     literals_to_update ?S = {#}› and
    unit: ‹entailed_clss_inv ?S› and
    to_upd: ‹clauses_to_update_inv ?S› and
    past: ‹past_invs ?S›
    using invs unfolding twl_struct_invs_def by clarify+
   have learned: ‹U' ⊆# U›
    using learned by auto
   have n_d: ‹no_dup M›
     using struct_inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
       cdclW_restart_mset.cdclW_M_level_inv_def by (auto simp: trail.simps)
   have valid': ‹valid_enqueued ?T›
     using valid by auto
   have entailed_clss_inv: ‹entailed_clss_inv ?T›
     unfolding entailed_clss_inv.simps
   proof
     fix C
     assume ‹C ∈# NE + clauses NE' + (UE + clauses UE')›
     then obtain L where
       lev_L: ‹get_level M L = 0›
       ‹L ∈ lits_of_l M› and
       C: ‹L ∈# C›
       using unit has_true by auto
     then show ‹∃L. L ∈# C ∧
             (None = None ∨ 0 < count_decided M ⟶
              get_level M L = 0 ∧ L ∈ lits_of_l M)›
       using C by blast
   qed
   have NN': ‹N' ⊆# N› unfolding N by auto
   have past_invs: ‹past_invs (M, N', U', None, NE+clauses NE', UE + clauses UE', {#}, Q)›
     using past unfolding past_invs.simps
   proof (intro conjI impI allI)
     fix M1 M2 K'
     assume H:‹M = M2 @ Decided K' # M1›
     let ?U = ‹(M1, N, U, None, NE, UE, {#}, {#})›
     let ?U' = ‹(M1, N', U', None, NE+clauses NE', UE + clauses UE', {#}, {#})›
     have
       1: ‹∀C∈#N + U.
           twl_lazy_update M1 C ∧
           watched_literals_false_of_max_level M1 C ∧
           twl_exception_inv ?U C› and
       2: ‹confl_cands_enqueued ?U› and
       3: ‹propa_cands_enqueued ?U› and
       4: ‹clauses_to_update_inv ?U›
       using H past unfolding past_invs.simps by blast+
     show ‹∀C∈#N' + U'.
          twl_lazy_update M1 C ∧
          watched_literals_false_of_max_level M1 C ∧
          twl_exception_inv ?U' C›
       using 1 learned twl_st_exception_inv_mono[OF learned NN', of M1 None NE UE ‹{#}› ‹{#}›] N
       by auto
     show ‹confl_cands_enqueued ?U'›
       using confl_cands_enqueued_mono[OF learned NN' 2] .
     show ‹propa_cands_enqueued ?U'›
       using propa_cands_enqueued_mono[OF learned NN' 3] .
     show ‹clauses_to_update_inv ?U'›
       using 4 learned by (auto simp add: filter_mset_empty_conv N)
   qed

   have [simp]: ‹cdclW_restart_mset.cdclW ≤ cdclW_restart_mset.cdclW_restart›
     using cdclW_restart_mset.cdclW_cdclW_restart by blast

   have clss_to_upd: ‹clauses_to_update_inv ?T›
     using to_upd learned by (auto simp add: filter_mset_empty_conv N ac_simps)
      obtain T' where
     res: ‹cdclW_restart_mset.restart (stateW_of ?S) T'› and
     res': ‹cdclW_restart_mset.cdclW** T' (stateW_of ?T)›
     using cdcl_twl_restart_cdclW[OF cdcl_twl_restart.restart_clauses[OF restart_clauses(1-4)] invs]
     by (auto simp: ac_simps N)
   then have ‹cdclW_restart_mset.cdclW_restart** (stateW_of ?S)
       (stateW_of ?T)›
     using rtranclp_mono[of cdclW_restart_mset.cdclW cdclW_restart_mset.cdclW_restart]
       cdclW_restart_mset.cdclW_cdclW_restart
     by (auto dest!: cdclW_restart_mset.cdclW_restart.intros
         cdclW_restart_mset.cdclW_rf.intros)
   from cdclW_restart_mset.rtranclp_cdclW_all_struct_inv_inv[OF this struct_inv]
   have struct_inv':
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of ?T)›
     .

    have smaller':
     ‹cdclW_restart_mset.no_smaller_propa (stateW_of ?T)›
     using smaller mset_subset_eqD[OF learned']
     by (auto 5 5 simp: cdclW_restart_mset.no_smaller_propa_def cdclW_restart_mset_state
         clauses_def N ac_simps)

   show ?case
    unfolding twl_struct_invs_def
    apply (intro conjI)
    subgoal using twl_st_inv_mono[OF learned NN' twl_st_inv] .
    subgoal by (rule valid')
    subgoal by (rule struct_inv')
    subgoal by (rule smaller')
    subgoal using twl_st_exception_inv_mono[OF learned NN' excp_inv] .
    subgoal using no_dup_q by auto
    subgoal using dist by auto
    subgoal using confl_cands_enqueued_mono[OF learned NN' confl_cands] .
    subgoal using propa_cands_enqueued_mono[OF learned NN' propa_cands] .
    subgoal by simp
    subgoal by (rule entailed_clss_inv)
    subgoal by (rule clss_to_upd)
    subgoal by (rule past_invs)
    done
qed

lemma rtranclp_cdcl_twl_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_restart** S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  using assms by (induction rule: rtranclp_induct) (auto simp: cdcl_twl_restart_twl_struct_invs)

lemma cdcl_twl_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_restart S T› and ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_restart.induct)
   (auto simp: twl_stgy_invs_def cdclW_restart_mset.cdclW_stgy_invariant_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def
      conflicting.simps cdclW_restart_mset.no_smaller_confl_def clauses_def trail.simps
      dest!: get_all_ann_decomposition_exists_prepend)

lemma rtranclp_cdcl_twl_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_restart** S T› and
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms by (induction rule: rtranclp_induct) (auto simp: cdcl_twl_restart_twl_stgy_invs)


context twl_restart_ops
begin

inductive cdcl_twl_stgy_restart :: ‹'v twl_st × nat ⇒ 'v twl_st × nat ⇒ bool› where
restart_step:
  ‹cdcl_twl_stgy_restart (S, n) (U, Suc n)›
  if
    ‹cdcl_twl_stgy++ S T› and
    ‹size (get_learned_clss T) > f n› and
    ‹cdcl_twl_restart T U› |
restart_full:
 ‹cdcl_twl_stgy_restart (S, n) (T, n)›
 if
    ‹full1 cdcl_twl_stgy S T›

lemma cdcl_twl_stgy_restart_init_clss:
  assumes ‹cdcl_twl_stgy_restart S T›
  shows
    ‹get_all_init_clss (fst S) = get_all_init_clss (fst T)›
  by (use assms in ‹induction rule: cdcl_twl_stgy_restart.induct›)
     (auto simp: full1_def cdcl_twl_restart.simps
     dest: rtranclp_cdcl_twl_stgy_all_learned_diff_learned dest!: tranclp_into_rtranclp)

lemma rtranclp_cdcl_twl_stgy_restart_init_clss:
  assumes ‹cdcl_twl_stgy_restart** S T›
  shows
    ‹get_all_init_clss (fst S) = get_all_init_clss (fst T)›
  by (use assms in ‹induction rule: rtranclp_induct›)
   (auto simp: full1_def dest: cdcl_twl_stgy_restart_init_clss)

lemma cdcl_twl_stgy_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_stgy_restart S T› and
    ‹twl_struct_invs (fst S)›
  shows ‹twl_struct_invs (fst T)›
  using assms
  by (induction rule: cdcl_twl_stgy_restart.induct)
     (auto simp add: full1_def intro: rtranclp_cdcl_twl_stgy_twl_struct_invs tranclp_into_rtranclp
      cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_twl_stgy_invs)

lemma rtranclp_cdcl_twl_stgy_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_stgy_restart** S T› and
    ‹twl_struct_invs (fst S)›
  shows ‹twl_struct_invs (fst T)›
  using assms
  by (induction)
     (auto intro: cdcl_twl_stgy_restart_twl_struct_invs)

lemma cdcl_twl_stgy_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_stgy_restart S T› and
    ‹twl_struct_invs (fst S)› and
    ‹twl_stgy_invs (fst S)›
  shows ‹twl_stgy_invs (fst T)›
  using assms
  by (induction rule: cdcl_twl_stgy_restart.induct)
    (auto simp add: full1_def dest!: tranclp_into_rtranclp
      intro: cdcl_twl_restart_twl_stgy_invs rtranclp_cdcl_twl_stgy_twl_stgy_invs )

lemma no_step_cdcl_twl_stgy_restart_cdcl_twl_stgy:
  assumes
    ns: ‹no_step cdcl_twl_stgy_restart S› and
    ‹twl_struct_invs (fst S)›
  shows
    ‹no_step cdcl_twl_stgy (fst S)›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain T where T: ‹cdcl_twl_stgy (fst S) T› by blast
  then have ‹twl_struct_invs T›
    using assms(2) cdcl_twl_stgy_twl_struct_invs by blast
  obtain U where U: ‹full (λS T. twl_struct_invs S ∧ cdcl_twl_stgy S T) T U›
   using wf_exists_normal_form_full[OF wf_cdcl_twl_stgy] by blast
  have ‹full cdcl_twl_stgy T U›
  proof -
    have
      st: ‹(λS T. twl_struct_invs S ∧ cdcl_twl_stgy S T)** T U› and
      ns: ‹no_step (λU V. twl_struct_invs U ∧ cdcl_twl_stgy U V) U›
      using U unfolding full_def by blast+
    have ‹cdcl_twl_stgy** T U›
      using st by (induction rule: rtranclp_induct) auto
    moreover have ‹no_step cdcl_twl_stgy U›
      using ns ‹twl_struct_invs T› calculation rtranclp_cdcl_twl_stgy_twl_struct_invs by blast
    ultimately show ?thesis
      unfolding full_def by blast
  qed
  then have ‹full1 cdcl_twl_stgy (fst S) U›
    using T by (auto intro: full_fullI)
  then show False
    using ns cdcl_twl_stgy_restart.intros(2)[of ‹fst S› U ‹snd S›]
    by fastforce
qed

lemma (in -) substract_left_le: ‹(a :: nat) + b < c ==> a <= c - b›
  by auto

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

lemma (in -) learned_clss_get_all_learned_clss[simp]:
   ‹learned_clss (stateW_of S) = get_all_learned_clss S›
  by (cases S) (auto simp: learned_clss.simps)

lemma cdcl_twl_stgy_restart_new_learned_in_all_simple_clss:
  assumes
    st: ‹cdcl_twl_stgy_restart** R S› and
    invR: ‹twl_struct_invs (fst R)›
  shows ‹set_mset (clauses (get_learned_clss (fst S))) ⊆
     simple_clss (atms_of_mm (get_all_init_clss (fst S)))›
proof
  fix C
  assume C: ‹C ∈# clauses (get_learned_clss (fst S))›
  have invS: ‹twl_struct_invs (fst S)›
    using invR rtranclp_cdcl_twl_stgy_restart_twl_struct_invs st by blast
  then have dist: ‹cdclW_restart_mset.distinct_cdclW_state (stateW_of (fst S))› and
      alien: ‹cdclW_restart_mset.no_strange_atm (stateW_of (fst S))›
    unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def by fast+
  have ‹atms_of C ⊆ atms_of_mm (get_all_init_clss (fst S))›
    using alien C unfolding cdclW_restart_mset.no_strange_atm_def
    by (cases S) (auto dest!: multi_member_split simp: cdclW_restart_mset_state)
  moreover have ‹distinct_mset C›
    using dist C unfolding cdclW_restart_mset.distinct_cdclW_state_def distinct_mset_set_def
    by (cases S) (auto dest: in_diffD simp: cdclW_restart_mset_state)
  moreover have ‹¬ tautology C›
    using invS C unfolding cdclW_restart_mset.cdclW_all_struct_inv_def twl_struct_invs_def
    by (cases S) (auto dest: in_diffD)
  ultimately show ‹C ∈ simple_clss (atms_of_mm (get_all_init_clss (fst S)))›
    unfolding simple_clss_def
    by clarify
qed

lemma cdcl_twl_stgy_restart_new:
  assumes
   ‹cdcl_twl_stgy_restart S T› and
   ‹twl_struct_invs (fst S)› and
   ‹distinct_mset (get_all_learned_clss (fst S) - A)›
 shows ‹distinct_mset (get_all_learned_clss (fst T) - A)›
  using assms
proof induction
  case (restart_step S T n U) note st = this(1) and res = this(3) and invs = this(4) and
    dist = this(5)
  have st: ‹ cdcl_twl_stgy** S T›
    using st by auto
  have ‹get_all_learned_clss U ⊆# get_all_learned_clss T›
    using res by (auto simp: cdcl_twl_restart.simps
     image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union])
  then have ‹get_all_learned_clss U - A ⊆#
          learned_clss (stateW_of T) - A›
    using mset_le_subtract by (cases S; cases T; cases U)
       (auto simp: learned_clss.simps ac_simps
        intro!: distinct_mset_mono[of ‹get_all_learned_clss U - get_all_learned_clss S›
          ‹learned_clss (stateW_of T) - learned_clss (stateW_of S)›])
  moreover {
    have ‹cdclW_restart_mset.cdclW_stgy** (stateW_of S) (stateW_of T)›
      by (rule rtranclp_cdcl_twl_stgy_cdclW_stgy[OF st]) (use invs in simp)
    then have ‹distinct_mset (learned_clss (stateW_of T) - A)›
      apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs)
      subgoal using invs unfolding twl_struct_invs_def fst_conv by fast
      subgoal using invs unfolding twl_struct_invs_def fst_conv by fast
      subgoal using dist by simp
      done
  }
  ultimately show ?case
    unfolding fst_conv
    by (rule distinct_mset_mono)
next
  case (restart_full S T n) note st = this(1) and invs = this(2) and dist = this(3)
  have st: ‹cdcl_twl_stgy** S T›
    using st unfolding full1_def by fastforce
  have ‹cdclW_restart_mset.cdclW_stgy** (stateW_of S) (stateW_of T)›
    by (rule rtranclp_cdcl_twl_stgy_cdclW_stgy[OF st]) (use invs in simp)
  then have ‹distinct_mset (learned_clss (stateW_of T) - A)›
    apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs)
    subgoal using invs unfolding twl_struct_invs_def fst_conv by fast
    subgoal using invs unfolding twl_struct_invs_def fst_conv by fast
    subgoal using dist by simp
    done
  then show ?case
    by (cases S; cases T) (auto simp: learned_clss.simps)
qed

lemma rtranclp_cdcl_twl_stgy_restart_new_abs:
  assumes
    ‹cdcl_twl_stgy_restart** S T› and
    ‹twl_struct_invs (fst S)› and
    ‹distinct_mset (get_all_learned_clss (fst S) - A)›
  shows ‹distinct_mset (get_all_learned_clss (fst T) - A)›
  using assms apply (induction)
  subgoal by auto
  subgoal by (auto intro: cdcl_twl_stgy_restart_new rtranclp_cdcl_twl_stgy_restart_twl_struct_invs)
  done

end


context twl_restart
begin

theorem wf_cdcl_twl_stgy_restart:
  ‹wf {(T, S :: 'v twl_st × nat). twl_struct_invs (fst S) ∧ cdcl_twl_stgy_restart S T}›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g :: ‹nat ⇒ 'v twl_st × nat› where
    g: ‹⋀i. cdcl_twl_stgy_restart (g i) (g (Suc i))› and
    inv: ‹⋀i. twl_struct_invs (fst (g i))›
    unfolding wf_iff_no_infinite_down_chain by fast

  have H: False if ‹no_step cdcl_twl_stgy (fst (g i))› for i
    using g[of i] that
    unfolding cdcl_twl_stgy_restart.simps
    by (auto simp: full1_def tranclp_unfold_begin)

  have snd_g: ‹snd (g i) = i + snd (g 0)› for i
    apply (induction i)
    subgoal by auto
    subgoal for i
      using g[of i] H[of ‹Suc i›] by (auto simp: cdcl_twl_stgy_restart.simps full1_def)
    done
  then have snd_g_0: ‹⋀i. i > 0 ⟹ snd (g i) = i + snd (g 0)›
    by blast
  have unbounded_f_g: ‹unbounded (λi. f (snd (g i)))›
    using f unfolding bounded_def by (metis add.commute f less_or_eq_imp_le snd_g
        not_bounded_nat_exists_larger not_le le_iff_add)

  have ‹∃h. cdcl_twl_stgy++ (fst (g i)) (h) ∧
         size (get_all_learned_clss (h)) > f (snd (g i)) ∧
         cdcl_twl_restart (h) (fst (g (i+1)))›
    for i
    using g[of i] H[of ‹Suc i›]
    unfolding cdcl_twl_stgy_restart.simps full1_def Suc_eq_plus1[symmetric]
    by force
  then obtain h :: ‹nat ⇒ 'v twl_st› where
    cdcl_twl: ‹cdcl_twl_stgy++ (fst (g i)) (h i)› and
    size_h_g: ‹size (get_all_learned_clss (h i)) > f (snd (g i))› and
    res: ‹cdcl_twl_restart (h i) (fst (g (i+1)))› for i
    by metis

  obtain k where
    f_g_k: ‹f (snd (g k)) >
       card (simple_clss (atms_of_mm (init_clss (stateW_of (h 0))))) +
           size (get_all_learned_clss (fst (g 0)))›
    using not_bounded_nat_exists_larger[OF unbounded_f_g] by blast
  have cdcl_twl: ‹cdcl_twl_stgy** (fst (g i)) (h i)› for i
    using cdcl_twl[of i] by auto
  have W_g_h: ‹cdclW_restart_mset.cdclW_stgy** (stateW_of (fst (g i))) (stateW_of (h i))› for i
    by (rule rtranclp_cdcl_twl_stgy_cdclW_stgy[OF cdcl_twl]) (rule inv)
  have tranclp_g: ‹cdcl_twl_stgy_restart** (g 0) (g i)› for i
    apply (induction i)
    subgoal by auto
    subgoal for i using g[of i] by auto
    done

  have dist_all_g:
    ‹distinct_mset (get_all_learned_clss (fst (g i)) - get_all_learned_clss (fst (g 0)))›
    for i
    apply (rule rtranclp_cdcl_twl_stgy_restart_new_abs[OF tranclp_g])
    subgoal using inv .
    subgoal by simp
    done

  have dist_h: ‹distinct_mset (get_all_learned_clss (h i) - get_all_learned_clss (fst (g 0)))›
    (is ‹distinct_mset (?U i)›)
    for i
    unfolding learned_clss_get_all_learned_clss[symmetric]
    apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs[OF W_g_h])
    subgoal using inv[of i] unfolding twl_struct_invs_def by fast
    subgoal using inv[of i] unfolding twl_struct_invs_def by fast
    subgoal using dist_all_g[of i] distinct_mset_minus
      unfolding learned_clss_get_all_learned_clss by auto
    done
  have dist_diff: ‹distinct_mset (c + (Ca + C) - ai) ⟹
       distinct_mset (c - ai)› for c Ca C ai
    by (metis add_diff_cancel_right' cancel_ab_semigroup_add_class.diff_right_commute
        distinct_mset_minus)

  have ‹get_all_learned_clss (fst (g (Suc i))) ⊆# get_all_learned_clss (h i)› for i
    using res[of i] by (auto simp: cdcl_twl_restart.simps
      image_mset_subseteq_mono[of ‹_ + _› _ clause, unfolded image_mset_union]
      intro: mset_le_decr_left1)

  have h_g: ‹init_clss (stateW_of (h i)) = init_clss (stateW_of (fst (g i)))› for i
    using cdclW_restart_mset.rtranclp_cdclW_stgy_no_more_init_clss[OF W_g_h[of i]] ..

  have h_g_Suc: ‹init_clss (stateW_of (h i)) = init_clss (stateW_of (fst (g (Suc i))))› for i
    using res[of i] by (auto simp: cdcl_twl_restart.simps init_clss.simps)
  have init_g_0: ‹init_clss (stateW_of (fst (g i))) = init_clss (stateW_of (fst (g 0)))› for i
    apply (induction i)
    subgoal ..
    subgoal for j
      using h_g[of j] h_g_Suc[of j] by simp
    done
  then have K: ‹init_clss (stateW_of (h i)) = init_clss (stateW_of (fst (g 0)))› for i
    using h_g[of i] by simp

  have incl: ‹set_mset (get_all_learned_clss (h i)) ⊆
         simple_clss (atms_of_mm (init_clss (stateW_of (h i))))› for i
    unfolding learned_clss_get_all_learned_clss[symmetric]
    supply [[unify_trace_failure]]
    apply (rule cdclW_restart_mset.cdclW_stgy_new_learned_in_all_simple_clss[of ‹stateW_of (fst (g i))›])
    subgoal by (rule rtranclp_cdcl_twl_stgy_cdclW_stgy[OF cdcl_twl]) (rule inv)
    subgoal using inv[of i]  unfolding twl_struct_invs_def by fast
    done
  have incl: ‹set_mset (get_all_learned_clss (h i)) ⊆
         simple_clss (atms_of_mm (init_clss (stateW_of (h i))))›  (is ‹set_mset (?V i) ⊆ _›) for i
    using incl[of i] by (cases ‹h i›) (auto dest: in_diffD)

  have incl_init: ‹set_mset (?U i) ⊆ simple_clss (atms_of_mm (init_clss (stateW_of (h i))))› for i
    using incl[of i] by (auto dest: in_diffD)
  have size_U_atms: ‹size (?U i) ≤ card (simple_clss (atms_of_mm (init_clss (stateW_of (h i)))))› for i
    apply (subst distinct_mset_size_eq_card[OF dist_h])
    apply (rule card_mono[OF _ incl_init])
    by (auto simp: simple_clss_finite)
  have S:
    ‹size (?V i) - size (get_all_learned_clss (fst (g 0))) ≤
      card (simple_clss (atms_of_mm (init_clss (stateW_of (h i)))))› for i
    apply (rule order.trans)
     apply (rule diff_size_le_size_Diff)
    apply (rule size_U_atms)
    done
  have S:
    ‹size (?V i) ≤
      card (simple_clss (atms_of_mm (init_clss (stateW_of (h i))))) +
       size (get_all_learned_clss (fst (g 0)))› for i
    using S[of i] by auto

  have H: ‹card (simple_clss (atms_of_mm (init_clss (stateW_of (h k))))) +
         size (get_all_learned_clss (fst (g 0))) > f (k + snd (g 0))› for k
    using S[of k] size_h_g[of k] unfolding snd_g[symmetric]
    by force

  show False
    using H[of k] f_g_k unfolding snd_g[symmetric]
    unfolding K
    by linarith
qed

end

abbreviation stateW_of_restart where
  ‹stateW_of_restart ≡ (λ(S, n). (stateW_of S, n))›

context twl_restart_ops
begin

lemma rtranclp_cdcl_twl_stgy_cdclW_restart_stgy:
  ‹cdcl_twl_stgy** S T ⟹ twl_struct_invs S ⟹
    cdclW_restart_mset.cdclW_restart_stgy** (stateW_of S, n) (stateW_of T, n)›
  using rtranclp_cdcl_twl_stgy_cdclW_stgy[of S T]
  by (auto dest: cdclW_restart_mset.rtranclp_cdclW_restart_stgy_cdclW_restart
     cdclW_restart_mset.rtranclp_cdclW_stgy_cdclW_restart_stgy)

lemma cdcl_twl_stgy_restart_cdclW_restart_stgy:
  ‹cdcl_twl_stgy_restart S T ⟹ twl_struct_invs (fst S) ⟹  twl_stgy_invs (fst S) ⟹
    cdclW_restart_mset.cdclW_restart_stgy** (stateW_of_restart S) (stateW_of_restart T)›
  apply (induction rule: cdcl_twl_stgy_restart.induct)
  subgoal for S T n U
    using rtranclp_cdcl_twl_stgy_cdclW_restart_stgy[of S T n]
      cdclW_restart_mset.cdclW_restart_stgy.intros [of ‹stateW_of_restart(T, n)›
        ‹(_, Suc n)›]
      cdclW_restart_mset.rtranclp_cdclW_stgy_cdclW_restart_stgy[of ‹_›
        ‹stateW_of U› ‹Suc n›]
       cdcl_twl_restart_cdclW_stgy[of T U]
       rtranclp_cdcl_twl_stgy_twl_struct_invs[of S T]
       rtranclp_cdcl_twl_stgy_twl_stgy_invs[of S T]
    apply (auto dest!: tranclp_into_rtranclp)
    by (meson r_into_rtranclp rtranclp_trans)
  subgoal for S T n
    using rtranclp_cdcl_twl_stgy_cdclW_restart_stgy[of S T n]
       rtranclp_cdcl_twl_stgy_twl_struct_invs[of S T]
       rtranclp_cdcl_twl_stgy_twl_stgy_invs[of S T]
    by (auto dest!: tranclp_into_rtranclp simp: full1_def)
  done

lemma rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_stgy_restart** S T› and
    ‹twl_struct_invs (fst S)› and
    ‹twl_stgy_invs (fst S)›
  shows ‹twl_stgy_invs (fst T)›
  using assms
  by (induction rule: rtranclp_induct)
    (auto intro: cdcl_twl_stgy_restart_twl_stgy_invs
        rtranclp_cdcl_twl_stgy_restart_twl_struct_invs)

lemma rtranclp_cdcl_twl_stgy_restart_cdclW_restart_stgy:
  ‹cdcl_twl_stgy_restart** S T ⟹ twl_struct_invs (fst S) ⟹  twl_stgy_invs (fst S) ⟹
    cdclW_restart_mset.cdclW_restart_stgy** (stateW_of_restart S) (stateW_of_restart T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S T]
       rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S T]
       cdcl_twl_stgy_restart_cdclW_restart_stgy[of T U]
    by (auto dest!: tranclp_into_rtranclp)
  done



definition (in twl_restart_ops) cdcl_twl_stgy_restart_with_leftovers where
  ‹cdcl_twl_stgy_restart_with_leftovers S U ⟷
     (∃T. cdcl_twl_stgy_restart** S (T, snd U) ∧ cdcl_twl_stgy** T (fst U))›

lemma cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart:
  ‹cdcl_twl_stgy_restart (T, m) (V, Suc m) ⟹
       cdcl_twl_stgy** S T ⟹ cdcl_twl_stgy_restart (S, m) (V, Suc m)›
  by (subst (asm) cdcl_twl_stgy_restart.simps)
   (auto simp: intro: cdcl_twl_stgy_restart.intros
      dest: rtranclp_tranclp_tranclp)

lemma cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2:
  ‹cdcl_twl_stgy_restart (T, m) (V, m) ⟹
       cdcl_twl_stgy** S T ⟹ cdcl_twl_stgy_restart (S, m) (V, m)›
  by (subst (asm) cdcl_twl_stgy_restart.simps)
    (auto simp: intro: cdcl_twl_stgy_restart.intros
      dest: rtranclp_tranclp_tranclp rtranclp_full1I)


definition cdcl_twl_stgy_restart_with_leftovers1 where
  ‹cdcl_twl_stgy_restart_with_leftovers1 S U ⟷
     cdcl_twl_stgy_restart S U ∨
     (cdcl_twl_stgy++ (fst S) (fst U) ∧ snd S = snd U)›

lemma (in twl_restart) wf_cdcl_twl_stgy_restart_with_leftovers1:
  ‹wf {(T :: 'v twl_st × nat, S).
        twl_struct_invs (fst S) ∧ cdcl_twl_stgy_restart_with_leftovers1 S T}›
  (is ‹wf ?S›)
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g :: ‹nat ⇒ 'v twl_st × nat› where
    g: ‹⋀i. cdcl_twl_stgy_restart_with_leftovers1 (g i) (g (Suc i))› and
    inv: ‹⋀i. twl_struct_invs (fst (g i))›
    unfolding wf_iff_no_infinite_down_chain by fast
  have ns: ‹¬no_step cdcl_twl_stgy (fst (g i))› for i
    using g[of i]
    by (fastforce simp: cdcl_twl_stgy_restart_with_leftovers1_def
        cdcl_twl_stgy_restart.simps full1_def tranclp_unfold_begin)

  define h where
    ‹h ≡ rec_nat (g 0) (λi Si. g (SOME k. cdcl_twl_stgy_restart Si (g k)))›
  have [simp]: ‹h 0 = g 0›
    unfolding h_def by auto

  have L: ‹cdcl_twl_stgy++ (fst (g i)) (fst (g (Suc (i + k)))) ∧
         cdcl_twl_stgy++ (fst (g (i + k))) (fst (g (Suc (i + k)))) ∧
         snd (g (Suc (i + k))) = snd (g i)›
    if ‹k < j› and
      H: ‹⋀k. k ≤ j ⟹ ¬cdcl_twl_stgy_restart (g i) (g (Suc i + k))›
    for k i j
    using that
  proof (induction j arbitrary: k)
    case 0
    then show ?case by auto
  next
    case (Suc j k)
    then have
      IH: ‹⋀k. k < j ⟹
         cdcl_twl_stgy++ (fst (g i)) (fst (g (Suc (i + k)))) ∧
         cdcl_twl_stgy++ (fst (g (i + k))) (fst (g (Suc (i + k)))) ∧
         snd (g (Suc (i + k))) = snd (g i)› and
      ‹k < Suc j› and
      H: ‹⋀k. k ≤ Suc j ⟹ ¬ cdcl_twl_stgy_restart (g i) (g (Suc i + k))›
      by auto
    show ?case
    proof (cases ‹k = j›)
      case False
      then show ?thesis
        using IH[of k] ‹k < Suc j› by simp
    next
      case [simp]: True
      consider
        (res) ‹cdcl_twl_stgy_restart (g ( (i+k))) (g ((Suc (i+k))))› |
        (stgy) ‹cdcl_twl_stgy++ (fst (g ((i+k)))) (fst (g ((Suc (i+k)))))› and
        ‹snd (g (Suc (i + k))) = snd (g (i + k))›
        using g[of ‹i+k›] unfolding cdcl_twl_stgy_restart_with_leftovers1_def
        by auto
      then show ?thesis
      proof cases
        case stgy
        then show ?thesis
          using IH[of ‹k - 1›]
          by (cases ‹0 < j›) auto
      next
        case res
        have Sucg: ‹Suc (snd (g ((i + k)))) = snd (g (Suc ((i + k))))›
          using res
            ns[of ‹Suc ((i + k))›]
          by (auto simp: cdcl_twl_stgy_restart.simps full1_def)

        have ‹cdcl_twl_stgy_restart (g i) (g (Suc (i + k)))›
          using IH[of ‹k - 1›]
            res cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart[ of ‹fst (g ((i + k)))›
              ‹snd (g ((i + k)))› ‹fst (g (Suc ((i + k))))› ‹fst (g i)›]
          unfolding Sucg prod.collapse
          by (cases ‹0 < j›) (auto intro!: cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart
              dest!: tranclp_into_rtranclp)
        then show ?thesis
          using H[of k] ‹k < Suc j›
          by auto
      qed
    qed
  qed
  have Ex_cdcl_twl_stgy_restart: ‹∃k > i. cdcl_twl_stgy_restart (g i) (g k)› for i
  proof (rule ccontr)
    assume ‹¬ ?thesis›
    then have H: ‹⋀k. k > i ⟹ ¬cdcl_twl_stgy_restart (g i) (g k)›
      by fast

    define g' where
      ‹g' = (λk. fst (g (k + i)))›
    have L: ‹cdcl_twl_stgy++ (fst (g i)) (fst (g (Suc (i + k)))) ∧
         cdcl_twl_stgy++ (fst (g (i + k))) (fst (g (Suc (i + k)))) ∧
         snd (g (Suc (i + k))) = snd (g i)›
      for k
      using L[of k ‹k+1› i] H[of ‹Suc i+_›]
      by auto
    have ‹(g' (Suc k), g' k) ∈ {(T, S). twl_struct_invs S ∧ cdcl_twl_stgy++ S T}› for k
      using L[of k] inv
      unfolding g'_def
      by (auto simp: ac_simps)
    then show False
      using tranclp_wf_cdcl_twl_stgy
      unfolding wf_iff_no_infinite_down_chain
      by fast
  qed
  have h_Suc: ‹h (Suc i) = g (SOME j. cdcl_twl_stgy_restart (h i) (g j))› for i
    unfolding h_def by auto
  have h_g: ‹∃j. h i = g j› for i
  proof (induction i)
    case 0
    then show ?case by auto
  next
    case (Suc i)
    then obtain i' where
      i': ‹h i = g i'›
      by blast
    define j where ‹j ≡ SOME j. cdcl_twl_stgy_restart (h i) (g j)›
    obtain k where
      k: ‹k > i'› and
      i_k: ‹cdcl_twl_stgy_restart (g i') (g k)›
      using Ex_cdcl_twl_stgy_restart[of i'] by blast
    have ‹cdcl_twl_stgy_restart (h i) (g j)›
      unfolding j_def
      apply (rule someI[of ‹λS. cdcl_twl_stgy_restart (h i) (g S)›])
      using k i_k unfolding i' by fast
    then show ?case
      unfolding h_Suc by auto
  qed

  have ‹cdcl_twl_stgy_restart (h i) (h (Suc i))› for i
  proof -
    obtain i' where
       h_g_i: ‹h i = g i'›
      using h_g by fast
    define j where ‹j ≡ SOME j. cdcl_twl_stgy_restart (h i) (g j)›
    obtain k where
      k: ‹k > i'› and
      i_k: ‹cdcl_twl_stgy_restart (g i') (g k)›
      using Ex_cdcl_twl_stgy_restart[of i'] by blast
    have ‹cdcl_twl_stgy_restart (h i) (g j)›
      unfolding j_def
      apply (rule someI[of _ k])
      using k i_k unfolding h_g_i by fast
    then show ?thesis
      unfolding h_Suc j_def[symmetric] .
  qed
  moreover have ‹⋀i. twl_struct_invs (fst (h i))›
    using inv h_g by metis
  ultimately show False
    using wf_cdcl_twl_stgy_restart
    unfolding wf_iff_no_infinite_down_chain by fast
qed


lemma (in twl_restart) wf_cdcl_twl_stgy_restart_measure:
   ‹wf ({((brkT, T, n), brkS, S, m).
         twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
        {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS})›
  (is ‹wf (?TWL ∪ ?BOOL)›)
proof (rule wf_union_compatible)
  show ‹wf ?TWL›
    apply (rule wf_subset)
     apply (rule wf_snd_wf_pair[OF wf_cdcl_twl_stgy_restart_with_leftovers1])
    by auto
  show ‹?TWL O ?BOOL ⊆ ?TWL›
    by auto

  show ‹wf ?BOOL›
    unfolding wf_iff_no_infinite_down_chain
  proof clarify
    fix f :: ‹nat ⇒ bool × 'b›
    assume H: ‹∀i. (f (Suc i), f i) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
    then have ‹(f (Suc 0), f 0) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}› and
      ‹(f (Suc 1), f 1) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
      by presburger+
    then show False
      by auto
  qed
qed

lemma (in twl_restart) wf_cdcl_twl_stgy_restart_measure_early:
   ‹wf ({((ebrk, brkT, T, n), ebrk, brkS, S, m).
         twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
        {((ebrkT, brkT, T), (ebrkS, brkS, S)). S = T ∧ (ebrkT ∨ brkT) ∧ (¬brkS ∧ ¬ebrkS)})›
  (is ‹wf (?TWL ∪ ?BOOL)›)
proof (rule wf_union_compatible)
  show ‹wf ?TWL›
    apply (rule wf_subset)
    apply (rule wf_snd_wf_pair)
     apply (rule wf_snd_wf_pair[OF wf_cdcl_twl_stgy_restart_with_leftovers1])
    by auto
  show ‹?TWL O ?BOOL ⊆ ?TWL›
    by auto

  show ‹wf ?BOOL›
    unfolding wf_iff_no_infinite_down_chain
  proof clarify
    fix f :: ‹nat ⇒ bool × bool × _›
    assume H: ‹∀i. (f (Suc i), f i) ∈ ?BOOL›
    then have ‹(f (Suc 0), f 0) ∈ ?BOOL› and
      ‹(f (Suc 1), f 1) ∈ ?BOOL›
      by presburger+
    then show False
      by auto
  qed
qed


lemma cdcl_twl_stgy_restart_with_leftovers_cdclW_restart_stgy:
  ‹cdcl_twl_stgy_restart_with_leftovers S T ⟹ twl_struct_invs (fst S) ⟹  twl_stgy_invs (fst S) ⟹
    cdclW_restart_mset.cdclW_restart_stgy** (stateW_of_restart S) (stateW_of_restart T)›
  unfolding cdcl_twl_stgy_restart_with_leftovers_def
  apply (rule exE)
   apply assumption
  subgoal for S'
    using
      rtranclp_cdcl_twl_stgy_restart_cdclW_restart_stgy[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_cdclW_restart_stgy[of S' ‹fst T› ‹snd T›]
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S ‹(S', snd T)›]
      by (cases T) auto
  done

lemma cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs:
  ‹cdcl_twl_stgy_restart_with_leftovers S T ⟹ twl_struct_invs (fst S) ⟹
    twl_struct_invs (fst T)›
  unfolding cdcl_twl_stgy_restart_with_leftovers_def
  apply (rule exE)
   apply assumption
  subgoal for S'
    using
      rtranclp_cdcl_twl_stgy_twl_struct_invs[of ‹S'› ‹(fst T)›]
      rtranclp_cdcl_twl_stgy_restart_cdclW_restart_stgy[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_cdclW_restart_stgy[of S' ‹fst T› ‹snd T›]
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S ‹(S', snd T)›]
    by auto
  done

lemma rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs:
  ‹cdcl_twl_stgy_restart_with_leftovers** S T ⟹ twl_struct_invs (fst S) ⟹
    twl_struct_invs (fst T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs[of T U]
    by auto
  done

lemma cdcl_twl_stgy_restart_with_leftovers_twl_stgy_invs:
  ‹cdcl_twl_stgy_restart_with_leftovers S T ⟹ twl_struct_invs (fst S) ⟹
    twl_stgy_invs (fst S) ⟹ twl_stgy_invs (fst T)›
  unfolding cdcl_twl_stgy_restart_with_leftovers_def
  apply (rule exE)
  apply assumption
  subgoal for S'
    using
      rtranclp_cdcl_twl_stgy_twl_struct_invs[of ‹S'› ‹(fst T)›]
      rtranclp_cdcl_twl_stgy_twl_stgy_invs[of ‹S'› ‹(fst T)›]
      rtranclp_cdcl_twl_stgy_restart_cdclW_restart_stgy[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_cdclW_restart_stgy[of S' ‹fst T› ‹snd T›]
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of S ‹(S', snd T)›]
      rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S ‹(S', snd T)›]
    by auto
  done

lemma rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_stgy_invs:
  ‹cdcl_twl_stgy_restart_with_leftovers** S T ⟹ twl_struct_invs (fst S) ⟹
    twl_stgy_invs (fst S) ⟹ twl_stgy_invs (fst T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_with_leftovers_twl_stgy_invs[of T U]
      rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs[of S T]
    by auto
  done

lemma rtranclp_cdcl_twl_stgy_restart_with_leftovers_cdclW_restart_stgy:
  ‹cdcl_twl_stgy_restart_with_leftovers** S T ⟹ twl_struct_invs (fst S) ⟹ twl_stgy_invs (fst S) ⟹
    cdclW_restart_mset.cdclW_restart_stgy** (stateW_of_restart S) (stateW_of_restart T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_with_leftovers_cdclW_restart_stgy[of T U]
    rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs[of S T]
    rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_stgy_invs[of S T]
    by auto
  done

end

end