Theory Watched_Literals.Watched_Literals_Watch_List_Simp

theory Watched_Literals_Watch_List_Simp imports Watched_Literals_Watch_List_Reduce Watched_Literals_Watch_List Watched_Literals_Watch_List_Inprocessing begin no_notation funcset (infixr "→" 60) definition cdcl_twl_full_restart_wl_GC_prog where ‹cdcl_twl_full_restart_wl_GC_prog S = do { ASSERT(cdcl_twl_full_restart_wl_GC_prog_pre S); S' ← cdcl_twl_local_restart_wl_spec0 S; T ← remove_one_annot_true_clause_imp_wl S'; ASSERT(mark_to_delete_clauses_GC_wl_pre T); U ← mark_to_delete_clauses_GC_wl T; V ← cdcl_GC_clauses_wl U; ASSERT(cdcl_twl_full_restart_wl_GC_prog_post S V); RETURN V }› lemma correct_watching'_correct_watching'_nobin: ‹correct_watching' S ⟹ correct_watching'_nobin S› by (cases S) (auto simp: correct_watching'.simps correct_watching'_nobin.simps) lemma cdcl_twl_full_restart_wl_GC_prog: ‹(cdcl_twl_full_restart_wl_GC_prog, cdcl_twl_full_restart_l_GC_prog) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ_i_n' S} →_f ⟨{(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S}⟩nres_rel› unfolding cdcl_twl_full_restart_wl_GC_prog_def cdcl_twl_full_restart_l_GC_prog_def apply (intro frefI nres_relI) apply (refine_vcg remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp[THEN fref_to_Down] mark_to_delete_clauses_wl_mark_to_delete_clauses_l2[THEN fref_to_Down] cdcl_GC_clauses_wl_cdcl_GC_clauses[THEN fref_to_Down] cdcl_twl_local_restart_wl_spec0_cdcl_twl_local_restart_l_spec0) subgoal unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def by blast subgoal by (auto dest: correct_watching'_correct_watching'_nobin) subgoal for S T U V W X unfolding mark_to_delete_clauses_GC_wl_pre_def mark_to_delete_clauses_l_GC_pre_def by normalize_goal+ (rule_tac x=X in exI; intro conjI; (rule_tac x=x in exI)?; auto) subgoal unfolding mark_to_delete_clause_GC_wl_pre_alt_def by (auto dest: correct_watching'_clauses_pointed_to2) subgoal for x y S S' T Ta U Ua V Va using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Va V] cdcl_twl_restart_l_inp.intros(1)[of y Va] apply - unfolding cdcl_twl_full_restart_wl_GC_prog_post_def by blast subgoal for x y S S' T Ta U Ua V Va using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Va V] by (auto dest!: cdcl_twl_restart_l_inp.intros(1)) done definition cdcl_twl_full_restart_inprocess_wl_prog where ‹cdcl_twl_full_restart_inprocess_wl_prog S = do { ASSERT(cdcl_twl_full_restart_wl_GC_prog_pre S); S' ← cdcl_twl_local_restart_wl_spec0 S; S' ← remove_one_annot_true_clause_imp_wl S'; T ← mark_duplicated_binary_clauses_as_garbage_wl S'; T ← forward_subsume_wl T; T ← pure_literal_eliminate_wl T; T ← simplify_clauses_with_units_st_wl T; if get_conflict_wl T ≠ None then do { ASSERT(cdcl_twl_full_restart_wl_GC_prog_post_confl S T); RETURN T } else do { ASSERT(mark_to_delete_clauses_GC_wl_pre T); U ← mark_to_delete_clauses_GC_wl T; V ← cdcl_GC_clauses_wl U; ASSERT(cdcl_twl_full_restart_wl_GC_prog_post S V); RETURN V } }› lemma correct_watching'_correct_watching'_leaking_bin: ‹correct_watching'_nobin S ⟹ correct_watching'_leaking_bin S› by (cases S) (auto simp: correct_watching'_nobin.simps correct_watching'_leaking_bin.simps) lemma correct_watching'_leaking_bin_correct_watching'_nobin: ‹correct_watching'_leaking_bin S ⟹ correct_watching'_nobin S› by (cases S) (auto simp: correct_watching'_nobin.simps correct_watching'_leaking_bin.simps) lemma cdcl_twl_full_restart_inprocess_wl_prog: ‹(cdcl_twl_full_restart_inprocess_wl_prog, cdcl_twl_full_restart_inprocess_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ_i_n' S} →_f ⟨{(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ (get_conflict_wl S = None ⟶ correct_watching S ∧ blits_in_ℒ_i_n S)}⟩nres_rel› unfolding cdcl_twl_full_restart_inprocess_wl_prog_def cdcl_twl_full_restart_inprocess_l_def apply (intro frefI nres_relI) apply (refine_vcg remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp[THEN fref_to_Down] cdcl_twl_local_restart_wl_spec0_cdcl_twl_local_restart_l_spec0 mark_to_delete_clauses_wl_mark_to_delete_clauses_l2[THEN fref_to_Down] cdcl_GC_clauses_wl_cdcl_GC_clauses[THEN fref_to_Down] mark_duplicated_binary_clauses_as_garbage_wl pure_literal_eliminate_wl forward_subsume_wl simplify_clauses_with_units_st_wl_simplify_clause_with_units_st2) subgoal unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def by blast subgoal by (auto dest: correct_watching'_correct_watching'_nobin) subgoal by (auto dest: correct_watching'_correct_watching'_leaking_bin) 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 subgoal for x y S' S'a T Ta U Ua V Va W Wa Y Ya using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Ya Y] unfolding cdcl_twl_full_restart_wl_GC_prog_post_confl_def apply - by (rule exI[of _ y], rule exI[of _ Ya]) (smt (verit, best) all_lits_st_alt_def basic_trans_rules(31) in_pair_collect_simp literals_are_ℒ_i_n'_def set_mset_set_mset_eq_iff union_iff) subgoal by auto subgoal for x y S' S'a S'b S'c T S'd Ta S'e W Wa Y Ya unfolding mark_to_delete_clauses_GC_wl_pre_def by (rule_tac x= Ya in exI) simp subgoal for x y S S' T Ta U Ua unfolding cdcl_twl_full_restart_wl_GC_prog_post_def mark_to_delete_clause_GC_wl_pre_alt_def by fast subgoal for x y S S' T Ta U Ua V Va W Wa X Xa Y Ya Z Za using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Za Z] unfolding cdcl_twl_full_restart_wl_GC_prog_post_def by fast subgoal for x y S' S'a T Ta U Ua V Va W Wa X Xa Y Ya Z Za using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Za Z] unfolding cdcl_twl_full_restart_wl_GC_prog_post_def by fast done context twl_restart_ops begin definition restart_prog_wl :: "'v twl_st_wl ⇒ nat ⇒ nat ⇒ nat ⇒ bool ⇒ ('v twl_st_wl × nat × nat × nat) nres" where ‹restart_prog_wl S last_GC last_Restart n brk = do { ASSERT(restart_abs_wl_pre S last_GC last_Restart brk); b ← restart_required_wl S last_GC last_Restart n; if b = RESTART ∧ ¬brk then do { T ← cdcl_twl_restart_wl_prog S; RETURN (T, last_GC, size (get_all_learned_clss_wl T), n) } else if (b = GC ∨ b = INPROCESS) ∧ ¬brk then do { if b ≠ INPROCESS then do { b ← SPEC(λ_. True); T ← (if b then cdcl_twl_full_restart_wl_prog S else cdcl_twl_full_restart_wl_GC_prog S); RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1) } else do { T ← cdcl_twl_full_restart_inprocess_wl_prog S; RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› lemma restart_prog_wl_alt_def: ‹restart_prog_wl S last_GC last_Restart n brk = do { ASSERT(restart_abs_wl_pre S last_GC last_Restart brk); b ← restart_required_wl S last_GC last_Restart n; let _ = (b = RESTART); if b = RESTART ∧ ¬brk then do { T ← cdcl_twl_restart_wl_prog S; RETURN (T, last_GC, size (get_all_learned_clss_wl T), n) } else if (b = GC ∨ b = INPROCESS) ∧ ¬brk then do { let _ = (b = INPROCESS); if b ≠ INPROCESS then do { b ← SPEC(λ_. True); T ← (if b then cdcl_twl_full_restart_wl_prog S else cdcl_twl_full_restart_wl_GC_prog S); RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1) } else do { T ← cdcl_twl_full_restart_inprocess_wl_prog S; RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› unfolding restart_prog_wl_def Let_def by auto lemma restart_abs_wl_pre_blits_in_ℒ_i_n: assumes pre: ‹restart_abs_wl_pre x1c last_GC last_Restart b› and ‹blits_in_ℒ_i_n x1c› shows ‹literals_are_ℒ_i_n' x1c› proof - obtain y x where y_x: ‹(y, x) ∈ twl_st_l None› and x1c_y: ‹(x1c, y) ∈ state_wl_l None› and struct_invs: ‹twl_struct_invs x› and list_invs: ‹twl_list_invs y› using pre unfolding restart_abs_wl_pre_def restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by blast then have eq: ‹set_mset (all_init_lits_of_wl x1c) = set_mset (all_lits_st x1c)› using y_x x1c_y literals_are_ℒ_i_n'_literals_are_ℒ_i_n_iff(4) by blast moreover have eq: ‹set_mset (all_learned_lits_of_wl x1c) ⊆ set_mset (all_lits_st x1c)› using y_x x1c_y unfolding all_lits_st_init_learned by auto ultimately show ‹literals_are_ℒ_i_n' x1c› using eq assms by (cases x1c) (clarsimp simp: blits_in_ℒ_i_n_def blits_in_ℒ_i_n'_def all_lits_def literals_are_ℒ_i_n'_def all_init_lits_def ac_simps) qed lemma cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog: ‹(uncurry4 restart_prog_wl, uncurry4 restart_prog_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} ×_f nat_rel×_f nat_rel×_f nat_rel ×_f bool_rel →_f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ (get_conflict_wl S = None ⟶ correct_watching S ∧ blits_in_ℒ_i_n S)} ×_r nat_rel×_r nat_rel×_r nat_rel⟩nres_rel› (is ‹_ ∈ ?R ×_f _ ×_f _ ×_f _ ×_f _ →_f ⟨?R'⟩nres_rel›) proof - have [simp]: ‹size (learned_clss_l (get_clauses_wl a)) = size ((get_learned_clss_wl a))› for a by (cases a, auto simp: get_learned_clss_wl_def) have [refine0]: ‹restart_required_wl a b c d ≤ ⇓ {(b, b'). (b' = (b = GC ∨ b = INPROCESS)) ∧ (b = RESTART ⟶ size (get_all_learned_clss_wl a) > c)} (GC_required_l a' b' d')› (is ‹_ ≤ ⇓ ?GC _›) if ‹(a, a') ∈ ?R› and ‹(b, b') ∈ nat_rel› ‹(d, d') ∈ nat_rel› ‹restart_abs_wl_pre a b c brk› for a a' b b' c c' d d' e e' brk using that unfolding restart_abs_wl_pre_def GC_required_l_def restart_abs_l_pre_def restart_required_wl_def restart_prog_pre_def apply - apply (refine_rcg) subgoal by auto subgoal by normalize_goal+ simp by (rule RES_refine) auto have [refine0]: ‹RETURN (b = RESTART) ≤ ⇓bool_rel (restart_required_l a' c d)› if ‹(b, b') ∈ ?GC a c'› ‹(a, a') ∈ ?R› ‹(c, c') ∈ nat_rel› for a a' b b' c c' d d' e e' using that unfolding restart_required_l_def by refine_rcg auto have [refine0]: ‹RETURN (b = INPROCESS) ≤ ⇓ bool_rel (inprocessing_required_l x1c)› for b x1c by (auto simp: inprocessing_required_l_def) show ?thesis supply [[goals_limit=1]] unfolding uncurry_def restart_prog_wl_alt_def restart_prog_l_def rewatch_clauses_def apply (intro frefI nres_relI) apply (refine_rcg cdcl_twl_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down] cdcl_twl_full_restart_wl_GC_prog[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_full_twl_restart_l_prog[THEN fref_to_Down] cdcl_twl_full_restart_inprocess_wl_prog[THEN fref_to_Down]) subgoal unfolding restart_abs_wl_pre_def by (fastforce simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto apply assumption+ subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by auto subgoal by (auto) subgoal by auto subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by (auto simp: correct_watching_correct_watching restart_abs_wl_pre_blits_in_ℒ_i_n) subgoal by auto done qed definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_stgy_restart_prog_wl (S₀::'v twl_st_wl) = do { (brk, T, _, _, _) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_wl_inv S₀⇖ (λ(brk, _). ¬brk) (λ(brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, last_GC, last_Restart, n) ← restart_prog_wl T last_GC last_Restart n brk; RETURN (brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Restart, n) }) (False, S₀::'v twl_st_wl, size (get_all_learned_clss_wl S₀), size (get_all_learned_clss_wl S₀), 0); RETURN T }› end definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_early_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_stgy_restart_prog_early_wl (S₀::'v twl_st_wl) = do { ebrk ← RES UNIV; (_, brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_wl_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, last_GC, last_Restart, n) ← restart_prog_wl T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Restart, n) }) (ebrk, False, S₀::'v twl_st_wl, size (get_all_learned_clss_wl S₀), size (get_all_learned_clss_wl S₀), 0); if ¬ brk then do { (brk, T, _, _, _) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_wl_inv T⇖ (λ(brk, _). ¬brk) (λ(brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, last_GC, last_Restart, n) ← restart_prog_wl T last_GC last_Restart n brk; RETURN (brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Restart, n) }) (False, T::'v twl_st_wl, last_GC, last_Restart, n); RETURN T } else RETURN T }› context twl_restart_ops begin definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_bounded_wl :: ‹'v twl_st_wl ⇒ (bool × 'v twl_st_wl) nres› where ‹cdcl_twl_stgy_restart_prog_bounded_wl (S₀::'v twl_st_wl) = do { ebrk ← RES UNIV; (ebrk, brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_wl_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, last_GC, last_Restart, n). do { ASSERT(¬brk); T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, last_GC, last_Restart, n) ← restart_prog_wl T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Restart, n) }) (ebrk, False, S₀::'v twl_st_wl, size (get_all_learned_clss_wl S₀), size (get_all_learned_clss_wl S₀), 0); RETURN (ebrk, T) }› lemma cdcl_twl_stgy_restart_prog_wl_cdcl_twl_stgy_restart_prog_l: ‹(cdcl_twl_stgy_restart_prog_wl, cdcl_twl_stgy_restart_prog_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} →_f ⟨state_wl_l None⟩nres_rel› (is ‹_ ∈ ?R →_f ⟨?S⟩nres_rel›) proof - let ?S = ‹{((brk, S), (brk', T)). (brk,brk') ∈ bool_rel ∧ (S, T) ∈ state_wl_l None ∧ (¬brk ⟶ (correct_watching S ∧ blits_in_ℒ_i_n S))}› let ?T = ‹ {((brk, S, l, m, n), ( brk', T, l', m', n')). ((l, m, n), (l', m', n')) ∈ nat_rel ×_r nat_rel ×_r nat_rel ∧ ((brk, S), (brk', T)) ∈ ?S}› have [refine0]: ‹(x, y) ∈ ?R ⟹ ((False, x, 0), False, y, 0) ∈ bool_rel ×_r ?R ×_r nat_rel› for x y by auto show ?thesis unfolding cdcl_twl_stgy_restart_prog_wl_def cdcl_twl_stgy_restart_prog_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹?T›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry4] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal by auto subgoal for S T U V unfolding cdcl_twl_stgy_restart_abs_wl_inv_def case_prod_beta apply (rule_tac x= ‹T›in exI) apply (rule_tac x= ‹fst (snd V)›in exI) by simp subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto done qed lemma cdcl_twl_stgy_restart_prog_bounded_wl_cdcl_twl_stgy_restart_prog_bounded_l: ‹(cdcl_twl_stgy_restart_prog_bounded_wl, cdcl_twl_stgy_restart_prog_bounded_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} →_f ⟨bool_rel ×_r state_wl_l None⟩nres_rel› (is ‹_ ∈ ?R →_f ⟨_⟩nres_rel›) proof - let ?S = ‹{((brk, S), (brk', T)). (brk,brk') ∈ bool_rel ∧ (S, T) ∈ state_wl_l None ∧ (¬brk ⟶ (correct_watching S ∧ blits_in_ℒ_i_n S))}› let ?T = ‹ {((ebrk, brk, S, l, m, n), (ebrk', brk', T, l', m', n')). ((ebrk, l, m, n), (ebrk', l', m', n')) ∈ bool_rel ×_r nat_rel ×_r nat_rel ×_r nat_rel ∧ ((brk, S), (brk', T)) ∈ ?S}› show ?thesis unfolding cdcl_twl_stgy_restart_prog_bounded_wl_def cdcl_twl_stgy_restart_prog_bounded_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹?T›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry4] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal by auto subgoal for x y ebrk ebrka xa x' unfolding cdcl_twl_stgy_restart_abs_wl_inv_def comp_def case_prod_beta apply (rule_tac x= ‹y›in exI) apply (rule_tac x= ‹fst (snd (snd x'))›in exI) by simp subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed theorem cdcl_twl_stgy_restart_prog_bounded_wl_spec: ‹(cdcl_twl_stgy_restart_prog_bounded_wl, cdcl_twl_stgy_restart_prog_bounded_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} → ⟨bool_rel ×_r state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_bounded_wl_cdcl_twl_stgy_restart_prog_bounded_l[where 'a='v] unfolding fref_param1 apply - by (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?; match_fun_rel?) lemma cdcl_twl_stgy_restart_prog_early_wl_cdcl_twl_stgy_restart_prog_early_l: ‹(cdcl_twl_stgy_restart_prog_early_wl, cdcl_twl_stgy_restart_prog_early_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} →_f ⟨state_wl_l None⟩nres_rel› (is ‹_ ∈ ?R →_f ⟨?S⟩nres_rel›) proof - let ?S = ‹{((brk, S), (brk', T)). (brk,brk') ∈ bool_rel ∧ (S, T) ∈ state_wl_l None ∧ (¬brk ⟶ (correct_watching S ∧ blits_in_ℒ_i_n S))}› let ?T = ‹ {((ebrk, brk, S, l, m, n), (ebrk', brk', T, l', m', n')). ((ebrk, l, m, n), (ebrk', l', m', n')) ∈ bool_rel ×_r nat_rel ×_r nat_rel ×_r nat_rel ∧ ((brk, S), (brk', T)) ∈ ?S}› let ?U = ‹ {((brk, S, l, m, n), (brk', T, l', m', n')). ((l, m, n), (l', m', n')) ∈ nat_rel ×_r nat_rel ×_r nat_rel ∧ ((brk, S), (brk', T)) ∈ ?S}› show ?thesis unfolding cdcl_twl_stgy_restart_prog_early_wl_def cdcl_twl_stgy_restart_prog_early_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹?U›] WHILEIT_refine[where R=‹?T›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry4] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal by auto subgoal for x y ebrk ebrka xa x' unfolding cdcl_twl_stgy_restart_abs_wl_inv_def comp_def case_prod_beta apply (rule_tac x= ‹y›in exI) apply (rule_tac x= ‹fst (snd (snd x'))›in exI) by simp subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i xb x'a unfolding cdcl_twl_stgy_restart_abs_wl_inv_def comp_def case_prod_beta apply (rule_tac x= ‹fst (snd (snd x'))›in exI) apply (rule_tac x= ‹(fst (snd x'a))›in exI) by simp subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed theorem cdcl_twl_stgy_restart_prog_wl_spec: ‹(cdcl_twl_stgy_restart_prog_wl, cdcl_twl_stgy_restart_prog_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} → ⟨state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_wl_cdcl_twl_stgy_restart_prog_l[where 'a='v] unfolding fref_param1 apply - by (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?) theorem cdcl_twl_stgy_restart_prog_early_wl_spec: ‹(cdcl_twl_stgy_restart_prog_early_wl, cdcl_twl_stgy_restart_prog_early_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ_i_n S} → ⟨state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_early_wl_cdcl_twl_stgy_restart_prog_early_l[where 'a='v] unfolding fref_param1 apply - by (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?; match_fun_rel?) end end