Theory Watched_Literals_List_Restart

theory Watched_Literals_List_Restart
  imports Watched_Literals_List Watched_Literals_Algorithm_Reduce
begin

text ‹
  Unlike most other refinements steps we have done, we don't try to refine our
  specification to our code directly: We first introduce an intermediate transition system which
  is closer to what we want to implement. Then we refine it to code.
›

(*TODO Move*)
lemma
  assumes ‹no_dup M›
  shows
    no_dup_same_annotD:
    ‹Propagated L C ∈ set M ⟹ Propagated L C' ∈ set M ⟹ C = C'› and
    no_dup_no_propa_and_dec:
    ‹Propagated L C ∈ set M ⟹ Decided L ∈ set M ⟹ False›
  using assms
  by (auto dest!: split_list elim: list_match_lel_lel)

text ‹
  This invariant abstract over the restart operation on the trail. There can be a backtracking on
  the trail and there can be a renumbering of the indexes.
›
inductive valid_trail_reduction for M M' :: ‹('v ,'c) ann_lits› where
backtrack_red:
  ‹valid_trail_reduction M M'›
  if
    ‹(Decided K # M'', M2) ∈ set (get_all_ann_decomposition M)› and
    ‹map lit_of M'' = map lit_of M'› and
    ‹map is_decided M'' = map is_decided M'› |
keep_red:
  ‹valid_trail_reduction M M'›
  if
    ‹map lit_of M = map lit_of M'› and
    ‹map is_decided M = map is_decided M'›

lemma valid_trail_reduction_simps: ‹valid_trail_reduction M M' ⟷
  ((∃K M'' M2. (Decided K # M'', M2) ∈ set (get_all_ann_decomposition M) ∧
     map lit_of M'' = map lit_of M' ∧ map is_decided M'' = map is_decided M' ∧
    length M' = length M'') ∨
   map lit_of M = map lit_of M' ∧ map is_decided M = map is_decided M' ∧ length M = length M')›
 apply (auto simp: valid_trail_reduction.simps dest: arg_cong[of ‹map lit_of _› _ length])
 apply (force dest: arg_cong[of ‹map lit_of _› _ length])+
 done

lemma valid_trail_reduction_refl[simp]:
  ‹valid_trail_reduction M M›
  by (rule valid_trail_reduction.keep_red)
    auto

lemma trail_changes_same_decomp:
  assumes
    M'_lit: ‹map lit_of M' = map lit_of ysa @ L # map lit_of zsa› and
    M'_dec: ‹map is_decided M' = map is_decided ysa @ False # map is_decided zsa›
  obtains C' M2 M1 where ‹M' = M2 @ Propagated L C' # M1› and
    ‹map lit_of M2 = map lit_of ysa›and
    ‹map is_decided M2 = map is_decided ysa› and
    ‹map lit_of M1 = map lit_of zsa› and
    ‹map is_decided M1 = map is_decided zsa›
proof -
  define M1 M2 K where ‹M1 ≡ drop (Suc (length ysa)) M'› and ‹M2 ≡ take (length ysa) M'› and
    ‹K ≡ hd (drop (length ysa) M')›
  have
    M': ‹M' = M2 @ K # M1›
    using arg_cong[OF M'_lit, of length] unfolding M1_def M2_def K_def
    by (simp add: Cons_nth_drop_Suc hd_drop_conv_nth)
  have [simp]:
    ‹length M2 = length ysa›
    ‹length M1 = length zsa›
    using arg_cong[OF M'_lit, of length] unfolding M1_def M2_def K_def by auto

  obtain C' where
    [simp]: ‹K = Propagated L C'›
    using M'_lit M'_dec unfolding M'
    by (cases K) auto

  show ?thesis
    using that[of M2 C' M1] M'_lit M'_dec unfolding M'
    by auto
qed

lemma
  assumes
    ‹map lit_of M = map lit_of M'› and
    ‹map is_decided M = map is_decided M'›
  shows
    trail_renumber_count_dec:
      ‹count_decided M = count_decided M'› and
    trail_renumber_get_level:
      ‹get_level M L = get_level M' L›
proof -
  have [dest]: ‹count_decided M = count_decided M'›
    if ‹map is_decided M = map is_decided M'› for M M'
    using that
    apply (induction M arbitrary: M' rule: ann_lit_list_induct)
    subgoal by auto
    subgoal for L M M'
      by (cases M')
        (auto simp: get_level_cons_if)
    subgoal for L C M M'
      by (cases M')
        (auto simp: get_level_cons_if)
    done
  then show ‹count_decided M = count_decided M'› using assms by blast
  show  ‹get_level M L = get_level M' L›
    using assms
    apply (induction M arbitrary: M' rule: ann_lit_list_induct)
    subgoal by auto
    subgoal for L M M'
      by (cases M'; cases ‹hd M'›)
        (auto simp: get_level_cons_if)
    subgoal for L C M M'
      by (cases M')
        (auto simp: get_level_cons_if)
    done
qed

lemma valid_trail_reduction_Propagated_inD:
  ‹valid_trail_reduction M M' ⟹ Propagated L C ∈ set M' ⟹ ∃C'. Propagated L C' ∈ set M›
  by (induction rule: valid_trail_reduction.induct)
    (force dest!: get_all_ann_decomposition_exists_prepend
      dest!: split_list[of ‹Propagated L C›] elim!: trail_changes_same_decomp)+

lemma valid_trail_reduction_Propagated_inD2:
  ‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ Propagated L C ∈ set M ⟹
     ∃C'. Propagated L C' ∈ set M'›
  apply (induction rule: valid_trail_reduction.induct)
  apply (auto dest!: get_all_ann_decomposition_exists_prepend
      dest!: split_list[of ‹Propagated L C›] elim!: trail_changes_same_decomp)+
    apply (metis add_Suc_right le_add2 length_Cons length_append length_map not_less_eq_eq)
  by (metis (no_types, lifting) in_set_conv_decomp trail_changes_same_decomp)

lemma get_all_ann_decomposition_change_annotation_exists:
  assumes
    ‹(Decided K # M', M2') ∈ set (get_all_ann_decomposition M2)› and
    ‹map lit_of M1 = map lit_of M2› and
    ‹map is_decided M1 = map is_decided M2›
  shows ‹∃M'' M2'. (Decided K # M'', M2') ∈ set (get_all_ann_decomposition M1) ∧
    map lit_of M'' = map lit_of M' ∧  map is_decided M'' = map is_decided M'›
  using assms
proof (induction M1 arbitrary: M2 M2' rule: ann_lit_list_induct)
  case Nil
  then show ?case by auto
next
  case (Decided L xs M2)
  then show ?case
    by (cases M2; cases ‹hd M2›) fastforce+
next
  case (Propagated L m xs M2) note IH = this(1) and prems = this(2-)
  show ?case
    using IH[of _ ‹tl M2›] prems get_all_ann_decomposition_decomp[of xs]
      get_all_ann_decomposition_decomp[of M2 ‹Decided K # M'›]
    by (cases M2; cases ‹hd M2›; cases ‹(get_all_ann_decomposition (tl M2))›;
        cases ‹hd (get_all_ann_decomposition xs)›; cases ‹get_all_ann_decomposition xs›)
      fastforce+
qed

lemma valid_trail_reduction_trans:
  assumes
    M1_M2: ‹valid_trail_reduction M1 M2› and
    M2_M3: ‹valid_trail_reduction M2 M3›
  shows ‹valid_trail_reduction M1 M3›
proof -
  consider
    (same) ‹map lit_of M2 = map lit_of M3› and
       ‹map is_decided M2 = map is_decided M3› ‹length M2 = length M3› |
    (decomp_M1) K M'' M2' where
      ‹(Decided K # M'', M2') ∈ set (get_all_ann_decomposition M2)› and
      ‹map lit_of M'' = map lit_of M3› and
      ‹map is_decided M'' = map is_decided M3› and
      ‹length M3 = length M''›
    using M2_M3 unfolding valid_trail_reduction_simps
    by auto
  note decomp_M2 = this
  consider
    (same) ‹map lit_of M1 = map lit_of M2› and
       ‹map is_decided M1 = map is_decided M2› ‹length M1 = length M2› |
    (decomp_M1) K M'' M2' where
      ‹(Decided K # M'', M2') ∈ set (get_all_ann_decomposition M1)› and
      ‹map lit_of M'' = map lit_of M2› and
      ‹map is_decided M'' = map is_decided M2› and
      ‹length M2 = length M''›
    using M1_M2 unfolding valid_trail_reduction_simps
    by auto
  then show ?thesis
  proof cases
    case same
    from decomp_M2
    show ?thesis
    proof cases
      case same': same
      then show ?thesis
        using same by (auto simp: valid_trail_reduction_simps)
    next
      case decomp_M1 note decomp = this(1) and eq = this(2,3) and [simp] = this(4)
      obtain M4 M5 where
         decomp45: ‹(Decided K # M4, M5) ∈ set (get_all_ann_decomposition M1)› and
         M4_lit: ‹map lit_of M4 = map lit_of M''› and
         M4_dec: ‹map is_decided M4 = map is_decided M''›
        using get_all_ann_decomposition_change_annotation_exists[OF decomp, of M1] eq same
        by (auto simp: valid_trail_reduction_simps)
      show ?thesis
        by (rule valid_trail_reduction.backtrack_red[OF decomp45])
          (use M4_lit M4_dec eq same in auto)
    qed
  next
    case decomp_M1 note decomp = this(1) and eq = this(2,3) and [simp] = this(4)
    from decomp_M2
    show ?thesis
    proof cases
      case same
      obtain M4 M5 where
         decomp45: ‹(Decided K # M4, M5) ∈ set (get_all_ann_decomposition M1)› and
         M4_lit: ‹map lit_of M4 = map lit_of M''› and
         M4_dec: ‹map is_decided M4 = map is_decided M''›
        using get_all_ann_decomposition_change_annotation_exists[OF decomp, of M1] eq same
        by (auto simp: valid_trail_reduction_simps)
      show ?thesis
        by (rule valid_trail_reduction.backtrack_red[OF decomp45])
          (use M4_lit M4_dec eq same in auto)
    next
      case (decomp_M1 K' M''' M2''') note decomp' = this(1) and eq' = this(2,3) and [simp] = this(4)
      obtain M4 M5 where
         decomp45: ‹(Decided K' # M4, M5) ∈ set (get_all_ann_decomposition M'')› and
         M4_lit: ‹map lit_of M4 = map lit_of M'''› and
         M4_dec: ‹map is_decided M4 = map is_decided M'''›
        using get_all_ann_decomposition_change_annotation_exists[OF decomp', of M''] eq
        by (auto simp: valid_trail_reduction_simps)
      obtain M6 where
        decomp45: ‹(Decided K' # M4, M6) ∈ set (get_all_ann_decomposition M1)›
        using get_all_ann_decomposition_exists_prepend[OF decomp45]
          get_all_ann_decomposition_exists_prepend[OF decomp]
          get_all_ann_decomposition_ex[of K' M4 ‹_ @ M2' @ Decided K # _ @ M5›]
        by (auto simp: valid_trail_reduction_simps)
      show ?thesis
        by (rule valid_trail_reduction.backtrack_red[OF decomp45])
          (use M4_lit M4_dec eq decomp_M1 in auto)
    qed
  qed
qed

lemma valid_trail_reduction_length_leD: ‹valid_trail_reduction M M' ⟹ length M' ≤ length M›
  by (auto simp: valid_trail_reduction_simps)

lemma valid_trail_reduction_level0_iff:
  assumes valid:  ‹valid_trail_reduction M M'› and n_d: ‹no_dup M›
  shows ‹(L ∈ lits_of_l M ∧ get_level M L = 0) ⟷ (L ∈ lits_of_l M' ∧ get_level M' L = 0)›
proof -
  have H[intro]: ‹map lit_of M = map lit_of M' ⟹ L ∈ lits_of_l M ⟹ L ∈  lits_of_l M'› for M M'
    by (metis lits_of_def set_map)
  have [dest]: ‹undefined_lit c L ⟹ L ∈ lits_of_l c ⟹ False› for c
    by (auto dest: in_lits_of_l_defined_litD)

  show ?thesis
    using valid
  proof cases
    case keep_red
    then show ?thesis
      by (metis H trail_renumber_get_level)
  next
    case (backtrack_red K M'' M2) note decomp = this(1) and eq = this(2,3)
    obtain M3 where M: ‹M = M3 @ Decided K # M''›
      using decomp by auto
    have ‹(L ∈ lits_of_l M ∧ get_level M L = 0) ⟷
      (L ∈ lits_of_l M'' ∧ get_level M'' L = 0)›
      using n_d unfolding M
      by (auto 4 4 simp: valid_trail_reduction_simps get_level_append_if get_level_cons_if
          atm_of_eq_atm_of
      dest: in_lits_of_l_defined_litD no_dup_append_in_atm_notin
      split: if_splits)
    also have ‹... ⟷ (L ∈ lits_of_l M' ∧ get_level M' L = 0)›
      using eq by (metis local.H trail_renumber_get_level)
    finally show ?thesis
      by blast
  qed
qed

lemma map_lit_of_eq_defined_litD: ‹map lit_of M = map lit_of M' ⟹ defined_lit M = defined_lit M'›
  apply (induction M arbitrary: M')
  subgoal by auto
  subgoal for L M M'
    by (cases M'; cases L; cases "hd M'")
      (auto simp: defined_lit_cons)
  done


lemma map_lit_of_eq_no_dupD: ‹map lit_of M = map lit_of M' ⟹ no_dup M = no_dup M'›
  apply (induction M arbitrary: M')
  subgoal by auto
  subgoal for L M M'
    by (cases M'; cases L; cases "hd M'")
      (auto dest: map_lit_of_eq_defined_litD)
  done

text ‹
  Remarks about the predicate:
  ▪ The cases \<^term>‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶
    E' ≠ 0 ⟶ P› are already covered by the invariants (where \<^term>‹P› means that there is
    clause which was already present before).
  ▪ There is no simple way to express that a reason is in \<^term>‹UE› or not in it. This was not a
    problem as long we did not empty it, but we had to include that. The only solution is to
    split the components in two parts: the one in the trail (that stay there forever and count
    toward the number of clauses) and the authorers that can be deleted.
›
inductive cdcl_twl_restart_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
restart_trail:
   ‹cdcl_twl_restart_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
       (M', N', None, NE + mset `# NE', UE'', NEk + mset `# NEk', UEk + mset `# UEk', NS, US', N0, U0', {#}, Q')›
  if
    ‹valid_trail_reduction M M'› and
    ‹init_clss_lf N = init_clss_lf N' + NE' + NEk'› and
    ‹learned_clss_lf N' + UE' + UEk' ⊆# learned_clss_lf N› and
    ‹∀E∈# (NE'+NEk'+UE'+UEk'). ∃L∈set E. L ∈ lits_of_l M ∧ get_level M L = 0› and
    ‹∀L E E' . Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E > 0  ⟶ E' > 0 ⟶
        E ∈# dom_m N' ∧ N' ∝ E = N ∝ E'› and
    ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶ E' ≠ 0 ⟶
       mset (N ∝ E') ∈# NEk + mset `# NEk' + UEk + mset `# UEk'› and
    ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E' = 0 ⟶ E = 0› and
    ‹0 ∉# dom_m N'› and
    ‹if length M = length M' then Q = Q' else Q' = {#}› and
    ‹US' = {#}› and
    ‹UE'' ⊆# UE + mset `# UE'› and
    ‹U0' = {#}›


lemma cdcl_twl_restart_l_refl:
  ‹get_conflict_l S = None ⟹ get_subsumed_learned_clauses_l S = {#} ⟹
  get_learned_clauses0_l S = {#} ⟹
  clauses_to_update_l S = {#} ⟹ twl_list_invs S ⟹ no_dup (get_trail_l S) ⟹
  cdcl_twl_restart_l S S›
  by (cases S)
    (auto simp: cdcl_twl_restart_l.simps twl_list_invs_def dest: no_dup_same_annotD)

lemma cdcl_twl_restart_l_list_invs:
  assumes
    ‹cdcl_twl_restart_l S T› and
    ‹twl_list_invs S›
  shows
    ‹twl_list_invs T›
  using assms
proof (induction rule: cdcl_twl_restart_l.induct)
  case (restart_trail M M' N N' NE' NEk' UE' UEk' NEk UEk Q Q' US' UE'' UE U0' NE NS US N0 U0) note red = this(1) and
    init = this(2) and
    learned = this(3) and NUE = this(4) and tr_ge0 = this(5) and tr_new0 = this(6) and
    tr_still0 = this(7) and dom0 = this(8) and QQ' = this(9) and US = this(10) and incl = this(11)
    and U0' = this(12) and list_invs = this(13)
  let ?S = ‹(M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0', {#}, Q)›
  let ?T = ‹(M', N', None, NE + mset `# NE', UE'', NEk + mset `# NEk', UEk + mset `# UEk', NS, US', N0, U0', {#}, Q')›
  show ?case
    unfolding twl_list_invs_def
  proof (intro conjI impI allI ballI)
    fix C
    assume ‹C ∈# clauses_to_update_l ?T›
    then show ‹C ∈# dom_m (get_clauses_l ?T)›
      by simp
  next
    show ‹0 ∉# dom_m (get_clauses_l ?T)›
      using dom0 by simp
  next
    fix L C
    assume LC: ‹Propagated L C ∈ set (get_trail_l ?T)› and C0: ‹0 < C›
    then obtain C' where LC': ‹Propagated L C' ∈ set (get_trail_l ?S)›
      using red by (auto dest!: valid_trail_reduction_Propagated_inD)
    moreover have C'0: ‹C' ≠ 0›
      apply (rule ccontr)
      using C0 tr_still0 LC LC'
      by (auto simp: twl_list_invs_def
        dest!: valid_trail_reduction_Propagated_inD)
    ultimately have C_dom: ‹C ∈# dom_m (get_clauses_l ?T)› and NCC': ‹N' ∝ C = N ∝ C'›
      using tr_ge0 C0 LC by auto
    show ‹C ∈# dom_m (get_clauses_l ?T)›
      using C_dom .

    have
      L_watched: ‹L ∈ set (watched_l (get_clauses_l ?S ∝ C'))› and
      L_C'0: ‹length (get_clauses_l ?S ∝ C') > 2 ⟹ L = get_clauses_l ?S ∝ C' ! 0›
      using list_invs C'0 LC' unfolding twl_list_invs_def
      by auto
    show ‹L ∈ set (watched_l (get_clauses_l ?T ∝ C))›
      using L_watched NCC' by simp

    show ‹length (get_clauses_l ?T ∝ C) > 2 ⟹ L = get_clauses_l ?T ∝ C ! 0›
      using L_C'0 NCC' by simp
  next
    show ‹distinct_mset (clauses_to_update_l ?T)›
      by auto
  next
    fix C
    assume ‹C ∈# ran_mf (get_clauses_l ?T)›
    then have ‹C ∈# ran_mf (get_clauses_l ?S)›
      by (smt (z3) all_clss_lf_ran_m get_clauses_l.simps learned local.init
        mset_subset_eq_exists_conv union_iff)
    moreover have ‹∀C∈#ran_m N. ¬ tautology (mset (fst C))›
      using list_invs unfolding twl_list_invs_def
      by simp
    ultimately show ‹¬tautology (mset C)›
      by auto
  qed
qed


lemma rtranclp_cdcl_twl_restart_l_list_invs:
  assumes
    ‹cdcl_twl_restart_l⇧*⇧* S T› and
    ‹twl_list_invs S›
  shows
    ‹twl_list_invs T›
  using assms by induction (auto intro: cdcl_twl_restart_l_list_invs)


inductive cdcl_twl_restart_only_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
restart_trail:
   ‹cdcl_twl_restart_only_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
       (M'', N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})›
  if
    ‹(Decided K # M'', M') ∈ set (get_all_ann_decomposition M)› |
no_restart:
   ‹cdcl_twl_restart_only_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
       (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›

lemma cdcl_twl_restart_only_l_list_invs:
  assumes
    ‹cdcl_twl_restart_only_l S T› and
    ‹twl_list_invs S›
  shows
    ‹twl_list_invs T›
  using assms
  by (induction rule: cdcl_twl_restart_only_l.induct)
    (auto simp: twl_list_invs_def valid_trail_reduction.simps)


lemma cdcl_twl_restart_only_l_cdcl_twl_restart_only:
  assumes
    ‹cdcl_twl_restart_only_l S T› and
    ST: ‹(S, S') ∈ twl_st_l None›
  shows ‹∃T'. (T, T') ∈ twl_st_l None ∧ cdcl_twl_restart_only S' T'›
  apply (rule_tac x = ‹(λ(M, N, U, C, NE, UE, NS, US, N0, U0, WS, Q).
    (drop (length (get_trail S') - length (get_trail_l T)) M, N, U, C, NE, UE, NS, US, N0, U0, WS,
    literals_to_update_l T)) S'›
    in exI)
  using assms
  apply (induction rule: cdcl_twl_restart_only_l.induct)
  apply (cases S')
  subgoal for K M'' M' M N NE UE NEk UEk NS US N0 U0 Q a b c d e f g h i j k l
    using convert_lits_l_decomp_ex(1)[of K M'' M' M ‹get_trail S'› N ‹NEk + UEk›]
    by (auto simp: twl_st_l_def convert_lits_l_decomp_ex
      intro: cdcl_twl_restart_only.intros(1))
  subgoal
    by (auto simp: twl_st_l_def convert_lits_l_imp_same_length
      intro: cdcl_twl_restart_only.intros(2))
  done

lemma cdcl_twl_restart_only_l_cdcl_twl_restart_only_spec:
  assumes ST: ‹(S, T) ∈ twl_st_l None› ‹twl_list_invs S›
  shows ‹SPEC (cdcl_twl_restart_only_l S) ≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
         clauses_to_update_l S = {#} ∧ get_conflict_l S = None}
    (SPEC (cdcl_twl_restart_only T))›
  apply (rule RES_refine)
  subgoal premises p for s
    using cdcl_twl_restart_only_l_cdcl_twl_restart_only[of S s, OF p(1)[simplified] assms(1)]
      cdcl_twl_restart_only_l_list_invs[of S s, OF p(1)[simplified]] p assms(2)
    apply - apply normalize_goal+
    apply (rule_tac x= x in bexI)
    apply (auto simp: cdcl_twl_restart_only_l.simps)
    done
  done

lemma cdcl_twl_restart_l_cdcl_twl_restart:
  assumes ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T›
  shows ‹SPEC (cdcl_twl_restart_l S) ≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
         clauses_to_update_l S = {#} ∧ get_conflict_l S = None}
     (SPEC (cdcl_twl_restart T))›
proof -
  have [simp]: ‹set (watched_l x) ∪ set (unwatched_l x) = set x› for x
    by (metis append_take_drop_id set_append)
  have ‹∃T'. cdcl_twl_restart T T' ∧ (S', T') ∈ twl_st_l None›
    if ‹cdcl_twl_restart_l S S'› for S'
    using that ST struct_invs
  proof (induction rule: cdcl_twl_restart_l.induct)
    case (restart_trail M M' N N' NE' NEk' UE' UEk' NEk UEk Q Q' US' UE'' UE U0' NE NS US N0 U0) note red = this(1) and
      init = this(2) and
      learned = this(3) and NUE = this(4) and tr_ge0 = this(5) and tr_new0 = this(6) and
      tr_still0 = this(7) and dom0 = this(8) and QQ' = this(9) and US = this(10) and incl = this(11)
      and U0 = this(12) and ST = this(13) and struct_invs = this(14)
    let ?T' = ‹(drop (length M - length M') (get_trail T), twl_clause_of `# init_clss_lf N',
          twl_clause_of `# learned_clss_lf N', None, NE+mset `# NE'+(NEk+mset`#NEk'), UE''+(UEk+mset`#UEk'), NS, US', N0,
          U0', {#}, Q')›
    have [intro]: ‹Q ≠ Q' ⟹ Q' = {#}›
      using QQ' by (auto split: if_splits)
    obtain TM where
        T: ‹T = (TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
        NE+NEk, UE+UEk, NS, US, N0, U0, {#}, Q)› and
      M_TM: ‹(M, TM) ∈ convert_lits_l N (NEk+UEk)›
      using ST
      by (cases T) (auto simp: twl_st_l_def)
    have ‹no_dup TM›
      using struct_invs unfolding T twl_struct_invs_def pcdcl_all_struct_invs_def
          cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
          cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      by (simp add: trail.simps)
    then have n_d: ‹no_dup M›
      using M_TM by auto
    have ‹cdcl_twl_restart T ?T'›
      using red
    proof (induction)
      case keep_red
      from arg_cong[OF this(1), of length] have [simp]: ‹length M = length M'› by simp
      have [simp]: ‹Q = Q'›
        using QQ' by simp
      have annot_in_clauses: ‹∀L E. Propagated L E ∈ set TM ⟶
        E ∈# clauses
              (twl_clause_of `# init_clss_lf N +
                twl_clause_of `# learned_clss_lf N')  +
              (NE + NEk + clauses (twl_clause_of `# (NE' + NEk'))) +
              (UE'' + (UEk + mset `# UEk'))›
      proof (intro allI impI conjI)
        fix L E
        assume ‹Propagated L E ∈ set TM›
        then obtain E' where LE'_M: ‹Propagated L E' ∈ set M› and
          E_E': ‹convert_lit N (NEk+UEk) (Propagated L E') (Propagated L E)›
          using in_convert_lits_lD[OF _ M_TM, of ‹Propagated L E›]
          by (auto simp: convert_lit.simps)
        then obtain E'' where LE''_M: ‹Propagated L E'' ∈ set M'›
          using valid_trail_reduction_Propagated_inD2[OF red, of L E'] by auto

        consider
          ‹E' = 0› and ‹E'' = 0› |
          ‹E' > 0› and ‹E'' = 0› and ‹mset (N ∝ E') ∈# NEk + mset `# NEk' + UEk + mset `# UEk'› |
          ‹E' > 0› and ‹E'' > 0› and ‹E'' ∈# dom_m N'› and ‹N ∝ E' = N' ∝ E''›
          using tr_ge0 tr_new0 tr_still0 LE'_M LE''_M E_E'
          by (cases ‹E''>0›; cases ‹E' > 0›) auto
        then show ‹E ∈# clauses
              (twl_clause_of `# init_clss_lf N +
                twl_clause_of `# learned_clss_lf N') +
              (NE + NEk + clauses (twl_clause_of `# (NE' + NEk'))) +
              (UE'' + (UEk + mset `# UEk'))›
          apply cases
          subgoal
            using E_E' incl tr_still0
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          subgoal
            using E_E' init
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          subgoal
            using E_E' init
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          done
      qed
      have ‹cdcl_twl_restart
        (TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
          NE + NEk, UE + UEk, NS, US, N0, U0, {#}, Q)
        (TM, twl_clause_of `# init_clss_lf N', twl_clause_of `# learned_clss_lf N', None,
          NE + NEk + (clauses (twl_clause_of `# (NE' + NEk'))), UE'' + (UEk + mset `# UEk'),
          NS, {#}, N0, {#}, {#}, Q)› (is ‹cdcl_twl_restart ?A ?B›)
        apply (rule cdcl_twl_restart.restart_clauses[where UE' = ‹(twl_clause_of `# (UE' + UEk'))›])
        subgoal
          using image_mset_subseteq_mono[OF learned, of twl_clause_of] by (auto simp: ac_simps)
        subgoal unfolding init image_mset_union by auto
        subgoal using NUE M_TM by auto
        subgoal by (rule annot_in_clauses)
        subgoal using US by (auto split: if_splits)
        subgoal using incl by (auto simp: mset_take_mset_drop_mset')
        done
      moreover have ‹?A = T›
        unfolding T by simp
      moreover have ‹?B = ?T'›
        using US U0
        by (auto simp: T mset_take_mset_drop_mset')
      ultimately show ?case
        by argo
    next
      case (backtrack_red K M2 M'') note decomp = this(1)
      have [simp]: ‹length M2 = length M'›
        using arg_cong[OF backtrack_red(2), of length] by simp
      have M_TM: ‹(drop (length M - length M') M, drop (length M - length M') TM) ∈
          convert_lits_l N (NEk+UEk)›
        using M_TM unfolding convert_lits_l_def list_rel_def by auto
      have red: ‹valid_trail_reduction (drop (length M - length M') M) M'›
        using red backtrack_red by (auto simp: valid_trail_reduction.simps)
      have annot_in_clauses: ‹∀L E. Propagated L E ∈ set (drop (length M - length M') TM) ⟶
        E ∈# clauses
              (twl_clause_of `# init_clss_lf N +
                twl_clause_of `# learned_clss_lf N')  +
              (NE + NEk + clauses (twl_clause_of `# (NE' + NEk'))) +
              (UE'' + (UEk + mset `# UEk'))›
      proof (intro allI impI conjI)
        fix L E
        assume ‹Propagated L E ∈ set (drop (length M - length M') TM)›
        then obtain E' where LE'_M: ‹Propagated L E' ∈ set (drop (length M - length M') M)› and
          E_E': ‹convert_lit N (NEk+UEk) (Propagated L E') (Propagated L E)›
          using in_convert_lits_lD[OF _ M_TM, of ‹Propagated L E›]
          by (auto simp: convert_lit.simps)
        then have ‹Propagated L E' ∈ set M2›
          using decomp by (auto dest!: get_all_ann_decomposition_exists_prepend)
        then obtain E'' where LE''_M: ‹Propagated L E'' ∈ set M'›
          using valid_trail_reduction_Propagated_inD2[OF red, of L E'] decomp
          by (auto dest!: get_all_ann_decomposition_exists_prepend)
        consider
          ‹E' = 0› and ‹E'' = 0› |
          ‹E' > 0› and ‹E'' = 0› and ‹mset (N ∝ E') ∈# NEk + mset `# NEk' + UEk + mset `# UEk'› |
          ‹E' > 0› and ‹E'' > 0› and ‹E'' ∈# dom_m N'› and ‹N ∝ E' = N' ∝ E''›
          using tr_ge0 tr_new0 tr_still0 LE'_M LE''_M E_E' decomp
          by (cases ‹E''>0›; cases ‹E' > 0›)
            (auto 5 5 dest!: get_all_ann_decomposition_exists_prepend
            simp: convert_lit.simps)
        then show ‹E ∈# clauses
              (twl_clause_of `# init_clss_lf N +
                twl_clause_of `# learned_clss_lf N')  +
              (NE + NEk + clauses (twl_clause_of `# (NE' + NEk'))) +
              (UE'' + (UEk + mset `# UEk'))›
          apply cases
          subgoal
            using E_E' incl
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          subgoal
            using E_E' init
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          subgoal
            using E_E' init
            by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
          done
      qed
      have lits_of_M2_M': ‹lits_of_l M2 = lits_of_l M'›
        using arg_cong[OF backtrack_red(2), of set] by (auto simp: lits_of_def)
      have lev_M2_M': ‹get_level M2 L = get_level M' L› for L
        using trail_renumber_get_level[OF backtrack_red(2-3)] by (auto simp: )
      have drop_M_M2: ‹drop (length M - length M') M = M2›
        using backtrack_red(1) by auto
      have H: ‹L ∈ lits_of_l (drop (length M - length M') TM) ∧
          get_level (drop (length M - length M') TM) L = 0›
        if ‹L ∈ lits_of_l M ∧ get_level M L = 0› for L
      proof -
        have ‹L ∈ lits_of_l M2 ∧ get_level M2 L = 0›
          using decomp that n_d
          by (auto dest!: get_all_ann_decomposition_exists_prepend
            dest: in_lits_of_l_defined_litD
            simp: get_level_append_if get_level_cons_if split: if_splits)
        then show ?thesis
          using M_TM
          by (auto dest!: simp: drop_M_M2)
      qed

      have
        ‹∃M2. (Decided K # drop (length M - length M') TM, M2) ∈ set (get_all_ann_decomposition TM)›
        using convert_lits_l_decomp_ex[OF decomp ‹(M, TM) ∈ convert_lits_l N (NEk + UEk)›]
          ‹(M, TM) ∈ convert_lits_l N (NEk + UEk)›
        by (simp add: convert_lits_l_imp_same_length)
      then obtain TM2 where decomp_TM:
          ‹(Decided K # drop (length M - length M') TM, TM2) ∈ set (get_all_ann_decomposition TM)›
          by blast
      have ‹cdcl_twl_restart
        (TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
          NE + NEk, UE + UEk, NS, US, N0, U0, {#}, Q)
        (drop (length M - length M') TM, twl_clause_of `# init_clss_lf N',
          twl_clause_of `# learned_clss_lf N', None,
          NE + NEk + clauses (twl_clause_of `# (NE' + NEk')), UE'' + (UEk + mset`#UEk'), NS, {#}, N0, {#},
          {#}, {#})› (is ‹cdcl_twl_restart ?A ?B›)
        apply (rule cdcl_twl_restart.restart_trail[where UE' = ‹(twl_clause_of `# (UE'+UEk'))›])
        apply (rule decomp_TM)
        subgoal
          using image_mset_subseteq_mono[OF learned, of twl_clause_of] by (auto simp: ac_simps)
        subgoal unfolding init image_mset_union by auto
        subgoal using NUE M_TM H by fastforce
        subgoal by (rule annot_in_clauses)
        subgoal using incl by (auto simp: mset_take_mset_drop_mset')
        done
      moreover have ‹?A = T›
        unfolding T by auto
      moreover have ‹?B = ?T'›
        using QQ' decomp US U0 unfolding T by (auto simp: mset_take_mset_drop_mset')
      ultimately show ?case
        by argo
    qed
    moreover {
      have ‹(M', drop (length M - length M') TM) ∈ convert_lits_l N' ((NEk+mset`#NEk') + (UEk+mset`#UEk'))›
      proof (rule convert_lits_lI)
        show ‹length M' = length (drop (length M - length M') TM)›
          using M_TM red by (auto simp: valid_trail_reduction.simps T
            dest: convert_lits_l_imp_same_length
            dest!: arg_cong[of ‹map lit_of _› _ length] get_all_ann_decomposition_exists_prepend)
        fix i
        assume i_M': ‹i < length M'›
        then have MM'_IM: ‹length M - length M' + i < length M›  ‹length M - length M' + i < length TM›
          using M_TM red by (auto simp: valid_trail_reduction.simps T
            dest: convert_lits_l_imp_same_length
            dest!: arg_cong[of ‹map lit_of _› _ length] get_all_ann_decomposition_exists_prepend)
        then have ‹convert_lit N (NEk + UEk) (drop (length M - length M') M ! i)
            (drop (length M - length M') TM ! i)›
          using M_TM list_all2_nthD[of ‹convert_lit N (NEk + UEk)› M TM ‹length M - length M' + i›] i_M'
          unfolding convert_lits_l_def list_rel_def p2rel_def
          by auto
        moreover
          have ‹lit_of (drop (length M - length M') M!i) = lit_of (M'!i)› and
            ‹is_decided (drop (length M - length M') M!i) = is_decided (M'!i)›
          using red i_M' MM'_IM
          by (auto 5 5 simp:valid_trail_reduction_simps nth_append
            dest: map_eq_nth_eq[of _ _ _ i]
            dest!: get_all_ann_decomposition_exists_prepend)
        moreover have ‹M'!i ∈ set M'›
          using i_M' by auto
        moreover have ‹drop (length M - length M') M!i ∈ set M›
          using MM'_IM by auto
        ultimately show ‹convert_lit N' ((NEk+mset`#NEk') + (UEk+mset`#UEk')) (M' ! i)
            (drop (length M - length M') TM ! i)›
          using tr_new0 tr_still0 tr_ge0
            by (cases ‹M'!i›)
             (fastforce simp: convert_lit.simps)+
      qed
      then have ‹((M', N', None, NE + mset `# NE', UE'', NEk+mset`#NEk', UEk+mset`#UEk', NS, US', N0, U0', {#}, Q'), ?T')
        ∈ twl_st_l None›
        using M_TM by (auto simp: twl_st_l_def T)
    }
    ultimately show ?case
      by fast
  qed
  moreover have ‹cdcl_twl_restart_l S S' ⟹ twl_list_invs S'› for S'
    by (rule cdcl_twl_restart_l_list_invs) (use list_invs in fast)+
  moreover have ‹cdcl_twl_restart_l S S' ⟹ clauses_to_update_l S' = {#} ∧ get_conflict_l S' = None› for S'
    by (auto simp: cdcl_twl_restart_l.simps)
  ultimately show ?thesis
    by (blast intro!: RES_refine)
qed



text ‹
  We here start the refinement towards an executable version of the restarts. The idea of the
  restart is the following:
  ▸ We backtrack to level 0. This simplifies further steps (even if it would be better not to do 
     that).
  ▸ We first move all clause annotating a literal to \<^term>‹NE› or \<^term>‹UE›.
  ▸ Now we can safely deleting any remaining learned clauses.
  ▸ Once all that is done, we have to recalculate the watch lists (and can on the way GC the set of
    clauses).

The key idea of our approach is that each transformation is a proper restart. As restarts can be
composed to obtain a single restart, we get a single restart. The modular approach is much nicer
to prove, but it also makes it easier to have several different restart paths (with and without GC).
›

subsubsection ‹Handle true clauses from the trail›

lemma in_set_mset_eq_in:
  ‹i ∈ set A ⟹ mset A = B ⟹ i ∈# B›
  by fastforce


text ‹Our transformation will be chains of a weaker version of restarts, that don't update the
  watch lists and only keep partial correctness of it.
›

lemma cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l:
  assumes
    ST: ‹cdcl_twl_restart_l S T› and TU: ‹cdcl_twl_restart_l T U› and
    n_d: ‹no_dup (get_trail_l S)›
  shows ‹cdcl_twl_restart_l S U›
  using assms
proof -
  obtain M M' N N' NE' UE' NEk UEk NEk' UEk' NE UE UE'' NS US N0 U0 Q Q' W' W where
    S: ‹S = (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)› and
    T: ‹T = (M', N', None, NE + mset `# NE', UE'', NEk + mset`#NEk', UEk + mset`#UEk', NS, {#}, N0, {#}, W', Q')› and
    tr_red: ‹valid_trail_reduction M M'› and
    init: ‹init_clss_lf N = init_clss_lf N' + NE' + NEk'› and
    learned: ‹learned_clss_lf N' + UE' + UEk' ⊆# learned_clss_lf N›  and
    NUE: ‹∀E∈#NE' + NEk' + UE' + UEk'. ∃L∈set E. L ∈ lits_of_l M ∧ get_level M L = 0› and
    ge0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ 0 < E ⟶ 0 < E' ⟶
        E ∈# dom_m N' ∧ N' ∝ E = N ∝ E'› and
    new0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶
         E' ≠ 0 ⟶ mset (N ∝ E') ∈# NEk + mset `# NEk' + UEk + mset `# UEk'› and
    still0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶
        E' = 0 ⟶ E = 0› and
    dom0: ‹0 ∉# dom_m N'› and
    QQ': ‹if length M = length M' then Q = Q' else Q' = {#}› and
    W: ‹W = {#}› and
    incl: ‹UE'' ⊆# UE + mset `# UE'›
    using ST unfolding cdcl_twl_restart_l.simps
    apply -
    apply normalize_goal+
    by force
  obtain M'' N'' NE'' U2E'' Q'' W'' NEk'' UEk'' UE''' where
    U: ‹U = (M'', N'', None, (NE + mset `# NE') + mset `# NE'', UE''',
      (NEk + mset`#NEk')+ mset`#NEk'', (UEk + mset`#UEk')+ mset`#UEk'',NS,
      {#}, N0, {#}, W'', Q'')› and
    tr_red': ‹valid_trail_reduction M' M''› and
    init': ‹init_clss_lf N' = init_clss_lf N'' + NE'' + NEk''› and
    learned': ‹learned_clss_lf N'' + U2E'' + UEk'' ⊆# learned_clss_lf N'› and
    NUE': ‹∀E∈#NE'' + NEk'' + U2E'' + UEk''.
        ∃L∈set E.
           L ∈ lits_of_l M' ∧
           get_level M' L = 0› and
    ge0': ‹∀L E E'.
        Propagated L E ∈ set M'' ⟶
        Propagated L E' ∈ set M' ⟶
        0 < E ⟶
        0 < E' ⟶
        E ∈# dom_m N'' ∧ N'' ∝ E = N' ∝ E'› and
    new0': ‹∀L E E'.
        Propagated L E ∈ set M'' ⟶
        Propagated L E' ∈ set M' ⟶
        E = 0 ⟶
        E' ≠ 0 ⟶
        mset (N' ∝ E')
        ∈# (NEk + mset `# NEk') + mset`#NEk'' + (UEk + mset `# UEk')+ mset`#UEk''› and
    still0': ‹∀L E E'.
        Propagated L E ∈ set M'' ⟶
        Propagated L E' ∈ set M' ⟶
        E' = 0 ⟶ E = 0›  and
    dom0': ‹0 ∉# dom_m N''› and
    Q'Q'': ‹if length M' = length M'' then Q' = Q'' else Q'' = {#}› and
    W': ‹W' = {#}› and
    W'': ‹W'' = {#}›
    and
     incl': ‹UE''' ⊆# UE'' + mset `# U2E''› 
    using TU unfolding cdcl_twl_restart_l.simps T apply -
    apply normalize_goal+
    by blast
  have U': ‹U = (M'', N'', None, NE + mset `# (NE' + NE''), UE''',
    NEk + mset`#(NEk'+ NEk''), UEk + mset`#(UEk'+UEk''), NS, {#}, 
      N0, {#}, W'', Q'')›
    unfolding U by simp
  show ?thesis
    unfolding S U' W W' W''
    apply (rule cdcl_twl_restart_l.restart_trail[where UE'=‹UE'+U2E''›])
    subgoal using valid_trail_reduction_trans[OF tr_red tr_red'] .
    subgoal using init init' by auto
    subgoal using learned learned' subset_mset.dual_order.trans
      by (smt (verit, ccfv_threshold) add.assoc mset_subset_eq_mono_add_right_cancel union_commute)
    subgoal using NUE NUE' valid_trail_reduction_level0_iff[OF tr_red] n_d unfolding S by auto
    subgoal using ge0 ge0' tr_red' init learned NUE ge0  still0' (* TODO tune proof *)
      apply (auto dest: valid_trail_reduction_Propagated_inD)
      apply (blast dest: valid_trail_reduction_Propagated_inD)+
       apply (metis neq0_conv still0' valid_trail_reduction_Propagated_inD)+
      done
    subgoal using new0 new0' tr_red' init learned NUE ge0  (* TODO tune proof *)
      apply (auto dest: valid_trail_reduction_Propagated_inD)
      by (smt neq0_conv valid_trail_reduction_Propagated_inD)
    subgoal using still0 still0' tr_red' by (fastforce dest: valid_trail_reduction_Propagated_inD)
    subgoal using dom0' .
    subgoal using QQ' Q'Q'' valid_trail_reduction_length_leD[OF tr_red]
        valid_trail_reduction_length_leD[OF tr_red']
      by (auto split: if_splits)
    subgoal by auto
    subgoal using incl incl' subset_mset.order_trans by fastforce
    subgoal by (rule refl)
    done
qed

lemma rtranclp_cdcl_twl_restart_l_no_dup:
  assumes
    ST: ‹cdcl_twl_restart_l⇧*⇧* S T› and
    n_d: ‹no_dup (get_trail_l S)›
  shows ‹no_dup (get_trail_l T)›
  using assms
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal
    by (auto simp: cdcl_twl_restart_l.simps valid_trail_reduction_simps
      dest: map_lit_of_eq_no_dupD dest!: no_dup_appendD get_all_ann_decomposition_exists_prepend)
  done

lemma tranclp_cdcl_twl_restart_l_cdcl_is_cdcl_twl_restart_l:
  assumes
    ST: ‹cdcl_twl_restart_l⇧+⇧+ S T› and
    n_d: ‹no_dup (get_trail_l S)›
  shows ‹cdcl_twl_restart_l S T›
  using assms
  apply (induction rule: tranclp_induct)
  subgoal by auto
  subgoal
    using cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l
    rtranclp_cdcl_twl_restart_l_no_dup by blast
  done


paragraph ‹Auxilary definition›
text ‹
  This definition states that the domain of the clauses is reduced, but the remaining clauses
  are not changed.
›
definition reduce_dom_clauses where
  ‹reduce_dom_clauses N N' ⟷
     (∀C. C ∈# dom_m N' ⟶ C ∈# dom_m N ∧ fmlookup N C = fmlookup N' C)›

lemma reduce_dom_clauses_fdrop[simp]: ‹reduce_dom_clauses N (fmdrop C N)›
  using distinct_mset_dom[of N]
  by (auto simp: reduce_dom_clauses_def dest: in_diffD multi_member_split
    distinct_mem_diff_mset)

lemma reduce_dom_clauses_refl[simp]: ‹reduce_dom_clauses N N›
  by (auto simp: reduce_dom_clauses_def)

lemma reduce_dom_clauses_trans:
  ‹reduce_dom_clauses N N' ⟹ reduce_dom_clauses N' N'a ⟹ reduce_dom_clauses N N'a›
  by (auto simp: reduce_dom_clauses_def)

definition valid_trail_reduction_eq where
  ‹valid_trail_reduction_eq M M' ⟷ valid_trail_reduction M M' ∧ length M = length M'›

lemma valid_trail_reduction_eq_alt_def:
  ‹valid_trail_reduction_eq M M' ⟷ map lit_of M = map lit_of M' ∧
      map is_decided M = map is_decided M'›
    by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
      dest!: get_all_ann_decomposition_exists_prepend
      dest: map_eq_imp_length_eq trail_renumber_get_level)

lemma valid_trail_reduction_change_annot:
   ‹valid_trail_reduction (M @ Propagated L C # M')
              (M @ Propagated L 0 # M')›
    by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps)

lemma valid_trail_reduction_eq_change_annot:
   ‹valid_trail_reduction_eq (M @ Propagated L C # M')
              (M @ Propagated L 0 # M')›
    by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps)

lemma valid_trail_reduction_eq_refl: ‹valid_trail_reduction_eq M M›
  by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction_refl)

lemma valid_trail_reduction_eq_get_level:
  ‹valid_trail_reduction_eq M M' ⟹ get_level M = get_level M'›
  by (intro ext)
    (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
      dest!: get_all_ann_decomposition_exists_prepend
      dest: map_eq_imp_length_eq trail_renumber_get_level)

lemma valid_trail_reduction_eq_lits_of_l:
  ‹valid_trail_reduction_eq M M' ⟹ lits_of_l M = lits_of_l M'›
  apply (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
      dest!: get_all_ann_decomposition_exists_prepend
      dest: map_eq_imp_length_eq trail_renumber_get_level)
  apply (metis image_set lits_of_def)+
  done

lemma valid_trail_reduction_eq_trans:
  ‹valid_trail_reduction_eq M M' ⟹ valid_trail_reduction_eq M' M'' ⟹
    valid_trail_reduction_eq M M''›
  unfolding valid_trail_reduction_eq_alt_def
  by auto

definition no_dup_reasons_invs_wl where
  ‹no_dup_reasons_invs_wl S ⟷
    (distinct_mset (mark_of `# filter_mset (λC. is_proped C ∧ mark_of C > 0) (mset (get_trail_l S))))›

inductive different_annot_all_killed where
propa_changed:
  ‹different_annot_all_killed N NUE (Propagated L C) (Propagated L C')›
    if ‹C ≠ C'› and ‹C' = 0› and
       ‹C ∈# dom_m N ⟹ mset (N∝C) ∈# NUE› |
propa_not_changed:
  ‹different_annot_all_killed N NUE (Propagated L C) (Propagated L C)› |
decided_not_changed:
  ‹different_annot_all_killed N NUE (Decided L) (Decided L)›

lemma different_annot_all_killed_refl[iff]:
  ‹different_annot_all_killed N NUE z z ⟷ is_proped z ∨ is_decided z›
  by (cases z) (auto simp: different_annot_all_killed.simps)

abbreviation different_annots_all_killed where
  ‹different_annots_all_killed N NUE ≡ list_all2 (different_annot_all_killed N NUE)›

lemma different_annots_all_killed_refl:
  ‹different_annots_all_killed N NUE M M›
  by (auto intro!: list.rel_refl_strong simp: count_decided_0_iff is_decided_no_proped_iff)


paragraph ‹Refinement towards code›

text ‹
  Once of the first thing we do, is removing clauses we know to be true. We do in two ways:
    ▪ along the trail (at level 0); this makes sure that annotations are kept;
    ▪ then along the watch list.

  This is (obviously) not complete but is faster by avoiding iterating over all clauses. Here are
  the rules we want to apply for our very limited inprocessing:
›
inductive remove_one_annot_true_clause :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
remove_irred_trail:
  ‹remove_one_annot_true_clause (M @ Propagated L C # M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
     (M @ Propagated L 0 # M', fmdrop C N, D, NE, {#}, add_mset (mset (N∝C)) NEk, UEk, NS, {#}, N0, {#}, W, Q)›
if
  ‹get_level (M @ Propagated L C # M') L = 0› and
  ‹C > 0› and
  ‹C ∈# dom_m N› and
  ‹irred N C› |
remove_red_trail:
  ‹remove_one_annot_true_clause (M @ Propagated L C # M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
     (M @ Propagated L 0 # M', fmdrop C N, D, NE, {#}, NEk, add_mset (mset (N∝C)) UEk, NS, {#}, N0, {#}, W, Q)›
if
  ‹get_level (M @ Propagated L C # M') L = 0› and
  ‹C > 0› and
  ‹C ∈# dom_m N› and
  ‹¬irred N C› |
remove_irred:
  ‹remove_one_annot_true_clause (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
     (M, fmdrop C N, D, add_mset (mset (N∝C))NE, {#}, NEk, UEk, NS, {#}, N0, {#}, W, Q)›
if
  ‹L ∈ lits_of_l M› and
  ‹get_level M L = 0› and
  ‹C ∈# dom_m N› and
  ‹L ∈ set (N∝C)› and
  ‹irred N C› and
  ‹∀L. Propagated L C ∉ set M› |
delete:
  ‹remove_one_annot_true_clause (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
     (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, W, Q)›
if
  ‹C ∈# dom_m N› and
  ‹¬irred N C› and
  ‹∀L. Propagated L C ∉ set M› |
delete_subsumed:
  ‹remove_one_annot_true_clause (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
     (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, W, Q)›

text ‹Remarks:
  ▸ \<^term>‹∀L. Propagated L C ∉ set M› is overkill. However, I am currently unsure how I want to
  handle it (either as \<^term>‹Propagated (N∝C!0) C ∉ set M› or as ``the trail contains only zero
  anyway'').›

lemma Ex_ex_eq_Ex: ‹(∃NE'. (∃b. NE' = {#b#} ∧ P b NE') ∧ Q NE') ⟷
   (∃b. P b {#b#} ∧ Q {#b#})›
   by auto

lemma in_set_definedD:
  ‹Propagated L' C ∈ set M' ⟹ defined_lit M' L'›
  ‹Decided L' ∈ set M' ⟹ defined_lit M' L'›
  by (auto simp: defined_lit_def)

lemma (in conflict_driven_clause_learning⇩W) trail_no_annotation_reuse:
  assumes
    struct_invs: ‹cdcl⇩W_all_struct_inv S› and
    LC: ‹Propagated L C ∈ set (trail S)› and
    LC': ‹Propagated L' C ∈ set (trail S)›
  shows "L = L'"
proof -
  have
    confl: ‹cdcl⇩W_conflicting S› and
    n_d: ‹no_dup (trail S)›
    using struct_invs unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
    by fast+
  have H: ‹L = L'› if ‹trail S = ysa @ Propagated L' C # c21 @ Propagated L C # zs›
    for ysa xsa c21 zs L L'
  proof -
    have 1: ‹c21 @ Propagated L C # zs ⊨as CNot (remove1_mset L' C) ∧ L' ∈# C›
      using confl unfolding cdcl⇩W_conflicting_def that
      by (auto)
    have that': ‹trail S = (ysa @ Propagated L' C # c21) @ Propagated L C # zs›
      unfolding that by auto
    have 2: ‹zs ⊨as CNot (remove1_mset L C) ∧ L ∈# C›
      using confl unfolding cdcl⇩W_conflicting_def that'
      by blast
    show ‹L = L'›
      using 1 2 n_d unfolding that
      by (auto dest!: multi_member_split
        simp: true_annots_true_cls_def_iff_negation_in_model add_mset_eq_add_mset
        Decided_Propagated_in_iff_in_lits_of_l)
  qed
  show ?thesis
    using H[of _ L _ L']  H[of _  L' _ L]
    using split_list[OF LC] split_list[OF LC']
    by (force elim!: list_match_lel_lel)
qed

lemma remove_one_annot_true_clause_cdcl_twl_restart_l:
  assumes
    rem: ‹remove_one_annot_true_clause S T› and
    lst_invs: ‹twl_list_invs S› and
    SS': ‹(S, S') ∈ twl_st_l None› and
    struct_invs: ‹twl_struct_invs S'› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}› and
    n_d: ‹no_dup (get_trail_l S)›
  shows ‹cdcl_twl_restart_l S T›
  using assms
proof -
  have dist_N: ‹distinct_mset (dom_m (get_clauses_l S))›
    by (rule distinct_mset_dom)
  then have C_notin_rem: ‹C ∉# remove1_mset C (dom_m (get_clauses_l S))› for C
    by (simp add: distinct_mset_remove1_All)
   have
    ‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
    dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
    annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
           0 < C ⟹
             (C ∈# dom_m (get_clauses_l S) ∧
            L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
            (length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
    ‹distinct_mset (clauses_to_update_l S)›
    using lst_invs unfolding twl_list_invs_def apply -
    by fast+

  have struct_S': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')›
    using struct_invs unfolding twl_struct_invs_def pcdcl_all_struct_invs_def state⇩W_of_def by fast
  show ?thesis
    using rem
  proof (cases rule: remove_one_annot_true_clause.cases)
    case (remove_irred_trail M L C M' N D NE UE NEk UEk NS US N0 U0 W Q) note S = this(1) and T = this(2) and
      lev_L = this(3) and C0 = this(4) and C_dom = this(5) and irred = this(6)
    have D: ‹D = None› and W: ‹W = {#}›
      using confl upd unfolding S by auto
    have NE: ‹add_mset (mset (N ∝ C)) NE = NE + mset `# {#N∝C#}›
      by simp
    have UE: ‹UE = UE + mset `# {#}›
      by simp
    have new_NUE: ‹∀E∈#{#} + {#N ∝ C#} + {#} + {#}.
       ∃La∈set E.
          La ∈ lits_of_l (M @ Propagated L C # M') ∧
          get_level (M @ Propagated L C # M') La = 0›
      apply (intro ballI impI)
      apply (rule_tac x=L in bexI)
      using lev_L annot[of L _] C0 by (auto simp: S dest: in_set_takeD[of _ 2])
    have [simp]: ‹Propagated L E' ∉ set M'› ‹Propagated L E' ∉ set M› for E'
      using n_d lst_invs
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E'› M]
           split_list[of ‹Propagated L E'› M'])
    have [simp]:  ‹Propagated L' C ∉ set M'› ‹Propagated L' C ∉ set M› for L'
      using SS' n_d C0 struct_S'
      cdcl⇩W_restart_mset.trail_no_annotation_reuse[of ‹state⇩W_of S'› L ‹(mset (N ∝ C))› L']
      apply (auto simp: S twl_st_l_def convert_lits_l_imp_same_length trail.simps
        )
      apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
        p2rel_def)
      apply (case_tac y)
      apply (auto simp: list_rel_append1 list_rel_split_right_iff defined_lit_convert_lits_l
        simp flip: p2rel_def convert_lits_l_def dest: in_set_definedD(1)[of _ _ M'])
      apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
        p2rel_def convert_lit.simps
        dest!: split_list[of ‹Propagated L' C› M']
           split_list[of ‹Propagated L' C› M])
      done
    have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M]
           elim!: list_match_lel_lel)
    have propa_M'M': ‹Propagated L E ∈ set M' ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M']
           split_list[of ‹Propagated L E'› M']
           elim!: list_match_lel_lel)
    have propa_MM': ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ False› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M']
           elim!: list_match_lel_lel)
    have propa_M'_nC_dom: ‹Propagated La E ∈ set M' ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
      using annot[of La E] unfolding S by auto
    have propa_M_nC_dom:  ‹Propagated La E ∈ set M ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
      using annot[of La E] unfolding S by auto
    have H: ‹add_mset (mset (N ∝ C)) NEk = NEk + mset `# {#N ∝ C#}›
      ‹UEk = UEk + mset `# {#}›
      ‹NE = NE + mset `# {#}›
      by auto
    show ?thesis
      unfolding S T D W NE
      apply (subst H)
      apply (subst(2) H(2))
      apply (subst(2) H(3))
      apply (rule cdcl_twl_restart_l.intros[where UE'=‹{#}›])
      subgoal by (auto simp: valid_trail_reduction_change_annot)
      subgoal using C_dom irred by auto
      subgoal using irred by auto
      subgoal using new_NUE .
      subgoal
        apply (intro conjI allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E]
          unfolding S by auto
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          unfolding S by auto
        done
      subgoal
        apply (intro allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          by auto
        done
      subgoal
        apply (intro allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          by auto
        done
      subgoal using dom0 unfolding S by (auto dest: in_diffD)
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      done
  next
    case (remove_red_trail M L C M' N D NE UE NEk UEk NS US N0 U0 W Q) note S =this(1) and T = this(2) and
      lev_L = this(3) and C0 = this(4) and C_dom = this(5) and irred = this(6)
    have D: ‹D = None› and W: ‹W = {#}›
      using confl upd unfolding S by auto
    have UE: ‹add_mset (mset (N ∝ C)) UE = UE + mset `# {#N∝C#}›
      by simp
    have NE: ‹NE = NE + mset `# {#}›
      by simp
    have new_NUE: ‹∀E∈#{#} + {#} + {#} + {#N ∝ C#}.
       ∃La∈set E.
          La ∈ lits_of_l (M @ Propagated L C # M') ∧
          get_level (M @ Propagated L C # M') La = 0›
      apply (intro ballI impI)
      apply (rule_tac x=L in bexI)
      using lev_L annot[of L _] C0 by (auto simp: S dest: in_set_takeD[of _ 2])
    have [simp]: ‹Propagated L E' ∉ set M'› ‹Propagated L E' ∉ set M› for E'
      using n_d lst_invs
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E'› M]
           split_list[of ‹Propagated L E'› M'])
    have [simp]:  ‹Propagated L' C ∉ set M'› ‹Propagated L' C ∉ set M› for L'
      using SS' n_d C0 struct_S'
      cdcl⇩W_restart_mset.trail_no_annotation_reuse[of ‹state⇩W_of S'› L ‹(mset (N ∝ C))› L']
      apply (auto simp: S twl_st_l_def convert_lits_l_imp_same_length trail.simps
        )
      apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
        p2rel_def)
      apply (case_tac y)
      apply (auto simp: list_rel_append1 list_rel_split_right_iff defined_lit_convert_lits_l
        simp flip: p2rel_def convert_lits_l_def dest: in_set_definedD(1)[of _ _ M'])
      apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
        p2rel_def convert_lit.simps
        dest!: split_list[of ‹Propagated L' C› M']
           split_list[of ‹Propagated L' C› M])
      done
    have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M]
           elim!: list_match_lel_lel)
    have propa_M'M': ‹Propagated L E ∈ set M' ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M']
           split_list[of ‹Propagated L E'› M']
           elim!: list_match_lel_lel)
    have propa_MM': ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ False› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M']
           elim!: list_match_lel_lel)
    have propa_M'_nC_dom:  ‹Propagated La E ∈ set M' ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
      using annot[of La E] unfolding S by auto
    have propa_M_nC_dom:  ‹Propagated La E ∈ set M ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
      using annot[of La E] unfolding S by auto
    have H: ‹add_mset (mset (N ∝ C)) UEk = UEk + mset `# {#N ∝ C#}›
      ‹NEk = NEk + mset `# {#}›
      ‹NE = NE + mset `# {#}›
      by auto
    show ?thesis
      unfolding S T D W UE
      apply (subst H)
      apply (subst(2) H(2))
      apply (subst(2) H(3))
      apply (rule cdcl_twl_restart_l.intros[where UE'=‹{#}›])
      subgoal by (auto simp: valid_trail_reduction_change_annot)
      subgoal using C_dom irred by auto
      subgoal using C_dom irred by auto
      subgoal using new_NUE .
      subgoal
        apply (intro conjI allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E]
          unfolding S by auto
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          unfolding S by auto
        done
      subgoal
        apply (intro allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          by auto
        done
      subgoal
        apply (intro allI impI)
        subgoal for La E E'
          using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
            propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
          by auto
        done
      subgoal using dom0 unfolding S by (auto dest: in_diffD)
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      done
  next
    case (remove_irred L M C N D NE UE NEk UEk NS US N0 U0 W Q) note S =this(1) and T = this(2) and
      L_M = this(3) and lev_L = this(4) and C_dom = this(5) and watched_L = this(6) and
      irred = this(7) and L_notin_M = this(8)
    have NE: ‹add_mset (mset (N ∝ C)) NE = NE + mset `# {#N∝C#}›
      by simp
    have UE: ‹UE = UE + mset `# {#}›
      by simp
    have D: ‹D = None› and W: ‹W = {#}›
      using confl upd unfolding S by auto
    have new_NUE: ‹∀E∈#{#N ∝ C#} + {#} + {#} + {#}.
       ∃La∈set E.
          La ∈ lits_of_l M ∧
          get_level M La = 0›
      apply (intro ballI impI)
      apply (rule_tac x=L in bexI)
      using lev_L annot[of L _] L_M watched_L by (auto simp: S dest: in_set_takeD[of _ 2])
    have C0: ‹C > 0›
      using dom0 C_dom unfolding S by (auto dest!: multi_member_split)
    have [simp]: ‹Propagated La C ∉ set M› for La
      using annot[of La C] dom0 n_d L_notin_M C0 unfolding S
      by auto
    have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M]
           elim!: list_match_lel_lel)
    have H: ‹UEk = UEk + mset `# {#}›
      ‹NEk = NEk + mset `# {#}›
      ‹NE = NE + mset `# {#}›
      by auto
    have H: ‹UEk = UEk + mset `# {#}›
      ‹NEk = NEk + mset `# {#}›
      by auto
    show ?thesis
      unfolding S T D W NE
      apply (subst(2) H(1))
      apply (subst(2)H(2))
      apply (rule cdcl_twl_restart_l.intros[where UE'=‹{#}›])
      subgoal by (auto simp: valid_trail_reduction_refl)
      subgoal using C_dom irred by auto
      subgoal using C_dom irred by auto
      subgoal using new_NUE .
      subgoal
        using n_d L_notin_M C_notin_rem annot propa_MM unfolding S by force
      subgoal
        using propa_MM by auto
      subgoal
        using propa_MM by auto
      subgoal using dom0 C_dom unfolding S by (auto dest: in_diffD)
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      done
  next
    case (delete C N M D NE UE NEk UEk NS US N0 U0 W Q) note S = this(1) and T = this(2) and C_dom = this(3) and
       irred = this(4) and L_notin_M = this(5)
    have D: ‹D = None› and W: ‹W = {#}›
      using confl upd unfolding S by auto
    have NE: ‹NE = NE + mset `# {#}›
      by simp
    have H: ‹UEk = UEk + mset `# {#}›
      ‹NEk = NEk + mset `# {#}›
      by auto
    have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
      using n_d
      by (auto simp: S twl_list_invs_def
        dest!: split_list[of ‹Propagated L E› M]
           split_list[of ‹Propagated L E'› M]
           elim!: list_match_lel_lel)
    show ?thesis
      unfolding S T D W
      apply (subst (2) NE)
      apply (subst(2) H(1))
      apply (subst(2)H(2))
      apply (rule cdcl_twl_restart_l.intros[where UE'=‹{#}›])
      subgoal by (auto simp: valid_trail_reduction_refl)
      subgoal using C_dom irred by auto
      subgoal using C_dom irred by auto
      subgoal by simp
      subgoal
        apply (intro conjI impI allI)
        subgoal for L E E'
          using n_d L_notin_M C_notin_rem annot propa_MM[of L E E'] unfolding S
          by (metis dom_m_fmdrop get_clauses_l.simps get_trail_l.simps in_remove1_msetI)
        subgoal for L E E'
          using n_d L_notin_M C_notin_rem annot propa_MM[of L E E'] unfolding S
          by auto
        done
      subgoal
        using propa_MM by auto
      subgoal
        using propa_MM by auto
      subgoal using dom0 C_dom unfolding S by (auto dest: in_diffD)
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      done
  next
    case (delete_subsumed M N D NE UE NEk UEk NS US N0 U0 W Q)
    have ‹cdcl_twl_restart_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
      (M, N, None, NE + mset `# {#}, {#}, NEk + mset `# {#}, UEk + mset `# {#},
      NS, {#}, N0, {#}, {#}, Q)›
      by (rule cdcl_twl_restart_l.intros)
        (use lst_invs n_d in ‹auto dest: no_dup_same_annotD simp: delete_subsumed twl_list_invs_def›)
    then show ?thesis
      using assms
      unfolding delete_subsumed
      by simp
  qed
qed


lemma is_annot_iff_annotates_first:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    C0: ‹C > 0›
  shows
    ‹(∃L. Propagated L C ∈ set (get_trail_l S)) ⟷
       ((length (get_clauses_l S ∝ C) > 2 ⟶
          Propagated (get_clauses_l S ∝ C ! 0) C ∈ set (get_trail_l S)) ∧
        ((length (get_clauses_l S ∝ C) ≤ 2 ⟶
	   Propagated (get_clauses_l S ∝ C ! 0) C ∈ set (get_trail_l S) ∨
	   Propagated (get_clauses_l S ∝ C ! 1) C ∈ set (get_trail_l S))))›
    (is ‹?A ⟷ ?B›)
proof (rule iffI)
  assume ?B
  then show ?A by auto
next
  assume ?A
  then obtain L where
    LC: ‹Propagated L C ∈ set (get_trail_l S)›
    by blast
  then have
    C: ‹C ∈# dom_m (get_clauses_l S)› and
    L_w: ‹L ∈ set (watched_l (get_clauses_l S ∝ C))› and
    L: ‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
    using list_invs C0 unfolding twl_list_invs_def by blast+
  have ‹twl_st_inv T›
    using struct_invs unfolding twl_struct_invs_def by fast
  then have le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
    using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
    by (cases S; cases T)
      (auto simp: twl_st_inv.simps twl_st_l_def
        image_Un[symmetric])
  show ?B
  proof (cases ‹length (get_clauses_l S ∝ C) > 2›)
    case True
    show ?thesis
      using L True LC by auto
  next
    case False
    then show ?thesis
      using LC le2 L_w
      by (cases ‹get_clauses_l S ∝ C›;
           cases ‹tl (get_clauses_l S ∝ C)›)
        auto
  qed
qed

lemma trail_length_ge2:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    LaC: ‹Propagated L C ∈ set (get_trail_l S)› and
    C0: ‹C > 0›
  shows
    ‹length (get_clauses_l S ∝ C) ≥ 2›
proof -
  have conv:
   ‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_kept_unit_clauses_l S)›
   using ST unfolding twl_st_l_def by auto

  have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
    lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)›
    using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      pcdcl_all_struct_invs_def state⇩W_of_def
    by fast+

  have n_d: ‹no_dup (get_trail_l S)›
    using ST lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: twl_st_l twl_st)
  have
    C: ‹C ∈# dom_m (get_clauses_l S)›
    using list_invs C0 LaC by (auto simp: twl_list_invs_def all_conj_distrib)
  have ‹twl_st_inv T›
    using struct_invs unfolding twl_struct_invs_def by fast
  then show le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
    using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
    by (cases S; cases T)
      (auto simp: twl_st_inv.simps twl_st_l_def
        image_Un[symmetric])
qed

lemma is_annot_no_other_true_lit:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    C0: ‹C > 0› and
    LaC: ‹Propagated La C ∈ set (get_trail_l S)› and
    LC: ‹L ∈ set (get_clauses_l S ∝ C)› and
    L: ‹L ∈ lits_of_l (get_trail_l S)›
  shows
    ‹La = L› and
    ‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
proof -
  have conv:
   ‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_kept_unit_clauses_l S)›
   using ST unfolding twl_st_l_def by auto

  obtain M2 M1 where
    tr_S: ‹get_trail_l S = M2 @ Propagated La C # M1›
    using split_list[OF LaC] by blast
  then obtain M2' M1' where
    tr_T: ‹get_trail T = M2' @ Propagated La (mset (get_clauses_l S ∝ C)) # M1'› and
    M2: ‹(M2, M2') ∈ convert_lits_l (get_clauses_l S) (get_kept_unit_clauses_l S)› and
    M1: ‹(M1, M1') ∈ convert_lits_l (get_clauses_l S) (get_kept_unit_clauses_l S)›
   using conv C0 by (auto simp: list_all2_append1 list_all2_append2 list_all2_Cons1 list_all2_Cons2
    convert_lits_l_def list_rel_def convert_lit.simps dest!: p2relD)
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
    lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)›
    using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      pcdcl_all_struct_invs_def state⇩W_of_def
    by fast+
  then have ‹La ∈# mset (get_clauses_l S ∝ C)› and
    ‹M1' ⊨as CNot (remove1_mset La (mset (get_clauses_l S ∝ C)))›
    using tr_T
    unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
    by (auto 5 5 simp: twl_st twl_st_l)
  then have
    ‹M1 ⊨as CNot (remove1_mset La (mset (get_clauses_l S ∝ C)))›
    using M1 convert_lits_l_true_clss_clss by blast
  then have all_false: ‹-K ∈ lits_of_l (get_trail_l S)›
    if ‹K ∈# remove1_mset La (mset (get_clauses_l S ∝ C))›
    for K
    using that tr_S unfolding true_annots_true_cls_def_iff_negation_in_model
    by (auto dest!: multi_member_split)
  have La0: ‹length (get_clauses_l S ∝ C) > 2 ⟹ La = get_clauses_l S ∝ C ! 0› and
    C: ‹C ∈# dom_m (get_clauses_l S)› and
    ‹La ∈ set (watched_l (get_clauses_l S ∝ C))›
    using list_invs tr_S C0 by (auto simp: twl_list_invs_def all_conj_distrib)
  have n_d: ‹no_dup (get_trail_l S)›
    using ST lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: twl_st_l twl_st)
  show ‹La = L›
  proof (rule ccontr)
    assume ‹¬?thesis›
    then have ‹L ∈# remove1_mset La (mset (get_clauses_l S ∝ C))›
      using LC by auto
    from all_false[OF this] show False
      using L n_d by (auto dest: no_dup_consistentD)
  qed
  then show ‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
    using La0 by simp
qed

lemma remove_one_annot_true_clause_cdcl_twl_restart_l2:
  assumes
    rem: ‹remove_one_annot_true_clause S T› and
    lst_invs: ‹twl_list_invs S› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}› and
    n_d: ‹(S, T') ∈ twl_st_l None› ‹twl_struct_invs T'›
  shows ‹cdcl_twl_restart_l S T›
proof -
  have n_d: ‹no_dup (get_trail_l S)›
    using n_d unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      pcdcl_all_struct_invs_def state⇩W_of_def
    by (auto simp: twl_st twl_st_l)

  show ?thesis
    apply (rule remove_one_annot_true_clause_cdcl_twl_restart_l[OF _ _ ‹(S, T') ∈ twl_st_l None›])
    subgoal using rem .
    subgoal using lst_invs .
    subgoal using ‹twl_struct_invs T'› .
    subgoal using confl .
    subgoal using upd .
    subgoal using n_d .
    done
qed

lemma remove_one_annot_true_clause_get_conflict_l:
  ‹remove_one_annot_true_clause S T ⟹ get_conflict_l T = get_conflict_l S›
  by (auto simp: remove_one_annot_true_clause.simps)

lemma rtranclp_remove_one_annot_true_clause_get_conflict_l:
  ‹remove_one_annot_true_clause⇧*⇧* S T ⟹ get_conflict_l T = get_conflict_l S›
  by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_get_conflict_l)

lemma remove_one_annot_true_clause_clauses_to_update_l:
  ‹remove_one_annot_true_clause S T ⟹ clauses_to_update_l T = clauses_to_update_l S›
  by (auto simp: remove_one_annot_true_clause.simps)

lemma remove_one_annot_true_clause_get_all_mark_of_propagated:
  ‹remove_one_annot_true_clause S T ⟹ set (get_all_mark_of_propagated (get_trail_l T)) ⊆ set (get_all_mark_of_propagated (get_trail_l S)) ∪ {0}›
  by (induction rule: remove_one_annot_true_clause.induct) auto

lemma rtranclp_remove_one_annot_true_clause_get_all_mark_of_propagated:
  ‹remove_one_annot_true_clause⇧*⇧* S T ⟹ set (get_all_mark_of_propagated (get_trail_l T)) ⊆ set (get_all_mark_of_propagated (get_trail_l S)) ∪ {0}›
  by (induction rule: rtranclp_induct)
   (blast dest: remove_one_annot_true_clause_get_all_mark_of_propagated)+

lemma rtranclp_remove_one_annot_true_clause_clauses_to_update_l:
  ‹remove_one_annot_true_clause⇧*⇧* S T ⟹ clauses_to_update_l T = clauses_to_update_l S›
  by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_clauses_to_update_l)

lemma cdcl_twl_restart_l_invs:
  assumes ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and ‹cdcl_twl_restart_l S S'›
  shows ‹∃T'. (S', T') ∈ twl_st_l None ∧ twl_list_invs S' ∧
         clauses_to_update_l S' = {#} ∧ cdcl_twl_restart T T' ∧ twl_struct_invs T'›
  using cdcl_twl_restart_l_cdcl_twl_restart[OF ST list_invs struct_invs]
  cdcl_twl_restart_twl_struct_invs[OF _ struct_invs]
  by (smt RETURN_ref_SPECD RETURN_rule assms(4) in_pair_collect_simp order_trans)


lemma rtranclp_cdcl_twl_restart_l_invs:
  assumes
    ‹cdcl_twl_restart_l⇧*⇧* S S'› and
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    ‹clauses_to_update_l S = {#}›
  shows ‹∃T'. (S', T') ∈ twl_st_l None ∧ twl_list_invs S' ∧
         clauses_to_update_l S' = {#} ∧ cdcl_twl_restart⇧*⇧* T T' ∧ twl_struct_invs T'›
  using assms(1)
  apply (induction rule: rtranclp_induct)
  subgoal
    using assms(2-) apply - by (rule exI[of _ T]) auto
  subgoal for T U
    using cdcl_twl_restart_l_invs[of T _ U] assms
    by (meson rtranclp.rtrancl_into_rtrancl)
  done


lemma rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2:
  assumes
    rem: ‹remove_one_annot_true_clause⇧*⇧* S T› and
    lst_invs: ‹twl_list_invs S› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}› and
    n_d: ‹(S, S') ∈ twl_st_l None› ‹twl_struct_invs S'›
  shows ‹∃T'. cdcl_twl_restart_l⇧*⇧* S T ∧ (T, T') ∈ twl_st_l None ∧ cdcl_twl_restart⇧*⇧* S' T' ∧
    twl_struct_invs T'›
  using rem
proof (induction)
  case base
  then show ?case
    using assms apply - by (rule_tac x=S' in exI) auto
next
  case (step U V) note st = this(1) and step = this(2) and IH = this(3)
  obtain U' where
    IH: ‹cdcl_twl_restart_l⇧*⇧* S U› and
    UT': ‹(U, U') ∈ twl_st_l None› and
    S'U': ‹cdcl_twl_restart⇧*⇧* S' U'›
    using IH by blast
  have ‹twl_list_invs U›
    using rtranclp_cdcl_twl_restart_l_list_invs[OF IH lst_invs] .
  have ‹get_conflict_l U = None›
    using rtranclp_remove_one_annot_true_clause_get_conflict_l[OF st] confl
    by auto
  have ‹clauses_to_update_l U = {#}›
    using rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF st] upd
    by auto
  have ‹twl_struct_invs U'›
      by (metis (no_types, opaque_lifting) ‹cdcl_twl_restart⇧*⇧* S' U'›
          cdcl_twl_restart_twl_struct_invs n_d(2) rtranclp_induct)
  have ‹cdcl_twl_restart_l U V›
    apply (rule remove_one_annot_true_clause_cdcl_twl_restart_l2[of _ _ U'])
    subgoal using step .
    subgoal using ‹twl_list_invs U› .
    subgoal using ‹get_conflict_l U = None› .
    subgoal using ‹clauses_to_update_l U = {#}› .
    subgoal using UT' .
    subgoal using ‹twl_struct_invs U'› .
    done
  moreover obtain V' where
    UT': ‹(V, V') ∈ twl_st_l None› and
    ‹cdcl_twl_restart U' V'› and
    ‹twl_struct_invs V'›
    using cdcl_twl_restart_l_invs[OF UT' _ _  ‹cdcl_twl_restart_l U V›] ‹twl_list_invs U›
      ‹twl_struct_invs U'›
    by blast
  ultimately show ?case
    using S'U' IH by fastforce
qed

definition drop_clause_add_move_init :: ‹'v twl_st_l ⇒ nat ⇒ 'v twl_st_l› where
  ‹drop_clause_add_move_init = (λ(M, N, D, NE0, UE, NS, US, N0, U0, Q, W) C.
     (M, fmdrop C N, D, add_mset (mset (N ∝ C)) NE0, UE, NS, {#}, N0, U0, Q, W))›

lemma [simp]:
  ‹get_trail_l (drop_clause_add_move_init V C) = get_trail_l V›
  by (cases V) (auto simp: drop_clause_add_move_init_def)

definition drop_clause :: ‹'v twl_st_l ⇒ nat ⇒ 'v twl_st_l› where
  ‹drop_clause = (λ(M, N, D, NE0, UE, NS, US, N0, U0, Q, W) C.
     (M, fmdrop C N, D, NE0, UE, NS, {#}, N0, U0, Q, W))›

lemma [simp]:
  ‹get_trail_l (drop_clause V C) = get_trail_l V›
  by (cases V) (auto simp: drop_clause_def)

definition remove_all_annot_true_clause_one_imp
where
‹remove_all_annot_true_clause_one_imp = (λ(C, S). do {
      if C ∈# dom_m (get_clauses_l S) then
        if irred (get_clauses_l S) C
        then RETURN (drop_clause_add_move_init S C)
        else RETURN (drop_clause S C)
      else do {
        RETURN S
      }
  })›

definition remove_one_annot_true_clause_imp_inv where
  ‹remove_one_annot_true_clause_imp_inv S =
    (λ(i, T). remove_one_annot_true_clause⇧*⇧* S T ∧ twl_list_invs S ∧ i ≤ length (get_trail_l S) ∧
      twl_list_invs S ∧
      clauses_to_update_l S = clauses_to_update_l T ∧
      literals_to_update_l S = literals_to_update_l T ∧
      get_conflict_l T = None ∧
      (∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
      get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧
      length (get_trail_l S) = length (get_trail_l T) ∧
      (∀j<i. is_proped (rev (get_trail_l T) ! j) ∧ mark_of (rev (get_trail_l T) ! j) = 0))›



definition remove_one_annot_true_clause_one_imp_pre where
  ‹remove_one_annot_true_clause_one_imp_pre i T ⟷
    (twl_list_invs T ∧ i < length (get_trail_l T) ∧
           twl_list_invs T ∧
           (∃S'. (T, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
           get_conflict_l T = None ∧ clauses_to_update_l T = {#})›

definition replace_annot_l_pre :: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ bool› where
‹replace_annot_l_pre L C S ⟷
   Propagated L C ∈ set (get_trail_l S) ∧ C > 0 ∧
   (∃i. remove_one_annot_true_clause_one_imp_pre i S)›

lemma (in -)[simp]:
  ‹(S, T) ∈ twl_st_l b ⟹ (λx. atm_of (lit_of x)) ` set (get_trail T) = (λx. atm_of (lit_of x)) ` set (get_trail_l S)›
  apply (cases S; cases T; cases b)
  apply (auto simp: twl_st_l_def dest: in_convert_lits_lD)
  apply (metis (mono_tags, lifting) defined_lit_convert_lits_l defined_lit_map rev_image_eqI)
  by (metis (mono_tags, lifting) defined_lit_convert_lits_l defined_lit_map rev_image_eqI)

lemma [twl_st_l,simp]:
  ‹(S, T) ∈ twl_st_l b ⟹ pget_all_init_clss (pstate⇩W_of T) = (get_all_init_clss_l S)›
  by (cases S; cases T; cases b)
   (auto simp: twl_st_l_def mset_take_mset_drop_mset' get_init_clss_l_def)

lemma [twl_st_l,simp]:
  ‹(S, T) ∈ twl_st_l b ⟹ pget_all_learned_clss (pstate⇩W_of T) = (get_all_learned_clss_l S)›
  by (cases S; cases T; cases b)
   (auto simp: twl_st_l_def mset_take_mset_drop_mset' get_learned_clss_l_def)

lemma replace_annot_l_pre_alt_def:
  ‹replace_annot_l_pre L C S ⟷
   (Propagated L C ∈ set (get_trail_l S) ∧ C > 0 ∧
   (∃i. remove_one_annot_true_clause_one_imp_pre i S)) ∧
   L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S +
       get_subsumed_init_clauses_l S + get_init_clauses0_l S)›
   (is ‹?A ⟷ ?B›)
proof -
  have ‹L ∈# all_lits_of_mm (mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S +
       get_subsumed_init_clauses_l S + get_init_clauses0_l S)›
    if pre: ‹replace_annot_l_pre L C S› and LC: ‹Propagated L C ∈ set (get_trail_l S)›
  proof -
    obtain T where
      ST: ‹(S, T) ∈ twl_st_l None› and
      struct: ‹twl_struct_invs T› and
      ‹get_conflict_l S = None›
      using pre unfolding replace_annot_l_pre_def
        remove_one_annot_true_clause_one_imp_pre_def
      by fast
    have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)›
      using struct unfolding twl_struct_invs_def
        cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      pcdcl_all_struct_invs_def state⇩W_of_def
      by fast
   moreover have ‹atm_of L ∈ atms_of_ms (mset ` set_mset (get_init_clss_l S)) ∪
      atms_of_mm (get_unit_init_clauses_l S) ∪
      atms_of_mm (get_subsumed_init_clauses_l S) ∪
      atms_of_mm (get_init_clauses0_l S)›
      using ST LC alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
      by (auto simp: twl_st twl_st_l in_all_lits_of_mm_ain_atms_of_iff
        lits_of_def image_image)
    ultimately show ‹?thesis›
      using ST LC unfolding cdcl⇩W_restart_mset.no_strange_atm_def
      by (auto simp: twl_st twl_st_l in_all_lits_of_mm_ain_atms_of_iff
        lits_of_def image_image get_init_clss_l_def)
  qed
  then show ‹?thesis›
    by (auto simp: replace_annot_l_pre_def)
qed

definition replace_annot_l :: ‹_ ⇒ _ ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
  ‹replace_annot_l L C =
    (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
      ASSERT(replace_annot_l_pre L C (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
      RES {(M', N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)| M'.
       (∃M2 M1 C. M = M2 @ Propagated L C # M1 ∧ M' = M2 @ Propagated L 0 # M1)}
   })›

definition remove_and_add_cls_l :: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
  ‹remove_and_add_cls_l C =
    (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
       ASSERT(C ∈# dom_m N);
        RETURN (M, fmdrop C N, D, NE, UE,
         (if irred N C then add_mset (mset (N∝C)) else id) NEk,
	 (if ¬irred N C then add_mset (mset (N∝C)) else id) UEk, NS, {#}, N0, U0, Q, W)
    })›

text ‹The following progrom removes all clauses that are annotations. However, this is not compatible
with special handling of binary clauses, since we want to make sure that they should not been deleted.
›
definition remove_one_annot_true_clause_one_imp :: ‹nat ⇒ 'v twl_st_l ⇒ (nat × 'v twl_st_l) nres›
where
‹remove_one_annot_true_clause_one_imp = (λi S. do {
      ASSERT(remove_one_annot_true_clause_one_imp_pre i S);
      ASSERT(is_proped ((rev (get_trail_l S))!i));
      (L, C) ← SPEC(λ(L, C). (rev (get_trail_l S))!i = Propagated L C);
      ASSERT(Propagated L C ∈ set (get_trail_l S));
      if C = 0 then RETURN (i+1, S)
      else do {
        ASSERT(C ∈# dom_m (get_clauses_l S));
	S ← replace_annot_l L C S;
	S ← remove_and_add_cls_l C S;
        RETURN (i+1, S)
      }
  })›

definition remove_all_learned_subsumed_clauses :: ‹'v twl_st_l ⇒ ('v twl_st_l) nres› where
‹remove_all_learned_subsumed_clauses = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W).
   RETURN (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W))›


lemma decomp_nth_eq_lit_eq:
  assumes
    ‹M = M2 @ Propagated L C' # M1› and
    ‹rev M ! i = Propagated L C› and
    ‹no_dup M› and
    ‹i < length M›
  shows ‹length M1 = i› and ‹C = C'›
proof -
  have [simp]: ‹defined_lit M1 (lit_of (M1 ! i))› if ‹i < length M1› for i
    using that by (simp add: in_lits_of_l_defined_litD lits_of_def)
  have[simp]: ‹undefined_lit M2 L ⟹
       k < length M2 ⟹
       M2 ! k ≠ Propagated L C› for k
    using defined_lit_def nth_mem by fastforce
  have[simp]: ‹undefined_lit M1 L ⟹
       k < length M1 ⟹
       M1 ! k ≠ Propagated L C› for k
    using defined_lit_def nth_mem by fastforce
  have ‹M ! (length M - Suc i) ∈ set M›
    apply (rule nth_mem)
    using assms by auto
  from split_list[OF this] show ‹length M1 = i› and ‹C = C'›
    using assms
    by (auto simp: nth_append nth_Cons nth_rev split: if_splits nat.splits
      elim!: list_match_lel_lel)
qed

lemma
  assumes ‹remove_one_annot_true_clause_imp_inv S s› and
    s[simp]: ‹s = (i, U)›
  shows
    remove_all_learned_subsumed_clauses_cdcl_twl_restart_l:
      ‹remove_all_learned_subsumed_clauses U ≤ SPEC(λU'. cdcl_twl_restart_l U U' ∧
        get_trail_l U = get_trail_l U')› (is ?A) and
    remove_one_annot_true_clause_imp_inv_no_dupD:
      ‹no_dup (get_trail_l U)› and
    remove_one_annot_true_clause_imp_inv_no_dupD2:
      ‹no_dup (get_trail_l S)›
proof -
  obtain x where
    SU: ‹remove_one_annot_true_clause⇧*⇧* S U› and
    list_invs: ‹twl_list_invs S› and
    ‹i ≤ length (get_trail_l S)› and
    ‹twl_list_invs S› and
    clss_upd_U: ‹clauses_to_update_l S = clauses_to_update_l U› and
    ‹literals_to_update_l S = literals_to_update_l U› and
    conflU: ‹get_conflict_l U = None› and
    conflS: ‹get_conflict_l S = None› and
    Sx: ‹(S, x) ∈ twl_st_l None› and
    struct_invs: ‹twl_struct_invs x› and
    clss_upd_S:  ‹clauses_to_update_l S = {#}› and
    ‹length (get_trail_l S) = length (get_trail_l U)› and
    ‹∀j<i. is_proped (rev (get_trail_l U) ! j) ∧
              mark_of (rev (get_trail_l U) ! j) = 0›
    using assms
    unfolding remove_all_learned_subsumed_clauses_def
      remove_one_annot_true_clause_imp_inv_def prod.case
    by blast
  obtain T' where
    list_invs_U: ‹twl_list_invs U› and
    UT': ‹(U, T') ∈ twl_st_l None› and
    xT': ‹cdcl_twl_restart⇧*⇧* x T'›
    using rtranclp_cdcl_twl_restart_l_list_invs[of S U, OF _ list_invs]
      rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF SU list_invs
        conflS clss_upd_S Sx struct_invs]
    by auto
  have 1: ‹Propagated L E ∈ set (get_trail_l U) ⟹ 0 < E ⟹ E ∈# dom_m (get_clauses_l U)›
    ‹0 ∉# dom_m (get_clauses_l U)› for E L
    using list_invs_U
    unfolding twl_list_invs_def
    by auto
  have ‹twl_struct_invs T'›
    using rtranclp_cdcl_twl_restart_twl_struct_invs struct_invs xT' by blast
  then show ‹no_dup (get_trail_l U)›
    unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def state⇩W_of_def
    using UT' by (simp add: twl_st)
  from no_dup_same_annotD[OF this]
  show ?A
    using clss_upd_U conflU 1 unfolding clss_upd_S
    unfolding remove_all_learned_subsumed_clauses_def
    by (refine_rcg)
      (auto simp: cdcl_twl_restart_l.simps)
   show ‹no_dup (get_trail_l S)›
     using Sx struct_invs
    unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def state⇩W_of_def
    by (simp add: twl_st)
qed

definition remove_one_annot_true_clause_imp :: ‹'v twl_st_l ⇒ ('v twl_st_l) nres›
where
‹remove_one_annot_true_clause_imp = (λS. do {
    k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧
        count_decided M1 = 0 ∧ k = length M1)
      ∨ (count_decided (get_trail_l S) = 0 ∧ k = length (get_trail_l S)));
    start ← SPEC (λi. i ≤ k ∧ (∀j < i. is_proped (rev (get_trail_l S) ! j) ∧ mark_of (rev (get_trail_l S) ! j) = 0));
    (i, T) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_inv S⇖
      (λ(i, S). i < k)
      (λ(i, S). remove_one_annot_true_clause_one_imp i S)
      (start, S);
    ASSERT (remove_one_annot_true_clause_imp_inv S (i, T));
    remove_all_learned_subsumed_clauses T
  })›


lemma remove_one_annot_true_clause_imp_same_length:
   ‹remove_one_annot_true_clause S T ⟹ length (get_trail_l S) = length (get_trail_l T)›
  by (induction rule: remove_one_annot_true_clause.induct) (auto simp: )

lemma rtranclp_remove_one_annot_true_clause_imp_same_length:
  ‹remove_one_annot_true_clause⇧*⇧* S T ⟹ length (get_trail_l S) = length (get_trail_l T)›
  by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_imp_same_length)

lemma remove_one_annot_true_clause_map_is_decided_trail:
  ‹remove_one_annot_true_clause S U ⟹
   map is_decided (get_trail_l S) = map is_decided (get_trail_l U)›
  by (induction rule: remove_one_annot_true_clause.induct)
    auto

lemma remove_one_annot_true_clause_map_mark_of_same_or_0:
  ‹remove_one_annot_true_clause S U ⟹
   mark_of (get_trail_l S ! i) = mark_of (get_trail_l U ! i) ∨ mark_of (get_trail_l U ! i) = 0›
  by (induction rule: remove_one_annot_true_clause.induct)
    (auto simp: nth_append nth_Cons split: nat.split)

lemma remove_one_annot_true_clause_imp_inv_trans:
 ‹remove_one_annot_true_clause_imp_inv S (i, T) ⟹ remove_one_annot_true_clause_imp_inv T U ⟹
  remove_one_annot_true_clause_imp_inv S U›
  using rtranclp_remove_one_annot_true_clause_imp_same_length[of S T]
  by (auto simp: remove_one_annot_true_clause_imp_inv_def)

lemma rtranclp_remove_one_annot_true_clause_map_is_decided_trail:
  ‹remove_one_annot_true_clause⇧*⇧* S U ⟹
   map is_decided (get_trail_l S) = map is_decided (get_trail_l U)›
  by (induction rule: rtranclp_induct)
    (auto simp: remove_one_annot_true_clause_map_is_decided_trail)

lemma rtranclp_remove_one_annot_true_clause_map_mark_of_same_or_0:
  ‹remove_one_annot_true_clause⇧*⇧* S U ⟹
   mark_of (get_trail_l S ! i) = mark_of (get_trail_l U ! i) ∨ mark_of (get_trail_l U ! i) = 0›
  by (induction rule: rtranclp_induct)
    (auto dest!: remove_one_annot_true_clause_map_mark_of_same_or_0)

lemma remove_one_annot_true_clause_map_lit_of_trail:
  ‹remove_one_annot_true_clause S U ⟹
   map lit_of (get_trail_l S) = map lit_of (get_trail_l U)›
  by (induction rule: remove_one_annot_true_clause.induct)
    auto

lemma rtranclp_remove_one_annot_true_clause_map_lit_of_trail:
  ‹remove_one_annot_true_clause⇧*⇧* S U ⟹
   map lit_of (get_trail_l S) = map lit_of (get_trail_l U)›
  by (induction rule: rtranclp_induct)
    (auto simp: remove_one_annot_true_clause_map_lit_of_trail)

lemma remove_one_annot_true_clause_reduce_dom_clauses:
  ‹remove_one_annot_true_clause S U ⟹
   reduce_dom_clauses (get_clauses_l S) (get_clauses_l U)›
  by (induction rule: remove_one_annot_true_clause.induct)
    auto

lemma rtranclp_remove_one_annot_true_clause_reduce_dom_clauses:
  ‹remove_one_annot_true_clause⇧*⇧* S U ⟹
   reduce_dom_clauses (get_clauses_l S) (get_clauses_l U)›
  by (induction rule: rtranclp_induct)
    (auto dest!: remove_one_annot_true_clause_reduce_dom_clauses intro: reduce_dom_clauses_trans)

lemma RETURN_le_RES_no_return:
  ‹f ≤ SPEC (λS. g S ∈ Φ) ⟹ do {S ← f; RETURN (g S)} ≤ RES Φ›
  by (cases f) (auto simp: RES_RETURN_RES)

lemma remove_one_annot_true_clause_one_imp_spec:
  assumes
    I: ‹remove_one_annot_true_clause_imp_inv S iT› and
    cond: ‹case iT of (i, S) ⇒ i < length (get_trail_l S)› and
    iT: ‹iT = (i, T)› and
    proped: ‹is_proped (rev (get_trail_l S) ! i)›
  shows ‹remove_one_annot_true_clause_one_imp i T
         ≤ SPEC  (λs'. remove_one_annot_true_clause_imp_inv S s' ∧
                (s', iT) ∈ measure (λ(i, _). length (get_trail_l S) - i))›
proof -
  obtain M N D NE UE NEk UEk NS US N0 U0 WS Q where
    T: ‹T = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
    by (cases T)

  obtain x where
    ST: ‹remove_one_annot_true_clause⇧*⇧* S T› and
    ‹twl_list_invs S› and
    ‹i ≤ length (get_trail_l S)› and
    ‹twl_list_invs S› and
    ‹(S, x) ∈ twl_st_l None› and
    ‹twl_struct_invs x› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}› and
    level0: ‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
    mark0: ‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
    le: ‹length (get_trail_l S) = length (get_trail_l T)› and
    clss_upd: ‹clauses_to_update_l S = clauses_to_update_l T› and
    lits_upd: ‹literals_to_update_l S = literals_to_update_l T›
    using I unfolding remove_one_annot_true_clause_imp_inv_def iT prod.case by blast
  then have list_invs_T: ‹twl_list_invs T›
    by (meson rtranclp_cdcl_twl_restart_l_list_invs
        rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2)
  obtain x' where
    Tx': ‹(T, x') ∈ twl_st_l None› and
    struct_invs_T: ‹twl_struct_invs x'›
    using ‹(S, x) ∈ twl_st_l None› ‹twl_list_invs S› ‹twl_struct_invs x› confl
     rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2 ST upd by blast
  then have n_d: ‹no_dup (get_trail_l T)›
    unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      pcdcl_all_struct_invs_def state⇩W_of_def
    by (auto simp: twl_st twl_st_l)

  have D: ‹D = None› and WS: ‹WS = {#}›
    using confl upd rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF ST]
    using rtranclp_remove_one_annot_true_clause_get_conflict_l[OF ST] unfolding T by auto
  have lits_of_ST: ‹lits_of_l (get_trail_l S) = lits_of_l (get_trail_l T)›
    using arg_cong[OF rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF ST], of set]
    by (simp add: lits_of_def)

  have rem_one_annot_i_T: ‹remove_one_annot_true_clause_one_imp_pre i T›
    using Tx' struct_invs_T level0 cond list_invs_T D WS
    unfolding remove_one_annot_true_clause_one_imp_pre_def iT T prod.case
    by fastforce
  have
    annot_in_dom: ‹C ∈# dom_m (get_clauses_l T)› (is ?annot)
    if
      ‹case LC of (L, C) ⇒ rev (get_trail_l T) ! i = Propagated L C› and
      ‹LC = (L, C)› and
      ‹¬(C = 0)›
    for LC L C
  proof -
    have ‹rev (get_trail_l T)!i ∈ set (get_trail_l T)›
      using list_invs_T assms le unfolding T
     by (auto simp: twl_list_invs_def rev_nth)
    then show ?annot
      using list_invs_T that le unfolding T
      by (auto simp: twl_list_invs_def simp del: nth_mem)
  qed
  have replace_annot_l:
    ‹replace_annot_l L C T
	≤ SPEC
	   (λSa. do {
		   S ← remove_and_add_cls_l C Sa;
		   RETURN (i + 1, S)
		 } ≤ SPEC
		      (λs'. remove_one_annot_true_clause_imp_inv S s' ∧
			    (s', iT)
			    ∈ measure (λ(i, _). length (get_trail_l S) - i)))›
    if
      rem_one: ‹remove_one_annot_true_clause_one_imp_pre i T› and
      ‹is_proped (rev (get_trail_l T) ! i)› and
      LC_d: ‹case LC of (L, C) ⇒ rev (get_trail_l T) ! i = Propagated L C› and
      LC: ‹LC = (L, C)› and
      LC_T: ‹Propagated L C ∈ set (get_trail_l T)› and
      ‹C ≠ 0› and
      dom: ‹C ∈# dom_m (get_clauses_l T)›
    for LC C L
  proof -
    have ‹i < length M›
      using rem_one unfolding remove_one_annot_true_clause_one_imp_pre_def T by auto

    {
      fix M2 Ca M1
      assume M: ‹M = M2 @ Propagated L Ca # M1› and ‹irred N Ca›
      have n_d: ‹no_dup M›
        using n_d unfolding T by auto
      then have [simp]: ‹Ca = C›
        using LC_T
        by (auto simp: T M dest!: in_set_definedD)
      have ‹Ca > 0›
        using that(6) by auto
      let ?U = ‹(M2 @ Propagated L 0 # M1, fmdrop Ca N, D, NE, {#},
         add_mset (mset (N ∝ Ca)) NEk, UEk, NS, {#}, N0, {#}, WS, Q)›

      have lev: ‹get_level (M2 @ Propagated L C # M1) L = 0› and
        M1: ‹length M1 = i›
        using n_d level0 LC_d decomp_nth_eq_lit_eq(1)[OF M
	   LC_d[unfolded T get_trail_l.simps LC prod.case]
	   n_d ‹i < length M›]
	unfolding M T
      apply (auto simp: count_decided_0_iff nth_append nth_Cons is_decided_no_proped_iff
        in_set_conv_nth rev_nth
       split: if_splits)
       by (metis diff_less gr_implies_not0 linorder_neqE_nat nth_rev_alt rev_nth zero_less_Suc)

      have TU: ‹remove_one_annot_true_clause T ?U›
        unfolding T M
	apply (rule remove_one_annot_true_clause.remove_irred_trail)
	using ‹irred N Ca› ‹Ca > 0› dom lev
	by (auto simp: T M)
      moreover {
	have ‹length (get_trail_l ?U) = length (get_trail_l T)›
	  using TU by (auto simp: remove_one_annot_true_clause.simps T M)
	then have ‹j<i ⟹ is_proped (rev (get_trail_l ?U) ! j)› for j
	  using arg_cong[OF remove_one_annot_true_clause_map_is_decided_trail[OF TU],
	   of ‹λxs. xs ! (length (get_trail_l ?U) - Suc j)›] level0  ‹i < length M›
	  by (auto simp: rev_nth T is_decided_no_proped_iff M
	    nth_append nth_Cons split: nat.splits)
      }
      moreover {
	have ‹length (get_trail_l ?U) = length (get_trail_l T)›
	  using TU by (auto simp: remove_one_annot_true_clause.simps T M)
	then have ‹j<i ⟹ mark_of (rev (get_trail_l ?U) ! j) = 0› for j
	  using remove_one_annot_true_clause_map_mark_of_same_or_0[OF TU,
	    of ‹(length (get_trail_l ?U) - Suc j)›] mark0  ‹i < length M›
	  by (auto simp: rev_nth T is_decided_no_proped_iff M
	    nth_append nth_Cons split: nat.splits)
      }
      moreover have ‹length (get_trail_l S) = length (get_trail_l ?U)›
	using le TU by (auto simp: T M split: if_splits)
      moreover have ‹∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S'›
        by (rule exI[of _ x])
	  (use ‹(S, x) ∈ twl_st_l None› ‹twl_struct_invs x› in blast)
      ultimately have 1: ‹remove_one_annot_true_clause_imp_inv S (Suc i, ?U)›
	using ‹twl_list_invs S› ‹i ≤ length (get_trail_l S)›
	‹(S, x) ∈ twl_st_l None› and
	‹twl_struct_invs x› and
	‹get_conflict_l S = None› and
	‹clauses_to_update_l S = {#}› and
	‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
	‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
	le T clss_upd lits_upd ST TU D M1 ‹i < length M›
	unfolding remove_one_annot_true_clause_imp_inv_def prod.case
	by (auto simp: less_Suc_eq nth_append)
      have 2: ‹length (get_trail_l S) - Suc i < length (get_trail_l S) - i›
        by (simp add: T ‹i < length M› diff_less_mono2 le)
      note 1 2
    }
    moreover {
      fix M2 Ca M1
      assume M: ‹M = M2 @ Propagated L Ca # M1› and ‹¬irred N Ca›
      have n_d: ‹no_dup M›
        using n_d unfolding T by auto
      then have [simp]: ‹Ca = C›
        using LC_T
        by (auto simp: T M dest!: in_set_definedD)
      have ‹Ca > 0›
        using that(6) by auto
      let ?U = ‹(M2 @ Propagated L 0 # M1, fmdrop Ca N, D, NE,
        {#}, NEk, add_mset (mset (N ∝ Ca)) UEk, NS, {#}, N0, {#}, WS, Q)›

      have lev: ‹get_level (M2 @ Propagated L C # M1) L = 0› and
        M1: ‹length M1 = i›
        using n_d level0 LC_d decomp_nth_eq_lit_eq(1)[OF M
	   LC_d[unfolded T get_trail_l.simps LC prod.case]
	   n_d ‹i < length M›]
	unfolding M T
      apply (auto simp: count_decided_0_iff nth_append nth_Cons is_decided_no_proped_iff
        in_set_conv_nth rev_nth
       split: if_splits)
       by (metis diff_less gr_implies_not0 linorder_neqE_nat nth_rev_alt rev_nth zero_less_Suc)

      have TU: ‹remove_one_annot_true_clause T ?U›
        unfolding T M
	apply (rule remove_one_annot_true_clause.remove_red_trail)
	using ‹¬irred N Ca› ‹Ca > 0› dom lev
	by (auto simp: T M)
      moreover {
	have ‹length (get_trail_l ?U) = length (get_trail_l T)›
	  using TU by (auto simp: remove_one_annot_true_clause.simps T M)
	then have ‹j<i ⟹ is_proped (rev (get_trail_l ?U) ! j)› for j
	  using arg_cong[OF remove_one_annot_true_clause_map_is_decided_trail[OF TU],
	   of ‹λxs. xs ! (length (get_trail_l ?U) - Suc j)›] level0  ‹i < length M›
	  by (auto simp: rev_nth T is_decided_no_proped_iff M
	    nth_append nth_Cons split: nat.splits)
      }
      moreover {
	have ‹length (get_trail_l ?U) = length (get_trail_l T)›
	  using TU by (auto simp: remove_one_annot_true_clause.simps T M)
	then have ‹j<i ⟹ mark_of (rev (get_trail_l ?U) ! j) = 0› for j
	  using remove_one_annot_true_clause_map_mark_of_same_or_0[OF TU,
	    of ‹(length (get_trail_l ?U) - Suc j)›] mark0  ‹i < length M›
	  by (auto simp: rev_nth T is_decided_no_proped_iff M
	    nth_append nth_Cons split: nat.splits)
      }
      moreover have ‹length (get_trail_l S) = length (get_trail_l ?U)›
	using le TU by (auto simp: T M split: if_splits)
      moreover have ‹∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S'›
        by (rule exI[of _ x])
	  (use ‹(S, x) ∈ twl_st_l None› ‹twl_struct_invs x› in blast)
      ultimately have 1: ‹remove_one_annot_true_clause_imp_inv S (Suc i, ?U)›
	using ‹twl_list_invs S› ‹i ≤ length (get_trail_l S)›
	‹(S, x) ∈ twl_st_l None› and
	‹twl_struct_invs x› and
	‹get_conflict_l S = None› and
	‹clauses_to_update_l S = {#}› and
	‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
	‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
	le T clss_upd lits_upd ST TU D cond ‹i < length M› M1
	unfolding remove_one_annot_true_clause_imp_inv_def prod.case
	by (auto simp: less_Suc_eq nth_append)
      have 2: ‹length (get_trail_l S) - Suc i < length (get_trail_l S) - i›        by (simp add: T ‹i < length M› diff_less_mono2 le)
      note 1 2
    }
    moreover have ‹C = Ca› if ‹M = M2 @ Propagated L Ca # M1› for M1 M2 Ca
      using LC_T n_d
      by (auto simp: T that dest!: in_set_definedD)
    moreover have ‹replace_annot_l_pre L C (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
      using LC_T that unfolding replace_annot_l_pre_def
      by (auto simp: T)
    ultimately show ?thesis
      using dom cond
      by (auto simp: remove_and_add_cls_l_def
        replace_annot_l_def T iT
	intro!: RETURN_le_RES_no_return ASSERT_leI)
  qed

  have rev_set: ‹rev (get_trail_l T) ! i ∈ set (get_trail_l T)›
    using assms
    by (metis length_rev nth_mem rem_one_annot_i_T
      remove_one_annot_true_clause_one_imp_pre_def set_rev)
  show ?thesis
    unfolding remove_one_annot_true_clause_one_imp_def
    apply refine_vcg
    subgoal using rem_one_annot_i_T unfolding iT T by simp
    subgoal using proped I le
      rtranclp_remove_one_annot_true_clause_map_is_decided_trail[of S T,
        THEN arg_cong, of ‹λxs. (rev xs) ! i›]
      unfolding iT T remove_one_annot_true_clause_imp_inv_def
        remove_one_annot_true_clause_one_imp_pre_def
      by (auto simp add: All_less_Suc rev_map is_decided_no_proped_iff)
    subgoal
      using rev_set unfolding T
      by auto
    subgoal using I le unfolding iT T remove_one_annot_true_clause_imp_inv_def
      remove_one_annot_true_clause_one_imp_pre_def
      by (auto simp add: All_less_Suc)
    subgoal using cond le unfolding iT T remove_one_annot_true_clause_one_imp_pre_def by auto
    subgoal by (rule annot_in_dom)
    subgoal for LC L C
      by (rule replace_annot_l)
    done

qed


lemma remove_one_annot_true_clause_count_dec: ‹remove_one_annot_true_clause S b ⟹
   count_decided (get_trail_l S) = count_decided (get_trail_l b)›
  by (auto simp: remove_one_annot_true_clause.simps)

lemma rtranclp_remove_one_annot_true_clause_count_dec:
  ‹remove_one_annot_true_clause⇧*⇧* S b ⟹
    count_decided (get_trail_l S) = count_decided (get_trail_l b)›
  by (induction rule: rtranclp_induct)
    (auto simp: remove_one_annot_true_clause_count_dec)

lemma valid_trail_reduction_count_dec_ge:
  ‹valid_trail_reduction M M' ⟹
    count_decided M' ≤ count_decided M›
  apply (induction rule: valid_trail_reduction.induct)
  by (auto simp: dest!: get_all_ann_decomposition_exists_prepend
    dest: trail_renumber_count_dec)

lemma (in -)cdcl_twl_restart_l_count_dec:
  ‹cdcl_twl_restart_l S b ⟹
    count_decided (get_trail_l S) ≥ count_decided (get_trail_l b)›
  by (induction rule: cdcl_twl_restart_l.induct)
    (auto simp: remove_one_annot_true_clause_count_dec
    dest: valid_trail_reduction_count_dec_ge)

lemma remove_one_annot_true_clause_imp_spec:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    ‹get_conflict_l S = None› and
    ‹clauses_to_update_l S = {#}›
  shows ‹remove_one_annot_true_clause_imp S ≤ SPEC(λT. cdcl_twl_restart_l S T)›
  unfolding remove_one_annot_true_clause_imp_def
  apply (refine_vcg WHILEIT_rule[where R=‹measure (λ(i, _). length (get_trail_l S) - i)› and
      I=‹remove_one_annot_true_clause_imp_inv S›]
    remove_all_learned_subsumed_clauses_cdcl_twl_restart_l[THEN order_trans])
  subgoal by auto
  subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def prod.simps apply -
    apply (intro conjI)
    apply (solves auto)+
    apply fast+
    done
  apply (rule remove_one_annot_true_clause_one_imp_spec[of _ _ ])
  subgoal unfolding remove_one_annot_true_clause_imp_inv_def by auto
  subgoal unfolding remove_one_annot_true_clause_imp_inv_def by auto
  subgoal
    by (auto dest!: get_all_ann_decomposition_exists_prepend
      simp: count_decided_0_iff rev_nth is_decided_no_proped_iff)
  subgoal
    by (auto dest!: get_all_ann_decomposition_exists_prepend
      simp: count_decided_0_iff rev_nth is_decided_no_proped_iff)
  subgoal by auto
  apply assumption
  apply assumption
  subgoal for x start s a b xa
    using tranclp_cdcl_twl_restart_l_cdcl_is_cdcl_twl_restart_l[of S xa]
      rtranclp_into_tranclp1[of cdcl_twl_restart_l S b xa]
      remove_one_annot_true_clause_imp_inv_no_dupD2[of S s ‹fst s› ‹snd s›]
    by (auto simp: remove_one_annot_true_clause_imp_inv_def
       dest!: rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2)
  done

lemma remove_one_annot_true_clause_imp_spec_lev0:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    ‹get_conflict_l S = None› and
    ‹clauses_to_update_l S = {#}› and
    ‹count_decided (get_trail_l S) = 0›
  shows ‹remove_one_annot_true_clause_imp S ≤ SPEC(λT. cdcl_twl_restart_l S T ∧
     count_decided (get_trail_l T) = 0 ∧ (∀L ∈ set (get_trail_l T). mark_of L = 0) ∧
     length (get_trail_l S) = length (get_trail_l T)) ›
proof -
  have H: ‹∀j<a. is_proped (rev (get_trail_l b) ! j) ∧
          mark_of (rev (get_trail_l b) ! j) = 0 ⟹  ¬ a < length (get_trail_l b) ⟹
      ∀x ∈ set (get_trail_l b). is_proped x ∧ mark_of x = 0› for a b
    apply (rule ballI)
    apply (subst (asm) set_rev[symmetric])
    apply (subst (asm) in_set_conv_nth)
    apply auto
    done
   have K: ‹a < length (get_trail_l b) ⟹ is_decided (get_trail_l b ! a) ⟹
     count_decided (get_trail_l b) ≠ 0› for a b
    using count_decided_0_iff nth_mem by blast
  show ?thesis
    apply (rule SPEC_rule_conjI)
    apply (rule remove_one_annot_true_clause_imp_spec[OF assms(1-5)])
    unfolding remove_one_annot_true_clause_imp_def
    apply (refine_vcg WHILEIT_rule[where
        R=‹measure (λ(i, _::'a twl_st_l). length (get_trail_l S) - i)› and
        I=‹remove_one_annot_true_clause_imp_inv S›]
      remove_one_annot_true_clause_one_imp_spec
      remove_all_learned_subsumed_clauses_cdcl_twl_restart_l[THEN order_trans])
    subgoal by auto
    subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def prod.simps apply - by (intro conjI) ((solves auto)+, fast, (solves auto)+)
    subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def by auto
    subgoal using assms by (auto simp: count_decided_0_iff is_decided_no_proped_iff
      rev_nth)
    subgoal by auto
    apply assumption
    apply assumption
    subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def
      apply (auto simp: rtranclp_remove_one_annot_true_clause_count_dec
        dest: cdcl_twl_restart_l_count_dec)
      done
    subgoal
      using assms(6) unfolding remove_one_annot_true_clause_imp_inv_def
      by (auto dest: H K)
    subgoal
      using assms(6) unfolding remove_one_annot_true_clause_imp_inv_def
      by (auto dest: H K)
  done
qed


definition collect_valid_indices :: ‹_ ⇒ nat list nres› where
  ‹collect_valid_indices S = SPEC (λN. True)›

definition mark_to_delete_clauses_l_inv
  :: ‹'v twl_st_l ⇒ nat list ⇒ nat × 'v twl_st_l × nat list ⇒ bool›
where
  ‹mark_to_delete_clauses_l_inv = (λS xs0 (i, T, xs).
      remove_one_annot_true_clause⇧*⇧* S T ∧
      get_trail_l S = get_trail_l T ∧
      (∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
      twl_list_invs S ∧
      get_conflict_l S = None ∧
      clauses_to_update_l S = {#})›

definition mark_to_delete_clauses_l_pre
  :: ‹'v twl_st_l ⇒ bool›
where
  ‹mark_to_delete_clauses_l_pre S ⟷
   (∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧ twl_list_invs S)›

definition mark_garbage_l:: ‹nat ⇒  'v twl_st_l ⇒ 'v twl_st_l›  where
  ‹mark_garbage_l = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
  (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, WS, Q))›

definition can_delete where
  ‹can_delete S C b = (b ⟶
    (length (get_clauses_l S ∝ C) = 2 ⟶
      (Propagated (get_clauses_l S ∝ C ! 0) C ∉ set (get_trail_l S)) ∧
      (Propagated (get_clauses_l S ∝ C ! 1) C ∉ set (get_trail_l S))) ∧
    (length (get_clauses_l S ∝ C) > 2 ⟶
      (Propagated (get_clauses_l S ∝ C ! 0) C ∉ set (get_trail_l S))) ∧
    ¬irred (get_clauses_l S) C)›

definition mark_to_delete_clauses_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹mark_to_delete_clauses_l  = (λS. do {
    ASSERT(mark_to_delete_clauses_l_pre S);
    xs ← collect_valid_indices S;
    to_keep ← SPEC(λ_::nat. True); ― ‹the minimum number of clauses that should be kept.›
    (_, S, _) ← WHILE⇩T⇗mark_to_delete_clauses_l_inv S xs⇖
      (λ(i, S, xs). i < length xs)
      (λ(i, S, xs). do {
        if(xs!i ∉# dom_m (get_clauses_l S)) then RETURN (i, S, delete_index_and_swap xs i)
        else do {
          ASSERT(0 < length (get_clauses_l S∝(xs!i)));
          ASSERT (xs ! i ≠ 0);
          can_del ← SPEC (can_delete S (xs!i));
          ASSERT(i < length xs);
          if can_del
          then
            RETURN (i, mark_garbage_l (xs!i) S, delete_index_and_swap xs i)
          else
            RETURN (i+1, S, xs)
       }
      })
      (to_keep, S, xs);
    remove_all_learned_subsumed_clauses S
  })›


lemma mark_to_delete_clauses_l_spec:
  assumes
    ST: ‹(S, S') ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs S'› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}›
  shows ‹mark_to_delete_clauses_l S ≤ ⇓ Id (SPEC(λT. remove_one_annot_true_clause⇧+⇧+ S T ∧
    get_trail_l S = get_trail_l T))›
proof -

  define I where
    ‹I (xs :: nat list) ≡ (λ(i :: nat, T, xs :: nat list). remove_one_annot_true_clause⇧*⇧* S T)› for xs

  have mark0: ‹mark_to_delete_clauses_l_pre S›
    using ST list_invs struct_invs unfolding mark_to_delete_clauses_l_pre_def
    by blast
  have I0: ‹I xs (l, S, xs')›
    for xs xs' :: ‹nat list› and l :: nat
  proof -
    show ?thesis
      unfolding I_def
      by auto
  qed
  have mark_to_delete_clauses_l_inv_notin:
    ‹mark_to_delete_clauses_l_inv S xs0 (a, aa, delete_index_and_swap xs' a)›
    if
      ‹mark_to_delete_clauses_l_pre S› and
      ‹xs0 ∈ {N. True}› and
      ‹mark_to_delete_clauses_l_inv S xs0 s› and
      ‹I xs0 s› and
      ‹case s of (i, S, xs) ⇒ i < length xs› and
      ‹aa' = (aa, xs')› and
      ‹s = (a, aa')› and
      ‹ba ! a ∉# dom_m (get_clauses_l aa)›
    for s a aa ba xs0 aa' xs'
  proof -
    show ?thesis
      using that
      unfolding mark_to_delete_clauses_l_inv_def
      by auto
  qed
  have I_notin: ‹I xs0 (a, aa, delete_index_and_swap xs' a)›
    if
      ‹mark_to_delete_clauses_l_pre S› and
      ‹xs0 ∈ {N. True}› and
      ‹mark_to_delete_clauses_l_inv S xs0 s› and
      ‹I xs0 s› and
      ‹case s of (i, S, xs) ⇒ i < length xs› and
      ‹aa' = (aa, xs')› and
      ‹s = (a, aa')› and
      ‹ba ! a ∉# dom_m (get_clauses_l aa)›
    for s a aa ba xs0 aa' xs'
  proof -
    show ?thesis
      using that
      unfolding I_def
      by auto
  qed

  have length_ge0: ‹0 < length (get_clauses_l aa ∝ (xs ! a))›
    if
      inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
      I: ‹I xs0 s› and
      cond: ‹case s of (i, S, xs0) ⇒ i < length xs0› and
      st:
        ‹aa' = (aa, xs)›
        ‹s = (a, aa')› and
      xs: ‹¬ xs ! a ∉# dom_m (get_clauses_l aa)›
    for s a b aa xs0 aa' xs
  proof -
    have
      rem: ‹remove_one_annot_true_clause⇧*⇧* S aa›
      using I unfolding I_def st prod.case by blast+
    then obtain T' where
      T': ‹(aa, T') ∈ twl_st_l None› and
      ‹twl_struct_invs T'›
      using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list_invs confl upd
       ST struct_invs] by blast
    then have ‹Multiset.Ball (get_clauses T') struct_wf_twl_cls›
      unfolding twl_struct_invs_def twl_st_inv_alt_def
      by fast
    then have ‹∀x∈#ran_m (get_clauses_l aa). 2 ≤ length (fst x)›
      using xs T' by (auto simp: twl_st_l)
    then show ?thesis
      using xs by (auto simp: ran_m_def)
  qed

  have mark_to_delete_clauses_l_inv_del:
      ‹mark_to_delete_clauses_l_inv S xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)› and
    I_del: ‹I xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
    if
      ‹mark_to_delete_clauses_l_pre S› and
      ‹xs0 ∈ {N. True}› and
      inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
      I: ‹I xs0 s› and
      i_le: ‹case s of (i, S, xs) ⇒ i < length xs› and
      st: ‹sT = (T, xs)›
         ‹s = (i, sT)› and
      in_dom: ‹¬ xs ! i ∉# dom_m (get_clauses_l T)› and
      ‹0 < length (get_clauses_l T ∝ (xs ! i))› and
      can_del: ‹can_delete T (xs ! i) b› and
      ‹i < length xs› and
      [simp]: ‹b›
     for x s i T b xs0 sT xs
  proof -
    obtain M N D NE UE NEk UEk NS US N0 U0 WS Q where
      S: ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
      by (cases S)
    obtain M' N' D' NE' UE' NEk' UEk' NS' US' N0' U0' WS' Q' where
      T: ‹T = (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', WS', Q')›
      by (cases T)
    have
      rem: ‹remove_one_annot_true_clause⇧*⇧* S T›
      using I unfolding I_def st prod.case by blast+

    obtain V where
      SU: ‹cdcl_twl_restart_l⇧*⇧* S T› and
      UV: ‹(T, V) ∈ twl_st_l None› and
      TV: ‹cdcl_twl_restart⇧*⇧* S' V› and
      struct_invs_V: ‹twl_struct_invs V›
      using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list_invs confl upd
        ST struct_invs]
      by auto
    have list_invs_U': ‹twl_list_invs T›
      using SU list_invs rtranclp_cdcl_twl_restart_l_list_invs by blast

    have ‹xs ! i > 0›
      apply (rule ccontr)
      using in_dom list_invs_U' unfolding twl_list_invs_def by (auto dest: multi_member_split)
    have ‹N' ∝ (xs ! i) ! 0 ∈ lits_of_l M'›
       if ‹Propagated (N' ∝ (xs ! i) ! 0) (xs0 ! i) ∈ set M'›
      using that by (auto dest!: split_list)
    then have not_annot: ‹Propagated Laa (xs ! i) ∈ set M' ⟹ False› for Laa
      using is_annot_iff_annotates_first[OF UV list_invs_U' struct_invs_V ‹xs ! i > 0›]
      is_annot_no_other_true_lit[OF UV list_invs_U' struct_invs_V ‹xs ! i > 0›, of Laa ‹
         N' ∝ (xs !i) ! 0›] can_del
      trail_length_ge2[OF UV list_invs_U' struct_invs_V _ ‹xs ! i > 0›, of Laa]
      unfolding S T can_delete_def
      by (auto dest: no_dup_same_annotD)

    have star: ‹remove_one_annot_true_clause T (mark_garbage_l (xs ! i) T)›
      unfolding st T mark_garbage_l_def prod.simps
      apply (rule remove_one_annot_true_clause.delete)
      subgoal using in_dom i_le unfolding st prod.case T by auto
      subgoal using can_del unfolding T can_delete_def by auto
      subgoal using not_annot unfolding T by auto
      done
    moreover have ‹get_trail_l (mark_garbage_l (xs ! i) T) = get_trail_l T›
      by (cases T) (auto simp: mark_garbage_l_def)
    ultimately show ‹mark_to_delete_clauses_l_inv S xs0
        (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
      using inv apply -
      unfolding mark_to_delete_clauses_l_inv_def prod.simps st
      apply normalize_goal+
      by (intro conjI; (rule_tac x=x in exI)?)
       auto

    show ‹I xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
      using rem star unfolding st I_def by simp
  qed
  have
    mark_to_delete_clauses_l_inv_keep:
      ‹mark_to_delete_clauses_l_inv S xs0 (i + 1, T, xs)› and
    I_keep: ‹I xs0 (i + 1, T, xs)›
    if
      ‹mark_to_delete_clauses_l_pre S› and
      inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
      I: ‹I xs0 s› and
      cond: ‹case s of (i, S, xs) ⇒ i < length xs› and
      st: ‹sT = (T, xs)›
         ‹s = (i, sT)› and
      dom: ‹¬ xs ! i ∉# dom_m (get_clauses_l T)› and
      ‹0 < length (get_clauses_l T ∝ (xs ! i))› and
      ‹can_delete T (xs ! i) b› and
      ‹i < length xs› and
      ‹¬ b›
    for x s i T b xs0 sT xs
  proof -
    show ‹mark_to_delete_clauses_l_inv S xs0 (i + 1, T, xs)›
      using inv
      unfolding mark_to_delete_clauses_l_inv_def prod.simps st
      by fast
    show  ‹I xs0 (i + 1, T, xs)›
      using I unfolding I_def st prod.simps .
  qed
  have remove_all_learned_subsumed_clauses: ‹remove_all_learned_subsumed_clauses aa
        ≤ SPEC
           (λT. remove_one_annot_true_clause⇧+⇧+ S T ∧
                get_trail_l S = get_trail_l T)›
    if
      ‹mark_to_delete_clauses_l_pre S› and
      ‹xs0 ∈ {N. True}› and
      ‹True› and
      ‹mark_to_delete_clauses_l_inv S xs0 s› and
      ‹I xs0 s› and
      ‹¬ (case s of (i, S, xs) ⇒ i < length xs)› and
      ‹s = (a, b)› and
      ‹b = (aa, ba)›
    for x s a b aa ba xs0
  proof -
    have 1: ‹remove_all_learned_subsumed_clauses aa
        ≤ SPEC
           (λT. remove_one_annot_true_clause aa T ∧
                get_trail_l aa = get_trail_l T)›
      unfolding remove_all_learned_subsumed_clauses_def
      by refine_rcg
        (auto intro!: remove_one_annot_true_clause.delete_subsumed)
    show ?thesis
      by (rule 1[THEN order_trans])
        (use that in ‹auto simp: mark_to_delete_clauses_l_inv_def›)
  qed
  show ?thesis
    unfolding mark_to_delete_clauses_l_def collect_valid_indices_def
    apply (rule ASSERT_refine_left)
     apply (rule mark0)
    apply (subst intro_spec_iff)
    apply (intro ballI)
    subgoal for xs0
      apply (refine_vcg
        WHILEIT_rule_stronger_inv[where I'=‹I xs0› and
          R= ‹measure (λ(i :: nat, N, xs0). Suc (length xs0) - i)›])
      subgoal by auto
      subgoal using list_invs confl upd ST struct_invs unfolding mark_to_delete_clauses_l_inv_def
          by (cases S') force
      subgoal by (rule I0)
      subgoal
        by (rule mark_to_delete_clauses_l_inv_notin)
      subgoal
        by (rule I_notin)
      subgoal
        by auto
      subgoal
        by (rule length_ge0)
      subgoal
        apply (auto simp: mark_to_delete_clauses_l_inv_def )
        by (metis gr0I rtranclp_cdcl_twl_restart_l_list_invs
          rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2 twl_list_invs_def)
      subgoal
        by auto
      subgoal ― ‹delete clause›
        by (rule mark_to_delete_clauses_l_inv_del)
      subgoal
        by (rule I_del)
      subgoal
        by auto
      subgoal ― ‹Keep clause›
        by (rule mark_to_delete_clauses_l_inv_keep)
      subgoal
        by (rule I_keep)
      subgoal
        by auto
      subgoal for x s a b aa ba
        by (rule remove_all_learned_subsumed_clauses)
      done
    done
qed

definition GC_clauses :: ‹nat clauses_l ⇒ nat clauses_l ⇒ (nat clauses_l × (nat ⇒ nat option)) nres› where
‹GC_clauses N N' = do {
  xs ← SPEC(λxs. set_mset (dom_m N) ⊆ set xs);
  (N, N', m) ← nfoldli
    xs
    (λ(N, N', m). True)
    (λC (N, N', m).
       if C ∈# dom_m N
       then do {
         C' ← SPEC(λi. i ∉# dom_m N' ∧ i ≠ 0);
	 RETURN (fmdrop C N, fmupd C' (N ∝ C, irred N C) N', m(C ↦ C'))
       }
       else
         RETURN (N, N', m))
    (N, N', (λ_. None));
  RETURN (N', m)
}›


inductive GC_remap
  :: ‹('a, 'b) fmap × ('a ⇒ 'c option) × ('c, 'b) fmap ⇒  ('a, 'b) fmap × ('a ⇒ 'c option) × ('c, 'b) fmap ⇒ bool›
where
remap_cons:
  ‹GC_remap (N, m, new) (fmdrop C N, m(C ↦ C'), fmupd C' (the (fmlookup N C)) new)›
   if ‹C' ∉# dom_m new› and
      ‹C ∈# dom_m N› and
      ‹C ∉ dom m› and
      ‹C' ∉ ran m›

lemma GC_remap_ran_m_old_new:
  ‹GC_remap (old, m, new) (old', m', new')  ⟹ ran_m old + ran_m new = ran_m old' + ran_m new'›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)

lemma GC_remap_init_clss_l_old_new:
  ‹GC_remap (old, m, new) (old', m', new')  ⟹
    init_clss_l old + init_clss_l new = init_clss_l old' + init_clss_l new'›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)

lemma GC_remap_learned_clss_l_old_new:
  ‹GC_remap (old, m, new) (old', m', new')  ⟹
    learned_clss_l old + learned_clss_l new = learned_clss_l old' + learned_clss_l new'›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)

lemma GC_remap_ran_m_remap:
  ‹GC_remap (old, m, new) (old', m', new')  ⟹ C ∈# dom_m old ⟹ C ∉# dom_m old' ⟹
         m' C ≠ None ∧
         fmlookup new' (the (m' C)) = fmlookup old C›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)

lemma GC_remap_ran_m_no_rewrite_map:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ C ∉# dom_m old ⟹ m' C = m C›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)


lemma GC_remap_ran_m_no_rewrite_fmap:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ C ∈# dom_m new ⟹
    C ∈# dom_m new' ∧ fmlookup new C = fmlookup new' C›
  by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)


lemma rtranclp_GC_remap_init_clss_l_old_new:
  ‹GC_remap⇧*⇧* S S' ⟹
    init_clss_l (fst S) + init_clss_l (snd (snd S)) = init_clss_l (fst S') + init_clss_l (snd (snd S'))›
  by (induction rule: rtranclp_induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits
      dest: GC_remap_init_clss_l_old_new)

lemma rtranclp_GC_remap_learned_clss_l_old_new:
  ‹GC_remap⇧*⇧* S S' ⟹
    learned_clss_l (fst S) + learned_clss_l (snd (snd S)) =
      learned_clss_l (fst S') + learned_clss_l (snd (snd S'))›
  by (induction rule: rtranclp_induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits
      dest: GC_remap_learned_clss_l_old_new)

lemma rtranclp_GC_remap_ran_m_no_rewrite_fmap:
  ‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (snd (snd S)) ⟹
    C ∈# dom_m (snd (snd S')) ∧ fmlookup (snd (snd S)) C = fmlookup (snd (snd S')) C›
  by (induction rule: rtranclp_induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_no_rewrite_fmap)

lemma GC_remap_ran_m_no_rewrite:
  ‹GC_remap S S' ⟹ C ∈# dom_m (fst S) ⟹ C ∈# dom_m (fst S') ⟹
         fmlookup (fst S) C = fmlookup (fst S') C›
  by (induction rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom
        distinct_mset_set_mset_remove1_mset
      dest: GC_remap_ran_m_remap)

lemma GC_remap_ran_m_lookup_kept:
  assumes
    ‹GC_remap⇧*⇧* S y› and
    ‹GC_remap y z› and
    ‹C ∈# dom_m (fst S)› and
    ‹C ∈# dom_m (fst z)› and
    ‹C ∉# dom_m (fst y)›
  shows ‹fmlookup (fst S) C = fmlookup (fst z) C›
  using assms by (smt GC_remap.cases fmlookup_drop fst_conv in_dom_m_lookup_iff)

lemma rtranclp_GC_remap_ran_m_no_rewrite:
  ‹GC_remap⇧*⇧*  S S' ⟹ C ∈# dom_m (fst S) ⟹ C ∈# dom_m (fst S') ⟹
    fmlookup (fst S) C = fmlookup (fst S') C›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z
    by (cases ‹C ∈# dom_m (fst y)›)
      (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
        intro: GC_remap_ran_m_lookup_kept)
  done

lemma GC_remap_ran_m_no_lost:
  ‹GC_remap S S' ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
  by (induction rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom distinct_mset_set_mset_remove1_mset
      dest: GC_remap_ran_m_remap)

lemma rtranclp_GC_remap_ran_m_no_lost:
  ‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z
    by (cases ‹C ∈# dom_m (fst y)›)
      (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin
        dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
        intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost)
  done


lemma GC_remap_ran_m_no_new_lost:
  ‹GC_remap S S' ⟹ dom (fst (snd S)) ⊆ set_mset (dom_m (fst S)) ⟹
    dom (fst (snd S')) ⊆ set_mset (dom_m (fst S))›
  by (induction rule: GC_remap.induct)
    (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom
        distinct_mset_set_mset_remove1_mset
      dest: GC_remap_ran_m_remap)

lemma rtranclp_GC_remap_ran_m_no_new_lost:
  ‹GC_remap⇧*⇧* S S' ⟹ dom (fst (snd S)) ⊆ set_mset (dom_m (fst S)) ⟹
    dom (fst (snd S')) ⊆ set_mset (dom_m (fst S))›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z
    using GC_remap_ran_m_no_lost[of y z] GC_remap_ran_m_remap[of ‹fst y› ‹fst (snd y)› ‹snd (snd y)›
      ‹fst z› ‹fst (snd z)› ‹snd (snd z)›] rtranclp_GC_remap_ran_m_no_lost[of x y]
      GC_remap_ran_m_no_rewrite_map[of ‹fst y› ‹fst (snd y)› ‹snd (snd y)›
      ‹fst z› ‹fst (snd z)› ‹snd (snd z)›]
    apply (auto simp flip: in_dom_m_lookup_iff simp del: lookup_None_notin_dom_m)
    apply (smt (verit, best) domIff option.collapse option.discI rtranclp_GC_remap_ran_m_no_lost subset_eq)
    done
  done


lemma rtranclp_GC_remap_map_ran:
  assumes
    ‹GC_remap⇧*⇧* S S'› and
    ‹(the ∘∘ fst) (snd S) `# mset_set (dom (fst (snd S))) = dom_m (snd (snd S))› and
    ‹finite (dom (fst (snd S)))›
  shows ‹finite (dom (fst (snd S'))) ∧
         (the ∘∘ fst) (snd S') `# mset_set (dom (fst (snd S'))) = dom_m (snd (snd S'))›
  using assms
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step y z) note star = this(1) and st = this(2) and IH = this(3) and H = this(4-)
  from st
  show ?case
  proof cases
    case (remap_cons C' new C N m)
    have ‹C ∉ dom m›
      using step remap_cons by auto
   then have [simp]: ‹{#the (if x = C then Some C' else m x). x ∈# mset_set (dom m)#} =
     {#the (m x). x ∈# mset_set (dom m)#}›
    apply (auto intro!: image_mset_cong split: if_splits)
    by (metis empty_iff finite_set_mset_mset_set local.remap_cons(5) mset_set.infinite set_mset_empty)

    show ?thesis
      using step remap_cons
      by (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin
        dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
        intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost dest: )
  qed
qed


lemma rtranclp_GC_remap_ran_m_no_new_map:
  ‹GC_remap⇧*⇧*  S S'  ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z
    by (cases ‹C ∈# dom_m (fst y)›)
      (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
        intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost)
  done

lemma rtranclp_GC_remap_learned_clss_lD:
  ‹GC_remap⇧*⇧* (N, x, m) (N', x', m') ⟹ learned_clss_l N + learned_clss_l m  = learned_clss_l N'  + learned_clss_l m'›
  by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
    (auto dest: GC_remap_learned_clss_l_old_new)

lemma rtranclp_GC_remap_learned_clss_l:
  ‹GC_remap⇧*⇧* (x1a, Map.empty, fmempty) (fmempty, m, x1ad) ⟹ learned_clss_l x1ad = learned_clss_l x1a›
  by (auto dest!: rtranclp_GC_remap_learned_clss_lD[of _ _ _ _ _ _])

lemma remap_cons2:
  assumes
      ‹C' ∉# dom_m new› and
      ‹C ∈# dom_m N› and
      ‹(the ∘∘ fst) (snd (N, m, new)) `# mset_set (dom (fst (snd (N, m, new)))) =
        dom_m (snd (snd (N, m, new)))› and
      ‹⋀x. x ∈# dom_m (fst (N, m, new)) ⟹ x ∉ dom (fst (snd (N, m, new)))› and
      ‹finite (dom m)›
  shows
    ‹GC_remap (N, m, new) (fmdrop C N, m(C ↦ C'), fmupd C' (the (fmlookup N C)) new)›
proof -
  have 3: ‹C ∈ dom m ⟹ False›
    apply (drule mk_disjoint_insert)
    using assms
    apply (auto 5 5 simp: ran_def)
    done

  have 4: ‹False› if C': ‹C' ∈ ran m›
  proof -
    obtain a where a: ‹a ∈ dom m› and [simp]: ‹m a = Some C'›
      using that C' unfolding ran_def
      by auto
    show False
      using mk_disjoint_insert[OF a] assms by (auto simp: union_single_eq_member)
  qed

  show ?thesis
    apply (rule remap_cons)
    apply (rule assms(1))
    apply (rule assms(2))
    apply (use 3 in fast)
    apply (use 4 in fast)
    done
qed


inductive_cases GC_remapE: ‹GC_remap S T›

lemma rtranclp_GC_remap_finite_map:
  ‹GC_remap⇧*⇧*  S S'  ⟹ finite (dom (fst (snd S))) ⟹ finite (dom (fst (snd S')))›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z
    by (auto elim: GC_remapE)
  done


lemma rtranclp_GC_remap_old_dom_map:
  ‹GC_remap⇧*⇧*  R S  ⟹ (⋀x. x ∈# dom_m (fst R) ⟹ x ∉ dom (fst (snd R))) ⟹
       (⋀x. x ∈# dom_m (fst S) ⟹ x ∉ dom (fst (snd S)))›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for y z x
    by (fastforce elim!: GC_remapE simp: distinct_mset_dom distinct_mset_set_mset_remove1_mset)
  done

lemma remap_cons2_rtranclp:
  assumes
      ‹(the ∘∘ fst) (snd R) `# mset_set (dom (fst (snd R))) = dom_m (snd (snd R))› and
      ‹⋀x. x ∈# dom_m (fst R) ⟹ x ∉ dom (fst (snd R))› and
      ‹finite (dom (fst (snd R)))› and
      st: ‹GC_remap⇧*⇧* R S› and
      C': ‹C' ∉# dom_m (snd (snd S))› and
      C: ‹C ∈# dom_m (fst S)›
  shows
    ‹GC_remap⇧*⇧* R (fmdrop C (fst S), (fst (snd S))(C ↦ C'), fmupd C' (the (fmlookup (fst S) C)) (snd (snd S)))›
proof -
  have
    1: ‹(the ∘∘ fst) (snd S) `# mset_set (dom (fst (snd S))) = dom_m (snd (snd S))› and
    2: ‹⋀x. x ∈# dom_m (fst S) ⟹ x ∉ dom (fst (snd S))› and
    3: ‹finite (dom (fst (snd S)))›
      using assms(1) assms(3) assms(4) rtranclp_GC_remap_map_ran apply blast
     apply (meson assms(2) assms(4) rtranclp_GC_remap_old_dom_map)
    using assms(3) assms(4) rtranclp_GC_remap_finite_map by blast
  have 5: ‹GC_remap S
     (fmdrop C (fst S), (fst (snd S))(C ↦ C'), fmupd C' (the (fmlookup (fst S) C)) (snd (snd S)))›
    using remap_cons2[OF C' C, of ‹(fst (snd S))›] 1 2 3 by (cases S) auto
  show ?thesis
    using 5 st by simp
qed

lemma (in -) fmdom_fmrestrict_set: ‹fmdrop xa (fmrestrict_set s N) = fmrestrict_set (s - {xa}) N›
  by (rule fmap_ext_fmdom)
   (auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset)

lemma (in -) GC_clauses_GC_remap:
  ‹GC_clauses N fmempty ≤ SPEC(λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧
    0 ∉# dom_m N'')›
proof -
  let ?remap = ‹(GC_remap)⇧*⇧*  (N, λ_. None, fmempty)›
  note remap = remap_cons2_rtranclp[of ‹(N, λ_. None, fmempty)›, of ‹(a, b, c)› for a b c, simplified]
  define I where
    ‹I a b ≡ (λ(old :: nat clauses_l, new :: nat clauses_l, m :: nat ⇒ nat option).
      ?remap (old, m, new) ∧ 0 ∉# dom_m new ∧
      set_mset (dom_m old) ⊆ set b)›
      for a b :: ‹nat list›
  have I0: ‹set_mset (dom_m N) ⊆ set x ⟹ I [] x (N, fmempty, λ_. None)› for x
    unfolding I_def
    by (auto intro!: fmap_ext_fmdom simp: fset_fmdom_fmrestrict_set fmember.rep_eq
      notin_fset dom_m_def)

  have I_drop: ‹I (l1 @ [xa]) l2
       (fmdrop xa a, fmupd xb (a ∝ xa, irred a xa) aa, ba(xa ↦ xb))›
  if
    ‹set_mset (dom_m N) ⊆ set x› and
    ‹x = l1 @ xa # l2› and
    ‹I l1 (xa # l2) σ› and
    ‹case σ of (N, N', m) ⇒ True› and
    ‹σ = (a, b)› and
    ‹b = (aa, ba)› and
    ‹xa ∈# dom_m a› and
    ‹xb ∉# dom_m aa ∧ xb ≠ 0›
    for x xa l1 l2 σ a b aa ba xb
  proof -
    have ‹insert xa (set l2) - set l1 - {xa} = set l2 - insert xa (set l1)›
      by auto
    have ‹GC_remap⇧*⇧* (N, Map.empty, fmempty)
        (fmdrop xa a, ba(xa ↦ xb), fmupd xb (the (fmlookup a xa)) aa)›
      by (rule remap)
        (use that in ‹auto simp: I_def›)
    then show ?thesis
      using that distinct_mset_dom[of a] distinct_mset_dom[of aa] unfolding I_def prod.simps
      apply (auto dest!: mset_le_subtract[of ‹dom_m _› _ ‹{#xa#}›] simp: mset_set.insert_remove)
      by (metis Diff_empty Diff_insert0 add_mset_remove_trivial finite_set_mset
        finite_set_mset_mset_set insert_subset_eq_iff mset_set.remove set_mset_mset subseteq_remove1)
  qed

  have I_notin: ‹I (l1 @ [xa]) l2 (a, aa, ba)›
    if
      ‹set_mset (dom_m N) ⊆ set x› and
      ‹x = l1 @ xa # l2› and
      ‹I l1 (xa # l2) σ› and
      ‹case σ of (N, N', m) ⇒ True› and
      ‹σ = (a, b)› and
      ‹b = (aa, ba)› and
      ‹xa ∉# dom_m a›
      for x xa l1 l2 σ a b aa ba
  proof -
    show ?thesis
      using that unfolding I_def
      by (auto dest!: multi_member_split)
  qed
  have early_break: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
     if
       ‹set_mset (dom_m N) ⊆ set x› and
       ‹x = l1 @ l2› and
       ‹I l1 l2 σ› and
       ‹¬ (case σ of (N, N', m) ⇒ True)› and
       ‹σ = (a, b)› and
       ‹b = (aa, ba)› and
       ‹(aa, ba) = (x1, x2)›
      for x l1 l2 σ a b aa ba x1 x2
   proof -
     show ?thesis using that by auto
   qed

  have final_rel: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
  if
    ‹set_mset (dom_m N) ⊆ set x› and
    ‹I x [] σ› and
    ‹case σ of (N, N', m) ⇒ True› and
    ‹σ = (a, b)› and
    ‹b = (aa, ba)› and
    ‹(aa, ba) = (x1, x2)›
  proof -
    show ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
      using that
      by (auto simp: I_def)
  qed
  have final_rel: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)› ‹0 ∉# dom_m x1›
    if
      ‹set_mset (dom_m N) ⊆ set x› and
      ‹I x [] σ› and
      ‹case σ of (N, N', m) ⇒ True› and
      ‹σ = (a, b)› and
      ‹b = (aa, ba)› and
      ‹(aa, ba) = (x1, x2)›
    for x σ a b aa ba x1 x2
    using that
    by (auto simp: I_def)
  show ?thesis
    unfolding GC_clauses_def
    apply (refine_vcg nfoldli_rule[where I = I])
    subgoal by (rule I0)
    subgoal by (rule I_drop)
    subgoal by (rule I_notin)
    ― ‹Final properties:›
    subgoal for x l1 l2 σ a b aa ba x1 x2
      by (rule early_break)
    subgoal
      by (auto simp: I_def)
    subgoal
      by (rule final_rel) assumption+
    subgoal
      by (rule final_rel) assumption+
    done
qed

definition cdcl_GC_clauses_pre :: ‹'v twl_st_l ⇒ bool› where
‹cdcl_GC_clauses_pre S ⟷ (
  ∃T. (S, T) ∈ twl_st_l None ∧
    twl_list_invs S ∧ twl_struct_invs T ∧
    get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧
    count_decided (get_trail_l S) = 0 ∧ (∀L∈set (get_trail_l S). mark_of L = 0)
  ) ›

definition cdcl_GC_clauses :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_GC_clauses = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
  ASSERT(cdcl_GC_clauses_pre (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
  b ← SPEC(λb. True);
  if b then do {
    (N', _) ← SPEC (λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧
      0 ∉# dom_m N'');
    RETURN (M, N', D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, WS, Q)
  }
  else RETURN (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, WS, Q)})›

lemma cdcl_GC_clauses_cdcl_twl_restart_l:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}› and
    count_dec: ‹count_decided (get_trail_l S) = 0› and
    mark: ‹∀L∈set (get_trail_l S). mark_of L = 0›
  shows ‹cdcl_GC_clauses S ≤ SPEC (λT. cdcl_twl_restart_l S T ∧
      get_trail_l S = get_trail_l T)›
proof -
  show ?thesis
    unfolding cdcl_GC_clauses_def
    apply refine_vcg
    subgoal using assms unfolding cdcl_GC_clauses_pre_def by blast
    subgoal using confl upd count_dec mark by (auto simp: cdcl_twl_restart_l.simps
        valid_trail_reduction_refl
      dest: rtranclp_GC_remap_init_clss_l_old_new rtranclp_GC_remap_learned_clss_l_old_new
      intro!: exI[of _ ‹{#}›])
    subgoal by simp
    subgoal using confl upd count_dec mark by (auto simp: cdcl_twl_restart_l.simps
        valid_trail_reduction_refl cdcl_GC_clauses_pre_def twl_list_invs_def)
    subgoal by simp
    done
qed

lemma remove_one_annot_true_clause_cdcl_twl_restart_l_spec:
  assumes
    ST: ‹(S, T) ∈ twl_st_l None› and
    list_invs: ‹twl_list_invs S› and
    struct_invs: ‹twl_struct_invs T› and
    confl: ‹get_conflict_l S = None› and
    upd: ‹clauses_to_update_l S = {#}›
  shows ‹SPEC(remove_one_annot_true_clause⇧+⇧+ S) ≤ SPEC(λT. cdcl_twl_restart_l S T)›
proof -
  have ‹cdcl_twl_restart_l S U'›
    if rem: ‹remove_one_annot_true_clause⇧+⇧+ S U'› for U'
  proof -
    have n_d: ‹no_dup (get_trail_l S)›
      using ST struct_invs unfolding twl_struct_invs_def
          cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
          cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
          pcdcl_all_struct_invs_def state⇩W_of_def
      by (simp add: twl_st twl_st_l)
    have subs_U': ‹get_subsumed_learned_clauses_l U' = {#} ∧ get_learned_clauses0_l U' = {#}›
      using rem unfolding tranclp_unfold_end
      by (cases U'; auto simp: remove_one_annot_true_clause.simps)
    have SU': ‹cdcl_twl_restart_l⇧*⇧* S U'›
      using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[of S U' T, OF
        tranclp_into_rtranclp[OF rem] list_invs
        confl upd ST struct_invs]
      apply -
      apply normalize_goal+
      by auto
    moreover have ‹cdcl_twl_restart_l S U'› if ‹S = U'›
      using confl upd rem rtranclp_cdcl_twl_restart_l_no_dup[OF SU'] list_invs
       n_d subs_U'
      unfolding that[symmetric]
      by (cases S)
        (auto simp: cdcl_twl_restart_l.simps twl_list_invs_def
         dest: no_dup_same_annotD)
    ultimately show ‹cdcl_twl_restart_l S U'›
      using tranclp_cdcl_twl_restart_l_cdcl_is_cdcl_twl_restart_l[of S U', OF _ n_d]
      by (meson rtranclpD)
  qed
  then show ?thesis
    by force
qed

definition (in -) restart_abs_l_pre :: ‹'v twl_st_l ⇒ nat ⇒ nat ⇒ bool ⇒ bool› where
  ‹restart_abs_l_pre S last_GC last_Restart brk ⟷
    (∃S'. (S, S') ∈ twl_st_l None ∧ restart_prog_pre S' last_GC last_Restart brk
      ∧ twl_list_invs S ∧ clauses_to_update_l S = {#})›

definition (in -) cdcl_twl_local_restart_l_spec :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
  ‹cdcl_twl_local_restart_l_spec = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q). do {
      ASSERT(∃last_GC last_Restart. restart_abs_l_pre (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
         last_GC last_Restart False);
      (M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
            Q' = {#}) ∨ (M' = M ∧ Q' = Q));
      RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
   })›

definition cdcl_twl_restart_l_prog where
‹cdcl_twl_restart_l_prog S = do {
   cdcl_twl_local_restart_l_spec S
  }›


lemma cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l:
  assumes inv: ‹restart_abs_l_pre S last_GC last_Restart False›
  shows ‹cdcl_twl_local_restart_l_spec S ≤ 
   ⇓  {(S, T). (S, T) ∈ Id ∧ twl_list_invs S}(SPEC (cdcl_twl_restart_only_l S))›
proof -
  obtain T where
    ST: ‹(S, T) ∈ twl_st_l None› and
    struct_invs: ‹twl_struct_invs T› and
    list_invs: ‹twl_list_invs S› and
    upd: ‹clauses_to_update_l S = {#}› and
    stgy_invs: ‹twl_stgy_invs T› and
    confl: ‹get_conflict_l S = None›
    using inv unfolding restart_abs_l_pre_def restart_prog_pre_def
    apply - apply normalize_goal+
    by (auto simp: twl_st_l twl_st)
  have S: ‹S = (get_trail_l S, snd S)›
    by (cases S) auto

  obtain M N D NE UE NEk UEk NS US N0 U0 W Q where
    S: ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)›
    by (cases S)
  have restart: ‹cdcl_twl_restart_only_l S (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q') ∧
    twl_list_invs (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q')› (is ‹?A ∧ ?B›)
    if decomp': ‹(∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
            Q' = {#}) ∨ (M' = M ∧ Q' = Q)›
    for M' K M2 Q'
  proof -
    consider
      (nope) ‹M = M'› and ‹Q' = Q› |
      (decomp) K M2 where ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
        ‹Q' = {#}›
      using decomp' by auto
    then have ?A
    proof cases
      case [simp]: nope
      have valid: ‹valid_trail_reduction M M'›
        by (use valid_trail_reduction.keep_red[of M'] in ‹auto simp: S›)
      have
        S1: ‹S = (M', N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)› and
        S2 : ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q') =
          (M', N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
        using confl upd unfolding S
        by auto
      show ?thesis
        unfolding S[symmetric] S1 S2
        by (rule cdcl_twl_restart_only_l.intros(2))
    next
      case decomp note decomp = this(1) and Q = this(2)
      have valid: ‹valid_trail_reduction M M'›
        by (use valid_trail_reduction.backtrack_red[OF decomp, of M'] in ‹auto simp: S›)
      have
        S1: ‹S = (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)› and
        S2 : ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q') = (M', N, None, NE, UE,
          NEk, UEk, NS, US, N0, U0, {#}, {#})›
        using confl upd unfolding S Q
        by auto

      show ?thesis
        unfolding S[symmetric] S1 S2
        by (rule cdcl_twl_restart_only_l.intros)
         (rule decomp)
    qed
    moreover have ?B
      using decomp' list_invs by (auto simp: twl_list_invs_def S
        dest!: get_all_ann_decomposition_exists_prepend)
    ultimately show ?thesis by fast
  qed
  show ?thesis
    apply (subst S)
    unfolding cdcl_twl_local_restart_l_spec_def prod.case RES_RETURN_RES2 less_eq_nres.simps
      uncurry_def
    apply (rule ASSERT_leI)
    subgoal using assms unfolding S by fast
    apply (rule RES_refine)
    apply clarsimp
    apply (rule restart)
    apply simp
    done
qed

definition (in -) cdcl_twl_local_restart_l_spec0 :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
  ‹cdcl_twl_local_restart_l_spec0 = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q). do {
      ASSERT(∃last_GC last_Restart. restart_abs_l_pre (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)
        last_GC last_Restart False);
      (M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
            Q' = {#} ∧ count_decided M' = 0) ∨ (M' = M ∧ Q' = Q ∧ count_decided M' = 0));
      RETURN (M, N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, W, Q)
   })›


lemma cdcl_twl_local_restart_l_spec0_cdcl_twl_restart_l:
  assumes inv: ‹restart_abs_l_pre S last_GC last_Restart False›
  shows ‹cdcl_twl_local_restart_l_spec0 S ≤ SPEC (λT. cdcl_twl_restart_l S T ∧ count_decided (get_trail_l T) = 0)›
proof -
  obtain T where
    ST: ‹(S, T) ∈ twl_st_l None› and
    struct_invs: ‹twl_struct_invs T› and
    list_invs: ‹twl_list_invs S› and
    upd: ‹clauses_to_update_l S = {#}› and
    stgy_invs: ‹twl_stgy_invs T› and
    confl: ‹get_conflict_l S = None›
    using inv unfolding restart_abs_l_pre_def restart_prog_pre_def
    apply - apply normalize_goal+
    by (auto simp: twl_st_l twl_st)
  have S: ‹S = (get_trail_l S, snd S)›
    by (cases S) auto

  obtain M N D NE UE NEk UEk NS US N0 U0 W Q where
    S: ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q)›
    by (cases S)
  have restart: ‹cdcl_twl_restart_l S (M', N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, W, Q')› (is ?A)
    if decomp': ‹(∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
            Q' = {#}) ∨ (M' = M ∧ Q' = Q)›
    for M' K M2 Q'
  proof -
    consider
      (nope) ‹M = M'› and ‹Q' = Q› |
      (decomp) K M2 where ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
        ‹Q' = {#}›
      using decomp' by auto
    then show ?A
    proof cases
      case [simp]: nope
      have valid: ‹valid_trail_reduction M M'›
        by (use valid_trail_reduction.keep_red[of M'] in ‹auto simp: S›)
      have
        S1: ‹S = (M', N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)› and
        S2 : ‹(M', N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, W, Q') =
        (M', N, None, NE + mset `# {#}, UE + mset `# {#}, NEk + mset `# {#}, UEk + mset `# {#},
           NS, {#}, N0, {#}, {#}, Q)›
        using confl upd unfolding S
        by auto
     have
        ‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
        dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
        annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
           0 < C ⟹
             (C ∈# dom_m (get_clauses_l S) ∧
            L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
            (length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
        ‹distinct_mset (clauses_to_update_l S)›
        using list_invs unfolding twl_list_invs_def S[symmetric] by auto
      have n_d: ‹no_dup M›
        using struct_invs ST unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
          cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def
        by (auto simp: twl_st_l twl_st S)
      have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
        using n_d
        by (auto simp: S twl_list_invs_def
            dest!: split_list[of ‹Propagated L E› M]
            split_list[of ‹Propagated L E'› M]
            dest: no_dup_same_annotD
            elim!: list_match_lel_lel)

      show ?thesis
        unfolding S[symmetric] S1 S2
        apply (rule cdcl_twl_restart_l.intros[where UE' = ‹{#}›])
        subgoal by (auto)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using dom0 unfolding S by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        done
    next
      case decomp note decomp = this(1) and Q = this(2)
      have valid: ‹valid_trail_reduction M M'›
        by (use valid_trail_reduction.backtrack_red[OF decomp, of M'] in ‹auto simp: S›)
      have
        S1: ‹S = (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)› and
        S2 : ‹(M', N, D, NE, UE, NEk, UEk, NS, {#}, N0, {#}, W, Q') =
          (M', N, None, NE + mset `# {#}, UE + mset `# {#},
          NEk + mset `# {#}, UEk + mset `# {#}, NS, {#}, N0, {#}, {#}, {#})›
        using confl upd unfolding S Q
        by auto

     have
        ‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
        dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
        annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
           0 < C ⟹
             (C ∈# dom_m (get_clauses_l S) ∧
            L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
            (length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
        ‹distinct_mset (clauses_to_update_l S)›
        using list_invs unfolding twl_list_invs_def S[symmetric] by auto
      have n_d: ‹no_dup M›
        using struct_invs ST unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
          cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def
        by (auto simp: twl_st_l twl_st S)
      obtain M3 where M: ‹M = M3 @ Decided K # M'›
        using decomp by auto
      have propa_MM: ‹Propagated L E ∈ set M' ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
        using n_d
        by (auto simp: S twl_list_invs_def M
            dest!: split_list[of ‹Propagated L E› M]
            split_list[of ‹Propagated L E'› M]
            dest: no_dup_same_annotD
            elim!: list_match_lel_lel)

      show ?thesis
        unfolding S[symmetric] S1 S2
        apply (rule cdcl_twl_restart_l.intros[where UE' = ‹{#}›])
        subgoal by (rule valid)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using propa_MM annot unfolding S by fastforce
        subgoal using dom0 unfolding S by auto
        subgoal using decomp unfolding S by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        done
    qed
  qed
  show ?thesis
    apply (subst S)
    unfolding cdcl_twl_local_restart_l_spec0_def prod.case RES_RETURN_RES2 less_eq_nres.simps
      uncurry_def
    apply (rule ASSERT_leI)
    subgoal using assms[unfolded S] by fast
    apply clarsimp
    apply (rule conjI)
    apply (rule restart)
    apply auto
    done
qed

definition cdcl_twl_full_restart_l_GC_prog_pre
  :: ‹'v twl_st_l ⇒ bool›
where
  ‹cdcl_twl_full_restart_l_GC_prog_pre S ⟷
   (∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧ twl_list_invs S ∧
    get_conflict T = None ∧ clauses_to_update T = {#} ∧
     cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init ((state⇩W_of T)))›

lemma valid_trail_reduction_lit_of_nth:
  ‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ i < length M ⟹
    lit_of (M ! i) = lit_of (M' ! i)›
  apply (induction rule: valid_trail_reduction.induct)
  subgoal premises p for K M'' M2
    using arg_cong[OF p(2), of length] p(1) arg_cong[OF p(2), of ‹λxs. xs ! i›] p(4)
    by (auto simp: nth_map nth_append nth_Cons split: if_splits
      dest!: get_all_ann_decomposition_exists_prepend)
  subgoal premises p
    using arg_cong[OF p(1), of length] p(3) arg_cong[OF p(1), of ‹λxs. xs ! i›] p(4)
    by (auto simp: nth_map nth_append nth_Cons split: if_splits
      dest!: get_all_ann_decomposition_exists_prepend)
  done

lemma cdcl_twl_restart_l_lit_of_nth:
  ‹cdcl_twl_restart_l S U ⟹ i < length (get_trail_l U) ⟹ is_proped (get_trail_l U ! i) ⟹
    length (get_trail_l S) = length (get_trail_l U) ⟹
    lit_of (get_trail_l S ! i) = lit_of (get_trail_l U ! i)›
  apply (induction rule: cdcl_twl_restart_l.induct)
  subgoal for M M' N N' NE' UE' NE UE Q Q'
    using valid_trail_reduction_length_leD[of M M']
    valid_trail_reduction_lit_of_nth[of M M' i]
    by auto
  done

lemma valid_trail_reduction_is_decided_nth:
  ‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ i < length M ⟹
    is_decided (M ! i) = is_decided (M' ! i)›
  apply (induction rule: valid_trail_reduction.induct)
  subgoal premises p for K M'' M2
    using arg_cong[OF p(2), of length] p(1) arg_cong[OF p(3), of ‹λxs. xs ! i›] p(4)
    by (auto simp: nth_map nth_append nth_Cons split: if_splits
      dest!: get_all_ann_decomposition_exists_prepend)
  subgoal premises p
    using arg_cong[OF p(1), of length] p(3) arg_cong[OF p(2), of ‹λxs. xs ! i›] p(4)
    by (auto simp: nth_map nth_append nth_Cons split: if_splits
      dest!: get_all_ann_decomposition_exists_prepend)
  done

lemma cdcl_twl_restart_l_mark_of_same_or_0:
  ‹cdcl_twl_restart_l S U ⟹ i < length (get_trail_l U) ⟹ is_proped (get_trail_l U ! i) ⟹
    length (get_trail_l S) = length (get_trail_l U) ⟹
     (mark_of (get_trail_l U ! i) > 0 ⟹ mark_of (get_trail_l S ! i) > 0 ⟹
        mset (get_clauses_l S ∝ mark_of (get_trail_l S ! i))
	 = mset (get_clauses_l U ∝ mark_of (get_trail_l U ! i)) ⟹ P) ⟹
    (mark_of (get_trail_l U ! i) = 0 ⟹ P) ⟹ P›
  apply (induction rule: cdcl_twl_restart_l.induct)
  subgoal for M M' N N' NE' UE' NE UE Q Q'
    using valid_trail_reduction_length_leD[of M M']
    valid_trail_reduction_lit_of_nth[of M M' i]
    valid_trail_reduction_is_decided_nth[of M M' i]
    split_list[of ‹M ! i› M, OF nth_mem] split_list[of ‹M' ! i› M', OF nth_mem]
    by (cases ‹M ! i›; cases ‹M' ! i›)
      (force simp: all_conj_distrib)+
  done


end