theory Watched_Literals_List_Enumeration imports Watched_Literals_Algorithm_Enumeration Watched_Literals.Watched_Literals_List begin lemma convert_lits_l_filter_decided_uminus: ‹(S, S') ∈ convert_lits_l M N ⟹ map (λx. -lit_of x) (filter is_decided S') = map (λx. -lit_of x) (filter is_decided S)› apply (induction S arbitrary: S') subgoal by auto subgoal for L S S' by (cases S') auto done lemma convert_lits_l_DECO_clause[simp]: ‹(S, S') ∈ convert_lits_l M N ⟹ DECO_clause S' = DECO_clause S› by (auto simp: DECO_clause_def uminus_lit_of_image_mset convert_lits_l_filter_decided_uminus simp flip: mset_filter mset_map) lemma convert_lits_l_TWL_DECO_clause[simp]: ‹(S, S') ∈ convert_lits_l M N ⟹ TWL_DECO_clause S' = TWL_DECO_clause S› by (auto simp: TWL_DECO_clause_def uminus_lit_of_image_mset) (auto simp: take_map[symmetric] drop_map[symmetric] mset_filter[symmetric] convert_lits_l_filter_decided mset_map[symmetric] simp del: mset_map) lemma [twl_st_l]: ‹(S, S') ∈ twl_st_l b ⟹ DECO_clause (get_trail S') = DECO_clause (get_trail_l S)› by (auto simp: twl_st_l_def convert_lits_l_DECO_clause) lemma [twl_st_l]: ‹(S, S') ∈ twl_st_l b ⟹ TWL_DECO_clause (get_trail S') = TWL_DECO_clause (get_trail_l S)› by (auto simp: twl_st_l_def convert_lits_l_DECO_clause) lemma DECO_clause_simp[simp]: ‹DECO_clause (A @ B) = DECO_clause A + DECO_clause B› ‹DECO_clause (Decided K # A) = add_mset (-K) (DECO_clause A)› ‹DECO_clause (Propagated K C # A) = DECO_clause A› ‹(⋀K. K ∈ set A ⟹ ¬is_decided K) ⟹ DECO_clause A = {#}› by (auto simp: DECO_clause_def filter_mset_empty_conv) definition find_decomp_target :: ‹nat ⇒ 'v twl_st_l ⇒ ('v twl_st_l × 'v literal) nres› where ‹find_decomp_target = (λi S. SPEC(λ(T, K). ∃M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧ (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧ get_level (get_trail_l S) K = i))› fun propagate_unit_and_add :: ‹'v literal ⇒ 'v twl_st ⇒ 'v twl_st› where ‹propagate_unit_and_add K (M, N, U, D, NE, UE, WS, Q) = (Propagated (-K) {#-K#} # M, N, U, None, add_mset {#-K#} NE, UE, {#}, {#K#})› fun propagate_unit_and_add_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where ‹propagate_unit_and_add_l K (M, N, D, NE, UE, WS, Q) = (Propagated (-K) 0 # M, N, None, add_mset {#-K#} NE, UE, {#}, {#K#})› definition negate_mode_bj_unit_l_inv :: ‹'v twl_st_l ⇒ bool› where ‹negate_mode_bj_unit_l_inv S ⟷ (∃(S'::'v twl_st) b. (S, S') ∈ twl_st_l b ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧ twl_struct_invs S' ∧ get_conflict_l S = None)› definition negate_mode_bj_unit_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where ‹negate_mode_bj_unit_l = (λS. do { ASSERT(negate_mode_bj_unit_l_inv S); (S, K) ← find_decomp_target 1 S; RETURN (propagate_unit_and_add_l K S) })› lemma negate_mode_bj_unit_l: fixes S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› assumes ‹count_decided (get_trail_l S) = 1› and SS': ‹(S, S') ∈ twl_st_l b› and struct_invs: ‹twl_struct_invs S'› and add_inv: ‹twl_list_invs S› and stgy_inv: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› shows ‹negate_mode_bj_unit_l S ≤ ⇓{(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› proof - have H: ‹∃y∈Collect (negate_model_and_add_twl S'). (propagate_unit_and_add_l x2 x1, y) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› if count_dec: ‹count_decided (get_trail_l S) = 1› and S_S': ‹(S, S') ∈ twl_st_l b› and ‹twl_struct_invs S'› and ‹twl_list_invs S› and ‹twl_stgy_invs S'› and x_S: ‹x ∈ {(T, K). ∃M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧ (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧ get_level (get_trail_l S) K = 1}› and x: ‹x = (x1, x2)› for x :: ‹'v twl_st_l × 'v literal› and x1 :: ‹'v twl_st_l› and x2 :: ‹'v literal› proof - let ?y0 = ‹(λ(M, Oth). (drop (length M - length (get_trail_l x1)) (get_trail S'), Oth)) S'› let ?y1 = ‹propagate_unit_and_add x2 ?y0› obtain M1 M2 where S_x1: ‹equality_except_trail S x1› and tr_M1: ‹get_trail_l x1 = M1› and decomp: ‹(Decided x2 # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S))› and lev_x2: ‹get_level (get_trail_l S) x2 = 1› using x_S unfolding x by blast obtain M2' where decomp': ‹(Decided x2 # drop (length (get_trail S') - length M1) (get_trail S'), M2') ∈ set (get_all_ann_decomposition (get_trail S'))› and conv: ‹(get_trail_l S, get_trail S') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› and conv_M1: ‹(M1, drop (length (get_trail S') - length M1) (get_trail S')) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› using convert_lits_l_decomp_ex[OF decomp, of ‹get_trail S'› ‹get_clauses_l S› ‹get_unit_clauses_l S›] S_S' by (auto simp: twl_st_l_def) have x2_DECO: ‹{#-x2#} = DECO_clause (get_trail S')› using decomp count_dec S_S' by (auto simp: twl_st_l filter_mset_empty_conv count_decided_0_iff dest!: get_all_ann_decomposition_exists_prepend) have M1_drop: ‹drop (length (get_trail_l S) - length M1) (get_trail_l S) = M1› using decomp by auto have ‹(propagate_unit_and_add_l x2 x1, ?y1) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› using S_S' S_x1 tr_M1 decomp decomp' lev_x2 add_inv conv_M1 unfolding x apply (cases x1; cases S') by (auto simp: twl_st_l_def twl_list_invs_def convert_lit.simps split: option.splits intro: convert_lits_l_extend_mono) moreover have ‹negate_model_and_add_twl S' ?y1› using S_S' confl lev_x2 count_dec tr_M1 S_x1 decomp decomp' M1_drop unfolding x by (cases x1) (auto simp: twl_st_l_def x2_DECO simp del: convert_lits_l_DECO_clause intro!: negate_model_and_add_twl.bj_unit[of _ _ ] split: option.splits) ultimately show ?thesis apply - by (rule bexI[of _ ?y1]) fast+ qed show ?thesis using assms unfolding negate_mode_bj_unit_l_def find_decomp_target_def apply (refine_rcg) subgoal unfolding negate_mode_bj_unit_l_inv_def by fast subgoal by (subst RETURN_RES_refine_iff) (rule H; assumption) done qed definition DECO_clause_l :: ‹('v, 'a) ann_lits ⇒ 'v clause_l› where ‹DECO_clause_l M = map (uminus o lit_of) (filter is_decided M)› fun propagate_nonunit_and_add :: ‹'v literal ⇒ 'v literal multiset twl_clause ⇒ 'v twl_st ⇒ 'v twl_st› where ‹propagate_nonunit_and_add K C (M, N, U, D, NE, UE, WS, Q) = do { (Propagated (-K) (clause C) # M, add_mset C N, U, None, NE, UE, {#}, {#K#}) }› fun propagate_nonunit_and_add_l :: ‹'v literal ⇒ 'v clause_l ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where ‹propagate_nonunit_and_add_l K C i (M, N, D, NE, UE, WS, Q) = do { (Propagated (-K) i # M, fmupd i (C, True) N, None, NE, UE, {#}, {#K#}) }› definition negate_mode_bj_nonunit_l_inv where ‹negate_mode_bj_nonunit_l_inv S ⟷ (∃S'' b. (S, S'') ∈ twl_st_l b ∧ twl_list_invs S ∧ count_decided (get_trail_l S) > 1 ∧ twl_struct_invs S'' ∧ twl_stgy_invs S'' ∧ get_conflict_l S = None)› definition negate_mode_bj_nonunit_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where ‹negate_mode_bj_nonunit_l = (λS. do { ASSERT(negate_mode_bj_nonunit_l_inv S); let C = DECO_clause_l (get_trail_l S); (S, K) ← find_decomp_target (count_decided (get_trail_l S)) S; i ← get_fresh_index (get_clauses_l S); RETURN (propagate_nonunit_and_add_l K C i S) })› lemma DECO_clause_l_DECO_clause[simp]: ‹mset (DECO_clause_l M1) = DECO_clause M1› by (induction M1) (auto simp: DECO_clause_l_def DECO_clause_def convert_lits_l_def) lemma TWL_DECO_clause_alt_def: ‹TWL_DECO_clause M1 = TWL_Clause (mset (watched_l (DECO_clause_l M1))) (mset (unwatched_l (DECO_clause_l M1)))› unfolding TWL_DECO_clause_def convert_lits_l_def by (auto simp: TWL_DECO_clause_def convert_lits_l_def filter_map take_map drop_map DECO_clause_l_def) lemma length_DECO_clause_l[simp]: ‹length (DECO_clause_l M) = count_decided M› unfolding DECO_clause_l_def count_decided_def by auto lemma negate_mode_bj_nonunit_l: fixes S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› assumes count_dec: ‹count_decided (get_trail_l S) > 1› and SS': ‹(S, S') ∈ twl_st_l b› and struct_invs: ‹twl_struct_invs S'› and add_inv: ‹twl_list_invs S› and stgy_inv: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› shows ‹negate_mode_bj_nonunit_l S ≤ ⇓{(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› proof - have H: ‹RETURN (propagate_nonunit_and_add_l x2 (DECO_clause_l (get_trail_l S)) i x1) ≤ ⇓ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› if x_S: ‹x ∈ {(T, K). ∃M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧ (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧ get_level (get_trail_l S) K = count_decided (get_trail_l S)}› and x: ‹x = (x1, x2)› and i: ‹i ∈ {i. 0 < i ∧ i ∉# dom_m (get_clauses_l x1)}› for x :: ‹'v twl_st_l × 'v literal› and x1 :: ‹'v twl_st_l› and x2 :: ‹'v literal› and i :: ‹nat› proof - obtain M N U D NE UE Q where x1: ‹x1 = (M, N, U, D, NE, UE, Q)› by (cases x1) obtain M1 M2 where S_x1: ‹equality_except_trail S x1› and tr_M1: ‹get_trail_l x1 = M1› and decomp: ‹(Decided x2 # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S))› and lev_K: ‹get_level (get_trail_l S) x2 = count_decided (get_trail_l S)› using x_S unfolding x by blast let ?y0 = ‹(λ(M, Oth). (drop (length M - length (get_trail_l x1)) (get_trail S'), Oth)) S'› let ?y1 = ‹propagate_nonunit_and_add x2 (TWL_DECO_clause (get_trail S')) ?y0› obtain M3 where M3: ‹get_trail_l S = M3 @ M2 @ Decided x2 # M1› using decomp by blast have confl': ‹get_conflict S' = None› and trail_S': ‹(get_trail_l S, get_trail S') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› using confl SS' by (auto simp: twl_st_l_def) have ‹no_dup (trail (state⇩W_of S'))› using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by fast then have ‹no_dup (get_trail_l S)› using SS' by (auto simp: twl_st twl_st_l) then have [simp]: ‹count_decided M3 = 0› ‹count_decided M2 = 0› ‹filter is_decided M3 = []› ‹filter is_decided M2 = []› using lev_K by (auto simp: M3 count_decided_0_iff) obtain M2' where decomp': ‹(Decided x2 # drop (length (get_trail S') - length M1) (get_trail S'), M2') ∈ set (get_all_ann_decomposition (get_trail S'))› and conv: ‹(get_trail_l S, get_trail S') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› and conv_M1: ‹(M1, drop (length (get_trail S') - length M1) (get_trail S')) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› using convert_lits_l_decomp_ex[OF decomp, of ‹get_trail S'› ‹get_clauses_l S› ‹get_unit_clauses_l S›] SS' by (auto simp: twl_st_l_def) have M1_drop: ‹drop (length (get_trail_l S) - length M1) (get_trail_l S) = M1› using decomp by auto moreover have ‹- x2 ∈ set (watched_l (DECO_clause_l (get_trail_l S)))› using S_x1 tr_M1 SS' i decomp add_inv lev_K M3 by (auto simp: DECO_clause_l_def) moreover have ‹DECO_clause_l (get_trail_l S) ! 0 = -x2› by (auto simp: M3 DECO_clause_l_def) moreover have ‹Propagated L i ∉ set M1› for L using add_inv i S_x1 M3 unfolding twl_list_invs_def by (cases S; cases x1) auto ultimately have ‹(propagate_nonunit_and_add_l x2 (DECO_clause_l (get_trail_l S)) i x1, ?y1) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› using S_x1 tr_M1 SS' i add_inv decomp conv_M1 M1_drop by (cases S; cases S') (auto simp add: x1 twl_st_l_def twl_list_invs_def init_clss_l_mapsto_upd_notin TWL_DECO_clause_alt_def[symmetric] learned_clss_l_mapsto_upd_notin_irrelev convert_lit.simps intro!: convert_lits_l_extend_mono[of _ _ N ‹D + NE›]) moreover have ‹?y1 ∈ Collect (negate_model_and_add_twl S')› using S_x1 tr_M1 i add_inv decomp confl confl' count_dec lev_K decomp' S_x1 SS' by (cases S; cases S') (auto simp: x1 twl_st_l_def intro!: negate_model_and_add_twl.bj_nonunit[of _ _ M2']) ultimately have ‹∃y∈Collect (negate_model_and_add_twl S'). (propagate_nonunit_and_add_l x2 (DECO_clause_l (get_trail_l S)) i x1, y) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› apply - apply (rule bexI[of _ ?y1]) apply fast+ done then show ?thesis unfolding x1 apply (subst RETURN_RES_refine_iff) by fast qed have ‹negate_mode_bj_nonunit_l_inv S› using assms unfolding negate_mode_bj_nonunit_l_inv_def by blast then show ?thesis unfolding negate_mode_bj_nonunit_l_def find_decomp_target_def get_fresh_index_def apply refine_vcg apply (rule H; assumption) done qed fun restart_nonunit_and_add :: ‹'v literal multiset twl_clause ⇒ 'v twl_st ⇒ 'v twl_st› where ‹restart_nonunit_and_add C (M, N, U, D, NE, UE, WS, Q) = do { (M, add_mset C N, U, None, NE, UE, {#}, {#}) }› fun restart_nonunit_and_add_l :: ‹'v clause_l ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where ‹restart_nonunit_and_add_l C i (M, N, D, NE, UE, WS, Q) = do { (M, fmupd i (C, True) N, None, NE, UE, {#}, {#}) }› definition negate_mode_restart_nonunit_l_inv :: ‹'v twl_st_l ⇒ bool› where ‹negate_mode_restart_nonunit_l_inv S ⟷ (∃S' b. (S, S') ∈ twl_st_l b ∧ twl_struct_invs S' ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧ count_decided (get_trail_l S) > 1 ∧ get_conflict_l S = None)› definition negate_mode_restart_nonunit_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where ‹negate_mode_restart_nonunit_l = (λS. do { ASSERT(negate_mode_restart_nonunit_l_inv S); let C = DECO_clause_l (get_trail_l S); i ← SPEC(λi. i < count_decided (get_trail_l S)); (S, K) ← find_decomp_target i S; i ← get_fresh_index (get_clauses_l S); RETURN (restart_nonunit_and_add_l C i S) })› lemma negate_mode_restart_nonunit_l: fixes S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› assumes count_dec: ‹count_decided (get_trail_l S) > 1› and SS': ‹(S, S') ∈ twl_st_l b› and struct_invs: ‹twl_struct_invs S'› and add_inv: ‹twl_list_invs S› and stgy_inv: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› shows ‹negate_mode_restart_nonunit_l S ≤ ⇓{(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› proof - have H: ‹RETURN (restart_nonunit_and_add_l (DECO_clause_l (get_trail_l S)) i x1) ≤ ⇓ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› if j: ‹j ∈ {i. i < count_decided (get_trail_l S)}› and x_S: ‹x ∈ {(T, K). ∃M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧ (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧ get_level (get_trail_l S) K = j}› and x: ‹x = (x1, x2)› and i: ‹i ∈ {i. 0 < i ∧ i ∉# dom_m (get_clauses_l x1)}› for x :: ‹'v twl_st_l × 'v literal› and x1 :: ‹'v twl_st_l› and x2 :: ‹'v literal› and i j :: ‹nat› proof - obtain M N U D NE UE Q where x1: ‹x1 = (M, N, U, D, NE, UE, Q)› by (cases x1) obtain M1 M2 where S_x1: ‹equality_except_trail S x1› and tr_M1: ‹get_trail_l x1 = M1› and decomp: ‹(Decided x2 # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S))› and lev_K: ‹get_level (get_trail_l S) x2 = j› using x_S unfolding x by blast let ?y0 = ‹(λ(M, Oth). (drop (length (get_trail S') - length M1) (get_trail S'), Oth)) S'› let ?y1 = ‹restart_nonunit_and_add (TWL_DECO_clause (get_trail S')) ?y0› obtain M3 where M3: ‹get_trail_l S = M3 @ M2 @ Decided x2 # M1› using decomp by blast have ‹M = M1› using S_x1 SS' decomp tr_M1 unfolding x1 by (cases S; cases S') auto have confl': ‹get_conflict S' = None› and trail_S': ‹(get_trail_l S, get_trail S') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› using confl SS' by (auto simp: twl_st_l) have ‹no_dup (trail (state⇩W_of S'))› using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by fast then have ‹no_dup (get_trail_l S)› using SS' by (auto simp: twl_st twl_st_l) obtain M2' where decomp': ‹(Decided x2 # drop (length (get_trail S') - length M1) (get_trail S'), M2') ∈ set (get_all_ann_decomposition (get_trail S'))› and conv: ‹(get_trail_l S, get_trail S') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› and conv_M1: ‹(M1, drop (length (get_trail S') - length M1) (get_trail S')) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› using convert_lits_l_decomp_ex[OF decomp, of ‹get_trail S'› ‹get_clauses_l S› ‹get_unit_clauses_l S›] SS' by (auto simp: twl_st_l_def) have M1_drop: ‹drop (length (get_trail_l S) - length M1) (get_trail_l S) = M1› using decomp by auto moreover have ‹Propagated L i ∉ set M1› for L using add_inv i S_x1 M3 unfolding twl_list_invs_def by (cases S; cases x1) auto ultimately have ‹(restart_nonunit_and_add_l (DECO_clause_l (get_trail_l S)) i x1, ?y1) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› using S_x1 tr_M1 SS' i add_inv decomp conv_M1 decomp' by (cases S; cases S') (auto simp: x1 twl_st_l_def twl_list_invs_def init_clss_l_mapsto_upd_notin TWL_DECO_clause_alt_def[symmetric] learned_clss_l_mapsto_upd_notin_irrelev dest: get_all_ann_decomposition_exists_prepend intro!: convert_lits_l_extend_mono[of _ _ N ‹D+NE›]) moreover { have ‹get_level (get_trail_l S) x2 < count_decided (get_trail_l S)› using lev_K j by auto then have ‹?y1 ∈ Collect (negate_model_and_add_twl S')› using S_x1 tr_M1 i add_inv decomp' confl confl' count_dec lev_K SS' by (cases S; cases S') (auto simp: x1 twl_st_l_def intro!: negate_model_and_add_twl.restart_nonunit[of x2 _ ‹M2'›]) } ultimately have ‹∃y∈Collect (negate_model_and_add_twl S'). (restart_nonunit_and_add_l (DECO_clause_l (get_trail_l S)) i x1, y) ∈ {(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}› apply - apply (rule bexI[of _ ?y1]) apply fast+ done then show ?thesis unfolding x1 apply (subst RETURN_RES_refine_iff) by fast qed show ?thesis unfolding negate_mode_restart_nonunit_l_def find_decomp_target_def get_fresh_index_def apply refine_vcg subgoal using assms unfolding negate_mode_restart_nonunit_l_inv_def by fast subgoal supply [[unify_trace_failure]] apply (rule H; assumption) done done qed definition negate_mode_l_inv where ‹negate_mode_l_inv S ⟷ (∃S' b. (S, S') ∈ twl_st_l b ∧ twl_struct_invs S' ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧ get_conflict_l S = None ∧ count_decided (get_trail_l S) ≠ 0)› definition negate_mode_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where ‹negate_mode_l S = do { ASSERT(negate_mode_l_inv S); if count_decided (get_trail_l S) = 1 then negate_mode_bj_unit_l S else do { b ← SPEC(λ_. True); if b then negate_mode_bj_nonunit_l S else negate_mode_restart_nonunit_l S } }› lemma negate_mode_l: fixes S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› assumes SS': ‹(S, S') ∈ twl_st_l b› and struct_invs: ‹twl_struct_invs S'› and add_inv: ‹twl_list_invs S› and stgy_inv: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› and ‹count_decided (get_trail_l S) ≠ 0› shows ‹negate_mode_l S ≤ ⇓{(S, S''). (S, S'') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (negate_model_and_add_twl S'))› unfolding negate_mode_l_def apply (refine_vcg negate_mode_restart_nonunit_l[OF _ SS'] negate_mode_bj_unit_l[OF _ SS'] negate_mode_bj_nonunit_l[OF _ SS'] lhs_step_If) subgoal using assms unfolding negate_mode_l_inv_def by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by simp subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by simp subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast done context fixes P :: ‹'v literal set ⇒ bool› begin definition cdcl_twl_enum_inv_l :: ‹'v twl_st_l ⇒ bool› where ‹cdcl_twl_enum_inv_l S ⟷ (∃S'. (S, S') ∈ twl_st_l None ∧ cdcl_twl_enum_inv S') ∧ twl_list_invs S› definition cdcl_twl_enum_l :: ‹'v twl_st_l ⇒ bool nres› where ‹cdcl_twl_enum_l S = do { S ← cdcl_twl_stgy_prog_l S; S ← WHILE⇩T⇗cdcl_twl_enum_inv_l⇖ (λS. get_conflict_l S = None ∧ count_decided(get_trail_l S) > 0 ∧ ¬P (lits_of_l (get_trail_l S))) (λS. do { S ← negate_mode_l S; cdcl_twl_stgy_prog_l S }) S; if get_conflict_l S = None then RETURN (if count_decided(get_trail_l S) = 0 then P (lits_of_l (get_trail_l S)) else True) else RETURN (False) }› lemma negate_model_and_add_twl_resultD: ‹negate_model_and_add_twl S T ⟹ clauses_to_update T = {#} ∧ get_conflict T = None› by (auto simp: negate_model_and_add_twl.simps) lemma cdcl_twl_enum_l: fixes S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› assumes SS': ‹(S, S') ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs S'› and add_inv: ‹twl_list_invs S› and stgy_inv: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› and ‹count_decided (get_trail_l S) ≠ 0› and ‹clauses_to_update_l S = {#}› shows ‹cdcl_twl_enum_l S ≤ ⇓ bool_rel (cdcl_twl_enum P S')› unfolding cdcl_twl_enum_l_def cdcl_twl_enum_def apply (refine_vcg cdcl_twl_stgy_prog_l_spec_final' negate_mode_l) subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by fast apply assumption subgoal for S S' U U' using assms unfolding cdcl_twl_enum_inv_l_def apply - apply (intro conjI) apply (rule exI[of _ U']) by auto subgoal by (auto simp: twl_st_l) apply auto[] subgoal unfolding cdcl_twl_enum_inv_def by auto subgoal by fast subgoal by (auto simp: twl_st_l cdcl_twl_enum_inv_def) subgoal by (auto simp: twl_st_l) subgoal by (auto simp: twl_st_l) subgoal for S S' T T' U U' by (rule cdcl_twl_stgy_prog_l_spec_final'[THEN order.trans]) (auto simp: twl_st twl_st_l cdcl_twl_stgy_prog_l_pre_def cdcl_twl_enum_inv_def intro: negate_model_and_add_twl_twl_struct_invs negate_model_and_add_twl_twl_stgy_invs conc_fun_R_mono dest: negate_model_and_add_twl_resultD) subgoal by (auto simp: twl_st_l) subgoal by (auto simp: twl_st_l) done end end