Theory IsaSAT_Decide

theory IsaSAT_Decide
  imports IsaSAT_Decide_Defs
begin

lemma (in -)not_is_None_not_None: ‹¬is_None s ⟹ s ≠ None›
  by (auto split: option.splits)


definition bump_find_next_undef where ‹
  bump_find_next_undef 𝒜 x M = (case x of Bump_Heuristics hstable focused foc tobmp ⇒
  if foc then do {
    L ← vmtf_find_next_undef 𝒜 focused M;
    RETURN (L, Bump_Heuristics hstable (update_next_search L focused) foc tobmp)
    } else  do {
    (L, hstable) ← acids_find_next_undef 𝒜 hstable M;
    RETURN (L, Bump_Heuristics hstable focused foc tobmp)
  })›

definition bump_find_next_undef_upd
  :: ‹nat multiset ⇒ (nat,nat)ann_lits ⇒ bump_heuristics ⇒
        (((nat,nat)ann_lits × bump_heuristics) × nat option)nres›
where
  ‹bump_find_next_undef_upd 𝒜 = (λM vm. do{
      (L, vm) ← bump_find_next_undef 𝒜 vm M;
      RETURN ((M, vm), L)
  })›


lemma isa_bump_find_next_undef_bump_find_next_undef:
  ‹(uncurry isa_bump_find_next_undef, uncurry (bump_find_next_undef 𝒜)) ∈
      Id ×r trail_pol 𝒜  →f ⟨⟨nat_rel⟩option_rel ×r Id⟩nres_rel ›
  unfolding isa_bump_find_next_undef_def bump_find_next_undef_def uncurry_def
    defined_atm_def[symmetric]
  apply (intro frefI nres_relI)
  apply (case_tac ‹x›, case_tac ‹fst x›,  case_tac ‹y›, case_tac ‹fst y›, hypsubst, clarsimp simp only: fst_conv tuple4.case)
  apply (refine_rcg isa_vmtf_find_next_undef_vmtf_find_next_undef[THEN fref_to_Down_curry]
    isa_acids_find_next_undef_acids_find_next_undef[THEN fref_to_Down_curry])
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  done

lemma isa_vmtf_find_next_undef_vmtf_find_next_undef:
  ‹(uncurry isa_vmtf_find_next_undef_upd, uncurry (bump_find_next_undef_upd 𝒜)) ∈
       trail_pol 𝒜  ×r  Id →f
          ⟨trail_pol 𝒜 ×f Id ×f  ⟨nat_rel⟩option_rel⟩nres_rel ›
  unfolding isa_vmtf_find_next_undef_upd_def isa_vmtf_find_next_undef_upd_def uncurry_def
    defined_atm_def[symmetric] bump_find_next_undef_upd_def
  apply (intro frefI nres_relI)
  apply (refine_rcg isa_bump_find_next_undef_bump_find_next_undef[THEN fref_to_Down_curry])
  subgoal by auto
  subgoal by (auto simp: update_next_search_def split: prod.splits)
  done
term isa_bump_find_next_undef
term bump_find_next_undef
lemma bump_find_next_undef_ref:
  assumes
    vmtf: ‹x ∈ bump_heur 𝒜 M›
  shows ‹bump_find_next_undef 𝒜 x M
    ≤ ⇓ Id (SPEC (λ(L, bmp).
        (L ≠ None ⟶ bmp ∈ bump_heur 𝒜 (Decided (Pos (the L)) # M)) ∧
        (L = None ⟶ bmp ∈ bump_heur 𝒜 M) ∧
        (L = None ⟶ (∀L∈#ℒall 𝒜. defined_lit M L)) ∧
    (L ≠ None ⟶ Pos (the L) ∈# ℒall 𝒜 ∧ undefined_lit M (Pos (the L)))))›
  using assms
  unfolding bump_find_next_undef_def
  apply (cases ‹get_focused_heuristics x›; cases ‹get_stable_heuristics x›)
  apply (cases x, simp only: tuple4.case)
  by (refine_vcg lhs_step_If)
   (auto intro!: vmtf_find_next_undef_ref[THEN order_trans]
      acids_find_next_undef[THEN order_trans] dest: vmtf_consD
    simp: bump_heur_def update_next_search_def)

definition find_undefined_atm
  :: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ bump_heuristics ⇒
       (((nat,nat) ann_lits × bump_heuristics) × nat option) nres›
where
  ‹find_undefined_atm 𝒜 M _ = SPEC(λ((M', vm), L).
     (L ≠ None ⟶ Pos (the L) ∈# ℒall 𝒜 ∧ undefined_atm M (the L)) ∧
  (L = None ⟶ (∀K∈# ℒall 𝒜. defined_lit M K)) ∧ M = M' ∧
  (L = None ⟶ vm ∈ bump_heur 𝒜 M)∧
  (L ≠ None ⟶ vm ∈ bump_heur 𝒜 (Decided (Pos (the L)) # M)))›

definition lit_of_found_atm_D_pre where
‹lit_of_found_atm_D_pre 𝒜 = (λ((φ, _), L). L ≠ None ⟶
       (the L ≤ unat32_max div 2 ∧ the L ∈# 𝒜 ∧ phase_save_heur_rel 𝒜 φ ))›

lemma lit_of_found_atm_D_pre:
  ‹heuristic_rel 𝒜 heur ⟹ isasat_input_bounded 𝒜 ⟹ (L ≠ None ⟹ the L ∈# 𝒜) ⟹
    get_saved_phase_option_heur_pre (L) (get_content heur)›
  by (auto simp: lit_of_found_atm_D_pre_def phase_saving_def heuristic_rel_def phase_save_heur_rel_def
    get_saved_phase_option_heur_pre_def get_next_phase_pre_def heuristic_rel_stats_def get_next_phase_heur_pre_stats_def
    atms_of_ℒall_𝒜in in_ℒall_atm_of_in_atms_of_iff dest: bspec[of _ _ ‹Pos (the L)›])

definition find_unassigned_lit_wl_D_heur_pre where
  ‹find_unassigned_lit_wl_D_heur_pre S ⟷
    (
      ∃T U.
        (S, T) ∈ state_wl_l None ∧
        (T, U) ∈ twl_st_l None ∧
        twl_struct_invs U ∧
        literals_are_ℒin (all_atms_st S) S ∧
        get_conflict_wl S = None
    )›

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


abbreviation twl_st_heur_decide_find'''
   :: ‹nat literal ⇒ nat ⇒ (isasat × nat twl_st_wl) set›
where
‹twl_st_heur_decide_find''' L r ≡ {(S, T). (S, T) ∈ twl_st_heur_decide_find L ∧
           length (get_clauses_wl_heur S) = r}›

lemma vmtf_find_next_undef_upd:
  ‹(uncurry (bump_find_next_undef_upd 𝒜), uncurry (find_undefined_atm 𝒜)) ∈
     [λ(M, vm). vm ∈ bump_heur 𝒜 M]f Id ×f Id → ⟨Id ×f Id ×f ⟨nat_rel⟩option_rel⟩nres_rel›
  unfolding bump_find_next_undef_upd_def find_undefined_atm_def
    update_next_search_def uncurry_def
  apply (intro frefI nres_relI)
  apply (clarify)
  apply (rule bind_refine_spec)
   prefer 2
   apply (rule bump_find_next_undef_ref[simplified])
  by (auto intro!: RETURN_SPEC_refine simp: image_image defined_atm_def[symmetric])

lemma find_unassigned_lit_wl_D'_find_unassigned_lit_wl_D:
  ‹(find_unassigned_lit_wl_D_heur, find_unassigned_lit_wl) ∈
     [find_unassigned_lit_wl_D_heur_pre]f
    {(S, T). (S, T) ∈ twl_st_heur''' r ∧ learned_clss_count S = u} →
  ⟨{((T, L), (T', L')). (L ≠ None ⟶ (T, T') ∈ twl_st_heur_decide_find''' (the L) r)  ∧
         (L = None ⟶ (T, T') ∈ twl_st_heur''' r)  ∧  L = L' ∧ learned_clss_count T = u ∧
         (L ≠ None ⟶ undefined_lit (get_trail_wl T') (the L) ∧ the L ∈# all_lits_st T') ∧
         get_conflict_wl T' = None}⟩nres_rel›
proof -
  have [simp]: ‹undefined_lit M (Pos (atm_of y)) = undefined_lit M y› for M y
    by (auto simp: defined_lit_map)
  have [simp]: ‹defined_atm M (atm_of y) = defined_lit M y› for M y
    by (auto simp: defined_lit_map defined_atm_def)

  have ID_R: ‹Id ×r ⟨Id⟩option_rel = Id›
    by auto

  define unassigned_atm where
     ‹unassigned_atm S L ⟷ (∃ M N D NE UE NS US WS Q.
         S = (M, N, D, NE, UE, NS, US, WS, Q) ∧
         (L ≠ None ⟶
            undefined_lit M (the L) ∧ the L ∈# ℒall (all_atms_st S) ∧
            atm_of (the L) ∈# all_atms_st S) ∧
         (L = None ⟶ (∄L'. undefined_lit M L' ∧
             atm_of L' ∈# all_atms_st S)))›
    for L :: ‹nat literal option› and S :: ‹nat twl_st_wl›

  have all_lits_st_atm: ‹L ∈# all_lits_st S ⟷ atm_of L ∈# all_atms_st S› for L S
    unfolding all_lits_st_def all_atms_st_def in_all_lits_of_mm_ain_atms_of_iff
      all_lits_def all_atms_def by (metis atm_of_all_lits_of_mm(1))

  have find_unassigned_lit_wl_D_alt_def:
   ‹find_unassigned_lit_wl S = do {
     L ← SPEC(unassigned_atm S);
     L ← RES {L, map_option uminus L};
     SPEC(λ((M, N, D, NE, UE, N0, U0, WS, Q), L').
         S = (M, N, D, NE, UE, N0, U0, WS, Q) ∧ L = L')
   }› for S
   unfolding find_unassigned_lit_wl_def RES_RES_RETURN_RES unassigned_atm_def
    RES_RES_RETURN_RES all_lits_def in_all_lits_of_mm_ain_atms_of_iff
    in_ℒall_atm_of_𝒜in in_set_all_atms_iff all_lits_st_atm
  by (cases S) auto

  have isa_vmtf_find_next_undef_upd:
    ‹isa_vmtf_find_next_undef_upd (get_trail_wl_heur S)
       (get_vmtf_heur S)
      ≤ ⇓ {(((M, vm), A), L). A = map_option atm_of L ∧
              unassigned_atm (bt, bu, bv, bw, bx, by, bz, baa, bab) L ∧
             (L ≠ None ⟶ vm ∈ bump_heur (all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)) (Decided (Pos (the A)) # bt)) ∧
             (L = None ⟶ vm ∈ bump_heur (all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)) bt) ∧
             (L ≠ None ⟶ the A ∈# all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)) ∧
             (M, bt) ∈ trail_pol (all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab))}
         (SPEC (unassigned_atm (bt, bu, bv, bw, bx, by, bz, baa, bab)))›
	  (is ‹_ ≤ ⇓ ?find _›)
    if
      pre: ‹find_unassigned_lit_wl_D_heur_pre (bt, bu, bv, bw, bx, by, bz, baa, bab)› and
      T: ‹(S,
	bt, bu, bv, bw, bx, by, bz, baa, bab)
       ∈ twl_st_heur› and
      ‹r =
       length
	(get_clauses_wl_heur
	  S)›
     for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao ap aq bd ar as at
	 au av aw be ax ay az bf bg bh bi bj bk bl bm bn bo bp bq br bs bt bu bv
	 bw bx "by" bz heur baa bab stats S
  proof -
    let ?𝒜 = ‹all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)›
    have pol:
      ‹(get_trail_wl_heur S, bt) ∈ trail_pol ?𝒜›
      using that by (cases bz; auto simp: twl_st_heur_def)
    have [intro]:
       ‹Multiset.Ball (ℒall ?𝒜) (defined_lit bt) ⟹
	 atm_of L' ∈# ?𝒜 ⟹
		undefined_lit bt L'⟹ False› for L'
      by (auto simp: atms_of_ms_def
	   all_lits_of_mm_union ran_m_def all_lits_of_mm_add_mset ℒall_union
	   eq_commute[of _ ‹the (fmlookup _ _)›] ℒall_atm_of_all_lits_of_m
	  atms_of_def ℒall_add_mset
	 dest!: multi_member_split
	  )

    show ?thesis
      apply (rule order.trans)
      apply (rule isa_vmtf_find_next_undef_vmtf_find_next_undef[of ?𝒜, THEN fref_to_Down_curry,
	 of _ _ bt ‹get_vmtf_heur S›])
      subgoal by fast
      subgoal
	 using pol by (cases ‹get_vmtf_heur S›) (auto simp: twl_st_heur_def all_atms_def[symmetric])
      apply (rule order.trans)
      apply (rule ref_two_step')
      apply (rule vmtf_find_next_undef_upd[THEN fref_to_Down_curry, of ?𝒜 bt ‹get_vmtf_heur S›])
      subgoal using T by (auto simp: all_atms_def twl_st_heur_def)
      subgoal by auto
      subgoal using pre
        apply (cases bab)
	apply (auto 5 0 simp: find_undefined_atm_def unassigned_atm_def conc_fun_RES all_atms_def[symmetric]
	   mset_take_mset_drop_mset'
	   intro!: RES_refine intro: )
	apply (auto intro:  simp: defined_atm_def)
	apply (rule_tac x = ‹Some (Pos ya)› in exI)
	apply (auto intro: simp: defined_atm_def  in_ℒall_atm_of_𝒜in
	  in_set_all_atms_iff)
	apply (rule_tac x = ‹Some (Pos y)› in exI)
	apply (auto intro: simp: defined_atm_def  in_ℒall_atm_of_𝒜in
	  in_set_all_atms_iff)
	done
    done
  qed

  have lit_of_found_atm: ‹lit_of_found_atm ao' x2a
	≤ ⇓ {(L, L'). L = L' ∧ map_option atm_of  L = x2a}
	   (RES {L, map_option uminus L})›
    if
      ‹find_unassigned_lit_wl_D_heur_pre (bt, bu, bv, bw, bx, by, bz, baa, bab)› and
      ‹(S, bt, bu, bv, bw, bx, by, bz, baa, bab) ∈ twl_st_heur› and
      ‹r = length (get_clauses_wl_heur S)› and
      ‹(x, L) ∈ ?find bt bu bv bw bx by bz baa bab› and
      ‹x1 = (x1a, x2)› and
      ‹x = (x1, x2a)›
     for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao ap aq bd ar as at
       au av aw be ax ay az bf bg bh bi bj bk bl bm bn bo bp bq br bs bt bu bv
       bw bx "by" bz x L x1 x1a x2 x2a heur baa bab ao' stats S
  proof -
    show ?thesis
      using that unfolding lit_of_found_atm_def
      by (auto simp: atm_of_eq_atm_of twl_st_heur_def intro!: RES_refine)
  qed
  have [simp]: ‹vmtf 𝒜 (Decided (Pos (atm_of ap)) # aa) = vmtf 𝒜 (Decided ap # aa)›
    ‹vmtf 𝒜 (Decided (-ap) # aa) = vmtf 𝒜 (Decided ap # aa)› for 𝒜 ap aa
    unfolding vmtf_def vmtf_ℒall_def
    by auto
  have [simp]: ‹acids 𝒜 (Decided (Pos (atm_of ap)) # aa) = acids 𝒜 (Decided ap # aa)›
    ‹acids 𝒜 (Decided (-ap) # aa) = acids 𝒜 (Decided ap # aa)› for 𝒜 ap aa
    unfolding acids_def defined_lit_map
    by auto
  have [simp]: ‹bump_heur 𝒜 (Decided (Pos (atm_of ap)) # aa)= bump_heur 𝒜 (Decided ap # aa)›
    ‹bump_heur 𝒜 (Decided (-ap) # aa) = bump_heur 𝒜 (Decided ap # aa)› for 𝒜 ap aa bc
    unfolding bump_heur_def
    by auto
  have [dest]: ‹find_unassigned_lit_wl_D_heur_pre (ca, cb, cc, cd, ce, cf, cg, ch, ci, cx, cy) ⟹ cc = None›
    for ca cb cc cd ce cf cg ch ci cy cx
    unfolding find_unassigned_lit_wl_D_heur_pre_def by auto
  show ?thesis
    unfolding find_unassigned_lit_wl_D_heur_def find_unassigned_lit_wl_D_alt_def find_undefined_atm_def
      ID_R Let_def
    apply (intro frefI nres_relI)
    apply clarify
    apply refine_vcg
    apply (rule isa_vmtf_find_next_undef_upd; assumption)
    subgoal
      by (rule lit_of_found_atm_D_pre)
       (auto simp add: twl_st_heur_def in_ℒall_atm_of_in_atms_of_iff Ball_def image_image
        mset_take_mset_drop_mset' all_atms_def[symmetric] unassigned_atm_def
          simp del: twl_st_of_wl.simps dest!: intro!: RETURN_RES_refine)
    apply (rule lit_of_found_atm; assumption)
    subgoal for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao L L'
      by (cases am)
      (clarsimp_all simp: twl_st_heur_def twl_st_heur_decide_find_def unassigned_atm_def atm_of_eq_atm_of uminus_𝒜in_iff learned_clss_count_def
         all_lits_st_alt_def[symmetric]
        simp del: twl_st_of_wl.simps dest!: intro!: RETURN_RES_refine;
        auto simp: atm_of_eq_atm_of uminus_𝒜in_iff all_atms_st_def; fail)+
    done
qed


lemma nofail_get_next_phase:
  ‹get_next_phase_heur_pre_stats True L  (get_restart_heuristics φ) ⟹
                nofail (get_next_phase_heur b L φ)›
  by (cases φ) (auto simp: phase_save_heur_rel_def phase_saving_def get_next_phase_heur_def get_next_phase_heur_stats_def
    get_next_phase_heur_pre_stats_def get_next_phase_stats_def
    nofail_def bind_ASSERT_eq_if ℒall_add_mset atms_of_def get_next_phase_pre_def split: if_splits
    dest!: multi_member_split)


lemma all_atms_st_cons_trail_Decided[simp]:
  ‹all_atms_st (cons_trail_Decided x'a x1b, oth) = all_atms_st (x1b, oth)› and
  all_atms_st_cons_trail_empty_Q:
  ‹NO_MATCH {#} Q ⟹
     all_atms_st (x1b, N, D, NS, US, NEk, UEk, NE, UE, N0, U0, Q, W) = all_atms_st (x1b, N, D, NS, US, NEk, UEk, NE, UE, N0, U0, {#}, W)›
  by (cases oth) (auto simp: cons_trail_Decided_def all_atms_st_def)

lemma decide_wl_or_skip_D_heur_decide_wl_or_skip_D:
  ‹(decide_wl_or_skip_D_heur, decide_wl_or_skip) ∈
    {(S, T). (S, T) ∈ twl_st_heur''' r ∧ learned_clss_count S =u} →f
    ⟨bool_rel ×f {(S, T). (S, T) ∈ twl_st_heur''' r ∧ learned_clss_count S =u}⟩ nres_rel›
  (is ‹_ ∈ ?A →f _›)
proof -
  have [simp]:
    ‹rev (cons_trail_Decided L M) = rev M @ [Decided L]›
    ‹no_dup (cons_trail_Decided L M) = no_dup (Decided L # M)›
    ‹bump_heur 𝒜 (cons_trail_Decided L M) = bump_heur 𝒜 (Decided L # M)›
    for M L 𝒜
    by (auto simp: cons_trail_Decided_def)

  have final: ‹decide_lit_wl_heur xb x1a
	≤ SPEC
	   (λT.  do {
                  RETURN (False, T)}
		≤ SPEC
		   (λc. (c, False, decide_lit_wl x'a x1)
			∈ bool_rel ×f ?A))›
    if
      ‹(x, y) ∈ {(S, T). (S, T) ∈ twl_st_heur''' r ∧ learned_clss_count S = u}› and
      ‹(xa, x')
       ∈ {((T, L), T', L').
    (L ≠ None ⟶ (T, T') ∈ twl_st_heur_decide_find''' (the L) r) ∧
    (L = None ⟶ (T, T') ∈ twl_st_heur''' r) ∧
    L = L' ∧
    learned_clss_count T = u ∧
    (L ≠ None ⟶
     undefined_lit (get_trail_wl T') (the L) ∧ the L ∈# all_lits_st T') ∧
    get_conflict_wl T' = None}› and
      st:
        ‹x' = (x1, x2)›
        ‹xa = (x1a, x2a)›
        ‹x2a = Some xb›
        ‹x2 = Some x'a› and
      ‹(xb, x'a) ∈ nat_lit_lit_rel›
    for x y xa x' x1 x2 x1a x2a xb x'a
  proof -
    show ?thesis
      unfolding decide_lit_wl_heur_def
        decide_lit_wl_def
      apply refine_vcg
      subgoal
        by (rule isa_length_trail_pre[of _ ‹get_trail_wl x1› ‹all_atms_st x1›])
	  (use that(2) in ‹auto simp: twl_st_heur_decide_find_def twl_st_heur_def st all_atms_def[symmetric]›)
      subgoal
        by (rule cons_trail_Decided_tr_pre[of _ ‹get_trail_wl x1› ‹all_atms_st x1›])
	  (use that(2) in ‹auto simp: twl_st_heur_decide_find_def st all_atms_def[symmetric]
          all_lits_st_alt_def[symmetric]›)
      subgoal
        using that(2) unfolding cons_trail_Decided_def[symmetric] st
        apply (clarsimp simp: twl_st_heur_def)[]
        apply (clarsimp simp add: twl_st_heur_def twl_st_heur_decide_find_def all_atms_def[symmetric]
	   isa_length_trail_length_u[THEN fref_to_Down_unRET_Id] out_learned_def
          all_lits_st_alt_def[symmetric] all_atms_st_cons_trail_empty_Q
	  intro!: cons_trail_Decided_tr[THEN fref_to_Down_unRET_uncurry]
	    isa_vmtf_consD)
        by (auto simp add: twl_st_heur_def all_atms_def[symmetric] learned_clss_count_def
	   isa_length_trail_length_u[THEN fref_to_Down_unRET_Id] out_learned_def
          all_lits_st_alt_def[symmetric] all_atms_st_cons_trail_empty_Q
	  intro!: cons_trail_Decided_tr[THEN fref_to_Down_unRET_uncurry]
	    isa_vmtf_consD)
      done
  qed

  have decide_wl_or_skip_alt_def: ‹decide_wl_or_skip S = (do {
    ASSERT(decide_wl_or_skip_pre S);
    (S, L) ← find_unassigned_lit_wl S;
    case L of
      None ⇒ RETURN (True, S)
    | Some L ⇒ RETURN (False, decide_lit_wl L S)
  })› for S
  unfolding decide_wl_or_skip_def by auto
  show ?thesis
    supply [[goals_limit=1]]
    unfolding decide_wl_or_skip_D_heur_def decide_wl_or_skip_alt_def decide_wl_or_skip_pre_def
     decide_l_or_skip_pre_def twl_st_of_wl.simps[symmetric]
    apply (intro nres_relI frefI same_in_Id_option_rel)
    apply (refine_vcg find_unassigned_lit_wl_D'_find_unassigned_lit_wl_D[of r u, THEN fref_to_Down])
    subgoal for x y
      unfolding decide_wl_or_skip_pre_def find_unassigned_lit_wl_D_heur_pre_def
	decide_wl_or_skip_pre_def decide_l_or_skip_pre_def decide_or_skip_pre_def
       apply normalize_goal+
       apply (rule_tac x = xa in exI)
       apply (rule_tac x = xb in exI)
       apply auto
       done
    apply (rule same_in_Id_option_rel)
    subgoal by (auto simp del: simp: twl_st_heur_def)
    subgoal by auto
    by (rule final; assumption?)
 qed


lemma bind_triple_unfold:
  ‹do {
    ((M, vm), L) ← (P :: _ nres);
    f ((M, vm), L)
} =
do {
    x ← P;
    f x
}›
  by (intro bind_cong) auto

lemma decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur2:
  ‹(decide_wl_or_skip_D_heur', decide_wl_or_skip_D_heur) ∈ Id →f ⟨Id⟩nres_rel›
  by (intro frefI nres_relI) (use decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur in auto)

end