Theory Watched_Literals_Initialisation

theory Watched_Literals_Initialisation
  imports Watched_Literals_List
begin

chapter ‹Initialisation of Data structure›

type_synonym 'v twl_st_init = ‹'v twl_st  × 'v clauses›


fun get_trail_init :: ‹'v twl_st_init ⇒ ('v, 'v clause) ann_lit list› where
  ‹get_trail_init ((M, _, _, _, _, _, _), _) = M›

fun get_conflict_init :: ‹'v twl_st_init ⇒ 'v cconflict› where
  ‹get_conflict_init ((_, _, _, D, _, _, _, _), _) = D›

fun literals_to_update_init :: ‹'v twl_st_init ⇒ 'v clause› where
  ‹literals_to_update_init ((_, _, _, _, _, _, _, _, _, _, _, Q), _) = Q›

fun get_init_clauses_init :: ‹'v twl_st_init ⇒ 'v twl_cls multiset› where
  ‹get_init_clauses_init ((_, N, _, _, _, _, _, _), _) = N›

fun get_learned_clauses_init :: ‹'v twl_st_init ⇒ 'v twl_cls multiset› where
  ‹get_learned_clauses_init ((_, _, U, _, _, _, _, _), _) = U›

fun get_unit_init_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_unit_init_clauses_init ((_, _, _, _, NE, _, _, _), _) = NE›

fun get_unit_learned_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_unit_learned_clauses_init ((_, _, _, _, _, UE, _, _), _) = UE›

fun get_subsumed_init_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_subsumed_init_clauses_init ((_, _, _, _, _, _, NS, US, _, _), _) = NS›

fun get_subsumed_learned_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_subsumed_learned_clauses_init ((_, _, _, _, _, _, NS, US, _, _), _) = US›

fun get_subsumed_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_subsumed_clauses_init ((_, _, _, _, _, _, NS, US, _, _), _) = NS + US›

fun clauses_to_update_init :: ‹'v twl_st_init ⇒ ('v literal × 'v twl_cls) multiset› where
  ‹clauses_to_update_init ((_, _, _, _, _, _, _, _, _, _, WS, _), _) = WS›

fun other_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹other_clauses_init ((_, _, _, _, _, _, _), OC) = OC›

fun get_init_clauses0_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_init_clauses0_init ((_, _, _, _, _, _, NS, US, N0, U0,_, _), _) = N0›

fun get_learned_clauses0_init :: ‹'v twl_st_init ⇒ 'v clauses› where
  ‹get_learned_clauses0_init ((_, _, _, _, _, _, NS, US, N0, U0,_, _), _) = U0›

fun add_to_init_clauses :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
  ‹add_to_init_clauses C ((M, N, U, D, NE, UE, NS, US, WS, Q), OC) =
      ((M, add_mset (twl_clause_of C) N, U, D, NE, UE, NS, US, WS, Q), OC)›

fun add_to_unit_init_clauses :: ‹'v clause ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
  ‹add_to_unit_init_clauses C ((M, N, U, D, NE, UE, NS, US, WS, Q), OC) =
      ((M, N, U, D, add_mset C NE, UE, NS, US, WS, Q), OC)›

fun set_conflict_init :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
 ‹set_conflict_init C ((M, N, U, _, NE, UE, NS, US, N0, U0, WS, Q), OC) =
       ((M, N, U, Some (mset C), add_mset (mset C) NE, UE, NS, US, N0, U0, {#}, {#}), OC)›

fun propagate_unit_init :: ‹'v literal ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
 ‹propagate_unit_init L ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC) =
       ((Propagated L {#L#} # M, N, U, D, add_mset {#L#} NE, UE, NS, US, N0, U0, WS, add_mset (-L) Q), OC)›

fun add_empty_conflict_init :: ‹'v twl_st_init ⇒ 'v twl_st_init› where
 ‹add_empty_conflict_init ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC) =
       ((M, N, U, Some {#}, NE, UE, NS, US, add_mset {#} N0, U0, WS, {#}), OC)›

fun add_to_clauses_init :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
   ‹add_to_clauses_init C ((M, N, U, D, NE, UE, NS, US, WS, Q), OC) =
        ((M, add_mset (twl_clause_of C) N, U, D, NE, UE, NS, US, WS, Q), OC)›

fun add_to_tautology_init :: ‹'v clause ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
add_to_tautology_init_def[simp del]:
  ‹add_to_tautology_init C ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC) =
    ((M, N, U, D, NE, UE, add_mset (remdups_mset C) NS, US, N0, U0, WS, Q), OC)›

type_synonym 'v twl_st_l_init = ‹'v twl_st_l × 'v clauses›

fun get_trail_l_init :: ‹'v twl_st_l_init ⇒ ('v, nat) ann_lit list› where
  ‹get_trail_l_init ((M, _, _, _, _, _, _), _) = M›

fun get_conflict_l_init :: ‹'v twl_st_l_init ⇒ 'v cconflict› where
  ‹get_conflict_l_init ((_, _, D, _, _, _, _), _) = D›

fun get_unit_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_unit_clauses_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q), _) = NE + NEk + UE + UEk›

fun get_kept_unit_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_kept_unit_clauses_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q), _) = NEk + UEk›

fun get_learned_unit_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_learned_unit_clauses_l_init ((M, N, D, NEk, UEk, NE, UE, WS, Q), _) = UE + UEk›

fun get_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses_l› where
  ‹get_clauses_l_init ((M, N, D, NE, UE, NS, US, WS, Q), _) = N›

fun literals_to_update_l_init :: ‹'v twl_st_l_init ⇒ 'v clause› where
  ‹literals_to_update_l_init ((_, _, _, _, _, NEk, UEk, NS, US, N0, U0, _, Q), _) = Q›

fun clauses_to_update_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses_to_update_l› where
  ‹clauses_to_update_l_init ((_, _, _, _, _, NEk, UEk, NS, US, N0, U0, WS, _), _) = WS›

fun other_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹other_clauses_l_init ((_, _, _, _, _, _, _), OC) = OC›

fun pstate⇩W_of_init :: "'v twl_st_init ⇒ 'v prag_st" where
‹pstate⇩W_of_init ((M, N, U, C, NE, UE, NS, US, N0, U0, Q), OC) =
  (M, clause `# N + OC, clause `# U, C, NE, UE, NS, US, N0, U0)›

fun state⇩W_of_init :: "'v twl_st_init ⇒ 'v cdcl⇩W_restart_mset" where
"state⇩W_of_init (S) = state_of (pstate⇩W_of_init S)"

fun get_subsumed_init_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_subsumed_init_clauses_l_init ((_, _, _, _, _, NEk, UEk, NS, US, _, _), _) = NS›

fun get_subsumed_learned_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_subsumed_learned_clauses_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q), _) = US›

fun get_subsumed_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_subsumed_clauses_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q), _) = NS+US›

fun get_init_clauses0_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_init_clauses0_l_init ((_, _, _, _, _, NEk, UEk, NS, US, N0, U0, _, _), _) = N0›

fun get_learned_clauses0_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_learned_clauses0_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0,WS, Q), _) = U0›

fun get_clauses0_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
  ‹get_clauses0_l_init ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0,WS, Q), _) = N0+U0›


named_theorems twl_st_init ‹Convertion for inital theorems›

lemma [twl_st_init]:
  ‹get_conflict_init (S, QC) = get_conflict S›
  ‹get_trail_init (S, QC) = get_trail S›
  ‹clauses_to_update_init (S, QC) = clauses_to_update S›
  ‹literals_to_update_init (S, QC) = literals_to_update S›
  by (solves ‹cases S; auto›)+

lemma [twl_st_init]:
  ‹clauses_to_update_init (add_to_unit_init_clauses (mset C) T) = clauses_to_update_init T›
  ‹literals_to_update_init (add_to_unit_init_clauses (mset C) T) = literals_to_update_init T›
  ‹get_conflict_init (add_to_unit_init_clauses (mset C) T) = get_conflict_init T›
  apply (cases T; auto simp: twl_st_inv.simps; fail)+
  done
lemma [twl_st_init]:
  ‹twl_st_inv (fst (add_to_unit_init_clauses (mset C) T)) ⟷  twl_st_inv (fst T)›
  ‹valid_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ valid_enqueued (fst T)›
  ‹no_duplicate_queued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ no_duplicate_queued (fst T)›
  ‹distinct_queued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ distinct_queued (fst T)›
  ‹confl_cands_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ confl_cands_enqueued (fst T)›
  ‹propa_cands_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ propa_cands_enqueued (fst T)›
  ‹twl_st_exception_inv (fst (add_to_unit_init_clauses (mset C) T)) ⟷ twl_st_exception_inv (fst T)›
    apply (cases T; auto simp: twl_st_inv.simps; fail)+
  apply (cases ‹get_conflict_init T›; cases T;
      auto simp: twl_st_inv.simps twl_exception_inv.simps; fail)+
  done

lemma [twl_st_init]:
  ‹trail (state⇩W_of_init T) = get_trail_init T›
  ‹get_trail (fst T) = get_trail_init (T)›
  ‹conflicting (state⇩W_of_init T) = get_conflict_init T›
  ‹init_clss (state⇩W_of_init T) = clauses (get_init_clauses_init T) + get_unit_init_clauses_init T +
    get_subsumed_init_clauses_init T + get_init_clauses0_init T + other_clauses_init T›
  ‹learned_clss (state⇩W_of_init T) = clauses (get_learned_clauses_init T) +
     get_unit_learned_clauses_init T + get_subsumed_learned_clauses_init T + get_learned_clauses0_init T›
  ‹conflicting (state⇩W_of (fst T)) = conflicting (state⇩W_of_init T)›
  ‹trail (state⇩W_of (fst T)) = trail (state⇩W_of_init T)›
  ‹clauses_to_update (fst T) = clauses_to_update_init T›
  ‹get_conflict (fst T) =  get_conflict_init T›
  ‹literals_to_update (fst T) = literals_to_update_init T›
  ‹subsumed_learned_clss (fst T) = get_subsumed_learned_clauses_init T›
  by (cases T; auto simp: cdcl⇩W_restart_mset_state; fail)+

definition twl_st_l_init :: ‹('v twl_st_l_init × 'v twl_st_init) set› where
  ‹twl_st_l_init = {(((M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), OC),
      ((M', N', C', NE', UE', NS', US', N0', U0', WS', Q'), OC')).
    (M , M') ∈ convert_lits_l N (NEk+UEk) ∧
    ((N', C', NE', UE', NS', US', N0', U0', WS', Q'), OC') =
      ((twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N,
         C, NE + NEk, UE + UEk, NS, US, N0, U0, {#}, Q), OC)}›

lemma twl_st_l_init_alt_def:
  ‹(S, T) ∈ twl_st_l_init ⟷
    (fst S, fst T) ∈ twl_st_l None ∧ other_clauses_l_init S = other_clauses_init T›
  by (cases S; cases T) (auto simp: twl_st_l_init_def twl_st_l_def)

lemma [twl_st_init]:
  assumes ‹(S, T) ∈ twl_st_l_init›
  shows
   ‹get_conflict_init T = get_conflict_l_init S›
   ‹get_conflict (fst T) = get_conflict_l_init S›
   ‹literals_to_update_init T = literals_to_update_l_init S›
   ‹clauses_to_update_init T = {#}›
   ‹other_clauses_init T = other_clauses_l_init S›
   ‹lits_of_l (get_trail_init T) = lits_of_l (get_trail_l_init S)›
   ‹lit_of `# mset (get_trail_init T) = lit_of `# mset (get_trail_l_init S)›
   by (use assms in ‹solves ‹cases S; auto simp: twl_st_l_init_def››)+

definition twl_struct_invs_init :: ‹'v twl_st_init ⇒ bool› where
  ‹twl_struct_invs_init S ⟷
    (twl_st_inv (fst S) ∧
    valid_enqueued (fst S) ∧
    pcdcl_all_struct_invs (pstate⇩W_of_init S) ∧
    cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of_init S) ∧
    twl_st_exception_inv (fst S) ∧
    no_duplicate_queued (fst S) ∧
    distinct_queued (fst S) ∧
    confl_cands_enqueued (fst S) ∧
    propa_cands_enqueued (fst S) ∧
    (get_conflict_init S ≠ None ⟶ clauses_to_update_init S = {#} ∧ literals_to_update_init S = {#}) ∧
    clauses_to_update_inv (fst S) ∧
    past_invs (fst S))
  ›

lemma state⇩W_of_state⇩W_of_init:
  ‹other_clauses_init W = {#} ⟹ state⇩W_of (fst W) = state⇩W_of_init W›
  by (cases W) auto

lemma twl_struct_invs_init_twl_struct_invs:
  ‹other_clauses_init W = {#} ⟹ twl_struct_invs_init W ⟹ twl_struct_invs (fst W)›
  unfolding twl_struct_invs_def twl_struct_invs_init_def
  apply (subst state⇩W_of_state⇩W_of_init; assumption?)+
  apply (intro iffI impI conjI)
  by (cases W; clarsimp simp: twl_st_init)+

fun add_empty_conflict_init_l :: ‹'v twl_st_l_init ⇒ 'v twl_st_l_init› where
  add_empty_conflict_init_l_def[simp del]:
   ‹add_empty_conflict_init_l ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), OC) =
       ((M, N, Some {#}, NE, UE, NEk, UEk, NS, US, add_mset {#} N0, U0, WS, {#}), OC)›


fun propagate_unit_init_l :: ‹'v literal ⇒ 'v twl_st_l_init ⇒ ('v twl_st_l_init) nres› where
  propagate_unit_init_l_def[simp del]:
   ‹propagate_unit_init_l L ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), OC) = do {
       M ← cons_trail_propagate_l L 0 M;
       RETURN ((M, N, D, NE, UE, add_mset {#L#} NEk, UEk, NS, US, N0, U0, WS, add_mset (-L) Q), OC)
     }›


fun already_propagated_unit_init_l :: ‹'v clause ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
  already_propagated_unit_init_l_def[simp del]:
   ‹already_propagated_unit_init_l C ((M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q), OC) =
       ((M, N, D, NE, UE, add_mset C NEk, UEk, NS, US, WS, Q), OC)›


fun set_conflict_init_l :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
  set_conflict_init_l_def[simp del]:
   ‹set_conflict_init_l C ((M, N, _, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), OC) =
       ((M, N, Some (mset C), add_mset (mset C) NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}), OC)›


fun add_to_clauses_init_l :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
  add_to_clauses_init_l_def[simp del]:
   ‹add_to_clauses_init_l C ((M, N, _, NE, UE, NEk, UEk, NS, US, WS, Q), OC) = do {
        i ← get_fresh_index N;
        RETURN ((M, fmupd i (C, True) N, None, NE, UE, NEk, UEk, NS, US, WS, Q), OC)
    }›

fun add_to_tautology_init_l :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
  add_to_tautology_init_l_def[simp del]:
  ‹add_to_tautology_init_l C ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), OC) =
  ((M, N, D, NE, UE, NEk, UEk, add_mset (remdups_mset (mset C)) NS, US, N0, U0, WS, Q), OC)›

fun add_to_other_init where
  ‹add_to_other_init C (S, OC) = (S, add_mset (remdups_mset (mset C)) OC)›

lemma fst_add_to_other_init [simp]: ‹fst (add_to_other_init a T) = fst T›
  by (cases T) auto

definition remdups_clause where
  ‹remdups_clause C = SPEC (λC'. mset C' = remdups_mset (mset C))›

definition init_dt_step :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
  ‹init_dt_step C S =
  (case get_conflict_l_init S of
    None ⇒ 
      if tautology (mset C)
      then RETURN (add_to_tautology_init_l C S)
      else do {
        C ← remdups_clause C;
        if length C = 0
      then RETURN (add_empty_conflict_init_l S)
      else if length C = 1
      then
        let L = hd C in
        if undefined_lit (get_trail_l_init S) L
        then propagate_unit_init_l L S
        else if L ∈ lits_of_l (get_trail_l_init S)
        then RETURN (already_propagated_unit_init_l (mset C) S)
        else RETURN (set_conflict_init_l C S)
      else 
          add_to_clauses_init_l C S
    }
  | Some D ⇒
      RETURN (add_to_other_init C S))›

definition init_dt :: ‹'v clause_l list ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
  ‹init_dt CS S = nfoldli CS (λ_. True) init_dt_step S›

definition init_dt_pre :: ‹'v clause_l list ⇒ _› where
  ‹init_dt_pre CS SOC ⟷
    (∃T. (SOC, T) ∈ twl_st_l_init ∧
      twl_struct_invs_init T ∧
      clauses_to_update_l_init SOC = {#} ∧
      (∀s∈set (get_trail_l_init SOC). ¬is_decided s) ∧
      (get_conflict_l_init SOC = None ⟶
          literals_to_update_l_init SOC = uminus `# lit_of `# mset (get_trail_l_init SOC)) ∧
      twl_list_invs (fst SOC) ∧
      twl_stgy_invs (fst T) ∧
     (other_clauses_l_init SOC ≠ {#} ⟶ get_conflict_l_init SOC ≠ None) ∧
     (∀C∈#ran_mf (get_clauses_l_init SOC). ¬tautology (mset C)))›

lemma init_dt_pre_ConsD: ‹init_dt_pre (a # CS) SOC ⟹ init_dt_pre CS SOC›
  unfolding init_dt_pre_def
  apply normalize_goal+
  by fastforce

definition init_dt_spec where
  ‹init_dt_spec CS SOC SOC' ⟷
     (∃T'. (SOC', T') ∈ twl_st_l_init ∧
           twl_struct_invs_init T' ∧
           clauses_to_update_l_init SOC' = {#} ∧
           (∀s∈set (get_trail_l_init SOC'). ¬is_decided s) ∧
           (get_conflict_l_init SOC' = None ⟶
              literals_to_update_l_init SOC' = uminus `# lit_of `# mset (get_trail_l_init SOC')) ∧
           (remdups_mset `# mset `# mset CS + mset `# ran_mf (get_clauses_l_init SOC) + other_clauses_l_init SOC +
                 get_unit_clauses_l_init SOC + get_subsumed_init_clauses_l_init SOC+ get_init_clauses0_l_init SOC =
            mset `# ran_mf (get_clauses_l_init SOC') + other_clauses_l_init SOC'  +
                get_unit_clauses_l_init SOC' + get_subsumed_init_clauses_l_init SOC' +
                get_init_clauses0_l_init SOC') ∧
           learned_clss_lf (get_clauses_l_init SOC) = learned_clss_lf (get_clauses_l_init SOC') ∧
           get_learned_unit_clauses_l_init SOC' = get_learned_unit_clauses_l_init SOC ∧
           get_subsumed_learned_clauses_l_init SOC' = get_subsumed_learned_clauses_l_init SOC ∧
           get_learned_clauses0_l_init SOC' = get_learned_clauses0_l_init SOC ∧
           twl_list_invs (fst SOC') ∧
           twl_stgy_invs (fst T') ∧
           (other_clauses_l_init SOC' ≠ {#} ⟶ get_conflict_l_init SOC' ≠ None) ∧
           ({#} ∈# mset `# mset CS ⟶ get_conflict_l_init SOC' ≠ None) ∧
           (get_conflict_l_init SOC ≠ None ⟶ get_conflict_l_init SOC = get_conflict_l_init SOC'))›


lemma twl_struct_invs_init_add_to_other_init:
  assumes
    lev: ‹count_decided (get_trail (fst T)) = 0› and
    invs: ‹twl_struct_invs_init T›
  shows
    ‹twl_struct_invs_init (add_to_other_init a T)›
      (is ?twl_struct_invs_init)
proof -
  let ?a = ‹remdups a›
  obtain M N U D NE UE Q OC WS NS US N0 U0 where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC)›
    by (cases T) auto
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + NS + N0 + OC, clauses U + UE + US + U0, D)› and
    smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + NS + N0 + OC, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by (auto simp: ac_simps)
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset ?a) (clauses N + NE + NS + N0 + OC),
      clauses U + UE + US + U0, D)›
    by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
       clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
       cdcl⇩W_restart_mset.reasons_in_clauses_def)
  then have ‹pcdcl_all_struct_invs (M, add_mset (mset ?a) (clauses N + OC), clauses U, D, NE, UE, NS, US, N0, U0)›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def
    by (auto simp: ac_simps entailed_clss_inv_def psubsumed_invs_def clauses0_inv_def)

  moreover have
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset ?a) (clauses N + NE + NS + N0 + OC),
        clauses U + UE + US + U0, D)›
    using lev smaller
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)
  ultimately show ?twl_struct_invs_init
    using invs
    unfolding twl_struct_invs_init_def T
    unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
    by (clarsimp simp: ac_simps)
qed

lemma clauses_to_update_inv_add_subsumed[simp]:
  ‹clauses_to_update_inv (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  clauses_to_update_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹clauses_to_update_inv (M, N, U, D, NE, UE, NS, add_mset a US, N0, U0, WS, Q) =
  clauses_to_update_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto; fail)+

lemma confl_cands_enqueued_add_subsumed[simp]:
  ‹confl_cands_enqueued (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  confl_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ›
  by (cases D; auto; fail)+

lemma propa_cands_enqueued_add_subsumed[simp]:
  ‹propa_cands_enqueued (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  propa_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ›
  by (cases D; auto; fail)+

lemma twl_exception_inv_add_subsumed[simp]:
  ‹twl_exception_inv (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  twl_exception_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹twl_exception_inv (M, N, U, D, NE, UE, NS, add_mset a US, N0, U0, WS, Q) =
  twl_exception_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto simp: twl_exception_inv.simps; fail)+

lemma past_invs_add_subsumed[simp]:
  ‹past_invs (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹past_invs (M, N, U, D, NE, UE, NS, add_mset a US, N0, U0, WS, Q) =
  past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto simp: past_invs.simps; fail)+

lemma twl_st_inv_add_subsumed[simp]:
  ‹twl_st_inv (M, N, U, D, NE, UE, add_mset a NS, US, N0, U0, WS, Q) =
  twl_st_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  ‹twl_st_inv (M, N, U, D, NE, UE, NS, add_mset a US, N0, U0, WS, Q) =
  twl_st_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
  by (cases D; auto simp: twl_st_inv.simps; fail)+
 
lemma twl_struct_invs_init_add_to_tautology_init:
  assumes
    tauto: ‹tautology a› and
    lev: ‹count_decided (get_trail (fst T)) = 0› and
    invs: ‹twl_struct_invs_init T›
  shows
    ‹twl_struct_invs_init (add_to_tautology_init a T)›
      (is ?twl_struct_invs_init)
proof -
  let ?a = ‹remdups_mset a›
  obtain M N U D NE UE Q OC WS NS US N0 U0 where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC)›
    by (cases T) auto
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + NS + N0 + OC, clauses U + UE + US + U0, D)› and
    smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + NS + N0 + OC, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by (auto simp: ac_simps)
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset ?a (clauses N + NE + NS + N0 + OC),
      clauses U + UE + US + U0, D)›
    by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
       clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
       cdcl⇩W_restart_mset.reasons_in_clauses_def)
  then have ‹pcdcl_all_struct_invs (M, (clauses N + OC), clauses U, D, NE, UE, add_mset ?a NS, US, N0, U0)›
    using invs tauto unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def
    by (auto simp: ac_simps entailed_clss_inv_def psubsumed_invs_def clauses0_inv_def)

  moreover have
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset ?a (clauses N + NE + NS + N0 + OC),
        clauses U + UE + US + U0, D)›
    using lev smaller
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)
  ultimately show ?twl_struct_invs_init
    using invs
    unfolding twl_struct_invs_init_def T
    unfolding fst_conv state⇩W_of_init.simps get_conflict.simps add_to_tautology_init_def
    by (clarsimp simp: ac_simps)
qed

lemma invariants_init_state:
  assumes
    lev: ‹count_decided (get_trail_init T) = 0› and
    wf: ‹∀C ∈# get_clauses (fst T). struct_wf_twl_cls C› and
    MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
    WS: ‹clauses_to_update_init T = {#}› and
    n_d: ‹no_dup (get_trail_init T)›
  shows ‹propa_cands_enqueued (fst T)› and ‹confl_cands_enqueued (fst T)› and ‹twl_st_inv (fst T)›
    ‹clauses_to_update_inv (fst T)› and ‹past_invs (fst T)› and ‹distinct_queued (fst T)› and
    ‹valid_enqueued (fst T)› and ‹twl_st_exception_inv (fst T)› and ‹no_duplicate_queued (fst T)›
proof -
  obtain M N U NE UE OC D NS US N0 U0 where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, {#}, uminus `# lit_of `# mset M), OC)›
    using MQ WS by (cases T) auto
  let ?Q = ‹uminus `# lit_of `# mset M›

  have [iff]: ‹M = M' @ Decided K # Ma ⟷ False› for M' K Ma
    using lev by (auto simp: count_decided_0_iff T)

  have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
    using wf that by (simp add: T twl_st_inv.simps)
  let ?T = ‹fst T›
  have [simp]: ‹propa_cands_enqueued ?T› if D: ‹D = None›
    unfolding propa_cands_enqueued.simps Ball_def T fst_conv D
    apply - apply (intro conjI impI allI)
    subgoal for x C
      using struct[of C]
      apply (case_tac C; auto simp: uminus_lit_swap lits_of_def size_2_iff
          true_annots_true_cls_def_iff_negation_in_model Ball_def remove1_mset_add_mset_If
          all_conj_distrib conj_disj_distribR ex_disj_distrib
          split: if_splits)
      done
    done
  then show ‹propa_cands_enqueued ?T›
    by (cases D) (auto simp: T)

  have [simp]: ‹confl_cands_enqueued ?T› if D: ‹D = None›
    unfolding confl_cands_enqueued.simps Ball_def T D fst_conv
    apply - apply (intro conjI impI allI)
    subgoal for x
      using struct[of x]
      by (case_tac x; case_tac ‹watched x›; auto simp: uminus_lit_swap lits_of_def)
    done
  then show ‹confl_cands_enqueued ?T›
    by (cases D) (auto simp: T)
  have [simp]: ‹get_level M L = 0› for L
    using lev by (auto simp: T count_decided_0_iff)
  show [simp]: ‹twl_st_inv ?T›
    unfolding T fst_conv twl_st_inv.simps Ball_def
    apply - apply (intro conjI impI allI)
    subgoal using wf by (auto simp: T)
    subgoal for C
      by (cases C)
        (auto simp: T twl_st_inv.simps twl_lazy_update.simps twl_is_an_exception_def
          lits_of_def uminus_lit_swap)
    subgoal for C
      using lev by (cases C)
        (auto simp: T twl_st_inv.simps twl_lazy_update.simps)
    done
  have [simp]: ‹{#C ∈# N. clauses_to_update_prop {#- lit_of x. x ∈# mset M#} M (L, C)#} = {#}›
    for L N
    by (auto simp: filter_mset_empty_conv clauses_to_update_prop.simps lits_of_def
        uminus_lit_swap)
  have ‹clauses_to_update_inv ?T› if D: ‹D = None›
    unfolding T D
    by (auto simp: filter_mset_empty_conv lits_of_def uminus_lit_swap)
  then show ‹clauses_to_update_inv (fst T)›
    by (cases D) (auto simp: T)

  show ‹past_invs ?T›
    by (auto simp: T past_invs.simps)

  show ‹distinct_queued ?T›
    using WS n_d by (auto simp: T no_dup_distinct_uminus)
  show ‹valid_enqueued ?T›
    using lev by (auto simp: T lits_of_def)

  show ‹twl_st_exception_inv (fst T)›
    unfolding T fst_conv twl_st_exception_inv.simps Ball_def
    apply - apply (intro conjI impI allI)
    apply (case_tac x; cases D)
    by (auto simp: T twl_exception_inv.simps lits_of_def uminus_lit_swap)

  show ‹no_duplicate_queued (fst T)›
    by (auto simp: T)
qed

lemma twl_struct_invs_init_init_state:
  assumes
    lev: ‹count_decided (get_trail_init T) = 0› and
    wf: ‹∀C ∈# get_clauses (fst T). struct_wf_twl_cls C› and
    MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
    WS: ‹clauses_to_update_init T = {#}› and
    struct_invs: ‹pcdcl_all_struct_invs (pstate⇩W_of_init T)› and
    ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of_init T)› and
    ‹get_conflict_init T ≠ None ⟶ clauses_to_update_init T = {#} ∧ literals_to_update_init T = {#}›
  shows ‹twl_struct_invs_init T›
proof -
  have n_d: ‹no_dup (get_trail_init T)›
    using struct_invs unfolding 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 (cases T) (auto simp: trail.simps)
  then show ?thesis
    using invariants_init_state[OF lev wf MQ WS n_d] assms unfolding twl_struct_invs_init_def
    by fast+
qed


lemma twl_struct_invs_init_add_to_unit_init_clauses:
  assumes
    dist: ‹distinct a› and
    lev: ‹count_decided (get_trail (fst T)) = 0› and
    invs: ‹twl_struct_invs_init T› and
    ex: ‹∃L ∈ set a. L ∈ lits_of_l (get_trail_init T)›
  shows
    ‹twl_struct_invs_init (add_to_unit_init_clauses (mset a) T)›
      (is ?all_struct)
proof -
  have [simp]: ‹remdups_mset (mset a) = mset a›
    using dist by (simp add: mset_set_set remdups_mset_def) 
  obtain M N U D NE UE Q NS US N0 U0 OC WS where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC)›
    by (cases T) auto
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by (auto simp: ac_simps)
  then have [simp]:
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset a) (OC + clauses N + NE + NS + N0),
      clauses U + UE + US + U0, D)›
    using twl_struct_invs_init_add_to_other_init[OF lev invs, of a] dist
    unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def
    by (simp add: ac_simps)
  then have invs': ‹pcdcl_all_struct_invs
                 (M,  clauses N + OC, clauses U, D, add_mset (mset a) NE, UE, NS, US, N0, U0)›
    using invs count_decided_ge_get_level[of M] lev ex unfolding twl_struct_invs_init_def pcdcl_all_struct_invs_def
    by (auto simp: psubsumed_invs_def entailed_clss_inv_def T ac_simps clauses0_inv_def)
  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset a) (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0, D)›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)
  have [simp]: ‹confl_cands_enqueued (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) ⟷
     confl_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    ‹propa_cands_enqueued (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) ⟷
      propa_cands_enqueued (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    ‹twl_st_inv (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) ⟷
        twl_st_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    ‹⋀x.  twl_exception_inv (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) x ⟷
          twl_exception_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) x›
    ‹clauses_to_update_inv (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) ⟷
       clauses_to_update_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    ‹past_invs (M, N, U, D, add_mset (mset a) NE, UE, NS, US, N0, U0, WS, Q) ⟷
        past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    by (cases D; auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+
  show ?all_struct
    using invs ex invs'
    unfolding twl_struct_invs_init_def T
    unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
    by (clarsimp simp del: entailed_clss_inv.simps)
qed


lemma twl_struct_invs_init_set_conflict_init:
  assumes
    dist: ‹distinct C› and
    lev: ‹count_decided (get_trail (fst T)) = 0› and
    invs: ‹twl_struct_invs_init T› and
    ex: ‹∀L ∈ set C. -L ∈ lits_of_l (get_trail_init T)› and
    nempty: ‹C ≠ []› and
    confl: ‹get_conflict_init T = None›
  shows
    ‹twl_struct_invs_init (set_conflict_init C T)›
      (is ?all_struct)
proof -
  obtain M N U D NE UE Q OC WS NS US N0 U0 where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC)›
    by (cases T) auto
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)› and
     pinvs: ‹pcdcl_all_struct_invs (pstate⇩W_of_init ((M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q), OC))›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by auto
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset C) (clauses N + OC+ NE + NS + N0),
        clauses U + UE + US + U0, Some (mset C))›
    using dist ex
    unfolding T twl_struct_invs_init_def
    by (auto 5 5 simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
       clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
       true_annots_true_cls_def_iff_negation_in_model)
  then have H: ‹pcdcl_all_struct_invs (pstate⇩W_of_init ((M, N, U, Some (mset C), add_mset (mset C) NE, UE, NS, US, N0, U0, WS, Q), OC))›
    using pinvs ex count_decided_ge_get_level[of M] lev nempty confl
    unfolding pcdcl_all_struct_invs_def entailed_clss_inv_def psubsumed_invs_def
    by (auto simp: entailed_clss_inv_def T clauses0_inv_def)

  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset C) (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0, Some (mset C))›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)
  let ?T = ‹(M, N, U, Some (mset C), add_mset (mset C) NE, UE, NS, US, N0, U0, {#}, {#})›

  have [simp]: ‹confl_cands_enqueued ?T›
    ‹propa_cands_enqueued ?T›
    ‹twl_st_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟹ twl_st_inv ?T›
    ‹⋀x.  twl_exception_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) x ⟹ twl_exception_inv ?T x›
    ‹clauses_to_update_inv (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟹ clauses_to_update_inv ?T›
    ‹past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟹ past_invs ?T›
    by (auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+

  show ?all_struct
    using invs ex H
    unfolding twl_struct_invs_init_def T
    unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
    by (clarsimp simp del: entailed_clss_inv.simps)
qed

lemma twl_struct_invs_init_propagate_unit_init:
  assumes
    lev: ‹count_decided (get_trail_init T) = 0› and
    invs: ‹twl_struct_invs_init T› and
    undef: ‹undefined_lit (get_trail_init T) L› and
    confl: ‹get_conflict_init T = None› and
    MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
    WS: ‹clauses_to_update_init T = {#}›
  shows
    ‹twl_struct_invs_init (propagate_unit_init L T)›
      (is ?all_struct)
proof -
  obtain M N U NE UE OC WS NS US N0 U0 where
    T: ‹T = ((M, N, U, None, NE, UE, NS, US, N0, U0, WS, uminus `# lit_of `# mset M), OC)›
    using confl MQ by (cases T) auto
  let ?Q = ‹uminus `# lit_of `# mset M›
  have [iff]: ‹- L ∈ lits_of_l M ⟷ False›
    using undef by (auto simp: T Decided_Propagated_in_iff_in_lits_of_l)
  have [simp]: ‹get_all_ann_decomposition M = [([], M)]›
    by (rule no_decision_get_all_ann_decomposition) (use lev in ‹auto simp: T count_decided_0_iff›)
  have H: ‹a @ Propagated L' mark' # b = Propagated L mark # M  ⟷
     (a = [] ∧ L = L' ∧ mark = mark' ∧ b = M) ∨
     (a ≠ [] ∧ hd a = Propagated L mark ∧ tl a @ Propagated L' mark' # b = M)›
    for a mark mark' L' b
    using undef by (cases a) (auto simp: T atm_of_eq_atm_of)
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0,  None)› and
    excep: ‹twl_st_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, WS, ?Q)› and
    st_inv: ‹twl_st_inv (M, N, U, None, NE, UE, NS, US, N0, U0, WS, ?Q)› and
    pinvs: ‹pcdcl_all_struct_invs (pstate⇩W_of_init T)›
    using invs confl unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by auto
  then have [simp]:
    ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset {#L#} (clauses N + OC + NE + NS + N0),
       clauses U + UE + US + U0, None)› and
    n_d: ‹no_dup M›
    by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def T
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
       clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
       cdcl⇩W_restart_mset.reasons_in_clauses_def)
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (Propagated L {#L#} # M,
        add_mset {#L#} (clauses N + OC + NE + NS + N0), clauses U + UE + US + U0, None)›
    using undef by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def T H
        cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
        cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
        cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
        clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
      consistent_interp_insert_iff)
  then have pinvs': ‹pcdcl_all_struct_invs (pstate⇩W_of_init (propagate_unit_init L T))›
    using pinvs lev count_decided_ge_get_level[of ‹Propagated L {#L#} # M›] unfolding pcdcl_all_struct_invs_def T
    by (auto simp: entailed_clss_inv_def psubsumed_invs_def clauses0_inv_def)
  have [iff]: ‹Propagated L {#L#} # M = M' @ Decided K # Ma ⟷ False› for M' K Ma
    using lev by (cases M') (auto simp: count_decided_0_iff T)
  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, None)›
    using invs confl unfolding T twl_struct_invs_init_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (Propagated L {#L#} # M, add_mset {#L#} (clauses N + NE + NS + N0 + OC),
        clauses U + UE + US + U0,  None)›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)

  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N  + OC + NE + NS + N0, clauses U + UE + US + U0, None)›
    using invs confl unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (Propagated L {#L#} # M, add_mset {#L#} (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0, None)›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, WS, ?Q)›
  let ?T = ‹(Propagated L {#L#} # M, N, U, None, add_mset {#L#} NE, UE, NS, US, N0, U0, WS, add_mset (-L) ?Q)›

  have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
    using st_inv that by (simp add: twl_st_inv.simps)
  show ‹twl_struct_invs_init (propagate_unit_init L T)›
    apply (rule twl_struct_invs_init_init_state)
    subgoal using lev by (auto simp: T)
    subgoal using struct by (auto simp: T)
    subgoal using MQ by (auto simp: T)
    subgoal using WS by (auto simp: T)
    subgoal using pinvs' by (simp add: T)
    subgoal by (auto simp: T)
    subgoal by (auto simp: T)
    done
qed

named_theorems twl_st_l_init
lemma [twl_st_l_init]:
  ‹clauses_to_update_l_init (already_propagated_unit_init_l C S) = clauses_to_update_l_init S›
  ‹get_trail_l_init (already_propagated_unit_init_l C S) = get_trail_l_init S›
  ‹get_conflict_l_init (already_propagated_unit_init_l C S) = get_conflict_l_init S›
  ‹other_clauses_l_init (already_propagated_unit_init_l C S) = other_clauses_l_init S›
  ‹clauses_to_update_l_init (already_propagated_unit_init_l C S) = clauses_to_update_l_init S›
  ‹literals_to_update_l_init (already_propagated_unit_init_l C S) = literals_to_update_l_init S›
  ‹get_clauses_l_init (already_propagated_unit_init_l C S) = get_clauses_l_init S›
  ‹get_unit_clauses_l_init (already_propagated_unit_init_l C S) = add_mset C (get_unit_clauses_l_init S)›
  ‹get_learned_unit_clauses_l_init (already_propagated_unit_init_l C S) =
       get_learned_unit_clauses_l_init S›
  ‹get_subsumed_learned_clauses_l_init (already_propagated_unit_init_l C S) =
       get_subsumed_learned_clauses_l_init S›
  ‹get_subsumed_init_clauses_l_init (already_propagated_unit_init_l C S) =
       get_subsumed_init_clauses_l_init S›
  ‹get_learned_clauses0_l_init (already_propagated_unit_init_l C S) =  get_learned_clauses0_l_init S›
  ‹get_init_clauses0_l_init (already_propagated_unit_init_l C S) =  get_init_clauses0_l_init S›
  ‹get_conflict_l_init (T, OC) = get_conflict_l T›
  by (solves ‹cases S; cases T; auto simp: already_propagated_unit_init_l_def›)+


lemma [twl_st_l_init]:
  ‹clauses_to_update_l_init (add_to_tautology_init_l C S) = clauses_to_update_l_init S›
  ‹get_trail_l_init (add_to_tautology_init_l C S) = get_trail_l_init S›
  ‹get_conflict_l_init (add_to_tautology_init_l C S) = get_conflict_l_init S›
  ‹other_clauses_l_init (add_to_tautology_init_l C S) = other_clauses_l_init S›
  ‹clauses_to_update_l_init (add_to_tautology_init_l C S) = clauses_to_update_l_init S›
  ‹literals_to_update_l_init (add_to_tautology_init_l C S) = literals_to_update_l_init S›
  ‹get_clauses_l_init (add_to_tautology_init_l C S) = get_clauses_l_init S›
  ‹get_unit_clauses_l_init (add_to_tautology_init_l C S) = (get_unit_clauses_l_init S)›
  ‹get_learned_unit_clauses_l_init (add_to_tautology_init_l C S) =
       get_learned_unit_clauses_l_init S›
  ‹get_subsumed_learned_clauses_l_init (add_to_tautology_init_l C S) =
       get_subsumed_learned_clauses_l_init S›
  ‹get_subsumed_init_clauses_l_init (add_to_tautology_init_l C S) =
     add_mset (remdups_mset (mset C)) (get_subsumed_init_clauses_l_init S)›
  ‹get_learned_clauses0_l_init (add_to_tautology_init_l C S) =  get_learned_clauses0_l_init S›
  ‹get_init_clauses0_l_init (add_to_tautology_init_l C S) =  get_init_clauses0_l_init S›
  by (solves ‹cases S; auto simp: add_to_tautology_init_l_def›)+

lemma [twl_st_l_init]:
  ‹(V, W) ∈ twl_st_l_init ⟹
    count_decided (get_trail_init W) = count_decided (get_trail_l_init V)›
  by (auto simp: twl_st_l_init_def)

lemma [twl_st_l_init]:
  ‹(V, W) ∈ twl_st_l_init ⟹get_subsumed_learned_clauses_init W = get_subsumed_learned_clauses_l_init V›
  by (cases V, cases W, auto simp: twl_st_l_init_def)

lemma [twl_st_l_init]:
  ‹get_conflict_l (fst T) =  get_conflict_l_init T›
  ‹literals_to_update_l (fst T) = literals_to_update_l_init T›
  ‹clauses_to_update_l (fst T) = clauses_to_update_l_init T›
  ‹get_subsumed_learned_clauses_l (fst T) = get_subsumed_learned_clauses_l_init T›
  ‹get_subsumed_init_clauses_l (fst T) = get_subsumed_init_clauses_l_init T›
  ‹get_subsumed_clauses_l (fst T) = get_subsumed_clauses_l_init T›
  ‹get_conflict_l (fst T) = get_conflict_l_init T›
  by (cases T; auto; fail)+

lemma entailed_clss_inv_add_to_unit_init_clauses:
  ‹count_decided (get_trail_init T) = 0 ⟹ C ≠ [] ⟹ hd C ∈ lits_of_l (get_trail_init T) ⟹
     entailed_clss_inv (pstate⇩W_of_init T) ⟹ entailed_clss_inv (pstate⇩W_of_init  (add_to_unit_init_clauses (mset C) T))›
  using count_decided_ge_get_level[of ‹get_trail_init T›]
  by (cases T; cases C; auto simp: twl_st_inv.simps twl_exception_inv.simps entailed_clss_inv_def)

lemma convert_lits_l_no_decision_iff: ‹(S, T) ∈ convert_lits_l M N ⟹
        (∀s∈set T. ¬ is_decided s) ⟷
        (∀s∈set S. ¬ is_decided s)›
  unfolding convert_lits_l_def
  by (induction rule: list_rel_induct)
    (auto simp: dest!: p2relD)

lemma twl_st_l_init_no_decision_iff:
   ‹(S, T) ∈ twl_st_l_init ⟹
        (∀s∈set (get_trail_init T). ¬ is_decided s) ⟷
        (∀s∈set (get_trail_l_init S). ¬ is_decided s)›
  by (subst convert_lits_l_no_decision_iff[of _ _ ‹get_clauses_l_init S›
        ‹get_kept_unit_clauses_l_init S›])
    (auto simp: twl_st_l_init_def)

lemma twl_st_l_init_defined_lit[twl_st_l_init]:
   ‹(S, T) ∈ twl_st_l_init ⟹
        defined_lit (get_trail_init T) = defined_lit (get_trail_l_init S)›
  by (auto simp: twl_st_l_init_def)

lemma [twl_st_l_init]:
  ‹(S, T) ∈ twl_st_l_init ⟹ get_learned_clauses_init T = {#} ⟷ learned_clss_l (get_clauses_l_init S) = {#}›
  ‹(S, T) ∈ twl_st_l_init ⟹ get_unit_learned_clauses_init T = {#} ⟷ get_learned_unit_clauses_l_init S = {#}
    ›
  by (cases S; cases T; auto simp: twl_st_l_init_def; fail)+


lemma init_dt_pre_already_propagated_unit_init_l:
  assumes
    hd_C: ‹hd C ∈ lits_of_l (get_trail_l_init S)› and
    pre: ‹init_dt_pre CS S› and
    nempty: ‹C ≠ []› and
    dist_C: ‹distinct C› and
    lev: ‹count_decided (get_trail_l_init S) = 0› and
    C': ‹mset (remdups C') = mset C›
  shows
    ‹init_dt_pre CS (already_propagated_unit_init_l (mset C) S)› (is ?pre) and
    ‹init_dt_spec [C'] S (already_propagated_unit_init_l (mset C) S)›  (is ?spec)
proof -
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None› and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init S). ¬ tautology (mset C)›
    using pre unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by presburger
  obtain M N D NE UE NEk UEk Q U OC NS US N0 U0 where
    S: ‹S = ((M, N, U, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)›
    by (cases S) auto
  have [simp]: ‹twl_list_invs (fst (already_propagated_unit_init_l (mset C) S))›
    using add_inv by (auto simp:  already_propagated_unit_init_l_def S
        twl_list_invs_def)
  have [simp]: ‹(already_propagated_unit_init_l (mset C) S, add_to_unit_init_clauses (mset C) T)
        ∈ twl_st_l_init›
    using SOC_T by (cases S)
      (auto simp: twl_st_l_init_def already_propagated_unit_init_l_def
        convert_lits_l_extend_mono)
  have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
    using SOC_T dec by (subst twl_st_l_init_no_decision_iff)
  have [simp]: ‹twl_stgy_invs (fst (add_to_unit_init_clauses (mset C) T))›
    using stgy_inv dec' unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
       cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
    by (cases T)
       (auto simp: cdcl⇩W_restart_mset_state clauses_def)
  note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
  have [simp]: ‹twl_struct_invs_init (add_to_unit_init_clauses (mset C) T)›
    apply (rule twl_struct_invs_init_add_to_unit_init_clauses)
    using inv hd_C nempty dist_C lev SOC_T dec'
    by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff intro: bexI[of _ ‹hd C›])
  show ?pre
    unfolding init_dt_pre_def
    apply (rule exI[of _ ‹add_to_unit_init_clauses (mset C) T›])
    using WS dec in_literals_to_update OC'_empty tauto by (auto simp: twl_st_init twl_st_l_init)
  show ?spec
    unfolding init_dt_spec_def
    apply (rule exI[of _ ‹add_to_unit_init_clauses (mset C) T›])
    using WS dec in_literals_to_update OC'_empty nempty dist_C C'
    by (auto simp: twl_st_init twl_st_l_init; fail)+
qed


lemma init_dt_pre_add_to_tautology_init_l:
  assumes
    pre: ‹init_dt_pre CS S› and
    tautology: ‹tautology (mset C)› and
    lev: ‹count_decided (get_trail_l_init S) = 0›
  shows
    ‹init_dt_pre CS (add_to_tautology_init_l C S)› (is ?pre) and
    ‹init_dt_spec [C] S (add_to_tautology_init_l C S)›  (is ?spec)
proof -
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init S). ¬ tautology (mset C)›
    using pre unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by presburger
  obtain M N D NE UE NEk UEk Q U OC NS US N0 U0 where
    S: ‹S = ((M, N, U, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)›
    by (cases S) auto
  let ?S = ‹add_to_tautology_init_l C S›
  have [simp]: ‹twl_list_invs (fst ?S)›
    using add_inv by (auto simp: add_to_tautology_init_l_def S
        twl_list_invs_def)
  have [simp]: ‹(add_to_tautology_init_l C S, add_to_tautology_init (mset C) T)
        ∈ twl_st_l_init›
    using SOC_T by (cases S)
      (auto simp: twl_st_l_init_def add_to_tautology_init_l_def add_to_tautology_init_def
        convert_lits_l_extend_mono)
  have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
    using SOC_T dec by (subst twl_st_l_init_no_decision_iff)
  have [simp]: ‹twl_stgy_invs (fst (add_to_tautology_init (mset C) T))›
    using stgy_inv dec' unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
       cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
    by (cases T)
      (auto simp: cdcl⇩W_restart_mset_state clauses_def add_to_tautology_init_def)
  note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
  have [simp]: ‹twl_struct_invs_init (add_to_tautology_init (mset C) T)›
    apply (rule twl_struct_invs_init_add_to_tautology_init)
    using inv tautology lev SOC_T dec'
    by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff intro: bexI[of _ ‹hd C›])
  show ?pre
    unfolding init_dt_pre_def
    apply (rule exI[of _ ‹add_to_tautology_init (mset C) T›])
    using WS dec in_literals_to_update OC'_empty tauto by (auto simp: twl_st_init twl_st_l_init)
  show ?spec
    unfolding init_dt_spec_def
    apply (rule exI[of _ ‹add_to_tautology_init (mset C) T›])
    using WS dec in_literals_to_update OC'_empty tautology
    by (auto simp: twl_st_init twl_st_l_init; fail)+
qed

lemma (in -) twl_stgy_invs_backtrack_lvl_0:
  ‹count_decided (get_trail T) = 0 ⟹ twl_stgy_invs T›
  using count_decided_ge_get_level[of ‹get_trail T›]
  by (cases T)
    (auto simp: twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
      cdcl⇩W_restart_mset.no_smaller_confl_def cdcl⇩W_restart_mset_state
      cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)

lemma init_dt_pre_propagate_unit_init:
  assumes
    hd_C: ‹undefined_lit (get_trail_l_init S) L› and
    pre: ‹init_dt_pre CS S› and
    lev: ‹count_decided (get_trail_l_init S) = 0› and
    confl: ‹get_conflict_l_init S = None› and
    C': ‹remdups C' = [L]›
  shows
    ‹propagate_unit_init_l L S ≤ SPEC(init_dt_pre CS)› (is ?pre) and
    ‹propagate_unit_init_l L S ≤ SPEC(init_dt_spec [C'] S)› (is ?spec)
proof -
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
    using pre unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by presburger
  obtain M N D NE UE NEk UEk Q U OC NS US N0 U0 where
    S: ‹S = ((M, N, U, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)›
    by (cases S) auto
  have 1: ‹propagate_unit_init_l L S ≤ SPEC( λS'. (S', propagate_unit_init L T)
        ∈ twl_st_l_init)›
    using SOC_T assms by (auto simp: twl_st_l_init_def propagate_unit_init_l_def
        convert_lit.simps cons_trail_propagate_l_def S convert_lits_l_extend_mono
        intro!: ASSERT_refine_right ASSERT_leI)
  have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
    using SOC_T dec by (subst twl_st_l_init_no_decision_iff)
  have [simp]: ‹twl_stgy_invs (fst (propagate_unit_init L T))›
    apply (rule twl_stgy_invs_backtrack_lvl_0)
    using lev SOC_T
    by (cases S) (auto simp: cdcl⇩W_restart_mset_state clauses_def twl_st_l_init_def)
  note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
  have 2: ‹twl_struct_invs_init (propagate_unit_init L T)›
    apply (rule twl_struct_invs_init_propagate_unit_init)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff uminus_lit_of_image_mset)
    subgoal
      using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
      by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff uminus_lit_of_image_mset)
    done
  have 3: ‹propagate_unit_init_l L S ≤ SPEC(λS. twl_list_invs (fst (S)))›
    using add_inv assms
    by (auto simp: S twl_list_invs_def propagate_unit_init_l_def cons_trail_propagate_l_def
       intro!: ASSERT_leI)
  show ?pre
    using assms 3 2 1
    unfolding init_dt_pre_def cons_trail_propagate_l_def
    propagate_unit_init_l_def S
    apply (simp only: S get_trail_l_init.simps not_False_eq_True assert.ASSERT_simps
      nres_monad3 nres_monad1 nres_order_simps mem_Collect_eq)
    apply (rule exI[of _ ‹propagate_unit_init L T›])
    using WS dec in_literals_to_update OC'_empty confl
    by (auto simp: twl_st_init twl_st_l_init)
  show ?spec
    using assms 1 2 3
    unfolding init_dt_spec_def cons_trail_propagate_l_def propagate_unit_init_l_def S
    apply (simp only: S get_trail_l_init.simps not_False_eq_True assert.ASSERT_simps
      nres_monad3 nres_monad1 nres_order_simps mem_Collect_eq)
    apply (rule exI[of _ ‹propagate_unit_init L T›])
    using WS dec in_literals_to_update OC'_empty confl C'
    by (auto simp: twl_st_init twl_st_l_init S
      simp flip: mset_remdups_remdups_mset)
qed

lemma [twl_st_l_init]:
  ‹get_trail_l_init (set_conflict_init_l C S) = get_trail_l_init S›
  ‹literals_to_update_l_init (set_conflict_init_l C S) = {#}›
  ‹clauses_to_update_l_init (set_conflict_init_l C S) = {#}›
  ‹get_conflict_l_init (set_conflict_init_l C S) = Some (mset C)›
  ‹get_unit_clauses_l_init (set_conflict_init_l C S) = add_mset (mset C) (get_unit_clauses_l_init S)›
  ‹get_subsumed_init_clauses_l_init (set_conflict_init_l C S) = get_subsumed_init_clauses_l_init S›
  ‹get_subsumed_learned_clauses_l_init (set_conflict_init_l C S) = get_subsumed_learned_clauses_l_init S›
  ‹get_learned_unit_clauses_l_init (set_conflict_init_l C S) = get_learned_unit_clauses_l_init S›
  ‹get_learned_clauses0_l_init (set_conflict_init_l C S) = get_learned_clauses0_l_init S›
  ‹get_init_clauses0_l_init (set_conflict_init_l C S) = get_init_clauses0_l_init S›
  ‹get_clauses_l_init (set_conflict_init_l C S) = get_clauses_l_init S›
  ‹other_clauses_l_init (set_conflict_init_l C S) = other_clauses_l_init S›
  by (cases S; auto simp: set_conflict_init_l_def; fail)+

lemma init_dt_pre_set_conflict_init_l:
  assumes
    [simp]: ‹get_conflict_l_init S = None› and
    pre: ‹init_dt_pre (C' # CS) S› and
    false: ‹∀L ∈ set C.  -L ∈ lits_of_l (get_trail_l_init S)› and
    nempty: ‹C ≠ []› and
    C': ‹mset (remdups C') = mset C›
  shows
    ‹init_dt_pre CS (set_conflict_init_l C S)› (is ?pre) and
    ‹init_dt_spec [C'] S (set_conflict_init_l C S)› (is ?spec)
proof -
  have dist_C: ‹distinct C›
    using C' using same_mset_distinct_iff by blast
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None› and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init S). ¬ tautology (mset C)›
    using pre C' unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by force
  obtain M N D NE UE NEk UEk Q U OC NS US N0 U0 where
    S: ‹S = ((M, N, U, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)›
    by (cases S) auto
  have [simp]: ‹twl_list_invs (fst (set_conflict_init_l C S))›
    using add_inv by (auto simp:  set_conflict_init_l_def S
        twl_list_invs_def)
  have [simp]: ‹(set_conflict_init_l C S, set_conflict_init C T)
        ∈ twl_st_l_init›
    using SOC_T by (cases S) (auto simp: twl_st_l_init_def set_conflict_init_l_def convert_lit.simps
         convert_lits_l_extend_mono)
  have dec': ‹count_decided (get_trail_init T) = 0›
    apply (subst count_decided_0_iff)
    apply (subst twl_st_l_init_no_decision_iff)
    using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
  have [simp]: ‹twl_stgy_invs (fst (set_conflict_init C T))›
    using stgy_inv dec' nempty count_decided_ge_get_level[of ‹get_trail_init T›]
    unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
       cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
    by (cases T; cases C)
       (auto 5 5 simp: cdcl⇩W_restart_mset_state clauses_def)
  note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
  have [simp]: ‹twl_struct_invs_init (set_conflict_init C T)›
    apply (rule twl_struct_invs_init_set_conflict_init)
    subgoal
      using inv nempty dist_C SOC_T dec false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    subgoal
      using inv nempty dist_C SOC_T dec' false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    subgoal
      using inv nempty dist_C SOC_T dec false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    subgoal
      using inv nempty dist_C SOC_T dec false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    subgoal
      using inv nempty dist_C SOC_T dec false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    subgoal
      using inv nempty dist_C SOC_T dec false nempty
      by (auto simp: twl_st_init count_decided_0_iff)
    done
  show ?pre
    unfolding init_dt_pre_def
    apply (rule exI[of _ ‹set_conflict_init C T›])
    using WS dec in_literals_to_update OC'_empty tauto by (auto simp: twl_st_init twl_st_l_init)
  show ?spec
    unfolding init_dt_spec_def
    apply (rule exI[of _ ‹set_conflict_init C T›])
    using WS dec in_literals_to_update OC'_empty C' by (auto simp: twl_st_init twl_st_l_init)
qed

lemma [twl_st_init]:
  ‹get_trail_init (add_empty_conflict_init T) = get_trail_init T›
  ‹get_conflict_init (add_empty_conflict_init T) = Some {#}›
  ‹clauses_to_update_init (add_empty_conflict_init T) =  clauses_to_update_init T›
  ‹literals_to_update_init (add_empty_conflict_init T) = {#}›
  by (cases T; auto simp:; fail)+

lemma [twl_st_l_init]:
  ‹get_trail_l_init (add_empty_conflict_init_l T) = get_trail_l_init T›
  ‹get_conflict_l_init (add_empty_conflict_init_l T) = Some {#}›
  ‹clauses_to_update_l_init (add_empty_conflict_init_l T) =  clauses_to_update_l_init T›
  ‹literals_to_update_l_init (add_empty_conflict_init_l T) = {#}›
  ‹get_unit_clauses_l_init (add_empty_conflict_init_l T) = get_unit_clauses_l_init T›
  ‹get_subsumed_init_clauses_l_init (add_empty_conflict_init_l T) = get_subsumed_init_clauses_l_init T›
  ‹get_subsumed_learned_clauses_l_init (add_empty_conflict_init_l T) = get_subsumed_learned_clauses_l_init T›
  ‹get_learned_unit_clauses_l_init (add_empty_conflict_init_l T) = get_learned_unit_clauses_l_init T›
  ‹get_clauses_l_init (add_empty_conflict_init_l T) = get_clauses_l_init T›
  ‹get_init_clauses0_l_init (add_empty_conflict_init_l T) = add_mset {#} (get_init_clauses0_l_init T)›
  ‹get_learned_clauses0_l_init (add_empty_conflict_init_l T) = get_learned_clauses0_l_init T›
  ‹other_clauses_l_init (add_empty_conflict_init_l T) = (other_clauses_l_init T)›
  by (cases T; auto simp: add_empty_conflict_init_l_def; fail)+

lemma twl_struct_invs_init_add_empty_conflict_init_l:
  assumes
    lev: ‹count_decided (get_trail (fst T)) = 0› and
    invs: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_init T = {#}›
  shows ‹twl_struct_invs_init (add_empty_conflict_init T)›
      (is ?all_struct)
proof -
  obtain M N U D NE UE Q OC NS US N0 U0 where
    T: ‹T = ((M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q), OC)›
    using WS by (cases T) auto
  let ?T = ‹(M, N, U, Some {#}, NE, UE, NS, US, add_mset {#} N0, U0, {#}, {#})›
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)› and
    pinvs: ‹pcdcl_all_struct_invs (pstate⇩W_of_init ((M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q), OC))›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by auto
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset {#} (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0, Some {#})›
    unfolding T twl_struct_invs_init_def
    by (auto 5 5 simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
       clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
       true_annots_true_cls_def_iff_negation_in_model)
  then have pinvs: ‹pcdcl_all_struct_invs (pstate⇩W_of_init (?T, OC))›
    using pinvs count_decided_ge_get_level[of M] lev
    unfolding pcdcl_all_struct_invs_def
    by (auto simp: T psubsumed_invs_def entailed_clss_inv_def clauses0_inv_def)
  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, D)›
    using invs unfolding T twl_struct_invs_init_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset {#} (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0, Some {#})›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)

  have [simp]: ‹confl_cands_enqueued ?T›
    ‹propa_cands_enqueued ?T›
    ‹twl_st_inv (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q) ⟹ twl_st_inv ?T›
    ‹⋀x.  twl_exception_inv (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q) x ⟹ twl_exception_inv ?T x›
    ‹clauses_to_update_inv (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q) ⟹ clauses_to_update_inv ?T›
    ‹past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, {#}, Q) ⟹ past_invs ?T›
    by (auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+

  show ?all_struct
    using invs pinvs
    unfolding twl_struct_invs_init_def T
    unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
    by (clarsimp simp del: entailed_clss_inv.simps)
qed

lemma init_dt_pre_add_empty_conflict_init_l:
  assumes
    confl[simp]: ‹get_conflict_l_init S = None› and
    pre: ‹init_dt_pre ([] # CS) S›
  shows
    ‹init_dt_pre CS (add_empty_conflict_init_l S)› (is ?pre)
    ‹init_dt_spec [[]] S (add_empty_conflict_init_l S)› (is ?spec)
proof -
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None› and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init S). ¬ tautology (mset C)›
    using pre unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by force
  obtain M N D NE UE NEk UEk Q U OC NS US N0 U0 where
    S: ‹S = ((M, N, U, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)›
    by (cases S) auto
  have [simp]: ‹twl_list_invs (fst (add_empty_conflict_init_l S))›
    using add_inv by (auto simp: add_empty_conflict_init_l_def S
        twl_list_invs_def)
  have [simp]: ‹(add_empty_conflict_init_l S, add_empty_conflict_init T)
        ∈ twl_st_l_init›
    using SOC_T by (cases S) (auto simp: twl_st_l_init_def add_empty_conflict_init_l_def)
  have dec': ‹count_decided (get_trail_init T) = 0›
    apply (subst count_decided_0_iff)
    apply (subst twl_st_l_init_no_decision_iff)
    using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
  have [simp]: ‹twl_stgy_invs (fst (add_empty_conflict_init T))›
    using stgy_inv dec' count_decided_ge_get_level[of ‹get_trail_init T›]
    unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
       cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
    by (cases T)
       (auto 5 5 simp: cdcl⇩W_restart_mset_state clauses_def)
  note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
  have [simp]: ‹twl_struct_invs_init (add_empty_conflict_init T)›
    apply (rule twl_struct_invs_init_add_empty_conflict_init_l)
    using inv SOC_T dec' WS
    by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff )
  show ?pre
    unfolding init_dt_pre_def
    apply (rule exI[of _ ‹add_empty_conflict_init T›])
    using WS dec in_literals_to_update OC'_empty tauto by (auto simp: twl_st_init twl_st_l_init)
  show ?spec
    unfolding init_dt_spec_def
    apply (rule exI[of _ ‹add_empty_conflict_init T›])
    using WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
qed

lemma [twl_st_l_init]:
  ‹get_trail (fst (add_to_clauses_init a T)) = get_trail_init T›
  by (cases T; auto; fail)

lemma [twl_st_l_init]:
  ‹other_clauses_l_init (T, OC) = OC›
  ‹clauses_to_update_l_init (T, OC) = clauses_to_update_l T›
  by (cases T; auto; fail)+

lemma twl_struct_invs_init_add_to_clauses_init:
  assumes
    lev: ‹count_decided (get_trail_init T) = 0› and
    invs: ‹twl_struct_invs_init T› and
    confl: ‹get_conflict_init T = None› and
    MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
    WS: ‹clauses_to_update_init T = {#}› and
   dist_C: ‹distinct C› and
   le_2: ‹length C ≥ 2›
  shows
    ‹twl_struct_invs_init (add_to_clauses_init C T)›
      (is ?all_struct)
proof -
  obtain M N U NE UE OC WS NS US N0 U0 where
    T: ‹T = ((M, N, U, None, NE, UE, NS, US, N0, U0, WS, uminus `# lit_of `# mset M), OC)›
    using confl MQ by (cases T) auto
  let ?Q = ‹uminus `# lit_of `# mset M›

  let ?S = ‹(M, N, U, None, NE, UE, NS, US, WS, ?Q)›
  have [simp]: ‹get_all_ann_decomposition M = [([], M)]›
    by (rule no_decision_get_all_ann_decomposition) (use lev in ‹auto simp: T count_decided_0_iff›)
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, (clauses N + OC + NE + NS + N0), clauses U + UE + US + U0,  None)› and
    excep: ‹twl_st_exception_inv (M, N, U, None, NE, UE, NS, US, N0, U0, WS, ?Q)› and
    st_inv: ‹twl_st_inv (M, N, U, None, NE, UE, NS, US, N0, U0, WS, ?Q)› and
    pinvs: ‹pcdcl_all_struct_invs
       (pstate⇩W_of_init ((M, N, U, None, NE, UE, NS, US, N0, U0, WS, uminus `# lit_of `# mset M), OC))›
    using invs confl unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def by auto
  then have
   ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset C) (clauses N + OC + NE + NS + N0),
     clauses U + UE + US + U0, None)› and
   n_d: ‹no_dup M›
    using dist_C
    by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
       cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
      clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def)
  then have pinvs': ‹pcdcl_all_struct_invs (pstate⇩W_of_init (add_to_clauses_init C T))›
    using invs unfolding T twl_struct_invs_init_def pcdcl_all_struct_invs_def
    by (auto simp: entailed_clss_inv_def psubsumed_invs_def mset_take_mset_drop_mset' clauses0_inv_def)
  have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + OC + NE + NS + N0, clauses U + UE + US + U0, None)›
    using invs confl unfolding T twl_struct_invs_init_def by auto
  then have [simp]:
     ‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset C) (clauses N + OC + NE + NS + N0),
        clauses U + UE + US + U0,  None)›
    using lev
    by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
        clauses_def T count_decided_0_iff)

  have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
    using st_inv that by (simp add: twl_st_inv.simps)

  show ‹twl_struct_invs_init (add_to_clauses_init C T)›
    apply (rule twl_struct_invs_init_init_state)
    subgoal using lev by (auto simp: T)
    subgoal using struct dist_C le_2 by (auto simp: T mset_take_mset_drop_mset')
    subgoal using MQ by (auto simp: T)
    subgoal using WS by (auto simp: T)
    subgoal using pinvs' by (simp add: T mset_take_mset_drop_mset')
    subgoal by (auto simp: T mset_take_mset_drop_mset')
    subgoal by (auto simp: T)
    done
qed

lemma get_trail_init_add_to_clauses_init[simp]:
  ‹get_trail_init (add_to_clauses_init a T) = get_trail_init T›
  by (cases T) auto

lemma init_dt_pre_add_to_clauses_init_l:
  assumes
    D: ‹get_conflict_l_init S = None› and
    a: ‹length a ≠ Suc 0› ‹a ≠ []› and
    pre: ‹init_dt_pre (a' # CS) S› and
    ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    C': ‹mset (remdups a') = mset a› and
    not_tauto: ‹¬tautology (mset a')›
  shows
    ‹add_to_clauses_init_l a S ≤ SPEC (init_dt_pre CS)› (is ?pre) and
    ‹add_to_clauses_init_l a S ≤ SPEC (init_dt_spec [a'] S)› (is ?spec)
proof -
  have not_tauto': ‹¬tautology (mset a)›
    by (metis C' consistent_interp_tautology not_tauto set_remdups)
  obtain T where
    SOC_T: ‹(S, T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init S = {#}› and
    dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init S = None ⟶
     literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
    add_inv: ‹twl_list_invs (fst S)› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None› and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init S). ¬ tautology (mset C)›
    using pre unfolding init_dt_pre_def
    apply -
    apply normalize_goal+
    by force
  have dec': ‹∀L ∈ set (get_trail_init T). ¬is_decided L›
    using SOC_T dec apply -
    apply (rule twl_st_l_init_no_decision_iff[THEN iffD2])
    using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
  obtain M N NE UE NEk UEk Q OC NS US N0 U0 where
    S: ‹S = ((M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)›
    using D WS by (cases S) auto
  have le_2: ‹length a ≥ 2›
    using a by (cases a) auto
  have
    ‹init_dt_pre CS ((M, fmupd i (a, True) N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)› (is ?pre1) and
    ‹init_dt_spec [a'] S
          ((M, fmupd i (a, True) N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)› (is ?spec1)
    if
      i_0: ‹0 < i› and
      i_dom: ‹i ∉# dom_m N›
    for i :: ‹nat›
  proof -
    let ?S = ‹((M, fmupd i (a, True) N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)›
    have ‹Propagated L i ∉ set M› for L
      using add_inv i_dom i_0 unfolding S
      by (auto simp: twl_list_invs_def)
    then have ‹(?S, add_to_clauses_init a T) ∈ twl_st_l_init›
      using SOC_T i_dom
      by (auto simp: S twl_st_l_init_def init_clss_l_mapsto_upd_notin
          learned_clss_l_mapsto_upd_notin_irrelev convert_lit.simps
          intro!: convert_lits_l_extend_mono[of _ _ N ‹NEk+UEk› ‹fmupd i (a, True) N›])
    moreover have ‹twl_struct_invs_init (add_to_clauses_init a T)›
      apply (rule twl_struct_invs_init_add_to_clauses_init)
      subgoal
        apply (subst count_decided_0_iff)
        apply (subst twl_st_l_init_no_decision_iff)
        using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
      subgoal by (use dec SOC_T in_literals_to_update in
          ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
      subgoal by (use dec SOC_T in_literals_to_update in
          ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
      subgoal by (use dec SOC_T in_literals_to_update in
          ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
      subgoal by (use dec SOC_T in_literals_to_update in
          ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
      subgoal using C' same_mset_distinct_iff by blast
      subgoal by (use dec SOC_T in_literals_to_update in
          ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
      done
    moreover have ‹twl_list_invs (M, fmupd i (a, True) N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
      using add_inv i_dom i_0 not_tauto' by (auto simp: S twl_list_invs_def ran_m_mapsto_upd_notin)
    moreover have ‹twl_stgy_invs (fst (add_to_clauses_init a T))›
      by (rule twl_stgy_invs_backtrack_lvl_0)
        (use dec' SOC_T in ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init
           twl_st_l_init_def›)
    ultimately show ?pre1 ?spec1
      unfolding init_dt_pre_def init_dt_spec_def apply -
      subgoal
        apply (rule exI[of _ ‹add_to_clauses_init a T›])
        using dec OC'_empty in_literals_to_update tauto not_tauto' by (auto simp: S
          ran_m_mapsto_upd_notin i_dom)
      subgoal
        apply (rule exI[of _ ‹add_to_clauses_init a T›])
        using dec OC'_empty in_literals_to_update i_dom i_0 a C'
        by (auto simp: S learned_clss_l_mapsto_upd_notin_irrelev ran_m_mapsto_upd_notin
          remdups_mset_idem)
      done
  qed
  then show ?pre ?spec
    by (auto simp: S add_to_clauses_init_l_def get_fresh_index_def RES_RETURN_RES)
qed

lemma init_dt_pre_init_dt_step:
  assumes pre: ‹init_dt_pre (a # CS) SOC›
  shows ‹init_dt_step a SOC ≤ SPEC (λSOC'. init_dt_pre CS SOC' ∧ init_dt_spec [a] SOC SOC')›
proof -
  obtain S OC where SOC: ‹SOC = (S, OC)›
    by (cases SOC) auto
  obtain T where
    SOC_T: ‹((S, OC), T) ∈ twl_st_l_init› and
    inv: ‹twl_struct_invs_init T› and
    WS: ‹clauses_to_update_l_init (S, OC) = {#}› and
    dec: ‹∀s∈set (get_trail_l_init (S, OC)). ¬ is_decided s› and
    in_literals_to_update: ‹get_conflict_l_init (S, OC) = None ⟶
     literals_to_update_l_init (S, OC) = uminus `# lit_of `# mset (get_trail_l_init (S, OC))› and
    add_inv: ‹twl_list_invs (fst (S, OC))› and
    stgy_inv: ‹twl_stgy_invs (fst T)› and
    OC'_empty: ‹other_clauses_l_init (S, OC) ≠ {#} ⟶ get_conflict_l_init (S, OC) ≠ None› and
    tauto: ‹∀C∈#ran_mf (get_clauses_l_init (S, OC)). ¬ tautology (mset C)›
    using pre unfolding SOC init_dt_pre_def
    apply -
    apply normalize_goal+
    by presburger
  have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
    using SOC_T dec by (rule twl_st_l_init_no_decision_iff[THEN iffD2])

  obtain M N D NE UE NEk UEk NS US N0 U0 Q where
    S: ‹SOC = ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)›
    using WS by (cases SOC) (auto simp: SOC)
  then have S': ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
    using S unfolding SOC by auto
  show ?thesis
  proof (cases ‹get_conflict_l (fst SOC)›)
    case None
    then show ?thesis
      using pre dec
      unfolding init_dt_step_def remdups_clause_def
      by refine_vcg
        (auto simp add: Let_def count_decided_0_iff SOC twl_st_l_init twl_st_init
          remdups_clause_def
          true_annot_iff_decided_or_true_lit length_list_Suc_0
          init_dt_step_def get_fresh_index_def RES_RETURN_RES
          intro: init_dt_pre_already_propagated_unit_init_l init_dt_pre_set_conflict_init_l
            init_dt_pre_propagate_unit_init init_dt_pre_add_empty_conflict_init_l
            init_dt_pre_add_to_clauses_init_l init_dt_pre_add_to_tautology_init_l
          intro!: SPEC_rule_conjI
          dest: init_dt_pre_ConsD in_lits_of_l_defined_litD tautology_length_ge2
          simp flip: mset_remdups_remdups_mset)
  next
    case  (Some D')
    then have [simp]: ‹D = Some D'›
      by (auto simp: S)
    have [simp]:
       ‹(((M, N, Some D', NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), add_mset (remdups_mset (mset a)) OC),
           add_to_other_init a T)
         ∈ twl_st_l_init› for a
      using SOC_T by (cases T; auto simp: S S' twl_st_l_init_def; fail)+
    have ‹init_dt_pre CS ((M, N, Some D', NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), add_mset (remdups_mset (mset a)) OC)›
      unfolding init_dt_pre_def
      apply (rule exI[of _ ‹add_to_other_init (a) T›])
      using inv WS dec' dec in_literals_to_update add_inv stgy_inv SOC_T tauto
      by (auto simp: S' count_decided_0_iff twl_st_init
          intro!: twl_struct_invs_init_add_to_other_init)
    moreover have ‹init_dt_spec [a] ((M, N, Some D', NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), OC)
      ((M, N, Some D', NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q), add_mset (remdups_mset (mset a)) OC)›
      unfolding init_dt_spec_def
      apply (rule exI[of _ ‹add_to_other_init (a) T›])
      using inv WS dec dec' in_literals_to_update add_inv stgy_inv SOC_T
      by (auto simp: S' count_decided_0_iff twl_st_init
          intro!: twl_struct_invs_init_add_to_other_init)
    ultimately show ?thesis
      by (auto simp: S init_dt_step_def)
  qed
qed

lemma [twl_st_l_init]:
  ‹get_trail_l_init (S, OC) = get_trail_l S›
  ‹literals_to_update_l_init (S, OC) = literals_to_update_l S›
  by (cases S; auto; fail)+

lemma init_dt_spec_append:
  assumes
    spec1: ‹init_dt_spec CS S T›  and
    spec: ‹init_dt_spec CS' T U›
  shows ‹init_dt_spec (CS @ CS') S U›
proof -
  obtain T' where
    TT': ‹(T, T') ∈ twl_st_l_init› and
    ‹twl_struct_invs_init T'› and
    ‹clauses_to_update_l_init T = {#}› and
    ‹∀s∈set (get_trail_l_init T). ¬ is_decided s› and
    ‹get_conflict_l_init T = None ⟶
     literals_to_update_l_init T = uminus `# lit_of `# mset (get_trail_l_init T)› and
    clss: ‹remdups_mset `# mset `# mset CS + mset `# ran_mf (get_clauses_l_init S) + other_clauses_l_init S +
        get_unit_clauses_l_init S +
        get_subsumed_init_clauses_l_init S +
        get_init_clauses0_l_init S =
        mset `# ran_mf (get_clauses_l_init T) + other_clauses_l_init T + get_unit_clauses_l_init T +
        get_subsumed_init_clauses_l_init T +
        get_init_clauses0_l_init T› and
    learned: ‹learned_clss_lf (get_clauses_l_init S) = learned_clss_lf (get_clauses_l_init T)› and
    unit_le:
      ‹get_subsumed_learned_clauses_l_init S = get_subsumed_learned_clauses_l_init T›
      ‹get_learned_clauses0_l_init S = get_learned_clauses0_l_init T›
      ‹get_learned_unit_clauses_l_init S = get_learned_unit_clauses_l_init T› and
    ‹twl_list_invs (fst T)› and
    ‹twl_stgy_invs (fst T')› and
    ‹other_clauses_l_init T ≠ {#} ⟶ get_conflict_l_init T ≠ None› and
    empty: ‹{#} ∈# mset `# mset CS ⟶ get_conflict_l_init T ≠ None› and
    confl_kept: ‹get_conflict_l_init S ≠ None ⟶ get_conflict_l_init S = get_conflict_l_init T›
    using spec1
    unfolding init_dt_spec_def apply -
    apply normalize_goal+
    by presburger

  obtain U' where
    UU': ‹(U, U') ∈ twl_st_l_init› and
    struct_invs: ‹twl_struct_invs_init U'› and
    WS: ‹clauses_to_update_l_init U = {#}› and
    dec: ‹∀s∈set (get_trail_l_init U). ¬ is_decided s› and
    confl: ‹get_conflict_l_init U = None ⟶
     literals_to_update_l_init U = uminus `# lit_of `# mset (get_trail_l_init U)› and
    clss': ‹remdups_mset `# mset `# mset CS' + mset `# ran_mf (get_clauses_l_init T) + other_clauses_l_init T +
     get_unit_clauses_l_init T + get_subsumed_init_clauses_l_init T + get_init_clauses0_l_init T =
     mset `# ran_mf (get_clauses_l_init U) + other_clauses_l_init U + get_unit_clauses_l_init U +
     get_subsumed_init_clauses_l_init U + get_init_clauses0_l_init U› and
    learned': ‹learned_clss_lf (get_clauses_l_init T) = learned_clss_lf (get_clauses_l_init U)› and
    unit_le': ‹get_learned_unit_clauses_l_init U = get_learned_unit_clauses_l_init T›
      ‹get_subsumed_learned_clauses_l_init U = get_subsumed_learned_clauses_l_init T›
      ‹get_learned_clauses0_l_init U = get_learned_clauses0_l_init T› and
    list_invs: ‹twl_list_invs (fst U)› and
    stgy_invs: ‹twl_stgy_invs (fst U')› and
    oth: ‹other_clauses_l_init U ≠ {#} ⟶ get_conflict_l_init U ≠ None› and
    empty': ‹{#} ∈# mset `# mset CS' ⟶ get_conflict_l_init U ≠ None› and
    confl_kept': ‹get_conflict_l_init T ≠ None ⟶ get_conflict_l_init T = get_conflict_l_init U›
    using spec
    unfolding init_dt_spec_def apply -
    apply normalize_goal+
    by metis
  have ‹remdups_mset `# mset `# mset (CS @ CS') + mset `# ran_mf (get_clauses_l_init S) + other_clauses_l_init S +
    get_unit_clauses_l_init S + get_subsumed_init_clauses_l_init S + get_init_clauses0_l_init S =
    remdups_mset `# mset `# mset CS' + (remdups_mset `# mset `# mset CS + mset `# ran_mf (get_clauses_l_init S) + other_clauses_l_init S +
    get_unit_clauses_l_init S + get_subsumed_init_clauses_l_init S + get_init_clauses0_l_init S)›
    by auto
  also have ‹... = remdups_mset `# mset `# mset CS' + mset `# ran_mf (get_clauses_l_init T) + other_clauses_l_init T +
        get_unit_clauses_l_init T + get_subsumed_init_clauses_l_init T + get_init_clauses0_l_init T›
    unfolding clss by (auto simp: ac_simps)
  finally have eq: ‹remdups_mset `# mset `# mset (CS @ CS') + mset `# ran_mf (get_clauses_l_init S) + other_clauses_l_init S +
    get_unit_clauses_l_init S +
    get_subsumed_init_clauses_l_init S +
    get_init_clauses0_l_init S =
    mset `# ran_mf (get_clauses_l_init U) + other_clauses_l_init U + get_unit_clauses_l_init U +
    get_subsumed_init_clauses_l_init U +
    get_init_clauses0_l_init U›
    unfolding clss' .
  show ?thesis
    unfolding init_dt_spec_def apply -
    apply (rule exI[of _ U'])
    apply (intro conjI)
    subgoal using UU' .
    subgoal using struct_invs .
    subgoal using WS .
    subgoal using dec .
    subgoal using confl .
    subgoal using eq .
    subgoal using learned' learned by simp
    subgoal using unit_le unit_le' by simp
    subgoal using unit_le unit_le' learned by auto
    subgoal using unit_le unit_le' learned by auto
    subgoal using list_invs .
    subgoal using stgy_invs .
    subgoal using oth .
    subgoal using empty empty' oth confl_kept' by auto
    subgoal using confl_kept confl_kept' by auto
    done
qed

lemma init_dt_full:
  fixes CS :: ‹'v literal list list› and SOC :: ‹'v twl_st_l_init› and S'
  defines
    ‹S ≡ fst SOC› and
    ‹OC ≡ snd SOC›
  assumes
    ‹init_dt_pre CS SOC›
  shows
    ‹init_dt CS SOC ≤ SPEC (init_dt_spec CS SOC)›
  using assms unfolding S_def OC_def
proof (induction CS arbitrary: SOC)
  case Nil
  then obtain S OC where SOC: ‹SOC = (S, OC)›
    by (cases SOC) auto
  from Nil
  obtain T where
    T: ‹(SOC, T) ∈ twl_st_l_init›
      ‹twl_struct_invs_init T›
      ‹clauses_to_update_l_init SOC = {#}›
      ‹∀s∈set (get_trail_l_init SOC). ¬ is_decided s›
      ‹get_conflict_l_init SOC = None ⟶
       literals_to_update_l_init SOC =
       uminus `# lit_of `# mset (get_trail_l_init SOC)›
      ‹twl_list_invs (fst SOC)›
      ‹twl_stgy_invs (fst T)›
      ‹other_clauses_l_init SOC ≠ {#} ⟶ get_conflict_l_init SOC ≠ None›
    unfolding init_dt_pre_def apply -
    apply normalize_goal+
    by auto

  then show ?case
    unfolding init_dt_def SOC init_dt_spec_def nfoldli_simps
    apply (intro RETURN_rule)
    unfolding prod.simps
    apply (rule exI[of _ T])
    using T by (auto simp: SOC twl_st_init twl_st_l_init)
next
  case (Cons a CS) note IH = this(1) and pre = this(2)
  note init_dt_step_def[simp]
  have 1: ‹init_dt_step a SOC ≤ SPEC (λSOC'. init_dt_pre CS SOC' ∧ init_dt_spec [a] SOC SOC')›
    by (rule init_dt_pre_init_dt_step[OF pre])
  have 2: ‹init_dt_spec (a # CS) SOC UOC›
    if spec: ‹init_dt_spec CS T UOC› and
       spec': ‹init_dt_spec [a] SOC T› for T UOC
    using init_dt_spec_append[OF spec' spec] by simp
  show ?case
    unfolding init_dt_def nfoldli_simps if_True
    apply (rule specify_left)
     apply (rule 1)
    apply (rule order.trans)
    unfolding init_dt_def[symmetric]
     apply (rule IH)
     apply (solves ‹simp›)
    apply (rule SPEC_rule)
    by (rule 2) fast+
qed

lemma init_dt_pre_empty_state:
  ‹init_dt_pre [] (([], fmempty, None, {#}, {#}, {#}, {#}, {#}, {#}, {#},{#}, {#},{#}), {#})›
  unfolding init_dt_pre_def
  by (auto simp: twl_st_l_init_def twl_struct_invs_init_def twl_st_inv.simps
      twl_struct_invs_def twl_st_inv.simps cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
      cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
      past_invs.simps clauses_def pcdcl_all_struct_invs_def clauses0_inv_def
      cdcl⇩W_restart_mset_state twl_list_invs_def psubsumed_invs_def
      twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
      cdcl⇩W_restart_mset.no_smaller_confl_def entailed_clss_inv_def
      cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)

lemma twl_init_invs:
  ‹twl_struct_invs_init (([], {#}, {#}, None, {#}, {#}, {#}, {#}, {#},{#}, {#},{#}), {#})›
  ‹twl_list_invs ([], fmempty, None, {#}, {#}, {#}, {#}, {#}, {#}, {#},{#}, {#},{#})›
  ‹twl_stgy_invs ([], {#}, {#}, None, {#}, {#}, {#}, {#}, {#}, {#}, {#},{#})›
  by (auto simp: twl_struct_invs_init_def twl_st_inv.simps twl_list_invs_def twl_stgy_invs_def
      past_invs.simps
      twl_struct_invs_def twl_st_inv.simps cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
      cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
      past_invs.simps clauses_def pcdcl_all_struct_invs_def clauses0_inv_def
      cdcl⇩W_restart_mset_state twl_list_invs_def psubsumed_invs_def
      twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
      cdcl⇩W_restart_mset.no_smaller_confl_def entailed_clss_inv_def
      cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)
end