Theory Watched_Literals_Watch_List

theory Watched_Literals_Watch_List_Initialisation imports Watched_Literals_Watch_List Watched_Literals_Initialisation begin subsection ‹Initialisation› type_synonym 'v twl_st_wl_init' = ‹(('v, nat) ann_lits × 'v clauses_l × 'v cconflict × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses ×'v lit_queue_wl)› type_synonym 'v twl_st_wl_init = ‹'v twl_st_wl_init' × 'v clauses› type_synonym 'v twl_st_wl_init_full = ‹'v twl_st_wl × 'v clauses› fun get_trail_init_wl :: ‹'v twl_st_wl_init ⇒ ('v, nat) ann_lit list› where ‹get_trail_init_wl ((M, _, _, _, _, _, _, _), _) = M› fun get_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses_l› where ‹get_clauses_init_wl ((_, N, _, _, _, _, _, _), OC) = N› fun get_conflict_init_wl :: ‹'v twl_st_wl_init ⇒ 'v cconflict› where ‹get_conflict_init_wl ((_, _, D, _, _, _, _, _), _) = D› fun literals_to_update_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clause› where ‹literals_to_update_init_wl ((_, _, _, _, _, _, _, NS, US, _, _, Q), _) = Q› fun other_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses› where ‹other_clauses_init_wl ((_, _, _, _, _, _), OC) = OC› fun add_empty_conflict_init_wl :: ‹'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where add_empty_conflict_init_wl_def[simp del]: ‹add_empty_conflict_init_wl ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC) = ((M, N, Some {#}, NE, UE, NEk, UEk, NS, US, add_mset {#} N0, U0, {#}), OC)› fun propagate_unit_init_wl :: ‹'v literal ⇒ 'v twl_st_wl_init ⇒ ('v twl_st_wl_init) nres› where propagate_unit_init_wl_def[simp del]: ‹propagate_unit_init_wl L ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC) = do { 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), OC)}› fun already_propagated_unit_init_wl :: ‹'v clause ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where already_propagated_unit_init_wl_def[simp del]: ‹already_propagated_unit_init_wl C ((M, N, D, NE, UE, NEk, UEk, Q), OC) = ((M, N, D, NE, UE, add_mset C NEk, UEk, Q), OC)› fun set_conflict_init_wl :: ‹'v literal ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where set_conflict_init_wl_def[simp del]: ‹set_conflict_init_wl L ((M, N, _, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC) = ((M, N, Some {#L#}, add_mset {#L#} NE, UE, NEk, UEk, NS, US, N0, U0, {#}), OC)› fun add_to_tautology_init_wl :: ‹'v clause_l ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init› where add_to_tautology_init_wl[simp del]: ‹add_to_tautology_init_wl C ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC) = ((M, N, D, NE, UE, NEk, UEk, add_mset (remdups_mset (mset C)) NS, US, N0, U0, Q), OC)› fun add_to_clauses_init_wl :: ‹'v clause_l ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where add_to_clauses_init_wl_def[simp del]: ‹add_to_clauses_init_wl C ((M, N, D, NE, UE, NEk, UEk, NS, US, Q), OC) = do { i ← get_fresh_index N; let b = (length C = 2); RETURN ((M, fmupd i (C, True) N, D, NE, UE, NEk, UEk, NS, US, Q), OC) }› definition init_dt_step_wl :: ‹'v clause_l ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where ‹init_dt_step_wl C S = (case get_conflict_init_wl S of None ⇒ if tautology (mset C) then RETURN (add_to_tautology_init_wl C S) else do { C ← remdups_clause C; if length C = 0 then RETURN (add_empty_conflict_init_wl S) else if length C = 1 then let L = hd C in if undefined_lit (get_trail_init_wl S) L then propagate_unit_init_wl L S else if L ∈ lits_of_l (get_trail_init_wl S) then RETURN (already_propagated_unit_init_wl (mset C) S) else RETURN (set_conflict_init_wl L S) else add_to_clauses_init_wl C S } | Some D ⇒ RETURN (add_to_other_init C S))› fun st_l_of_wl_init :: ‹'v twl_st_wl_init' ⇒ 'v twl_st_l› where ‹st_l_of_wl_init (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q) = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)› definition state_wl_l_init' where ‹state_wl_l_init' = {(S ,S'). S' = st_l_of_wl_init S}› definition init_dt_wl :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init nres› where ‹init_dt_wl CS = nfoldli CS (λ_. True) init_dt_step_wl› definition state_wl_l_init :: ‹('v twl_st_wl_init × 'v twl_st_l_init) set› where ‹state_wl_l_init = {(S, S'). (fst S, fst S') ∈ state_wl_l_init' ∧ other_clauses_init_wl S = other_clauses_l_init S'}› fun all_blits_are_in_problem_init where [simp del]: ‹all_blits_are_in_problem_init (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ⟷ (∀L. (∀(i, K, b)∈#mset (W L). K ∈# all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NEk + UEk) + (NS + US) + (N0 + U0))))› text ‹We assume that no clause has been deleted during initialisation. The definition is slightly redundant since term‹i ∈# dom_m N› is already entailed by term‹fst `# mset (W L) = clause_to_update L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})›.› named_theorems twl_st_wl_init lemma [twl_st_wl_init]: assumes ‹(S, S') ∈ state_wl_l_init› shows ‹get_conflict_l_init S' = get_conflict_init_wl S› ‹get_trail_l_init S' = get_trail_init_wl S› ‹other_clauses_l_init S' = other_clauses_init_wl S› ‹count_decided (get_trail_l_init S') = count_decided (get_trail_init_wl S)› using assms by (solves ‹cases S; cases S'; auto simp: state_wl_l_init_def state_wl_l_def state_wl_l_init'_def›)+ lemma in_clause_to_update_in_dom_mD: ‹bb ∈# clause_to_update L (a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, {#}, {#}) ⟹ bb ∈# dom_m aa› unfolding clause_to_update_def by force lemma init_dt_step_wl_init_dt_step: assumes S_S': ‹(S, S') ∈ state_wl_l_init› shows ‹init_dt_step_wl C S ≤ ⇓ state_wl_l_init (init_dt_step C S')› (is ‹_ ≤ ⇓ ?A _›) proof - define remdups_clause' :: ‹'a clause_l ⇒ 'a clause_l nres› where ‹remdups_clause' C = remdups_clause C› for C :: ‹'a clause_l› have remdups_clause: ‹remdups_clause' C ≤⇓ {(D,E). D = E ∧ distinct D} (remdups_clause C)› (is ‹_ ≤ ⇓ ?C _›) unfolding remdups_clause_def remdups_clause'_def by (auto intro!: RES_refine intro!: distinct_mset_mset_distinct[THEN iffD1] simp del: distinct_mset_remdups_mset distinct_mset_mset_distinct) fastforce have confl: ‹(get_conflict_init_wl S, get_conflict_l_init S') ∈ ⟨Id⟩option_rel› using S_S' by (auto simp: twl_st_wl_init) have false: ‹(add_empty_conflict_init_wl S, add_empty_conflict_init_l S') ∈ ?A› using S_S' apply (cases S; cases S') apply (auto simp: add_empty_conflict_init_wl_def add_empty_conflict_init_l_def all_blits_are_in_problem_init.simps state_wl_l_init'_def state_wl_l_init_def state_wl_l_def correct_watching.simps clause_to_update_def) done have [refine]: ‹ab = ac ⟹ C=C' ⟹ cons_trail_propagate_l (hd C) 0 ab ≤ ⇓ Id (cons_trail_propagate_l (hd C') 0 ac)› for C C' ab ac by auto have propa_unit: ‹propagate_unit_init_wl (hd C) S ≤ ⇓ ?A (propagate_unit_init_l (hd C') S')› if ‹(C, C') ∈ ?C› for C C' using S_S' apply (cases S; cases S'; cases ‹fst S›; cases ‹fst S'›; hypsubst) unfolding propagate_unit_init_wl_def propagate_unit_init_l_def fst_conv apply hypsubst unfolding propagate_unit_init_wl_def propagate_unit_init_l_def apply refine_rcg using that apply (auto simp: propagate_unit_init_l_def propagate_unit_init_wl_def state_wl_l_init'_def state_wl_l_init_def state_wl_l_def clause_to_update_def cons_trail_propagate_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset all_lits_of_mm_union) done have already_propa: ‹(already_propagated_unit_init_wl (mset C) S, already_propagated_unit_init_l (mset C') S') ∈ ?A› if ‹(C, C') ∈ ?C› for C C' using S_S' that by (cases S; cases S') (auto simp: already_propagated_unit_init_wl_def already_propagated_unit_init_l_def state_wl_l_init_def state_wl_l_def clause_to_update_def all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def) have set_conflict: ‹(set_conflict_init_wl (hd C) S, set_conflict_init_l C' S') ∈ ?A› if ‹C' = [hd C]› for C C' using S_S' that by (cases S; cases S') (auto simp: set_conflict_init_wl_def set_conflict_init_l_def state_wl_l_init_def state_wl_l_def clause_to_update_def state_wl_l_init'_def all_lits_of_mm_add_mset all_lits_of_m_add_mset) have add_to_clauses_init_wl: ‹add_to_clauses_init_wl C S ≤ ⇓ state_wl_l_init (add_to_clauses_init_l C' S')› if C: ‹length C ≥ 2› and conf: ‹get_conflict_l_init S' = None› and CC': ‹(C,C') ∈ ?C› for C C' proof - have [iff]: ‹C ! Suc 0 ∉ set (watched_l C) ⟷ False› ‹C ! 0 ∉ set (watched_l C) ⟷ False› and [dest!]: ‹⋀L. L ≠ C ! 0 ⟹ L ≠ C ! Suc 0 ⟹ L ∈ set (watched_l C) ⟹ False› using C by (cases C; cases ‹tl C›; auto)+ have [dest!]: ‹C ! 0 = C ! Suc 0 ⟹ False› using C CC' by (cases C; cases ‹tl C›; auto)+ show ?thesis using S_S' conf C CC' by (cases S; cases S') (auto 5 5 simp: add_to_clauses_init_wl_def add_to_clauses_init_l_def get_fresh_index_def state_wl_l_init_def state_wl_l_def clause_to_update_def all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def RES_RETURN_RES Let_def intro!: RES_refine filter_mset_cong2) qed have add_to_other_init': ‹(add_to_other_init C S, add_to_other_init C S') ∈ ?A› for C using S_S' by (cases S; cases S') (auto simp: state_wl_l_init_def state_wl_l_def clause_to_update_def all_lits_of_mm_add_mset all_lits_of_m_add_mset state_wl_l_init'_def) have add_to_tautology_init_wl: ‹(add_to_tautology_init_wl (C) S, add_to_tautology_init_l C' S') ∈ ?A› if ‹(C, C') ∈ Id› for C C' using S_S' that by (cases S; cases S') (auto simp: add_to_tautology_init_wl.simps add_to_tautology_init_l_def state_wl_l_init_def state_wl_l_init'_def) show ?thesis unfolding init_dt_step_wl_def init_dt_step_def apply (subst remdups_clause'_def[symmetric]) apply (refine_rcg confl false propa_unit already_propa set_conflict remdups_clause add_to_clauses_init_wl add_to_other_init' add_to_tautology_init_wl) subgoal by simp subgoal by simp subgoal using S_S' by (simp add: twl_st_wl_init) subgoal using S_S' by (simp add: twl_st_wl_init) subgoal using S_S' by (simp add: twl_st_wl_init) subgoal using S_S' by (simp add: twl_st_wl_init) subgoal for C Ca by (cases Ca) auto subgoal by linarith done qed lemma init_dt_wl_init_dt: assumes S_S': ‹(S, S') ∈ state_wl_l_init› shows ‹init_dt_wl C S ≤ ⇓ state_wl_l_init (init_dt C S')› proof - have C: ‹(C, C) ∈ ⟨Id⟩list_rel› by (auto simp: list_rel_def list.rel_refl_strong) show ?thesis unfolding init_dt_wl_def init_dt_def apply (refine_vcg C S_S') subgoal using S_S' by fast subgoal by (auto intro!: init_dt_step_wl_init_dt_step) done qed definition init_dt_wl_pre where ‹init_dt_wl_pre C S ⟷ (∃S'. (S, S') ∈ state_wl_l_init ∧ init_dt_pre C S')› definition init_dt_wl_spec where ‹init_dt_wl_spec C S T ⟷ (∃S' T'. (S, S') ∈ state_wl_l_init ∧ (T, T') ∈ state_wl_l_init ∧ init_dt_spec C S' T')› lemma init_dt_wl_init_dt_wl_spec: assumes ‹init_dt_wl_pre CS S› shows ‹init_dt_wl CS S ≤ SPEC (init_dt_wl_spec CS S)› proof - obtain S' where SS': ‹(S, S') ∈ state_wl_l_init› and pre: ‹init_dt_pre CS S'› using assms unfolding init_dt_wl_pre_def by blast show ?thesis apply (rule order.trans) apply (rule init_dt_wl_init_dt[OF SS']) apply (rule order.trans) apply (rule ref_two_step') apply (rule init_dt_full[OF pre]) apply (unfold conc_fun_SPEC) apply (rule SPEC_rule) apply normalize_goal+ using SS' pre unfolding init_dt_wl_spec_def by blast qed fun correct_watching_init :: ‹'v twl_st_wl ⇒ bool› where [simp del]: ‹correct_watching_init (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ⟷ all_blits_are_in_problem_init (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ∧ (∀L. distinct_watched (W L) ∧ (∀(i, K, b)∈#mset (W L). i ∈# dom_m N ∧ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)) ∧ fst `# mset (W L) = clause_to_update L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}))› lemma correct_watching_init_correct_watching: ‹correct_watching_init T ⟹ correct_watching T› by (cases T) (fastforce simp: correct_watching.simps correct_watching_init.simps filter_mset_eq_conv all_blits_are_in_problem_init.simps in_clause_to_update_in_dom_mD) lemma image_mset_Suc: ‹Suc `# {#C ∈# M. P C#} = {#C ∈# Suc `# M. P (C-1)#}› by (induction M) auto lemma correct_watching_init_add_unit: assumes ‹correct_watching_init (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› shows ‹correct_watching_init (M, N, D, add_mset C NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› proof - have [intro!]: ‹(a, x) ∈ set (W L) ⟹ a ∈# dom_m N ⟹ b ∈ set (N ∝a) ⟹ b ∉# all_lits_of_mm {#mset (fst x). x ∈# ran_m N#} ⟹ b ∈# all_lits_of_mm NE› for x b F a L unfolding ran_m_def by (auto dest!: multi_member_split simp: all_lits_of_mm_add_mset in_clause_in_all_lits_of_m) show ?thesis using assms unfolding correct_watching_init.simps clause_to_update_def Ball_def by (fastforce simp: correct_watching.simps all_lits_of_mm_add_mset all_lits_of_m_add_mset Ball_def all_conj_distrib clause_to_update_def all_blits_are_in_problem_init.simps all_lits_of_mm_union dest!: ) qed lemma correct_watching_init_propagate: ‹correct_watching_init ((L # M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) ⟷ correct_watching_init ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))› ‹correct_watching_init ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, add_mset C Q, W)) ⟷ correct_watching_init ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))› unfolding correct_watching_init.simps clause_to_update_def Ball_def by (auto simp: correct_watching.simps all_lits_of_mm_add_mset all_lits_of_m_add_mset Ball_def all_conj_distrib clause_to_update_def all_blits_are_in_problem_init.simps) lemma all_blits_are_in_problem_cons[simp]: ‹all_blits_are_in_problem_init (Propagated L i # a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b) ⟷ all_blits_are_in_problem_init (a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)› ‹all_blits_are_in_problem_init (Decided L # a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b) ⟷ all_blits_are_in_problem_init (a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)› ‹all_blits_are_in_problem_init (a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, add_mset L ae, b) ⟷ all_blits_are_in_problem_init (a, aa, ab, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)› ‹NO_MATCH None y ⟹ all_blits_are_in_problem_init (a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b) ⟷ all_blits_are_in_problem_init (a, aa, None, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)› ‹NO_MATCH {#} ae ⟹ all_blits_are_in_problem_init (a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b) ⟷ all_blits_are_in_problem_init (a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, {#}, b)› by (auto simp: all_blits_are_in_problem_init.simps) lemma correct_watching_init_cons[simp]: ‹NO_MATCH None y ⟹ correct_watching_init ((a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)) ⟷ correct_watching_init ((a, aa, None, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b))› ‹NO_MATCH {#} ae ⟹ correct_watching_init ((a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, ae, b)) ⟷ correct_watching_init ((a, aa, y, ac, ad, NEk, UEk, NS, US, N0, U0, {#}, b))› apply (auto simp: correct_watching_init.simps clause_to_update_def) apply (subst (asm) all_blits_are_in_problem_cons(4)) apply auto apply (subst all_blits_are_in_problem_cons(4)) apply auto apply (subst (asm) all_blits_are_in_problem_cons(5)) apply auto apply (subst all_blits_are_in_problem_cons(5)) apply auto done lemma clause_to_update_mapsto_upd_notin: assumes i: ‹i ∉# dom_m N› shows ‹clause_to_update L (M, N(i ↪ C'), C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = (if L ∈ set (watched_l C') then add_mset i (clause_to_update L (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)) else (clause_to_update L (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)))› ‹clause_to_update L (M, fmupd i (C', b) N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = (if L ∈ set (watched_l C') then add_mset i (clause_to_update L (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)) else (clause_to_update L (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)))› using assms by (auto simp: clause_to_update_def intro!: filter_mset_cong) lemma correct_watching_init_add_clause: assumes corr: ‹correct_watching_init ((a, aa, None, ac, ad, NEk, UEk, NS, US, N0, U0, Q, b))› and leC: ‹2 ≤ length C› and i_notin[simp]: ‹i ∉# dom_m aa› and dist[iff]: ‹C ! 0 ≠ C ! Suc 0› shows ‹correct_watching_init ((a, fmupd i (C, red) aa, None, ac, ad, NEk, UEk, NS, US, N0, U0, Q, b (C ! 0 := b (C ! 0) @ [(i, C ! Suc 0, length C = 2)], C ! Suc 0 := b (C ! Suc 0) @ [(i, C ! 0, length C = 2)])))› proof - have [iff]: ‹C ! Suc 0 ≠ C ! 0› using ‹C ! 0 ≠ C ! Suc 0› by argo have [iff]: ‹C ! Suc 0 ∈# all_lits_of_m (mset C)› ‹C ! 0 ∈# all_lits_of_m (mset C)› ‹C ! Suc 0 ∈ set C› ‹ C ! 0 ∈ set C› ‹C ! 0 ∈ set (watched_l C)› ‹C ! Suc 0 ∈ set (watched_l C)› using leC by (force intro!: in_clause_in_all_lits_of_m nth_mem simp: in_set_conv_iff intro: exI[of _ 0] exI[of _ ‹Suc 0›])+ have [dest!]: ‹⋀L. L ≠ C ! 0 ⟹ L ≠ C ! Suc 0 ⟹ L ∈ set (watched_l C) ⟹ False› by (cases C; cases ‹tl C›; auto)+ have i: ‹i ∉ fst ` set (b L)› for L using corr i_notin unfolding correct_watching_init.simps by force have [iff]: ‹(i,c, d) ∉ set (b L)› for L c d using i[of L] by (auto simp: image_iff) then show ?thesis using corr by (force simp: correct_watching_init.simps all_blits_are_in_problem_init.simps ran_m_mapsto_upd_notin all_lits_of_mm_add_mset all_lits_of_mm_union clause_to_update_mapsto_upd_notin correctly_marked_as_binary.simps split: if_splits) qed definition rewatch :: ‹'v clauses_l ⇒ ('v literal ⇒ 'v watched) ⇒ ('v literal ⇒ 'v watched) nres› where ‹rewatch N W = do { xs ← SPEC(λxs. set_mset (dom_m N) ⊆ set xs ∧ distinct xs); nfoldli xs (λ_. True) (λi W. do { if i ∈# dom_m N then do { ASSERT(i ∈# dom_m N); ASSERT(length (N ∝ i) ≥ 2); let L1 = N ∝ i ! 0; let L2 = N ∝ i ! 1; let n = length (N ∝ i); let b = (n = 2); ASSERT(L1 ≠ L2); ASSERT(length (W L1) < size (dom_m N)); let W = W(L1 := W L1 @ [(i, L2, b)]); ASSERT(length (W L2) < size (dom_m N)); let W = W(L2 := W L2 @ [(i, L1, b)]); RETURN W } else RETURN W }) W }› lemma rewatch_correctness: assumes [simp]: ‹W = (λ_. [])› and H[dest]: ‹⋀x. x ∈# dom_m N ⟹ distinct (N ∝ x) ∧ length (N ∝ x) ≥ 2› shows ‹rewatch N W ≤ SPEC(λW. correct_watching_init (M, N, C, NE, UE, NEk, UEk, NS, US, N₀, U₀, Q, W))› proof - define I where ‹I ≡ λ(a :: nat list) (b :: nat list) W. correct_watching_init ((M, fmrestrict_set (set a) N, C, NE, UE, NEk, UEk, NS, US, N₀, U₀, Q, W))› have I0: ‹set_mset (dom_m N) ⊆ set x ∧ distinct x ⟹ I [] x W› for x unfolding I_def by (auto simp: correct_watching_init.simps all_blits_are_in_problem_init.simps clause_to_update_def) have le: ‹length (σ L) < size (dom_m N)› if ‹correct_watching_init (M, fmrestrict_set (set l1) N, C, NE, UE, NEk, UEk, NS, US, N₀, U₀, Q, σ)› and ‹set_mset (dom_m N) ⊆ set x ∧ distinct x› and ‹x = l1 @ xa # l2› ‹xa ∈# dom_m N› for L l1 σ xa l2 x proof - have 1: ‹card (set l1) ≤ length l1› by (auto simp: card_length) have ‹distinct_watched (σ L)› and ‹fst ` set (σ L) ⊆ set l1 ∩ set_mset (dom_m N)› using that by (fastforce simp: correct_watching_init.simps dom_m_fmrestrict_set')+ then have ‹length (map fst (σ L)) ≤ card (set l1 ∩ set_mset (dom_m N))› using 1 by (subst distinct_card[symmetric]) (auto simp: distinct_watched_alt_def intro!: card_mono intro: order_trans) also have ‹... < card (set_mset (dom_m N))› using that by (auto intro!: psubset_card_mono) also have ‹... = size (dom_m N)› by (simp add: distinct_mset_dom distinct_mset_size_eq_card) finally show ?thesis by simp qed show ?thesis unfolding rewatch_def apply (subst (3) Let_def) apply (refine_vcg nfoldli_rule[where I = ‹I›]) subgoal by (rule I0) subgoal using assms unfolding I_def by auto subgoal for x xa l1 l2 σ using H[of xa] unfolding I_def apply - by (rule, subst (asm)nth_eq_iff_index_eq) linarith+ subgoal for x xa l1 l2 σ unfolding I_def by (rule le) subgoal for x xa l1 l2 σ unfolding I_def by (drule le[where L = ‹N ∝ xa ! 1›]) (auto simp: I_def dest!: le) subgoal for x xa l1 l2 σ unfolding I_def by (cases ‹the (fmlookup N xa)›) (auto simp: dom_m_fmrestrict_set' intro!: correct_watching_init_add_clause) subgoal unfolding I_def by auto subgoal by auto subgoal unfolding I_def by (auto simp: fmlookup_restrict_set_id') done qed definition state_wl_l_init_full :: ‹('v twl_st_wl_init_full × 'v twl_st_l_init) set› where ‹state_wl_l_init_full = {(S, S'). (fst S, fst S') ∈ state_wl_l None ∧ snd S = snd S'}› definition added_only_watched :: ‹('v twl_st_wl_init_full × 'v twl_st_wl_init) set› where ‹added_only_watched = {(((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W), OC), ((M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q'), OC')). (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q) = (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q') ∧ OC = OC'}› definition init_dt_wl_spec_full :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init_full ⇒ bool› where ‹init_dt_wl_spec_full C S T'' ⟷ (∃S' T T'. (S, S') ∈ state_wl_l_init ∧ (T :: 'v twl_st_wl_init, T') ∈ state_wl_l_init ∧ init_dt_spec C S' T' ∧ correct_watching_init (fst T'') ∧ (T'', T) ∈ added_only_watched)› definition init_dt_wl_full :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init_full nres› where ‹init_dt_wl_full CS S = do{ ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC) ← init_dt_wl CS S; W ← rewatch N (λ_. []); RETURN ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W), OC) }› lemma init_dt_wl_spec_rewatch_pre: assumes ‹init_dt_wl_spec CS S T› and ‹N = get_clauses_init_wl T› and ‹C ∈# dom_m N› shows ‹distinct (N ∝ C) ∧ length (N ∝ C) ≥ 2› proof - obtain x xa xb where ‹N = get_clauses_init_wl T› and Sx: ‹(S, x) ∈ state_wl_l_init› and Txa: ‹(T, xa) ∈ state_wl_l_init› and xa_xb: ‹(xa, xb) ∈ twl_st_l_init› and struct_invs: ‹twl_struct_invs_init xb› and ‹clauses_to_update_l_init xa = {#}› and ‹∀s∈set (get_trail_l_init xa). ¬ is_decided s› and ‹get_conflict_l_init xa = None ⟶ literals_to_update_l_init xa = uminus `# lit_of `# mset (get_trail_l_init xa)› and ‹remdups_mset `# mset `# mset CS + mset `# ran_mf (get_clauses_l_init x) + other_clauses_l_init x + get_unit_clauses_l_init x + get_subsumed_init_clauses_l_init x + get_init_clauses0_l_init x = mset `# ran_mf (get_clauses_l_init xa) + other_clauses_l_init xa + get_unit_clauses_l_init xa + get_subsumed_init_clauses_l_init xa + get_init_clauses0_l_init xa› and ‹learned_clss_lf (get_clauses_l_init x) = learned_clss_lf (get_clauses_l_init xa)› and ‹get_learned_unit_clauses_l_init xa = get_learned_unit_clauses_l_init x› and ‹get_subsumed_learned_clauses_l_init xa = get_subsumed_learned_clauses_l_init x› ‹get_learned_clauses0_l_init xa = get_learned_clauses0_l_init x› ‹twl_list_invs (fst xa)› and ‹twl_stgy_invs (fst xb)› and ‹other_clauses_l_init xa ≠ {#} ⟶ get_conflict_l_init xa ≠ None› and ‹{#} ∈# mset `# mset CS ⟶ get_conflict_l_init xa ≠ None› and ‹get_conflict_l_init x ≠ None ⟶ get_conflict_l_init x = get_conflict_l_init xa› using assms unfolding init_dt_wl_spec_def init_dt_spec_def apply - by normalize_goal+ presburger have ‹twl_st_inv (fst xb)› using struct_invs unfolding twl_struct_invs_init_def by fast then have ‹Multiset.Ball (get_clauses (fst xb)) struct_wf_twl_cls› by (cases xb) (auto simp: twl_st_inv.simps) with ‹C ∈# dom_m N› show ?thesis using Txa xa_xb assms by (cases T; cases ‹fmlookup N C›; cases ‹snd (the(fmlookup N C))›) (auto simp: state_wl_l_init_def twl_st_l_init_def conj_disj_distribR Collect_disj_eq Collect_conv_if mset_take_mset_drop_mset' state_wl_l_init'_def ran_m_def dest!: multi_member_split) qed lemma init_dt_wl_full_init_dt_wl_spec_full: assumes ‹init_dt_wl_pre CS S› shows ‹init_dt_wl_full CS S ≤ SPEC (init_dt_wl_spec_full CS S)› proof - show ?thesis unfolding init_dt_wl_full_def apply (rule specify_left) apply (rule init_dt_wl_init_dt_wl_spec) subgoal by (rule assms) apply clarify apply (rule specify_left) apply (rule_tac M =a and N=aa and C=ab and NE=ac and UE=ad and Q=b and NEk=ae and UEk = af and NS=ag and US=ah and N₀=ai and U₀=aj in rewatch_correctness[OF _ init_dt_wl_spec_rewatch_pre]) subgoal by simp apply assumption subgoal by simp subgoal by simp subgoal for a aa ab ac ad ae af ag ah b ba W using assms unfolding init_dt_wl_spec_full_def init_dt_wl_pre_def init_dt_wl_spec_def by (auto simp: added_only_watched_def state_wl_l_init_def state_wl_l_init'_def) done qed end

Theory Watched_Literals_Watch_List_Initialisation