Theory Watched_Literals_Algorithm

theory Watched_Literals_Algorithm
  imports
    More_Sepref.WB_More_Refinement
    Watched_Literals_Transition_System
    Watched_Literals_All_Literals
begin

chapter ‹First Refinement: Deterministic Rule Application›

section ‹Unit Propagation Loops›

definition set_conflict_pre :: ‹'v twl_cls ⇒ 'v twl_st ⇒ bool› where
  ‹set_conflict_pre C S ⟷
    (∃L C'. let S' = (set_clauses_to_update (add_mset (L, C') (clauses_to_update S)) S) in
    twl_struct_invs S' ∧ twl_stgy_invs S' ∧ get_trail S' ⊨as CNot (clause C))›

definition set_conflicting :: ‹'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st› where
  ‹set_conflicting = (λC (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q).
    (M, N, U, Some (clause C), NE, UE, NS, US, N0, U0, {#}, {#}))›

definition mop_set_conflicting :: ‹'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹mop_set_conflicting = (λC S. do {
     ASSERT (set_conflict_pre C S);
     RETURN (set_conflicting C S)})›

definition propagate_lit_pre :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ bool› where
‹propagate_lit_pre L' C S ⟷
  (∃L C'. let S' = (set_clauses_to_update (add_mset (L, C') (clauses_to_update S)) S) in
   twl_struct_invs S' ∧ twl_stgy_invs S' ∧ undefined_lit (get_trail S) L' ∧
   L' ∈# all_lits_of_mm (clauses (get_clauses S) + unit_clss S))›

definition propagate_lit :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st› where
  ‹propagate_lit = (λL' C (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q). do {
      (Propagated L' (clause C) # M, N, U, D, NE, UE, NS, US, N0, U0, WS, add_mset (-L') Q)})›

definition mop_propagate_lit :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹mop_propagate_lit = (λL' C S. do {
      ASSERT(propagate_lit_pre L' C S);
      RETURN (propagate_lit L' C S)})›

definition update_clauseS_pre  :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ bool› where
  ‹update_clauseS_pre L C S ⟷
   (let S = (set_clauses_to_update (add_mset (L, C) (clauses_to_update S)) S) in
     L ∈# watched C ∧ C ∈# get_clauses S ∧ twl_struct_invs S ∧ twl_stgy_invs S)›

definition update_clauseS :: ‹'v literal ⇒ 'v twl_cls ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹update_clauseS = (λL C (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q). do {
        ASSERT(update_clauseS_pre L C (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q));
        K ← SPEC (λL. L ∈# unwatched C ∧ -L ∉ lits_of_l M);
        if K ∈ lits_of_l M
        then RETURN (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)
        else do {
          (N', U') ← SPEC (λ(N', U'). update_clauses (N, U) C L K (N', U'));
          RETURN (M, N', U', D, NE, UE, NS, US, N0, U0, WS, Q)
        }
  })›

definition all_lits_of_st :: ‹'v twl_st ⇒ 'v literal multiset› where
‹all_lits_of_st S ≡ all_lits_of_mm (clauses (get_clauses S) + unit_clss S + subsumed_clauses S +
    get_all_clauses0 S)›

definition mop_lit_is_pos where
  ‹mop_lit_is_pos L S = do {
     ASSERT(L ∈# all_lits_of_st S ∧
        no_dup (get_trail S));
     RETURN (L ∈ lits_of_l (get_trail S))
  }›

definition unit_propagation_inner_loop_body :: ‹'v literal ⇒ 'v twl_cls ⇒
  'v twl_st ⇒ 'v twl_st nres› where
  ‹unit_propagation_inner_loop_body = (λL C S. do {
    do {
      bL' ← SPEC (λK. K ∈# clause C);
      val_bL' ← mop_lit_is_pos bL' S;
      if val_bL'
      then RETURN S
      else do {
        L' ← SPEC (λK. K ∈# watched C - {#L#});
        ASSERT (watched C = {#L, L'#});
        val_L' ← mop_lit_is_pos L' S;
        if val_L'
        then RETURN S
        else
          if ∀L ∈# unwatched C. -L ∈ lits_of_l (get_trail S)
          then
            if -L' ∈ lits_of_l (get_trail S)
            then do {mop_set_conflicting C S}
            else do {mop_propagate_lit L' C S}
          else do {
            update_clauseS L C S
          }
      }
    }
  })
›

definition unit_propagation_inner_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹unit_propagation_inner_loop S0 = do {
    n ← SPEC(λ_::nat. True);
    (S, _) ← WHILET⇗λ(S, n). twl_struct_invs S ∧ twl_stgy_invs S ∧ cdcl_twl_cp** S0 S ∧
          (clauses_to_update S ≠ {#} ∨ n > 0 ⟶ get_conflict S = None)⇖
      (λ(S, n). clauses_to_update S ≠ {#} ∨ n > 0)
      (λ(S, n). do {
        b ← SPEC(λb. (b ⟶ n > 0) ∧ (¬b ⟶ clauses_to_update S ≠ {#}));
        if ¬b then do {
          ASSERT(clauses_to_update S ≠ {#});
          (L, C) ← SPEC (λC. C ∈# clauses_to_update S);
          let S' = set_clauses_to_update (clauses_to_update S - {#(L, C)#}) S;
          T ← unit_propagation_inner_loop_body L C S';
          RETURN (T, if get_conflict T = None then n else 0)
        } else do { ⌦‹This branch allows us to do skip some clauses.›
          RETURN (S, n - 1)
        }
      })
      (S0, n);
    RETURN S
  }
›

lemma unit_propagation_inner_loop_body: (* \htmllink{unit_propagation_inner_loop_body} *)
  fixes S :: ‹'v twl_st›
  assumes
    ‹clauses_to_update S ≠ {#}› and
    x_WS: ‹(L, C) ∈# clauses_to_update S› and
    inv: ‹twl_struct_invs S› and
    inv_s: ‹twl_stgy_invs S› and
    confl: ‹get_conflict S = None›
  shows
     ‹unit_propagation_inner_loop_body L C
          (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
        ≤ (SPEC (λT'.  twl_struct_invs T' ∧ twl_stgy_invs T' ∧ cdcl_twl_cp** S T' ∧
           (T', S) ∈ measure (size ∘ clauses_to_update)))› (is ?spec is ‹_ ≤ ?R›) and
    ‹nofail (unit_propagation_inner_loop_body L C
       (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S))› (is ?fail)
proof -
  obtain M N U D NE UE NS US N0 U0 WS Q where
    S: ‹S = (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    by (cases S) auto

  have ‹C ∈# N + U› and struct: ‹struct_wf_twl_cls C› and L_C: ‹L ∈# watched C› and
    uL_M: ‹-L ∈ lits_of_l M›
    using inv multi_member_split[OF x_WS]
    unfolding twl_struct_invs_def twl_st_inv.simps S
    by force+

  have uL: ‹- L ∈ lits_of_l M› and
    all_struct: ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of S)›
    using inv x_WS unfolding twl_struct_invs_def S pcdcl_all_struct_invs_def by auto

  have ‹cdclW_restart_mset.no_strange_atm (stateW_of S)› and
    ‹cdclW_restart_mset.cdclW_M_level_inv (stateW_of S)›
    using all_struct unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+
  then have alien_L: ‹L ∈# all_lits_of_mm (clauses N + clauses U + (NE + NS + UE + US + N0 + U0))› and
    n_d: ‹no_dup M›
    using uL unfolding cdclW_restart_mset.no_strange_atm_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by (auto simp: S cdclW_restart_mset_state in_all_lits_of_mm_ain_atms_of_iff)
  have ‹C ∈# N + U ⟹ b ∈# clause C ⟹
    b ∈# all_lits_of_mm (clauses N + clauses U + (NE + NS + UE + US + N0 + U0))› for b C
    by (auto dest!: multi_member_split simp: all_lits_of_mm_add_mset all_lits_of_m_add_mset)

  note [[goals_limit=15]]
  show ?spec
    using assms unfolding unit_propagation_inner_loop_body_def update_clause.simps
      mop_lit_is_pos_def nres_monad3
  proof (refine_vcg; (unfold prod.inject clauses_to_update.simps set_clauses_to_update.simps
        ball_simps)?;  clarify?; (unfold triv_forall_equality)?)
    fix L' :: ‹'v literal›
    assume
      ‹clauses_to_update S ≠ {#}› and
      twl_inv: ‹twl_struct_invs S›
    have ‹C ∈# N + U› and struct: ‹struct_wf_twl_cls C› and L_C: ‹L ∈# watched C›
      using twl_inv x_WS unfolding twl_struct_invs_def twl_st_inv.simps S by (auto; fail)+

    define WS' where ‹WS' = WS - {#(L, C)#}›
    have WS_WS': ‹WS = add_mset (L, C) WS'›
      using x_WS unfolding WS'_def S by auto

    have D: ‹D = None›
      using confl S by auto

    let ?S' = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, add_mset (L, C) WS', Q)›
    let ?T = ‹(set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
    let ?T' = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, WS', Q)›

    { ― ‹blocking literal›
      fix K'
      assume
          K': ‹K' ∈# clause C›
      show ‹K' ∈# all_lits_of_st (set_clauses_to_update
                      (remove1_mset (L, C) (clauses_to_update S)) S)›
        using K' ‹C ∈# N + U› by (auto dest!: multi_member_split
            simp: all_lits_of_mm_add_mset all_lits_of_m_add_mset clauses_def S all_lits_of_st_def)

      show ‹no_dup (get_trail
                    (set_clauses_to_update
                      (remove1_mset (L, C)
                        (clauses_to_update S))
                      S))›
        using n_d by (auto simp: S)
      assume
          L': ‹K' ∈ lits_of_l (get_trail ?T)›

      have ‹cdcl_twl_cp ?S' ?T'›
        by (rule cdcl_twl_cp.delete_from_working) (use L' K' S in simp_all)

      then have cdcl: ‹cdcl_twl_cp S ?T›
        using L' D by (simp add: S WS_WS')
      show ‹twl_struct_invs ?T›
        using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)

      show ‹twl_stgy_invs ?T›
        using cdcl inv_s inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)

      show ‹cdcl_twl_cp** S ?T›
        using D WS_WS' cdcl by auto

      show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
        by (simp add: WS'_def[symmetric] WS_WS' S)

    }

    assume L': ‹L' ∈# remove1_mset L (watched C)›
    show watched: ‹watched C = {#L, L'#}›
      by (cases C) (use struct L_C L' in ‹auto simp: size_2_iff›)
    then have L_C': ‹L ∈# clause C› and L'_C': ‹L' ∈# clause C›
      by (cases C; auto; fail)+

      show ‹L' ∈# all_lits_of_st (set_clauses_to_update
                      (remove1_mset (L, C) (clauses_to_update S)) S)›
        using L'_C' ‹C ∈# N + U› by (auto dest!: multi_member_split
            simp: all_lits_of_mm_add_mset all_lits_of_m_add_mset clauses_def S all_lits_of_st_def)


    { ― ‹if term‹L' ∈ lits_of_l M›, then:›
      assume L': ‹L' ∈ lits_of_l (get_trail ?T)›

      have ‹cdcl_twl_cp ?S' ?T'›
        by (rule cdcl_twl_cp.delete_from_working) (use L' L'_C' watched S in simp_all)

      then have cdcl: ‹cdcl_twl_cp S ?T›
        using L' watched D by (simp add: S WS_WS')
      show ‹twl_struct_invs ?T›
        using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)

      show ‹twl_stgy_invs ?T›
        using cdcl inv_s inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)

      show ‹cdcl_twl_cp** S ?T›
        using D WS_WS' cdcl by auto

      show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
        by (simp add: WS'_def[symmetric] WS_WS' S)

    }
      ― ‹if term‹L' ∈ lits_of_l M›, else:›
    let ?M = ‹get_trail ?T›
    assume L': ‹L' ∉ lits_of_l ?M›
    {
      { ― ‹if term‹∀L ∈# unwatched C. -L ∈ lits_of_l ?M›, then›
        assume unwatched: ‹∀L∈#unwatched C. - L ∈ lits_of_l ?M›

        { ― ‹if term‹-L' ∈ lits_of_l ?M› then›
          let ?T' = ‹(M, N, U, Some (clause C), NE, UE, NS, US, N0, U0, {#}, {#})›
          let ?T = ‹set_conflicting C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
          assume uL': ‹-L' ∈ lits_of_l ?M›
          have cdcl: ‹cdcl_twl_cp ?S' ?T'›
            by (rule cdcl_twl_cp.conflict) (use uL' L' watched unwatched S in simp_all)
          then have cdcl: ‹cdcl_twl_cp S ?T›
            using uL' L' watched unwatched by (simp add: set_conflicting_def WS_WS' S D)

          have ‹twl_struct_invs ?T›
            using cdcl inv D unfolding WS_WS'
            by (force intro: cdcl_twl_cp_twl_struct_invs)
          moreover have ‹twl_stgy_invs ?T›
            using cdcl inv inv_s D unfolding WS_WS'
            by (force intro: cdcl_twl_cp_twl_stgy_invs)
          moreover have ‹cdcl_twl_cp** S ?T›
            using D WS_WS' cdcl S by auto
          moreover have ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
            by (simp add: S WS'_def[symmetric] WS_WS' set_conflicting_def)

          moreover have ‹get_trail (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S))
             S) ⊨as CNot (clause C)›
             using unwatched uL' watched L' uL_M by (cases C; auto simp: true_annots_true_cls_def_iff_negation_in_model S)
         ultimately show ‹mop_set_conflicting C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
           ≤ ?R›
           using assms
           by (auto simp: mop_set_conflicting_def set_conflict_pre_def Let_def S
              intro!: ASSERT_leI exI[of _ L] exI[of _ C])

        }


        { ― ‹if term‹-L' ∈ lits_of_l M › else›
           let ?S = ‹(M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
          let ?T' = ‹(Propagated L' (clause C) # M, N, U, None, NE, UE, NS, US, N0, U0, WS', add_mset (- L') Q)›
          let ?S' = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, add_mset (L, C) WS', Q)›
          let ?T = ‹propagate_lit L' C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)›
          assume uL': ‹- L' ∉ lits_of_l ?M›

          have undef: ‹undefined_lit M L'›
            using uL' L' by (auto simp: S defined_lit_map lits_of_def atm_of_eq_atm_of)

          have cdcl: ‹cdcl_twl_cp ?S' ?T'›
            by (rule cdcl_twl_cp.propagate) (use uL' L' undef watched unwatched D S in simp_all)
          then have cdcl: ‹cdcl_twl_cp S ?T›
            using uL' L' undef watched unwatched D S WS_WS' by (simp add: propagate_lit_def)

          moreover have  ‹twl_struct_invs ?T›
            using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)

          moreover have  ‹cdcl_twl_cp** S ?T›
            using cdcl D WS_WS' by force
          moreover have  ‹twl_stgy_invs ?T›
            using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
          moreover have ‹L' ∈# all_lits_of_mm (clauses N + clauses U + (NE + UE))›
            using L'_C' ‹C ∈# N + U› by (auto simp: all_lits_of_mm_add_mset all_lits_of_m_add_mset
               dest!: multi_member_split)
          ultimately show ‹mop_propagate_lit L' C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
           ≤ ?R›
           using x_WS inv inv_s undef
           by (auto simp: mop_propagate_lit_def propagate_lit_pre_def propagate_lit_def Let_def S
              intro!: ASSERT_leI exI[of _ L] exI[of _ C] dest: multi_member_split)
        }
      }

      fix La
― ‹if term‹∀L ∈# unwatched C. -L ∈ lits_of_l M›, else›
      {
        let ?S = ‹(M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
        let ?S' = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, add_mset (L, C) WS', Q)›
        let ?T = ‹set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S›
        fix K M' N' U' D' WS'' NE' UE' Q' N'' U''
        have ‹update_clauseS L C (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S)
              ≤ SPEC (λS'. twl_struct_invs S' ∧ twl_stgy_invs S' ∧ cdcl_twl_cp** S S' ∧
              (S', S) ∈ measure (size ∘ clauses_to_update))› (is ?upd)
          apply (rewrite at ‹set_clauses_to_update _ ⌑› S)
          apply (rewrite at ‹clauses_to_update ⌑› S)
          unfolding update_clauseS_def clauses_to_update.simps set_clauses_to_update.simps
          apply clarify
        proof refine_vcg
          fix x xa a b
          show ‹update_clauseS_pre L C (M, N, U, D, NE, UE, NS, US, N0, U0, remove1_mset (L, C) WS, Q)›
            using assms L_C ‹C ∈# N + U› unfolding update_clauseS_pre_def S Let_def
            by auto
          assume K: ‹x ∈# unwatched C ∧ - x ∉ lits_of_l M›
          have uL: ‹- L ∈ lits_of_l M›
            using inv unfolding twl_struct_invs_def S WS_WS' by auto
          { ― ‹BLIT›
            let ?T = ‹(M, N, U, D, NE, UE, NS, US, N0, U0, remove1_mset (L, C) WS, Q)›
            let ?T' = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, WS', Q)›

            assume ‹x ∈ lits_of_l M›
            have uL: ‹- L ∈ lits_of_l M›
              using inv unfolding twl_struct_invs_def S WS_WS' by auto
            have ‹L ∈# clause C› ‹x ∈# clause C›
              using watched K by (cases C; simp; fail)+
            have ‹cdcl_twl_cp ?S' ?T'›
              by (rule cdcl_twl_cp.delete_from_working[OF ‹x ∈# clause C› ‹x ∈ lits_of_l M›])
            then have cdcl: ‹cdcl_twl_cp S ?T›
              by (auto simp: S D WS_WS')

            show ‹twl_struct_invs ?T›
              using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)


            show ‹twl_stgy_invs ?T›
              using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
            show ‹cdcl_twl_cp** S ?T›
              using D WS_WS' cdcl by auto
            show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
              by (simp add: WS'_def[symmetric] WS_WS' S)
          }
          assume
            update: ‹case xa of (N', U') ⇒ update_clauses (N, U) C L x (N', U')› and
            [simp]: ‹xa = (a, b)›
          let ?T' = ‹(M, a, b, None, NE, UE, NS, US, N0, U0, WS', Q)›
          let ?T = ‹(M, a, b, D, NE, UE, NS, US, N0, U0, remove1_mset (L, C) WS, Q)›
          have ‹cdcl_twl_cp ?S' ?T'›
            by (rule cdcl_twl_cp.update_clause)
              (use uL L' K update watched S in ‹simp_all add: true_annot_iff_decided_or_true_lit›)
          then have cdcl: ‹cdcl_twl_cp S ?T›
            by (auto simp: S D WS_WS')

          show ‹twl_struct_invs ?T›
            using cdcl inv D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_struct_invs)

          have uL: ‹- L ∈ lits_of_l M›
            using inv unfolding twl_struct_invs_def S WS_WS' by auto

          show ‹twl_stgy_invs ?T›
            using cdcl inv inv_s D unfolding S WS_WS' by (force intro: cdcl_twl_cp_twl_stgy_invs)
          show ‹cdcl_twl_cp** S ?T›
            using D WS_WS' cdcl by auto
          show ‹(?T, S) ∈ measure (size ∘ clauses_to_update)›
            by (simp add: WS'_def[symmetric] WS_WS' S)
        qed
        moreover assume ‹¬?upd›
        ultimately show ‹- La ∈
          lits_of_l (get_trail (set_clauses_to_update (remove1_mset (L, C) (clauses_to_update S)) S))›
          by fast
      }
    }
  qed
  from SPEC_nofail[OF this] show ?fail .
qed

declare unit_propagation_inner_loop_body(1)[THEN order_trans, refine_vcg]

lemma unit_propagation_inner_loop:
  assumes ‹twl_struct_invs S› and inv: ‹twl_stgy_invs S› and ‹get_conflict S = None›
  shows ‹unit_propagation_inner_loop S ≤ SPEC (λS'. twl_struct_invs S' ∧ twl_stgy_invs S' ∧
    cdcl_twl_cp** S S' ∧ clauses_to_update S' = {#})›
  unfolding unit_propagation_inner_loop_def
  apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(S, n). (size o clauses_to_update) S + n)›])
  subgoal by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by (auto simp add: twl_struct_invs_def)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  done

declare unit_propagation_inner_loop[THEN order_trans, refine_vcg]

definition pop_literal_to_update_pre where
  ‹pop_literal_to_update_pre S ⟷
     twl_struct_invs S ∧ twl_stgy_invs S ∧ clauses_to_update S = {#} ∧
     literals_to_update S ≠ {#}›

definition mop_pop_literal_to_update :: ‹'v twl_st ⇒ ('v literal × 'v twl_st) nres› where
  ‹mop_pop_literal_to_update S = do {
      ASSERT(pop_literal_to_update_pre S);
      L ← SPEC (λL. L ∈# literals_to_update S);
      let S' = set_clauses_to_update {#(L, C)|C ∈# get_clauses S. L ∈# watched C#}
           (set_literals_to_update (literals_to_update S - {#L#}) S);
      RETURN (L, S')
   }›

definition unit_propagation_outer_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹unit_propagation_outer_loop S0 =
    WHILET⇗λS. twl_struct_invs S ∧ twl_stgy_invs S ∧ cdcl_twl_cp** S0 S ∧ clauses_to_update S = {#}⇖
      (λS. literals_to_update S ≠ {#})
      (λS. do {
        (L, S') ← mop_pop_literal_to_update S;
        ASSERT(cdcl_twl_cp S S');
        unit_propagation_inner_loop S'
      })
      S0
›

(* don't use no_step here to allow the abbreviation to fold by default *)
abbreviation unit_propagation_outer_loop_spec where
  ‹unit_propagation_outer_loop_spec S S' ≡ twl_struct_invs S' ∧ cdcl_twl_cp** S S' ∧
    literals_to_update S' = {#} ∧  (∀S'a. ¬ cdcl_twl_cp S' S'a) ∧ twl_stgy_invs S'›

lemma unit_propagation_outer_loop:
  assumes ‹twl_struct_invs S› and ‹clauses_to_update S = {#}› and confl: ‹get_conflict S = None› and
    ‹twl_stgy_invs S›
  shows ‹unit_propagation_outer_loop S ≤ SPEC (λS'. twl_struct_invs S' ∧ cdcl_twl_cp** S S' ∧
    literals_to_update S' = {#} ∧ no_step cdcl_twl_cp S' ∧ twl_stgy_invs S')›
proof -
  have assert_twl_cp: ‹cdcl_twl_cp T T'› (is ?twl) and
    assert_twl_struct_invs:
      ‹twl_struct_invs T'›
           (is ‹twl_struct_invs ?T'›) and
    assert_stgy_invs:
      ‹twl_stgy_invs T'› (is ?stgy)
     if
      p: ‹literals_to_update T ≠ {#}› and
      L_T: ‹L ∈# literals_to_update T› and
      invs: ‹twl_struct_invs T ∧ twl_stgy_invs T ∧cdcl_twl_cp** S T ∧ clauses_to_update T = {#}› and
      eq: ‹(L, set_clauses_to_update (Pair L `# {#C ∈# get_clauses T. L ∈# watched C#})
            (set_literals_to_update (remove1_mset L (literals_to_update T)) T)) =
       (L', T')›
      for L T L' T'
  proof -
    from that have
      p: ‹literals_to_update T ≠ {#}› and
      L_T: ‹L ∈# literals_to_update T› and
      struct_invs: ‹twl_struct_invs T› and
      ‹cdcl_twl_cp** S T› and
      w_q: ‹clauses_to_update T = {#}› and
      eq[simp]: ‹L' = L› ‹T' = (set_clauses_to_update (Pair L `# {#Ca ∈# get_clauses T. L ∈# watched Ca#})
        (set_literals_to_update (remove1_mset L (literals_to_update T)) T))›
      by fast+
    have ‹get_conflict T = None›
      using w_q p invs unfolding twl_struct_invs_def by auto
    then obtain M N U NE UE NS US N0 U0 Q where
      T: ‹T = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
      using w_q p by (cases T) auto
    define Q' where ‹Q' = remove1_mset L Q›
    have Q: ‹Q = add_mset L Q'›
      using L_T unfolding Q'_def T by auto

      ― ‹Show assertion that one step has been done›
    show twl: ?twl
      unfolding eq T set_clauses_to_update.simps set_literals_to_update.simps literals_to_update.simps Q'_def[symmetric]
      unfolding Q get_clauses.simps
      by (rule cdcl_twl_cp.pop)
    then show ‹twl_struct_invs ?T'›
      using cdcl_twl_cp_twl_struct_invs struct_invs by blast


    then show ?stgy
      using twl cdcl_twl_cp_twl_stgy_invs[OF twl] invs by blast
  qed

  show ?thesis
    unfolding unit_propagation_outer_loop_def mop_pop_literal_to_update_def nres_monad3
    apply (refine_vcg WHILEIT_rule[where R = ‹{(T, S). twl_struct_invs S ∧ cdcl_twl_cp++ S T}›])
                apply ((simp_all add: assms tranclp_wf_cdcl_twl_cp; fail)+)[6]
    subgoal unfolding pop_literal_to_update_pre_def by blast
    subgoal by (rule assert_twl_cp) ― ‹Assertion›
    subgoal by (rule assert_twl_struct_invs) ― ‹WHILE-loop invariants›
    subgoal by (rule assert_stgy_invs)
    subgoal for S L
      by (cases S)
       (auto simp: twl_st twl_struct_invs_def)
    subgoal by (simp; fail)
    subgoal by auto
    subgoal by auto
    subgoal by simp
    subgoal by auto ― ‹Termination›
    subgoal ― ‹Final invariants›
      by simp
    subgoal by simp
    subgoal by auto
    subgoal by (auto simp: cdcl_twl_cp.simps)
    subgoal by simp
    done
qed

declare unit_propagation_outer_loop[THEN order_trans, refine_vcg]


section ‹Other Rules›

subsection ‹Decide›

definition find_unassigned_lit :: ‹'v twl_st ⇒ 'v literal option nres› where
  ‹find_unassigned_lit = (λS.
      SPEC (λL.
        (L ≠ None ⟶ undefined_lit (get_trail S) (the L) ∧
           (the L) ∈# all_lits_of_st S) ∧
        (L = None ⟶ (∄L. undefined_lit (get_trail S) L ∧
         L ∈# all_lits_of_st S))))›

definition propagate_dec where
  ‹propagate_dec = (λL (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q).
     (Decided L # M, N, U, D, NE, UE, NS, US, N0, U0, WS, {#-L#}))›

definition decide_or_skip_pre :: ‹'v twl_st ⇒ bool› where
  ‹decide_or_skip_pre S ⟷
    clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧ get_conflict S = None ∧
    twl_struct_invs S ∧ twl_stgy_invs S›

definition decide_or_skip :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹decide_or_skip S = do {
     ASSERT(decide_or_skip_pre S);
     L ← find_unassigned_lit S;
     case L of
       None ⇒ RETURN (True, S)
     | Some L ⇒ RETURN (False, propagate_dec L S)
  }
›

lemma decide_or_skip_spec:
  assumes ‹clauses_to_update S = {#}› and ‹literals_to_update S = {#}› and ‹get_conflict S = None› and
    twl: ‹twl_struct_invs S› and twl_s: ‹twl_stgy_invs S›
  shows ‹decide_or_skip S ≤ SPEC(λ(brk, T). cdcl_twl_o** S T ∧
       get_conflict T = None ∧
       no_step cdcl_twl_o T ∧ (brk ⟶ no_step cdcl_twl_stgy T) ∧ twl_struct_invs T ∧
       twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
       (¬brk ⟶ literals_to_update T ≠ {#}) ∧
       (¬no_step cdcl_twl_o S ⟶ cdcl_twl_o++ S T))›
proof -
  obtain M N U NE UE NS US N0 U0 where S: ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
    using assms by (cases S) auto
  have atm_N_U:
    ‹atm_of L ∈ atms_of_ms (clause ` set_mset U) ⟹
       atm_of L ∈ atms_of_mm (clauses N + NE + NS + N0)›
    ‹atms_of_mm (get_all_clss (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})) = atms_of_mm (clauses N + NE + NS + N0)›
    for L
  proof -
    have ‹cdclW_restart_mset.no_strange_atm (stateW_of S)› and unit: ‹entailed_clss_inv (pstateW_of S)›
      using twl unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
        pcdcl_all_struct_invs_def
      by auto
    then show
      ‹atm_of L ∈ atms_of_ms (clause ` set_mset U) ⟹ atm_of L ∈ atms_of_mm (clauses N + NE + NS + N0)›
      ‹atms_of_mm (get_all_clss (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})) = atms_of_mm (clauses N + NE + NS + N0)›
      by (auto simp: cdclW_restart_mset.no_strange_atm_def S cdclW_restart_mset_state image_Un)
  qed
  {
    fix L
    assume undef: ‹undefined_lit M L› and L: ‹atm_of L ∈ atms_of_mm (clauses N + NE + NS + N0)›
    let ?T = ‹(Decided L # M, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#- L#})›
    have o: ‹cdcl_twl_o (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#}) ?T›
      by (rule cdcl_twl_o.decide) (use undef L in auto)
    have twl': ‹twl_struct_invs ?T›
      using S cdcl_twl_o_twl_struct_invs o twl by blast
    have twl_s': ‹twl_stgy_invs ?T›
      using S cdcl_twl_o_twl_stgy_invs o twl twl_s by blast
    note o twl' twl_s'
  } note H = this
  have H'[unfolded S, simp]:
    ‹L ∈# all_lits_of_st S ⟷ atm_of L ∈ atms_of_mm (clauses N + NE + NS + N0)› for L
    using atm_N_U(2)
    by (auto simp: S all_lits_of_st_def all_lits_def in_all_lits_of_mm_ain_atms_of_iff)
  show ?thesis
    using assms unfolding S find_unassigned_lit_def propagate_dec_def decide_or_skip_def
      atm_N_U
    apply (refine_vcg)
    subgoal unfolding decide_or_skip_pre_def by blast
    subgoal by fast
    subgoal by blast
    subgoal by (force simp: H elim!: cdcl_twl_oE cdcl_twl_stgyE cdcl_twl_cpE dest!: atm_N_U(1))
    subgoal by (force elim!: cdcl_twl_oE cdcl_twl_stgyE cdcl_twl_cpE)
    subgoal by fast
    subgoal by fast
    subgoal by fast
    subgoal by fast
    subgoal by (auto elim!: cdcl_twl_oE)
    subgoal using atm_N_U(1) H' by (auto simp: cdcl_twl_o.simps decide)
    subgoal by auto
    subgoal by (auto elim!: cdcl_twl_oE)
    subgoal using atm_N_U H by auto
    subgoal using H H' atm_N_U by auto
    subgoal using H H' atm_N_U by auto
    subgoal by auto
    subgoal by auto
    subgoal using H H' atm_N_U by auto
    done
qed

declare decide_or_skip_spec[THEN order_trans, refine_vcg]


subsection ‹Skip and Resolve Loop›

definition skip_and_resolve_loop_inv where
  ‹skip_and_resolve_loop_inv S0 =
    (λ(brk, S). cdcl_twl_o** S0 S ∧ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
          get_conflict S ≠ None ∧
          count_decided (get_trail S) ≠ 0 ∧
          get_trail S ≠ [] ∧
          get_conflict S ≠ Some {#} ∧
          (brk ⟶ no_step cdclW_restart_mset.skip (stateW_of S) ∧
            no_step cdclW_restart_mset.resolve (stateW_of S)))›

definition tl_state :: ‹'v twl_st ⇒ (bool × 'v twl_st)› where
  ‹tl_state = (λ(M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q). do {
      (False, (tl M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q))})›

definition mop_tl_state_pre :: ‹'v twl_st ⇒ bool› where
‹mop_tl_state_pre S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
          get_conflict S ≠ None ∧
          count_decided (get_trail S) ≠ 0 ∧
          get_trail S ≠ [] ∧
          get_conflict S ≠ Some {#} ∧
          is_proped (hd (get_trail S)) ∧
          lit_of (hd (get_trail S)) ∈# all_lits_of_st S ∧
          lit_of (hd (get_trail S)) ∉# the (get_conflict S) ∧
          -lit_of (hd (get_trail S)) ∉# the (get_conflict S)›

definition mop_tl_state :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹mop_tl_state = (λS. do {
    ASSERT(mop_tl_state_pre S);
    RETURN(tl_state S)})›

definition update_confl_tl_pre :: ‹'v literal ⇒ 'v clause ⇒ 'v twl_st ⇒ bool› where
‹update_confl_tl_pre L D S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
          get_conflict S ≠ None ∧
          count_decided (get_trail S) ≠ 0 ∧
          get_trail S ≠ [] ∧
          get_conflict S ≠ Some {#} ∧
          L ∈# D ∧
          -L ∈# the (get_conflict S) ∧
          hd (get_trail S) = Propagated L D ∧
          L ∈# all_lits_of_st S›

definition update_confl_tl :: ‹'v literal ⇒ 'v clause ⇒ 'v twl_st ⇒ (bool × 'v twl_st)› where
  ‹update_confl_tl = (λL C (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q).
     (False, (tl M, N, U, Some (remove1_mset L (remove1_mset (-L) ((the D) ∪# C))), NE, UE, NS, US, N0, U0, WS, Q)))›

definition mop_update_confl_tl :: ‹'v literal ⇒ 'v clause ⇒ 'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹mop_update_confl_tl = (λL C S. do {
     ASSERT(update_confl_tl_pre L C S);
     RETURN (update_confl_tl L C S)})›

definition mop_lit_notin_conflict :: ‹'v literal ⇒ 'v twl_st ⇒ bool nres› where
  ‹mop_lit_notin_conflict L S = do {
    ASSERT(get_conflict S ≠ None ∧ -L ∉# the (get_conflict S) ∧ L ∈# all_lits_of_st S);
    RETURN (L ∉# the (get_conflict S))
  }›

definition mop_maximum_level_removed_pre :: ‹'v literal ⇒ 'v twl_st ⇒ bool› where
‹mop_maximum_level_removed_pre L S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
          get_conflict S ≠ None ∧
          count_decided (get_trail S) ≠ 0 ∧
          get_trail S ≠ [] ∧
          get_conflict S ≠ Some {#} ∧
          -L ∈# the (get_conflict S) ∧
          L = lit_of (hd (get_trail S))›

definition mop_maximum_level_removed :: ‹'v literal ⇒ 'v twl_st ⇒ bool nres› where
‹mop_maximum_level_removed L S = do {
   ASSERT (mop_maximum_level_removed_pre L S);
   RETURN (get_maximum_level (get_trail S) (remove1_mset (-L) (the (get_conflict S))) = count_decided (get_trail S))
}›

definition mop_hd_trail_pre :: ‹'v twl_st ⇒ bool› where
‹mop_hd_trail_pre S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
      get_conflict S ≠ None ∧
      get_trail S ≠ [] ∧ is_proped (hd (get_trail S)) ∧
      get_conflict S ≠ Some {#}›

definition mop_hd_trail :: ‹'v twl_st ⇒ ('v literal × 'v clause) nres› where
  ‹mop_hd_trail S = do{
     ASSERT(mop_hd_trail_pre S);
     SPEC(λ(L, C). Propagated L C = hd (get_trail S))
  }›

definition skip_and_resolve_loop :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹skip_and_resolve_loop S0 =
    do {
      (_, S) ←
        WHILET⇗skip_and_resolve_loop_inv S0⇖
        (λ(uip, S). ¬uip ∧ ¬is_decided (hd (get_trail S)))
        (λ(_, S).
          do {
            (L, C) ← mop_hd_trail S;
            b ← mop_lit_notin_conflict (-L) S;
            if b then
              do {mop_tl_state S}
            else do {
                b ← mop_maximum_level_removed L S;
                if b
                then
                  do {mop_update_confl_tl L C S}
                else
                  do {RETURN (True, S)}}
          }
        )
        (False, S0);
      RETURN S
    }
  ›

lemma skip_and_resolve_loop_spec:
  assumes struct_S: ‹twl_struct_invs S› and stgy_S: ‹twl_stgy_invs S› and
    ‹clauses_to_update S = {#}› and ‹literals_to_update S = {#}› and
    ‹get_conflict S ≠ None› and count_dec: ‹count_decided (get_trail S) > 0›
  shows ‹skip_and_resolve_loop S ≤ SPEC(λT. cdcl_twl_o** S T ∧ twl_struct_invs T ∧ twl_stgy_invs T ∧
      no_step cdclW_restart_mset.skip (stateW_of T) ∧
      no_step cdclW_restart_mset.resolve (stateW_of T) ∧
      get_conflict T ≠ None ∧ clauses_to_update T = {#} ∧ literals_to_update T = {#})›
     (is ‹_ ≤ ?R›)
  unfolding skip_and_resolve_loop_def mop_hd_trail_def nres_monad3 mop_lit_notin_conflict_def
    mop_maximum_level_removed_def
proof (refine_vcg WHILEIT_rule[where R = ‹measure (λ(brk, S). Suc (length (get_trail S) - If brk 1 0))›];
      remove_dummy_vars)
  let ?R = ‹(λa b. SPEC
          (λs'. skip_and_resolve_loop_inv S s' ∧
                (s', a, b)
                ∈ measure
                   (λ(brk, S).
                       Suc (length (get_trail S) - (if brk then 1 else 0)))))›
  show ‹wf (measure (λ(brk, S). Suc (length (get_trail S) - (if brk then 1 else 0))))›
    by auto

  have neg: ‹get_trail S ⊨as CNot (the (get_conflict S))› if ‹get_conflict S ≠ None›
      using assms that unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
        cdclW_restart_mset.cdclW_conflicting_def pcdcl_all_struct_invs_def
      by (cases S, auto simp add: cdclW_restart_mset_state)
  then have ‹get_trail S ≠ []› if ‹get_conflict S ≠ Some {#}›
    using that assms by auto
  then show ‹skip_and_resolve_loop_inv S (False, S)›
    using assms by (cases S) (auto simp: skip_and_resolve_loop_inv_def cdclW_restart_mset.skip.simps
          cdclW_restart_mset.resolve.simps cdclW_restart_mset_state
          twl_stgy_invs_def cdclW_restart_mset.conflict_non_zero_unless_level_0_def)

  fix brk :: bool and T :: ‹'a twl_st›
  assume
    inv: ‹skip_and_resolve_loop_inv S (brk, T)› and
    brk: ‹case (brk, T) of (brk, S) ⇒ ¬ brk ∧ ¬ is_decided (hd (get_trail S))›
  have [simp]: ‹brk = False›
    using brk by auto
  have M_not_empty: ‹get_trail T ≠ []›
    using brk inv unfolding skip_and_resolve_loop_inv_def by auto
  then show ‹mop_hd_trail_pre T›
    using brk inv unfolding skip_and_resolve_loop_inv_def mop_hd_trail_pre_def
    by (cases ‹get_trail T›; cases ‹hd (get_trail T)›)  auto

  fix L :: ‹'a literal› and C
  assume
    LC: ‹case (L, C) of (L, C) ⇒ Propagated L C = hd (get_trail T)›

  obtain M N U D NE UE NS US N0 U0 WS Q where
    T: ‹T = (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    by (cases T)


  obtain M' :: ‹('a, 'a clause) ann_lits› and D' where
    M: ‹get_trail T = Propagated L C # M'› and WS: ‹WS = {#}› and Q: ‹Q = {#}› and D: ‹D = Some D'› and
    st: ‹cdcl_twl_o** S T› and twl: ‹twl_struct_invs T› and D': ‹D' ≠ {#}› and
    twl_stgy_S: ‹twl_stgy_invs T› and
    count_dec[simp]: ‹count_decided (tl M) > 0› ‹count_decided (tl M) ≠ 0› ‹count_decided M ≠ 0›
    using brk inv LC unfolding skip_and_resolve_loop_inv_def
    by (cases ‹get_trail T›; cases ‹hd (get_trail T)›) (auto simp: T)

  show ‹get_conflict T ≠ None›
     by (auto simp: T D)

  have ‹cdclW_restart_mset.cdclW_conflicting (stateW_of T)› and
       ‹cdclW_restart_mset.cdclW_M_level_inv (stateW_of T)› and
       alien: ‹cdclW_restart_mset.no_strange_atm (stateW_of T)›
    using twl D D' M unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      pcdcl_all_struct_invs_def by auto
  then have ‹M ⊨as CNot D'› and n_d: ‹no_dup M› and
    confl_proped: ‹⋀L mark a b.
        a @ Propagated L mark # b = trail (stateW_of T) ⟶
        b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
    using M unfolding cdclW_restart_mset.cdclW_conflicting_def cdclW_restart_mset.cdclW_M_level_inv_def
    by (auto simp add: cdclW_restart_mset_state T D)
  then show ‹- (- L) ∉# the (get_conflict T)›
    using M by (auto simp: T D dest!: multi_member_split uminus_lits_of_l_definedD)
  show alien_L: ‹- L  ∈# all_lits_of_st T›
    using alien M
    by (cases T)
      (auto simp: cdclW_restart_mset.no_strange_atm_def all_lits_of_st_def
        cdclW_restart_mset_state in_all_lits_of_mm_ain_atms_of_iff)

  have LD': ‹L ∉# D'›
    using ‹M ⊨as CNot D'› M n_d
    by (auto dest!: multi_member_split dest: uminus_lits_of_l_definedD simp: T)

  { ― ‹skip›
    assume LD: ‹- L ∉# the (get_conflict T)›
    let ?T = ‹snd (tl_state T)›
    have o_S_T: ‹cdcl_twl_o T ?T›
      using cdcl_twl_o.skip[of L ‹the D› C M' N U NE UE NS US N0 U0]
      using LD D inv M unfolding skip_and_resolve_loop_inv_def T WS Q D by (auto simp: tl_state_def)
    have st_T: ‹cdcl_twl_o** S ?T›
      using st o_S_T by auto
    moreover have twl_T: ‹twl_struct_invs ?T›
      using struct_S twl o_S_T cdcl_twl_o_twl_struct_invs by blast
    moreover have twl_stgy_T: ‹twl_stgy_invs ?T›
      using twl o_S_T stgy_S twl_stgy_S cdcl_twl_o_twl_stgy_invs by blast
    moreover have ‹tl M ≠ []›
      using twl_T D D' unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
        cdclW_restart_mset.cdclW_conflicting_def pcdcl_all_struct_invs_def
      by (auto simp: cdclW_restart_mset_state T tl_state_def)
    moreover have ‹- lit_of (hd M) ∈# all_lits_of_st T› ‹is_proped (hd M)›
       ‹- lit_of (hd M) ∉# the (get_conflict T)›  ‹lit_of (hd M) ∉# the (get_conflict T)›
      using M alien_L LD LD' D
      by (auto intro!: ASSERT_leI simp: T tl_state_def in_all_lits_of_mm_uminus_iff)
    ultimately show ‹mop_tl_state T ≤ ?R brk T›
      using WS Q D D' twl_stgy_S twl alien_L LD
      unfolding skip_and_resolve_loop_inv_def mop_tl_state_pre_def mop_tl_state_def all_lits_of_st_def
      by (auto intro!: ASSERT_leI simp: T tl_state_def in_all_lits_of_mm_uminus_iff)
  }

  { ― ‹resolve›
    assume
      LD: ‹¬- L ∉# the (get_conflict T)›

    have count_dec': ‹count_decided M' = count_decided M›
      using M unfolding T by auto
    then show mop_maximum_level_removed_pre: ‹mop_maximum_level_removed_pre L T›
      using count_dec twl_stgy_S twl D' LD M unfolding mop_maximum_level_removed_pre_def
      by (auto simp: T D WS Q simp del: count_dec)

    assume
      max: ‹get_maximum_level (get_trail T) (remove1_mset (-L) (the (get_conflict T)))
        = count_decided (get_trail T)›

    let ?D = ‹remove1_mset (- L) (the (get_conflict T)) ∪# remove1_mset L C›
    let ?T = ‹snd (update_confl_tl L C T)›

    have ‹cdclW_restart_mset.cdclW_conflicting (stateW_of T)›
      using twl D D' M unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
        pcdcl_all_struct_invs_def by auto
    then have ‹L ∈# C› ‹M' ⊨as CNot (remove1_mset L C)› ‹M ⊨as CNot D'›
      using M
      unfolding cdclW_restart_mset.cdclW_conflicting_def
      by (force simp: T cdclW_restart_mset_state D)+
    then have ‹-L ∉# C›
      using n_d M by (auto simp: T add_mset_eq_add_mset Decided_Propagated_in_iff_in_lits_of_l
         dest!: multi_member_split)
    have ‹L ∉# D'›
      using ‹M ⊨as CNot D'› M n_d
      by (auto simp: T Decided_Propagated_in_iff_in_lits_of_l
         dest!: multi_member_split)
    then have D_alt[simp]: ‹D' ∪# C - {#L, - L#} = ?D›
      ‹the D ∪# C - {#L, - L#} = ?D›
      using LD ‹L ∈# C› ‹-L ∉# C›
      by (auto simp: T D sup_union_right1 dest!: multi_member_split)
    have o_S_T: ‹cdcl_twl_o T ?T›
      using cdcl_twl_o.resolve[of L ‹the D› C M' N U NE UE] LD D max M WS Q D
      by (auto simp: T D update_confl_tl_def)
    then have st_T: ‹cdcl_twl_o** S ?T›
      using st by auto
    moreover have twl_T: ‹twl_struct_invs ?T›
      using st_T twl o_S_T cdcl_twl_o_twl_struct_invs by blast
    moreover have twl_stgy_T: ‹twl_stgy_invs ?T›
      using twl o_S_T twl_stgy_S cdcl_twl_o_twl_stgy_invs by blast
    moreover {
      have ‹cdclW_restart_mset.cdclW_conflicting (stateW_of ?T)›
      using twl_T D D' M unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      pcdcl_all_struct_invs_def by auto
      then have ‹tl M ⊨as CNot ?D›
        using M unfolding cdclW_restart_mset.cdclW_conflicting_def
        by (auto simp add: cdclW_restart_mset_state T update_confl_tl_def)
    }
    moreover have ‹get_conflict ?T ≠ Some {#}›
      using twl_stgy_T count_dec unfolding twl_stgy_invs_def update_confl_tl_def
        cdclW_restart_mset.conflict_non_zero_unless_level_0_def T
        by (auto simp: trail.simps conflicting.simps)
    moreover have ‹update_confl_tl_pre L C T›
      using WS Q D D' mop_maximum_level_removed_pre twl_stgy_T twl twl_stgy_S M LD count_dec
        confl_proped[of ‹[]› L C ‹M'›] alien_L
      unfolding skip_and_resolve_loop_inv_def
      by (auto simp add: cdclW_restart_mset.skip.simps cdclW_restart_mset.resolve.simps all_lits_of_st_def
          cdclW_restart_mset_state update_confl_tl_def T update_confl_tl_pre_def in_all_lits_of_mm_uminus_iff)
    ultimately show  ‹mop_update_confl_tl L C T ≤ ?R brk T›
      using WS Q D D' mop_maximum_level_removed_pre M count_dec unfolding skip_and_resolve_loop_inv_def
      by (auto simp add: cdclW_restart_mset.skip.simps cdclW_restart_mset.resolve.simps
          cdclW_restart_mset_state update_confl_tl_def T mop_update_confl_tl_def)
  }
  { ― ‹No step›
    assume
      LD: ‹¬- L ∉# the (get_conflict T)› and
      max: ‹get_maximum_level (get_trail T) (remove1_mset (- L) (the (get_conflict T)))
         ≠ count_decided (get_trail T)›

    show ‹skip_and_resolve_loop_inv S (True, T)›
      using inv max LD D M unfolding skip_and_resolve_loop_inv_def
      by (auto simp add: cdclW_restart_mset.skip.simps cdclW_restart_mset.resolve.simps
          cdclW_restart_mset_state T)
    show ‹((True, T), (brk, T)) ∈ measure (λ(brk, S). Suc (length (get_trail S) - (if brk then 1 else 0)))›
      using M_not_empty by simp
  }
next ― ‹Final properties›
  fix brk T U
  assume
    inv: ‹skip_and_resolve_loop_inv S (brk, T)› and
    brk: ‹¬(case (brk, T) of (brk, S) ⇒ ¬ brk ∧ ¬ is_decided (hd (get_trail S)))›
  show ‹cdcl_twl_o** S T›
    using inv by (auto simp add: skip_and_resolve_loop_inv_def)

  { assume ‹is_decided (hd (get_trail T))›
    then have ‹no_step cdclW_restart_mset.skip (stateW_of T)› and
        ‹no_step cdclW_restart_mset.resolve (stateW_of T)›
      by (cases T;  auto simp add: cdclW_restart_mset.skip.simps
          cdclW_restart_mset.resolve.simps cdclW_restart_mset_state)+
  }
  moreover
  { assume ‹brk›
    then have ‹no_step cdclW_restart_mset.skip (stateW_of T)› and
      ‹no_step cdclW_restart_mset.resolve (stateW_of T)›
      using inv by (auto simp: skip_and_resolve_loop_inv_def)
  }
  ultimately show ‹¬ cdclW_restart_mset.skip (stateW_of T) U› and
    ‹¬ cdclW_restart_mset.resolve (stateW_of T) U›
    using brk unfolding prod.case by blast+

  show ‹twl_struct_invs T›
    using inv unfolding skip_and_resolve_loop_inv_def by auto
  show ‹twl_stgy_invs T›
    using inv unfolding skip_and_resolve_loop_inv_def by auto

  show ‹get_conflict T ≠ None›
    using inv by (auto simp: skip_and_resolve_loop_inv_def)

  show ‹clauses_to_update T = {#}›
    using inv by (auto simp: skip_and_resolve_loop_inv_def)

  show ‹literals_to_update T = {#}›
    using inv by (auto simp: skip_and_resolve_loop_inv_def)
qed

declare skip_and_resolve_loop_spec[THEN order_trans, refine_vcg]


subsection ‹Backtrack›

definition extract_shorter_conflict_pre :: ‹'v twl_st ⇒ bool› where
  ‹extract_shorter_conflict_pre S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧ get_trail S ≠ []›

definition extract_shorter_conflict :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹extract_shorter_conflict = (λ(M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q). do {
    ASSERT(extract_shorter_conflict_pre (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q));
    SPEC(λS'. ∃D'. S' = (M, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q) ∧
       D' ⊆# the D ∧ clause `# (N + U) + NE + NS + UE + US + N0 + U0 ⊨pm D' ∧ -lit_of (hd M) ∈# D')
  })›

fun equality_except_conflict :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
‹equality_except_conflict (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)
    (M', N', U', D', NE', UE', NS', US', N0', U0', WS', Q') ⟷
  M = M' ∧ N = N' ∧ U = U' ∧ NE = NE' ∧ UE = UE' ∧ NS = NS' ∧ US = US' ∧ N0 = N0' ∧ U0 = U0' ∧
      WS = WS' ∧ Q = Q'›

lemma extract_shorter_conflict_alt_def:
  ‹extract_shorter_conflict S = do {
   ASSERT(extract_shorter_conflict_pre S);
    SPEC(λS'. ∃D'. equality_except_conflict S S' ∧ Some D' = get_conflict S' ∧
       D' ⊆# the (get_conflict S) ∧ clause `# (get_clauses S) + unit_clss S + subsumed_clauses S + get_all_clauses0 S ⊨pm D' ∧
       -lit_of (hd (get_trail S)) ∈# D')}›
  unfolding extract_shorter_conflict_def
  by (cases S) (auto simp: ac_simps intro!: bind_cong[OF refl])

definition reduce_trail_bt :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹reduce_trail_bt = (λL (M, N, U, D', NE, UE, WS, Q). do {
        M1 ← SPEC(λM1. ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
              get_level M K = get_maximum_level M (the D' - {#-L#}) + 1);
        RETURN (M1, N, U, D', NE, UE, WS, Q)
  })›

definition propagate_bt_pre :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st ⇒ bool› where
  ‹propagate_bt_pre L L' S ⟷ (∃M N U D NE UE NS US WS Q M' D'.
    S = (M, N, U, Some D, NE, UE,NS, US,  WS, Q) ∧
    twl_stgy_invs (M' @ M, N, U, Some D', NE, UE, NS, US, WS, Q) ∧
    twl_struct_invs (M' @ M, N, U, Some D', NE, UE, NS, US, WS, Q) ∧
    D ⊆# D' ∧
    -L ∈# D ∧
    get_conflict S ≠ None ∧
    L' ∈# D - {#-L#} ∧
    L ≠ -L' ∧
    get_level (M) L' = get_maximum_level (M) (D - {#-L#}) ∧
    undefined_lit M L ∧
    L ∈# all_lits_of_st  (M, N, U, Some D, NE, UE, NS, US, WS, Q)∧
    L' ∈# all_lits_of_st  (M, N, U, Some D, NE, UE, NS, US, WS, Q) ∧
    (set_mset (all_lits_of_m D) ⊆
       set_mset (all_lits_of_st  (M, N, U, Some D, NE, UE, NS, US, WS, Q))))›

definition propagate_bt :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st ⇒ 'v twl_st› where
  ‹propagate_bt = (λL L' (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q). do {
      (Propagated (-L) (the D) # M, N, add_mset (TWL_Clause {#-L, L'#} (the D - {#-L, L'#})) U,
      None, NE, UE, NS, US, N0, U0, WS, {#L#})
   })›

definition mop_propagate_bt :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹mop_propagate_bt = (λL L' S. do {
     ASSERT(propagate_bt_pre L L' S);
     RETURN (propagate_bt L L' S)
   })›


definition propagate_unit_bt_pre :: ‹'v literal ⇒ 'v twl_st ⇒ bool› where
  ‹propagate_unit_bt_pre L S ⟷ (∃M N U NE UE NS US N0 U0 WS Q M' D'.
    S = (M, N, U, Some {#-L#}, NE, UE, NS, US, N0, U0, WS, Q) ∧
    twl_stgy_invs (M' @ M, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q) ∧
    twl_struct_invs (M' @ M, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q) ∧
    {#-L#} ⊆# D' ∧
    undefined_lit M L ∧
    L ∈# all_lits_of_st (M, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q))›

definition propagate_unit_bt :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st› where
  ‹propagate_unit_bt = (λL (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q).
     (Propagated (-L) (the D) # M, N, U, None, NE, add_mset (the D) UE, NS, US, N0, U0, WS, {#L#}))›


definition mop_propagate_unit_bt :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹mop_propagate_unit_bt = (λL S. do {
    ASSERT (propagate_unit_bt_pre L S);
    RETURN (propagate_unit_bt L S)
  })›


definition mop_lit_hd_trail_pre :: ‹'v twl_st ⇒ bool› where
‹mop_lit_hd_trail_pre S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
      clauses_to_update S = {#} ∧ literals_to_update S = {#} ∧
      get_conflict S ≠ None ∧
      get_trail S ≠ [] ∧
      get_conflict S ≠ Some {#}›

definition mop_lit_hd_trail :: ‹'v twl_st ⇒ ('v literal) nres› where
  ‹mop_lit_hd_trail S = do {
     ASSERT(mop_lit_hd_trail_pre S);
     SPEC(λL. L = lit_of (hd (get_trail S)))
  }›

definition backtrack_inv where
  ‹backtrack_inv S ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧ get_trail S ≠ [] ∧
    get_conflict S ≠ None ∧ get_conflict S ≠ Some {#} ∧ -lit_of (hd (get_trail S)) ∈# the (get_conflict S) ∧
    no_step cdclW_restart_mset.skip (stateW_of S) ∧ no_step cdclW_restart_mset.resolve (stateW_of S)›

definition find_lit_of_max_level where
   ‹find_lit_of_max_level =  (λS L. do {
    ASSERT(distinct_mset (the (get_conflict S)) ∧ -L ∈# the (get_conflict S));
    SPEC(λL'. L' ∈# the (get_conflict S) - {#-L#} ∧
      get_level (get_trail S) L' = get_maximum_level (get_trail S) (the (get_conflict S) - {#-L#}))
   })›



definition backtrack :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹backtrack S =
    do {
      ASSERT(backtrack_inv S);
      L ← mop_lit_hd_trail S;
      S ← extract_shorter_conflict S;
      S ← reduce_trail_bt L S;

      if size (the (get_conflict S)) > 1
      then do {
        L' ← find_lit_of_max_level S L;
        mop_propagate_bt L L' S
      }
      else do {
        mop_propagate_unit_bt L S
      }
    }
  ›

lemma
  assumes confl: ‹get_conflict S ≠ None› ‹get_conflict S ≠ Some {#}› and
    w_q: ‹clauses_to_update S = {#}› and p: ‹literals_to_update S = {#}› and
    ns_s: ‹no_step cdclW_restart_mset.skip (stateW_of S)› and
    ns_r: ‹no_step cdclW_restart_mset.resolve (stateW_of S)› and
    twl_struct: ‹twl_struct_invs S› and twl_stgy: ‹twl_stgy_invs S›
  shows
    backtrack_spec:
    ‹backtrack S ≤ SPEC (λT. cdcl_twl_o S T ∧ get_conflict T = None ∧ no_step cdcl_twl_o T ∧
      twl_struct_invs T ∧ twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
      literals_to_update T ≠ {#})› (is ?spec) and
    backtrack_nofail:
      ‹nofail (backtrack S)› (is ?fail)
proof -
  let ?S = ‹stateW_of S›
  have inv_s: ‹cdclW_restart_mset.cdclW_stgy_invariant ?S› and
    inv: ‹cdclW_restart_mset.cdclW_all_struct_inv ?S›
    using twl_struct twl_stgy unfolding pcdcl_all_struct_invs_def twl_struct_invs_def
      twl_stgy_invs_def by auto
  let ?D' = ‹the (conflicting ?S)›
  have M_CNot_D': ‹trail ?S ⊨as CNot ?D'› and
     dist: ‹distinct_mset ?D'›
    using inv confl unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_conflicting_def
      cdclW_restart_mset.distinct_cdclW_state_def
    by (cases ‹conflicting ?S›; cases S; auto simp: cdclW_restart_mset_state; fail)+
  then have trail: ‹get_trail S ≠ []›
    using confl unfolding true_annots_true_cls_def_iff_negation_in_model
    by (cases S) (auto simp: cdclW_restart_mset_state)
   have all_struct:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (stateW_of S)›
      using twl_struct
      by (auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def)
    then have uL_D: ‹- lit_of (hd (get_trail S)) ∈# the (get_conflict S)›
      using cdclW_restart_mset.no_step_skip_hd_in_conflicting[of
          ‹stateW_of S›] ns_s ns_r confl twl_stgy
      by (auto simp: twl_st twl_stgy_invs_def pcdcl_all_struct_invs_def)

  show ?spec
    unfolding backtrack_def extract_shorter_conflict_def reduce_trail_bt_def
     mop_lit_hd_trail_def mop_propagate_bt_def mop_propagate_unit_bt_def
     find_lit_of_max_level_def
  proof (refine_vcg; remove_dummy_vars; clarify?)
    show ‹backtrack_inv S›
      using uL_D trail confl assms unfolding backtrack_inv_def by fast
    show ‹mop_lit_hd_trail_pre S›
      using trail confl assms unfolding mop_lit_hd_trail_pre_def
      by auto
    fix M M1 M2 :: ‹('a, 'a clause) ann_lits› and
      N U :: ‹'a twl_clss› and
      D :: ‹'a clause option› and D' :: ‹'a clause› and NE UE NS US N0 U0 :: ‹'a clauses› and
      WS :: ‹'a clauses_to_update› and Q :: ‹'a lit_queue› and K K' :: ‹'a literal›
    let ?S = ‹(M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    let ?T = ‹(M, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q)›
    let ?U = ‹(M1, N, U, Some D', NE, UE, NS, US, N0, U0, WS, Q)›
    let ?MS = ‹get_trail ?S›
    let ?MT = ‹get_trail ?T›
    assume
      S: ‹S = (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q)›
    show ‹extract_shorter_conflict_pre ?S›
      using assms trail unfolding S extract_shorter_conflict_pre_def by auto
  have alien: ‹cdclW_restart_mset.no_strange_atm (stateW_of S)› and
    ‹cdclW_restart_mset.cdclW_M_level_inv (stateW_of S)›
    using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+
  then have alien_L: ‹lit_of (hd M) ∈# all_lits_of_st ?S›
    using trail unfolding cdclW_restart_mset.no_strange_atm_def
      cdclW_restart_mset.cdclW_M_level_inv_def all_lits_of_st_def
    by (cases M) (auto simp: S cdclW_restart_mset_state in_all_lits_of_mm_ain_atms_of_iff)

    assume
      D'_D: ‹D' ⊆# the D› and
      L_D': ‹-lit_of (hd M) ∈# D'›
    show ‹distinct_mset (the (get_conflict ?U))›
      using dist distinct_mset_mono[OF D'_D] by (auto simp: S cdclW_restart_mset_state)
    show ‹- lit_of (hd (get_trail ?S)) ∈# the (get_conflict ?U)›
      using L_D' by (auto simp: S)

    assume
      N_U_NE_UE_D': ‹clauses (N + U) + NE + NS + UE + US + N0 + U0 ⊨pm D'› and
      decomp: ‹(Decided K' # M1, M2) ∈ set (get_all_ann_decomposition M)› and
      lev_K': ‹get_level M K' = get_maximum_level M (remove1_mset (- lit_of (hd ?MS))
               (the (Some D'))) + 1›
    have WS: ‹WS = {#}› and Q: ‹Q = {#}›
      using w_q p unfolding S by auto

    have uL_D: ‹- lit_of (hd M) ∈# the D›
      using decomp N_U_NE_UE_D' D'_D L_D' lev_K'
      unfolding WS Q
      by auto

    have D_Some_the: ‹D = Some (the D)›
      using confl S by auto
    let ?S' = ‹stateW_of S›
    have inv_s: ‹cdclW_restart_mset.cdclW_stgy_invariant ?S'› and
      inv: ‹cdclW_restart_mset.cdclW_all_struct_inv ?S'›
      using twl_struct twl_stgy unfolding twl_struct_invs_def twl_stgy_invs_def
        pcdcl_all_struct_invs_def by auto
    have Q: ‹Q = {#}› and WS: ‹WS = {#}›
      using w_q p unfolding S by auto
    have M_CNot_D': ‹M ⊨as CNot D'›
      using M_CNot_D' S D'_D
      by (auto simp: cdclW_restart_mset_state true_annots_true_cls_def_iff_negation_in_model)
    obtain L'' M' where M: ‹M = L'' # M'›
      using trail S by (cases M) auto
    have D'_empty: ‹D' ≠ {#}›
      using L_D' by auto
    have L'_D: ‹-lit_of L'' ∈# D'›
      using L_D' by (auto simp: cdclW_restart_mset_state M)
    have lev_inv: ‹cdclW_restart_mset.cdclW_M_level_inv ?S'›
      using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast
    then have n_d: ‹no_dup M› and dec: ‹backtrack_lvl ?S' = count_decided M›
      using S unfolding cdclW_restart_mset.cdclW_M_level_inv_def
      by (auto simp: cdclW_restart_mset_state)
    then have uL''_M: ‹-lit_of L'' ∉ lits_of_l M›
      by (auto simp: Decided_Propagated_in_iff_in_lits_of_l M)
    have ‹get_maximum_level M (remove1_mset (-lit_of (hd M)) D') < count_decided M›
    proof (cases L'')
      case (Decided x1) note L'' = this(1)
      have ‹distinct_mset (the D)›
        using inv S confl unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
          cdclW_restart_mset.distinct_cdclW_state_def
        by (auto simp: cdclW_restart_mset_state)
      then have ‹distinct_mset D'›
        using D'_D by (blast intro: distinct_mset_mono)
      then have ‹- x1 ∉# remove1_mset (- x1) D'›
        using L'_D L'' D'_D by (auto dest: distinct_mem_diff_mset)
      then have H: ‹∀x∈#remove1_mset (- lit_of (hd M)) D'. undefined_lit [L''] x›
        using L'' M_CNot_D' uL''_M
        by (fastforce simp: atms_of_def atm_of_eq_atm_of M true_annots_true_cls_def_iff_negation_in_model
            dest: in_diffD)
      have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) D') =
        get_maximum_level M' (remove1_mset (- lit_of (hd M)) D')›
        using get_maximum_level_skip_beginning[OF H, of M'] M
        by auto
      then show ?thesis
        using count_decided_ge_get_maximum_level[of M' ‹remove1_mset (-lit_of (hd M)) D'›] M L''
        by simp
    next
      case (Propagated L C) note L'' = this(1)
      moreover {
        have ‹∀L mark a b. a @ Propagated L mark # b = trail (stateW_of S) ⟶
          b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
          using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
            cdclW_restart_mset.cdclW_conflicting_def
          by blast
        then have ‹L ∈# C›
          by (force simp: S M cdclW_restart_mset_state L'') }
      moreover have D_empty: ‹the D ≠ {#}›
        using D'_D D'_empty by auto
      moreover have ‹-L ∈# the D›
        using ns_s L'' confl D_empty
        by (force simp: cdclW_restart_mset.skip.simps S M cdclW_restart_mset_state)
      ultimately have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))
          < count_decided M›
        using ns_r confl count_decided_ge_get_maximum_level[of M
	  ‹remove1_mset (-lit_of (hd M)) (the D)›]
        by (fastforce simp add: cdclW_restart_mset.resolve.simps S M
            cdclW_restart_mset_state)

      moreover have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) D') ≤
              get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))›
        by (rule get_maximum_level_mono) (use D'_D in ‹auto intro: mset_le_subtract›)
      ultimately show ?thesis
        by simp
    qed

    then have ‹∃K M1 M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
      get_level M K = get_maximum_level M (remove1_mset (-lit_of (hd M)) D') + 1›
      using cdclW_restart_mset.backtrack_ex_decomp n_d
      by (auto simp: cdclW_restart_mset_state S)

    define i where ‹i = get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›

    let ?T =  ‹(Propagated (-lit_of (hd M)) D' # M1, N,
      add_mset (TWL_Clause {#-lit_of (hd M), K#} (D' - {#-lit_of (hd M), K#})) U,
      None, NE, UE, NS, US, N0, U0, WS, {#lit_of (hd M)#})›
    let ?T' = ‹(Propagated (-lit_of (hd M)) D' # M1, N,
      add_mset (TWL_Clause {#-lit_of (hd M), K#} (D' - {#-lit_of (hd M), K#})) U,
      None, NE, UE, NS, US, N0, U0, WS, {#- (-lit_of (hd M))#})›

    have lev_D': ‹count_decided M = get_maximum_level (L'' # M') D'›
      using count_decided_ge_get_maximum_level[of M D'] L'_D
        get_maximum_level_ge_get_level[of ‹-lit_of L''› D' M] unfolding M
      by (auto split: if_splits)

    have ‹the D ≠ {#}›
      using D'_D D'_empty L'_D by (auto)
    have uL'_D: ‹lit_of L'' ∉# D'›
      using L_D' n_d M_CNot_D' by (auto simp: cdclW_restart_mset_state M add_mset_eq_add_mset
          Decided_Propagated_in_iff_in_lits_of_l
        dest!: multi_member_split)

    { ― ‹conflict clause > 1 literal›
      assume size_D: ‹1 < size (the (get_conflict ?U))› and
      K_D: ‹K ∈# remove1_mset (- lit_of (hd ?MS)) (the (get_conflict ?U))› and
      lev_K: ‹get_level (get_trail ?U) K = get_maximum_level (get_trail ?U)
          (remove1_mset (- lit_of (hd (get_trail ?S))) (the (get_conflict ?U)))›
      have neq: ‹lit_of (hd M) ≠ - K›
        using dist K_D D'_D L_D' distinct_mset_mono[OF D'_D]
        by (auto simp: S conflicting.simps M distinct_mset_remove1_All)
      moreover have ‹undefined_lit M1 (lit_of (hd (get_trail ?S)))›
        using decomp n_d M
        apply (auto simp: dest!: get_all_ann_decomposition_exists_prepend)
        apply (case_tac c; case_tac M2)
        apply auto
        done
      moreover have ‹lit_of (hd (get_trail ?S)) ∈# all_lits_of_st ?S›
        using alien_L by (auto simp: M)
      moreover have ‹K ∈# all_lits_of_st ?S›
        using alien  neq  mset_subset_eqD[OF D'_D in_diffD[OF K_D,
            unfolded get_conflict.simps option.sel]] assms(1)
        unfolding cdclW_restart_mset.no_strange_atm_def all_lits_of_st_def all_lits_of_st_def
        by (auto simp: S cdclW_restart_mset_state in_all_lits_of_mm_ain_atms_of_iff
          dest!: multi_member_split)
      moreover have ‹set_mset (all_lits_of_m D') ⊆ set_mset (all_lits_of_st ?S)›
        using alien assms(1) atms_of_subset_mset_mono[OF D'_D]
        unfolding cdclW_restart_mset.no_strange_atm_def all_lits_of_st_def
        by (fastforce simp: S cdclW_restart_mset_state in_all_lits_of_mm_ain_atms_of_iff
             in_all_lits_of_m_ain_atms_of_iff)
      ultimately show ‹propagate_bt_pre (lit_of (hd (get_trail ?S))) K ?U›
        using ‹the D ≠ {#}› assms D'_D D'_empty L'_D K_D uL'_D lev_K
           get_all_ann_decomposition_exists_prepend[OF decomp] uL_D
        unfolding propagate_bt_pre_def S all_lits_of_st_def
        by (auto simp: L_D' intro!: exI[of _ ‹take (length M - length M1) M›]
           exI[of _ ‹the D›])
      have ‹∀L' ∈# D'. -L' ∈ lits_of_l M›
        using M_CNot_D' uL''_M
        by (fastforce simp: atms_of_def atm_of_eq_atm_of M true_annots_true_cls_def_iff_negation_in_model
            dest: in_diffD)
      obtain c where c: ‹M = c @ M2 @ Decided K' # M1›
        using get_all_ann_decomposition_exists_prepend[OF decomp] by blast
      have ‹get_level M K' = Suc (count_decided M1)›
        using n_d unfolding c by auto
      then have i: ‹i = count_decided M1›
        using lev_K' unfolding i_def by auto
      have lev_M_M1: ‹∀L' ∈# D' - {#-lit_of (hd M)#}. get_level M L' = get_level M1 L'›
      proof
        fix L'
        assume L': ‹L' ∈# D' - {#-lit_of (hd M)#}›
        have ‹get_level M L' > count_decided M1› if ‹defined_lit (c @ M2 @ Decided K' # []) L'›
          using get_level_skip_end[OF that, of M1] n_d that get_level_last_decided_ge[of ‹c @ M2›]
          by (auto simp: c)
        moreover have ‹get_level M L' ≤ i›
          using get_maximum_level_ge_get_level[OF L', of M] unfolding i_def by auto
        ultimately show ‹get_level M L' = get_level M1 L'›
          using n_d c L' i by (cases ‹defined_lit (c @ M2 @ Decided K' # []) L'›) auto
      qed
      have ‹get_level M1 `# remove1_mset (- lit_of (hd M)) D' = get_level M `# remove1_mset (- lit_of (hd M)) D'›
        by (rule image_mset_cong) (use lev_M_M1 in auto)
      then have max_M1_M1_D: ‹get_maximum_level M1 (remove1_mset (- lit_of (hd M)) D') =
        get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›
        unfolding get_maximum_level_def by argo


      have ‹∃L' ∈# remove1_mset (-lit_of (hd M)) D'.
           get_level M L' = get_maximum_level M (remove1_mset (- lit_of (hd M)) D')›
        by (rule get_maximum_level_exists_lit_of_max_level)
          (use size_D in ‹auto simp: remove1_mset_empty_iff›)
      have D'_ne_single: ‹D' ≠ {#- lit_of (hd M)#}›
        using size_D apply (cases D', simp)
        apply (rename_tac L D'')
        apply (case_tac D'')
        by simp_all
      have cdcl: ‹cdcl_twl_o (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ?T'›
        unfolding Q WS option.sel list.sel
        apply (subst D_Some_the)
        apply (rule cdcl_twl_o.backtrack_nonunit_clause[of ‹-lit_of (hd M)› _ K' M1 M2 _ _ i])
        subgoal using D'_D L_D' by blast
        subgoal using L'_D decomp M by auto
        subgoal using L'_D decomp M by auto
        subgoal using L'_D M lev_D' by auto
        subgoal using i lev_D' i_def by auto
        subgoal using lev_K' i_def by auto
        subgoal using D'_ne_single .
        subgoal using D'_D .
        subgoal using N_U_NE_UE_D' by (auto simp: ac_simps)
        subgoal using L_D' .
        subgoal using K_D by (auto dest: in_diffD)
        subgoal using lev_K lev_M_M1 K_D by (simp add: i_def max_M1_M1_D)
        done
    moreover have ‹get_conflict ?T' = None ∧ clauses_to_update ?T' = {#} ∧ literals_to_update ?T' ≠ {#}›
      unfolding WS Q
        using S cdcl_twl_o_twl_struct_invs twl_struct by (auto simp: propagate_bt_def)
    moreover have ‹(∀S'. ¬ cdcl_twl_o ?T' S')› by (auto simp: cdcl_twl_o.simps)
    moreover have ‹twl_struct_invs ?T'›
        using S cdcl cdcl_twl_o_twl_struct_invs[OF cdcl] twl_struct twl_stgy by auto
    moreover have ‹twl_stgy_invs ?T'›
        using S cdcl cdcl_twl_o_twl_stgy_invs[OF cdcl] twl_struct twl_stgy by auto
    moreover have ‹clauses_to_update ?T' = {#}›
        using WS by (auto simp: propagate_bt_def)

    moreover have False if ‹cdcl_twl_o ?T' (an, ao, ap, aq, ar, as, at', b)›
        for an ao ap aq ar as at' b
        using that by (auto simp: cdcl_twl_o.simps propagate_bt_def)
    ultimately show cdcl:
       ‹cdcl_twl_o ?S (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
       ‹get_conflict (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = None›
       ‹twl_struct_invs (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
       ‹twl_stgy_invs (propagate_bt (lit_of (hd (get_trail ?S))) K ?U)›
       ‹clauses_to_update (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = {#}›
       ‹⋀S'. cdcl_twl_o (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) S' ⟹ False›
       ‹literals_to_update (propagate_bt (lit_of (hd (get_trail ?S))) K ?U) = {#} ⟹ False›
      unfolding propagate_bt_def by auto
    }

    { ― ‹conflict clause has 1 literal›
      assume ‹¬ 1 < size (the (get_conflict ?U))›
      then have D': ‹D' = {#-lit_of (hd M)#}›
        using L'_D by (cases D') (auto simp: M)
      let ?T = ‹(Propagated (- lit_of (hd M)) D' # M1, N, U, None, NE, add_mset D' UE, NS, US, N0, U0, WS,
        unmark (hd M))›
      let ?T' = ‹(Propagated (- lit_of (hd M)) D' # M1, N, U, None, NE, add_mset D' UE, NS, US, N0, U0, WS,
        {#- (-lit_of (hd M))#})›

      have i_0: ‹i = 0›
        using i_def by (auto simp: D')

      have cdcl: ‹cdcl_twl_o (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ?T'›
        unfolding D' option.sel WS Q apply (subst D_Some_the)
        apply (rule cdcl_twl_o.backtrack_unit_clause[of _ ‹the D› K' M1 M2 _ D' i])
        subgoal using D'_D D' by auto
        subgoal using decomp by simp
        subgoal by (simp add: M)
        subgoal using D' by (auto simp: get_maximum_level_add_mset)
        subgoal using i_def by simp
        subgoal using lev_K' i_def[symmetric] by auto
        subgoal using D' .
        subgoal using D'_D .
        subgoal using N_U_NE_UE_D' by (auto simp: ac_simps)
        done
      moreover have ‹get_conflict ?T' = None›
        by (auto simp add: propagate_unit_bt_def)

      moreover have ‹twl_struct_invs ?T'›
        using S cdcl cdcl_twl_o_twl_struct_invs twl_struct by blast

      moreover have ‹twl_stgy_invs ?T'›
        using S cdcl cdcl_twl_o_twl_stgy_invs twl_struct twl_stgy by blast
      moreover have ‹clauses_to_update ?T' = {#}›
        using WS by (auto simp add: propagate_unit_bt_def)
      ultimately show cdcl:
       ‹cdcl_twl_o ?S (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
       ‹get_conflict (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = None›
       ‹twl_struct_invs (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
       ‹twl_stgy_invs (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U)›
       ‹clauses_to_update (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = {#}›
      unfolding propagate_unit_bt_def by auto
      show False if ‹literals_to_update (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) = {#}›
        using that by (auto simp add: propagate_unit_bt_def)
      fix an ao ap aq ar as at' b
      show False if ‹cdcl_twl_o (propagate_unit_bt (lit_of (hd (get_trail ?S))) ?U) (an, ao, ap, aq, ar, as, at', b)›
        using that by (auto simp: cdcl_twl_o.simps propagate_unit_bt_def)
      have ‹undefined_lit M1 (lit_of (hd (get_trail ?S)))›
        using decomp n_d M
        apply (auto simp: dest!: get_all_ann_decomposition_exists_prepend)
        apply (case_tac c; case_tac M2)
        apply auto
        done
      then show ‹propagate_unit_bt_pre (lit_of (hd (get_trail ?S))) ?U›
        using ‹the D ≠ {#}› assms D'_D D'_empty L'_D uL'_D alien_L cdcl
           get_all_ann_decomposition_exists_prepend[OF decomp] uL_D
        unfolding propagate_unit_bt_pre_def S all_lits_of_st_def
        by (auto simp: L_D' D' intro!: exI[of _ ‹take (length M - length M1) M›]
           exI[of _ ‹the D›])
    }
  qed
  then show ?fail
    using nofail_simps(2) pwD1 by blast
qed

declare backtrack_spec[THEN order_trans, refine_vcg]


subsection ‹Full loop›

definition cdcl_twl_o_prog_pre :: ‹'v twl_st ⇒ bool› where
  ‹cdcl_twl_o_prog_pre S' ⟷
     no_step cdcl_twl_cp S' ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
      clauses_to_update S' = {#} ∧ literals_to_update S' = {#}›

definition cdcl_twl_o_prog :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹cdcl_twl_o_prog S =
    do {
      ASSERT(cdcl_twl_o_prog_pre S);
      if get_conflict S = None
      then decide_or_skip S
      else do {
        if count_decided (get_trail S) > 0
        then do {
          T ← skip_and_resolve_loop S;
          ASSERT(get_conflict T ≠ None ∧ get_conflict T ≠ Some {#});
          U ← backtrack T;
          RETURN (False, U)
        }
        else
          RETURN (True, S)
      }
    }
  ›

setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper ("split_all_tac"))›
declare split_paired_All[simp del]

lemma skip_and_resolve_same_decision_level:
  assumes ‹cdcl_twl_o S T›  ‹get_conflict T ≠ None›
  shows  ‹count_decided (get_trail T) = count_decided (get_trail S)›
  using assms by (induction rule: cdcl_twl_o.induct) auto


lemma skip_and_resolve_conflict_before:
  assumes ‹cdcl_twl_o S T› ‹get_conflict T ≠ None›
  shows  ‹get_conflict S ≠ None›
  using assms by (induction rule: cdcl_twl_o.induct) auto

lemma rtranclp_skip_and_resolve_same_decision_level:
  ‹cdcl_twl_o** S T ⟹ get_conflict S ≠ None ⟹ get_conflict T ≠ None ⟹
    count_decided (get_trail T) = count_decided (get_trail S)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using skip_and_resolve_conflict_before[of T U]
    by (auto simp: skip_and_resolve_same_decision_level)
  done

lemma empty_conflict_lvl0:
  ‹twl_stgy_invs T ⟹ get_conflict T = Some {#} ⟹ count_decided (get_trail T) = 0›
  by (cases T) (auto simp: twl_stgy_invs_def cdclW_restart_mset.conflict_non_zero_unless_level_0_def
      trail.simps conflicting.simps)

abbreviation cdcl_twl_o_prog_spec where
  ‹cdcl_twl_o_prog_spec S ≡ λ(brk, T).
       cdcl_twl_o** S T ∧
       (get_conflict T ≠ None ⟶ count_decided (get_trail T) = 0) ∧
       (¬ brk ⟶ get_conflict T = None ∧ (∀S'. ¬ cdcl_twl_o T S')) ∧
       (brk ⟶ get_conflict T ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy T S')) ∧
       twl_struct_invs T ∧ twl_stgy_invs T ∧ clauses_to_update T = {#} ∧
       (¬ brk ⟶ literals_to_update T ≠ {#}) ∧
       (¬brk ⟶ ¬ (∀S'. ¬ cdcl_twl_o S S') ⟶ cdcl_twl_o++ S T) ∧
       cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›

lemma cdcl_twl_o_prog_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹literals_to_update S = {#}› and
    ns_cp: ‹no_step cdcl_twl_cp S› and
    ent: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_o_prog S ≤ SPEC(cdcl_twl_o_prog_spec S)›
    (is ‹_ ≤ ?S›)
proof -
  have [iff]: ‹¬ cdcl_twl_cp S T› for T
    using ns_cp by fast

  show ?thesis
    unfolding cdcl_twl_o_prog_def
    apply (refine_vcg decide_or_skip_spec[THEN order_trans]; remove_dummy_vars)
    ― ‹initial invariants›
    subgoal using assms unfolding cdcl_twl_o_prog_pre_def by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal by simp
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal for T using assms empty_conflict_lvl0[of T]
      rtranclp_skip_and_resolve_same_decision_level[of S T] by auto
    subgoal using assms by auto
    subgoal using assms by (auto elim!: cdcl_twl_oE simp: image_Un)
    subgoal by (auto elim!: cdcl_twl_stgyE cdcl_twl_oE cdcl_twl_cpE)
    subgoal by (auto simp: rtranclp_unfold elim!: cdcl_twl_oE)
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    subgoal using assms by auto
    done
qed

declare cdcl_twl_o_prog_spec[THEN order_trans, refine_vcg]


section ‹Full Strategy›

abbreviation cdcl_twl_stgy_prog_inv where
  ‹cdcl_twl_stgy_prog_inv S0 ≡ λ(brk, T). twl_struct_invs T ∧ twl_stgy_invs T ∧
        (brk ⟶ final_twl_state T) ∧ cdcl_twl_stgy** S0 T ∧ clauses_to_update T = {#} ∧
        (¬brk ⟶ get_conflict T = None)›

definition cdcl_twl_stgy_prog :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹cdcl_twl_stgy_prog S0 =
  do {
    do {
      (brk, T) ← WHILET⇗cdcl_twl_stgy_prog_inv S0⇖
        (λ(brk, _). ¬brk)
        (λ(brk, S).
        do {
          T ← unit_propagation_outer_loop S;
          cdcl_twl_o_prog T
        })
        (False, S0);
      RETURN T
    }
  }
  ›

lemma wf_cdcl_twl_stgy_measure:
   ‹wf ({((brkT, T), (brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy++ S T}
        ∪ {((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS})›
  (is ‹wf (?TWL ∪ ?BOOL)›)
proof (rule wf_union_compatible)
  show ‹wf ?TWL›
    using tranclp_wf_cdcl_twl_stgy wf_snd_wf_pair by blast
  show ‹?TWL O ?BOOL ⊆ ?TWL›
    by auto

  show ‹wf ?BOOL›
    unfolding wf_iff_no_infinite_down_chain
  proof clarify
    fix f :: ‹nat ⇒ bool × 'b›
    assume H: ‹∀i. (f (Suc i), f i) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
    then have ‹(f (Suc 0), f 0) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}› and
      ‹(f (Suc 1), f 1) ∈ {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
      by presburger+
    then show False
      by auto
  qed
qed

lemma cdcl_twl_o_final_twl_state:
  assumes
    ‹cdcl_twl_stgy_prog_inv S (brk, T)› and
    ‹case (brk, T) of (brk, _) ⇒ ¬ brk› and
    twl_o: ‹cdcl_twl_o_prog_spec U (True, V)›
  shows ‹final_twl_state V›
proof -
  have ‹cdcl_twl_o** U V› and
    confl_lev: ‹get_conflict V ≠ None ⟶ count_decided (get_trail V) = 0› and
    final: ‹get_conflict V ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy V S')›
    ‹twl_struct_invs V›
    ‹twl_stgy_invs V›
    ‹clauses_to_update V = {#}›
    using twl_o
    by force+

  show ?thesis
    unfolding final_twl_state_def
    using confl_lev final
    by auto
qed

lemma cdcl_twl_stgy_in_measure:
  assumes
    twl_stgy: ‹cdcl_twl_stgy_prog_inv S (brk0, T)› and
    brk0: ‹case (brk0, T) of (brk, uu_) ⇒ ¬ brk› and
    twl_o: ‹cdcl_twl_o_prog_spec U V› and
    [simp]: ‹twl_struct_invs U› and
    TU: ‹cdcl_twl_cp** T U› and
    ‹literals_to_update U = {#}›
  shows ‹(V, brk0, T)
         ∈ {((brkT, T), brkS, S). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
            {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}›
proof -
  have [simp]: ‹twl_struct_invs T›
    using twl_stgy by fast+
  obtain brk' V' where
    V: ‹V = (brk', V')›
    by (cases V)
  have
    UV: ‹cdcl_twl_o** U V'› and
    ‹(get_conflict V' ≠ None ⟶ count_decided (get_trail V') = 0)› and
    not_brk': ‹(¬ brk' ⟶ get_conflict V' = None ∧ (∀S'. ¬ cdcl_twl_o V' S'))› and
    brk': ‹(brk' ⟶ get_conflict V' ≠ None ∨ (∀S'. ¬ cdcl_twl_stgy V' S'))› and
    [simp]: ‹twl_struct_invs V'›
    ‹twl_stgy_invs V'›
    ‹clauses_to_update V' = {#}› and
    no_lits_to_upd: ‹(0 < count_decided (get_trail V') ⟶ ¬ brk' ⟶ literals_to_update V' ≠ {#})›
    ‹(¬brk' ⟶ ¬ (∀S'. ¬ cdcl_twl_o U S') ⟶ cdcl_twl_o++ U V')›
    using twl_o unfolding V
    by fast+
    have ‹cdcl_twl_stgy** T V'›
      using TU UV by (auto dest!: rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD)
    then have TV_or_tranclp_TV: ‹T = V' ∨ cdcl_twl_stgy++ T V'›
      unfolding rtranclp_unfold by auto
    have [simp]: ‹¬ cdcl_twl_stgy++ V' V'›
      using wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of V'] by auto
    have [simp]: ‹brk0 = False›
      using brk0 by auto

    have ‹brk'› if ‹T = V'›
    proof -
      have ns_TV: ‹¬cdcl_twl_stgy++ T V'›
        using that[symmetric] wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of T] by auto

      have ns_T_T: ‹¬cdcl_twl_o++ T T›
        using wf_not_refl[OF tranclp_wf_cdcl_twl_o, of T] by auto
      have ‹T = U›
        by (metis (no_types, opaque_lifting) TU UV ns_TV rtranclp_cdcl_twl_cp_stgyD
            rtranclp_cdcl_twl_o_stgyD rtranclp_tranclp_tranclp rtranclp_unfold)
      show ?thesis
        using assms ‹literals_to_update U = {#}› unfolding V that[symmetric] ‹T = U›[symmetric]
        by (auto simp: ns_T_T)
    qed

    then show ?thesis
      using TV_or_tranclp_TV
      unfolding V
      by auto
qed

lemma cdcl_twl_o_prog_cdcl_twl_stgy:
  assumes
    twl_stgy: ‹cdcl_twl_stgy_prog_inv S (brk, S')› and
    ‹case (brk, S') of (brk, uu_) ⇒ ¬ brk› and
    twl_o: ‹cdcl_twl_o_prog_spec T (brk', U)› and
    ‹twl_struct_invs T› and
    cp: ‹cdcl_twl_cp** S' T› and
    ‹literals_to_update T = {#}› and
    ‹∀S'. ¬ cdcl_twl_cp T S'› and
    ‹twl_stgy_invs T›
  shows ‹cdcl_twl_stgy** S U›
proof -
  have ‹cdcl_twl_stgy** S S'›
    using twl_stgy by fast
  moreover {
    have ‹cdcl_twl_o** T U›
      using twl_o by fast
    then have ‹cdcl_twl_stgy** S' U›
      using cp by (auto dest!: rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD)
  }
  ultimately show ?thesis by auto
qed

lemma cdcl_twl_stgy_prog_spec: (* \htmllink{cdcl_twl_stgy_prog_spec} *)
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_prog S ≤ conclusive_TWL_norestart_run S›
  unfolding cdcl_twl_stgy_prog_def full_def conclusive_TWL_norestart_run_def
  apply (refine_vcg WHILEIT_rule[where
     R = ‹{((brkT, T), (brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
          {((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
      remove_dummy_vars)
  ― ‹Well foundedness of the relation›
  subgoal using wf_cdcl_twl_stgy_measure .

  ― ‹initial invariants:›
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp

― ‹loop invariants:›
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdclW_cp)
  subgoal by simp
  subgoal for brk b x
    apply (subgoal_tac ‹pcdcl** (pstateW_of S) (pstateW_of x)›)
    subgoal
      using assms
        rtranclp_pcdcl_entailed_by_init[of ‹pstateW_of S› ‹pstateW_of x›]
      by (auto simp: twl_struct_invs_def)
    subgoal (*TODO Proof*)
      apply (auto simp: twl_struct_invs_def)
      apply (meson assms(1) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_trans)+
      done
    done
  subgoal by simp
  subgoal by simp
  subgoal by (rule cdcl_twl_o_final_twl_state)
  subgoal by (rule cdcl_twl_o_prog_cdcl_twl_stgy)
  subgoal by simp
  subgoal for brk0 T U brl V
    by clarsimp

  ― ‹Final properties›
  subgoal for brk0 T U V  ― ‹termination›
    by (rule cdcl_twl_stgy_in_measure)
  subgoal by simp
  subgoal by fast
  done


definition cdcl_twl_stgy_prog_break :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹cdcl_twl_stgy_prog_break S0 =
  do {
    b ← SPEC(λ_. True);
    (b, brk, T) ← WHILET⇗λ(b, S). cdcl_twl_stgy_prog_inv S0 S⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(_, brk, S). do {
          T ← unit_propagation_outer_loop S;
          T ← cdcl_twl_o_prog T;
          b ← SPEC(λ_. True);
          RETURN (b, T)
        })
        (b, False, S0);
    if brk then RETURN T
    else ―‹finish iteration is required only›
      cdcl_twl_stgy_prog T
  }
  ›

lemma wf_cdcl_twl_stgy_measure_break:
  ‹wf ({((bT, brkT, T), (bS, brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
          {((bT, brkT, T), (bS, brkS, S)). S = T ∧ brkT ∧ ¬brkS}
          )›
    (is ‹?wf ?R›)
proof -
  have 1: ‹wf ({((brkT, T), brkS, S). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
    {((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS})›
    (is ‹wf ?S›)
    by (rule wf_cdcl_twl_stgy_measure)
  have ‹wf {((bT, T), (bS, S)). (T, S) ∈ ?S}›
    apply (rule wf_snd_wf_pair)
    apply (rule wf_subset)
    apply (rule 1)
    apply auto
    done
  then show ?thesis
    apply (rule wf_subset)
    apply auto
    done
qed

lemma cdcl_twl_stgy_prog_break_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› and
    ent: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_prog_break S ≤ conclusive_TWL_norestart_run S›
  unfolding cdcl_twl_stgy_prog_break_def full_def conclusive_TWL_norestart_run_def
  apply (refine_vcg cdcl_twl_stgy_prog_spec[unfolded conclusive_TWL_norestart_run_def]
       WHILEIT_rule[where
     R = ‹{((bT, brkT, T), (bS, brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
          {((bT, brkT, T), (bS, brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
      remove_dummy_vars)
  ― ‹Well foundedness of the relation›
  subgoal using wf_cdcl_twl_stgy_measure_break .

  ― ‹initial invariants:›
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp

  ― ‹loop invariants:›
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdclW_cp)
  subgoal by simp+
  subgoal for brk b x xa
    apply (subgoal_tac ‹pcdcl** (pstateW_of S) (pstateW_of xa)›)
    subgoal
      using assms
        rtranclp_pcdcl_entailed_by_init[of ‹pstateW_of S› ‹pstateW_of xa›]
      by (auto simp: twl_struct_invs_def)
    subgoal (*TODO Proof*)
      apply (auto simp: twl_struct_invs_def)
      apply (meson assms(1) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_trans)+
      done
    done

  subgoal by simp
  subgoal by simp
  subgoal for x a aa ba xa x1a
    by (rule cdcl_twl_o_final_twl_state[of S a aa ba]) simp_all
  subgoal for x a aa ba xa x1a
    by (rule cdcl_twl_o_prog_cdcl_twl_stgy[of S a aa ba xa x1a]) fast+
  subgoal by simp
  subgoal for brk0 T U brl V
    by clarsimp

  ― ‹Final properties›
  subgoal for x a aa ba xa xb  ― ‹termination›
    using cdcl_twl_stgy_in_measure[of S a aa ba xa] by fast
  subgoal by simp
  subgoal by fast

  ― ‹second loop›
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal for brk b x
    apply (subgoal_tac ‹pcdcl** (pstateW_of S) (pstateW_of x)›)
    subgoal
      using assms
        rtranclp_pcdcl_entailed_by_init[of ‹pstateW_of S› ‹pstateW_of x›]
      by (auto simp: twl_struct_invs_def)
    subgoal (*TODO Proof*)
      apply (auto simp: twl_struct_invs_def)
      apply (meson assms(1) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_trans)+
      done
    done
  subgoal using assms by auto
  done

definition cdcl_twl_stgy_prog_early :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹cdcl_twl_stgy_prog_early S0 =
  do {
    b ← SPEC(λ_. True);
    (b, brk, T) ← WHILET⇗λ(b, S). cdcl_twl_stgy_prog_inv S0 S⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(_, brk, S). do {
          T ← unit_propagation_outer_loop S;
          T ← cdcl_twl_o_prog T;
          b ← SPEC(λ_. True);
          RETURN (b, T)
        })
        (b, False, S0);
    RETURN (brk , T)
  }
  ›

lemma cdcl_twl_stgy_prog_early_spec:
  assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
    ‹get_conflict S = None› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    ‹cdcl_twl_stgy_prog_early S ≤ partial_conclusive_TWL_norestart_run S›
  unfolding cdcl_twl_stgy_prog_early_def full_def partial_conclusive_TWL_norestart_run_def
  apply (refine_vcg
       WHILEIT_rule[where
     R = ‹{((bT, brkT, T), (bS, brkS, S)). twl_struct_invs S ∧ cdcl_twl_stgy++ S T} ∪
          {((bT, brkT, T), (bS, brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
      remove_dummy_vars)
  ― ‹Well foundedness of the relation›
  subgoal using wf_cdcl_twl_stgy_measure_break .

  ― ‹initial invariants:›
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp
  subgoal using assms by simp

  ― ‹loop invariants:›
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdclW_cp)
  subgoal by simp
  subgoal for brk b x xa
    apply (subgoal_tac ‹pcdcl** (pstateW_of S) (pstateW_of xa)›)
    subgoal
      using assms
        rtranclp_pcdcl_entailed_by_init[of ‹pstateW_of S› ‹pstateW_of xa›]
      by (auto simp: twl_struct_invs_def)
    subgoal (*TODO Proof*)
      apply (auto simp: twl_struct_invs_def)
      apply (meson assms(1) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_trans)+
      done
    done
  subgoal by simp
  subgoal by simp
  subgoal for x a aa ba xa x1a
    by (rule cdcl_twl_o_final_twl_state[of S a aa ba]) simp_all
  subgoal for x a aa ba xa x1a
    by (rule cdcl_twl_o_prog_cdcl_twl_stgy[of S a aa ba xa x1a]) fast+
  subgoal by simp
  subgoal for brk0 T U brl V
    by clarsimp

  ― ‹Final properties›
  subgoal for x a aa ba xa xb  ― ‹termination›
    using cdcl_twl_stgy_in_measure[of S a aa ba xa] by fast
  subgoal by simp
  subgoal by fast
  done

end