Theory Watched_Literals_Transition_System_Inprocessing

theory Watched_Literals_Transition_System_Inprocessing
  imports Watched_Literals_Transition_System
begin
text ‹
  The subsumption is very similar to the PCDCL case.
›
inductive cdcl_twl_subsumed :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
subsumed_II:
  ‹cdcl_twl_subsumed (M, N + {#C, C'#}, U, D, NE, UE, NS, US, N0, U0, {#}, Q)
     (M, add_mset C N, U, D, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
  if ‹clause C ⊆# clause C'› |
subsumed_RR:
  ‹cdcl_twl_subsumed (M, N, U + {#C, C'#}, D, NE, UE, NS, US, N0, U0, {#}, Q)
     (M, N, add_mset C U, D, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
  if ‹clause C ⊆# clause C'› |
subsumed_IR:
  ‹cdcl_twl_subsumed (M, add_mset C N, add_mset C' U, D, NE, UE, NS, US, N0, U0, {#}, Q)
     (M, add_mset C N, U, D, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
  if ‹clause C ⊆# clause C'› |
subsumed_RI:
  ‹cdcl_twl_subsumed (M, add_mset C' N, add_mset C U, D, NE, UE, NS, US, N0, U0, {#}, Q)
     (M, add_mset C N, U, D, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
  if ‹clause C ⊆# clause C'› ‹¬tautology (clause C)› ‹distinct_mset (clause C)›

lemma cdcl_twl_subsumed_cdcl_subsumed:
  ‹cdcl_twl_subsumed S T ⟹ cdcl_subsumed (pstateW_of S) (pstateW_of T) ∨ cdcl_subsumed_RI (pstateW_of S) (pstateW_of T)›
  apply (induction rule: cdcl_twl_subsumed.induct)
  subgoal by (auto simp: cdcl_subsumed.simps pstateW_of.simps)
  subgoal by (auto simp: cdcl_subsumed.simps)
  subgoal by (auto simp: cdcl_subsumed.simps)
  subgoal by (auto simp: cdcl_subsumed_RI.simps)
  done

lemma cdcl_twl_subsumed_II_simp:
  ‹cdcl_twl_subsumed S S'›
  if ‹S = (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q)›
     ‹S' = (M, remove1_mset C' N, U, D, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›e
    ‹clause C ⊆# clause C'›
    ‹C ∈# N›
    ‹C' ∈# remove1_mset C N›
  using that subsumed_II[of C C'] by (auto dest!: multi_member_split)

lemma cdcl_twl_subsumed_RR_simp:
  ‹cdcl_twl_subsumed S S'›
  if ‹S = (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q)›
     ‹S' = (M, N, remove1_mset C' U, D, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
    ‹clause C ⊆# clause C'›
    ‹C ∈# U›
    ‹C' ∈# remove1_mset C U›
  using that subsumed_RR[of C C' M N ‹U -{#C,C'#}› D NE UE NS US N0 U0 Q]
  by (auto dest!: multi_member_split)

lemma cdcl_twl_subsumed_IR_simp:
  ‹cdcl_twl_subsumed S S'›
  if ‹S = (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q)›
     ‹S' = (M, N, remove1_mset C' U, D, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
    ‹clause C ⊆# clause C'›
    ‹C ∈# N›
    ‹C' ∈# U›
  using that subsumed_IR[of C C' M ‹N - {#C#}› ‹U -{#C'#}› D NE UE NS US N0 U0 Q]
  by (auto dest!: multi_member_split)

lemma cdcl_twl_subsumed_RI_simp:
  ‹cdcl_twl_subsumed S T›
  if ‹S =  (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q)› ‹clause C ⊆# clause C'›
    ‹T = (M, add_mset C (remove1_mset C' N), remove1_mset C U, D, NE, UE, add_mset (clause C') NS,
      US, N0, U0, {#}, Q)›
    ‹¬tautology (clause C)› ‹distinct_mset (clause C)›
    ‹C' ∈# N› ‹C ∈# U›
  using that subsumed_RI[of C C' M ‹N - {#C'#}› ‹U - {#C#}› D NE UE NS US N0 U0 Q]
  by (auto dest!: multi_member_split)

text ‹
  The lifting from term‹cdcl_subresolution› is a lot more complicated due to the handling of
  unit and nonunit clauses. Basically, we have to split every rule in two. Hence we don't have a
  one-to-one mapping anymore, but need to use term‹cdcl_flush_unit› or rule of that kind.

  We don't support (yet) generation of the empty clause. This is very tricky because we entirely
  leave the CDCL calculus.

 The condition term‹∀L ∈# clause E. undefined_lit M L› is not necessary from the point of view of CDCL,
 but it makes it much easier to fulfill the conditions of the watched literals. It should be possible
 to do so, but we would need to add conditions on it. However, this makes the inprocessing harder to
 do.
›
inductive cdcl_twl_subresolution :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
twl_subresolution_II_nonunit:
  ‹cdcl_twl_subresolution (M, N + {#C, C'#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N + {#C, E#}, U, None, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›  ‹¬tautology (D + D')›
   ‹clause E = remdups_mset D'› ‹size (watched E) = 2› ‹struct_wf_twl_cls E› ‹∀L ∈# clause E. undefined_lit M L› |
twl_subresolution_II_unit:
  ‹cdcl_twl_subresolution (M, N + {#C, C'#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K {#K#} # M, N + {#C#}, U, None, add_mset {#K#} NE, UE,
        add_mset (clause C') NS, US, N0, U0, {#}, add_mset (-K) Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›  ‹¬tautology (D + D')›
   ‹remdups_mset D' = {#K#}› ‹undefined_lit M K›|

twl_subresolution_LL_nonunit:
  ‹cdcl_twl_subresolution (M, N, U + {#C, C'#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U + {#C, E#}, None, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹clause E = remdups_mset D'› ‹¬tautology (D + D')› ‹size (watched E) = 2› ‹∀L ∈# clause E. undefined_lit M L› |
twl_subresolution_LL_unit:
  ‹cdcl_twl_subresolution (M, N, U + {#C, C'#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K {#K#} # M, N, U + {#C#}, None, NE, add_mset {#K#} UE, NS,
       add_mset (clause C') US, N0, U0, {#}, add_mset (-K) Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹remdups_mset D' = {#K#}› ‹¬tautology (D + D')› ‹undefined_lit M K›|

twl_subresolution_LI_nonunit:
  ‹cdcl_twl_subresolution (M, N + {#C#}, U + {#C'#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N + {#C#}, U + {#E#}, None, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹clause E = remdups_mset D'›  ‹¬tautology (D + D')› ‹size (watched E) = 2› ‹∀L ∈# clause E. undefined_lit M L›|
twl_subresolution_LI_unit:
  ‹cdcl_twl_subresolution (M, N + {#C#}, U + {#C'#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K {#K#} # M, N + {#C#}, U, None, NE, add_mset {#K#} UE, NS,
      add_mset (clause C') US, N0, U0, {#}, add_mset (-K) Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹remdups_mset D' = {#K#}›  ‹¬tautology (D + D')› ‹undefined_lit M K›|

twl_subresolution_IL_nonunit:
  ‹cdcl_twl_subresolution (M, N + {#C'#}, U + {#C#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N + {#E#}, U + {#C#}, None, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹clause E = remdups_mset D'›  ‹¬tautology (D + D')› ‹size (watched E) = 2› ‹∀L ∈# clause E. undefined_lit M L› |
twl_subresolution_IL_unit:
  ‹cdcl_twl_subresolution (M, N + {#C'#}, U + {#C#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K {#K#} # M, N, U + {#C#}, None, add_mset {#K#} NE, UE,
       add_mset (clause C') NS, US, N0, U0, {#}, add_mset (-K) Q)›
 if
   ‹clause C = add_mset L D›
   ‹clause C' = add_mset (-L) D'›
   ‹count_decided M = 0› ‹D ⊆# D'›
   ‹remdups_mset D' = {#K#}›  ‹¬tautology (D + D')› ‹undefined_lit M K›


lemma past_invs_count_decided0: ‹count_decided (get_trail S) = 0 ⟹ past_invs S›
  by (cases S) (auto simp: past_invs.simps)

lemma cdcl_twl_subresolution_past_invs: ‹cdcl_twl_subresolution S T ⟹ past_invs T›
  by (induction rule: cdcl_twl_subresolution.induct)
    (auto simp: past_invs_count_decided0)

lemma twl_lazy_update_subresII: ‹count_decided M = 0 ⟹ struct_wf_twl_cls C ⟹
  ¬ twl_is_an_exception (C) (Q) {#} ⟹ - K ∉# watched C ⟹
  twl_lazy_update (M) C ⟹
  twl_lazy_update (Propagated K {#K#} # M) C›
  using count_decided_ge_get_level[of M]
  by (cases C)
   (fastforce simp: get_level_cons_if has_blit_def uminus_lit_swap twl_is_an_exception_def
    dest!: multi_member_split
    elim!: size_mset_SucE)

lemma watched_literals_false_of_max_level_prop_lvl0: ‹count_decided M = 0 ⟹ watched_literals_false_of_max_level (Propagated K {#K#} # M) C›
  using count_decided_ge_get_level[of M]
  by (cases C)
   (fastforce simp: get_level_cons_if has_blit_def uminus_lit_swap twl_is_an_exception_def
    dest!: multi_member_split
    elim!: size_mset_SucE)

lemma watched_literals_false_of_max_level_lvl0: ‹count_decided M = 0 ⟹ watched_literals_false_of_max_level (M) C›
  using count_decided_ge_get_level[of M]
  by (cases C)
   (fastforce simp: get_level_cons_if has_blit_def uminus_lit_swap twl_is_an_exception_def
    dest!: multi_member_split
    elim!: size_mset_SucE)

lemma twl_lazy_update_undefined: ‹∀L ∈# clause E. undefined_lit M L ⟹ twl_lazy_update M E›
  by (cases E)
   (auto simp: has_blit_def Decided_Propagated_in_iff_in_lits_of_l
    dest!: multi_member_split)

lemma struct_wf_twl_cls_remdupsI:
  ‹clause E = remdups_mset D' ⟹ size (watched E) = 2 ⟹  struct_wf_twl_cls E›
  by (cases E) auto

lemma cdcl_twl_subresolution_twl_st_inv:
  ‹cdcl_twl_subresolution S T ⟹ twl_st_inv S ⟹ twl_st_inv T›
  by (induction rule: cdcl_twl_subresolution.induct)
    (auto simp: twl_st_inv.simps twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0
    twl_lazy_update_subresII twl_is_an_exception_add_mset_to_queue
    watched_literals_false_of_max_level_prop_lvl0
    intro: struct_wf_twl_cls_remdupsI)

lemma cdcl_twl_subresolution_valid_enqueued:
  ‹cdcl_twl_subresolution S T ⟹ valid_enqueued S ⟹ valid_enqueued T›
  by (induction rule: cdcl_twl_subresolution.induct)
    (auto simp: get_level_cons_if)

lemma cdcl_twl_subresolution_decompE:
  assumes
    ‹cdcl_twl_subresolution S T› and ‹Multiset.Ball (get_clauses S) (distinct_mset o clause)› and
    subres: ‹cdcl_subresolution (pstateW_of S) (pstateW_of T)  ⟹ thesis› and
    unit: ‹⋀S' T'. cdcl_subresolution (pstateW_of S) S' ⟹
     cdcl_propagate S' (T') ⟹ cdcl_flush_unit (T') (pstateW_of T)  ⟹ thesis›
  shows thesis
    using assms(1,2,3)
  apply (cases rule: cdcl_twl_subresolution.cases)
  subgoal for C L D C' D' M E N U NE UE NS US Q
    apply (rule subres)
    using cdcl_subresolution.intros(1)[of M D D' ‹clauses N› L ‹clauses U› None NE UE NS US]
    by auto
  subgoal for C L D C' D' M E N U NE UE NS US N0 U0 Q
    apply (rule unit[of ‹(M, clauses N + {#clause C, D'#}, clauses U, None, NE, UE,
      add_mset (clause C') NS, US, N0, U0)›
      ‹(Propagated E D' # M, clauses N + {#clause C, D'#}, clauses U, None, NE, UE,
        add_mset (clause C') NS, US, N0, U0)›])
    subgoal
      by (auto simp: cdcl_subresolution.simps distinct_mset_remdups_mset_id)
    subgoal
      by (auto simp: cdcl_propagate.simps distinct_mset_remdups_mset_id)
    subgoal
      by (auto simp: cdcl_flush_unit.simps distinct_mset_remdups_mset_id)
    done
    supply[[goals_limit=1]]
    subgoal for C L D C' D' M E N U NE UE NS US Q
      apply (rule subres)
      using cdcl_subresolution.intros(2)[of M D D' ‹clauses N› ‹clauses U› L None NE UE NS US]
      by auto
    subgoal for C L D C' D' M E N U NE UE NS US N0 U0 Q
      apply (rule unit[of ‹(M, clauses N, clauses U + {#clause C, D'#}, None, NE, UE,
        NS, add_mset (clause C') US, N0, U0)›
        ‹(Propagated E D' # M, clauses N, clauses U + {#clause C, D'#}, None, NE, UE, NS,
          add_mset (clause C') US, N0, U0)›])
      subgoal
        apply (auto simp: cdcl_subresolution.simps distinct_mset_remdups_mset_id)
        apply (rule_tac x=D in exI)
        apply (rule_tac x=D' in exI)
        apply auto
        done
      subgoal
        by (auto simp: cdcl_propagate.simps distinct_mset_remdups_mset_id)
      subgoal
        by (auto simp: cdcl_flush_unit.simps distinct_mset_remdups_mset_id)
      done
    subgoal for C L D C' D' M E N U NE UE NS US Q
      apply (rule subres)
      using cdcl_subresolution.intros(3)[of M D D' ‹clauses N› L ‹clauses U› None NE UE NS US]
      by auto
    subgoal for C L D C' D' M E N U NE UE NS US N0 U0 Q
      apply (rule unit[of ‹(M, clauses N + {#clause C#}, clauses U + {#D'#}, None, NE, UE,
        NS, add_mset (clause C') US, N0, U0)›
        ‹(Propagated E D' # M, clauses N + {#clause C#}, clauses U + {#D'#}, None, NE, UE, NS,
          add_mset (clause C') US, N0, U0)›])
      subgoal
        apply (auto simp: cdcl_subresolution.simps distinct_mset_remdups_mset_id)
        apply (drule_tac x=D in spec)
        apply (drule_tac x=D' in spec)
        apply auto
        done
      subgoal
        by (auto simp: cdcl_propagate.simps distinct_mset_remdups_mset_id)
      subgoal
        by (auto simp: cdcl_flush_unit.simps distinct_mset_remdups_mset_id)
      done
    subgoal for C L D C' D' M E N U NE UE NS US N0 U0 Q
      apply (rule subres)
      using cdcl_subresolution.intros(4)[of M D' D ‹clauses N› ‹-L› ‹clauses U› None NE UE NS US]
      by (auto simp: ac_simps)
    subgoal for C L D C' D' M K N U NE UE NS US N0 U0 Q
      apply (rule unit[of ‹(M, clauses N + {#D'#}, clauses U + {#clause C#}, None, NE, UE,
        add_mset (clause C') NS, US, N0, U0)›
        ‹(Propagated K D' # M, clauses N + {#D'#}, clauses U + {#clause C#}, None, NE, UE,
          add_mset (clause C') NS, US, N0, U0)›])
      subgoal
        apply (auto simp: cdcl_subresolution.simps distinct_mset_remdups_mset_id)
        apply (auto 5 5  intro: dest: spec[of _ ‹-L›] dest!: spec[of _ ‹clauses N›])
        done
      subgoal
        by (auto simp: cdcl_propagate.simps distinct_mset_remdups_mset_id)
      subgoal
        by (auto simp: cdcl_flush_unit.simps distinct_mset_remdups_mset_id)
      done
    done

lemma cdcl_twl_subresolution_pcdcl_all_struct_invs:
  ‹cdcl_twl_subresolution S T ⟹
  pcdcl_all_struct_invs (pstateW_of S) ⟹ pcdcl_all_struct_invs (pstateW_of T)›
  apply (elim cdcl_twl_subresolution_decompE)
  subgoal
    by (cases S)
     (auto simp: pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
         cdclW_restart_mset.distinct_cdclW_state_def
      dest!: multi_member_split)
  subgoal
    by (drule cdcl_subresolution)
      (simp_all add: rtranclp_pcdcl_all_struct_invs)
  subgoal
    apply (drule pcdcl.intros pcdcl_core.intros)+
    apply (drule cdcl_subresolution)
    using rtranclp_pcdcl_all_struct_invs by blast
  done

lemma cdcl_twl_subresolution_smaller_propa:
  ‹cdcl_twl_subresolution S T ⟹ cdclW_restart_mset.no_smaller_propa (stateW_of T)›
  apply (induction rule: cdcl_twl_subresolution.induct)
  apply (auto simp: cdclW_restart_mset.no_smaller_propa_def)
  apply (case_tac M'; auto; fail)+
  done
lemma cdcl_twl_subresolution_twl_st_exception_inv:
  ‹cdcl_twl_subresolution S T ⟹ no_dup (get_trail S) ⟹
  twl_st_exception_inv S ⟹ twl_st_exception_inv T›
  apply (induction rule: cdcl_twl_subresolution.induct)
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis mset_subset_eqD mset_subset_eq_add_left set_mset_remdups_mset
      uminus_lits_of_l_definedD)
    apply (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
    by (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis Un_iff clause.simps no_has_blit_propagate twl_clause.sel(1) twl_clause.sel(2))+
    done
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis mset_subset_eqD mset_subset_eq_add_left set_mset_remdups_mset
      uminus_lits_of_l_definedD)
    apply (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
    by (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis Un_iff clause.simps no_has_blit_propagate twl_clause.sel(1) twl_clause.sel(2))+
    done
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis mset_subset_eqD mset_subset_eq_add_left set_mset_remdups_mset
      uminus_lits_of_l_definedD)
    apply (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
    by (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis Un_iff clause.simps no_has_blit_propagate twl_clause.sel(1) twl_clause.sel(2))+
    done
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis mset_subset_eqD mset_subset_eq_add_left set_mset_remdups_mset
      uminus_lits_of_l_definedD)
    apply (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
    by (metis Un_iff clause.simps twl_clause.sel(1) twl_clause.sel(2))
  subgoal
    unfolding twl_st_exception_inv.simps
    apply (intro ballI)
    apply (rename_tac x; case_tac x)
    apply (auto simp: twl_exception_inv.simps)
    apply (metis Un_iff clause.simps no_has_blit_propagate twl_clause.sel(1) twl_clause.sel(2))+
    done
  done


lemma cdcl_twl_subresolution_dup_enqueued:
  ‹cdcl_twl_subresolution S T ⟹ no_duplicate_queued S ⟹ no_duplicate_queued T›
  by (induction rule: cdcl_twl_subresolution.induct) auto

lemma cdcl_twl_subresolution_distinct_enqueued:
  ‹cdcl_twl_subresolution S T ⟹ distinct_queued S ⟹ no_duplicate_queued S ⟹ distinct_queued T›
  apply (induction rule: cdcl_twl_subresolution.induct)
  unfolding distinct_queued.simps
  by (auto dest:  mset_le_add_mset simp: undefined_notin)

lemma Cons_entails_CNotE:
  assumes ‹K # M ⊨as CNot Ca› ‹distinct_mset Ca› and
    1: ‹M ⊨as CNot Ca ⟹ -lit_of K ∉# Ca ⟹ thesis› and
    2: ‹M ⊨as CNot (remove1_mset (-lit_of K) Ca) ⟹ -lit_of K ∈# Ca ⟹ thesis›
  shows thesis
  using assms(1,2)
  apply (cases ‹-lit_of K ∈# Ca›)
  subgoal
    by (rule 2)
     (auto dest!: multi_member_split
      simp: true_annots_true_cls_def_iff_negation_in_model uminus_lit_swap
      add_mset_eq_add_mset)
  subgoal
    by (rule 1)
     (auto dest!: multi_member_split
      simp: true_annots_true_cls_def_iff_negation_in_model uminus_lit_swap
      add_mset_eq_add_mset)
  done

lemma propa_confl_cands_enqueued_simps[simp]:
  ‹propa_confl_cands_enqueued (M, N, U, None, add_mset E NE, UE, NS, US, N0, U0, {#}, Q) ⟷
     propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#},Q)›
  ‹propa_confl_cands_enqueued (M, N, U, None, NE, add_mset E UE, NS, US, N0, U0, {#}, Q) ⟷
    propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#},Q)›
  ‹propa_confl_cands_enqueued (M, N, U, None, NE, UE, add_mset (C') NS, US, N0, U0, {#}, Q) ⟷
     propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  ‹propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, add_mset (C') US, N0, U0, {#}, Q) ⟷
    propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  apply (auto)
  done

lemma propa_confl_cands_enqueuedD:
  ‹propa_confl_cands_enqueued (M, add_mset C N, U, None, NE, UE, NS, US, N0, U0, {#}, Q) ⟹
    propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  ‹propa_confl_cands_enqueued (M, N, add_mset C U, None, NE, UE, NS, US, N0, U0, {#}, Q) ⟹
    propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  by auto

lemma add_mset_diff_add_mset_If:
  "(add_mset L' C) - add_mset L C'= (if L = L' then C - C' else remove1_mset L C + {#L'#} - C')"
  by (auto simp: multiset_eq_iff)

lemma propa_confl_cands_enqueued_propagate:
  assumes
    ‹Multiset.Ball (N+U) (struct_wf_twl_cls)› and
    prev: ‹propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)› and
    excep: ‹twl_st_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)› and
    ‹count_decided M = 0› and
    nd: ‹no_dup (Propagated L C # M)›
  shows ‹propa_confl_cands_enqueued (Propagated L C # M, N, U, None, NE, UE, NS, US, N0, U0,
     {#}, add_mset (-L) Q)›
  unfolding propa_confl_cands_enqueued.simps
proof (intro ballI impI)
  fix Ca La
  assume NU: ‹Ca∈#N + U› and La_Ca: ‹La ∈# clause Ca› and
    ent: ‹Propagated L C # M ⊨as CNot (remove1_mset La (clause Ca))› and
    not_true: ‹La ∉ lits_of_l (Propagated L C # M)›
  have [simp]: ‹get_level M L = 0› for L
    using count_decided_ge_get_level[of M] assms
      by auto
  have dist2: ‹distinct_mset (clause Ca)› and watched: ‹size (watched Ca) = 2›
    using assms(1) NU by (cases Ca; auto dest!: multi_member_split)+
  then have dist: ‹distinct_mset (remove1_mset La (clause Ca))›
    by auto
  show ‹(∃L'. L' ∈# watched Ca ∧ L' ∈# add_mset (- L) Q) ∨ (∃L. (L, Ca) ∈# {#})›
  proof (rule Cons_entails_CNotE[OF ent dist])
    assume ‹M ⊨as CNot (remove1_mset La (clause Ca))› and
      ‹- lit_of (Propagated L C) ∉# remove1_mset La (clause Ca)›
    then have ‹∃L'. L' ∈# watched Ca ∧ L' ∈# Q›
      using prev NU not_true La_Ca
      by (auto simp: dest!: multi_member_split)
    then show ?thesis
      by auto
  next
    assume neg: ‹M ⊨as CNot (remove1_mset (- lit_of (Propagated L C)) (remove1_mset La (clause Ca)))› and
      inL: ‹- lit_of (Propagated L C) ∈# remove1_mset La (clause Ca)›
    with in_diffD[OF this(2)] have [simp]: ‹L ≠ -La› ‹L ≠ La›
      using dist2 not_true by (auto dest!: multi_member_split)

    have ‹twl_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q) Ca›
      using excep NU by auto
    then show ‹(∃L'. L' ∈# watched Ca ∧ L' ∈# add_mset (- L) Q) ∨ (∃L. (L, Ca) ∈# {#})›
      apply -
      apply (rule ccontr)
      using neg watched not_true nd inL
      apply (cases Ca)
      apply (auto elim!: Cons_entails_CNotE dest!: multi_member_split[of _ N] multi_member_split[of ‹-L›]
        simp: distinct_mset_remove1_All uminus_lit_swap removeAll_notin has_blit_def add_mset_diff_add_mset_If
        twl_exception_inv.simps size_2_iff all_conj_distrib remove1_mset_add_mset_If)
      apply (auto split: if_splits simp: remove1_mset_add_mset_If Decided_Propagated_in_iff_in_lits_of_l
        dest: no_dup_consistentD uminus_lits_of_l_definedD
        dest!: multi_member_split; fail)+
      done
  qed
qed

lemma propa_confl_cands_enqueued_learn:
  assumes
    prev: ‹propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)› and
    ‹∀L ∈# clause C. undefined_lit M L› ‹struct_wf_twl_cls C› ‹no_dup M›
  shows ‹propa_confl_cands_enqueued (M, add_mset C N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
    ‹propa_confl_cands_enqueued (M, N, add_mset C U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  using assms
  by (cases C; force simp: size_2_iff Decided_Propagated_in_iff_in_lits_of_l)+

lemma propa_confl_cands_enqueued_learn_empty:
  assumes
    prev: ‹propa_confl_cands_enqueued (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  shows ‹propa_confl_cands_enqueued (M, N, U, Some C, NE, UE, NS, US, add_mset {#} N0, U0, {#}, Q')›
    ‹propa_confl_cands_enqueued (M, N, U, Some C, NE, UE, NS, US, N0, add_mset {#} U0, {#}, Q')›
  using assms
  by (cases C; force simp: Decided_Propagated_in_iff_in_lits_of_l)+

lemma twl_exception_inv_skip_clause:
  ‹twl_exception_inv (M, add_mset C' (N), U, None, NE, UE, NS, US, N0, U0, {#}, Q) C ⟹
    twl_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q) C›
  ‹twl_exception_inv (M, N, add_mset C' U, None, NE, UE, NS, US, N0, U0, {#}, Q) C ⟹
    twl_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q) C›
  by (cases C) (auto simp: twl_exception_inv.simps)

lemma cdcl_twl_subresolution_propa_confl_cands_enqueued:
  assumes
    ‹cdcl_twl_subresolution S T›
    ‹Multiset.Ball (get_clauses S) (struct_wf_twl_cls)› and
    prev: ‹propa_confl_cands_enqueued S› and
    excep: ‹twl_st_exception_inv S› and
    nd: ‹no_dup (get_trail S)›
  shows ‹propa_confl_cands_enqueued T›
  using assms
    apply (induction rule: cdcl_twl_subresolution.induct)
  subgoal for C L D C' D' M E N U NE UE NS US N0 U0 Q
    by (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _]
      intro!: propa_confl_cands_enqueued_learn(1)[where C=E]
      dest: propa_confl_cands_enqueuedD)
  subgoal for C L D C' D' M K N U NE UE NS US Q
    apply (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _] twl_exception_inv_skip_clause[where C'=C' and N=‹add_mset C N›]
      intro: propa_confl_cands_enqueued_learn(1)[where C=C' and N=‹add_mset C N›]
      intro!: propa_confl_cands_enqueued_propagate
      dest: propa_confl_cands_enqueuedD
      dest!: multi_member_split[of _ N] multi_member_split[of _ U])
    done
  subgoal for C L D C' D' M E N U NE UE NS US Q
    by (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _]
      intro!: propa_confl_cands_enqueued_learn(2)[where C=E] struct_wf_twl_cls_remdupsI
      dest: propa_confl_cands_enqueuedD)
  subgoal for C L D C' D' M K N U NE UE NS US Q
    apply (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _] twl_exception_inv_skip_clause[where C'=C' and N=‹add_mset C N›]
      intro: propa_confl_cands_enqueued_learn(1)[where C=C' and N=‹add_mset C N›]
      intro!: propa_confl_cands_enqueued_propagate
      dest: propa_confl_cands_enqueuedD
      dest!: multi_member_split[of _ N] multi_member_split[of _ U])
    apply (simp_all add: twl_exception_inv.simps(1))
    done
  subgoal for C L D C' D' M E N U NE UE NS US Q
    by (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _]
      intro!: propa_confl_cands_enqueued_learn(2)[where C=E] struct_wf_twl_cls_remdupsI
      dest: propa_confl_cands_enqueuedD)
  subgoal for C L D C' D' M K N U NE UE NS US Q
    apply (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _] twl_exception_inv_skip_clause[where C'=C' and N=‹add_mset C N›]
      intro: propa_confl_cands_enqueued_learn(1)[where C=C' and N=‹add_mset C N›]
      intro!: propa_confl_cands_enqueued_propagate
      dest: propa_confl_cands_enqueuedD
      dest!: multi_member_split[of _ N] multi_member_split[of _ U])
    done
  subgoal for C L D C' D' M E N U NE UE NS US Q
    by (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _]
      intro!: propa_confl_cands_enqueued_learn(1)[where C=E] struct_wf_twl_cls_remdupsI
      dest: propa_confl_cands_enqueuedD)
  subgoal for C L D C' D' M K N U NE UE NS US Q
    apply (auto simp del: propa_confl_cands_enqueued.simps
      simp: add_mset_commute[of C _] twl_exception_inv_skip_clause[where C'=C' and N=‹add_mset C N›]
      intro: propa_confl_cands_enqueued_learn(1)[where C=C' and N=‹add_mset C N›]
      intro!: propa_confl_cands_enqueued_propagate
      dest: propa_confl_cands_enqueuedD
      dest!: multi_member_split[of _ N] multi_member_split[of _ U])
    apply (simp_all add: twl_exception_inv.simps(1))
    done
  done

lemma cdcl_twl_subresolution_conflict:
  ‹cdcl_twl_subresolution S T ⟹ get_conflict T = None›
  by (induction rule: cdcl_twl_subresolution.induct) auto

lemma clause_alt_def:
  ‹clause C =  watched C +  unwatched C›
  by (cases C) auto

lemma cdcl_twl_subresolution_clauses_to_update_inv:
  ‹cdcl_twl_subresolution S T ⟹ no_dup (get_trail S) ⟹
  clauses_to_update_inv S ⟹ clauses_to_update_inv T›
  apply (induction rule: cdcl_twl_subresolution.induct)
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      add_mset_eq_add_mset dest: no_has_blit_propagate
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      add_mset_eq_add_mset dest: no_has_blit_propagate
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      add_mset_eq_add_mset dest: no_has_blit_propagate
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      dest!: multi_member_split[of ‹_ :: _ literal›])
  subgoal
    by (auto simp: all_conj_distrib clauses_to_update_prop.simps filter_mset_empty_conv
      eq_commute[of _ ‹remdups_mset _›] clause_alt_def Decided_Propagated_in_iff_in_lits_of_l
      add_mset_eq_add_mset dest: no_has_blit_propagate
      dest!: multi_member_split[of ‹_ :: _ literal›])
  done

lemma cdcl_twl_subresolution_twl_struct_invs:
  assumes ‹cdcl_twl_subresolution S T›
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
proof -
  have ‹Multiset.Ball (get_clauses S) struct_wf_twl_cls› ‹no_dup (get_trail S)›
    using assms(2) unfolding  twl_struct_invs_def pcdcl_all_struct_invs_def
      cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset.cdclW_M_level_inv_def
    by (cases S;  auto simp: twl_st_simps)+
  moreover have ‹pcdcl_all_struct_invs (pstateW_of T)› ‹twl_st_inv T›
    using assms cdcl_twl_subresolution_pcdcl_all_struct_invs[of S T]
      cdcl_twl_subresolution_twl_st_inv[of S T]
    unfolding twl_struct_invs_def
    by auto
  then have ‹Multiset.Ball (get_clauses T) struct_wf_twl_cls› ‹no_dup (get_trail T)›
    unfolding  twl_struct_invs_def pcdcl_all_struct_invs_def
      cdclW_restart_mset.cdclW_all_struct_inv_def cdclW_restart_mset.cdclW_M_level_inv_def
    by (cases T;  auto simp: twl_st_simps; fail)+
  ultimately show ?thesis
    using cdcl_twl_subresolution_twl_st_inv[of S T]
      cdcl_twl_subresolution_valid_enqueued[of S T]
      cdcl_twl_subresolution_pcdcl_all_struct_invs[of S T]
      cdcl_twl_subresolution_smaller_propa[of S T]
      cdcl_twl_subresolution_twl_st_exception_inv[of S T]
      cdcl_twl_subresolution_dup_enqueued[of S T]
      cdcl_twl_subresolution_distinct_enqueued[of S T]
      cdcl_twl_subresolution_propa_confl_cands_enqueued[of S T]
      cdcl_twl_subresolution_propa_confl_cands_enqueued[of S T]
      propa_confl_cands_enqueued_propa_confl_enqueued[of S]
      propa_confl_cands_enqueued_propa_confl_enqueued[of T]
      cdcl_twl_subresolution_conflict[of S T]
      cdcl_twl_subresolution_twl_st_exception_inv[of S T]
      cdcl_twl_subresolution_clauses_to_update_inv[of S T]
      cdcl_twl_subresolution_past_invs[of S T] assms
    unfolding twl_struct_invs_def
    by clarsimp
qed

lemma Propagated_eq_DecidedD:
  ‹Propagated L C # M1 = M @ Decided K # M' ⟷
      M ≠ [] ∧ hd M = Propagated L C ∧ M1 = tl M @ Decided K # M'›
  by (cases M) auto

lemma cdcl_twl_subresolution_twl_stgy_invs:
  assumes ‹cdcl_twl_subresolution S T›
    ‹twl_struct_invs S›
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_subresolution.induct)
   (auto simp: twl_stgy_invs_def
    cdclW_restart_mset.cdclW_stgy_invariant_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    cdclW_restart_mset.no_smaller_confl_def
    Propagated_eq_DecidedD)

inductive cdcl_twl_unitres_true :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
  ‹cdcl_twl_unitres_true (M, N + {#C#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U, None, add_mset (clause C) NE, UE, NS, US, N0, U0, {#}, Q)›
  if ‹L ∈# clause C› ‹get_level M L = 0› ‹L ∈ lits_of_l M› |
  ‹cdcl_twl_unitres_true (M, N , U+ {#C#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U, None, NE, add_mset (clause C) UE, NS, US, N0, U0, {#}, Q)›
  if ‹L ∈# clause C› ‹get_level M L = 0› ‹L ∈ lits_of_l M›

lemma cdcl_twl_unitres_true_cdcl_unitres_true:
  ‹cdcl_twl_unitres_true S T ⟹ cdcl_unitres_true (pstateW_of S) (pstateW_of T)›
  by (force simp: cdcl_twl_unitres_true.simps cdcl_unitres_true.simps
    dest!: multi_member_split)

lemma cdcl_twl_unitres_true_invs:
  ‹cdcl_twl_unitres_true S T ⟹ twl_st_inv S ⟹ twl_st_inv T›
  ‹cdcl_twl_unitres_true S T ⟹ valid_enqueued S ⟹ valid_enqueued T›
  ‹cdcl_twl_unitres_true S T ⟹ twl_st_exception_inv S ⟹ twl_st_exception_inv T›
  ‹cdcl_twl_unitres_true S T ⟹ no_duplicate_queued S ⟹ no_duplicate_queued T›
  ‹cdcl_twl_unitres_true S T ⟹ distinct_queued S ⟹ distinct_queued T›
  ‹cdcl_twl_unitres_true S T ⟹ confl_cands_enqueued S ⟹ confl_cands_enqueued T›
  ‹cdcl_twl_unitres_true S T ⟹ propa_cands_enqueued S ⟹ propa_cands_enqueued T›
  ‹cdcl_twl_unitres_true S T ⟹ clauses_to_update_inv S ⟹ clauses_to_update_inv T›
  ‹cdcl_twl_unitres_true S T ⟹ past_invs S ⟹ past_invs T›
  ‹cdcl_twl_unitres_true S T ⟹ get_conflict T = None›
  ‹cdcl_twl_unitres_true S T ⟹ cdclW_restart_mset.no_smaller_propa (state_of (pstateW_of S)) ⟹
    cdclW_restart_mset.no_smaller_propa (state_of (pstateW_of T))›
  ‹cdcl_twl_unitres_true S T ⟹ pcdcl_all_struct_invs (pstateW_of S) ⟹ pcdcl_all_struct_invs (pstateW_of T)›
  apply (auto simp: cdcl_twl_unitres_true.simps twl_st_inv.simps
    twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
    past_invs.simps dest: cdcl_twl_unitres_true_cdcl_unitres_true)[11]
  apply (auto dest!: cdcl_twl_unitres_true_cdcl_unitres_true
    pcdcl.intros(8) pcdcl_all_struct_invs)
  done

lemma cdcl_twl_unitres_true_twl_struct_invs:
  ‹cdcl_twl_unitres_true S T ⟹ twl_struct_invs S ⟹ twl_struct_invs T›
  using cdcl_twl_unitres_true_invs[of S T]
  by (auto simp: twl_struct_invs_def)

lemma cdcl_twl_unitres_true_twl_stgy_invs:
  assumes ‹cdcl_twl_unitres_true S T›
    ‹twl_struct_invs S›
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_unitres_true.induct)
    (auto simp: twl_stgy_invs_def
    cdclW_restart_mset.cdclW_stgy_invariant_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    cdclW_restart_mset.no_smaller_confl_def
    Propagated_eq_DecidedD)


inductive cdcl_twl_unitres :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
‹cdcl_twl_unitres (M, N + {#D#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, add_mset E N, U, None, NE, UE, add_mset (clause D)  NS, US, N0, U0, {#}, Q)›
  if ‹count_decided M = 0› and
    ‹clause D = C+C'›
    ‹add_mset (C+C') (clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
    ‹¬tautology C› ‹distinct_mset C›
    ‹struct_wf_twl_cls E›
    ‹Multiset.Ball (clause E) (undefined_lit M)›
    ‹clause E = C› |
‹cdcl_twl_unitres (M, N + {#D#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K C # M, N, U, None, add_mset C NE, UE, add_mset (clause D) NS, US, N0, U0, {#}, add_mset (-K) Q)›
  if ‹count_decided M = 0› and
    ‹clause D = C+C'›
    ‹add_mset (C+C') (clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
    ‹¬tautology C› ‹distinct_mset C›
    ‹C = {#K#}›
    ‹undefined_lit M K› |
‹cdcl_twl_unitres (M, N, U + {#D#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, add_mset E U, None, NE, UE, NS, add_mset (clause D) US, N0, U0, {#}, Q)›
  if ‹count_decided M = 0› and
    ‹clause D = C+C'›
    ‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
    ‹¬tautology C› ‹distinct_mset C›
    ‹struct_wf_twl_cls E›
    ‹clause E = C›
    ‹Multiset.Ball (clause E) (undefined_lit M)›
    ‹atms_of C ⊆ atms_of_ms (clause ` set_mset N) ∪ atms_of_mm NE ∪ atms_of_mm NS ∪ atms_of_mm N0› |
‹cdcl_twl_unitres (M, N, U + {#D#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (Propagated K C # M, N, U, None, NE, add_mset C UE, NS, add_mset (clause D) US, N0, U0, {#}, add_mset (-K) Q)›
  if ‹count_decided M = 0› and
    ‹clause D = C+C'›
    ‹clauses N + NE + NS + N0 ⊨psm mset_set (CNot C')›
    ‹¬tautology C› ‹distinct_mset C›
    ‹C = {#K#}›
    ‹undefined_lit M K›
    ‹atms_of C ⊆ atms_of_ms (clause ` set_mset N) ∪ atms_of_mm NE ∪ atms_of_mm NS ∪ atms_of_mm N0› |
‹cdcl_twl_unitres (M, N, U + {#D#}, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U, Some {#}, NE, UE, NS, add_mset (clause D) US, N0, add_mset {#} U0, {#}, {#})›
  if ‹count_decided M = 0› and
    ‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot (clause D))› |
‹cdcl_twl_unitres (M, N + {#D#}, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U, Some {#}, NE, UE, add_mset (clause D) NS, US, add_mset {#} N0, U0, {#}, {#})›
  if ‹count_decided M = 0› and
    ‹(clauses (add_mset D N) + NE + NS + N0) ⊨psm mset_set (CNot (clause D))›

lemma cdcl_twl_unitres_cdcl_unitres:
  ‹cdcl_twl_unitres S T ⟹ cdcl_unitres (pstateW_of S) (pstateW_of T)›
  by (induction rule: cdcl_twl_unitres.cases)
   (fastforce simp: cdcl_unitres.simps)+

lemma cdcl_twl_unitres_invs:
  ‹cdcl_twl_unitres S T ⟹ twl_st_inv S ⟹ twl_st_inv T›
  by (induction rule: cdcl_twl_unitres.induct)
   (auto simp: twl_st_inv.simps twl_lazy_update_subresII
    twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0
    twl_is_an_exception_add_mset_to_queue)

lemma struct_wf_twl_cls_alt_def:
  ‹struct_wf_twl_cls C ⟷ distinct_mset (clause C) ∧ size (watched C) = 2›
  by (cases C) auto

lemma cdcl_twl_unitres_struct_invs:
  assumes ‹cdcl_twl_unitres S T› and ‹twl_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init ((stateW_of S))›
  shows ‹twl_struct_invs T›
  unfolding twl_struct_invs_def
proof (intro conjI)
  have st_inv: ‹twl_st_inv S› and
    valid: ‹valid_enqueued S› and
    except: ‹twl_st_exception_inv S› and
    dup: ‹no_duplicate_queued S› and
    dist: ‹distinct_queued S› and
    clss: ‹clauses_to_update_inv S› and
    past: ‹past_invs S› and
    confl_cands: ‹confl_cands_enqueued S› and
    propa_cands: ‹propa_cands_enqueued S› and
    dupq: ‹no_duplicate_queued S› and
    distq: ‹distinct_queued S› and
    invs: ‹pcdcl_all_struct_invs (pstateW_of S)› and
    propa: ‹cdclW_restart_mset.no_smaller_propa (stateW_of S)›
    using assms(2) unfolding twl_struct_invs_def by fast+

  have n_d: ‹no_dup (get_trail S)›
    using invs unfolding pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  show st_inv_T: ‹twl_st_inv T› and ‹valid_enqueued T›
    using valid count_decided_ge_get_level[of ‹get_trail S›] assms(1) st_inv n_d except
    by (auto simp: twl_st_inv.simps twl_lazy_update_subresII
    twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0 get_level_cons_if
    twl_is_an_exception_add_mset_to_queue cdcl_twl_unitres.simps
    twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
    past_invs.simps Decided_Propagated_in_iff_in_lits_of_l clause_alt_def
      uminus_lit_swap
    dest!: multi_member_split
      dest: mset_le_add_mset simp: undefined_notin; fail)+

  show ‹twl_st_exception_inv T›
    using count_decided_ge_get_level[of ‹get_trail S›] assms(1) except n_d
    by (auto simp: twl_st_inv.simps twl_lazy_update_subresII
    twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0 get_level_cons_if
    twl_is_an_exception_add_mset_to_queue cdcl_twl_unitres.simps
    twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
    past_invs.simps Decided_Propagated_in_iff_in_lits_of_l clause_alt_def
      uminus_lit_swap
    dest!: multi_member_split
      dest: mset_le_add_mset simp: undefined_notin)
  show ‹clauses_to_update_inv T›
    using clss assms(1) n_d
    by (auto simp: cdcl_twl_unitres.simps filter_mset_empty_conv all_conj_distrib
      Decided_Propagated_in_iff_in_lits_of_l clauses_to_update_prop.simps
      split: if_splits dest: has_blit_Cons)
     (auto simp:  clause_alt_def Decided_Propagated_in_iff_in_lits_of_l split: if_splits; fail)+
  show invs_T: ‹pcdcl_all_struct_invs (pstateW_of T)›
    using cdcl_twl_unitres_cdcl_unitres[OF assms(1)] invs assms(3)
    by (auto dest!: cdcl_unitres_learn_subsume rtranclp_pcdcl_all_struct_invs)
  show ‹past_invs T›
    using assms(1)
    by (auto simp: cdcl_twl_unitres.simps past_invs.simps Propagated_eq_DecidedD)
  have struct: ‹∀C ∈# get_clauses S. struct_wf_twl_cls C›
    by (use st_inv n_d propa_cands confl_cands in ‹cases S; auto simp: twl_st_inv.simps; fail›)+
  then have ‹propa_confl_cands_enqueued S›
    by (subst propa_confl_cands_enqueued_propa_confl_enqueued[of S])
     (use st_inv n_d propa_cands confl_cands in ‹auto simp: twl_st_inv.simps; fail›)+
  with assms(1) have ‹propa_confl_cands_enqueued T›
    using n_d struct except
    by (induction rule: cdcl_twl_unitres.cases)
     (auto 5 4 intro!: propa_confl_cands_enqueued_propagate
      simp: propa_confl_cands_enqueued_learn  propa_confl_cands_enqueued_learn_empty
      dest: propa_confl_cands_enqueuedD twl_exception_inv_skip_clause
      dest: multi_member_split[of ‹_ :: _ twl_clause›]
      simp del: propa_confl_cands_enqueued.simps)
  moreover have struct: ‹∀C ∈# get_clauses T. struct_wf_twl_cls C›
    by (use st_inv_T  in ‹cases T; auto simp: twl_st_inv.simps; fail›)+
  moreover have ‹no_dup (get_trail T)›
    using invs_T unfolding pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  ultimately show ‹confl_cands_enqueued T› and ‹propa_cands_enqueued T›
    by (subst (asm) propa_confl_cands_enqueued_propa_confl_enqueued[of T]; auto; fail)+
  show ‹no_duplicate_queued T› and ‹distinct_queued T›
    using dupq distq n_d assms(1)
    by (force simp: cdcl_twl_unitres.simps past_invs.simps Propagated_eq_DecidedD undefined_notin
      dest!: multi_member_split split_list dest: mset_le_add_mset)+

  show ‹get_conflict T ≠ None ⟶ clauses_to_update T = {#} ∧ literals_to_update T = {#}›
    using assms(1)
    by (auto simp: cdcl_twl_unitres.simps past_invs.simps Propagated_eq_DecidedD)

  show ‹cdclW_restart_mset.no_smaller_propa (stateW_of T)›
    using assms(1)
    by (auto simp: cdcl_twl_unitres.simps past_invs.simps Propagated_eq_DecidedD
      cdclW_restart_mset.no_smaller_propa_def)
qed

lemma cdcl_twl_unitres_twl_stgy_invs:
  assumes ‹cdcl_twl_unitres S T›
    ‹twl_struct_invs S›
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_unitres.induct)
   (auto simp: twl_stgy_invs_def
    cdclW_restart_mset.cdclW_stgy_invariant_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    cdclW_restart_mset.no_smaller_confl_def
    Propagated_eq_DecidedD)


lemma twl_exception_inv_add_subsumed:
  ‹twl_exception_inv (M1, N, U, D, NE, UE, add_mset (C') NS, US, N0, U0, WS, Q) =
  twl_exception_inv (M1, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹twl_exception_inv (M1, N, U, D, NE, UE, NS, add_mset (C') US, N0, U0, WS, Q) =
  twl_exception_inv (M1, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (intro ext; cases D; auto simp: twl_exception_inv.simps)+

lemma propa_confl_cands_enqueued_add_subsumed:
  ‹propa_confl_cands_enqueued (M, N, U, D, NE, UE, add_mset (C') NS, US, N0, U0, WS, Q) ⟷
  propa_confl_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹propa_confl_cands_enqueued (M, N, U, D, NE, UE, NS, add_mset (C') US, N0, U0, WS, Q) ⟷
  propa_confl_cands_enqueued (M, N, U, D, NE, UE,  NS, US, N0, U0, WS, Q)›
  by (cases D; auto)+

lemma propa_confl_cands_enqueued_remove_learnD:
  ‹propa_confl_cands_enqueued (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟹
  propa_confl_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto)

lemma propa_confl_cands_enqueued_remove_learnD2:
  ‹propa_confl_cands_enqueued (M, add_mset C (add_mset C' N), U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟹
  propa_confl_cands_enqueued (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹propa_confl_cands_enqueued (M, N, add_mset C (add_mset C' U), D, NE, UE, NS, US, N0, U0, WS, Q) ⟹
  propa_confl_cands_enqueued (M, N, add_mset C U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹propa_confl_cands_enqueued (M,  add_mset C N, (add_mset C' U), D, NE, UE, NS, US, N0, U0, WS, Q) ⟹
  propa_confl_cands_enqueued (M,  add_mset C N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto)+

lemma cdcl_subsumed_RI_all_struct_invs:
  ‹cdcl_subsumed_RI S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  by (elim cdcl_subsumed_RID)
   (auto simp add: cdcl_learn_clause_all_struct_inv cdcl_learn_clause_entailed_clss_inv
      cdcl_learn_clause_psubsumed_invs cdcl_subsumed_all_struct_inv cdcl_subsumed_entailed_clss_inv
      cdcl_subsumed_psubsumed_invs pcdcl_all_struct_invs_def
    intro: pcdcl.intros(2) pcdcl.intros(4) pcdcl_clauses0_inv)
 
lemma cdcl_unitres_pcdcl_all_struct_invs:
  ‹cdcl_unitres S T ⟹ cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  pcdcl_all_struct_invs (S) ⟹
  pcdcl_all_struct_invs (T)›
  using cdcl_unitres_learn_subsume rtranclp_pcdcl_all_struct_invs by blast

lemma cdcl_twl_unitres_pcdcl_all_struct_invs:
  ‹cdcl_twl_unitres S T ⟹ cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  pcdcl_all_struct_invs (pstateW_of S) ⟹
  pcdcl_all_struct_invs (pstateW_of T)›
  by (drule cdcl_twl_unitres_cdcl_unitres)
    (simp add: cdcl_unitres_pcdcl_all_struct_invs)

lemma cdcl_twl_subsumed_struct_invs:
  assumes ‹cdcl_twl_subsumed S T› and ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  unfolding twl_struct_invs_def
proof (intro conjI)
  have st_inv: ‹twl_st_inv S› and
    valid: ‹valid_enqueued S› and
    except: ‹twl_st_exception_inv S› and
    dup: ‹no_duplicate_queued S› and
    dist: ‹distinct_queued S› and
    clss: ‹clauses_to_update_inv S› and
    past: ‹past_invs S› and
    confl_cands: ‹confl_cands_enqueued S› and
    propa_cands: ‹propa_cands_enqueued S› and
    dupq: ‹no_duplicate_queued S› and
    distq: ‹distinct_queued S› and
    invs: ‹pcdcl_all_struct_invs (pstateW_of S)› and
    propa:  ‹cdclW_restart_mset.no_smaller_propa (stateW_of S)› and
    confl: ‹get_conflict S ≠ None ⟶ clauses_to_update S = {#} ∧ literals_to_update S = {#}› and
    smaller: ‹cdclW_restart_mset.no_smaller_propa (stateW_of S)›
    using assms(2) unfolding twl_struct_invs_def by fast+

  have n_d: ‹no_dup (get_trail S)›
    using invs unfolding pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  show st_inv_T: ‹twl_st_inv T› and ‹valid_enqueued T›
    using valid count_decided_ge_get_level[of ‹get_trail S›] assms(1) st_inv n_d except
    by (auto simp: twl_st_inv.simps twl_lazy_update_subresII
      twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0 get_level_cons_if
      twl_is_an_exception_add_mset_to_queue cdcl_twl_subsumed.simps
      twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
      past_invs.simps Decided_Propagated_in_iff_in_lits_of_l clause_alt_def
        uminus_lit_swap
      dest!: multi_member_split
        dest: mset_le_add_mset simp: undefined_notin; fail)+

  show ‹twl_st_exception_inv T›
    using count_decided_ge_get_level[of ‹get_trail S›] assms(1) except n_d
      by (cases ‹get_conflict S›)
      (auto simp: twl_st_inv.simps twl_lazy_update_subresII
        twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0 get_level_cons_if
        twl_is_an_exception_add_mset_to_queue cdcl_twl_subsumed.simps
        twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
        past_invs.simps Decided_Propagated_in_iff_in_lits_of_l clause_alt_def
          uminus_lit_swap
        dest!: multi_member_split
          dest: mset_le_add_mset simp: undefined_notin)

  show ‹clauses_to_update_inv T›
    using clss assms(1) n_d
    by (cases ‹get_conflict S›)
      (auto simp: cdcl_twl_subsumed.simps filter_mset_empty_conv all_conj_distrib
      Decided_Propagated_in_iff_in_lits_of_l clauses_to_update_prop.simps
      split: if_splits dest: has_blit_Cons)
  show invs_T: ‹pcdcl_all_struct_invs (pstateW_of T)›
    using cdcl_twl_subsumed_cdcl_subsumed[OF assms(1)] assms(2) invs
    by (auto dest!: cdcl_unitres_learn_subsume rtranclp_pcdcl_all_struct_invs cdcl_subsumed_RI_all_struct_invs
      simp: cdcl_subsumed_all_struct_inv cdcl_subsumed_entailed_clss_inv cdcl_subsumed_psubsumed_invs
        pcdcl_all_struct_invs_def
      intro: pcdcl.intros(4) pcdcl_clauses0_inv)

  show ‹past_invs T›
    using assms(1) past
    by (auto simp: cdcl_twl_subsumed.simps past_invs.simps Propagated_eq_DecidedD all_conj_distrib
       twl_lazy_update_subresII
        twl_lazy_update_undefined watched_literals_false_of_max_level_lvl0 get_level_cons_if
        twl_is_an_exception_add_mset_to_queue
        twl_exception_inv.simps filter_mset_empty_conv clauses_to_update_prop.simps
        Decided_Propagated_in_iff_in_lits_of_l clause_alt_def
        dest!: multi_member_split
          dest: mset_le_add_mset simp: undefined_notin)

  have propa_confl_cands_enqueued_IR: ‹propa_confl_cands_enqueued  (M, add_mset C' N, add_mset C U, D, NE, UE, NS, US, N0, U0, {#}, Q) ⟹
    propa_confl_cands_enqueued  (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0, {#}, Q)› for M C' N C U D NE UE US Q NS N0 U0
    by (cases D)  (auto simp: )
  have struct: ‹∀C ∈# get_clauses S. struct_wf_twl_cls C›
    by (use st_inv n_d propa_cands confl_cands in ‹cases S; auto simp: twl_st_inv.simps; fail›)+
  then have ‹propa_confl_cands_enqueued S›
    by (subst propa_confl_cands_enqueued_propa_confl_enqueued[of S])
     (use st_inv n_d propa_cands confl_cands in ‹auto simp: twl_st_inv.simps; fail›)+
  with assms(1) have ‹propa_confl_cands_enqueued T›
    using n_d struct except
    by (induction rule: cdcl_twl_subsumed.cases)
     (auto 5 4 intro!: propa_confl_cands_enqueued_propagate
      simp: propa_confl_cands_enqueued_learn twl_exception_inv_add_subsumed
        propa_confl_cands_enqueued_add_subsumed add_mset_commute
      dest: propa_confl_cands_enqueuedD twl_exception_inv_skip_clause
        propa_confl_cands_enqueued_remove_learnD2 propa_confl_cands_enqueued_IR
      dest: multi_member_split[of ‹_ :: _ twl_clause›]
      simp del: propa_confl_cands_enqueued.simps)
  moreover have struct: ‹∀C ∈# get_clauses T. struct_wf_twl_cls C›
    by (use st_inv_T  in ‹cases T; auto simp: twl_st_inv.simps; fail›)+
  moreover have ‹no_dup (get_trail T)›
    using invs_T unfolding pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  ultimately show ‹confl_cands_enqueued T› and ‹propa_cands_enqueued T›
    by (subst (asm) propa_confl_cands_enqueued_propa_confl_enqueued[of T]; auto; fail)+
  show ‹no_duplicate_queued T› and ‹distinct_queued T›
    using dupq distq n_d assms(1)
    by (force simp: cdcl_twl_subsumed.simps past_invs.simps Propagated_eq_DecidedD undefined_notin
      dest!: multi_member_split split_list dest: mset_le_add_mset)+

  show ‹get_conflict T ≠ None ⟶ clauses_to_update T = {#} ∧ literals_to_update T = {#}›
    using assms(1) confl
    by (auto simp: cdcl_twl_subsumed.simps past_invs.simps Propagated_eq_DecidedD)

  show ‹cdclW_restart_mset.no_smaller_propa (stateW_of T)›
    using assms(1) smaller
    apply (auto simp: cdcl_twl_subsumed.simps past_invs.simps Propagated_eq_DecidedD
      cdclW_restart_mset.no_smaller_propa_def)
    apply blast+
    done
qed

lemma cdcl_subresolutions_entailed_by_init:
  ‹cdcl_subresolution S T ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  apply (induction rule: cdcl_subresolution.induct)
  subgoal by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
    insert_commute)
  subgoal for M C C' N U L D NE UE NS US N0 U0
    using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of ‹set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0› L C' C]
      true_clss_cls_cong_set_mset[of ‹N + NE + NS + N0› ‹C+C'› C']
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      insert_commute subset_mset.le_iff_add ac_simps)
  subgoal for M C C' N L U D NE UE NS US N0 U0
    using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of ‹set_mset (N + {#add_mset L C#}) ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0› L C' C]
      true_clss_cls_cong_set_mset[of ‹(N + {#add_mset L C#}) + NE + NS + N0› ‹C+C'› C']
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      insert_commute subset_mset.le_iff_add ac_simps)
  subgoal for M C C' N L U D NE UE NS US N0 U0
    using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of
        ‹set_mset (N + {#add_mset L C#}) ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0› L C' C]
      true_clss_cls_cong_set_mset[of ‹(N + {#add_mset L C#}) + NE + NS + N0› ‹C+C'› C]
    by (force simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      insert_commute ac_simps)
  done

inductive cdcl_twl_promote_false :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
‹cdcl_twl_promote_false (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0, WS, Q)
  (M, N, U, Some {#}, NE, UE, NS, US, add_mset {#} N0, U0, WS, Q)›
  if ‹clause C = {#}› ‹count_decided M = 0›|
‹cdcl_twl_promote_false (M, N, add_mset C U, D, NE, UE, NS, US, N0, U0, WS, Q)
    (M, N, U, Some {#}, NE, UE, NS, US, N0, add_mset {#} U0, WS, Q)›
  if ‹clause C = {#}› ‹count_decided M = 0›

lemma cdcl_twl_promote_false_cdcl_promote_false:
  ‹cdcl_twl_promote_false S T ⟹ cdcl_promote_false (pstateW_of S) (pstateW_of T)›
  by (auto simp: cdcl_twl_promote_false.simps cdcl_promote_false.simps)

lemma cdcl_twl_promote_false_twl_stgy_invs:
  assumes ‹cdcl_twl_promote_false S T›
    ‹twl_struct_invs S›
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_promote_false.induct)
   (auto simp: twl_stgy_invs_def cdclW_restart_mset.cdclW_stgy_invariant_def
    cdclW_restart_mset.no_smaller_confl_def clauses_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def)

lemma cdcl_subsumed_RI_stgy_invs:
  ‹cdcl_subsumed_RI (pstateW_of S) (pstateW_of T) ⟹ twl_stgy_invs S ⟹
  twl_stgy_invs T›
  apply (cases rule: cdcl_subsumed_RI.cases, assumption)
  apply (cases S; cases T; auto simp: twl_stgy_invs_def
    cdclW_restart_mset.cdclW_stgy_invariant_def cdclW_restart_mset.no_smaller_confl_def
    clauses_def cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    all_conj_distrib)
  apply (metis member_add_mset set_image_mset)
  apply (metis member_add_mset set_image_mset)
  apply (metis member_add_mset set_image_mset)
  apply (metis image_mset_add_mset member_add_mset multi_member_split set_image_mset)
  done

lemma cdcl_twl_subsumed_stgy_invs:
  ‹cdcl_twl_subsumed S T ⟹
          twl_struct_invs S ⟹
          cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
          cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T) ⟹
          twl_stgy_invs S ⟹ twl_stgy_invs T›
  apply (drule cdcl_twl_subsumed_cdcl_subsumed)
  apply (elim disjE)
  apply (simp add: state_of_cdcl_subsumed twl_stgy_invs_def)
  apply (simp add: cdcl_subsumed_RI_stgy_invs)
  done

lemma cdcl_twl_subsumed_twl_stgy_invs:
  assumes ‹cdcl_twl_subsumed S T›
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (metis (no_types, lifting) assms cdcl_subsumed_RI_stgy_invs
    cdcl_twl_subsumed_cdcl_subsumed stateW_of_def state_of_cdcl_subsumed twl_stgy_invs_def)


inductive cdcl_twl_pure_remove :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
‹cdcl_twl_pure_remove (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
  (Propagated L {#L#} # M, N, U, None, add_mset {#L#} NE, UE, NS, US, N0, U0, {#}, add_mset (-L) Q)›
  if ‹count_decided M = 0›
    ‹-L ∉  ⋃ ((set_mset o clause) ` set_mset N)›
    ‹atm_of L ∈ atms_of_mm (clauses N + NE + NS + N0)›
    ‹undefined_lit M L›

lemma cdcl_twl_pure_remove_cdcl_pure_remove:
  ‹cdcl_twl_pure_remove S T ⟹ cdcl_pure_literal_remove (pstateW_of S) (pstateW_of T)›
  by (auto simp: cdcl_twl_pure_remove.simps cdcl_pure_literal_remove.simps
    dest!: multi_member_split)


lemma cdcl_twl_pure_remove_twl_struct_invs:
  assumes pure: ‹cdcl_twl_pure_remove S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
proof -
  have st_inv: ‹twl_st_inv S› and
    valid: ‹valid_enqueued S› and
    smaller: ‹cdclW_restart_mset.no_smaller_propa (stateW_of S)› and
    exception: ‹twl_st_exception_inv S› and
    ‹pcdcl_all_struct_invs (pstateW_of S)› and
    dup: ‹no_duplicate_queued S›
      ‹distinct_queued S›
      ‹confl_cands_enqueued S›
      ‹propa_cands_enqueued S› and
    invs: ‹pcdcl_all_struct_invs (pstateW_of S)› and
    upd_inv: ‹clauses_to_update_inv S›
    using assms unfolding twl_struct_invs_def by fast+
  have n_d: ‹no_dup (get_trail S)›
    using invs unfolding pcdcl_all_struct_invs_def
      cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  have wf: ‹∀C ∈# get_clauses S. struct_wf_twl_cls C›
    using st_inv by (cases S) (auto simp: twl_st_inv.simps)
  have propa_confl: ‹propa_confl_cands_enqueued S›
    by (subst propa_confl_cands_enqueued_propa_confl_enqueued)
     (use wf dup n_d in auto)
  have ‹twl_st_inv T›
    using pure st_inv
    by (auto simp: cdcl_twl_pure_remove.simps twl_st_inv.simps
      twl_is_an_exception_add_mset_to_queue watched_literals_false_of_max_level_prop_lvl0
      intro!: twl_lazy_update_subresII
      dest: multi_member_split)
  moreover have ‹valid_enqueued T›
    using valid pure
    by (auto simp: cdcl_twl_pure_remove.simps twl_st_inv.simps
      get_level_cons_if)
  moreover have ‹cdclW_restart_mset.no_smaller_propa (stateW_of T)›
    using pure smaller
    by (auto simp: cdclW_restart_mset.no_smaller_propa_def
      cdcl_twl_pure_remove.simps Propagated_eq_DecidedD)
  moreover have ‹twl_st_exception_inv T›
    using pure n_d exception apply -
    by (cases rule: cdcl_twl_pure_remove.cases, assumption)
     (auto simp: cdcl_twl_pure_remove.simps Propagated_eq_DecidedD
        twl_exception_inv.simps uminus_lit_swap
      intro!: propa_confl_cands_enqueued_propagate
      dest!: no_has_blit_propagate'
      dest!: multi_member_split[of ‹_ :: _ clause›])
   moreover have ‹no_duplicate_queued T›
     ‹distinct_queued T›
     using pure dup apply (auto simp: no_duplicate_queued.simps
       cdcl_twl_pure_remove.simps
       dest!: multi_member_split[of _ ‹_ :: _ clause›]
       dest: mset_subset_eq_insertD msed_map_invR)[]
     using pure dup apply (auto simp: no_duplicate_queued.simps
       cdcl_twl_pure_remove.simps undefined_notin
       dest!: multi_member_split[of _ ‹_ :: _ clause›]
       dest: mset_subset_eq_insertD dest: msed_map_invR)[]
     apply (solves ‹frule mset_subset_eq_insertD; clarsimp simp: undefined_notin›)+
     done
   moreover {
     have ‹propa_confl_cands_enqueued T›
       using pure dup propa_confl wf exception n_d
       by (auto simp: cdcl_twl_pure_remove.simps
         twl_exception_inv.simps
         simp del: propa_confl_cands_enqueued.simps 
         intro!: propa_confl_cands_enqueued_propagate)[]
     then have
      ‹confl_cands_enqueued T ∧ propa_cands_enqueued T›
    by (subst (asm) propa_confl_cands_enqueued_propa_confl_enqueued)
     (use pure wf dup n_d in ‹auto simp: cdcl_twl_pure_remove.simps›)[3]
  }
  moreover have ‹get_conflict T ≠ None ⟶ clauses_to_update T = {#} ∧ literals_to_update T = {#}›
    using pure by (auto simp: cdcl_twl_pure_remove.simps)
  moreover have ‹clauses_to_update_inv T›
    using n_d pure upd_inv
    by (auto simp: cdcl_twl_pure_remove.simps filter_mset_empty_conv all_conj_distrib
      Decided_Propagated_in_iff_in_lits_of_l clauses_to_update_prop.simps
      split: if_splits dest: has_blit_Cons)
     (auto simp:  clause_alt_def Decided_Propagated_in_iff_in_lits_of_l split: if_splits; fail)+
  moreover have ‹past_invs T›
    using pure by (auto simp: cdcl_twl_pure_remove.simps past_invs.simps
      Propagated_eq_DecidedD)
  moreover have ‹pcdcl_all_struct_invs (pstateW_of T)›
    using cdcl_twl_pure_remove_cdcl_pure_remove invs pcdcl.intros(10) pcdcl_all_struct_invs pure
    by blast
  ultimately show ?thesis
    unfolding twl_struct_invs_def
    by simp
qed

lemma cdcl_twl_pure_remove_twl_stgy_invs:
  assumes pure: ‹cdcl_twl_pure_remove S T› and
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms by (auto simp: cdcl_twl_pure_remove.simps
    twl_stgy_invs_def cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    cdclW_restart_mset.cdclW_stgy_invariant_def Propagated_eq_DecidedD
    cdclW_restart_mset.no_smaller_confl_def)

end