Theory IsaSAT_Restart

theory IsaSAT_Restart
  imports
    Watched_Literals.WB_Sort Watched_Literals.Watched_Literals_Watch_List_Simp IsaSAT_Rephase_State
    IsaSAT_Setup IsaSAT_VMTF IsaSAT_Sorting IsaSAT_Proofs IsaSAT_Restart_Defs
    IsaSAT_Bump_Heuristics
begin

chapter ‹Restarts›

lemma twl_st_heur_change_subsumed_clauses:
  fixes lcount lcount' :: clss_size
  assumes ‹(S,
     (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) ∈ twl_st_heur›
    ‹set_mset (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) = set_mset (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS', US', N0, U0, Q, W))›and
    ‹clss_size_corr N NE UE NEk UEk NS' US' N0 U0 lcount'›
  shows ‹(set_learned_count_wl_heur lcount' S,
     (M, N, D, NE, UE, NEk, UEk, NS', US', N0, U0, Q, W)) ∈ twl_st_heur›
proof -
  note cong = trail_pol_cong heuristic_rel_cong
      option_lookup_clause_rel_cong isa_vmtf_cong heuristic_rel_cong
  note cong2 = D0_cong phase_saving_cong cach_refinement_empty_cong vdom_m_cong isasat_input_nempty_cong
    isasat_input_bounded_cong empty_occs_list_cong
  show ?thesis
    supply[[goals_limit=1]]
    supply [dest!] = cong[OF assms(2)]
    using assms(1) assms(3) apply -
    unfolding twl_st_heur_def in_pair_collect_simp prod.simps get_trail_wl.simps get_clauses_wl.simps
      get_conflict_wl.simps literals_to_update_wl.simps get_watched_wl.simps
      IsaSAT_Setup.get_unkept_unit_learned_clss_wl.simps
      IsaSAT_Setup.get_kept_unit_init_clss_wl.simps
      IsaSAT_Setup.get_kept_unit_learned_clss_wl.simps get_subsumed_init_clauses_wl.simps
      get_subsumed_learned_clauses_wl.simps get_init_clauses0_wl.simps isasat_state_simp
       get_learned_clauses0_wl.simps IsaSAT_Setup.get_unkept_unit_init_clss_wl.simps
    apply normalize_goal+
    apply (subst (asm) cong2[OF assms(2)])+
    apply (intro conjI)
    apply ((drule cong[OF assms(2)])+; assumption)+
    done
qed

text ‹
  This is a list of comments (how does it work for glucose and cadical) to prepare the future
  refinement:
  ▸ Reduction
     ▪ every 2000+300*n (rougly since inprocessing changes the real number, cadical)
           (split over initialisation file); don't restart if level < 2 or if the level is less
       than the fast average
     ▪ curRestart * nbclausesbeforereduce;
          curRestart = (conflicts / nbclausesbeforereduce) + 1 (glucose)
  ▸ Killed
     ▪ half of the clauses that ❙‹can› be deleted (i.e., not used since last restart), not strictly
       LBD, but a probability of being useful.
     ▪ half of the clauses
  ▸ Restarts:
     ▪ EMA-14, aka restart if enough clauses and slow\_glue\_avg * opts.restartmargin > fast\_glue (file ema.cpp)
     ▪ (lbdQueue.getavg() * K) > (sumLBD / conflictsRestarts),
       text‹conflictsRestarts > LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid() && trail.size() > R * trailQueue.getavg()›
›
declare all_atms_def[symmetric,simp]

lemma twl_st_heur_restart_anaD: ‹x ∈ twl_st_heur_restart_ana r ⟹ x ∈ twl_st_heur_restart›
  by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def)

lemma twl_st_heur_restartD:
  ‹x ∈ twl_st_heur_restart ⟹ x ∈ twl_st_heur_restart_ana (length (get_clauses_wl_heur (fst x)))›
  by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def)

named_theorems twl_st_heur_restart

lemma [twl_st_heur_restart]:
  assumes ‹(S, T) ∈ twl_st_heur_restart›
  shows ‹(get_trail_wl_heur S, get_trail_wl T) ∈ trail_pol (all_init_atms_st T)›
  using assms by (cases S; cases T)
   (simp only: twl_st_heur_restart_def get_trail_wl.simps
    mem_Collect_eq prod.case get_clauses_wl.simps get_unit_init_clss_wl.simps all_init_atms_st_def
    all_init_atms_def get_init_clauses0_wl.simps tuple17.inject get_unkept_unit_init_clss_wl.simps
    get_kept_unit_init_clss_wl.simps
    get_subsumed_init_clauses_wl.simps split: isasat_int_splits)

lemma trail_pol_literals_are_in_ℒin_trail:
  ‹(M', M) ∈ trail_pol 𝒜 ⟹ literals_are_in_ℒin_trail 𝒜 M›
  unfolding literals_are_in_ℒin_trail_def trail_pol_def
  by auto

lemma refine_generalise1: ‹A ≤ B ⟹ do {x ← B; C x} ≤ D ⟹ do {x ← A; C x} ≤ (D:: 'a nres)›
  using Refine_Basic.bind_mono(1) dual_order.trans by blast

lemma refine_generalise2: "A ≤ B ⟹ do {x ← do {x ← B; A' x}; C x} ≤ D ⟹
  do {x ← do {x ← A; A' x}; C x} ≤ (D:: 'a nres)"
  by (simp add: refine_generalise1)


lemma trail_pol_no_dup: ‹(M, M') ∈ trail_pol 𝒜 ⟹ no_dup M'›
  by (auto simp: trail_pol_def)

definition remove_all_annot_true_clause_imp_wl_D_pre
  :: ‹nat multiset ⇒ nat literal ⇒ nat twl_st_wl ⇒ bool›
where
  ‹remove_all_annot_true_clause_imp_wl_D_pre 𝒜 L S ⟷ (L ∈# ℒall 𝒜)›

definition remove_all_annot_true_clause_imp_wl_D_heur_pre where
  ‹remove_all_annot_true_clause_imp_wl_D_heur_pre L S ⟷
    (∃S'. (S, S') ∈ twl_st_heur_restart
      ∧ remove_all_annot_true_clause_imp_wl_D_pre (all_init_atms_st S') L S')›

definition five_uint64 :: ‹64 word› where
  ‹five_uint64 = 5›

definition div2 where [simp]: ‹div2 n = n div 2›

definition safe_minus where ‹safe_minus a b = (if b ≥ a then 0 else a - b)›


definition restart_flag_rel :: ‹(8 word × restart_type) set› where
  ‹restart_flag_rel = {(FLAG_no_restart, NO_RESTART), (FLAG_restart, RESTART), (FLAG_GC_restart, GC),
  (FLAG_Reduce_restart, GC), (FLAG_Inprocess_restart, INPROCESS)}›

lemma clss_size_corr_restart_simp2:
  ‹NO_MATCH {#} UE ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c =
  clss_size_corr_restart N NE {#} NEk UEk NS US N0 U0 c›
  ‹NO_MATCH {#} US ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c =
   clss_size_corr_restart N NE UE NEk UEk NS {#} N0 U0 c›
  ‹NO_MATCH {#} U0 ⟹ clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c =
  clss_size_corr_restart N NE UE NEk UEk NS US N0 {#} c› and
  clss_size_corr_restart_intro:
  ‹C ∈# dom_m N ⟹ ¬irred N C ⟹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 c ⟹
  clss_size_corr_restart (fmdrop C N) NE UE NEk UEk NS US' N0 U0' (clss_size_decr_lcount c)›
  by (auto simp: clss_size_corr_restart_def)

lemma mark_garbage_heur_wl:
  assumes
    ST: ‹(S, T) ∈ twl_st_heur_restart› and
    ‹C ∈# dom_m (get_clauses_wl T)› and
    ‹¬ irred (get_clauses_wl T) C› and ‹i < length (get_tvdom S)› and
    iC: ‹get_tvdom S ! i = C›
  shows ‹(mark_garbage_heur3 C i S, mark_garbage_wl C T) ∈ twl_st_heur_restart›
proof -
  show ?thesis
    using assms distinct_mset_dom[of ‹get_clauses_wl T›]
      distinct_mset_mono[of ‹mset (get_avdom S)› ‹mset (get_vdom S)›]
  apply (cases S; cases T)
   apply (simp add: twl_st_heur_restart_def mark_garbage_heur3_def mark_garbage_wl_def)
  by (auto simp: twl_st_heur_restart_def mark_garbage_heur3_def mark_garbage_wl_def
         learned_clss_l_l_fmdrop size_remove1_mset_If clss_size_corr_restart_intro
    simp: all_init_atms_def all_init_lits_def aivdom_inv_dec_remove_clause
     simp del: all_init_atms_def[symmetric]
    intro: valid_arena_extra_information_mark_to_delete'
    intro!: aivdom_inv_dec_remove_and_swap_inactive_tvdom
    aivdom_inv_dec_remove_and_swap_inactive
      dest!: in_set_butlastD in_vdom_m_fmdropD
    elim!: in_set_upd_cases)
qed

lemma mark_garbage_heur_wl_ana:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart_ana r› and
    ‹C ∈# dom_m (get_clauses_wl T)› and
    ‹¬ irred (get_clauses_wl T) C› ‹C = get_tvdom S ! i› ‹i < length (get_tvdom S)›
  shows ‹(mark_garbage_heur3 C i S, mark_garbage_wl C T) ∈ twl_st_heur_restart_ana r›
proof -
  have [intro!]: ‹distinct n ⟹ mset n ⊆# mset m ⟹ mset (removeAll (n ! i) n) ⊆# mset m› for n A m
    by (metis filter_mset_eq_conv mset_filter removeAll_filter_not_eq subset_mset.dual_order.trans)

  show ?thesis
    using assms
    using assms distinct_mset_dom[of ‹get_clauses_wl T›]
      distinct_mset_mono[of ‹mset (get_avdom S)› ‹mset (get_vdom S)›]
    apply (cases S; cases T)
    apply (simp add: twl_st_heur_restart_ana_def mark_garbage_heur3_def mark_garbage_wl_def)
    by (auto simp: twl_st_heur_restart_def mark_garbage_heur3_def mark_garbage_wl_def
      learned_clss_l_l_fmdrop size_remove1_mset_If init_clss_l_fmdrop_irrelev aivdom_inv_dec_remove_clause
      valid_arena_extra_information_mark_to_delete' clss_size_corr_restart_intro
      simp: all_init_atms_def all_init_lits_def clss_size_corr_restart_simp2
      simp del: all_init_atms_def[symmetric] clss_size_corr_restart_simp
      intro: valid_arena_extra_information_mark_to_delete'
      intro!: aivdom_inv_dec_remove_and_swap_inactive
      aivdom_inv_dec_remove_and_swap_inactive_tvdom
      dest!: in_set_butlastD in_vdom_m_fmdropD
      elim!: in_set_upd_cases)
qed

lemma mark_unused_st_heur_ana:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart_ana r› and
    ‹C ∈# dom_m (get_clauses_wl T)›
  shows ‹(mark_unused_st_heur C S, T) ∈ twl_st_heur_restart_ana r›
  using assms
  apply (cases S; cases T)
   apply (simp add: twl_st_heur_restart_ana_def mark_unused_st_heur_def)
  apply (auto simp: twl_st_heur_restart_def mark_garbage_heur_def mark_garbage_wl_def
         learned_clss_l_l_fmdrop size_remove1_mset_If
     simp: all_init_atms_def all_init_lits_def
     simp del: all_init_atms_def[symmetric]
     intro!: valid_arena_mark_unused
     dest!: in_set_butlastD in_vdom_m_fmdropD
     elim!: in_set_upd_cases)
  done

lemma twl_st_heur_restart_valid_arena[twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart›
  shows ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))›
  using assms by (auto simp: twl_st_heur_restart_def)

lemma twl_st_heur_restart_get_avdom_nth_get_vdom[twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart› ‹i < length (get_avdom S)›
  shows ‹get_avdom S ! i ∈ set (get_vdom S)›
  using assms by (auto 5 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
    dest!: set_mset_mono)

lemma twl_st_heur_restart_get_tvdom_nth_get_vdom[twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart› ‹i < length (get_tvdom S)›
  shows ‹get_tvdom S ! i ∈ set (get_vdom S)›
  using assms by (auto 5 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
    dest!: set_mset_mono)

lemma [twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart› and
    ‹C ∈ set (get_avdom S)›
  shows ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))› and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
proof -
  show ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))›
    using assms
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_dom_status_iff(1) aivdom_inv_dec_alt_def
        split: prod.splits)
  assume C: ‹C ∈# dom_m (get_clauses_wl T)›
  show ‹arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
  show ‹arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
  show ‹arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
qed


lemma [twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart_ana r› and
    ‹C ∈ set (get_avdom S)›
  shows ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))› and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
    using assms
    by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart)

lemma [twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart› and
    ‹C ∈ set (get_tvdom S)›
  shows ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))› and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
proof -
  show ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))›
    using assms
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_dom_status_iff(1) aivdom_inv_dec_alt_def
        split: prod.splits)
  assume C: ‹C ∈# dom_m (get_clauses_wl T)›
  show ‹arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
  show ‹arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
  show ‹arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
    using assms C
    by (cases S; cases T)
      (auto simp add: twl_st_heur_restart_def clause_not_marked_to_delete_heur_def
          arena_lifting
        split: prod.splits)
qed

lemma [twl_st_heur_restart]:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart_ana r› and
    ‹C ∈ set (get_tvdom S)›
  shows ‹clause_not_marked_to_delete_heur S C ⟷ (C ∈# dom_m (get_clauses_wl T))› and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_lit (get_clauses_wl_heur S) C = get_clauses_wl T ∝ C ! 0›and
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_status (get_clauses_wl_heur S) C = LEARNED ⟷ ¬irred (get_clauses_wl T) C›
    ‹C ∈# dom_m (get_clauses_wl T) ⟹ arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl T ∝ C)›
    using assms
    by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart)

lemma number_clss_to_keep_impl_number_clss_to_keep:
  ‹(number_clss_to_keep_impl, number_clss_to_keep) ∈ Id →f ⟨nat_rel⟩nres_rel›
  by (auto simp: number_clss_to_keep_impl_def number_clss_to_keep_def Let_def intro!: frefI nres_relI)

lemma in_set_delete_index_and_swapD:
  ‹x ∈ set (delete_index_and_swap xs i) ⟹ x ∈ set xs›
  apply (cases ‹i < length xs›)
  apply (auto dest!: in_set_butlastD)
  by (metis List.last_in_set in_set_upd_cases list.size(3) not_less_zero)

lemma delete_index_vdom_heur_twl_st_heur_restart_ana:
  ‹(S, T) ∈ twl_st_heur_restart_ana r ⟹ i < length (get_tvdom S) ⟹
  get_tvdom S ! i ∉# dom_m (get_clauses_wl T) ⟹
    (delete_index_vdom_heur i S, T) ∈ twl_st_heur_restart_ana r›
  using in_set_delete_index_and_swapD[of _ ‹get_tvdom S› i]
    distinct_mset_mono[of ‹mset (get_tvdom S)› ‹mset (get_vdom S)›]
  supply [[goals_limit=1]]
  by (clarsimp simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def delete_index_vdom_heur_def)
    (auto intro!: aivdom_inv_dec_removed_inactive_tvdom)


lemma incr_wasted_st:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart_ana r›
  shows ‹(incr_wasted_st C S, T) ∈ twl_st_heur_restart_ana r›
  using assms
  apply (cases S; cases T)
   apply (simp add: twl_st_heur_restart_ana_def incr_wasted_st_def)
   apply (auto simp: twl_st_heur_restart_def heuristic_rel_stats_def
     learned_clss_l_l_fmdrop size_remove1_mset_If phase_save_heur_rel_def
     simp: all_init_atms_def all_init_lits_def 
     simp del: all_init_atms_def[symmetric]
     intro!: valid_arena_mark_unused
     dest!: in_set_butlastD in_vdom_m_fmdropD
     elim!: in_set_upd_cases)
  done


lemma twl_st_heur_restart_same_annotD:
  ‹(S, T) ∈ twl_st_heur_restart ⟹ Propagated L C ∈ set (get_trail_wl T) ⟹
     Propagated L C' ∈ set (get_trail_wl T) ⟹ C = C'›
  ‹(S, T) ∈ twl_st_heur_restart ⟹ Propagated L C ∈ set (get_trail_wl T) ⟹
     Decided L ∈ set (get_trail_wl T) ⟹ False›
  by (auto simp: twl_st_heur_restart_def dest: no_dup_no_propa_and_dec
    no_dup_same_annotD)

lemma ℒall_mono:
  ‹set_mset 𝒜 ⊆ set_mset ℬ ⟹ L  ∈# ℒall 𝒜 ⟹ L  ∈# ℒall ℬ›
  by (auto simp: ℒall_def)

lemma all_lits_of_mm_mono2:
  ‹x ∈# (all_lits_of_mm A) ⟹ set_mset A ⊆ set_mset B ⟹ x ∈# (all_lits_of_mm B)›
  by (auto simp: all_lits_of_mm_def)


lemma ℒall_init_all:
  ‹L ∈# ℒall (all_init_atms_st x1a) ⟹ L ∈# ℒall (all_atms_st x1a)›
  using all_init_lits_of_wl_all_lits_st ℒall_all_atms
    ℒall_all_init_atms(2) by blast



lemma twl_st_heur_restartD2:
  ‹x ∈ twl_st_heur_restart ⟹ x ∈ twl_st_heur_restart_ana' (length (get_clauses_wl_heur (fst x)))
  (learned_clss_count (fst x))›
  by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def)

lemma ℒall_atm_of_all_init_lits_of_mm:
  ‹set_mset (ℒall (atm_of `# all_init_lits N NUE)) = set_mset (all_init_lits N NUE)›
  by (auto simp: all_init_lits_def ℒall_atm_of_all_lits_of_mm)

lemma trail_pol_replace_annot_in_trail_spec:
  assumes
    ‹atm_of x2 < length (trail_get_reason (get_trail_wl_heur S))› and
    x2: ‹atm_of x2 ∈# all_init_atms_st (ys @ Propagated x2 C # zs, x2n')› and
    ‹(S, (ys @ Propagated x2 C # zs, x2n'))
    ∈ twl_st_heur_restart_ana r› and
    M: ‹M = get_trail_wl_heur S›
  shows
    ‹(set_trail_wl_heur (trail_update_reason_at x2 0 M) S,
        (ys @ Propagated x2 0 # zs, x2n'))
       ∈ twl_st_heur_restart_ana r›
proof -
  let ?S = ‹(ys @ Propagated x2 C # zs, x2n')›
  let ?𝒜 = ‹all_init_atms_st ?S›
  have pol: ‹(get_trail_wl_heur S, ys @ Propagated x2 C # zs)
         ∈ trail_pol (all_init_atms_st ?S)›
    using assms(3) unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def all_init_atms_st_def
    by (cases x2n') auto
  obtain x y x1b x1c x1d x1e x2d x2e where
    tr: ‹get_trail_wl_heur S = (x1b, x1c, x1d, x1e, x2d)› and
    x2d: ‹x2d = (count_decided (ys @ Propagated x2 C # zs), y, x2e)› and
    reasons: ‹((map lit_of (rev (ys @ Propagated x2 C # zs)), x1e),
      ys @ Propagated x2 C # zs)
     ∈ ann_lits_split_reasons ?𝒜› and
    pol: ‹∀L∈#ℒall ?𝒜.        nat_of_lit L < length x1c ∧
        x1c ! nat_of_lit L = polarity (ys @ Propagated x2 C # zs) L› and
    n_d: ‹no_dup (ys @ Propagated x2 C # zs)› and
    lvls: ‹∀L∈#ℒall ?𝒜. atm_of L < length x1d ∧
        x1d ! atm_of L = get_level (ys @ Propagated x2 C # zs) L› and
    ‹undefined_lit ys (lit_of (Propagated x2 C))› and
    ‹undefined_lit zs (lit_of (Propagated x2 C))› and
    inA:‹∀L∈set (ys @ Propagated x2 C # zs). lit_of L ∈# ℒall ?𝒜› and
    cs: ‹control_stack y (ys @ Propagated x2 C # zs)› and
    ‹literals_are_in_ℒin_trail ?𝒜 (ys @ Propagated x2 C # zs)› and
    ‹length (ys @ Propagated x2 C # zs) < unat32_max› and
    ‹length (ys @ Propagated x2 C # zs) ≤ unat32_max div 2 + 1› and
    ‹count_decided (ys @ Propagated x2 C # zs) < unat32_max› and
    ‹length (map lit_of (rev (ys @ Propagated x2 C # zs))) =
     length (ys @ Propagated x2 C # zs)› and
    bounded: ‹isasat_input_bounded ?𝒜› and
    x1b: ‹x1b = map lit_of (rev (ys @ Propagated x2 C # zs))› and
    ‹zeroed_trail (ys @ Propagated x2 C # zs) x2e›
    using pol unfolding trail_pol_alt_def
    apply (cases ‹get_trail_wl_heur S›)
    by blast
  have lev_eq: ‹get_level (ys @ Propagated x2 C # zs) =
    get_level (ys @ Propagated x2 0 # zs)›
    ‹count_decided (ys @ Propagated x2 C # zs) =
      count_decided (ys @ Propagated x2 0 # zs)›
    by (auto simp: get_level_cons_if get_level_append_if)
  have [simp]: ‹atm_of x2 < length x1e›
    using reasons x2 assms(1) unfolding tr by auto

  have ‹((x1b, x1e[atm_of x2 := 0]), ys @ Propagated x2 0 # zs)
       ∈ ann_lits_split_reasons ?𝒜›
    using reasons n_d undefined_notin
    by (auto simp: ann_lits_split_reasons_def x1b
      DECISION_REASON_def atm_of_eq_atm_of)
  moreover have n_d': ‹no_dup (ys @ Propagated x2 0 # zs)›
    using n_d by auto
  moreover have ‹∀L∈#ℒall ?𝒜.
     nat_of_lit L < length x1c ∧
        x1c ! nat_of_lit L = polarity (ys @ Propagated x2 0 # zs) L›
    using pol by (auto simp: polarity_def)
  moreover have ‹∀L∈#ℒall ?𝒜.
    atm_of L < length x1d ∧
           x1d ! atm_of L = get_level (ys @ Propagated x2 0 # zs) L›
    using lvls by (auto simp: get_level_append_if get_level_cons_if)
  moreover have ‹control_stack y (ys @ Propagated x2 0 # zs)›
    using cs apply -
    apply (subst control_stack_alt_def[symmetric, OF n_d'])
    apply (subst (asm) control_stack_alt_def[symmetric, OF n_d])
    unfolding control_stack'_def lev_eq
    apply normalize_goal
    apply (intro ballI conjI)
    apply (solves auto)
    unfolding set_append list.set(2) Un_iff insert_iff
    apply (rule disjE, assumption)
    subgoal for L
      by (drule_tac x = L in bspec)
        (auto simp: nth_append nth_Cons split: nat.splits)
    apply (rule disjE[of ‹_ = _›], assumption)
    subgoal for L
      by (auto simp: nth_append nth_Cons split: nat.splits)
    subgoal for L
      by (drule_tac x = L in bspec)
        (auto simp: nth_append nth_Cons split: nat.splits)
    done
  moreover have ‹zeroed_trail (ys @ Propagated x2 0 # zs) x2e›
    using ‹zeroed_trail (ys @ Propagated x2 C # zs) x2e›
    by (auto simp: zeroed_trail_def nth_append nth_Cons split: if_splits nat.splits)
  ultimately have
    ‹((x1b, x1c, x1d, x1e[atm_of x2 := 0], x2d), ys @ Propagated x2 0 # zs)
         ∈ trail_pol ?𝒜›
    using n_d x2 inA bounded
    unfolding trail_pol_def x2d
    by simp

  moreover { fix aaa ca
    have ‹vmtf_ℒall (all_init_atms aaa ca) (ys @ Propagated x2 C # zs) =
       vmtf_ℒall (all_init_atms aaa ca) (ys @ Propagated x2 0 # zs)›
       by (auto simp: vmtf_ℒall_def)
    then have ‹vmtf (all_init_atms aaa ca) (ys @ Propagated x2 C # zs) =
      vmtf (all_init_atms aaa ca) (ys @ Propagated x2 0 # zs)›
      by (auto simp: vmtf_def  vmtf_def
	image_iff)
    moreover have ‹vmtf (all_init_atms aaa ca) (get_unit_trail (ys @ Propagated x2 C # zs)) =
      vmtf (all_init_atms aaa ca) (get_unit_trail(ys @ Propagated x2 0 # zs))›
      by (auto simp: vmtf_def  get_unit_trail_def takeWhile_append vmtf_ℒall_def
	image_iff)
    moreover have ‹acids (all_init_atms aaa ca) (get_unit_trail (ys @ Propagated x2 C # zs)) =
      acids (all_init_atms aaa ca) (get_unit_trail(ys @ Propagated x2 0 # zs))›
      apply (auto simp: acids_def get_unit_trail_def takeWhile_append vmtf_ℒall_def
	image_iff)
      apply (metis (no_types, lifting) map_lit_of_eq_defined_litD valid_trail_reduction_eq_alt_def
        valid_trail_reduction_eq_change_annot)+
      done
    moreover have ‹acids (all_init_atms aaa ca) ((ys @ Propagated x2 C # zs)) =
      acids (all_init_atms aaa ca) ((ys @ Propagated x2 0 # zs))›
      apply (auto simp: acids_def get_unit_trail_def takeWhile_append vmtf_ℒall_def
	image_iff)
      apply (metis (mono_tags, lifting) map_lit_of_eq_defined_litD valid_trail_reduction_eq_alt_def
        valid_trail_reduction_eq_change_annot)+
      done
    ultimately have ‹bump_heur (all_init_atms aaa ca) (ys @ Propagated x2 C # zs) =
      bump_heur (all_init_atms aaa ca) (ys @ Propagated x2 0 # zs)›
      by (auto simp: bump_heur_def)
  }
  moreover { fix D
    have ‹get_level (ys @ Propagated x2 C # zs) = get_level (ys @ Propagated x2 0 # zs)›
      by (auto simp: get_level_append_if get_level_cons_if)
    then have ‹counts_maximum_level (ys @ Propagated x2 C # zs) D =
      counts_maximum_level (ys @ Propagated x2 0 # zs) D› and
      ‹out_learned (ys @ Propagated x2 C # zs) = out_learned (ys @ Propagated x2 0 # zs)›
      by (auto simp: counts_maximum_level_def card_max_lvl_def
        out_learned_def intro!: ext)
  }
  ultimately show ?thesis
    using assms(3) unfolding twl_st_heur_restart_ana_def M
    by (cases x2n')
      (auto simp: twl_st_heur_restart_def all_init_atms_st_def tr trail_update_reason_at_def
        simp flip: mset_map drop_map)
qed

lemmas trail_pol_replace_annot_in_trail_spec2 =
  trail_pol_replace_annot_in_trail_spec[of ‹- _›, simplified]

lemma ℒall_ball_all:
  ‹(∀L ∈# ℒall (all_atms N NUE). P L) = (∀L ∈# all_lits N NUE. P L)›
  ‹(∀L ∈# ℒall (all_init_atms N NUE). P L) = (∀L ∈# all_init_lits N NUE. P L)›
  by (simp_all add: ℒall_all_atms_all_lits  ℒall_all_init_atms)

lemma clss_size_corr_restart_intro3[intro]:
  ‹clss_size_corr_restart N NE UE NEk UEk NS US N0 U0 lcount ⟹
  clss_size_corr_restart N NE UE NEk UEk NS {#} N0 {#} (clss_size_resetUS0 lcount)›
  by (auto simp: clss_size_corr_restart_def clss_size_resetUS_def clss_size_def
    clss_size_resetU0_def clss_size_resetUE_def)

lemma twl_st_heur_restart_ana_US_empty:
  ‹NO_MATCH {#} US ⟹ NO_MATCH {#} U0 ⟹  NO_MATCH {#} UE ⟹ (S, M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, W, Q) ∈ twl_st_heur_restart_ana r ⟹
   (set_learned_count_wl_heur (clss_size_resetUS0 (get_learned_count S)) S, M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, W, Q)
       ∈ twl_st_heur_restart_ana r›
  by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def
    intro: clss_size_corr_simp)

fun equality_except_trail_empty_US_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where
‹equality_except_trail_empty_US_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)
     (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', WS', Q') ⟷
  N = N' ∧ D = D' ∧ NE = NE' ∧ NEk = NEk' ∧ UEk = UEk' ∧ NS = NS' ∧ US = {#} ∧ UE = {#} ∧
  N0' = N0 ∧ U0 = {#} ∧ WS = WS' ∧ Q = Q'›

lemma equality_except_conflict_wl_get_clauses_wl:
    ‹equality_except_conflict_wl S Y ⟹ get_clauses_wl S = get_clauses_wl Y› and
  equality_except_conflict_wl_get_trail_wl:
    ‹equality_except_conflict_wl S Y ⟹ get_trail_wl S = get_trail_wl Y› and
  equality_except_trail_empty_US_wl_get_conflict_wl:
    ‹equality_except_trail_empty_US_wl S Y ⟹ get_conflict_wl S = get_conflict_wl Y› and
  equality_except_trail_empty_US_wl_get_clauses_wl:
    ‹equality_except_trail_empty_US_wl S Y⟹ get_clauses_wl S = get_clauses_wl Y›
 by (cases S; cases Y; solves auto)+

lemma isasat_replace_annot_in_trail_replace_annot_in_trail_spec:
  ‹(((L, C), S), ((L', C'), S')) ∈ Id ×f Id ×f twl_st_heur_restart_ana' r u ⟹
  isasat_replace_annot_in_trail L C S ≤
    ⇓{(U, U'). (U, U') ∈ twl_st_heur_restart_ana' r u ∧
        get_clauses_wl_heur U = get_clauses_wl_heur S ∧
        get_learned_count U = clss_size_resetUS0 (get_learned_count S) ∧
       get_vdom U = get_vdom S ∧
       equality_except_trail_empty_US_wl U' S'}
    (replace_annot_wl L' C' S')›
  unfolding isasat_replace_annot_in_trail_def replace_annot_wl_def
    uncurry_def replace_reason_in_trail_def nres_monad3
  apply (cases S', hypsubst, unfold prod.case)
  apply refine_rcg
  subgoal
    by (auto simp: trail_pol_alt_def ann_lits_split_reasons_def ℒall_ball_all all_init_lits_of_wl_def
      twl_st_heur_restart_def twl_st_heur_restart_ana_def replace_annot_wl_pre_def
      all_init_lits_alt_def(2))
  subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f
    unfolding replace_annot_wl_pre_def replace_annot_l_pre_def bind_to_let_conv Let_def
    apply (clarify dest!: split_list[of ‹Propagated _ _›])
    apply (rule RETURN_SPEC_refine)
    apply (rule_tac x = ‹(ys @ Propagated L 0 # zs, x2, x1a, x2a, {#}, x2b, x1c, x2c, {#}, x2d, {#}, x2e, x1f)› in exI)
    apply (intro conjI)
    prefer 2
    apply (rule_tac x = ‹ys @ Propagated L 0 # zs› in exI)
    apply (intro conjI)
    apply blast
    by (auto intro!: trail_pol_replace_annot_in_trail_spec[where C=C]
        trail_pol_replace_annot_in_trail_spec2
      simp: atm_of_eq_atm_of all_init_atms_def replace_annot_wl_pre_def
      ℒall_ball_all replace_annot_l_pre_def state_wl_l_def all_init_lits_of_wl_def
      all_init_lits_def ac_simps
        twl_st_heur_restart_ana_US_empty learned_clss_count_def  all_init_atms_st_def
      simp del: all_init_atms_def[symmetric]; fail)+
  done

lemma get_pos_of_level_in_trail_le_decomp:
  assumes
    ‹(S, T) ∈ twl_st_heur_restart›
  shows ‹get_pos_of_level_in_trail (get_trail_wl T) 0
         ≤ SPEC
            (λk. ∃M1. (∃M2 K.
                          (Decided K # M1, M2)
                          ∈ set (get_all_ann_decomposition (get_trail_wl T))) ∧
                      count_decided M1 = 0 ∧ k = length M1)›
  unfolding get_pos_of_level_in_trail_def
proof (rule SPEC_rule)
  fix x
  assume H: ‹x < length (get_trail_wl T) ∧
        is_decided (rev (get_trail_wl T) ! x) ∧
        get_level (get_trail_wl T) (lit_of (rev (get_trail_wl T) ! x)) = 0 + 1›
  let ?M1 = ‹rev (take x (rev (get_trail_wl T)))›
  let ?K =  ‹Decided ((lit_of(rev (get_trail_wl T) ! x)))›
  let ?M2 = ‹rev (drop  (Suc x) (rev (get_trail_wl T)))›
  have T: ‹(get_trail_wl T) = ?M2 @ ?K # ?M1› and
     K: ‹Decided (lit_of ?K) = ?K›
    apply (subst append_take_drop_id[symmetric, of _ ‹length (get_trail_wl T) - Suc x›])
    apply (subst Cons_nth_drop_Suc[symmetric])
    using H
    apply (auto simp: rev_take rev_drop rev_nth)
    apply (cases ‹rev (get_trail_wl T) ! x›)
    apply (auto simp: rev_take rev_drop rev_nth)
    done
  have n_d: ‹no_dup (get_trail_wl T)›
    using assms(1)
    by (auto simp: twl_st_heur_restart_def)
  obtain M2 where
    ‹(?K # ?M1, M2) ∈ set (get_all_ann_decomposition (get_trail_wl T))›
    using get_all_ann_decomposition_ex[of ‹lit_of ?K› ?M1 ?M2]
    apply (subst (asm) K)
    apply (subst (asm) K)
    apply (subst (asm) T[symmetric])
    by blast
  moreover have ‹count_decided ?M1 = 0›
    using n_d H
    by (subst (asm)(1) T, subst (asm)(11)T, subst T) auto
  moreover have ‹x = length ?M1›
    using n_d H by auto
  ultimately show ‹∃M1. (∃M2 K. (Decided K # M1, M2)
                 ∈ set (get_all_ann_decomposition (get_trail_wl T))) ∧
             count_decided M1 = 0 ∧ x = length M1 ›
    by blast
qed

lemma twl_st_heur_restart_isa_length_trail_get_trail_wl:
  ‹(S, T) ∈ twl_st_heur_restart_ana r ⟹ mop_isa_length_trail (get_trail_wl_heur S) = RETURN (length (get_trail_wl T))›
  unfolding isa_length_trail_def twl_st_heur_restart_ana_def twl_st_heur_restart_def trail_pol_alt_def
    mop_isa_length_trail_def isa_length_trail_pre_def
  by (subgoal_tac ‹(case get_trail_wl_heur S of
            (M', xs, lvls, reasons, k, cs) ⇒ length M' ≤ unat32_max)›)
    (cases S;auto dest: ann_lits_split_reasons_map_lit_of intro!: ASSERT_leI; fail)+

lemma twl_st_heur_restart_count_decided_st_alt_def:
  fixes S :: isasat
  shows ‹(S, T) ∈ twl_st_heur_restart_ana r ⟹ count_decided_st_heur S = count_decided (get_trail_wl T)›
  unfolding count_decided_st_def twl_st_heur_restart_ana_def trail_pol_def twl_st_heur_restart_def
  by (cases T) (auto simp: count_decided_st_heur_def count_decided_pol_def)

lemma twl_st_heur_restart_trailD:
  ‹(S, T) ∈ twl_st_heur_restart_ana r ⟹
    (get_trail_wl_heur S, get_trail_wl T) ∈ trail_pol (all_init_atms_st T)›
  by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def all_init_atms_st_def
    get_unit_init_clss_wl_alt_def)

lemma no_dup_nth_proped_dec_notin:
  ‹no_dup M ⟹ k < length M ⟹ M ! k = Propagated L C ⟹ Decided L ∉ set M›
  apply (auto dest!: split_list simp: nth_append nth_Cons defined_lit_def in_set_conv_nth
    split: if_splits nat.splits)
  by (metis no_dup_no_propa_and_dec nth_mem)

lemma get_literal_and_reason:
  assumes
    ‹((k, S), k', T) ∈ nat_rel ×f twl_st_heur_restart_ana r› and
    ‹remove_one_annot_true_clause_one_imp_wl_pre k' T› and
    proped: ‹is_proped (rev (get_trail_wl T) ! k')›
  shows ‹do {
           L ← isa_trail_nth (get_trail_wl_heur S) k;
           C ← get_the_propagation_reason_pol (get_trail_wl_heur S) L;
           RETURN (L, C)
         } ≤ ⇓ {((L, C), L', C'). L = L' ∧ C' = the C ∧ C ≠ None}
              (SPEC (λp. rev (get_trail_wl T) ! k' = Propagated (fst p) (snd p)))›
proof -
  have n_d: ‹no_dup (get_trail_wl T)› and
   res: ‹((k, S), k', T) ∈ nat_rel ×f twl_st_heur_restart›
    using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def)
  from no_dup_nth_proped_dec_notin[OF this(1), of ‹length (get_trail_wl T) - Suc k'›]
  have dec_notin: ‹Decided (lit_of (rev (fst T) ! k')) ∉ set (fst T)›
    using proped assms(2) by (cases T; cases ‹rev (get_trail_wl T) ! k'›)
     (auto simp: twl_st_heur_restart_def state_wl_l_def
      remove_one_annot_true_clause_one_imp_wl_pre_def twl_st_l_def
      remove_one_annot_true_clause_one_imp_pre_def rev_nth
      dest: no_dup_nth_proped_dec_notin)
  have k': ‹k' < length (get_trail_wl T)› and [simp]: ‹fst T = get_trail_wl T›
    using proped assms(2)
    by (cases T; auto simp: twl_st_heur_restart_def state_wl_l_def
      remove_one_annot_true_clause_one_imp_wl_pre_def twl_st_l_def
      remove_one_annot_true_clause_one_imp_pre_def; fail)+
  define k'' where ‹k'' ≡ length (get_trail_wl T) - Suc k'›
  have k'': ‹k'' < length (get_trail_wl T)›
    using k' by (auto simp: k''_def)
  have ‹rev (get_trail_wl T) ! k' = get_trail_wl T ! k''›
    using k' k'' by (auto simp: k''_def nth_rev)
  then have ‹rev_trail_nth (fst T) k' ∈# ℒall (all_init_atms_st T)›
    using k'' assms nth_mem[OF k']
    by (auto simp: twl_st_heur_restart_ana_def rev_trail_nth_def get_unit_init_clss_wl_alt_def
      trail_pol_alt_def twl_st_heur_restart_def all_init_atms_st_def)
  then have 1: ‹(SPEC (λp. rev (get_trail_wl T) ! k' = Propagated (fst p) (snd p))) =
    do {
      L ← RETURN (rev_trail_nth (fst T) k');
      ASSERT(L ∈# ℒall (all_init_atms_st T));
      C ← (get_the_propagation_reason (fst T) L);
      ASSERT(C ≠ None);
      RETURN (L, the C)
    }›
    using proped dec_notin k' nth_mem[OF k''] no_dup_same_annotD[OF n_d]
    apply (subst dual_order.eq_iff)
    apply (rule conjI)
    subgoal
      unfolding get_the_propagation_reason_def
      apply (cases ‹rev (get_trail_wl T) ! k'›)
      apply (auto simp: RES_RES_RETURN_RES rev_trail_nth_def
            get_the_propagation_reason_def lits_of_def rev_nth
  	    RES_RETURN_RES
           dest: split_list
	    simp flip: k''_def
	    intro!: le_SPEC_bindI[of _ ‹Some (mark_of (get_trail_wl T ! k''))›])
      apply (cases ‹rev (get_trail_wl T) ! k'›) (*TODO proof*)
      apply  (auto simp: RES_RES_RETURN_RES rev_trail_nth_def RES_ASSERT_moveout
          get_the_propagation_reason_def lits_of_def rev_nth
	  RES_RETURN_RES
        simp flip: k''_def
        dest: split_list
        intro!: exI[of _ ‹Some (mark_of (rev (get_trail_wl T) ! k'))›])
	  apply (subst RES_ASSERT_moveout)
	    by (auto 4 3 simp: RES_RETURN_RES image_iff
        dest: split_list
        intro!: exI[of _ ‹Some (mark_of ((get_trail_wl T) ! k''))›])
    subgoal
      apply (cases ‹rev (get_trail_wl T) ! k'›) (*TODO proof*)
      apply  (auto simp: RES_RES_RETURN_RES rev_trail_nth_def RES_ASSERT_moveout
          get_the_propagation_reason_def lits_of_def rev_nth
	  RES_RETURN_RES
        simp flip: k''_def
        dest: split_list
        intro!: exI[of _ ‹Some (mark_of (rev (get_trail_wl T) ! k'))›])
	  apply (subst RES_ASSERT_moveout)
	    by (auto 4 3 simp: RES_RETURN_RES image_iff
        dest: split_list
        intro!: exI[of _ ‹Some (mark_of ((get_trail_wl T) ! k''))›])
    done

  show ?thesis
    supply RETURN_as_SPEC_refine[refine2 del]
    apply (subst 1)
    apply (refine_rcg
      isa_trail_nth_rev_trail_nth[THEN fref_to_Down_curry, unfolded comp_def,
        of _ _ _ _ ‹all_init_atms_st T›]
      get_the_propagation_reason_pol[THEN fref_to_Down_curry, unfolded comp_def,
        of ‹all_init_atms_st T›])
    subgoal using k' by auto
    subgoal using assms by (cases S; auto dest: twl_st_heur_restart_trailD)
    subgoal by auto
    subgoal for K K'
      using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def
        all_init_atms_st_def get_unit_init_clss_wl_alt_def)
    subgoal
      by auto
    done
qed


lemma red_in_dom_number_of_learned_ge1: ‹C' ∈# dom_m baa ⟹ ¬ irred baa C' ⟹ Suc 0 ≤ size (learned_clss_l baa)›
  by (auto simp: ran_m_def dest!: multi_member_split)


definition find_decomp_wl0 :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where
  ‹find_decomp_wl0 = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q', W').
  (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
  count_decided M' = 0) ∧
  (N', D', NE', UE', NEk', UEk', NS', US, N0, U0, Q', W') = (N, D, NE, UE, NEk, UEk, NS, US', N0', U0', Q, W))›
lemma cdcl_twl_local_restart_wl_spec0_alt_def:
  ‹cdcl_twl_local_restart_wl_spec0 = (λS. do {
    ASSERT(restart_abs_wl_pre2 S False);
    if count_decided (get_trail_wl S) > 0
    then do {
      T ← SPEC(find_decomp_wl0 S);
      RETURN (empty_Q_wl T)
    } else RETURN (empty_US_heur_wl S)})›
  by (intro ext; case_tac S)
   (auto 6 4 simp: cdcl_twl_local_restart_wl_spec0_def
	RES_RETURN_RES2 image_iff RES_RETURN_RES empty_US_heur_wl_def
	find_decomp_wl0_def empty_Q_wl_def uncurry_def
       intro!: bind_cong[OF refl]
      dest: get_all_ann_decomposition_exists_prepend)


lemma cdcl_twl_local_restart_wl_spec0:
  assumes Sy:  ‹(S, y) ∈ twl_st_heur_restart_ana' r u› and
    ‹get_conflict_wl y = None›
  shows ‹do {
      if count_decided_st_heur S > 0
      then do {
        S ← find_decomp_wl_st_int 0 S;
        empty_Q (empty_US_heur S)
      } else RETURN (empty_US_heur S)
    }
         ≤ ⇓ (twl_st_heur_restart_ana' r u) (cdcl_twl_local_restart_wl_spec0 y)›
proof -
  define upd :: ‹_ ⇒ _ ⇒ isasat ⇒ isasat› where
    ‹upd M' vm = (λ S. set_vmtf_wl_heur vm (set_trail_wl_heur M' S))›
     for M' :: trail_pol and vm

  have find_decomp_wl_st_int_alt_def:
    ‹find_decomp_wl_st_int = (λhighest S. do{
      (M', vm) ← isa_find_decomp_wl_imp (get_trail_wl_heur S) highest (get_vmtf_heur S);
      RETURN (upd M' vm S)
    })›
    unfolding upd_def find_decomp_wl_st_int_def
    by (auto intro!: ext)

  have [refine0]: ‹do {
	  (M', vm) ←
	    isa_find_decomp_wl_imp (get_trail_wl_heur S) 0 (get_vmtf_heur S);
	  RETURN (upd M' vm S)
    } ≤ ⇓ {(S,
     T).
    (set_literals_to_update_wl_heur (isa_length_trail (get_trail_wl_heur S))
     (set_heur_wl_heur (restart_info_restart_done_heur (get_heur S)) S),
	  (empty_Q_wl2 T)) ∈ twl_st_heur_restart_ana' r u ∧
	  isa_length_trail_pre (get_trail_wl_heur S)} (SPEC (find_decomp_wl0 y))›
     (is ‹_ ≤ ⇓ ?A _›)
    if
      ‹0 < count_decided_st_heur S› and
      ‹0 < count_decided (get_trail_wl y)›
  proof -
    have A:‹ ?A = {(S,
     T).
    (set_literals_to_update_wl_heur (length (get_trail_wl T))
     (set_heur_wl_heur (restart_info_restart_done_heur (get_heur S)) S),
	  (empty_Q_wl2 T)) ∈ twl_st_heur_restart_ana' r u ∧
	  isa_length_trail_pre (get_trail_wl_heur S)}›
	  supply[[goals_limit=1]]
      apply (rule ; rule)
      subgoal for x
        apply clarify
	apply (frule twl_st_heur_restart_isa_length_trail_get_trail_wl)
        by (auto simp:  trail_pol_def empty_Q_wl2_def mop_isa_length_trail_def)
      subgoal for x
        apply clarify
	apply (frule twl_st_heur_restart_isa_length_trail_get_trail_wl)
        by (auto simp:  trail_pol_def empty_Q_wl2_def
            mop_isa_length_trail_def learned_clss_count_def)
      done

    let ?𝒜 = ‹all_init_atms_st y›
    have vm: ‹get_vmtf_heur S ∈ bump_heur ?𝒜 (get_trail_wl y)› (is ‹?vm ∈ _›) and
      n_d: ‹no_dup (get_trail_wl y)›
      using Sy
      by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def
        all_init_atms_st_def get_unit_init_clss_wl_alt_def)

    have find_decomp_w_ns_pre:
      ‹find_decomp_w_ns_pre (all_init_atms_st y) ((get_trail_wl y, 0), ?vm)›
      using that assms vm unfolding find_decomp_w_ns_pre_def
      by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def
        all_init_atms_st_def get_unit_init_clss_wl_alt_def
        dest: trail_pol_literals_are_in_ℒin_trail)
    have 1: ‹isa_find_decomp_wl_imp (get_trail_wl_heur S) 0 (get_vmtf_heur S) ≤
       ⇓ ({(M, M'). (M, M') ∈ trail_pol ?𝒜 ∧ count_decided M' = 0} ×f Id)
         (find_decomp_w_ns ?𝒜 (get_trail_wl y) 0 vm')›
      apply (rule  order_trans)
      apply (rule isa_find_decomp_wl_imp_find_decomp_wl_imp[THEN fref_to_Down_curry2,
        of ‹get_trail_wl y› 0 ?vm _ _ _ ?𝒜])
      subgoal using that by auto
      subgoal
        using Sy vm
	by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def get_unit_init_clss_wl_alt_def
          all_init_atms_st_def)
      apply (rule order_trans, rule ref_two_step')
      apply (rule find_decomp_wl_imp_find_decomp_wl'[THEN fref_to_Down_curry2,
        of ?𝒜 ‹get_trail_wl y› 0 ?vm])
      subgoal by (rule find_decomp_w_ns_pre)
      subgoal by auto
      subgoal
        using n_d
        by (fastforce simp: find_decomp_w_ns_def conc_fun_RES Image_iff)
      done

  show ?thesis
      supply [[goals_limit=1]] unfolding A
      apply (rule bind_refine_res[OF _ 1[unfolded find_decomp_w_ns_def conc_fun_RES]])
      apply (case_tac y, cases S)
      apply clarify
      apply (rule RETURN_SPEC_refine)
      using assms
      by (auto simp: upd_def find_decomp_wl0_def
        intro!: RETURN_SPEC_refine clss_size_corr_simp simp: twl_st_heur_restart_def out_learned_def
	    empty_Q_wl2_def twl_st_heur_restart_ana_def learned_clss_count_def
            all_init_atms_st_def
	intro: isa_length_trail_pre dest: no_dup_appendD)
  qed
  have [simp]: ‹clss_size_corr_restart x1a x1c x1d NEk UEk x1e x1f x1g x1h (ck, cl, cd, cm, cn) ⟹
    clss_size_corr_restart x1a x1c x1d NEk UEk x1e {#} x1g {#} (ck, 0, cd, 0, 0)›
    for  x1a x1c x1d x1e x1f x1g x1h ck cl cm cn NEk UEk cd
    by (auto simp: clss_size_corr_restart_def clss_size_def)

  have Sy': ‹(empty_US_heur S, empty_US_heur_wl y) ∈ twl_st_heur_restart_ana' r u›
    using Sy by (cases y; cases S; auto simp: twl_st_heur_restart_ana_def
      empty_US_heur_wl_def twl_st_heur_restart_def empty_US_heur_def clss_size_resetUE_def
      clss_size_lcountUEk_def
      clss_size_resetUS_def clss_size_lcount_def clss_size_lcountU0_def clss_size_resetU0_def
      learned_clss_count_def clss_size_def clss_size_lcountUS_def clss_size_lcountUE_def)
  show ?thesis
    unfolding find_decomp_wl_st_int_alt_def
      cdcl_twl_local_restart_wl_spec0_alt_def
    apply refine_vcg
    subgoal
      using Sy by (auto simp: twl_st_heur_restart_count_decided_st_alt_def)
    subgoal for Sa T
      unfolding empty_Q_def empty_Q_wl_def empty_US_heur_def empty_Q_wl2_def
      apply clarify
      apply (frule twl_st_heur_restart_isa_length_trail_get_trail_wl)
      by refine_vcg
       (cases ‹get_learned_count Sa›, auto simp add: mop_isa_length_trail_def twl_st_heur_restart_ana_def get_unit_init_clss_wl_alt_def
        twl_st_heur_restart_def learned_clss_count_def clss_size_resetUS_def clss_size_lcountUEk_def Let_def
        clss_size_lcount_def clss_size_lcountU0_def clss_size_resetU0_def clss_size_resetUE_def
      learned_clss_count_def clss_size_def clss_size_lcountUS_def clss_size_lcountUE_def)
    subgoal
      using Sy' .
    done
qed

lemma no_get_all_ann_decomposition_count_dec0:
  ‹(∀M1. (∀M2 K. (Decided K # M1, M2) ∉ set (get_all_ann_decomposition M))) ⟷
  count_decided M = 0›
  apply (induction M rule: ann_lit_list_induct)
  subgoal by auto
  subgoal for L M
    by auto
  subgoal for L C M
    by (cases ‹get_all_ann_decomposition M›) fastforce+
  done

lemma get_pos_of_level_in_trail_decomp_iff:
  assumes ‹no_dup M›
  shows ‹((∃M1 M2 K.
                (Decided K # M1, M2)
                ∈ set (get_all_ann_decomposition M) ∧
                count_decided M1 = 0 ∧ k = length M1)) ⟷
    k < length M ∧ count_decided M > 0 ∧ is_decided (rev M ! k) ∧ get_level M (lit_of (rev M ! k)) = 1›
  (is ‹?A ⟷ ?B›)
proof
  assume ?A
  then obtain K M1 M2 where
    decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and
    [simp]: ‹count_decided M1 = 0› and
    k_M1: ‹length M1 = k›
    by auto
  then have ‹k < length M›
    by auto
  moreover have ‹rev M ! k = Decided K›
    using decomp
    by (auto dest!: get_all_ann_decomposition_exists_prepend
      simp: nth_append
      simp flip: k_M1)
  moreover have ‹get_level M (lit_of (rev M ! k)) = 1›
    using assms decomp
    by (auto dest!: get_all_ann_decomposition_exists_prepend
      simp: get_level_append_if nth_append
      simp flip: k_M1)
  ultimately show ?B
    using decomp by auto
next
  assume ?B
  define K where ‹K = lit_of (rev M ! k)›
  obtain M1 M2 where
    M: ‹M = M2 @ Decided K # M1› and
    k_M1: ‹length M1 = k›
    apply (subst (asm) append_take_drop_id[of ‹length M - Suc k›, symmetric])
    apply (subst (asm) Cons_nth_drop_Suc[symmetric])
    unfolding K_def
    subgoal using ‹?B› by auto
    subgoal using ‹?B› K_def by (cases ‹rev M ! k›) (auto simp: rev_nth)
    done
  moreover have ‹count_decided M1 = 0›
    using assms ‹?B› unfolding M
    by (auto simp: nth_append k_M1)
  ultimately show ?A
    using get_all_ann_decomposition_ex[of K M1 M2]
    unfolding M
    by auto
qed

lemma remove_all_learned_subsumed_clauses_wl_id:
  ‹(x2a, x2) ∈ twl_st_heur_restart_ana' r u ⟹
   RETURN (empty_US_heur x2a)
    ≤ ⇓ (twl_st_heur_restart_ana' r u)
       (remove_all_learned_subsumed_clauses_wl x2)›
   by (cases x2a; cases x2)
    (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def learned_clss_count_def
     remove_all_learned_subsumed_clauses_wl_def empty_US_heur_def
     intro: clss_size_corr_simp)

lemma mark_garbage_heur4_remove_and_add_cls_l:
  ‹(S, T) ∈ {(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧ learned_clss_count S ≤ u} ⟹ (C, C') ∈ Id ⟹
    mark_garbage_heur4 C S
       ≤ ⇓ {(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧ learned_clss_count S ≤ u}
            (remove_and_add_cls_wl C' T)›
  unfolding mark_garbage_heur4_def remove_and_add_cls_wl_def Let_def
  apply (cases T, hypsubst, unfold prod.case)
  apply refine_rcg
  subgoal
    by (auto simp add: twl_st_heur_restart_def twl_st_heur_restart_ana_def arena_lifting get_unit_init_clss_wl_alt_def
      dest!: clss_size_corr_restart_rew multi_member_split simp: ran_m_def)
  subgoal
    supply [[goals_limit=1]]
    apply (auto simp: learned_clss_count_def)
    apply (clarsimp simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def
        arena_lifting isasat_state_simp
     valid_arena_extra_information_mark_to_delete'
      all_init_atms_fmdrop_add_mset_unit learned_clss_l_l_fmdrop
      learned_clss_l_l_fmdrop_irrelev aivdom_inv_dec_remove_clause
      size_Diff_singleton red_in_dom_number_of_learned_ge1 learned_clss_count_def
      clss_size_corr_restart_intro clss_size_corr_restart_simp3
      dest: in_vdom_m_fmdropD dest: in_diffD
      intro: clss_size_corr_restart_intro)
    apply (auto simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def
        arena_lifting
     valid_arena_extra_information_mark_to_delete'
      all_init_atms_fmdrop_add_mset_unit learned_clss_l_l_fmdrop
      learned_clss_l_l_fmdrop_irrelev aivdom_inv_dec_remove_clause
      size_Diff_singleton red_in_dom_number_of_learned_ge1 learned_clss_count_def
      clss_size_corr_restart_intro clss_size_corr_restart_simp3
      dest: in_vdom_m_fmdropD dest: in_diffD
      intro: clss_size_corr_restart_intro)
    done
  done

lemma remove_one_annot_true_clause_one_imp_wl_pre_fst_le_uint32:
  assumes ‹(x, y) ∈ nat_rel ×f {p. (fst p, snd p) ∈ twl_st_heur_restart_ana r ∧
          learned_clss_count (fst p) ≤ u}› and
    ‹remove_one_annot_true_clause_one_imp_wl_pre (fst y) (snd y)›
  shows ‹fst x + 1 ≤ Suc (unat32_max div 2)›
proof -
  have [simp]: ‹fst y = fst x›
    using assms by (cases x, cases y) auto
  have ‹fst x < length (get_trail_wl (snd y))›
    using assms apply -
    unfolding
     remove_one_annot_true_clause_one_imp_wl_pre_def
     remove_one_annot_true_clause_one_imp_pre_def
   by normalize_goal+ auto
  moreover have ‹(get_trail_wl_heur (snd x), get_trail_wl (snd y)) ∈ trail_pol (all_init_atms_st (snd y))›
    using assms
    by (cases x, cases y) (simp add: twl_st_heur_restart_ana_def
      twl_st_heur_restart_def all_init_atms_st_def)
  ultimately show ‹?thesis›
    by (auto simp add: trail_pol_alt_def)
qed

lemma remove_one_annot_true_clause_one_imp_wl_alt_def:
‹remove_one_annot_true_clause_one_imp_wl = (λi S. do {
      ASSERT(remove_one_annot_true_clause_one_imp_wl_pre i S);
      ASSERT(is_proped (rev (get_trail_wl S) ! i));
      (L, C) ← SPEC(λ(L, C). (rev (get_trail_wl S))!i = Propagated L C);
      ASSERT(Propagated L C ∈ set (get_trail_wl S));
      ASSERT(L ∈# all_init_lits_of_wl S);
      if C = 0 then RETURN (i+1, S)
      else do {
        ASSERT(C ∈# dom_m (get_clauses_wl S));
	S ← replace_annot_wl L C S;
        _ ← RETURN (log_clause S C);
	S ← remove_and_add_cls_wl C S;
        RETURN (i+1, S)
      }
  })›
  by (auto simp: remove_one_annot_true_clause_one_imp_wl_def log_clause_def cong: if_cong)


lemma log_clause_heur_log_clause2_ana:
  assumes ‹(S,T) ∈ twl_st_heur_restart_ana' r u› ‹(C,C') ∈ nat_rel›
  shows ‹log_clause_heur S C ≤⇓unit_rel (log_clause2 T C')›
proof -
  have [refine0]: ‹(0,0)∈nat_rel›
    by auto
  have length: ‹⇓ nat_rel ((RETURN ∘ (λc. length (get_clauses_wl T ∝ c))) C') ≤ SPEC (λc. (c, length (get_clauses_wl T ∝ C')) ∈ {(a,b). a=b ∧ a = length (get_clauses_wl T ∝ C)})›
    by (use assms in auto)
  show ?thesis
    unfolding log_clause_heur_def log_clause2_def comp_def uncurry_def mop_arena_length_st_def
      mop_access_lit_in_clauses_heur_def
    apply (refine_vcg mop_arena_lit[where vdom = ‹set (get_vdom S)› and N = ‹get_clauses_wl T›, THEN order_trans] 
      mop_arena_length[where vdom = ‹set (get_vdom S)›, THEN fref_to_Down_curry, THEN order_trans, unfolded prod.simps])
    apply assumption
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
    apply (rule length)
    subgoal by (use assms in ‹auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest: arena_lifting(10)›)
    subgoal by auto
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
    apply assumption
    subgoal by (use assms in auto)
    apply (rule refl)
    subgoal by auto
    by auto
qed

lemma log_del_clause_heur_log_clause:
  assumes ‹(S,T) ∈ twl_st_heur_restart_ana' r u› ‹(C,C') ∈ nat_rel› ‹C ∈# dom_m (get_clauses_wl T)›
  shows ‹log_del_clause_heur S C ≤ SPEC (λc. (c, log_clause T C') ∈ unit_rel)›
    unfolding log_del_clause_heur_alt_def
    apply (rule log_clause_heur_log_clause2_ana[THEN order_trans, OF assms(1,2)])
    apply (rule order_trans)
    apply (rule ref_two_step')
    apply (rule log_clause2_log_clause[THEN fref_to_Down_curry])
    using assms by auto

lemma remove_one_annot_true_clause_one_imp_wl_D_heur_remove_one_annot_true_clause_one_imp_wl_D:
  ‹(uncurry remove_one_annot_true_clause_one_imp_wl_D_heur,
    uncurry remove_one_annot_true_clause_one_imp_wl) ∈
    nat_rel ×f twl_st_heur_restart_ana' r u →f
    ⟨nat_rel ×f twl_st_heur_restart_ana' r u⟩nres_rel›
  unfolding remove_one_annot_true_clause_one_imp_wl_D_heur_def
    remove_one_annot_true_clause_one_imp_wl_alt_def case_prod_beta uncurry_def
  apply (intro frefI nres_relI)
  subgoal for x y
  apply (refine_rcg get_literal_and_reason[where r=r]
    isasat_replace_annot_in_trail_replace_annot_in_trail_spec
      [where r=r and u=u] log_del_clause_heur_log_clause
    mark_garbage_heur4_remove_and_add_cls_l[where r=r and u=u])
  subgoal
    by (auto simp: prod_rel_fst_snd_iff)
  subgoal unfolding remove_one_annot_true_clause_one_imp_wl_pre_def
    by auto
  subgoal
    by (rule remove_one_annot_true_clause_one_imp_wl_pre_fst_le_uint32)
  subgoal for p pa
    by (cases pa)
      (auto simp: all_init_atms_def simp del: all_init_atms_def[symmetric])
  subgoal
    by (cases x, cases y)
     (fastforce simp: twl_st_heur_restart_def
       trail_pol_alt_def)+
  subgoal by auto
  subgoal for p pa
    by (cases pa; cases p; cases x; cases y)
      (auto simp: all_init_atms_def learned_clss_count_def simp del: all_init_atms_def[symmetric])
  apply (solves auto)
  subgoal by auto
  subgoal in_dom_m for p pa S Sa
    unfolding mark_garbage_pre_def
      arena_is_valid_clause_idx_def
      prod.case
    apply (case_tac Sa; cases y)
    apply (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
    done
  subgoal for p pa S Sa
    using in_dom_m
    unfolding mark_garbage_pre_def
      arena_is_valid_clause_idx_def
      prod.case
    apply (rule_tac x = ‹get_clauses_wl Sa› in exI)
    apply (rule_tac x = ‹set (get_vdom S)› in exI)
    apply (case_tac Sa; cases y)
    apply (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
    done
  subgoal for p pa S Sa
    unfolding arena_is_valid_clause_vdom_def
    apply (rule_tac x = ‹get_clauses_wl Sa› in exI)
    apply (rule_tac x = ‹set (get_vdom S)› in exI)
    apply (case_tac Sa; cases y)
    apply (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def)
    done
  subgoal
    by (auto simp: prod_rel_fst_snd_iff dest: get_learned_count_learned_clss_countD)
  subgoal
    by (auto simp: prod_rel_fst_snd_iff dest: get_learned_count_learned_clss_countD)
  subgoal
    by auto
  subgoal
    by (cases x, cases y) fastforce
  done
  done

lemma remove_one_annot_trail_zeroed_until_state:
  assumes
    ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
    ‹(isa_length_trail_pre ∘ get_trail_wl_heur) x› and
    ‹(k, ka) ∈ nat_rel› and
    ka: ‹ka ∈ {k. (∃M1 M2 K.
         (Decided K # M1, M2)
         ∈ set (get_all_ann_decomposition (get_trail_wl y)) ∧
         count_decided M1 = 0 ∧ k = length M1) ∨
        count_decided (get_trail_wl y) = 0 ∧ k = length (get_trail_wl y)}›
  shows ‹trail_zeroed_until_state x ≤ ka› (is ?A) and
    ‹j < trail_zeroed_until_state x ⟹ is_proped (rev (get_trail_wl y) ! j)› (is ‹?X ⟹ ?B›)and
    ‹j < trail_zeroed_until_state x ⟹ mark_of (rev (get_trail_wl y) ! j) = 0› (is ‹?X ⟹ ?C›)
proof -
  define 𝒜 where ‹𝒜 = (all_init_atms (get_clauses_wl y)
       (IsaSAT_Setup.get_unkept_unit_init_clss_wl y +
        IsaSAT_Setup.get_kept_unit_init_clss_wl y +
        get_subsumed_init_clauses_wl y +
        get_init_clauses0_wl y))›
  have ‹(get_trail_wl_heur x, get_trail_wl y) ∈ trail_pol 𝒜›
    using assms(1) unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def 𝒜_def
    by fast
  then show ?A
    ‹?X ⟹ ?B›
    ‹?X ⟹ ?C›
    using ka
    apply (auto simp: trail_pol_def zeroed_trail_def trail_zeroed_until_state_def
      trail_zeroed_until_def)
    by (meson annotated_lit.distinct_disc(1) get_pos_of_level_in_trail_decomp_iff leI)
qed

lemma remove_one_annot_true_clause_imp_wl_alt_def:
  ‹remove_one_annot_true_clause_imp_wl = (λS. do {
    k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_wl S)) ∧
        count_decided M1 = 0 ∧ k = length M1)
      ∨ (count_decided (get_trail_wl S) = 0 ∧ k = length (get_trail_wl S)));
    start ← SPEC (λi. i ≤ k ∧ (∀j < i. is_proped (rev (get_trail_wl S) ! j) ∧ mark_of (rev (get_trail_wl S) ! j) = 0));
    (i, T) ← WHILET⇗remove_one_annot_true_clause_imp_wl_inv S⇖
      (λ(i, S). i < k)
      (λ(i, S). remove_one_annot_true_clause_one_imp_wl i S)
    (start, S);
    ASSERT (remove_one_annot_true_clause_imp_wl_inv S (i, T));
    T ← RETURN T;
    remove_all_learned_subsumed_clauses_wl T
  })›
  unfolding remove_one_annot_true_clause_imp_wl_def Let_def by auto

definition remove_one_annot_true_clause_imp_wl_D_heur :: ‹isasat ⇒ isasat nres›
where
‹remove_one_annot_true_clause_imp_wl_D_heur = (λS. do {
    ASSERT((isa_length_trail_pre o get_trail_wl_heur) S);
    k ← (if count_decided_st_heur S = 0
      then RETURN (isa_length_trail (get_trail_wl_heur S))
      else get_pos_of_level_in_trail_imp (get_trail_wl_heur S) 0);
    let start = trail_zeroed_until_state S;
    (i, T) ← WHILET⇗remove_one_annot_true_clause_imp_wl_D_heur_inv S⇖
      (λ(i, S). i < k)
      (λ(i, S). remove_one_annot_true_clause_one_imp_wl_D_heur i S)
      (start, S);
    ASSERT (remove_one_annot_true_clause_imp_wl_D_heur_inv S (i, T));
    T ← RETURN (trail_set_zeroed_until_state i T);
    RETURN (empty_US_heur T)
  })›

lemma remove_one_annot_true_clause_trail_set_zeroed_until_state:
    ‹(x, y) ∈ twl_st_heur_restart_ana' r u ⟹
    (xa, x') ∈ nat_rel ×f twl_st_heur_restart_ana' r (learned_clss_count x) ⟹
    x' = (x1, x2) ⟹
    xa = (x1a, x2a) ⟹
    remove_one_annot_true_clause_imp_wl_inv y (x1, x2) ⟹
    remove_one_annot_true_clause_imp_wl_D_heur_inv x (x1a, x2a) ⟹
    (trail_set_zeroed_until_state x1a x2a, x2)
  ∈ twl_st_heur_restart_ana' r u›
  supply [[goals_limit=1]]
  apply (simp add: twl_st_heur_restart_ana_def trail_set_zeroed_until_state_def
    twl_st_heur_restart_def)
  apply (rule trail_set_zeroed_until_rel)
  apply (solves simp)
  unfolding remove_one_annot_true_clause_imp_wl_D_heur_inv_def
    remove_one_annot_true_clause_imp_wl_inv_def remove_one_annot_true_clause_imp_inv_def
    prod.simps
  apply normalize_goal+
  apply (simp add: zeroed_trail_def)
  done


find_theorems trail_set_zeroed_until

lemma remove_one_annot_true_clause_imp_wl_D_heur_remove_one_annot_true_clause_imp_wl_D:
  ‹(remove_one_annot_true_clause_imp_wl_D_heur, remove_one_annot_true_clause_imp_wl) ∈
  twl_st_heur_restart_ana' r u →f
  ⟨twl_st_heur_restart_ana' r u⟩nres_rel›
  (is ‹_ ∈ ?A →f _›)
  unfolding remove_one_annot_true_clause_imp_wl_alt_def
    remove_one_annot_true_clause_imp_wl_D_heur_def
  apply (intro frefI nres_relI)
  subgoal for x y
  apply (refine_vcg
    WHILEIT_refine[where R = ‹nat_rel ×r {(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧ learned_clss_count S ≤ learned_clss_count x}›]
    remove_one_annot_true_clause_one_imp_wl_D_heur_remove_one_annot_true_clause_one_imp_wl_D[THEN fref_to_Down_curry])
  subgoal by (auto simp: trail_pol_alt_def isa_length_trail_pre_def
    twl_st_heur_restart_def twl_st_heur_restart_ana_def)
  subgoal by (auto dest: twl_st_heur_restart_isa_length_trail_get_trail_wl
   simp: twl_st_heur_restart_count_decided_st_alt_def mop_isa_length_trail_def)
  subgoal
    apply (rule order_trans)
    apply (rule get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail_CS[THEN fref_to_Down_curry,
        of ‹get_trail_wl y› 0 _ _ ‹all_init_atms_st y›])
    subgoal by (auto simp: get_pos_of_level_in_trail_pre_def
      twl_st_heur_restart_count_decided_st_alt_def)
    subgoal by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def
        all_init_atms_st_def get_unit_init_clss_wl_alt_def)
    subgoal
      apply (subst get_pos_of_level_in_trail_decomp_iff)
      apply (solves ‹auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def›)
      apply (auto simp: get_pos_of_level_in_trail_def
        twl_st_heur_restart_count_decided_st_alt_def)
      done
    done
    subgoal by (rule remove_one_annot_trail_zeroed_until_state)
    subgoal by (rule remove_one_annot_trail_zeroed_until_state)
    subgoal by (rule remove_one_annot_trail_zeroed_until_state)
    subgoal by auto
    subgoal for k k' start T T'
      apply (subst (asm)(11) surjective_pairing)
      apply (subst (asm)(15) surjective_pairing)
      unfolding remove_one_annot_true_clause_imp_wl_D_heur_inv_def
        prod_rel_iff
      apply (subst (8) surjective_pairing, subst prod.case)
      apply (rule_tac x=y in exI)
      apply (rule_tac x= ‹snd T'› in exI)
      by (auto intro: twl_st_heur_restart_anaD simp: prod_rel_fst_snd_iff twl_st_heur_restart_anaD)
    subgoal by auto
    subgoal by auto
    subgoal for k k' start T T'
      apply (subst (asm)(11) surjective_pairing)
      apply (subst (asm)(15) surjective_pairing)
      unfolding remove_one_annot_true_clause_imp_wl_D_heur_inv_def
        prod_rel_iff
      apply (subst (8) surjective_pairing, subst prod.case)
      apply (rule_tac x=y in exI)
      apply (rule_tac x= ‹snd T'› in exI)
      by (auto intro: twl_st_heur_restart_anaD simp: prod_rel_fst_snd_iff twl_st_heur_restart_anaD)
    apply (rule remove_one_annot_true_clause_trail_set_zeroed_until_state)
    apply assumption+
    subgoal for k ka start xa x' x1 x2
      by (auto intro!: remove_all_learned_subsumed_clauses_wl_id)
  done
  done


lemmas iterate_over_VMTF_def =
  iterate_over_VMTF_alt_def[unfolded iterate_over_VMTFC_def simp_thms]

definition iterate_over_ℒallC where
  ‹iterate_over_ℒallC = (λf 𝒜0 I P x. do {
    𝒜 ← SPEC(λ𝒜. set_mset 𝒜 = set_mset 𝒜0 ∧ distinct_mset 𝒜);
    (_, x) ← WHILET⇗λ(𝒜, x). I 𝒜 x⇖
      (λ(ℬ, x). ℬ ≠ {#} ∧ P x)
      (λ(ℬ, x). do {
        ASSERT(ℬ ≠ {#});
        A ← SPEC (λA. A ∈# ℬ);
        x ← f A x;
        RETURN (remove1_mset A ℬ, x)
      })
      (𝒜, x);
    RETURN x
  })›

definition iterate_over_ℒall :: ‹_› where
  iterate_over_ℒall_alt_def: ‹iterate_over_ℒall f 𝒜 I  = iterate_over_ℒallC f 𝒜 I (λ_. True)›

lemmas iterate_over_ℒall_def =
  iterate_over_ℒall_alt_def[unfolded iterate_over_ℒallC_def simp_thms]


lemma iterate_over_VMTFC_iterate_over_ℒallC:
  fixes x :: 'a
  assumes vmtf: ‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M› and
    nempty: ‹𝒜 ≠ {#}› ‹isasat_input_bounded 𝒜› and
    II': ‹⋀x ℬ. set_mset ℬ ⊆ set_mset 𝒜 ⟹ I' ℬ x ⟹ I x› and
    ‹⋀x. I x ⟹ P x = Q x›
  shows ‹iterate_over_VMTFC f I P (ns, Some fst_As) x ≤ ⇓ Id (iterate_over_ℒallC f 𝒜 I' Q x)›
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    ‹fst_As = hd (ys' @ xs')› and
    ‹lst_As = last (ys' @ xs')› and
    vmtf_ℒ: ‹vmtf_ℒall 𝒜 M (set xs', set ys')› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    le: ‹∀L∈atms_of (ℒall 𝒜). L < length ns›
    using vmtf unfolding vmtf_def
    by blast
  define zs where ‹zs = ys' @ xs'›
  define is_lasts where
    ‹is_lasts ℬ n m ⟷ set_mset ℬ = set (drop m zs) ∧ set_mset ℬ ⊆ set_mset 𝒜 ∧
        distinct_mset ℬ ∧
        card (set_mset ℬ) ≤ length zs ∧
        card (set_mset ℬ) + m = length zs ∧
        (n = option_hd (drop m zs)) ∧
        m ≤ length zs› for ℬ and n :: ‹nat option› and m
  have card_𝒜: ‹card (set_mset 𝒜) = length zs›
    ‹set_mset 𝒜 = set zs› and
    nempty': ‹zs ≠ []› and
    dist_zs: ‹distinct zs›
    using vmtf_ℒ vmtf_ns_distinct[OF vmtf_ns] nempty
    unfolding vmtf_ℒall_def eq_commute[of _ ‹atms_of _›] zs_def
    by (auto simp: atms_of_ℒall_𝒜in card_Un_disjoint distinct_card)
  have hd_zs_le: ‹hd zs < length ns›
    using vmtf_ns_le_length[OF vmtf_ns, of ‹hd zs›] nempty'
    unfolding zs_def[symmetric]
    by auto
  have [refine0]: ‹
       (the x1a, A) ∈ nat_rel ⟹
       x = x2b ⟹
       f (the x1a) x2b ≤ ⇓ Id (f A x)› for x1a A x x2b
      by auto
  define iterate_over_VMTF2 where
    ‹iterate_over_VMTF2 ≡ (λf (I :: 'a ⇒ bool) (vm :: (nat, nat) vmtf_node list, n) x. do {
      let _ = remdups_mset 𝒜;
      (_, _, x) ← WHILET⇗λ(n,m, x). I x⇖
        (λ(n, _, x). n ≠ None ∧ P x)
        (λ(n, m, x). do {
          ASSERT(n ≠ None);
          let A = the n;
          ASSERT(A < length ns);
          ASSERT(A ≤ unat32_max div 2);
          x ← f A x;
          RETURN (get_next ((ns ! A)), Suc m, x)
        })
        (n, 0, x);
      RETURN x
    })›
  have iterate_over_VMTF2_alt_def:
    ‹iterate_over_VMTF2 ≡ (λf (I :: 'a ⇒ bool) (vm :: (nat, nat) vmtf_node list, n) x. do {
      (_, _, x) ← WHILET⇗λ(n,m, x). I x⇖
        (λ(n, _, x). n ≠ None ∧ P x)
        (λ(n, m, x). do {
          ASSERT(n ≠ None);
          let A = the n;
          ASSERT(A < length ns);
          ASSERT(A ≤ unat32_max div 2);
          x ← f A x;
          RETURN (get_next ((ns ! A)), Suc m, x)
        })
        (n, 0, x);
      RETURN x
    })›
    unfolding iterate_over_VMTF2_def by force
  have nempty_iff: ‹(x1 ≠ None ∧ P x2a) = (x1b ≠ {#} ∧ Q xb)› (is ‹?A = ?B›)
  if
    ‹(remdups_mset 𝒜, 𝒜') ∈ Id› and
    H: ‹(x, x') ∈ {((n, m, x), 𝒜', y). is_lasts 𝒜' n m ∧ x = y}› and
    ‹case x of (n, m, xa) ⇒ I xa› and
    ‹case x' of (𝒜', x) ⇒ I' 𝒜' x› and
    st[simp]:
      ‹x2 = (x1a, x2a)›
      ‹x = (x1, x2)›
      ‹x' = (x1b, xb)›
    for 𝒜' x x' x1 x2 x1a x2a x1b xb
  proof
    have KK: ‹P x2a = Q xb›
      by (subst assms) (use that in auto)
    show ?A if ?B
      using that H unfolding KK
      by (auto simp: is_lasts_def)
    show ?B if ?A
      using that H unfolding KK
      by (auto simp: is_lasts_def)
  qed
  have IH: ‹((get_next (ns ! the x1a), Suc x1b, xa), remove1_mset A x1, xb)
        ∈ {((n, m, x), 𝒜', y). is_lasts 𝒜' n m ∧ x = y}›
     if
      ‹(remdups_mset 𝒜, 𝒜') ∈ Id› and
      H: ‹(x, x') ∈ {((n, m, x), 𝒜', y). is_lasts 𝒜' n m ∧ x = y}› and
      ‹case x of (n, uu_, x) ⇒ n ≠ None ∧ P x› and
      nempty: ‹case x' of (ℬ, x) ⇒ ℬ ≠ {#} ∧ Q x› and
      ‹case x of (n, m, xa) ⇒ I xa› and
      ‹case x' of (𝒜', x) ⇒ I' 𝒜' x› and
      st:
        ‹x' = (x1, x2)›
        ‹x2a = (x1b, x2b)›
        ‹x = (x1a, x2a)›
        ‹(xa, xb) ∈ Id› and
      ‹x1 ≠ {#}› and
      ‹x1a ≠ None› and
      A: ‹(the x1a, A) ∈ nat_rel› and
      ‹the x1a < length ns›
      for 𝒜' x x' x1 x2 x1a x2a x1b x2b A xa xb
  proof -
    have [simp]: ‹distinct_mset x1› ‹x1b < length zs›
      using H A nempty
      apply (auto simp: st is_lasts_def simp flip: Cons_nth_drop_Suc)
      apply (cases ‹x1b = length zs›)
      apply auto
      done
    then have [simp]: ‹zs ! x1b ∉ set (drop (Suc x1b) zs)›
      by (auto simp: in_set_drop_conv_nth nth_eq_iff_index_eq dist_zs)
    have [simp]: ‹length zs - Suc x1b + x1b = length zs ⟷ False›
      using ‹x1b < length zs› by presburger
    have ‹vmtf_ns (take x1b zs @ zs ! x1b # drop (Suc x1b) zs) m ns›
      using vmtf_ns
      by (auto simp: Cons_nth_drop_Suc simp flip: zs_def)
    from vmtf_ns_last_mid_get_next_option_hd[OF this]
    show ?thesis
      using H A st
      by (auto simp: st is_lasts_def dist_zs distinct_card distinct_mset_set_mset_remove1_mset
           simp flip: Cons_nth_drop_Suc)
  qed
  have WTF[simp]: ‹length zs - Suc 0 = length zs ⟷ zs = []›
    by (cases zs) auto
  have zs2: ‹set (xs' @ ys') = set zs›
    by (auto simp: zs_def)
  have is_lasts_le:  ‹is_lasts x1 (Some A) x1b ⟹ A < length ns› for x2 xb x1b x1 A
    using vmtf_ℒ le nth_mem[of ‹x1b› zs] unfolding is_lasts_def prod.case vmtf_ℒall_def
      set_append[symmetric]zs_def[symmetric] zs2
    by (auto simp: eq_commute[of ‹set zs› ‹atms_of (ℒall 𝒜)›] hd_drop_conv_nth
      simp del: nth_mem)
  have le_unat32_max: ‹the x1a ≤ unat32_max div 2›
    if
      ‹(remdups_mset 𝒜, 𝒜') ∈ Id› and
      ‹(x, x') ∈ {((n, m, x), 𝒜', y). is_lasts 𝒜' n m ∧ x = y}› and
      ‹case x of (n, uu_, x) ⇒ n ≠ None ∧ P x› and
      ‹case x' of (ℬ, x) ⇒ ℬ ≠ {#} ∧ Q x› and
      ‹case x of (n, m, xa) ⇒ I xa› and
      ‹case x' of (𝒜', x) ⇒ I' 𝒜' x› and
      ‹x' = (x1, x2)› and
      ‹x2a = (x1b, xb)› and
      ‹x = (x1a, x2a)› and
      ‹x1 ≠ {#}› and
      ‹x1a ≠ None› and
      ‹(the x1a, A) ∈ nat_rel› and
      ‹the x1a < length ns›
    for 𝒜' x x' x1 x2 x1a x2a x1b xb A
  proof -
    have ‹the x1a ∈# 𝒜›
      using that unfolding is_lasts_def
      by clarsimp (auto simp: is_lasts_def)
    then show ?thesis
      using nempty by (auto dest!: multi_member_split simp: ℒall_add_mset)
  qed
  have  ‹iterate_over_VMTF2 f I (ns, Some fst_As) x ≤ ⇓ Id (iterate_over_ℒallC f 𝒜 I' Q x)›
    unfolding iterate_over_VMTF2_def iterate_over_ℒallC_def prod.case
    apply (refine_vcg WHILEIT_refine[where R = ‹{((n :: nat option, m::nat, x::'a), (𝒜' :: nat multiset, y)).
        is_lasts 𝒜' n m ∧ x = y}›])
    subgoal by simp
    subgoal by simp
    subgoal
      using card_𝒜 fst_As nempty nempty' hd_conv_nth[OF nempty'] hd_zs_le unfolding zs_def[symmetric]
        is_lasts_def
      by (simp_all add:  eq_commute[of ‹remdups_mset _›])
    subgoal for 𝒜' x x' x1 x2 x1a xaa using II'[of ‹_› xaa] unfolding is_lasts_def by auto
    subgoal for 𝒜' x x' x1 x2 x1a x2a x1b xb
      by (rule nempty_iff)
    subgoal by auto
    subgoal for 𝒜' x x' x1 x2 x1a x2a x1b xb
      by (simp add: is_lasts_def in_set_dropI)
    subgoal for 𝒜' x x' x1 x2 x1a x2a x1b xb
      by (auto simp: is_lasts_le)
    subgoal by (rule le_unat32_max)
    subgoal by auto
    subgoal for 𝒜' x x' x1 x2 x1a x2a x1b x2b A xa xb
      by (rule IH)
    subgoal by auto
    done
  moreover have ‹iterate_over_VMTFC f I P (ns, Some fst_As) x  ≤ ⇓ Id (iterate_over_VMTF2 f I (ns, Some fst_As) x)›
    unfolding iterate_over_VMTF2_alt_def iterate_over_VMTFC_def prod.case
    by (refine_vcg WHILEIT_refine[where R = ‹{((n :: nat option, x::'a), (n' :: nat option, m'::nat, x'::'a)).
        n = n' ∧ x = x'}›]) auto
  ultimately show ?thesis
    by simp
qed


lemma iterate_over_VMTF_iterate_over_ℒall:
  fixes x :: 'a
  assumes vmtf: ‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M› and
    nempty: ‹𝒜 ≠ {#}› ‹isasat_input_bounded 𝒜› ‹⋀x ℬ. set_mset ℬ ⊆ set_mset 𝒜 ⟹ I' ℬ x ⟹ I x›
  shows ‹iterate_over_VMTF f I (ns, Some fst_As) x ≤ ⇓ Id (iterate_over_ℒall f 𝒜 I' x)›
  unfolding iterate_over_VMTF_alt_def iterate_over_ℒall_alt_def
  apply (rule iterate_over_VMTFC_iterate_over_ℒallC[OF assms])
  by auto


definition arena_is_packed :: ‹arena ⇒ nat clauses_l ⇒ bool› where
‹arena_is_packed arena N ⟷ length arena = (∑C ∈# dom_m N. length (N ∝ C) + header_size (N ∝ C))›

lemma arena_is_packed_empty[simp]: ‹arena_is_packed [] fmempty›
  by (auto simp: arena_is_packed_def)

lemma arena_is_packed_append:
  assumes ‹arena_is_packed (arena) N› and
    [simp]: ‹length C = length (fst C') + header_size (fst C')› and
    [simp]: ‹a ∉# dom_m N›
  shows ‹arena_is_packed (arena @ C) (fmupd a C' N)›
  using assms(1) by (auto simp: arena_is_packed_def
    intro!: sum_mset_cong)

lemma arena_is_packed_append_valid:
  assumes
    in_dom: ‹fst C ∈# dom_m x1a› and
    valid0: ‹valid_arena x1c x1a vdom0› and
    valid: ‹valid_arena x1d x2a (set x2d)› and
    packed: ‹arena_is_packed x1d x2a› and
    n: ‹n = header_size  (x1a ∝ (fst C))›
  shows ‹arena_is_packed
          (x1d @
           Misc.slice (fst C - n)
            (fst C + arena_length x1c (fst C)) x1c)
          (fmupd (length x1d + n) (the (fmlookup x1a (fst C))) x2a)›
proof -
  have [simp]: ‹length x1d + n ∉# dom_m x2a›
  using valid by (auto dest: arena_lifting(2) valid_arena_in_vdom_le_arena
    simp: arena_is_valid_clause_vdom_def header_size_def)
  have [simp]: ‹arena_length x1c (fst C) = length (x1a ∝ (fst C))› ‹fst C ≥ n›
      ‹fst C - n < length x1c›  ‹fst C < length x1c›
    using valid0 valid in_dom by (auto simp: arena_lifting n less_imp_diff_less)
  have [simp]: ‹length
     (Misc.slice (fst C - n)
       (fst C + length (x1a ∝ (fst C))) x1c) =
     length (x1a ∝ fst C) + header_size (x1a ∝ fst C)›
     using valid in_dom arena_lifting(10)[OF valid0]
     by (fastforce simp: slice_len_min_If min_def arena_lifting(4) simp flip: n)
  show ?thesis
    by (rule arena_is_packed_append[OF packed]) auto
qed

definition move_is_packed :: ‹arena ⇒ _ ⇒ arena ⇒ _ ⇒ bool› where
‹move_is_packed arenao No arena N ⟷
   ((∑C∈#dom_m No. length (No ∝ C) + header_size (No ∝ C)) +
   (∑C∈#dom_m N. length (N ∝ C) + header_size (N ∝ C)) ≤ length arenao)›

lemma valid_arena_header_size:
  ‹valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹ arena_header_size arena C = header_size (N ∝ C)›
  by (auto simp: arena_header_size_def header_size_def arena_lifting)

definition rewatch_spec :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹rewatch_spec = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS).
  SPEC (λ(M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q', WS').
     (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q') = (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q) ∧
     correct_watching' (M, N', D, NE, UE, NEk', UEk', NS', US, N0, U0, Q', WS') ∧
     literals_are_ℒin' (M, N', D, NE, UE, NEk', UEk', NS', US, N0, U0, Q', WS')))›

lemma blits_in_ℒin'_restart_wl_spec0':
  ‹literals_are_ℒin' (a, aq, ab, ac, ad, NEk, UEk, ae, af, N0, U0, Q, b) ⟹
       literals_are_ℒin' (a, aq, ab, ac, ad, NEk, UEk, ae, af, N0, U0, {#}, b)›
  by (auto simp: literals_are_ℒin'_empty blits_in_ℒin'_restart_wl_spec0)

abbreviation twl_st_heur_restart'''u where
  ‹twl_st_heur_restart'''u r u ≡
  {(S, T). (S, T) ∈ twl_st_heur_restart ∧ length (get_clauses_wl_heur S) = r ∧
  learned_clss_count S ≤ u}›

abbreviation twl_st_heur_restart''''u where
  ‹twl_st_heur_restart''''u r u ≡
  {(S, T). (S, T) ∈ twl_st_heur_restart ∧ length (get_clauses_wl_heur S) ≤ r  ∧
  learned_clss_count S ≤ u}›


fun correct_watching''' :: ‹_ ⇒ 'v twl_st_wl ⇒ bool› where
  ‹correct_watching''' 𝒜 (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ⟷
    (∀L ∈# all_lits_of_mm 𝒜.
       distinct_watched (W L) ∧
       (∀(i, K, b)∈#mset (W L).
             i ∈# dom_m N ∧ K ∈ set (N ∝ i) ∧ K ≠ L ∧
             correctly_marked_as_binary N (i, K, b)) ∧
        fst `# mset (W L) = clause_to_update L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}))›

declare correct_watching'''.simps[simp del]

lemma correct_watching'''_add_clause:
  assumes
    corr: ‹correct_watching''' 𝒜 ((a, aa, CD, ac, ad, NEk, UEk, NS, US, N0, U0, Q, b))› and
    leC: ‹2 ≤ length C› and
    i_notin[simp]: ‹i ∉# dom_m aa› and
    dist[iff]: ‹C ! 0 ≠ C ! Suc 0›
  shows ‹correct_watching''' 𝒜
          ((a, fmupd i (C, red) aa, CD, ac, ad, NEk, UEk, NS, US, N0, U0, Q, b
            (C ! 0 := b (C ! 0) @ [(i, C ! Suc 0, length C = 2)],
             C ! Suc 0 := b (C ! Suc 0) @ [(i, C ! 0, length C = 2)])))›
proof -
  have [iff]: ‹C ! Suc 0 ≠ C ! 0›
    using  ‹C ! 0 ≠ C ! Suc 0› by argo
  have [iff]: ‹C ! Suc 0 ∈# all_lits_of_m (mset C)› ‹C ! 0 ∈# all_lits_of_m (mset C)›
    ‹C ! Suc 0 ∈ set C› ‹ C ! 0 ∈ set C› ‹C ! 0 ∈ set (watched_l C)› ‹C ! Suc 0 ∈ set (watched_l C)›
    using leC by (force intro!: in_clause_in_all_lits_of_m nth_mem simp: in_set_conv_iff
        intro: exI[of _ 0] exI[of _ ‹Suc 0›])+
  have [dest!]: ‹⋀L. L ≠ C ! 0 ⟹ L ≠ C ! Suc 0 ⟹ L ∈ set (watched_l C) ⟹ False›
     by (cases C; cases ‹tl C›; auto)+
  have i: ‹i ∉ fst ` set (b L)› if ‹L∈#all_lits_of_mm 𝒜›for L
    using corr i_notin that unfolding correct_watching'''.simps
    by force
  have [iff]: ‹(i,c, d) ∉ set (b L)› if ‹L∈#all_lits_of_mm 𝒜› for L c d
    using i[of L, OF that] by (auto simp: image_iff)
  then show ?thesis
    using corr
    by (force simp: correct_watching'''.simps ran_m_mapsto_upd_notin
        all_lits_of_mm_add_mset all_lits_of_mm_union clause_to_update_mapsto_upd_notin correctly_marked_as_binary.simps
        split: if_splits)
qed


lemma rewatch_correctness:
  assumes empty: ‹⋀L. L ∈# all_lits_of_mm 𝒜 ⟹ W L = []› and
    H[dest]: ‹⋀x. x ∈# dom_m N ⟹ distinct (N ∝ x) ∧ length (N ∝ x) ≥ 2› and
    incl: ‹set_mset (all_lits_of_mm (mset `# ran_mf N)) ⊆ set_mset (all_lits_of_mm 𝒜)›
  shows
    ‹rewatch N W ≤ SPEC(λW. correct_watching''' 𝒜 (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))›
proof -
  define I where
    ‹I ≡ λ(a :: nat list) (b :: nat list) W.
        correct_watching''' 𝒜 ((M, fmrestrict_set (set a) N, C, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))›
  have I0: ‹set_mset (dom_m N) ⊆ set x ∧ distinct x ⟹ I [] x W› for x
    using empty unfolding I_def by (auto simp: correct_watching'''.simps
       all_blits_are_in_problem_init.simps clause_to_update_def
       all_lits_of_mm_union)
  have le: ‹length (σ L) < size (dom_m N)›
     if ‹correct_watching''' 𝒜 (M, fmrestrict_set (set l1) N, C, NE, UE, NEk, UEk, NS, US, N0, U0, Q, σ)› and
      ‹set_mset (dom_m N) ⊆ set x ∧ distinct x› and
     ‹x = l1 @ xa # l2› ‹xa ∈# dom_m N› ‹L ∈ set (N ∝ xa)›
     for L l1 σ xa l2 x
  proof -
    have 1: ‹card (set l1) ≤ length l1›
      by (auto simp: card_length)
    have ‹L ∈# all_lits_of_mm 𝒜›
      using that incl in_clause_in_all_lits_of_m[of L ‹mset (N ∝ xa)›]
      by (auto simp: correct_watching'''.simps dom_m_fmrestrict_set' ran_m_def
          all_lits_of_mm_add_mset all_lits_of_m_add_mset atm_of_all_lits_of_m
          in_all_lits_of_mm_ain_atms_of_iff
        dest!: multi_member_split)
    then have ‹distinct_watched (σ L)› and ‹fst ` set (σ L) ⊆ set l1 ∩ set_mset (dom_m N)›
      using that incl
      by (auto simp: correct_watching'''.simps dom_m_fmrestrict_set' dest!: multi_member_split)
    then have ‹length (map fst (σ L)) ≤ card (set l1 ∩ set_mset (dom_m N))›
      using 1 by (subst distinct_card[symmetric])
       (auto simp: distinct_watched_alt_def intro!: card_mono intro: order_trans)
    also have ‹... < card (set_mset (dom_m N))›
      using that by (auto intro!: psubset_card_mono)
    also have ‹... = size (dom_m N)›
      by (simp add: distinct_mset_dom distinct_mset_size_eq_card)
    finally show ?thesis by simp
  qed
  show ?thesis
    unfolding rewatch_def
    apply (refine_vcg
      nfoldli_rule[where I = ‹I›])
    subgoal by (rule I0)
    subgoal using assms unfolding I_def by auto
    subgoal for x xa l1 l2 σ  using H[of xa] unfolding I_def apply -
      by (rule, subst (asm)nth_eq_iff_index_eq)
        linarith+
    subgoal for x xa l1 l2 σ unfolding I_def by (rule le) (auto intro!: nth_mem)
    subgoal for x xa l1 l2 σ unfolding I_def by (drule le[where L = ‹N ∝ xa ! 1›]) (auto simp: I_def dest!: le)
    subgoal for x xa l1 l2 σ
      unfolding I_def
      by (cases ‹the (fmlookup N xa)›)
       (auto intro!: correct_watching'''_add_clause simp: dom_m_fmrestrict_set')
    subgoal
      unfolding I_def
      by auto
    subgoal by auto
    subgoal unfolding I_def
      by (auto simp: fmlookup_restrict_set_id')
    done
qed

lemma heuristic_rel_incr_restartI[intro!]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_restart_phase_end end_of_phase heur)›
  by (auto simp: heuristic_rel_def heuristic_rel_stats_def incr_restart_phase_end_def)

lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana:
  ‹(RETURN o get_conflict_wl_is_None_heur,  RETURN o get_conflict_wl_is_None) ∈
    twl_st_heur_restart_ana' r (u) →f ⟨Id⟩nres_rel›
  unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
  apply (intro frefI nres_relI) apply refine_rcg
  by (auto simp: twl_st_heur_restart_ana_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
      option_lookup_clause_rel_def twl_st_heur_restart_def
     split: option.splits)
lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None_restart:
  ‹(RETURN o get_conflict_wl_is_None_heur,  RETURN o get_conflict_wl_is_None) ∈
    twl_st_heur_restart →f ⟨Id⟩nres_rel›
  unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
  apply (intro frefI nres_relI) apply refine_rcg
  by (auto simp: twl_st_heur_restart_ana_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
      option_lookup_clause_rel_def twl_st_heur_restart_def
     split: option.splits)

(*TODO rename*)
lemma all_init_atms_alt_def:
  ‹all_init_atms (get_clauses_wl S')
        (IsaSAT_Setup.get_unkept_unit_init_clss_wl S' + IsaSAT_Setup.get_kept_unit_init_clss_wl S' + get_subsumed_init_clauses_wl S' +
  get_init_clauses0_wl S') = all_init_atms_st S'›
  by (auto simp: all_init_atms_st_def IsaSAT_Setup.get_unit_init_clss_wl_alt_def)

lemma twl_st_heur_restart_state_simp:
  assumes ‹(S, S') ∈ twl_st_heur_restart›
  shows
     twl_st_heur_state_simp_watched: ‹C ∈# ℒall (all_init_atms_st S') ⟹
       watched_by_int S C = watched_by S' C›
      ‹C ∈# ℒall (all_init_atms_st S') ⟹
       get_watched_wl_heur S ! (nat_of_lit C) =  get_watched_wl S' C›and
     ‹literals_to_update_wl S' =
         uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev (get_trail_wl S')))› and
     twl_st_heur_state_simp_watched2: ‹C ∈# ℒall (all_init_atms_st S') ⟹
       nat_of_lit C < length(get_watched_wl_heur S)›
  using assms unfolding twl_st_heur_restart_def
  by (solves ‹cases S; cases S'; auto simp add: Let_def map_fun_rel_def ac_simps all_init_atms_st_def›)+

lemma twl_st_heur_restart_ana_state_simp:
  assumes ‹(S, S') ∈ twl_st_heur_restart_ana u›
  shows
     twl_st_heur_restart_ana_state_simp_watched: ‹C ∈# ℒall (all_init_atms_st S') ⟹
       watched_by_int S C = watched_by S' C›
      ‹C ∈# ℒall (all_init_atms_st S') ⟹
       get_watched_wl_heur S ! (nat_of_lit C) =  get_watched_wl S' C›and
     ‹literals_to_update_wl S' =
         uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev (get_trail_wl S')))› and
     twl_st_heur_restart_ana_state_simp_watched2: ‹C ∈# ℒall (all_init_atms_st S') ⟹
       nat_of_lit C < length(get_watched_wl_heur S)›
  using assms twl_st_heur_restart_state_simp[of S S'] unfolding twl_st_heur_restart_ana_def
  by (auto simp: )

lemma twl_st_heur_restart_ana_watchlist_in_vdom:
  ‹get_watched_wl_heur x2e ! nat_of_lit L ! x1d = (a, b) ⟹
  (x2e, x2f) ∈ twl_st_heur_restart_ana r ⟹ L ∈# ℒall (all_init_atms_st x2f) ⟹
  x1d < length (get_watched_wl_heur x2e ! nat_of_lit L) ⟹
    a ∈ set (get_vdom x2e)›
  apply (drule nth_mem)
  by (subst (asm) twl_st_heur_restart_ana_state_simp, assumption, assumption)+
   (auto 5 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def vdom_m_def
    all_init_atms_alt_def
    dest!: multi_member_split)

lemma twl_st_heur_restart_alt_def2:
  ‹twl_st_heur_restart =
  {(S,T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_init_atms_st T) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_init_atms_st T) ∧
    (D = None ⟶ j ≤ length M) ∧
    Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D0 (all_init_atms_st T)) ∧
    vm ∈ bump_heur (all_init_atms_st T) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_init_atms_st T) cach ∧
    out_learned M D outl ∧
    clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} lcount ∧
    vdom_m (all_init_atms_st T) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_init_atms_st T) ∧
    isasat_input_nempty (all_init_atms_st T) ∧
    old_arena = [] ∧
      heuristic_rel (all_init_atms_st T) heur ∧
    (occs, empty_occs_list (all_init_atms_st T)) ∈ occurrence_list_ref
  }›
  unfolding twl_st_heur_restart_def Let_def
  by (auto simp: all_init_atms_st_def)

lemma length_watched_le_ana:
  assumes
    prop_inv: ‹correct_watching'_leaking_bin x1› and
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur_restart_ana r› and
    x2': ‹x2 ∈# ℒall (all_init_atms_st x1)›
  shows ‹length (watched_by x1 x2) ≤ r - MIN_HEADER_SIZE›
proof -
  have x2: ‹x2 ∈# all_init_lits_of_wl x1›
    using ℒall_all_init_atms(2) x2' by blast
  have dist: ‹distinct_watched (watched_by x1 x2)›
    using prop_inv x2 unfolding all_atms_def all_lits_def
    by (cases x1; auto simp: correct_watching'_leaking_bin.simps ac_simps all_lits_st_alt_def[symmetric])
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒall_atm_of_all_lits_of_mm correct_watching.simps)
  have dist_vdom: ‹distinct (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def twl_st_heur'_def aivdom_inv_dec_alt_def Let_def)

  have
      valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
    using xb_x'a unfolding all_atms_def all_lits_def
    by (cases x1)
     (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def Let_def)

  have ‹vdom_m (all_init_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_alt_def2 ac_simps Let_def)

  then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
    using x2' unfolding vdom_m_def ℒall_all_atms ℒall_all_init_atms
    by (cases x1)
      (force simp: twl_st_heur'_def twl_st_heur_def
        dest!: multi_member_split)
  have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
    by (rule distinct_subseteq_iff[THEN iffD1])
      (use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
         ‹simp_all flip: distinct_mset_mset_distinct›)
  have vdom_incl: ‹set (get_vdom x1a) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur x1a)}›
    using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto

  have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - MIN_HEADER_SIZE›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ?thesis
    using size_mset_mono[OF watched_incl] xb_x'a
    by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›]
      simp: twl_st_heur_restart_ana_def)
qed

lemma D0_cong': ‹set_mset 𝒜 = set_mset ℬ ⟹ x ∈ D0 𝒜 ⟹ x ∈ D0 ℬ›
  by (subst (asm) D0_cong, assumption)
lemma map_fun_rel_D0_cong: ‹set_mset 𝒜 = set_mset ℬ ⟹x ∈ ⟨Id⟩map_fun_rel (D0 𝒜) ⟹ x ∈ ⟨Id⟩map_fun_rel (D0 ℬ)›
  by (subst (asm) D0_cong, assumption)

lemma vdom_m_cong': "set_mset 𝒜 = set_mset ℬ ⟹ x ∈ vdom_m 𝒜 a b ⟹ x ∈ vdom_m ℬ a b"
  by (subst (asm) vdom_m_cong, assumption)
lemma vdom_m_cong'': "set_mset 𝒜 = set_mset ℬ ⟹ vdom_m 𝒜 a b ⊆ A ⟹ vdom_m ℬ a b ⊆ A"
  by (subst (asm) vdom_m_cong, assumption)
lemma cach_refinement_empty_cong': "set_mset 𝒜 = set_mset ℬ ⟹ cach_refinement_empty 𝒜 x ⟹ cach_refinement_empty ℬ x"
  by (subst (asm) cach_refinement_empty_cong, assumption)

end