Theory Watched_Literals_Algorithm_Reduce

theory Watched_Literals_Algorithm_Reduce
imports Watched_Literals_Algorithm Watched_Literals_Transition_System_Simp
  Watched_Literals_Transition_System_Reduce
  Weidenbach_Book_Base.Explorer
begin

context twl_restart_ops
begin

text ‹
  We refine in two steps. In the first, we refine the transition system directly. Then we simplify
  the stat and remove the unnecessary state and replace them by the counts we need.
›
text ‹Restarts are never necessary›
definition GC_required :: "'v twl_st ⇒ nat ⇒ nat ⇒ bool nres" where
  ‹GC_required S last_GC_learnt_clss n = do {
     ASSERT(size (get_all_learned_clss S) ≥ last_GC_learnt_clss);
     SPEC (λb. b ⟶ size (get_all_learned_clss S) - last_GC_learnt_clss > f n)}›

definition restart_required :: "'v twl_st ⇒ nat ⇒ nat ⇒ bool nres" where
  ‹restart_required S last_Restart_learnt_clss n = do {
    ASSERT(size (get_all_learned_clss S) ≥ last_Restart_learnt_clss);
    SPEC (λb. b ⟶ size (get_all_learned_clss S) > last_Restart_learnt_clss)
  }›

definition inprocessing_required :: "'v twl_st ⇒ bool nres" where
  ‹inprocessing_required S = do {
    SPEC (λb. True)
  }›

definition (in -) restart_prog_pre_int :: ‹'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st ⇒ bool ⇒ bool› where
  ‹restart_prog_pre_int last_GC last_Restart S brk ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
    (¬brk ⟶ get_conflict S = None) ∧
    size (get_all_learned_clss S) ≥ size (get_all_learned_clss last_Restart) ∧
    size (get_all_learned_clss S) ≥ size (get_all_learned_clss last_GC) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›

definition restart_prog_int
  :: ‹'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st ⇒ nat ⇒ nat ⇒ bool ⇒ ('v twl_st × 'v twl_st × 'v twl_st × nat × nat) nres›
where
  ‹restart_prog_int last_GC last_Restart S m n brk = do {
     ASSERT(restart_prog_pre_int last_GC last_Restart S brk);
     b ← GC_required S (size (get_all_learned_clss last_GC)) n;
     b2 ← restart_required S  (size (get_all_learned_clss last_Restart))  n;
     if b2 ∧ ¬brk then do {
       T ← SPEC(λT. cdcl_twl_restart_only S T);
       RETURN (last_GC, T, T, Suc m, n)
     }
     else if b ∧ ¬brk then do {
       b ← inprocessing_required S;
       if ¬b then do {
         T  ← SPEC(λT. cdcl_twl_restart S T);
         RETURN (T, T, T, m, Suc n)
      }
      else do {
         T ← SPEC(λT. cdcl_twl_inp** S T ∧ count_decided (get_trail T) = 0);
         RETURN (T, T, T, m, Suc n)
      }
    }
    else
      RETURN (last_GC, last_Restart, S, m, n)
  }›

fun cdcl_twl_stgy_restart_prog_int_inv where
  ‹cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0) (brk, R, S, T, m, n) ⟷
    twl_restart_inv (S0, T0, U0, m0, n0, True) ∧
    twl_stgy_restart_inv (S0, T0, U0, m0, n0, True) ∧
    (brk ⟶ final_twl_state T) ∧
    cdcl_twl_stgy_restart** (S0, T0, U0, m0, n0, True) (R, S, T, m, n, ¬brk) ∧
    clauses_to_update T = {#} ∧ (¬brk ⟶ get_conflict T = None)›

lemmas cdcl_twl_stgy_restart_prog_int_inv_def[simp del] =
  cdcl_twl_stgy_restart_prog_int_inv.simps

lemma cdcl_twl_stgy_restart_prog_int_inv_alt_def:
  ‹cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0) (brk, R, S, T, m, n) ⟷
    twl_restart_inv (S0, T0, U0, m0, n0, True) ∧
    twl_stgy_restart_inv (S0, T0, U0, m0, n0, True) ∧
    twl_stgy_restart_inv (R, S, T, m, n, ¬brk) ∧
    twl_restart_inv (R, S, T, m, n, ¬brk) ∧
    (brk ⟶ final_twl_state T) ∧
    cdcl_twl_stgy_restart** (S0, T0, U0, m0, n0, True) (R, S, T, m, n, ¬brk) ∧
  clauses_to_update T = {#} ∧ (¬brk ⟶ get_conflict T = None)›
  unfolding cdcl_twl_stgy_restart_prog_int_inv_def
  by (auto dest: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv
    rtranclp_cdcl_twl_stgy_restart_twl_stgy_restart_inv)


text ‹
  In the main loop, and purely to simplify the proof, we remember the state obtained after the last
  restart in order to relate it to the number of clauses. In a first proof attempt, we try to make
  do without it by only assuming its existence, but we could no prove that the loop terminates,
  because the state can change each time.

  This state is not needed at all in the execution and will be removed in the next refinement step.
›
definition cdcl_twl_stgy_restart_prog_intg
  :: "nat ⇒ nat ⇒ 'v twl_st ⇒'v twl_st ⇒'v twl_st ⇒ 'v twl_st nres"
where
  ‹cdcl_twl_stgy_restart_prog_intg m0 n0 S0 T0 U0 =
  do {
    (brk, _, _, T, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0)⇖
      (λ(brk, _). ¬brk)
      (λ(brk, S, S', S'', m,  n).
      do {
        T ← unit_propagation_outer_loop S'';
        (brk, T) ← cdcl_twl_o_prog T;
        (S, S', T, m', n') ← restart_prog_int S S' T m n brk;
        RETURN (brk ∨ get_conflict T ≠ None, S, S', T, m', n')
      })
      (False, S0, T0, U0, m0, n0);
    RETURN T
  }›

abbreviation cdcl_twl_stgy_restart_prog_int where
  ‹cdcl_twl_stgy_restart_prog_int S ≡ cdcl_twl_stgy_restart_prog_intg 0 0 S S S›

lemmas cdcl_twl_stgy_restart_prog_int_def = cdcl_twl_stgy_restart_prog_intg_def

abbreviation cdcl_algo_termination_early_rel
  :: ‹((bool × bool × 'v twl_st × 'v twl_st ×  'v twl_st × nat × nat) × _) set›
where
  ‹cdcl_algo_termination_early_rel ≡
  {((ebrkT :: bool, brkT :: bool, R' :: 'v twl_st, S' :: 'v twl_st, T' :: 'v twl_st, m' :: nat, n' :: nat),
       (ebrkS, brkS, R :: 'v twl_st, S :: 'v twl_st, T :: 'v twl_st, m :: nat, n :: nat)).
     twl_restart_inv (R, S, T, m, n, ¬brkS) ∧ ¬brkS ∧
     cdcl_twl_stgy_restart++ (R, S, T, m, n, ¬brkS) (R', S', T', m', n', ¬brkT)} ∪
  {((ebrkT :: bool, brkT :: bool, R' :: 'v twl_st, S' :: 'v twl_st, T' :: 'v twl_st, m' :: nat, n' :: nat),
  (ebrkS, brkS, R :: 'v twl_st, S :: 'v twl_st, T :: 'v twl_st, m :: nat, n :: nat)).
  ¬brkS ∧ brkT}›

end


context twl_restart
begin

lemma cdcl_twl_stgy_restart_tranclpI:
  ‹cdcl_twl_stgy++ T U ⟹ cdcl_twl_stgy_restart++ (R, S, T, m, n, True) (R, S, U, m, n, True)›
  by (induction rule: tranclp_induct)
    (auto dest!: cdcl_twl_stgy_restart.intros(1)[of _ _ R S m n])

lemma cdcl_twl_stgy_restart_rtranclpI:
  ‹cdcl_twl_stgy** T U ⟹ cdcl_twl_stgy_restart** (R, S, T, m, n, True) (R, S, U, m, n, True)›
  by (induction rule: rtranclp_induct)
    (auto dest!: cdcl_twl_stgy_restart.intros(1)[of _ _ R S m n])

lemma  wf_cdcl_algo_termination_early_rel: ‹wf cdcl_algo_termination_early_rel› (is ‹wf (?C ∪ ?D)›)
proof -
  have A: ‹{(T, S :: 'v twl_st_restart). twl_restart_inv S ∧ cdcl_twl_stgy_restart S T}+ =
    {(T, S :: 'v twl_st_restart). twl_restart_inv S ∧ cdcl_twl_stgy_restart++ S T}› (is ‹?A = ?B›)
  proof -
    have ‹(x, y) ∈ ?A ⟹ (x, y) ∈ ?B› for x y
      by (induction rule: trancl_induct)
        auto
    moreover have ‹cdcl_twl_stgy_restart++ S T ⟹ twl_restart_inv S ⟹ (T, S) ∈ ?A› for S T
      apply (induction rule: tranclp_induct)
      subgoal by auto
      subgoal for T U
        by (rule trancl_into_trancl2[of _ T])
          (use rtranclp_cdcl_twl_stgy_restart_twl_restart_inv[of S T] in ‹simp_all add: tranclp_into_rtranclp›)
      done
    ultimately show ?thesis
      by blast
  qed
  have ‹wf ?D›
    by (rule wf_no_loop) auto
  moreover have ‹wf ?C›
    by (rule wf_if_measure_in_wf[OF wf_trancl[OF wf_cdcl_twl_stgy_restart, unfolded A],
        of _  ‹λ(_, brkT, R, S, T, n, n'). (R, S, T, n, n', ¬brkT)›])
      auto
  moreover have ‹?D O ?C ⊆ ?D›
    by auto
  ultimately show ?thesis
    apply (subst Un_commute)
    by (rule wf_union_compatible)
qed

definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_bounded_intg
     :: "nat ⇒ nat ⇒ 'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st ⇒ (bool × 'v twl_st) nres"
where
  ‹cdcl_twl_stgy_restart_prog_bounded_intg m n S0 T0 U0 =
  do {
    ebrk ← RES UNIV;
    (ebrk, _, _, _, T, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m, n) o snd⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, Q, R, S, m, n).
      do {
        T ← unit_propagation_outer_loop S;
        (brk, T) ← cdcl_twl_o_prog T;
        (Q, R, T, m, n) ← restart_prog_int Q R T m n brk;
	ebrk ← RES UNIV;
        RETURN (ebrk, brk ∨ get_conflict T ≠ None, Q, R, T, m, n)
      })
      (ebrk, False, S0, T0, U0, m, n);
    RETURN (ebrk, T)
  }›

abbreviation (in twl_restart_ops) cdcl_twl_stgy_restart_prog_bounded_int where
  ‹cdcl_twl_stgy_restart_prog_bounded_int S ≡ cdcl_twl_stgy_restart_prog_bounded_intg 0 0 S S S›

lemmas cdcl_twl_stgy_restart_prog_bounded_int_def = cdcl_twl_stgy_restart_prog_bounded_intg_def

lemma pcdcl_core_stgy_get_all_learned_clss:
  ‹pcdcl_core_stgy T U ⟹
  size (pget_all_learned_clss T) ≤ size (pget_all_learned_clss U)›
  by (induction rule: pcdcl_core_stgy.induct)
   (cases T; cases U; auto simp: cdcl_conflict.simps cdcl_propagate.simps cdcl_decide.simps
    cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps
    dest!: arg_cong[of ‹clauses _› ‹_› size])+

lemma cdcl_twl_cp_get_all_learned_clss:
  ‹cdcl_twl_cp T U ⟹
    size (get_all_learned_clss T) = size (get_all_learned_clss U)›
  by (induction rule: cdcl_twl_cp.induct)
   (auto simp: update_clauses.simps dest!: multi_member_split)

lemma rtranclp_cdcl_twl_cp_get_all_learned_clss:
  ‹cdcl_twl_cp** T U ⟹
    size (get_all_learned_clss T) = size (get_all_learned_clss U)›
  by (induction rule:rtranclp_induct)
   (auto  dest: cdcl_twl_cp_get_all_learned_clss)

lemma cdcl_twl_o_get_all_learned_clss:
  ‹cdcl_twl_o T U ⟹
    size (get_all_learned_clss T) ≤ size (get_all_learned_clss U)›
  by (induction rule: cdcl_twl_o.induct)
   (auto simp: update_clauses.simps dest!: multi_member_split)

lemma rtranclp_cdcl_twl_o_get_all_learned_clss:
  ‹cdcl_twl_o** T U ⟹
    size (get_all_learned_clss T) ≤ size (get_all_learned_clss U)›
  by (induction rule:rtranclp_induct)
   (auto  dest: cdcl_twl_o_get_all_learned_clss)

lemma rtranclp_pcdcl_stgy_only_restart_pget_all_learned_clss_mono:
  ‹pcdcl_stgy_only_restart** S T ⟹
    size (pget_all_learned_clss S) ≤ size (pget_all_learned_clss T)›
  by (induction rule:rtranclp_induct)
   (auto  dest: pcdcl_stgy_only_restart_pget_all_learned_clss_mono)

lemma cdcl_twl_inp_clauses_to_update:
  ‹cdcl_twl_inp** S T ⟹ clauses_to_update S = {#} ⟹ clauses_to_update T = {#}›
  by (cases rule: rtranclp.cases, assumption)
   (auto simp: cdcl_twl_inp.simps cdcl_twl_subsumed.simps cdcl_twl_subresolution.simps
    cdcl_twl_restart.simps cdcl_twl_unitres.simps cdcl_twl_unitres_true.simps
    cdcl_twl_pure_remove.simps)

lemma restart_prog_bounded_spec:
  assumes
    ‹iebrk ∈ UNIV› and
    inv: ‹(cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0) ∘ snd) (ebrk, brk, S, T, U, m, n)› and
    cond: ‹case (ebrk, brk, S, T, U, m, n) of
     (ebrk, brk, uu_) ⇒ ¬ brk ∧ ¬ ebrk› and
    other_inv: ‹cdcl_twl_o_prog_spec V (brkW, W)› and
    ‹twl_struct_invs V› and
    ‹cdcl_twl_cp** U V› and
    ‹literals_to_update V = {#}› and
    ‹∀S'. ¬ cdcl_twl_cp V S'› and
    ‹twl_stgy_invs V›
  shows ‹restart_prog_int S T W m n brkW
         ≤ SPEC
            (λx. (case x of (Q, R, T, m, n) ⇒ do {
                                ebrk ← RES UNIV;
                                RETURN (ebrk, brkW ∨ get_conflict T ≠ None, Q, R, T, m, n)
                              })
                 ≤ SPEC
                    (λs'. (cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0) ∘ snd) s' ∧
                          (s', ebrk, brk, S, T, U, m, n)
                          ∈ cdcl_algo_termination_early_rel))›
    (is ‹_ ≤ SPEC (λx. _ ≤ SPEC(λs. ?I s ∧ _ ∈ ?term))›)
proof -

  have [simp]: ‹¬brk› ‹¬ebrk›
    using cond by auto
  have struct_invs': ‹cdcl_twl_restart W T' ⟹ cdcl_twl_stgy** T' V' ⟹ twl_struct_invs V'› for T' V'
    using assms(3) cdcl_twl_restart_twl_struct_invs
      by (metis (no_types, lifting) assms(4) case_prodD rtranclp_cdcl_twl_stgy_twl_struct_invs)
  have stgy_invs: ‹cdcl_twl_restart W V' ⟹ cdcl_twl_stgy** V' W' ⟹ twl_stgy_invs W'› for V' W'
    using assms(3) cdcl_twl_restart_twl_stgy_invs
    by (metis (no_types, lifting) assms(4) case_prodD cdcl_twl_restart_twl_struct_invs
      rtranclp_cdcl_twl_stgy_twl_stgy_invs)

  have res_no_clss_to_upd: ‹cdcl_twl_restart U V ⟹ clauses_to_update V = {#}› for V
    by (auto simp: cdcl_twl_restart.simps)
  have res_no_confl: ‹cdcl_twl_restart U V ⟹ get_conflict V = None› for V
    by (auto simp: cdcl_twl_restart.simps)

  have
    struct_invs_S0: ‹twl_struct_invs S0› ‹twl_struct_invs T0› ‹twl_struct_invs U0› and
    struct_invs_S: ‹twl_struct_invs S› and
    struct_invs_T: ‹twl_struct_invs T› and
    struct_invs_U: ‹twl_struct_invs U› and
    twl_stgy_invs_S0: ‹twl_stgy_invs S0›‹twl_stgy_invs T0›‹twl_stgy_invs U0› and
    twl_stgy_invs_S: ‹twl_stgy_invs S› and
    twl_stgy_invs_T: ‹twl_stgy_invs T› and
    twl_stgy_invs_U: ‹twl_stgy_invs U› and
    ‹brk ⟶ final_twl_state U› and
    twl_res: ‹cdcl_twl_stgy_restart** (S0, T0, U0, m0, n0, True) (S, T, U, m, n, ¬ brk)› and
    clss_T: ‹clauses_to_update U = {#}› and
    confl: ‹¬ brk ⟶ get_conflict U = None› and
    STU_inv: ‹pcdcl_stgy_restart_inv (pstateW_of S, pstateW_of T, pstateW_of U, m, n, ¬ brk)› and
    [simp]: ‹twl_restart_inv (S0, T0, U0, m0, n0, True)›
    ‹twl_stgy_restart_inv (S0, T0, U0, m0, n0, True)› and
    init: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
       ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T)›
       ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of U)›
    using inv unfolding cdcl_twl_stgy_restart_prog_int_inv_alt_def prod.case comp_def snd_conv
      twl_restart_inv_def twl_stgy_restart_inv_def by fast+

  have
    cdcl_o: ‹cdcl_twl_o** V W› and
    conflict_W: ‹get_conflict W ≠ None ⟹ count_decided (get_trail W) = 0› and
    brk'_no_step: ‹brkW ⟹ final_twl_state W› and
    struct_invs_W: ‹twl_struct_invs W› and
    stgy_invs_W: ‹twl_stgy_invs W› and
    clss_to_upd_W: ‹clauses_to_update W = {#}› and
    lits_to_upd_W: ‹¬ brkW ⟶ literals_to_update W ≠ {#}› and
    confl_W: ‹¬ brkW ⟶ get_conflict W = None› and
    ent: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of V)›
    using other_inv unfolding final_twl_state_def by fast+
  have ent_W: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of W)›
    using assms(5) rtranclp_cdcl_twl_o_stgyD[OF cdcl_o] ent
      rtranclp_cdcl_twl_stgy_entailed_by_init by blast
  have ‹cdcl_twl_stgy** V W›
    by (meson cdcl_o assms(5) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD
      rtranclp_trans)

  have ‹size (get_all_learned_clss T) ≤ size (get_all_learned_clss W)›
     ‹size (get_all_learned_clss S) ≤ size (get_all_learned_clss W)›
    using STU_inv assms(6) cdcl_o unfolding pcdcl_stgy_restart_inv_def
    by (auto dest!: rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono
      rtranclp_cdcl_twl_cp_get_all_learned_clss rtranclp_cdcl_twl_o_get_all_learned_clss
      rtranclp_pcdcl_stgy_only_restart_pget_all_learned_clss_mono)
  then have restart_W: ‹restart_prog_pre_int S T W brkW›
    using struct_invs_W stgy_invs_W confl_W ent_W unfolding restart_prog_pre_int_def by auto

  have UW: ‹cdcl_twl_stgy_restart** (S, T, U, m, n, True) (S, T, W, m, n, True)›
    apply (rule cdcl_twl_stgy_restart_rtranclpI)
    by (meson ‹cdcl_twl_stgy** V W› assms(6) rtranclp_cdcl_twl_cp_stgyD rtranclp_trans)
  have restart_only: ‹?I (ebrk', False ∨ get_conflict X ≠ None, S, X, X, Suc m, n)› (is ?A) and
    restart_only_term: ‹((ebrk', False ∨ get_conflict X ≠ None, S, X, X, Suc m, n), ebrk, brk, S, T, U, m, n) ∈ ?term› (is ?B)
    if 
      ‹restart_prog_pre_int S T W False› and
      less: ‹True ⟶
      size (get_all_learned_clss T) < size (get_all_learned_clss W)› and
      WX: ‹cdcl_twl_restart_only W X› and
      ‹ebrk' ∈ UNIV› and
      y and
      x
     for x y X ebrk'
  proof -
    have WX': ‹cdcl_twl_stgy_restart (S, T, W, m, n, True) (S, X, X, Suc m, n, True)›
      by (rule cdcl_twl_stgy_restart.intros)
        (use less WX in auto)
    show ?A
      using UW WX twl_res WX' clss_to_upd_W
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def cdcl_twl_restart_only.simps)
    show ?B
      using STU_inv UW WX' init
        by (auto simp: twl_restart_inv_def struct_invs_S struct_invs_T struct_invs_U)
  qed
  have GC: ‹?I (ebrk', False ∨ get_conflict Y ≠ None, Y, Y, Y, m, Suc n)› (is ?A) and
    GC_term: ‹((ebrk', False ∨ get_conflict Y ≠ None, Y, Y, Y, m, Suc n), ebrk, brk, S, T, U, m, n) ∈ ?term› (is ?B)
    if 
      ‹restart_prog_pre_int S T W False› and
      less: ‹True ⟶ f n < size (get_all_learned_clss W) - size (get_all_learned_clss S)› and
      WX: ‹cdcl_twl_inp** W Y›
        ‹count_decided (get_trail Y) = 0› and
      ‹ebrk' ∈ UNIV› and
      ‹¬ brkW›
    for x X Y ebrk' W'
  proof -
    have struct_X: ‹twl_struct_invs Y›
      using rtranclp_cdcl_twl_inp_invs(1)[OF WX(1) struct_invs_W ent_W] .

    have clss: ‹clauses_to_update Y = {#}›
      using cdcl_twl_inp_clauses_to_update[OF WX(1) clss_to_upd_W] .
    have WX': ‹cdcl_twl_stgy_restart (S, T, W, m, n, True) (Y, Y, Y, m, Suc n, True)›
      by (rule cdcl_twl_stgy_restart.intros(2))
        (use less WX clss in ‹auto dest!: cdcl_twl_inp.intros›)
    have ‹count_decided (get_trail Y) = 0 ⟹ get_conflict Y ≠ None ⟹ final_twl_state Y›
      by (auto simp: final_twl_state_def)
    moreover have ‹count_decided (get_trail Y) = 0 ⟹ get_conflict Y ≠ None ⟹
      cdcl_twl_stgy_restart (Y, Y, Y, m, Suc n, True) (Y, Y, Y, m, Suc n, False)›
      by (rule cdcl_twl_stgy_restart.intros)
        (auto simp: pcdcl_twl_final_state_def)
    ultimately show ?A
      using UW WX twl_res WX' clss
      by (cases ‹get_conflict Y = None›) (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def)
    show ?B
      using STU_inv UW WX' init
      by (auto simp: twl_restart_inv_def struct_invs_S struct_invs_T struct_invs_U)
  qed
  have continue: ‹?I (ebrk', brkW' ∨ ¬unsat, S, T, W, m, n)› (is ?A) and
    continue_term: ‹((ebrk', brkW' ∨ ¬unsat, S, T, W, m, n), ebrk, brk, S, T, U, m, n) ∈ ?term› (is ?B)
    if ‹unsat ⟷ get_conflict W = None› ‹brkW' ⟷ brkW›
    for ebrk' unsat brkW'
  proof -
    show ?A
      using brk'_no_step confl_W clss_to_upd_W UW twl_res
        cdcl_twl_stgy_restart.intros(4)[of W S T m n]
      unfolding that
      apply (cases ‹get_conflict W = None›; cases brkW)
      apply (auto simp add: cdcl_twl_stgy_restart_prog_int_inv_def)
      apply (metis (no_types, lifting) final_twl_state_def pcdcl_twl_final_state_def rtranclp.simps rtranclp_trans)+
      done
    have ‹cdcl_twl_stgy++ V W› if ‹¬brkW›
      using  ‹cdcl_twl_stgy** V W› lits_to_upd_W that assms(7) unfolding rtranclp_unfold
      by auto
    then have [simp]: ‹cdcl_twl_stgy_restart++ (S, T, U, m, n, True) (S, T, W, m, n, True)› if ‹¬brkW›
      by (meson assms(6) cdcl_twl_stgy_restart_tranclpI
        rtranclp_cdcl_twl_cp_stgyD rtranclp_tranclp_tranclp that)

    show ?B
      using STU_inv brk'_no_step init
      apply (cases ‹get_conflict W = None›; cases brkW)
      by (auto simp: twl_restart_inv_def struct_invs_S struct_invs_T struct_invs_U that)
  qed
  have noinp_continue: ‹?I (xd, False ∨ get_conflict ab ≠ None, ab, ab, ab, m, Suc n)› (is ?A) and
    noinp_term: ‹((xd, False ∨ get_conflict ab ≠ None, ab, ab, ab, m, Suc n), ebrk, brk, S, T, U, m, n) ∈ ?term›
      (is ?B)
    if
      ‹restart_prog_pre_int S T W False› and
      ‹size (get_all_learned_clss S) ≤ size (get_all_learned_clss W)› and
      less: ‹True ⟶
       f n < size (get_all_learned_clss W) - size (get_all_learned_clss S)› and
      ‹size (get_all_learned_clss T) ≤ size (get_all_learned_clss W)› and
      ‹xa ⟶ size (get_all_learned_clss T) < size (get_all_learned_clss W)› and
      ‹¬ (xa ∧ ¬ False)› and
      WX: ‹cdcl_twl_restart W ab› and
      ‹xd ∈ UNIV› and
      [simp]: x ‹¬ brkW› ‹¬ xb›
      for x xa xb ab xd
  proof -
    have [simp]: ‹get_conflict W = None› ‹get_conflict ab = None› ‹clauses_to_update ab = {#}›
      using that(1) WX
      by (auto simp: restart_prog_pre_int_def cdcl_twl_restart.simps)
    have WX': ‹cdcl_twl_stgy_restart (S, T, W, m, n, True) (ab, ab, ab, m, Suc n, True)›
      by (rule cdcl_twl_stgy_restart.intros(2)[of _ _ _ ab])
        (use less WX in ‹auto dest!: cdcl_twl_inp.intros›)
    then show ?A
      using UW twl_res by (auto simp add: cdcl_twl_stgy_restart_prog_int_inv_def)
    show ?B
      using UW twl_res WX' ‹twl_restart_inv (S0, T0, U0, m0, n0, True)› by (auto
        dest: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv)
  qed

  show ?thesis
    unfolding restart_prog_int_def restart_required_def GC_required_def inprocessing_required_def
    apply (refine_vcg lhs_step_If; remove_dummy_vars)
    subgoal by (rule restart_W)
    subgoal by (auto simp: restart_prog_pre_int_def)
    subgoal by (auto simp: restart_prog_pre_int_def)
    subgoal by (rule restart_only)
    subgoal by (rule restart_only_term)
    subgoal by (rule noinp_continue)
    subgoal by (rule noinp_term)
    subgoal by (rule GC)
    subgoal by (rule GC_term)
    subgoal by (rule continue) auto
    subgoal by (rule continue_term) auto
    done
qed


lemma (in twl_restart) cdcl_twl_stgy_prog_bounded_int_spec:
  fixes n :: nat
  assumes ‹twl_restart_inv (S, T, U, m, n, False)› and
    ‹twl_stgy_restart_inv (S, T, U, m, n, False)› and
    ‹clauses_to_update U = {#}› and
    ‹get_conflict U = None›
  shows
    ‹cdcl_twl_stgy_restart_prog_bounded_intg m n S T U ≤ partial_conclusive_TWL_run2 m n S T U›
  supply RETURN_as_SPEC_refine[refine2 del]
  unfolding cdcl_twl_stgy_restart_prog_bounded_intg_def full_def partial_conclusive_TWL_run2_def
  apply (refine_vcg
    WHILEIT_rule[where
    R = ‹cdcl_algo_termination_early_rel›];
    remove_dummy_vars)
  subgoal
    by (rule wf_cdcl_algo_termination_early_rel)
  subgoal
    using assms by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_restart_inv_def
      twl_struct_invs_def pcdcl_stgy_restart_inv_def twl_stgy_restart_inv_def)
  subgoal
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
      twl_restart_inv_def
      dest!: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv)
  subgoal
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def)
  subgoal
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def)
  subgoal
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
      twl_restart_inv_def
      dest: rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs)
  subgoal
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
      twl_restart_inv_def no_step_cdcl_twl_cp_no_step_cdclW_cp
      dest: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv)
  subgoal by fast
  subgoal for x a aa ab ac ad ae be xa
    using assms
    using
      rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of ‹(S, T, U, m, n, True)›
      ‹(ab, ac, ad, ae, be, True)›]
    by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def
       twl_restart_inv_def
      intro: rtranclp_cdcl_twl_stgy_entailed_by_init
      dest!: rtranclp_cdcl_twl_cp_stgyD
      simp flip:  stateW_of_def)
  subgoal
    by (rule restart_prog_bounded_spec)
  subgoal for x brk T U m n ebrk V
    apply (rule_tac x=T in exI)
    apply (rule_tac x=U in exI)
    apply (rule_tac x= ‹(m, n, ¬brk)› in exI)
    by (auto simp add: cdcl_twl_stgy_restart_prog_int_inv_def)
  done


lemma cdcl_twl_stgy_restart_prog_int_spec:
  fixes S0 :: ‹'v twl_st›
  assumes ‹twl_restart_inv (S0, T0, U0, m0, n0, False)› and
    ‹twl_stgy_restart_inv (S0, T0, U0, m0, n0, False)› and
    ‹clauses_to_update U0 = {#}› and
    ‹get_conflict U0 = None›
  shows
    ‹cdcl_twl_stgy_restart_prog_intg m0 n0 S0 T0 U0 ≤ conclusive_TWL_run2 m0 n0 S0 T0 U0›
proof -
  define RETURN_FALSE where ‹RETURN_FALSE = RETURN False›
  have cdcl_twl_stgy_restart_prog_alt_def:
    ‹cdcl_twl_stgy_restart_prog_intg m0 n0 S0 T0 U0 =
    do {
    _ ← RETURN False;
    (brk, _, _, T, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, m0, n0)⇖
      (λ(brk, _). ¬brk)
      (λ(brk, S, S', S'', m,  n).
      do {
        T ← unit_propagation_outer_loop S'';
        (brk, T) ← cdcl_twl_o_prog T;
        (S, S', T, m', n') ← restart_prog_int S S' T m n brk;
        _ ← RETURN_FALSE;
        RETURN (brk ∨ get_conflict T ≠ None, S, S', T, m', n')
      })
      (False, S0, T0, U0, m0, n0);
    RETURN T
    }›
    unfolding cdcl_twl_stgy_restart_prog_int_def RETURN_FALSE_def
    by auto

  have [refine]: ‹RETURN False ≤ ⇓ {(b, b'). (b = b') ∧ ¬b} (RES UNIV)›
     ‹RETURN_FALSE ≤ ⇓ {(b, b'). (b = b') ∧ ¬b} (RES UNIV)›
    by (auto intro!: RETURN_RES_refine simp: RETURN_FALSE_def)
   have [refine]: ‹((False, S0, T0, U0, (m0::nat), (n0 :: nat)), ebrk, False, S0, T0, U0,
      m0, n0) ∈ {(T, (b, S)). S = T ∧ ¬b}›
     if ‹(u, ebrk) ∈ {(b, b'). (b = b') ∧ ¬b}› for ebrk u
     using that
     by auto
   have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'›
     for x x'
     using that by auto

  have ref_early: ‹cdcl_twl_stgy_restart_prog_intg m0 n0 S0 T0 U0 ≤ ⇓{((S), (ebrk, T)). S = T ∧ ¬ebrk}
       (cdcl_twl_stgy_restart_prog_bounded_intg m0 n0 S0 T0 U0)›
    unfolding cdcl_twl_stgy_restart_prog_alt_def cdcl_twl_stgy_restart_prog_bounded_intg_def
    apply refine_rcg
    apply assumption
    subgoal by auto
    subgoal by auto
    apply (rule this_is_the_identity)
    subgoal by auto
    apply (rule this_is_the_identity)
    subgoal by auto
    apply (rule this_is_the_identity)
    subgoal by simp
    subgoal by auto
    subgoal by auto
    done

  show ?thesis
    apply (rule order_trans[OF ref_early])
    apply (rule order_trans[OF ref_two_step'])
    apply (rule cdcl_twl_stgy_prog_bounded_int_spec[OF assms])
    unfolding conc_fun_RES partial_conclusive_TWL_run2_def conclusive_TWL_run2_def by fastforce
qed

end

context twl_restart_ops
begin

definition (in -) restart_prog_pre :: ‹'v twl_st ⇒ nat ⇒ nat ⇒ bool ⇒ bool› where
  ‹restart_prog_pre S last_GC last_Restart  brk ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
    (¬brk ⟶ get_conflict S = None) ∧
    size (get_all_learned_clss S) ≥ last_Restart ∧
    size (get_all_learned_clss S) ≥ last_GC ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›

definition restart_prog
  :: ‹'v twl_st ⇒ nat ⇒ nat ⇒ nat ⇒ bool ⇒ ('v twl_st × nat × nat × nat) nres›
where
  ‹restart_prog S last_GC last_Restart n brk = do {
     ASSERT(restart_prog_pre S last_GC last_Restart brk);
     b ← GC_required S last_GC  n;
     b2 ← restart_required S last_Restart  n;
     if b2 ∧ ¬brk then do {
       T ← SPEC(λT. cdcl_twl_restart_only S T);
       RETURN (T, last_GC, (size (get_all_learned_clss T)), n)
     }
     else
     if b ∧ ¬brk then do {
         b ← inprocessing_required S;
         if ¬b then  do {
           V ← SPEC(λU. cdcl_twl_restart S U);
           RETURN (V, (size (get_all_learned_clss V)), (size (get_all_learned_clss V)), Suc n)
       } else do {
           T ← SPEC(λT. cdcl_twl_inp** S T ∧ count_decided (get_trail T) = 0);
           RETURN (T, (size (get_all_learned_clss T)), (size (get_all_learned_clss T)), Suc n)
        }
     }
     else
       RETURN (S, last_GC, last_Restart, n)
   }›

lemma restart_prog_spec:
  ‹(uncurry4 restart_prog, uncurry5 restart_prog_int) ∈
  {(((((S, last_GC), last_Restart), n), brk),
  (((((last_GC', last_Restart'), S'), m'), n'), brk')).
  S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
  last_Restart = size (get_all_learned_clss last_Restart') ∧
  n = n' ∧ brk = brk'} →f
  ⟨{((S, last_GC, last_Restart, n),
   (last_GC', last_Restart', S', m', n')).
  S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
  last_Restart = size (get_all_learned_clss last_Restart') ∧
  n = n'}⟩nres_rel›
proof -
  have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'› for x x'
    using that by auto
  show ?thesis
    unfolding restart_prog_def restart_prog_int_def uncurry_def
    apply (intro frefI nres_relI)
    apply refine_rcg
    subgoal
      by (auto simp: restart_prog_pre_def restart_prog_pre_int_def)
    apply (rule this_is_the_identity)
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    done
qed

fun cdcl_twl_stgy_restart_prog_inv:: "'v twl_st × nat ⇒ (bool × 'v twl_st × nat × nat ×nat) ⇒ bool" where
 [simp del]: ‹cdcl_twl_stgy_restart_prog_inv (S0, n0)(brk, T, last_GC, last_Restart, n) ⟷
    (∃last_GC' last_Restart' m m0 T0 U0. last_GC = size (get_all_learned_clss last_GC') ∧
      last_Restart = size (get_all_learned_clss last_Restart') ∧
     cdcl_twl_stgy_restart_prog_int_inv (T0, U0, S0, m0, n0) (brk, last_GC', last_Restart', T, m, n))›

lemma cdcl_twl_stgy_restart_prog_inv_def:
  ‹cdcl_twl_stgy_restart_prog_inv= (λ(S0, n0) (brk, T, last_GC, last_Restart, n).
    (∃last_GC' last_Restart' m m0 T0 U0. last_GC = size (get_all_learned_clss last_GC') ∧
      last_Restart = size (get_all_learned_clss last_Restart') ∧
  cdcl_twl_stgy_restart_prog_int_inv (T0, U0, S0, m0, n0) (brk, last_GC', last_Restart', T, m, n)))›
  by (force intro!: ext simp: cdcl_twl_stgy_restart_prog_inv.simps)

definition cdcl_twl_stgy_restart_progg
  :: "nat ⇒ nat ⇒ nat ⇒ 'v twl_st ⇒ 'v twl_st nres"
where
  ‹cdcl_twl_stgy_restart_progg n0 last_GC last_Restart S0 =
  do {
    (brk, T, _, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_inv (S0, n0)⇖
      (λ(brk, _). ¬brk)
      (λ(brk, S'', S, S', n).
      do {
        T ← unit_propagation_outer_loop S'';
        (brk, T) ← cdcl_twl_o_prog T;
        (T, S, S', n') ← restart_prog T S S' n brk;
        RETURN (brk ∨ get_conflict T ≠ None, T, S, S', n')
      })
      (False, S0, last_GC, last_Restart, n0);
    RETURN T
  }›

abbreviation cdcl_twl_stgy_restart_prog where
  ‹cdcl_twl_stgy_restart_prog S ≡
     cdcl_twl_stgy_restart_progg 0 (size (get_all_learned_clss S)) (size (get_all_learned_clss S)) S›

lemmas cdcl_twl_stgy_restart_prog_def = cdcl_twl_stgy_restart_progg_def

lemma (in -) fref_to_Down_curry4_5:
  ‹(uncurry4 f, uncurry5 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c'. P (((((x', y'), z'), a'), b'), c') ⟹
        (((((x, y), z), a), b), (((((x', y'), z'), a'), b'), c')) ∈ A ⟹
         f x y z a b ≤ ⇓ B (g x' y' z' a' b' c'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma cdcl_twl_stgy_restart_progg_cdcl_twl_stgy_restart_prog_intg:
  ‹cdcl_twl_stgy_restart_progg n0 (size (get_all_learned_clss T)) (size (get_all_learned_clss U)) S ≤ ⇓Id (cdcl_twl_stgy_restart_prog_intg m0 n0 T U S)›
proof -
  have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'› for x x'
    using that by auto
  show ?thesis
    unfolding cdcl_twl_stgy_restart_prog_def cdcl_twl_stgy_restart_prog_int_def uncurry_def
    apply (refine_rcg
      WHILEIT_refine[where R = ‹{((brk :: bool,  S :: 'v twl_st, last_GC, last_Restart, n),
     (brk', last_GC', last_Restart', S', m', n')).
    S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
    last_Restart = size (get_all_learned_clss last_Restart') ∧
      n = n' ∧ brk = brk'}›]
      restart_prog_spec[THEN fref_to_Down_curry4_5])
    subgoal
      by auto
    subgoal
      unfolding cdcl_twl_stgy_restart_prog_inv_def by blast
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    done
qed

lemma cdcl_twl_stgy_restart_prog_cdcl_twl_stgy_restart_prog_int:
  ‹(cdcl_twl_stgy_restart_prog, cdcl_twl_stgy_restart_prog_int) ∈ Id →f ⟨Id⟩nres_rel›
proof -
  show ?thesis
    unfolding uncurry_def Down_id_eq
    apply (intro frefI nres_relI)
    apply (rule order_trans[OF cdcl_twl_stgy_restart_progg_cdcl_twl_stgy_restart_prog_intg])
    apply auto
    done
qed


lemma (in twl_restart) cdcl_twl_stgy_restart_prog_specg:
  fixes S0 :: ‹'v twl_st›
  assumes ‹twl_restart_inv (T0, U0, S0, m0, n0, False)› and
    ‹twl_stgy_restart_inv (T0, U0, S0,  m0, n0, False)› and
    ‹clauses_to_update S0 = {#}› and
    ‹get_conflict S0 = None›
  shows
    ‹cdcl_twl_stgy_restart_progg n0 (size (get_all_learned_clss T0)) (size (get_all_learned_clss U0)) S0 ≤ conclusive_TWL_run2 m0 n0 T0 U0 S0›
  apply (rule order_trans)
  apply (rule cdcl_twl_stgy_restart_progg_cdcl_twl_stgy_restart_prog_intg[of _ _ _ _ m0])
  apply simp
  apply (rule cdcl_twl_stgy_restart_prog_int_spec[OF assms])
  done

lemma (in twl_restart) cdcl_twl_stgy_restart_prog_spec:
  fixes S :: ‹'v twl_st›
  assumes
    ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_restart_prog S ≤ conclusive_TWL_run S›
  by (rule order_trans[OF cdcl_twl_stgy_restart_prog_specg[of _ _ _ 0]])
   (use assms in ‹force simp: twl_restart_inv_def pcdcl_stgy_restart_inv_def
      twl_struct_invs_def twl_stgy_restart_inv_def conclusive_TWL_run2_def
      conclusive_TWL_run_def›)+


definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_boundedg
   :: "nat ⇒ nat ⇒ nat ⇒ 'v twl_st ⇒ (bool × 'v twl_st) nres"
where
  ‹cdcl_twl_stgy_restart_prog_boundedg n0 last_GC last_Restart S0=
  do {
    ebrk ← RES UNIV;
    (ebrk, _, T, _, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_inv (S0, n0) o snd⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, S, last_GC, last_Restart, n).
      do {
        T ← unit_propagation_outer_loop S;
        (brk, T) ← cdcl_twl_o_prog T;
        (T, last_GC, last_Restart, n) ← restart_prog T last_GC last_Restart n brk;
	ebrk ← RES UNIV;
        RETURN (ebrk, brk ∨ get_conflict T ≠ None, T, last_GC, last_Restart, n)
      })
      (ebrk, False, S0, last_GC, last_Restart, n0);
    RETURN (ebrk, T)
  }›

abbreviation cdcl_twl_stgy_restart_prog_bounded where
 ‹cdcl_twl_stgy_restart_prog_bounded S ≡ cdcl_twl_stgy_restart_prog_boundedg 0 (size (get_all_learned_clss S))
      (size (get_all_learned_clss S)) S›

lemmas cdcl_twl_stgy_restart_prog_bounded_def =
  cdcl_twl_stgy_restart_prog_boundedg_def

lemma cdcl_twl_stgy_restart_prog_boundedg_cdcl_twl_stgy_restart_prog_bounded_intg:
  ‹cdcl_twl_stgy_restart_prog_boundedg n0 (size (get_all_learned_clss T0))
      (size (get_all_learned_clss U0)) S ≤ ⇓Id (cdcl_twl_stgy_restart_prog_bounded_intg m0 n0 T0 U0 S)›
proof -
  have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'› for x x'
    using that by auto
  show ?thesis
    unfolding cdcl_twl_stgy_restart_prog_bounded_def cdcl_twl_stgy_restart_prog_bounded_intg_def
      uncurry_def
    apply (refine_rcg
      WHILEIT_refine[where R = ‹{((ebrk :: bool, brk :: bool,  S :: 'v twl_st, last_GC, last_Restart, n),
     (ebrk', brk', last_GC', last_Restart', S', m', n')).
    S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
    last_Restart = size (get_all_learned_clss last_Restart') ∧
      n = n' ∧ brk = brk' ∧ ebrk = ebrk'}›]
      restart_prog_spec[THEN fref_to_Down_curry4_5])
    subgoal
      by auto
    subgoal for ebrk ebrka x x'
      unfolding cdcl_twl_stgy_restart_prog_inv_def prod.case case_prod_beta comp_def
      apply (rule exI[of _ ‹fst (snd (snd ((x'))))›])
      apply (rule exI[of _ ‹fst (snd (snd (snd ((x')))))›])
      apply (rule_tac exI[of _ ‹fst (snd (snd (snd (snd (snd (x'))))))›])
      apply (rule_tac exI[of _ m0])
      apply (rule_tac exI[of _ T0])
      apply (rule_tac exI[of _ U0])
      by simp
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    done
qed

lemma cdcl_twl_stgy_restart_prog_bounded_cdcl_twl_stgy_restart_prog_bounded_int:
  ‹(cdcl_twl_stgy_restart_prog_bounded, cdcl_twl_stgy_restart_prog_bounded_int) ∈ Id →f ⟨Id⟩nres_rel›
proof -
  have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'› for x x'
    using that by auto
  show ?thesis
    unfolding uncurry_def
    apply (intro frefI nres_relI)
    apply (rule order_trans[OF cdcl_twl_stgy_restart_prog_boundedg_cdcl_twl_stgy_restart_prog_bounded_intg])
    apply (auto simp add: )
    done
qed
thm twl_restart_inv_def
lemma (in twl_restart) cdcl_twl_stgy_prog_bounded_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_restart_prog_bounded S ≤ partial_conclusive_TWL_run S›
  apply (rule order_trans)
  apply (rule cdcl_twl_stgy_restart_prog_bounded_cdcl_twl_stgy_restart_prog_bounded_int[THEN fref_to_Down, of _ S])
  apply simp
  apply simp
  apply (rule order_trans[OF ref_two_step'])
  apply (rule cdcl_twl_stgy_prog_bounded_int_spec)
  apply ((use assms in ‹auto simp: twl_restart_inv_def pcdcl_stgy_restart_inv_def
    twl_struct_invs_def twl_stgy_restart_inv_def partial_conclusive_TWL_run2_def
    partial_conclusive_TWL_run_def›)+)[4]
  unfolding partial_conclusive_TWL_run2_def partial_conclusive_TWL_run_def
  by fastforce


definition cdcl_twl_stgy_restart_prog_early_intg
  :: "'v twl_st ⇒'v twl_st ⇒'v twl_st ⇒ 'v twl_st nres"
where
  ‹cdcl_twl_stgy_restart_prog_early_intg S0 T0 U0=
  do {
    ebrk ← RES UNIV;
    (ebrk, brk, last_GC, last_Restart, T,m, n) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, 0, 0) o snd⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, last_GC, last_Restart, S, m, n).
      do {
        T ← unit_propagation_outer_loop S;
        (brk, T) ← cdcl_twl_o_prog T;
        (last_GC, last_Restart, T, m, n) ← restart_prog_int last_GC last_Restart T m n brk;
	ebrk ← RES UNIV;
        RETURN (ebrk, brk ∨ get_conflict T ≠ None, last_GC, last_Restart, T, m, n)
      })
      (ebrk, False, S0, T0, U0, 0, 0);
    if ¬brk then do {
      (brk, last_GC, last_Restart, T, _, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (last_GC, last_Restart, T, m, n)⇖
	(λ(brk, _). ¬brk)
	(λ(brk, last_GC, last_Restart, S, m, n).
	do {
	  T ← unit_propagation_outer_loop S;
	  (brk, T) ← cdcl_twl_o_prog T;
	  (last_GC, last_Restart, T, m, n) ← restart_prog_int last_GC last_Restart T m n brk;
	  RETURN (brk ∨ get_conflict T ≠ None, last_GC, last_Restart, T, m, n)
	})
	(False, last_GC, last_Restart, T, m, n);
      RETURN T
    }
    else RETURN T
  }›

lemmas cdcl_twl_stgy_restart_prog_early_int_def =
  cdcl_twl_stgy_restart_prog_early_intg_def

lemma cdcl_twl_stgy_restart_prog_early_intg_alt_def:
  ‹cdcl_twl_stgy_restart_prog_early_intg S0  T0 U0 =
  do {
    ebrk ← RES UNIV;
    (ebrk, brk, last_GC, last_Restart, T,m, n) ← WHILET⇗cdcl_twl_stgy_restart_prog_int_inv (S0, T0, U0, 0, 0) o snd⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, last_GC, last_Restart, S, m, n).
      do {
        T ← unit_propagation_outer_loop S;
        (brk, T) ← cdcl_twl_o_prog T;
        (last_GC, last_Restart, T, m, n) ← restart_prog_int last_GC last_Restart T m n brk;
	ebrk ← RES UNIV;
        RETURN (ebrk, brk ∨ get_conflict T ≠ None, last_GC, last_Restart, T, m, n)
      })
      (ebrk, False, S0, T0, U0, 0, 0);
    if ¬brk then do {
        cdcl_twl_stgy_restart_prog_intg m n last_GC last_Restart T
      } else RETURN T
  }›
   unfolding cdcl_twl_stgy_restart_prog_intg_def cdcl_twl_stgy_restart_prog_early_intg_def
   by (auto intro!: bind_cong[OF refl])

definition cdcl_twl_stgy_restart_prog_early :: "'v twl_st ⇒ 'v twl_st nres" where
  ‹cdcl_twl_stgy_restart_prog_early S0 =
  do {
    ebrk ← RES UNIV;
    (ebrk, brk, T, last_GC, last_Restart, n) ← WHILET⇗cdcl_twl_stgy_restart_prog_inv (S0, 0) o snd⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, S, last_GC, last_Restart, n).
      do {
        T ← unit_propagation_outer_loop S;
        (brk, T) ← cdcl_twl_o_prog T;
        (T, last_GC, last_Restart, n) ← restart_prog T last_GC last_Restart n brk;
	ebrk ← RES UNIV;
        RETURN (ebrk, brk ∨ get_conflict T ≠ None, T, last_GC, last_Restart, n)
      })
      (ebrk, False, S0, size (get_all_learned_clss S0), size (get_all_learned_clss S0), 0);
    if ¬brk then do {
      (brk, T, last_GC, last_Restart, _) ← WHILET⇗cdcl_twl_stgy_restart_prog_inv (T, n)⇖
	(λ(brk, _). ¬brk)
	(λ(brk, S, last_GC, last_Restart, n).
	do {
	  T ← unit_propagation_outer_loop S;
	  (brk, T) ← cdcl_twl_o_prog T;
	  (T, last_GC, last_Restart, n) ← restart_prog T last_GC last_Restart n brk;
	  RETURN (brk ∨ get_conflict T ≠ None, T, last_GC, last_Restart, n)
	})
	(False, T, last_GC, last_Restart, n);
      RETURN T
    }
    else RETURN T
  }›

abbreviation cdcl_twl_stgy_restart_prog_early_int where
  ‹cdcl_twl_stgy_restart_prog_early_int S ≡ cdcl_twl_stgy_restart_prog_early_intg S S S›


lemma (in twl_restart) cdcl_twl_stgy_prog_early_int_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_restart_prog_early_int S ≤ conclusive_TWL_run S›
proof -
  show ?thesis
    unfolding cdcl_twl_stgy_restart_prog_early_intg_alt_def conclusive_TWL_run_def
    apply (refine_vcg
      cdcl_twl_stgy_restart_prog_int_spec[THEN order_trans]
      WHILEIT_rule[where
      R = ‹cdcl_algo_termination_early_rel›];
      remove_dummy_vars)
    subgoal
      by (rule wf_cdcl_algo_termination_early_rel)
    subgoal
      using assms by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_restart_inv_def
        twl_struct_invs_def pcdcl_stgy_restart_inv_def twl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
        twl_restart_inv_def
        dest!: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
        twl_restart_inv_def
        dest: rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def twl_stgy_restart_inv_def
        twl_restart_inv_def no_step_cdcl_twl_cp_no_step_cdclW_cp
        dest: rtranclp_cdcl_twl_stgy_restart_twl_restart_inv)
    subgoal by fast
    subgoal for x a aa ab ac ad ae be xa
      using assms
      using
        rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of ‹(S, S, S, 0, 0, True)›
        ‹(ab, ac, ad, ae, be, True)›]
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_def
         twl_restart_inv_def
        intro: rtranclp_cdcl_twl_stgy_entailed_by_init
        dest!: rtranclp_cdcl_twl_cp_stgyD
        simp flip:  stateW_of_def)
    subgoal
      by (rule restart_prog_bounded_spec)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_alt_def twl_restart_inv_def
        twl_stgy_restart_inv_def pcdcl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_alt_def twl_restart_inv_def
        twl_stgy_restart_inv_def pcdcl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_alt_def twl_restart_inv_def
        twl_stgy_restart_inv_def pcdcl_stgy_restart_inv_def)
    subgoal
      by (auto simp: cdcl_twl_stgy_restart_prog_int_inv_alt_def twl_restart_inv_def
        twl_stgy_restart_inv_def pcdcl_stgy_restart_inv_def)
    subgoal for x a aa ab ac ad ae be
      unfolding conclusive_TWL_run2_def cdcl_twl_stgy_restart_prog_int_inv_def
        cdcl_twl_stgy_restart_prog_int_inv_alt_def comp_def snd_conv
      apply (rule SPEC_rule)
      apply normalize_goal+
      apply (rule_tac x=xb in exI)
      apply (rule_tac x=xc in exI)
      apply (rule_tac x=xd in exI)
      apply (rule_tac x=0 in exI)
      apply (rule_tac x=0 in exI)
      apply auto
      done
    subgoal for x a aa ab ac ad ae be
      unfolding conclusive_TWL_run2_def cdcl_twl_stgy_restart_prog_int_inv_def
        cdcl_twl_stgy_restart_prog_int_inv_alt_def comp_def snd_conv
      apply normalize_goal+
      apply (rule_tac x=ab in exI)
      apply (rule_tac x=ac in exI)
      apply (rule_tac x= ‹(ae, be, ¬aa)› in exI)
      apply (rule_tac x=0 in exI)
      apply (rule_tac x=0 in exI)
      apply auto
      done
    done
qed

lemma cdcl_twl_stgy_restart_prog_early_cdcl_twl_stgy_restart_prog_early:
  ‹cdcl_twl_stgy_restart_prog_early S ≤ ⇓Id (cdcl_twl_stgy_restart_prog_early_int S)›
proof -
  have this_is_the_identity: ‹x ≤ ⇓Id (x')› if ‹x = x'› for x x'
    using that by auto
  show ?thesis
    unfolding cdcl_twl_stgy_restart_prog_early_def cdcl_twl_stgy_restart_prog_early_int_def
      uncurry_def
    apply (refine_rcg
      WHILEIT_refine[where R = ‹{((ebrk :: bool, brk :: bool,  S :: 'v twl_st, last_GC, last_Restart, n),
     (ebrk', brk', last_GC', last_Restart', S', m', n')).
    S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
    last_Restart = size (get_all_learned_clss last_Restart') ∧
      n = n' ∧ brk = brk' ∧ ebrk = ebrk'}›]
      WHILEIT_refine[where R = ‹{((brk :: bool,  S :: 'v twl_st, last_GC, last_Restart, n),
     (brk', last_GC', last_Restart', S', m', n')).
    S = S' ∧ last_GC = size (get_all_learned_clss last_GC') ∧
    last_Restart = size (get_all_learned_clss last_Restart') ∧
      n = n' ∧ brk = brk'}›]
      restart_prog_spec[THEN fref_to_Down_curry4_5])
    subgoal
      by auto
    subgoal for ebrk ebrka x x'
      unfolding cdcl_twl_stgy_restart_prog_inv_def prod.case case_prod_beta comp_def
      apply (rule exI[of _ ‹fst (snd (snd ((x'))))›])
      apply (rule exI[of _ ‹fst (snd (snd (snd ((x')))))›])
      apply (rule_tac exI[of _ ‹fst (snd (snd (snd (snd (snd (x'))))))›])
      apply (rule_tac exI[of _ 0])
      apply (rule_tac exI[of _ S])
      apply (rule_tac exI[of _ S])
      by simp
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by auto
    subgoal for ebrk ebrka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h
      x2h x1i x2i x1j x2j xa x'a
      unfolding cdcl_twl_stgy_restart_prog_inv_def prod.case case_prod_beta comp_def
      apply (rule exI[of _ ‹fst (snd (((x'a))))›])
      apply (rule exI[of _ ‹fst (snd (snd (((x'a)))))›])
      apply (rule_tac exI[of _ ‹fst ((snd (snd (snd (snd (x'a))))))›])
      apply (rule_tac exI[of _ x1e])
      apply (rule_tac exI[of _ x1b])
      apply (rule_tac exI[of _ x1c])
      apply (cases x'a)
      by simp
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    apply (rule this_is_the_identity)
    subgoal
      by auto
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    subgoal
      by simp
    done
qed

lemma (in twl_restart) cdcl_twl_stgy_restart_prog_early_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_restart_prog_early S ≤ conclusive_TWL_run S›
  apply (rule order_trans[OF cdcl_twl_stgy_restart_prog_early_cdcl_twl_stgy_restart_prog_early])
  apply (subst Down_id_eq)
  apply (rule cdcl_twl_stgy_prog_early_int_spec[OF assms])
  done

end

end