Theory IsaSAT_Simplify_Pure

theory IsaSAT_Simplify_Pure_Literals imports IsaSAT_Simplify_Pure_Literals_Defs Watched_Literals.Watched_Literals_Watch_List_Inprocessing More_Refinement_Libs.WB_More_Refinement_Loops IsaSAT_Restart begin lemma isa_pure_literal_count_occs_clause_wl_pure_literal_count_occs_clause_wl: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› ‹(occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st S'))› ‹(C,C')∈nat_rel› shows ‹isa_pure_literal_count_occs_clause_wl C S occs remaining ≤⇓{((occs, remaining), occs'). (occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st S'))} (pure_literal_count_occs_clause_wl C' S' occs')› proof - have pure_literal_count_occs_clause_wl_alt_def: ‹pure_literal_count_occs_clause_wl C S occs = do { ASSERT (pure_literal_count_occs_clause_wl_pre C S occs); let m = length (get_clauses_wl S ∝ C); (i, occs) ← WHILE_T⇗pure_literal_count_occs_clause_wl_invs C S occs⇖ (λ(i, occs). i < m) (λ(i, occs). do { let L = get_clauses_wl S ∝ C ! i; let occs = occs (L := True); RETURN (i+1, occs) }) (0, occs); RETURN occs }› for C S occs by (auto simp: pure_literal_count_occs_clause_wl_def) have [refine0]: ‹ ((0, occs, remaining), 0, occs') ∈ {((n, occs, remaining), n', occs'). (n,n')∈ nat_rel ∧ (occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st S'))}› using assms by auto show ?thesis supply RETURN_as_SPEC_refine[refine2 del] unfolding isa_pure_literal_count_occs_clause_wl_def pure_literal_count_occs_clause_wl_alt_def mop_arena_length_st_def mop_access_lit_in_clauses_heur_def apply (refine_vcg mop_arena_length[THEN fref_to_Down_curry, unfolded comp_def, of ‹get_clauses_wl S'› C' ‹get_clauses_wl_heur S› C ‹set (get_vdom S)›] mop_arena_lit(2)[THEN RETURN_as_SPEC_refine, of _ _ ‹set (get_vdom S)›]) subgoal using assms unfolding isa_pure_literal_count_occs_clause_wl_pre_def by fast subgoal unfolding pure_literal_count_occs_clause_wl_pre_def pure_literal_count_occs_l_clause_pre_def by normalize_goal+ auto subgoal using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def) subgoal using assms unfolding isa_pure_literal_count_occs_clause_wl_invs_def by fast subgoal by auto subgoal by auto subgoal using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def) subgoal unfolding pure_literal_count_occs_clause_wl_pre_def pure_literal_count_occs_l_clause_pre_def by normalize_goal+ auto subgoal using assms by auto subgoal by auto subgoal by auto subgoal unfolding pure_literal_count_occs_clause_wl_pre_def pure_literal_count_occs_l_clause_pre_def by normalize_goal+ (auto simp add: map_fun_rel_def ran_m_def all_init_atms_alt_def ℒ_a_l_l_all_init_atms(2) all_init_lits_of_wl_def all_lits_of_mm_add_mset dest!: multi_member_split dest: nth_mem_mset[THEN in_clause_in_all_lits_of_m]) subgoal unfolding pure_literal_count_occs_clause_wl_pre_def pure_literal_count_occs_l_clause_pre_def apply normalize_goal+ apply (auto 4 3 simp add: map_fun_rel_def ran_m_def all_init_atms_alt_def ℒ_a_l_l_all_init_atms(2) all_init_lits_of_wl_def all_lits_of_mm_add_mset dest!: multi_member_split dest: nth_mem_mset[THEN in_clause_in_all_lits_of_m] in_all_lits_of_mm_uminusD) by (metis Un_iff all_lits_of_mm_add_mset in_all_lits_of_mm_uminusD in_clause_in_all_lits_of_m nth_mem_mset set_mset_union) subgoal by (auto simp add: map_fun_rel_def) subgoal by auto done qed (*TODO Move*) lemma distinct_mset_add_subset_iff: ‹distinct_mset (A+B) ⟹ A + B ⊆# C ⟷ A ⊆# C ∧ B ⊆# C› by (induction A) (auto simp add: insert_subset_eq_iff subset_remove1_mset_notin) lemma isa_pure_literal_count_occs_wl_pure_literal_count_occs_wl: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› shows ‹isa_pure_literal_count_occs_wl S ≤ ⇓ (bool_rel ×_f ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st S'))) (pure_literal_count_occs_wl S')› proof - have pure_literal_count_occs_wl_alt_def: ‹pure_literal_count_occs_wl S = do { ASSERT (pure_literal_count_occs_wl_pre S); xs ← SPEC (λxs. distinct_mset xs ∧ (∀C∈#dom_m (get_clauses_wl S). irred (get_clauses_wl S) C ⟶ C ∈# xs)); abort ← RES (UNIV :: bool set); let occs = (λ_. False); (_, occs, abort) ← WHILE_T(λ(A, occs, abort). A ≠ {#} ∧ ¬abort) (λ(A, occs, abort). do { ASSERT (A ≠ {#}); C ← SPEC (λC. C ∈# A); b ← RETURN (C ∈# dom_m (get_clauses_wl S)); if (b ∧ irred (get_clauses_wl S) C) then do { occs ← pure_literal_count_occs_clause_wl C S occs; abort ← RES (UNIV :: bool set); RETURN (remove1_mset C A, occs, abort) } else RETURN (remove1_mset C A, occs, abort) }) (xs, occs, abort); RETURN (abort, occs) }› for S by (auto simp: pure_literal_count_occs_wl_def) have dist: ‹distinct_mset A ⟹ distinct_mset B ⟹ set_mset A ∩ set_mset B = {} ⟹ distinct_mset (A + B)› for A B by (metis distinct_mset_add set_mset_eq_empty_iff set_mset_inter) have [refine0]: ‹pure_literal_count_occs_wl_pre S' ⟹ RETURN (get_avdom S @ get_ivdom S) ≤ ⇓ (list_mset_rel) (SPEC (λxs. distinct_mset xs ∧ (∀C∈#dom_m (get_clauses_wl S'). irred (get_clauses_wl S') C ⟶ C ∈# xs)))› apply (rule RETURN_SPEC_refine) apply (rule exI[of _ ‹mset (get_avdom S @ get_ivdom S)›]) using assms unfolding twl_st_heur_restart_def twl_st_heur_restart_ana_def in_pair_collect_simp apply - apply normalize_goal+ by (auto simp: list_mset_rel_def br_def aivdom_inv_dec_alt_def dest: distinct_mset_mono intro!: dist) have conj_eqI: ‹a=a' ⟹ b=b' ⟹ (a&b) = (a'&b')› for a a' b b' by auto have [refine0]: ‹(get_avdom S @ get_ivdom S, xs) ∈ list_mset_rel ⟹ (c ≤ 0, abort) ∈ bool_rel ⟹ ((0, replicate (length (get_watched_wl_heur S)) False, c), xs, λ_. False, abort) ∈ {(i,xs). xs = mset (drop i (get_avdom S @ get_ivdom S))} ×_r ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st S')) ×_r {(a,b). b = (a ≤ 0)}› for xs abort c using assms unfolding twl_st_heur_restart_def twl_st_heur_restart_ana_def in_pair_collect_simp apply - apply normalize_goal+ by (auto simp: list_mset_rel_def br_def map_fun_rel_def all_init_atms_alt_def) have [refine0]: ‹RETURN (0 ≥ a) ≤ ⇓ bool_rel (RES UNIV)› for a by auto have K: ‹(a',b)∈ nat_rel ⟹ (a, a'∈# dom_m (get_clauses_wl S')) ∈ A⟹ (a,b∈# dom_m (get_clauses_wl S'))∈A› for a b f A a' by auto have aivdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl S'))› and valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def aivdom_inv_dec_alt_def dest!: ) have dist_vdom: ‹distinct (get_vdom S)› and valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def aivdom_inv_dec_alt_def) have vdom_incl: ‹set (get_vdom S) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur S)}› using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto have dist: ‹distinct_mset A ⟹ distinct_mset B ⟹ set_mset A ∩ set_mset B = {} ⟹ distinct_mset (A + B)› for A B by (metis distinct_mset_add set_mset_eq_empty_iff set_mset_inter) then have dist2: ‹distinct_mset (mset (get_avdom S @ get_ivdom S))› using aivdom unfolding aivdom_inv_dec_alt_def by (auto intro!: dist dest: distinct_mset_mono) have ‹mset (get_avdom S @ get_ivdom S) ⊆# mset (get_vdom S)› using dist2 aivdom unfolding aivdom_inv_dec_alt_def by (auto simp: distinct_mset_add_subset_iff dist2) then have ‹length (get_avdom S @ get_ivdom S) ≤ length (get_vdom S)› using size_mset_mono by fastforce also have le_vdom_arena: ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S) - 2› by (subst distinct_card[OF dist_vdom, symmetric]) (use card_mono[OF _ vdom_incl] in auto) finally have le: ‹length (get_avdom S @ get_ivdom S) ≤ length (get_clauses_wl_heur S) - 2› . show ?thesis unfolding isa_pure_literal_count_occs_wl_def pure_literal_count_occs_wl_alt_def apply (rewrite at ‹let _ = length _ in _› Let_def) apply (rewrite at ‹let _ = _ - _ in _› Let_def) apply (refine_vcg mop_arena_status2[where vdom=‹set(get_vdom S)› and N=‹get_clauses_wl S'›] isa_pure_literal_count_occs_clause_wl_pure_literal_count_occs_clause_wl) subgoal by (rule le) subgoal by (auto simp: word_greater_zero_iff) subgoal by (auto simp: access_avdom_at_pre_def) subgoal by (auto simp: access_avdom_at_pre_def) subgoal by (auto simp: access_ivdom_at_pre_def length_avdom_def) subgoal by (auto 6 4 intro: in_set_dropI simp: nth_append) apply (assumption) subgoal using aivdom apply (simp add: aivdom_inv_dec_alt_def) by (metis (no_types, lifting) Un_iff length_append mset_subset_eqD nth_mem_mset set_mset_mset set_union_code) subgoal by (rule valid) apply (rule K;assumption) subgoal by auto apply (rule assms) subgoal by simp subgoal by (auto simp: drop_Suc_nth simp del: drop_append) subgoal by (auto simp: drop_Suc_nth simp del: drop_append) subgoal by auto done qed (*TODO dedup*) lemma lookup_clause_rel_cong: ‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ lookup_clause_rel 𝒜 ⟹ L ∈ lookup_clause_rel ℬ› using ℒ_a_l_l_cong[of 𝒜 ℬ] atms_of_ℒ_a_l_l_cong[of 𝒜 ℬ] unfolding lookup_clause_rel_def by (cases L) (auto) lemma isa_propagate_pure_bt_wl_propagate_pure_bt_wl: assumes S₀T: ‹(S₀, T) ∈ twl_st_heur_restart_ana' r u› and ‹(L,L')∈Id› shows ‹isa_propagate_pure_bt_wl L S₀ ≤⇓{(U, V). (U,V)∈twl_st_heur_restart_ana' r u ∧ get_vmtf_heur U = get_vmtf_heur S₀} (propagate_pure_bt_wl L' T)› proof - have propagate_pure_bt_wl_alt_def: ‹propagate_pure_bt_wl = (λL (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS). do { ASSERT(propagate_pure_wl_pre L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS)); M ← cons_trail_propagate_l L 0 M; RETURN (M, N, D, NE, UE, add_mset {#L#} NEk, UEk, NS, US, N0, U0, add_mset (-L) Q, WS)})› unfolding propagate_pure_bt_wl_def by auto have [refine]: ‹S=S₀ ⟹ M = get_trail_wl T ⟹ mop_isa_length_trail (get_trail_wl_heur S) ≤ SPEC (λca. (ca, length M) ∈ Id)› for S M apply (subst twl_st_heur_restart_isa_length_trail_get_trail_wl[of _ T r]) using S₀T apply simp using S₀T apply (simp_all add: twl_st_heur_restart_ana_def twl_st_heur_restart_def all_init_atms_st_alt_def all_init_atms_alt_def) done have trail: ‹(get_trail_wl_heur S₀, get_trail_wl T) ∈ trail_pol (all_init_atms_st T)› for x2a x2 using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def all_init_atms_alt_def) have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x by auto have H': ‹A = B ⟹ A x ⟹ B x› for A B x by auto obtain M N D NE UE NEk UEk NS US N0 U0 Q WS where T: ‹T = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS)› by (cases T) { assume pre: ‹propagate_pure_wl_pre L T› note cong = trail_pol_cong heuristic_rel_cong option_lookup_clause_rel_cong vdom_m_cong[symmetric, THEN H] isasat_input_nempty_cong[THEN iffD1] isasat_input_bounded_cong[THEN iffD1] cach_refinement_empty_cong[THEN H'] phase_saving_cong[THEN H'] ℒ_a_l_l_cong[THEN H] D₀_cong[THEN H] lookup_clause_rel_cong map_fun_rel_D₀_cong isa_vmtf_cong[THEN isa_vmtf_consD] isasat_input_nempty_cong[THEN iffD1] isasat_input_bounded_cong[THEN iffD1] note subst = empty_occs_list_cong let ?T = ‹(Propagated L 0 # M, N, D, NE, UE, add_mset {#L'#} NEk, UEk, NS, US, N0, U0, add_mset (- L') Q, WS)› have ‹L' ∈# all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l N#} + (NE + NEk) + NS + N0)› and D: ‹D = None› and undef: ‹undefined_lit M L'› using pre assms(2) unfolding propagate_pure_wl_pre_def propagate_pure_l_pre_def apply - by (solves ‹normalize_goal+; auto simp: T twl_st_l_def all_init_lits_of_wl_def›)+ then have H: ‹set_mset (all_init_lits_of_wl ?T) = set_mset (all_init_lits_of_wl T)› unfolding T by (auto simp: all_init_lits_of_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset in_all_lits_of_mm_uminus_iff) then have H: ‹set_mset (all_init_atms_st ?T) = set_mset (all_init_atms_st T)› unfolding all_init_atms_st_alt_def by auto note _ = D undef subst[OF H] cong[OF H[symmetric]] } note cong = this(4-) and subst = this(3) and D = this(1) and undef = this(2) show ?thesis supply [simp del] = isasat_input_nempty_def isasat_input_bounded_def unfolding propagate_pure_bt_wl_alt_def isa_propagate_pure_bt_wl_def T apply (rewrite at ‹let _ = get_trail_wl_heur _ in _› Let_def) apply (rewrite at ‹let _ = get_stats_heur _ in _› Let_def) apply (cases S₀) apply (hypsubst, unfold prod.simps) apply (refine_vcg cons_trail_Propagated_tr2[of _ _ _ _ _ _ ‹all_init_atms_st T›]) subgoal by (auto simp: DECISION_REASON_def) subgoal by (rule cons_trail_Propagated_tr_pre[of _ ‹get_trail_wl T› ‹all_init_atms_st T›]) (use ‹(L,L')∈Id› trail in ‹auto simp: propagate_pure_wl_pre_def propagate_pure_l_pre_def state_wl_l_def twl_st_l_def ℒ_a_l_l_all_init_atms all_init_lits_of_wl_def all_init_lits_of_l_def get_init_clss_l_def T›) subgoal by (use trail assms in ‹auto simp: T›) subgoal by (use ‹(L,L')∈Id› trail in ‹auto simp: propagate_pure_wl_pre_def propagate_pure_l_pre_def state_wl_l_def twl_st_l_def ℒ_a_l_l_all_init_atms all_init_lits_of_wl_def all_init_lits_of_l_def get_init_clss_l_def T›) subgoal using assms D undef unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def ℒ_a_l_l_all_init_atms all_init_atms_st_alt_def all_init_atms_alt_def T subst unfolding all_init_atms_st_alt_def[symmetric] apply - apply (simp only: in_pair_collect_simp) apply (intro conjI) subgoal apply simp using cong T apply fast done subgoal by simp subgoal apply simp using cong T apply fast done subgoal apply auto done subgoal apply simp done subgoal apply simp using cong(10-) T apply fast done subgoal apply simp using cong(10-) T by fast subgoal by simp subgoal by simp subgoal apply simp using cong T by fast subgoal by simp subgoal by simp subgoal apply simp using cong(4) T by fast subgoal by simp subgoal apply simp using cong T by fast subgoal by simp (use cong T in fast) subgoal by simp subgoal by simp (use cong T in fast) subgoal using subst by (simp add: T all_init_atms_st_def) subgoal by (simp add: learned_clss_count_def) subgoal by (simp add: learned_clss_count_def) subgoal by (simp add: subst) done done qed lemma isa_pure_literal_deletion_wl_pure_literal_deletion_wl: assumes S₀T: ‹(S₀, T) ∈ twl_st_heur_restart_ana' r u› and occs: ‹(occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D₀ (all_init_atms_st T))› shows ‹isa_pure_literal_deletion_wl occs S₀ ≤⇓{((_, U), V). (U,V)∈twl_st_heur_restart_ana' r u} (pure_literal_deletion_wl occs' T)› proof - have B: ‹⇓Id(pure_literal_deletion_wl occs' T) ≥ (do { ASSERT (pure_literal_deletion_wl_pre T); iterate_over_ℒ_a_l_l (λA (T). do { ASSERT (A ∈# all_init_atms_st T); let L = (if occs' (Pos A) ∧ ¬ occs' (Neg A) then Pos A else Neg A); let val = polarity (get_trail_wl T) L; if ¬occs' (-L) ∧ val = None then do {S ← propagate_pure_bt_wl L T; RETURN (S)} else RETURN (T) }) (atm_of `# all_init_lits_of_wl T) (λxs S. pure_literal_deletion_wl_inv T (atm_of `# all_init_lits_of_wl T) (S, xs)) (T)})› (is ‹_ ≥ ?B› is ‹_ ≥ do { ASSERT _; iterate_over_ℒ_a_l_l ?f _ _ _}›) proof - have [refine0]: ‹(x, xs) ∈ Id ⟹ set_mset x = set_mset (atm_of `# all_init_lits_of_wl T) ⟹ ((x, T), T, xs) ∈ {((a,b), (c,d)). (a,d) ∈Id ∧ (b,c)∈Id}› for x xs by (auto simp: all_init_atms_st_alt_def) have K: ‹a=b ⟹ a ≤⇓Id b› for a b by auto have Lin: ‹pure_literal_deletion_wl_inv T (atm_of `# all_init_lits_of_wl T) (x1, x2) ⟹ L ∈# x2 ⟹ L ∈# all_init_atms_st x1› for L x1 x2 unfolding pure_literal_deletion_wl_inv_def prod.simps pure_literal_deletion_l_inv_def apply normalize_goal+ apply (simp add: all_init_atms_st_alt_def) by (metis (no_types, lifting) all_init_lits_of_l_all_init_lits_of_wl mset_subset_eqD multiset.set_map rtranclp_cdcl_twl_pure_remove_l_same(7)) show ?thesis unfolding iterate_over_VMTF_def pure_literal_deletion_wl_def pure_literal_deletion_candidates_wl_def iterate_over_ℒ_a_l_l_def iterate_over_ℒ_a_l_lC_def nres_monad3 nres_bind_let_law If_bind_distrib apply (rewrite at ‹let _ = ⋃ _ in _› Let_def) apply refine_vcg subgoal by (auto simp: all_init_atms_st_alt_def) subgoal by fast subgoal for 𝒜 xs x x' x1 x2 unfolding all_init_atms_st_alt_def pure_literal_deletion_l_inv_def pure_literal_deletion_wl_inv_def case_prod_beta apply normalize_goal+ apply (rename_tac ya yb yc, rule_tac x=ya in exI[of]) apply (rule_tac x=yb in exI[of]) apply (intro conjI) apply simp apply simp apply (rule_tac x=yc in exI[of]) apply simp_all by (metis distinct_subseteq_iff set_image_mset subset_mset.dual_order.trans subset_mset.order_refl) subgoal by auto subgoal by auto subgoal by auto subgoal by (simp add: Lin) subgoal by (auto simp: polarity_def) apply (rule K) subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed have vmtf: ‹get_vmtf_heur S₀ ∈ bump_heur (all_init_atms_st T) (get_trail_wl T)› and nempty: ‹isasat_input_nempty (all_init_atms_st T)› and bounded: ‹isasat_input_bounded (all_init_atms_st T)› using assms unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def by (simp_all add: all_init_atms_alt_def del: isasat_input_nempty_def) let ?vm = ‹get_vmtf_heur S₀› obtain M where vmtf': ‹(get_vmtf_heur_array S₀, fst (snd (bump_get_heuristics ?vm)), get_vmtf_heur_fst S₀, fst (snd (snd (snd (bump_get_heuristics ?vm)))), snd (snd (snd (snd (bump_get_heuristics ?vm))))) ∈ vmtf (all_init_atms_st T) M› and M: ‹M = (get_trail_wl T) ∨ M = (get_unit_trail (get_trail_wl T))› using vmtf unfolding bump_heur_def get_vmtf_heur_array_def bump_get_heuristics_def get_vmtf_heur_fst_def by (cases ‹bump_get_heuristics ns›) (auto simp: bump_get_heuristics_def bumped_vmtf_array_fst_def split: if_splits) have C: ‹⇓Id ?B ≥ (do { ASSERT (pure_literal_deletion_wl_pre T); (S) ← iterate_over_VMTF ?f (λS. ∃xs. pure_literal_deletion_wl_inv T (atm_of `# all_init_lits_of_wl T) (S, xs)) (get_vmtf_heur_array S₀, Some (get_vmtf_heur_fst S₀)) (T); RETURN (S) })› (is ‹_ ≥ ?C›) apply (refine_vcg iterate_over_VMTF_iterate_over_ℒ_a_l_l) unfolding nres_monad2 all_init_atms_st_alt_def[symmetric] apply (rule iterate_over_VMTF_iterate_over_ℒ_a_l_l[OF vmtf']) subgoal using nempty by auto subgoal using bounded by auto subgoal by blast done have D: ‹⇓(twl_st_heur_restart_ana' r u) ?C ≥ (do { ASSERT (pure_literal_deletion_wl_pre T); S ← iterate_over_VMTF (λA (T). do { ASSERT (nat_of_lit (Pos A) < length occs); ASSERT (nat_of_lit (Neg A) < length occs); ASSERT (occs ! (nat_of_lit(Pos A)) = occs' (Pos A)); ASSERT (occs ! (nat_of_lit(Neg A)) = occs' (Neg A)); let L = (if occs ! (nat_of_lit(Pos A)) ∧ ¬ occs ! (nat_of_lit (Neg A)) then Pos A else Neg A); val ← mop_polarity_pol (get_trail_wl_heur T) L; ASSERT (nat_of_lit (-L) < length occs); if ¬occs ! nat_of_lit (-L) ∧ val = None then do {S ← isa_propagate_pure_bt_wl L T; ASSERT (get_vmtf_heur_array S₀ = get_vmtf_heur_array S); RETURN (S)} else RETURN (T) }) (λS. get_vmtf_heur_array S₀ = get_vmtf_heur_array S) (get_vmtf_heur_array S₀, Some (get_vmtf_heur_fst S₀)) (S₀); RETURN S})› (is ‹_ ≥ ?D›) proof - have [refine]: ‹ ((Some (get_vmtf_heur_fst S₀), S₀), Some (get_vmtf_heur_fst S₀), T) ∈ Id ×_r {(U,V). (U,V)∈twl_st_heur_restart_ana' r u ∧ get_vmtf_heur_array S₀ = get_vmtf_heur_array U}› using assms by auto have H: ‹P ∈#ℒ_a_l_l (atm_of `# all_init_lits_of_wl A) ⟷ atm_of P ∈# all_init_atms_st A› for P A using ℒ_a_l_l_all_init_atms(2) in_ℒ_a_l_l_atm_of_𝒜_i_n by (metis all_init_atms_st_alt_def) have K: ‹a=b ⟹(a,b)∈Id› for a b by auto have [simp, intro!]: ‹(x2a, x2) ∈ twl_st_heur_restart_ana r ⟹ (get_trail_wl_heur x2a, get_trail_wl x2) ∈ trail_pol (atm_of `# all_init_lits_of_wl x2)› for x2a x2 by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def all_init_atms_alt_def all_init_atms_st_alt_def) have occs_st: ‹occs ! (nat_of_lit (Pos (x1))) = occs' (Pos (x1))› ‹occs ! (nat_of_lit (Neg (x1))) = occs' (Neg (x1))› ‹nat_of_lit (Pos x1) < length occs› ‹nat_of_lit (Neg x1) < length occs› if inv: ‹∃xs. pure_literal_deletion_wl_inv T (atm_of `# all_init_lits_of_wl T) (x2, xs)› ‹x1 ∈# all_init_atms_st x2› for x1 x2 proof - obtain xs where inv: ‹pure_literal_deletion_wl_inv T (atm_of `# all_init_lits_of_wl T) (x2, xs)› using inv by auto have ‹x1 ∈# all_init_atms_st T› using inv unfolding pure_literal_deletion_wl_inv_def prod.simps pure_literal_deletion_l_inv_def apply - by normalize_goal+ (metis (no_types, opaque_lifting) all_init_atms_st_alt_def all_init_lits_of_l_all_init_lits_of_wl rtranclp_cdcl_twl_pure_remove_l_same(7) set_image_mset that(2)) then show ‹occs ! (nat_of_lit (Pos (x1))) = occs' (Pos (x1))› ‹occs ! (nat_of_lit (Neg (x1))) = occs' (Neg (x1))› ‹nat_of_lit (Pos x1) < length occs› ‹nat_of_lit (Neg x1) < length occs› using occs by (auto simp: map_fun_rel_def ℒ_a_l_l_add_mset dest!: multi_member_split) qed show ?thesis unfolding iterate_over_VMTF_def nres_monad3 nres_bind_let_law prod.simps If_bind_distrib mop_polarity_pol_def nres_monad2 nres_monad1[of _ ‹λx. RETURN (_,x)›] apply (refine_vcg isa_propagate_pure_bt_wl_propagate_pure_bt_wl[where r=r and u=u]) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for x x' x1 x2 x1a x2a unfolding case_prod_beta by (rule occs_st) (assumption, simp) subgoal for x x' x1 x2 x1a x2a unfolding case_prod_beta by (rule occs_st) (assumption, simp) subgoal for x x' x1 x2 x1a x2a unfolding case_prod_beta by (rule occs_st) (assumption, simp) subgoal for x x' x1 x2 x1a x2a unfolding case_prod_beta by (rule occs_st) (assumption, simp) subgoal for x x' x1 x2 x1a x2a by (rule polarity_pol_pre[of _ _ ‹(all_init_atms_st x2)›]) (auto simp add: H ℒ_a_l_l_all_init_atms all_init_atms_st_alt_def all_init_atms_alt_def) apply (rule K) subgoal for x x' x1 x2 x1a x2a using assms by (auto intro!: polarity_pol_polarity[of ‹(all_init_atms_st x2)›, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id] simp: H all_init_atms_st_alt_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: get_vmtf_heur_array_def) subgoal by auto subgoal by auto subgoal by auto done qed have E: ‹⇓{((_, U), V). (U,V)∈Id}?D ≥ isa_pure_literal_deletion_wl_raw occs S₀› (is ‹_ ≥ ?E›) proof - have K: ‹a=b ⟹ a≤⇓Id b› for a b by auto have H1: ‹(S, x'a) ∈ Id ⟹ ((x1b + 1, S), x'a) ∈ {((a,b),c). (b,c)∈Id}› for S x'a x1b by auto have H2: ‹⋀x x' x1 x2 x1a x2a. pure_literal_deletion_wl_pre T ⟹ isa_pure_literal_deletion_wl_pre S₀ ⟹ (x, x') ∈ {((a, b, c), x, y). (a, x) ∈ Id ∧ (c, y) ∈ Id} ⟹ x' = (x1, x2) ⟹ x = (x1a, x2a) ⟹ (x2a, x2) ∈ {((a,b),c). (b,c)∈Id}› by auto have [refine]: ‹((Some (get_vmtf_heur_fst S₀), 0, S₀), Some (get_vmtf_heur_fst S₀), S₀) ∈ {((a,b,c), (x,y)). (a,x)∈ Id ∧ (c,y)∈Id}› by auto show ?thesis unfolding isa_pure_literal_deletion_wl_raw_def iterate_over_VMTF_def prod.simps Let_def apply refine_vcg subgoal using assms unfolding isa_pure_literal_deletion_wl_pre_def by fast 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 apply (rule K) subgoal by auto subgoal by auto apply (rule K) subgoal by auto subgoal by auto apply (rule H1) subgoal by auto subgoal by auto subgoal by auto apply (rule H2; assumption) subgoal by auto done qed have F: ‹⇓Id ?E ≥ isa_pure_literal_deletion_wl occs S₀› proof - have [refine]: ‹((Some (get_vmtf_heur_fst S₀), 0, S₀), snd (get_vmtf_heur_array S₀, Some (get_vmtf_heur_fst S₀)), 0, S₀) ∈ Id ×_r Id ×_r Id› by auto have K: ‹a=b ⟹ a≤⇓Id b› for a b by auto show ?thesis unfolding isa_pure_literal_deletion_wl_def isa_pure_literal_deletion_wl_raw_def iterate_over_VMTF_def nres_monad3 nres_monad2 If_bind_distrib case_prod_beta nres_bind_let_law apply refine_vcg subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule K) subgoal by auto subgoal by auto apply (rule K) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed show ?thesis apply (rule order_trans[OF F]) apply (rule order_trans) apply (rule ref_two_step'[OF E]) apply (subst conc_fun_chain) apply (rule order_trans) apply (rule ref_two_step'[OF D]) apply (subst conc_fun_chain) apply (rule order_trans) apply (rule ref_two_step'[OF C]) apply (subst conc_fun_chain) apply (rule order_trans) apply (rule ref_two_step'[OF B]) apply (rule ref_two_step'') by auto qed end

Theory IsaSAT_Simplify_Pure_Literals