Theory IsaSAT_Occurence

theory IsaSAT_Occurence_List imports IsaSAT_Literals IsaSAT_Watch_List IsaSAT_Mark begin section ‹Occurrence lists› text ‹ Occurrence lists (in a single watched way) are very similar to watch lists. For simplification purpose, we use occurrence lists and watch lists, but Kissat uses only the latter for memory efficiency. This file started as an experiment. We attempted to do better than our watch lists because we know and understand a lot more on refinement. This turned out to do really work out as expected however. There are two ways to achieve the refinement: ▪ the most abstract requires to know the set of variable. Which means that we have to somehow get it. Which is impossible (some of the information is deleted anyway), but also something we probably should not try to do. ▪ just use a bound. What is the conclusion of all that? Well not much, except that full abstraction is hard to get. So we still end up with the concrete data in the isasat state, which I find sad, but I don't see any way to do it better -- and no I am no going back to a locale with an upper bound on the literals; been there, done that. › subsection ‹Abstract Occurrence Lists› type_synonym raw_occurences = ‹nat literal ⇒ nat list› type_synonym occurences = ‹nat set × raw_occurences› definition valid_occurrences where ‹valid_occurrences ℬ = (λ(𝒜, xs). set_mset ℬ = 𝒜)› text ‹Only useful for proofs.› definition occ_list :: ‹occurences ⇒ nat literal ⇒ nat list› where ‹occ_list = (λ(𝒜, xs) L. xs L)› definition occ_list_at :: ‹occurences ⇒ nat literal ⇒ nat ⇒ nat› where ‹occ_list_at 𝒜xs L i = occ_list 𝒜xs L ! i› definition occ_list_at_pre :: ‹occurences ⇒ nat literal ⇒ nat ⇒ bool› where ‹occ_list_at_pre = (λ(n, xs) L i. atm_of L ∈ n ∧ i < length (xs L))› definition mop_occ_list_at :: ‹occurences ⇒ nat literal ⇒ nat ⇒ nat nres› where ‹mop_occ_list_at = (λ𝒜xs L i. do { ASSERT (occ_list_at_pre 𝒜xs L i); RETURN (occ_list_at 𝒜xs L i) })› definition occ_list_length_pre :: ‹occurences ⇒ nat literal ⇒ bool› where ‹occ_list_length_pre = (λ(𝒜, xs) L. atm_of L ∈ 𝒜)› definition occ_list_length :: ‹occurences ⇒ nat literal ⇒ nat› where ‹occ_list_length = (λ(𝒜, xs) L. do { (length (xs L)) })› definition mop_occ_list_length :: ‹occurences ⇒ nat literal ⇒ nat nres› where ‹mop_occ_list_length = (λ𝒜xs L. do { ASSERT (occ_list_length_pre 𝒜xs L); RETURN (occ_list_length 𝒜xs L) })› definition occ_list_append_pre :: ‹occurences ⇒ nat literal ⇒ bool› where ‹occ_list_append_pre = (λ(𝒜, xs) L. atm_of L ∈ 𝒜)› definition occ_list_append :: ‹nat ⇒ occurences ⇒ nat literal ⇒ occurences› where ‹occ_list_append = (λx (𝒜, xs) L. (𝒜, xs (L := xs L @ [x])))› definition mop_occ_list_append :: ‹nat ⇒ occurences ⇒ nat literal ⇒ occurences nres› where ‹mop_occ_list_append = (λx 𝒜xs L . do { ASSERT (occ_list_append_pre (𝒜xs) L); RETURN (occ_list_append x (𝒜xs) L) })› definition occ_list_clear_at_pre :: ‹occurences ⇒ nat literal ⇒ bool› where ‹occ_list_clear_at_pre = (λ(𝒜, xs) L. atm_of L ∈ 𝒜)› definition occ_list_clear_at :: ‹occurences ⇒ nat literal ⇒ occurences nres› where ‹occ_list_clear_at = (λ(𝒜, xs) L . do { ASSERT (occ_list_clear_at_pre (𝒜, xs) L); RETURN (𝒜, xs (L := [])) })› definition occ_list_clear_all_pre :: ‹occurences ⇒ bool› where ‹occ_list_clear_all_pre = (λ(𝒜, xs). True)› definition occ_list_clear_all :: ‹occurences ⇒ occurences nres› where ‹occ_list_clear_all = (λ(𝒜, xs) . do { ASSERT (occ_list_clear_all_pre (𝒜, xs)); RETURN (𝒜, λ_. []) })› definition all_occurrences :: ‹nat multiset ⇒ occurences ⇒ nat multiset› where ‹all_occurrences 𝒜 = (λ(n, xs). ∑_# (mset `# xs `# Pos `# remdups_mset 𝒜 + mset `# xs `# Neg `# remdups_mset 𝒜))› definition occ_list_create_pre :: ‹nat set ⇒ nat set ⇒ bool› where ‹occ_list_create_pre n = (λ𝒜. True)› definition mop_occ_list_create :: ‹nat set ⇒ occurences nres› where ‹mop_occ_list_create = (λn. do { ASSERT (finite n); RETURN (n, λ_. []) })› abbreviation raw_empty_occs_list :: ‹nat literal ⇒ nat list› where ‹raw_empty_occs_list ≡ (λ_. [])› definition empty_occs_list :: ‹nat multiset ⇒ nat set × (nat literal ⇒ nat list)› where ‹empty_occs_list 𝒜 ≡ (set_mset 𝒜, λ_. [])› lemma empty_occs_list_cong: ‹set_mset A = set_mset B ⟹ empty_occs_list A = empty_occs_list B› unfolding empty_occs_list_def by auto definition occurrence_list where ‹occurrence_list 𝒜 = {((n, ys), xs). (ys, xs)∈Id ∧ n = (set_mset 𝒜)}› lemma mop_occ_list_create: shows ‹mop_occ_list_create (set_mset 𝒜) ≤ SPEC (λc. (c, raw_empty_occs_list) ∈ occurrence_list 𝒜)› (is ‹?A ≤ ?B›) unfolding mop_occ_list_create_def by refine_vcg (use in ‹auto simp: RETURN_RES_refine_iff occurrence_list_def›) lemma mop_occ_list_at: assumes ‹occ_list_at_pre occs L i› shows ‹mop_occ_list_at occs L i ≤ SPEC (λc. (c, occ_list_at occs L i) ∈ Id)› (is ‹?A ≤ ?B›) using assms unfolding mop_occ_list_at_def by refine_vcg auto lemma mop_occ_list_append: assumes ‹occ_list_append_pre occs L› shows ‹mop_occ_list_append x occs L ≤ SPEC (λc. (c, occ_list_append x occs L) ∈ Id)› using assms unfolding mop_occ_list_append_def by refine_vcg auto abbreviation occ_list_append_r :: ‹nat literal ⇒ nat ⇒ (nat literal ⇒ nat list) ⇒ _› where ‹occ_list_append_r L x xs ≡ xs (L := xs L @ [x])› subsection ‹Concrete Occurrence lists› text ‹We use text‹cocc› for concrete occurrence lists.› type_synonym occurences_ref = ‹nat list list› abbreviation D₁ :: ‹nat set ⇒ (nat × nat literal) set› where ‹D₁ 𝒜_i_n ≡ (λL. (nat_of_lit L, L)) ` (Pos ` 𝒜_i_n ∪ Neg ` 𝒜_i_n)› definition occurrence_list_ref :: ‹(occurences_ref × occurences) set› where ‹occurrence_list_ref ≡ {(xs, (n, ys)). (xs, ys)∈⟨⟨nat_rel⟩list_rel⟩map_fun_rel (D₁ n) ∧ (∀L. L ∉ fst ` (D₁ n) ⟶ L < length xs ⟶ xs ! L = [])}› lemma empty_occs_list_cong': ‹set_mset A = set_mset B ⟹ (occs, empty_occs_list A) ∈ occurrence_list_ref ⟹ (occs, empty_occs_list B) ∈ occurrence_list_ref› unfolding empty_occs_list_def by auto definition cocc_list_at :: ‹occurences_ref ⇒ nat literal ⇒ nat ⇒ nat› where ‹cocc_list_at xs L i = xs ! nat_of_lit L ! i› definition cocc_list_at_pre :: ‹occurences_ref ⇒ nat literal ⇒ nat ⇒ bool› where ‹cocc_list_at_pre = (λxs L i. i < length (xs ! nat_of_lit L) ∧ nat_of_lit L < length xs)› definition mop_cocc_list_at :: ‹occurences_ref ⇒ nat literal ⇒ nat ⇒ nat nres› where ‹mop_cocc_list_at = (λ𝒜xs L i. do { ASSERT (cocc_list_at_pre 𝒜xs L i); RETURN (cocc_list_at 𝒜xs L i) })› (*TODO this is certainly a dup*) lemma ℒ_a_l_l_add_mset: ‹set_mset (ℒ_a_l_l (add_mset K A)) = set_mset (ℒ_a_l_l A) ∪ {Pos K, Neg K}› by (auto simp: ℒ_a_l_l_def) lemma mop_cocc_list_at_mop_occ_list_at: assumes ‹(xs, 𝒜xs) ∈ occurrence_list_ref› ‹(L,L')∈Id› ‹(i,i')∈nat_rel› shows ‹mop_cocc_list_at xs L i ≤ ⇓{(K,K'). (K,K')∈nat_rel ∧ K = occ_list_at 𝒜xs L' i ∧ K = cocc_list_at xs L' i ∧ nat_of_lit L' < length xs ∧ i < length (xs ! nat_of_lit L)} (mop_occ_list_at 𝒜xs L' i')› using assms unfolding mop_cocc_list_at_def mop_occ_list_at_def occurrence_list_ref_def apply refine_rcg subgoal by (cases L) (auto simp: cocc_list_at_pre_def occ_list_at_pre_def ℒ_a_l_l_add_mset map_fun_rel_def dest: bspec[of _ _ L]) subgoal by (cases L) (auto simp: cocc_list_at_pre_def occ_list_at_pre_def ℒ_a_l_l_add_mset cocc_list_at_def occ_list_at_def map_fun_rel_def occ_list_def dest: bspec[of _ _ L]) done definition cocc_list_length_pre :: ‹occurences_ref ⇒ nat literal ⇒ bool› where ‹cocc_list_length_pre = (λ(xs) L. nat_of_lit L < length xs)› definition cocc_list_length :: ‹occurences_ref ⇒ nat literal ⇒ nat› where ‹cocc_list_length = (λxs L. do { (length (xs ! nat_of_lit L)) })› definition mop_cocc_list_length :: ‹occurences_ref ⇒ nat literal ⇒ nat nres› where ‹mop_cocc_list_length = (λ𝒜xs L. do { ASSERT (cocc_list_length_pre 𝒜xs L); RETURN (cocc_list_length 𝒜xs L) })› lemma mop_cocc_list_length_mop_occ_list_length: assumes ‹(xs, 𝒜xs) ∈ occurrence_list_ref› ‹(L,L')∈Id› shows ‹mop_cocc_list_length xs L ≤ ⇓nat_rel (mop_occ_list_length 𝒜xs L')› using assms unfolding mop_cocc_list_length_def mop_occ_list_length_def occurrence_list_ref_def apply refine_vcg subgoal by (cases L) (auto simp: occ_list_length_pre_def cocc_list_length_pre_def ℒ_a_l_l_add_mset map_fun_rel_def dest!: multi_member_split) subgoal by (cases L) (auto simp: occ_list_length_pre_def cocc_list_length_pre_def ℒ_a_l_l_add_mset map_fun_rel_def occ_list_length_def cocc_list_length_def dest: bspec[of _ _ L]) done definition cocc_list_append_pre :: ‹occurences_ref ⇒ nat literal ⇒ bool› where ‹cocc_list_append_pre = (λxs L. nat_of_lit L < length xs)› definition cocc_list_append :: ‹nat ⇒ occurences_ref ⇒ nat literal ⇒ occurences_ref› where ‹cocc_list_append = (λx xs L. xs [nat_of_lit L := xs ! (nat_of_lit L) @ [x]])› definition mop_cocc_list_append :: ‹nat ⇒ occurences_ref ⇒ nat literal ⇒ occurences_ref nres› where ‹mop_cocc_list_append = (λx 𝒜xs L . do { ASSERT (cocc_list_append_pre (𝒜xs) L); RETURN (cocc_list_append x (𝒜xs) L) })› lemma mop_cocc_list_append_mop_occ_list_append: assumes ‹(xs, 𝒜xs) ∈ occurrence_list_ref› ‹(L,L')∈Id› and ‹(x,x')∈nat_rel› shows ‹mop_cocc_list_append x xs L ≤ ⇓{(a,b). (a,b)∈occurrence_list_ref ∧ a = cocc_list_append x xs L ∧ nat_of_lit L < length xs} (mop_occ_list_append x' 𝒜xs L')› using assms unfolding mop_cocc_list_append_def mop_occ_list_append_def occurrence_list_ref_def apply refine_vcg subgoal by (cases L) (auto simp: cocc_list_append_pre_def occ_list_append_pre_def ℒ_a_l_l_add_mset map_fun_rel_def dest!: bspec[of _ _ L]) subgoal apply (cases L) apply (auto simp: cocc_list_append_pre_def occ_list_append_pre_def ℒ_a_l_l_add_mset map_fun_rel_def cocc_list_append_def occ_list_append_def) apply (force simp add: image_image image_Un)+ done done definition mop_cocc_list_create :: ‹nat ⇒ occurences_ref nres› where ‹mop_cocc_list_create = (λn. do { RETURN (replicate n []) })› lemma mop_cocc_list_create_mop_occ_list_create: assumes ‹n > 2* Max 𝒜 + 1› ‹finite 𝒜› shows ‹mop_cocc_list_create n ≤ ⇓(occurrence_list_ref) (mop_occ_list_create 𝒜)› unfolding mop_cocc_list_create_def mop_occ_list_create_def occurrence_list_ref_def using assms by (auto simp: map_fun_rel_def Max_gr_iff dest: Max_ge) definition cocc_list_clear_at_pre :: ‹occurences_ref ⇒ nat literal ⇒ bool› where ‹cocc_list_clear_at_pre = (λ(xs) L. nat_of_lit L < length xs)› definition cocc_list_clear_at :: ‹occurences_ref ⇒ nat literal ⇒ occurences_ref nres› where ‹cocc_list_clear_at = (λxs L . do { ASSERT (cocc_list_clear_at_pre xs L); RETURN (xs [nat_of_lit L := []]) })› lemma cocc_list_clear_at_occ_list_clear_at: assumes ‹(xs, 𝒜xs) ∈ occurrence_list_ref› ‹(L,L')∈Id› shows ‹cocc_list_clear_at xs L ≤ ⇓(occurrence_list_ref) (occ_list_clear_at 𝒜xs L')› using assms unfolding cocc_list_clear_at_def occ_list_clear_at_def case_prod_beta occurrence_list_ref_def apply refine_vcg subgoal by (cases L) (auto simp: cocc_list_clear_at_pre_def occ_list_clear_at_pre_def ℒ_a_l_l_add_mset map_fun_rel_def dest: bspec[of _ _ L]) subgoal by (cases L) (auto simp: cocc_list_append_pre_def occ_list_append_pre_def ℒ_a_l_l_add_mset map_fun_rel_def cocc_list_append_def occ_list_append_def; force)+ done definition cocc_list_clear_all_pre :: ‹occurences_ref ⇒ bool› where ‹cocc_list_clear_all_pre = (λxs. True)› definition cocc_list_clear_all :: ‹occurences_ref ⇒ occurences_ref nres› where ‹cocc_list_clear_all = (λ(xs) . do { ASSERT (cocc_list_clear_all_pre (xs)); RETURN (replicate (length xs) []) })› lemma cocc_list_clear_all_occ_list_clear_all: assumes ‹(xs, 𝒜xs) ∈ occurrence_list_ref› shows ‹cocc_list_clear_all xs ≤ ⇓(occurrence_list_ref) (occ_list_clear_all 𝒜xs)› using assms unfolding cocc_list_clear_all_def occ_list_clear_all_def case_prod_beta occurrence_list_ref_def apply refine_vcg subgoal by (auto simp: cocc_list_clear_all_pre_def occ_list_clear_all_pre_def ℒ_a_l_l_add_mset map_fun_rel_def dest: bspec[of _ _ L]) subgoal by (auto simp: cocc_list_append_pre_def occ_list_append_pre_def ℒ_a_l_l_add_mset map_fun_rel_def cocc_list_append_def occ_list_append_def; force)+ done section ‹Clause Marking› text ‹ Experiment: This should eventually replace the stuff used for the conflicts. Experiment in the current state to see if useful. If it is this should be generalized. However, not clear because distinct, so not really multisets. Experiment: is keeping the set of variables as sets useful? is the refinement from there on okay (both from doing it and also performance wise) › subsection ‹Abstract Representation› type_synonym clause_hash = ‹(nat set × nat clause)› definition clause_hash_ref where ‹clause_hash_ref 𝒜 = {((ℬ, C), D). C = D ∧ set_mset 𝒜 = ℬ ∧ atms_of C ⊆ ℬ}› definition ch_create_pre :: ‹nat set ⇒ bool› where ‹ch_create_pre n = (True)› text ‹The fact that the nat set must be passed as argument is really ugly› definition mop_ch_create :: ‹nat set ⇒ clause_hash nres› where ‹mop_ch_create n = do { ASSERT (ch_create_pre n); RETURN (n, {#}) }› definition ch_add :: ‹nat literal ⇒ clause_hash ⇒ clause_hash› where ‹ch_add L = (λ(𝒜, C). (𝒜, add_mset L C))› definition ch_add_pre :: ‹nat literal ⇒ clause_hash ⇒ bool› where ‹ch_add_pre L = (λ(𝒜, C). atm_of L ∈ 𝒜 ∧ L ∉# C)› definition mop_ch_add :: ‹nat literal ⇒ clause_hash ⇒ clause_hash nres› where ‹mop_ch_add L C = do { ASSERT (ch_add_pre L C); RETURN (ch_add L C) }› definition ch_remove :: ‹nat literal ⇒ clause_hash ⇒ clause_hash› where ‹ch_remove L = (λ(𝒜, C). (𝒜, remove1_mset L C))› definition ch_remove_pre :: ‹nat literal ⇒ clause_hash ⇒ bool› where ‹ch_remove_pre L = (λ(𝒜, C). atm_of L ∈ 𝒜 ∧ L ∈# C)› definition mop_ch_remove :: ‹nat literal ⇒ clause_hash ⇒ clause_hash nres› where ‹mop_ch_remove L C = do { ASSERT (ch_remove_pre L C); RETURN (ch_remove L C) }› definition ch_in :: ‹nat literal ⇒ clause_hash ⇒ bool› where ‹ch_in L = (λ(𝒜, C). L ∈# C)› definition ch_in_pre :: ‹nat literal ⇒ clause_hash ⇒ bool› where ‹ch_in_pre L = (λ(𝒜, C). atm_of L ∈ 𝒜)› definition mop_ch_in :: ‹nat literal ⇒ clause_hash ⇒ bool nres› where ‹mop_ch_in L C = do { ASSERT (ch_in_pre L C); RETURN (ch_in L C) }› definition ch_remove_clause :: ‹nat clause ⇒ clause_hash ⇒ clause_hash› where ‹ch_remove_clause D = (λ(𝒜, C). (𝒜, C - D))› definition ch_remove_clause_pre :: ‹nat clause ⇒ clause_hash ⇒ bool› where ‹ch_remove_clause_pre D = (λ(𝒜, C). D ⊆# C)› definition mop_ch_remove_clause :: ‹nat clause ⇒ clause_hash ⇒ clause_hash nres› where ‹mop_ch_remove_clause L C = do { ASSERT (ch_remove_clause_pre L C); RETURN (ch_remove_clause L C) }› definition ch_remove_all :: ‹clause_hash ⇒ clause_hash› where ‹ch_remove_all = (λ(𝒜, C). (𝒜, {#}))› definition mop_ch_remove_all :: ‹nat clause ⇒ clause_hash ⇒ clause_hash nres› where ‹mop_ch_remove_all D C = do { ASSERT (D = snd C ∧ atm_of ` (set_mset D) ⊆ fst C); RETURN (ch_remove_all C) }› definition ch_add_all :: ‹nat clause ⇒ clause_hash ⇒ clause_hash› where ‹ch_add_all D = (λ(𝒜, C). (𝒜, C + D))› definition ch_add_all_pre :: ‹nat clause ⇒ clause_hash ⇒ bool› where ‹ch_add_all_pre D = (λ(𝒜, C). atms_of D ⊆ 𝒜 ∧ C ∩# D = {#} ∧ distinct_mset D)› definition mop_ch_add_all :: ‹nat clause ⇒ clause_hash ⇒ clause_hash nres› where ‹mop_ch_add_all L C = do { ASSERT (ch_add_all_pre L C); RETURN (ch_add_all L C) }› lemma mop_ch_create: shows ‹mop_ch_create (set_mset 𝒜) ≤ SPEC (λc. (c, {#}) ∈ clause_hash_ref 𝒜)› (is ‹?A ≤ ?B›) unfolding mop_ch_create_def by refine_vcg (auto simp: clause_hash_ref_def ch_create_pre_def RETURN_RES_refine_iff) lemma mop_ch_add: assumes ‹(C, D) ∈ clause_hash_ref 𝒜› and ‹atm_of L ∈# 𝒜› and ‹(L,L')∈Id› ‹L∉#D› shows ‹mop_ch_add L C ≤ SPEC(λc. (c, add_mset L' D) ∈ clause_hash_ref 𝒜)› using assms unfolding mop_ch_add_def apply refine_vcg subgoal unfolding ch_add_pre_def by (auto simp: clause_hash_ref_def) subgoal by (auto simp: clause_hash_ref_def ch_add_def) done lemma mop_ch_add_all: assumes ‹(C, D) ∈ clause_hash_ref 𝒜› and ‹atms_of L ⊆ set_mset 𝒜› and ‹(L,L')∈Id› ‹D ∩# L' = {#}› and ‹distinct_mset L'› shows ‹mop_ch_add_all L C ≤ SPEC(λc. (c, L' + D) ∈ clause_hash_ref 𝒜)› using assms unfolding mop_ch_add_all_def apply refine_vcg subgoal unfolding ch_add_all_pre_def by (auto simp: clause_hash_ref_def) subgoal by (auto simp: clause_hash_ref_def ch_add_all_def) done lemma mop_ch_in: assumes ‹(C, D) ∈ clause_hash_ref 𝒜› and ‹atm_of L ∈# 𝒜› and ‹(L,L')∈Id› shows ‹mop_ch_in L C ≤ SPEC(λc. (c, L' ∈# D) ∈ bool_rel)› using assms unfolding mop_ch_in_def apply refine_vcg subgoal unfolding ch_in_pre_def by (auto simp: clause_hash_ref_def) subgoal by (auto simp: clause_hash_ref_def ch_in_def) done lemma mop_ch_remove: assumes ‹(C, D) ∈ clause_hash_ref 𝒜› and ‹atm_of L ∈# 𝒜› and ‹(L,L')∈Id› ‹L∈#D› shows ‹mop_ch_remove L C ≤ SPEC(λc. (c, remove1_mset L' D) ∈ clause_hash_ref 𝒜)› using assms unfolding mop_ch_remove_def apply refine_vcg subgoal unfolding ch_remove_pre_def by (auto simp: clause_hash_ref_def) subgoal by (auto simp: clause_hash_ref_def ch_remove_def dest: in_atms_of_minusD) done lemma mop_ch_remove_all: assumes ‹(C, D) ∈ clause_hash_ref 𝒜› ‹atm_of ` set_mset D ⊆ set_mset 𝒜› shows ‹mop_ch_remove_all D C ≤ SPEC(λc. (c, {#}) ∈ clause_hash_ref 𝒜)› using assms unfolding mop_ch_remove_all_def apply refine_vcg subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def) subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def) subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def) done subsection ‹Concrete Representation› text ‹ TODO: The mark structure should probably be replaced by our abstract ch-stuff TODO: the alternative version consists in keeping the multiset, but replacing the atoms by the upper bound. This makes it possible to keep the abstraction (kind of). However, it is very clear what would be the difference. › definition clause_hash :: ‹(bool list × clause_hash) set› where ‹clause_hash = {(xs, (𝒜, C)). (∀L ∈ snd ` D₁ 𝒜. xs ! nat_of_lit L ⟷ L ∈# C) ∧ (∀L∈fst ` D₁ 𝒜. L < length xs) ∧ distinct_mset C}› definition mop_cch_create :: ‹nat ⇒ bool list nres› where ‹mop_cch_create n = do { RETURN (replicate n False) }› lemma mop_cch_create_mop_cch_create: assumes ‹∀L∈fst ` D₁ 𝒜. L < n› shows ‹mop_cch_create n ≤ ⇓clause_hash (mop_ch_create 𝒜)› using assms unfolding mop_cch_create_def mop_ch_create_def by refine_vcg (auto simp: clause_hash_def mset_as_position.intros) definition cch_add :: ‹nat literal ⇒ bool list ⇒ bool list› where ‹cch_add L = (λC. C [nat_of_lit L := True])› definition cch_add_pre :: ‹nat literal ⇒ bool list ⇒ bool› where ‹cch_add_pre L = (λC. nat_of_lit L < length C)› definition mop_cch_add :: ‹nat literal ⇒ bool list ⇒ bool list nres› where ‹mop_cch_add L C = do { ASSERT (cch_add_pre L C); RETURN (cch_add L C) }› lemma mop_cch_add_mop_cch_add: assumes ‹(C, D) ∈ clause_hash› and ‹(L,L')∈Id› shows ‹mop_cch_add L C ≤ ⇓ clause_hash (mop_ch_add L' D)› proof - have [iff]: ‹2 * x1 = Suc (2 * xa) ⟷ False› ‹Suc (2 * x1) = 2 * xa ⟷ False› for xa x1 :: nat by presburger+ show ?thesis using assms unfolding mop_cch_add_def mop_ch_add_def clause_hash_def apply refine_rcg subgoal by (cases L) (auto simp: ch_add_pre_def cch_add_pre_def dest: bspec) subgoal by (cases L') (auto simp: cch_add_def ch_add_def cch_add_pre_def ch_add_pre_def intro!: mset_as_position.intros dest: bspec[of _ _ L']) done qed definition cch_remove :: ‹nat literal ⇒ bool list ⇒ bool list› where ‹cch_remove L = (λC. C[nat_of_lit L := False])› definition cch_remove_pre :: ‹nat literal ⇒ bool list ⇒ bool› where ‹cch_remove_pre L = (λC. nat_of_lit L < length C)› definition mop_cch_remove :: ‹nat literal ⇒ bool list ⇒ bool list nres› where ‹mop_cch_remove L C = do { ASSERT (cch_remove_pre L C); RETURN (cch_remove L C) }› lemma mop_cch_remove_mop_ch_remove: assumes ‹(C, D) ∈ clause_hash› and ‹(L,L')∈Id› shows ‹mop_cch_remove L C ≤ ⇓ clause_hash (mop_ch_remove L' D)› proof - have [iff]: ‹2 * x1 = Suc (2 * xa) ⟷ False› ‹Suc (2 * x1) = 2 * xa ⟷ False› for xa x1 :: nat by presburger+ show ?thesis using assms unfolding mop_cch_remove_def mop_ch_remove_def clause_hash_def apply refine_rcg subgoal by (cases L) (auto simp: ch_remove_pre_def cch_remove_pre_def dest: bspec) subgoal by (cases L') (auto simp: cch_remove_def ch_remove_def cch_remove_pre_def ch_remove_pre_def distinct_mset_remove1_All intro!: mset_as_position.intros dest: bspec[of _ _ L']) done qed definition cch_in :: ‹nat literal ⇒ bool list ⇒ bool› where ‹cch_in L = (λC. C ! nat_of_lit L)› definition cch_in_pre :: ‹nat literal ⇒ bool list ⇒ bool› where ‹cch_in_pre L = (λC. nat_of_lit L < length C)› definition mop_cch_in :: ‹nat literal ⇒ bool list ⇒ bool nres› where ‹mop_cch_in L C = do { ASSERT (cch_in_pre L C); RETURN (cch_in L C) }› lemma mop_cch_in_mop_ch_in: assumes ‹(C, D) ∈ clause_hash› and ‹(L,L')∈Id› shows ‹mop_cch_in L C ≤ ⇓ bool_rel (mop_ch_in L' D)› proof - have [iff]: ‹2 * x1 = Suc (2 * xa) ⟷ False› ‹Suc (2 * x1) = 2 * xa ⟷ False› for xa x1 :: nat by presburger+ show ?thesis using assms unfolding mop_cch_in_def mop_ch_in_def clause_hash_def apply refine_rcg subgoal by (cases L) (auto simp: ch_in_pre_def cch_in_pre_def dest: bspec) subgoal by (cases L') (auto simp: cch_in_def ch_in_def cch_in_pre_def ch_in_pre_def intro!: mset_as_position.intros dest: bspec[of _ _ L']) done qed definition mop_cch_remove_all :: ‹nat clause_l ⇒ bool list ⇒ bool list nres› where ‹mop_cch_remove_all C D = do { (_, D) ← WHILE_T (λ(i, D). i < length C) (λ(i, D). RETURN (i+1, D[nat_of_lit (C!i) := False])) (0, D); RETURN D }› abbreviation cocc_content :: ‹nat list list ⇒ nat multiset› where ‹cocc_content coccs ≡ sum_list (map mset coccs)› definition cocc_content_set :: ‹nat list list ⇒ nat set› where ‹cocc_content_set coccs ≡ ⋃(image set (set coccs))› (*TODO why doesn't that come from subset_mset.sum_list_update?*) lemma sum_list_update_mset: "k < size xs ⟹ sum_list (xs[k := x]) = sum_list xs + x - xs ! k" for xs :: ‹'a multiset list› unfolding sum_mset_sum_list[symmetric] apply (subst mset_update, assumption) apply (auto simp: cancel_comm_monoid_add_class.sum_mset_diff ac_simps) done lemma sum_list_cocc_list_append[simp]: ‹nat_of_lit La < length coccs ⟹ sum_list (map mset (cocc_list_append C coccs La)) = add_mset C (sum_list (map mset coccs))› apply (auto simp: cocc_list_append_def map_update sum_list_update sum_list_update_mset) done lemma cocc_content_set_append[simp]: ‹nat_of_lit La < length coccs ⟹ cocc_content_set (cocc_list_append C coccs La) = insert C (cocc_content_set coccs)› apply (simp only: cocc_content_set_def cocc_list_append_def in_set_upd_eq) apply auto apply (smt (verit, ccfv_threshold) in_set_conv_nth in_set_upd_cases length_Suc_rev_conv nat_neq_iff not_less_eq nth_append_first nth_append_length nth_mem) unfolding Bex_def apply (subst in_set_upd_eq, simp) apply (metis in_set_conv_nth length_Suc_rev_conv nat_in_between_eq(1) nth_append_length) by (smt (verit, best) in_set_conv_nth le_imp_less_Suc length_Suc_rev_conv length_list_update less_imp_le_nat list_update_append1 list_update_id nth_list_update_neq set_update_memI) lemma all_occurrences_add_mset: ‹all_occurrences (add_mset (atm_of L) A) occs = all_occurrences (removeAll_mset (atm_of L) A) occs + mset (occ_list occs L) + mset (occ_list occs (-L))› by (cases L; cases occs) (auto simp: all_occurrences_def occ_list_def remdups_mset_removeAll remdups_mset_singleton_removeAll removeAll_notin simp del: remdups_mset_singleton_sum) lemma all_occurrences_add_mset2: ‹all_occurrences (add_mset (L) A) occs = all_occurrences (removeAll_mset (L) A) occs + mset (occ_list occs (Pos L)) + mset (occ_list occs (Neg L))› by (cases occs) (auto simp: all_occurrences_def occ_list_def remdups_mset_removeAll remdups_mset_singleton_removeAll removeAll_notin simp del: remdups_mset_singleton_sum) lemma all_occurrences_insert_lit: ‹all_occurrences A (insert (atm_of L) B, occs) = all_occurrences (A) (B, occs)› and all_occurrences_occ_list_append_r: ‹all_occurrences (removeAll_mset (atm_of L) A) (B, occ_list_append_r L C b) = all_occurrences (removeAll_mset (atm_of L) A) (B, b)› apply (auto simp: all_occurrences_def) by (smt (verit) distinct_mset_remdups_mset distinct_mset_remove1_All image_mset_cong2 literal.sel(1) literal.sel(2) remdups_mset_removeAll removeAll_subseteq_remove1_mset subset_mset_removeAll_iff) end

Theory IsaSAT_Occurence_List