section ‹Partial Annotated Herbrand Interpretation›
text ‹We here define decided literals (that will be used in both DPLL and CDCL) and the entailment
corresponding to it.›
theory Partial_Annotated_Herbrand_Interpretation
imports
Partial_Herbrand_Interpretation
begin
subsection ‹Decided Literals›
subsubsection ‹Definition›
datatype ('v, 'w, 'mark) annotated_lit =
is_decided: Decided (lit_dec: 'v) |
is_proped: Propagated (lit_prop: 'w) (mark_of: 'mark)
type_synonym ('v, 'w, 'mark) annotated_lits = ‹('v, 'w, 'mark) annotated_lit list›
type_synonym ('v, 'mark) ann_lit = ‹('v literal, 'v literal, 'mark) annotated_lit›
lemma ann_lit_list_induct[case_names Nil Decided Propagated]:
assumes
‹P []› and
‹⋀L xs. P xs ⟹ P (Decided L # xs)› and
‹⋀L m xs. P xs ⟹ P (Propagated L m # xs)›
shows ‹P xs›
using assms apply (induction xs, simp)
by (rename_tac a xs, case_tac a) auto
lemma is_decided_ex_Decided:
‹is_decided L ⟹ (⋀K. L = Decided K ⟹ P) ⟹ P›
by (cases L) auto
lemma is_propedE: ‹is_proped L ⟹ (⋀K C. L = Propagated K C ⟹ P) ⟹ P›
by (cases L) auto
lemma is_decided_no_proped_iff: ‹is_decided L ⟷ ¬is_proped L›
by (cases L) auto
lemma not_is_decidedE:
‹¬is_decided E ⟹ (⋀K C. E = Propagated K C ⟹ thesis) ⟹ thesis›
by (cases E) auto
type_synonym ('v, 'm) ann_lits = ‹('v, 'm) ann_lit list›
fun lit_of :: ‹('a, 'a, 'mark) annotated_lit ⇒ 'a› where
‹lit_of (Decided L) = L› |
‹lit_of (Propagated L _) = L›
definition lits_of :: ‹('a, 'b) ann_lit set ⇒ 'a literal set› where
‹lits_of Ls = lit_of ` Ls›
abbreviation lits_of_l :: ‹('a, 'b) ann_lits ⇒ 'a literal set› where
‹lits_of_l Ls ≡ lits_of (set Ls)›
lemma lits_of_l_empty[simp]:
‹lits_of {} = {}›
unfolding lits_of_def by auto
lemma lits_of_insert[simp]:
‹lits_of (insert L Ls) = insert (lit_of L) (lits_of Ls)›
unfolding lits_of_def by auto
lemma lits_of_l_Un[simp]:
‹lits_of (l ∪ l') = lits_of l ∪ lits_of l'›
unfolding lits_of_def by auto
lemma finite_lits_of_def[simp]:
‹finite (lits_of_l L)›
unfolding lits_of_def by auto
abbreviation unmark where
‹unmark ≡ (λa. {#lit_of a#})›
abbreviation unmark_s where
‹unmark_s M ≡ unmark ` M›
abbreviation unmark_l where
‹unmark_l M ≡ unmark_s (set M)›
lemma atms_of_ms_lambda_lit_of_is_atm_of_lit_of[simp]:
‹atms_of_ms (unmark_l M') = atm_of ` lits_of_l M'›
unfolding atms_of_ms_def lits_of_def by auto
lemma lits_of_l_empty_is_empty[iff]:
‹lits_of_l M = {} ⟷ M = []›
by (induct M) (auto simp: lits_of_def)
lemma in_unmark_l_in_lits_of_l_iff: ‹{#L#} ∈ unmark_l M ⟷ L ∈ lits_of_l M›
by (induction M) auto
lemma atm_lit_of_set_lits_of_l:
"(λl. atm_of (lit_of l)) ` set xs = atm_of ` lits_of_l xs"
unfolding lits_of_def by auto
subsubsection ‹Entailment›
definition true_annot :: ‹('a, 'm) ann_lits ⇒ 'a clause ⇒ bool› (infix "⊨a" 49) where
‹I ⊨a C ⟷ (lits_of_l I) ⊨ C›
definition true_annots :: ‹('a, 'm) ann_lits ⇒ 'a clause_set ⇒ bool› (infix "⊨as" 49) where
‹I ⊨as CC ⟷ (∀C ∈ CC. I ⊨a C)›
lemma true_annot_empty_model[simp]:
‹¬[] ⊨a ψ›
unfolding true_annot_def true_cls_def by simp
lemma true_annot_empty[simp]:
‹¬I ⊨a {#}›
unfolding true_annot_def true_cls_def by simp
lemma empty_true_annots_def[iff]:
‹[] ⊨as ψ ⟷ ψ = {}›
unfolding true_annots_def by auto
lemma true_annots_empty[simp]:
‹I ⊨as {}›
unfolding true_annots_def by auto
lemma true_annots_single_true_annot[iff]:
‹I ⊨as {C} ⟷ I ⊨a C›
unfolding true_annots_def by auto
lemma true_annot_insert_l[simp]:
‹M ⊨a A ⟹ L # M ⊨a A›
unfolding true_annot_def by auto
lemma true_annots_insert_l [simp]:
‹M ⊨as A ⟹ L # M ⊨as A›
unfolding true_annots_def by auto
lemma true_annots_union[iff]:
‹M ⊨as A ∪ B ⟷ (M ⊨as A ∧ M ⊨as B)›
unfolding true_annots_def by auto
lemma true_annots_insert[iff]:
‹M ⊨as insert a A ⟷ (M ⊨a a ∧ M ⊨as A)›
unfolding true_annots_def by auto
lemma true_annot_append_l:
‹M ⊨a A ⟹ M' @ M ⊨a A›
unfolding true_annot_def by auto
lemma true_annots_append_l:
‹M ⊨as A ⟹ M' @ M ⊨as A›
unfolding true_annots_def by (auto simp: true_annot_append_l)
text ‹Link between ‹⊨as› and ‹⊨s›:›
lemma true_annots_true_cls:
‹I ⊨as CC ⟷ lits_of_l I ⊨s CC›
unfolding true_annots_def Ball_def true_annot_def true_clss_def by auto
lemma in_lit_of_true_annot:
‹a ∈ lits_of_l M ⟷ M ⊨a {#a#}›
unfolding true_annot_def lits_of_def by auto
lemma true_annot_lit_of_notin_skip:
‹L # M ⊨a A ⟹ lit_of L ∉# A ⟹ M ⊨a A›
unfolding true_annot_def true_cls_def by auto
lemma true_clss_singleton_lit_of_implies_incl:
‹I ⊨s unmark_l MLs ⟹ lits_of_l MLs ⊆ I›
unfolding true_clss_def lits_of_def by auto
lemma true_annot_true_clss_cls:
‹MLs ⊨a ψ ⟹ set (map unmark MLs) ⊨p ψ›
unfolding true_annot_def true_clss_cls_def true_cls_def
by (auto dest: true_clss_singleton_lit_of_implies_incl)
lemma true_annots_true_clss_cls:
‹MLs ⊨as ψ ⟹ set (map unmark MLs) ⊨ps ψ›
by (auto
dest: true_clss_singleton_lit_of_implies_incl
simp add: true_clss_def true_annots_def true_annot_def lits_of_def true_cls_def
true_clss_clss_def)
lemma true_annots_decided_true_cls[iff]:
‹map Decided M ⊨as N ⟷ set M ⊨s N›
proof -
have *: ‹lit_of ` Decided ` set M = set M› unfolding lits_of_def by force
show ?thesis by (simp add: true_annots_true_cls * lits_of_def)
qed
lemma true_annot_singleton[iff]: ‹M ⊨a {#L#} ⟷ L ∈ lits_of_l M›
unfolding true_annot_def lits_of_def by auto
lemma true_annots_true_clss_clss:
‹A ⊨as Ψ ⟹ unmark_l A ⊨ps Ψ›
unfolding true_clss_clss_def true_annots_def true_clss_def
by (auto dest!: true_clss_singleton_lit_of_implies_incl
simp: lits_of_def true_annot_def true_cls_def)
lemma true_annot_commute:
‹M @ M' ⊨a D ⟷ M' @ M ⊨a D›
unfolding true_annot_def by (simp add: Un_commute)
lemma true_annots_commute:
‹M @ M' ⊨as D ⟷ M' @ M ⊨as D›
unfolding true_annots_def by (auto simp: true_annot_commute)
lemma true_annot_mono[dest]:
‹set I ⊆ set I' ⟹ I ⊨a N ⟹ I' ⊨a N›
using true_cls_mono_set_mset_l unfolding true_annot_def lits_of_def
by (metis (no_types) Un_commute Un_upper1 image_Un sup.orderE)
lemma true_annots_mono:
‹set I ⊆ set I' ⟹ I ⊨as N ⟹ I' ⊨as N›
unfolding true_annots_def by auto
subsubsection ‹Defined and Undefined Literals›
text ‹We introduce the functions @{term defined_lit} and @{term undefined_lit} to know whether a
literal is defined with respect to a list of decided literals (aka a trail in most cases).
Remark that @{term undefined} already exists and is a completely different Isabelle function.
›
definition defined_lit :: ‹('a literal, 'a literal, 'm) annotated_lits ⇒ 'a literal ⇒ bool›
where
‹defined_lit I L ⟷ (Decided L ∈ set I) ∨ (∃P. Propagated L P ∈ set I)
∨ (Decided (-L) ∈ set I) ∨ (∃P. Propagated (-L) P ∈ set I)›
abbreviation undefined_lit :: ‹('a literal, 'a literal, 'm) annotated_lits ⇒ 'a literal ⇒ bool›
where ‹undefined_lit I L ≡ ¬defined_lit I L›
lemma defined_lit_rev[simp]:
‹defined_lit (rev M) L ⟷ defined_lit M L›
unfolding defined_lit_def by auto
lemma atm_imp_decided_or_proped:
assumes ‹x ∈ set I›
shows
‹(Decided (- lit_of x) ∈ set I)
∨ (Decided (lit_of x) ∈ set I)
∨ (∃l. Propagated (- lit_of x) l ∈ set I)
∨ (∃l. Propagated (lit_of x) l ∈ set I)›
using assms by (metis (full_types) lit_of.elims)
lemma literal_is_lit_of_decided:
assumes ‹L = lit_of x›
shows ‹(x = Decided L) ∨ (∃l'. x = Propagated L l')›
using assms by (cases x) auto
lemma true_annot_iff_decided_or_true_lit:
‹defined_lit I L ⟷ (lits_of_l I ⊨l L ∨ lits_of_l I ⊨l -L)›
unfolding defined_lit_def by (auto simp add: lits_of_def rev_image_eqI
dest!: literal_is_lit_of_decided)
lemma consistent_inter_true_annots_satisfiable:
‹consistent_interp (lits_of_l I) ⟹ I ⊨as N ⟹ satisfiable N›
by (simp add: true_annots_true_cls)
lemma defined_lit_map:
‹defined_lit Ls L ⟷ atm_of L ∈ (λl. atm_of (lit_of l)) ` set Ls›
unfolding defined_lit_def apply (rule iffI)
using image_iff apply fastforce
by (fastforce simp add: atm_of_eq_atm_of dest: atm_imp_decided_or_proped)
lemma defined_lit_uminus[iff]:
‹defined_lit I (-L) ⟷ defined_lit I L›
unfolding defined_lit_def by auto
lemma Decided_Propagated_in_iff_in_lits_of_l:
‹defined_lit I L ⟷ (L ∈ lits_of_l I ∨ -L ∈ lits_of_l I)›
unfolding lits_of_def by (metis lits_of_def true_annot_iff_decided_or_true_lit true_lit_def)
lemma consistent_add_undefined_lit_consistent[simp]:
assumes
‹consistent_interp (lits_of_l Ls)› and
‹undefined_lit Ls L›
shows ‹consistent_interp (insert L (lits_of_l Ls))›
using assms unfolding consistent_interp_def by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
lemma decided_empty[simp]:
‹¬defined_lit [] L›
unfolding defined_lit_def by simp
lemma undefined_lit_single[iff]:
‹defined_lit [L] K ⟷ atm_of (lit_of L) = atm_of K›
by (auto simp: defined_lit_map)
lemma undefined_lit_cons[iff]:
‹undefined_lit (L # M) K ⟷ atm_of (lit_of L) ≠ atm_of K ∧ undefined_lit M K›
by (auto simp: defined_lit_map)
lemma undefined_lit_append[iff]:
‹undefined_lit (M @ M') K ⟷ undefined_lit M K ∧ undefined_lit M' K›
by (auto simp: defined_lit_map)
lemma defined_lit_cons:
‹defined_lit (L # M) K ⟷ atm_of (lit_of L) = atm_of K ∨ defined_lit M K›
by (auto simp: defined_lit_map)
lemma defined_lit_append:
‹defined_lit (M @ M') K ⟷ defined_lit M K ∨ defined_lit M' K›
by (auto simp: defined_lit_map)
lemma in_lits_of_l_defined_litD: ‹L_max ∈ lits_of_l M ⟹ defined_lit M L_max›
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
lemma undefined_notin: ‹undefined_lit M (lit_of x) ⟹ x ∉ set M› for x M
by (metis in_lits_of_l_defined_litD insert_iff lits_of_insert mk_disjoint_insert)
lemma uminus_lits_of_l_definedD:
‹-x ∈ lits_of_l M ⟹ defined_lit M x›
by (simp add: Decided_Propagated_in_iff_in_lits_of_l)
lemma defined_lit_Neg_Pos_iff:
‹defined_lit M (Neg A) ⟷ defined_lit M (Pos A)›
by (simp add: defined_lit_map)
lemma defined_lit_Pos_atm_iff[simp]:
‹defined_lit M1 (Pos (atm_of x)) ⟷ defined_lit M1 x›
by (cases x) (auto simp: defined_lit_Neg_Pos_iff)
lemma defined_lit_mono:
‹defined_lit M2 L ⟹ set M2 ⊆ set M3 ⟹ defined_lit M3 L›
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
lemma defined_lit_nth:
‹n < length M2 ⟹ defined_lit M2 (lit_of (M2 ! n))›
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def)
subsection ‹Backtracking›
fun backtrack_split :: ‹('a, 'v, 'm) annotated_lits
⇒ ('a, 'v, 'm) annotated_lits × ('a, 'v, 'm) annotated_lits› where
‹backtrack_split [] = ([], [])› |
‹backtrack_split (Propagated L P # mlits) = apfst ((#) (Propagated L P)) (backtrack_split mlits)› |
‹backtrack_split (Decided L # mlits) = ([], Decided L # mlits)›
lemma backtrack_split_fst_not_decided: ‹a ∈ set (fst (backtrack_split l)) ⟹ ¬is_decided a›
by (induct l rule: ann_lit_list_induct) auto
lemma backtrack_split_snd_hd_decided:
‹snd (backtrack_split l) ≠ [] ⟹ is_decided (hd (snd (backtrack_split l)))›
by (induct l rule: ann_lit_list_induct) auto
lemma backtrack_split_list_eq[simp]:
‹fst (backtrack_split l) @ (snd (backtrack_split l)) = l›
by (induct l rule: ann_lit_list_induct) auto
lemma backtrack_snd_empty_not_decided:
‹backtrack_split M = (M'', []) ⟹ ∀l∈set M. ¬ is_decided l›
by (metis append_Nil2 backtrack_split_fst_not_decided backtrack_split_list_eq snd_conv)
lemma backtrack_split_some_is_decided_then_snd_has_hd:
‹∃l∈set M. is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', L' # M')›
by (metis backtrack_snd_empty_not_decided list.exhaust prod.collapse)
text ‹Another characterisation of the result of @{const backtrack_split}. This view allows some
simpler proofs, since @{term takeWhile} and @{term dropWhile} are highly automated:›
lemma backtrack_split_takeWhile_dropWhile:
‹backtrack_split M = (takeWhile (Not o is_decided) M, dropWhile (Not o is_decided) M)›
by (induction M rule: ann_lit_list_induct) auto
subsection ‹Decomposition with respect to the First Decided Literals›
text ‹In this section we define a function that returns a decomposition with the first decided
literal. This function is useful to define the backtracking of DPLL.›
subsubsection ‹Definition›
text ‹The pattern @{term ‹get_all_ann_decomposition [] = [([], [])]›} is necessary otherwise, we
can call the @{term hd} function in the other pattern. ›
fun get_all_ann_decomposition :: ‹('a, 'b, 'm) annotated_lits
⇒ (('a, 'b, 'm) annotated_lits × ('a, 'b, 'm) annotated_lits) list› where
‹get_all_ann_decomposition (Decided L # Ls) =
(Decided L # Ls, []) # get_all_ann_decomposition Ls› |
‹get_all_ann_decomposition (Propagated L P# Ls) =
(apsnd ((#) (Propagated L P)) (hd (get_all_ann_decomposition Ls)))
# tl (get_all_ann_decomposition Ls)› |
‹get_all_ann_decomposition [] = [([], [])]›
value ‹get_all_ann_decomposition [Propagated A5 B5, Decided C4, Propagated A3 B3,
Propagated A2 B2, Decided C1, Propagated A0 B0]›
text ‹Now we can prove several simple properties about the function.›
lemma get_all_ann_decomposition_never_empty[iff]:
‹get_all_ann_decomposition M = [] ⟷ False›
by (induct M, simp) (rename_tac a xs, case_tac a, auto)
lemma get_all_ann_decomposition_never_empty_sym[iff]:
‹[] = get_all_ann_decomposition M ⟷ False›
using get_all_ann_decomposition_never_empty[of M] by presburger
lemma get_all_ann_decomposition_decomp:
‹hd (get_all_ann_decomposition S) = (a, c) ⟹ S = c @ a›
proof (induct S arbitrary: a c)
case Nil
then show ?case by simp
next
case (Cons x A)
then show ?case by (cases x; cases ‹hd (get_all_ann_decomposition A)›) auto
qed
lemma get_all_ann_decomposition_backtrack_split:
‹backtrack_split S = (M, M') ⟷ hd (get_all_ann_decomposition S) = (M', M)›
proof (induction S arbitrary: M M')
case Nil
then show ?case by auto
next
case (Cons a S)
then show ?case using backtrack_split_takeWhile_dropWhile by (cases a) force+
qed
lemma get_all_ann_decomposition_Nil_backtrack_split_snd_Nil:
‹get_all_ann_decomposition S = [([], A)] ⟹ snd (backtrack_split S) = []›
by (simp add: get_all_ann_decomposition_backtrack_split sndI)
text ‹This functions says that the first element is either empty or starts with a decided element
of the list.›
lemma get_all_ann_decomposition_length_1_fst_empty_or_length_1:
assumes ‹get_all_ann_decomposition M = (a, b) # []›
shows ‹a = [] ∨ (length a = 1 ∧ is_decided (hd a) ∧ hd a ∈ set M)›
using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
case Nil then show ?case by simp
next
case (Decided L mark)
then show ?case by simp
next
case (Propagated L mark M)
then show ?case by (cases ‹get_all_ann_decomposition M›) force+
qed
lemma get_all_ann_decomposition_fst_empty_or_hd_in_M:
assumes ‹get_all_ann_decomposition M = (a, b) # l›
shows ‹a = [] ∨ (is_decided (hd a) ∧ hd a ∈ set M)›
using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
case Nil
then show ?case by auto
next
case (Decided L ann xs)
then show ?case by auto
next
case (Propagated L m xs) note IH = this(1) and d = this(2)
then show ?case
using IH[of ‹fst (hd (get_all_ann_decomposition xs))› ‹snd (hd(get_all_ann_decomposition xs))›]
by (cases ‹get_all_ann_decomposition xs›; cases a) auto
qed
lemma get_all_ann_decomposition_snd_not_decided:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
and ‹L ∈ set b›
shows ‹¬is_decided L›
using assms apply (induct M arbitrary: a b rule: ann_lit_list_induct, simp)
by (rename_tac L' xs a b, case_tac ‹get_all_ann_decomposition xs›; fastforce)+
lemma tl_get_all_ann_decomposition_skip_some:
assumes ‹x ∈ set (tl (get_all_ann_decomposition M1))›
shows ‹x ∈ set (tl (get_all_ann_decomposition (M0 @ M1)))›
using assms
by (induct M0 rule: ann_lit_list_induct)
(auto simp add: list.set_sel(2))
lemma hd_get_all_ann_decomposition_skip_some:
assumes ‹(x, y) = hd (get_all_ann_decomposition M1)›
shows ‹(x, y) ∈ set (get_all_ann_decomposition (M0 @ Decided K # M1))›
using assms
proof (induction M0 rule: ann_lit_list_induct)
case Nil
then show ?case by auto
next
case (Decided L M0)
then show ?case by auto
next
case (Propagated L C M0) note xy = this(1)[OF this(2-)] and hd = this(2)
then show ?case
by (cases ‹get_all_ann_decomposition (M0 @ Decided K # M1)›)
(auto dest!: get_all_ann_decomposition_decomp
arg_cong[of ‹get_all_ann_decomposition _› _ hd])
qed
lemma in_get_all_ann_decomposition_in_get_all_ann_decomposition_prepend:
‹(a, b) ∈ set (get_all_ann_decomposition M') ⟹
∃b'. (a, b' @ b) ∈ set (get_all_ann_decomposition (M @ M'))›
apply (induction M rule: ann_lit_list_induct)
apply (metis append_Nil)
apply auto[]
by (rename_tac L' m xs, case_tac ‹get_all_ann_decomposition (xs @ M')›) auto
lemma in_get_all_ann_decomposition_decided_or_empty:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
shows ‹a = [] ∨ (is_decided (hd a))›
using assms
proof (induct M arbitrary: a b rule: ann_lit_list_induct)
case Nil then show ?case by simp
next
case (Decided l M)
then show ?case by auto
next
case (Propagated l mark M)
then show ?case by (cases ‹get_all_ann_decomposition M›) force+
qed
lemma get_all_ann_decomposition_remove_undecided_length:
assumes ‹∀l ∈ set M'. ¬is_decided l›
shows ‹length (get_all_ann_decomposition (M' @ M'')) = length (get_all_ann_decomposition M'')›
using assms by (induct M' arbitrary: M'' rule: ann_lit_list_induct) auto
lemma get_all_ann_decomposition_not_is_decided_length:
assumes ‹∀l ∈ set M'. ¬is_decided l›
shows ‹1 + length (get_all_ann_decomposition (Propagated (-L) P # M))
= length (get_all_ann_decomposition (M' @ Decided L # M))›
using assms get_all_ann_decomposition_remove_undecided_length by fastforce
lemma get_all_ann_decomposition_last_choice:
assumes ‹tl (get_all_ann_decomposition (M' @ Decided L # M)) ≠ []›
and ‹∀l ∈ set M'. ¬is_decided l›
and ‹hd (tl (get_all_ann_decomposition (M' @ Decided L # M))) = (M0', M0)›
shows ‹hd (get_all_ann_decomposition (Propagated (-L) P # M)) = (M0', Propagated (-L) P # M0)›
using assms by (induct M' rule: ann_lit_list_induct) auto
lemma get_all_ann_decomposition_except_last_choice_equal:
assumes ‹∀l ∈ set M'. ¬is_decided l›
shows ‹tl (get_all_ann_decomposition (Propagated (-L) P # M))
= tl (tl (get_all_ann_decomposition (M' @ Decided L # M)))›
using assms by (induct M' rule: ann_lit_list_induct) auto
lemma get_all_ann_decomposition_hd_hd:
assumes ‹get_all_ann_decomposition Ls = (M, C) # (M0, M0') # l›
shows ‹tl M = M0' @ M0 ∧ is_decided (hd M)›
using assms
proof (induct Ls arbitrary: M C M0 M0' l)
case Nil
then show ?case by simp
next
case (Cons a Ls M C M0 M0' l) note IH = this(1) and g = this(2)
{ fix L ann level
assume a: ‹a = Decided L›
have ‹Ls = M0' @ M0›
using g a by (force intro: get_all_ann_decomposition_decomp)
then have ‹tl M = M0' @ M0 ∧ is_decided (hd M)› using g a by auto
}
moreover {
fix L P
assume a: ‹a = Propagated L P›
have ‹tl M = M0' @ M0 ∧ is_decided (hd M)›
using IH Cons.prems unfolding a by (cases ‹get_all_ann_decomposition Ls›) auto
}
ultimately show ?case by (cases a) auto
qed
lemma get_all_ann_decomposition_exists_prepend[dest]:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
shows ‹∃c. M = c @ b @ a›
using assms apply (induct M rule: ann_lit_list_induct)
apply simp
by (rename_tac L' xs, case_tac ‹get_all_ann_decomposition xs›;
auto dest!: arg_cong[of ‹get_all_ann_decomposition _› _ hd]
get_all_ann_decomposition_decomp)+
lemma get_all_ann_decomposition_incl:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
shows ‹set b ⊆ set M› and ‹set a ⊆ set M›
using assms get_all_ann_decomposition_exists_prepend by fastforce+
lemma get_all_ann_decomposition_exists_prepend':
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
obtains c where ‹M = c @ b @ a›
using assms apply (induct M rule: ann_lit_list_induct)
apply auto[1]
by (rename_tac L' xs, case_tac ‹hd (get_all_ann_decomposition xs)›,
auto dest!: get_all_ann_decomposition_decomp simp add: list.set_sel(2))+
lemma union_in_get_all_ann_decomposition_is_subset:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
shows ‹set a ∪ set b ⊆ set M›
using assms by force
lemma Decided_cons_in_get_all_ann_decomposition_append_Decided_cons:
‹∃c''. (Decided K # c, c'') ∈ set (get_all_ann_decomposition (c' @ Decided K # c))›
apply (induction c' rule: ann_lit_list_induct)
apply auto[2]
apply (rename_tac L xs,
case_tac ‹hd (get_all_ann_decomposition (xs @ Decided K # c))›)
apply (case_tac ‹get_all_ann_decomposition (xs @ Decided K # c)›)
by auto
lemma fst_get_all_ann_decomposition_prepend_not_decided:
assumes ‹∀m∈set MS. ¬ is_decided m›
shows ‹set (map fst (get_all_ann_decomposition M))
= set (map fst (get_all_ann_decomposition (MS @ M)))›
using assms apply (induction MS rule: ann_lit_list_induct)
apply auto[2]
by (rename_tac L m xs; case_tac ‹get_all_ann_decomposition (xs @ M)›) simp_all
lemma no_decision_get_all_ann_decomposition:
‹∀l∈set M. ¬ is_decided l ⟹ get_all_ann_decomposition M = [([], M)]›
by (induction M rule: ann_lit_list_induct) auto
subsubsection ‹Entailment of the Propagated by the Decided Literal›
lemma get_all_ann_decomposition_snd_union:
‹set M = ⋃(set ` snd ` set (get_all_ann_decomposition M)) ∪ {L |L. is_decided L ∧ L ∈ set M}›
(is ‹?M M = ?U M ∪ ?Ls M›)
proof (induct M rule: ann_lit_list_induct)
case Nil
then show ?case by simp
next
case (Decided L M) note IH = this(1)
then have ‹Decided L ∈ ?Ls (Decided L # M)› by auto
moreover have ‹?U (Decided L # M) = ?U M› by auto
moreover have ‹?M M = ?U M ∪ ?Ls M› using IH by auto
ultimately show ?case by auto
next
case (Propagated L m M)
then show ?case by (cases ‹(get_all_ann_decomposition M)›) auto
qed
definition all_decomposition_implies :: ‹'a clause set
⇒ (('a, 'm) ann_lits × ('a, 'm) ann_lits) list ⇒ bool› where
‹all_decomposition_implies N S ⟷ (∀(Ls, seen) ∈ set S. unmark_l Ls ∪ N ⊨ps unmark_l seen)›
lemma all_decomposition_implies_empty[iff]:
‹all_decomposition_implies N []› unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_single[iff]:
‹all_decomposition_implies N [(Ls, seen)] ⟷ unmark_l Ls ∪ N ⊨ps unmark_l seen›
unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_append[iff]:
‹all_decomposition_implies N (S @ S')
⟷ (all_decomposition_implies N S ∧ all_decomposition_implies N S')›
unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_cons_pair[iff]:
‹all_decomposition_implies N ((Ls, seen) # S')
⟷ (all_decomposition_implies N [(Ls, seen)] ∧ all_decomposition_implies N S')›
unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_cons_single[iff]:
‹all_decomposition_implies N (l # S') ⟷
(unmark_l (fst l) ∪ N ⊨ps unmark_l (snd l) ∧
all_decomposition_implies N S')›
unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_trail_is_implied:
assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)›
shows ‹N ∪ {unmark L |L. is_decided L ∧ L ∈ set M}
⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))›
using assms
proof (induct ‹length (get_all_ann_decomposition M)› arbitrary: M)
case 0
then show ?case by auto
next
case (Suc n) note IH = this(1) and length = this(2) and decomp = this(3)
consider
(le1) ‹length (get_all_ann_decomposition M) ≤ 1›
| (gt1) ‹length (get_all_ann_decomposition M) > 1›
by arith
then show ?case
proof cases
case le1
then obtain a b where g: ‹get_all_ann_decomposition M = (a, b) # []›
by (cases ‹get_all_ann_decomposition M›) auto
moreover {
assume ‹a = []›
then have ?thesis using Suc.prems g by auto
}
moreover {
assume l: ‹length a = 1› and m: ‹is_decided (hd a)› and hd: ‹hd a ∈ set M›
then have ‹unmark (hd a) ∈ {unmark L |L. is_decided L ∧ L ∈ set M}› by auto
then have H: ‹unmark_l a ∪ N ⊆ N ∪ {unmark L |L. is_decided L ∧ L ∈ set M}›
using l by (cases a) auto
have f1: ‹unmark_l a ∪ N ⊨ps unmark_l b›
using decomp unfolding all_decomposition_implies_def g by simp
have ?thesis
apply (rule true_clss_clss_subset) using f1 H g by auto
}
ultimately show ?thesis
using get_all_ann_decomposition_length_1_fst_empty_or_length_1 by blast
next
case gt1
then obtain Ls0 seen0 M' where
Ls0: ‹get_all_ann_decomposition M = (Ls0, seen0) # get_all_ann_decomposition M'› and
length': ‹length (get_all_ann_decomposition M') = n› and
M'_in_M: ‹set M' ⊆ set M›
using length by (induct M rule: ann_lit_list_induct) (auto simp: subset_insertI2)
let ?d = ‹⋃(set ` snd ` set (get_all_ann_decomposition M'))›
let ?unM = ‹{unmark L |L. is_decided L ∧ L ∈ set M}›
let ?unM' = ‹{unmark L |L. is_decided L ∧ L ∈ set M'}›
{
assume ‹n = 0›
then have ‹get_all_ann_decomposition M' = []› using length' by auto
then have ?thesis using Suc.prems unfolding all_decomposition_implies_def Ls0 by auto
}
moreover {
assume n: ‹n > 0›
then obtain Ls1 seen1 l where
Ls1: ‹get_all_ann_decomposition M' = (Ls1, seen1) # l›
using length' by (induct M' rule: ann_lit_list_induct) auto
have ‹all_decomposition_implies N (get_all_ann_decomposition M')›
using decomp unfolding Ls0 by auto
then have N: ‹N ∪ ?unM' ⊨ps unmark_s ?d›
using IH length' by auto
have l: ‹N ∪ ?unM' ⊆ N ∪ ?unM›
using M'_in_M by auto
from true_clss_clss_subset[OF this N]
have ΨN: ‹N ∪ ?unM ⊨ps unmark_s ?d› by auto
have ‹is_decided (hd Ls0)› and LS: ‹tl Ls0 = seen1 @ Ls1›
using get_all_ann_decomposition_hd_hd[of M] unfolding Ls0 Ls1 by auto
have LSM: ‹seen1 @ Ls1 = M'› using get_all_ann_decomposition_decomp[of M'] Ls1 by auto
have M': ‹set M' = ?d ∪ {L |L. is_decided L ∧ L ∈ set M'}›
using get_all_ann_decomposition_snd_union by auto
{
assume ‹Ls0 ≠ []›
then have ‹hd Ls0 ∈ set M›
using get_all_ann_decomposition_fst_empty_or_hd_in_M Ls0 by blast
then have ‹N ∪ ?unM ⊨p unmark (hd Ls0)›
using ‹is_decided (hd Ls0)› by (metis (mono_tags, lifting) UnCI mem_Collect_eq
true_clss_cls_in)
} note hd_Ls0 = this
have l: ‹unmark ` (?d ∪ {L |L. is_decided L ∧ L ∈ set M'}) = unmark_s ?d ∪ ?unM'›
by auto
have ‹N ∪ ?unM' ⊨ps unmark ` (?d ∪ {L |L. is_decided L ∧ L ∈ set M'})›
unfolding l using N by (auto simp: all_in_true_clss_clss)
then have t: ‹N ∪ ?unM' ⊨ps unmark_l (tl Ls0)›
using M' unfolding LS LSM by auto
then have ‹N ∪ ?unM ⊨ps unmark_l (tl Ls0)›
using M'_in_M true_clss_clss_subset[OF _ t, of ‹N ∪ ?unM›] by auto
then have ‹N ∪ ?unM ⊨ps unmark_l Ls0›
using hd_Ls0 by (cases Ls0) auto
moreover have ‹unmark_l Ls0 ∪ N ⊨ps unmark_l seen0›
using decomp unfolding Ls0 by simp
moreover have ‹⋀M Ma. (M::'a clause set) ∪ Ma ⊨ps M›
by (simp add: all_in_true_clss_clss)
ultimately have Ψ: ‹N ∪ ?unM ⊨ps unmark_l seen0›
by (meson true_clss_clss_left_right true_clss_clss_union_and true_clss_clss_union_l_r)
moreover have ‹unmark ` (set seen0 ∪ ?d) = unmark_l seen0 ∪ unmark_s ?d›
by auto
ultimately have ?thesis using ΨN unfolding Ls0 by simp
}
ultimately show ?thesis by auto
qed
qed
lemma all_decomposition_implies_propagated_lits_are_implied:
assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)›
shows ‹N ∪ {unmark L |L. is_decided L ∧ L ∈ set M} ⊨ps unmark_l M›
(is ‹?I ⊨ps ?A›)
proof -
have ‹?I ⊨ps unmark_s {L |L. is_decided L ∧ L ∈ set M}›
by (auto intro: all_in_true_clss_clss)
moreover have ‹?I ⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))›
using all_decomposition_implies_trail_is_implied assms by blast
ultimately have ‹N ∪ {unmark m |m. is_decided m ∧ m ∈ set M}
⊨ps unmark ` ⋃(set ` snd ` set (get_all_ann_decomposition M))
∪ unmark ` {m |m. is_decided m ∧ m ∈ set M}›
by blast
then show ?thesis
by (metis (no_types) get_all_ann_decomposition_snd_union[of M] image_Un)
qed
lemma all_decomposition_implies_insert_single:
‹all_decomposition_implies N M ⟹ all_decomposition_implies (insert C N) M›
unfolding all_decomposition_implies_def by auto
lemma all_decomposition_implies_union:
‹all_decomposition_implies N M ⟹ all_decomposition_implies (N ∪ N') M›
unfolding all_decomposition_implies_def sup.assoc[symmetric] by (auto intro: true_clss_clss_union_l)
lemma all_decomposition_implies_mono:
‹N ⊆ N' ⟹ all_decomposition_implies N M ⟹ all_decomposition_implies N' M›
by (metis all_decomposition_implies_union le_iff_sup)
lemma all_decomposition_implies_mono_right:
‹all_decomposition_implies I (get_all_ann_decomposition (M' @ M)) ⟹
all_decomposition_implies I (get_all_ann_decomposition M)›
apply (induction M' arbitrary: M rule: ann_lit_list_induct)
subgoal by auto
subgoal by auto
subgoal for L C M' M
by (cases ‹get_all_ann_decomposition (M' @ M)›) auto
done
subsection ‹Negation of a Clause›
text ‹
We define the negation of a @{typ ‹'a clause›}: it converts a single clause to a set of clauses,
where each clause is a single literal (whose negation is in the original clause).›
definition CNot :: ‹'v clause ⇒ 'v clause_set› where
‹CNot ψ = { {#-L#} | L. L ∈# ψ }›
lemma finite_CNot[simp]: ‹finite (CNot C)›
by (auto simp: CNot_def)
lemma in_CNot_uminus[iff]:
shows ‹{#L#} ∈ CNot ψ ⟷ -L ∈# ψ›
unfolding CNot_def by force
lemma
shows
CNot_add_mset[simp]: ‹CNot (add_mset L ψ) = insert {#-L#} (CNot ψ)› and
CNot_empty[simp]: ‹CNot {#} = {}› and
CNot_plus[simp]: ‹CNot (A + B) = CNot A ∪ CNot B›
unfolding CNot_def by auto
lemma CNot_eq_empty[iff]:
‹CNot D = {} ⟷ D = {#}›
unfolding CNot_def by (auto simp add: multiset_eqI)
lemma in_CNot_implies_uminus:
assumes ‹L ∈# D› and ‹M ⊨as CNot D›
shows ‹M ⊨a {#-L#}› and ‹-L ∈ lits_of_l M›
using assms by (auto simp: true_annots_def true_annot_def CNot_def)
lemma CNot_remdups_mset[simp]:
‹CNot (remdups_mset A) = CNot A›
unfolding CNot_def by auto
lemma Ball_CNot_Ball_mset[simp]:
‹(∀x∈CNot D. P x) ⟷ (∀L∈# D. P {#-L#})›
unfolding CNot_def by auto
lemma consistent_CNot_not:
assumes ‹consistent_interp I›
shows ‹I ⊨s CNot φ ⟹ ¬I ⊨ φ›
using assms unfolding consistent_interp_def true_clss_def true_cls_def by auto
lemma total_not_true_cls_true_clss_CNot:
assumes ‹total_over_m I {φ}› and ‹¬I ⊨ φ›
shows ‹I ⊨s CNot φ›
using assms unfolding total_over_m_def total_over_set_def true_clss_def true_cls_def CNot_def
apply clarify
by (rename_tac x L, case_tac L) (force intro: pos_lit_in_atms_of neg_lit_in_atms_of)+
lemma total_not_CNot:
assumes ‹total_over_m I {φ}› and ‹¬I ⊨s CNot φ›
shows ‹I ⊨ φ›
using assms total_not_true_cls_true_clss_CNot by auto
lemma atms_of_ms_CNot_atms_of[simp]:
‹atms_of_ms (CNot C) = atms_of C›
unfolding atms_of_ms_def atms_of_def CNot_def by fastforce
lemma true_clss_clss_contradiction_true_clss_cls_false:
‹C ∈ D ⟹ D ⊨ps CNot C ⟹ D ⊨p {#}›
unfolding true_clss_clss_def true_clss_cls_def total_over_m_def
by (metis Un_commute atms_of_empty atms_of_ms_CNot_atms_of atms_of_ms_insert atms_of_ms_union
consistent_CNot_not insert_absorb sup_bot.left_neutral true_clss_def)
lemma true_annots_CNot_all_atms_defined:
assumes ‹M ⊨as CNot T› and a1: ‹L ∈# T›
shows ‹atm_of L ∈ atm_of ` lits_of_l M›
by (metis assms atm_of_uminus image_eqI in_CNot_implies_uminus(1) true_annot_singleton)
lemma true_annots_CNot_all_uminus_atms_defined:
assumes ‹M ⊨as CNot T› and a1: ‹-L ∈# T›
shows ‹atm_of L ∈ atm_of ` lits_of_l M›
by (metis assms atm_of_uminus image_eqI in_CNot_implies_uminus(1) true_annot_singleton)
lemma true_clss_clss_false_left_right:
assumes ‹{{#L#}} ∪ B ⊨p {#}›
shows ‹B ⊨ps CNot {#L#}›
unfolding true_clss_clss_def true_clss_cls_def
proof (intro allI impI)
fix I
assume
tot: ‹total_over_m I (B ∪ CNot {#L#})› and
cons: ‹consistent_interp I› and
I: ‹I ⊨s B›
have ‹total_over_m I ({{#L#}} ∪ B)› using tot by auto
then have ‹¬I ⊨s insert {#L#} B›
using assms cons unfolding true_clss_cls_def by simp
then show ‹I ⊨s CNot {#L#}›
using tot I by (cases L) auto
qed
lemma true_annots_true_cls_def_iff_negation_in_model:
‹M ⊨as CNot C ⟷ (∀L ∈# C. -L ∈ lits_of_l M)›
unfolding CNot_def true_annots_true_cls true_clss_def by auto
lemma true_clss_def_iff_negation_in_model:
‹M ⊨s CNot C ⟷ (∀l ∈# C. -l ∈ M)›
by (auto simp: CNot_def true_clss_def)
lemma true_annots_CNot_definedD:
‹M ⊨as CNot C ⟹ ∀L ∈# C. defined_lit M L›
unfolding true_annots_true_cls_def_iff_negation_in_model
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
lemma true_annot_CNot_diff:
‹I ⊨as CNot C ⟹ I ⊨as CNot (C - C')›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model dest: in_diffD)
lemma CNot_mset_replicate[simp]:
‹CNot (mset (replicate n L)) = (if n = 0 then {} else {{#-L#}})›
by (induction n) auto
lemma consistent_CNot_not_tautology:
‹consistent_interp M ⟹ M ⊨s CNot D ⟹ ¬tautology D›
by (metis atms_of_ms_CNot_atms_of consistent_CNot_not satisfiable_carac' satisfiable_def
tautology_def total_over_m_def)
lemma atms_of_ms_CNot_atms_of_ms: ‹atms_of_ms (CNot CC) = atms_of_ms {CC}›
by simp
lemma total_over_m_CNot_toal_over_m[simp]:
‹total_over_m I (CNot C) = total_over_set I (atms_of C)›
unfolding total_over_m_def total_over_set_def by auto
lemma true_clss_cls_plus_CNot:
assumes
CC_L: ‹A ⊨p add_mset L CC› and
CNot_CC: ‹A ⊨ps CNot CC›
shows ‹A ⊨p {#L#}›
unfolding true_clss_clss_def true_clss_cls_def CNot_def total_over_m_def
proof (intro allI impI)
fix I
assume
tot: ‹total_over_set I (atms_of_ms (A ∪ {{#L#}}))› and
cons: ‹consistent_interp I› and
I: ‹I ⊨s A›
let ?I = ‹I ∪ {Pos P|P. P ∈ atms_of CC ∧ P ∉ atm_of ` I}›
have cons': ‹consistent_interp ?I›
using cons unfolding consistent_interp_def
by (auto simp: uminus_lit_swap atms_of_def rev_image_eqI)
have I': ‹?I ⊨s A›
using I true_clss_union_increase by blast
have tot_CNot: ‹total_over_m ?I (A ∪ CNot CC)›
using tot atms_of_s_def by (fastforce simp: total_over_m_def total_over_set_def)
then have tot_I_A_CC_L: ‹total_over_m ?I (A ∪ {add_mset L CC})›
using tot unfolding total_over_m_def total_over_set_atm_of by auto
then have ‹?I ⊨ add_mset L CC› using CC_L cons' I' unfolding true_clss_cls_def by blast
moreover
have ‹?I ⊨s CNot CC› using CNot_CC cons' I' tot_CNot unfolding true_clss_clss_def by auto
then have ‹¬A ⊨p CC›
by (metis (no_types, lifting) I' atms_of_ms_CNot_atms_of_ms atms_of_ms_union cons'
consistent_CNot_not tot_CNot total_over_m_def true_clss_cls_def)
then have ‹¬?I ⊨ CC› using ‹?I ⊨s CNot CC› cons' consistent_CNot_not by blast
ultimately have ‹?I ⊨ {#L#}› by blast
then show ‹I ⊨ {#L#}›
by (metis (no_types, lifting) atms_of_ms_union cons' consistent_CNot_not tot total_not_CNot
total_over_m_def total_over_set_union true_clss_union_increase)
qed
lemma true_annots_CNot_lit_of_notin_skip:
assumes LM: ‹L # M ⊨as CNot A› and LA: ‹lit_of L ∉# A› ‹-lit_of L ∉# A›
shows ‹M ⊨as CNot A›
using LM unfolding true_annots_def Ball_def
proof (intro allI impI)
fix l
assume H: ‹∀x. x ∈ CNot A ⟶ L # M ⊨a x › and l: ‹l ∈ CNot A›
then have ‹L # M ⊨a l› by auto
then show ‹M ⊨a l› using LA l by (cases L) (auto simp: CNot_def)
qed
lemma true_clss_clss_union_false_true_clss_clss_cnot:
‹A ∪ {B} ⊨ps {{#}} ⟷ A ⊨ps CNot B›
using total_not_CNot consistent_CNot_not unfolding total_over_m_def true_clss_clss_def
by fastforce
lemma true_annot_remove_hd_if_notin_vars:
assumes ‹a # M'⊨a D› and ‹atm_of (lit_of a) ∉ atms_of D›
shows ‹M' ⊨a D›
using assms true_cls_remove_hd_if_notin_vars unfolding true_annot_def by auto
lemma true_annot_remove_if_notin_vars:
assumes ‹M @ M'⊨a D› and ‹∀x∈atms_of D. x ∉ atm_of ` lits_of_l M›
shows ‹M' ⊨a D›
using assms by (induct M) (auto dest: true_annot_remove_hd_if_notin_vars)
lemma true_annots_remove_if_notin_vars:
assumes ‹M @ M'⊨as D› and ‹∀x∈atms_of_ms D. x ∉ atm_of ` lits_of_l M›
shows ‹M' ⊨as D› unfolding true_annots_def
using assms unfolding true_annots_def atms_of_ms_def
by (force dest: true_annot_remove_if_notin_vars)
lemma all_variables_defined_not_imply_cnot:
assumes
‹∀s ∈ atms_of_ms {B}. s ∈ atm_of ` lits_of_l A› and
‹¬ A ⊨a B›
shows ‹A ⊨as CNot B›
unfolding true_annot_def true_annots_def Ball_def CNot_def true_lit_def
proof (clarify, rule ccontr)
fix L
assume LB: ‹L ∈# B› and L_false: ‹¬ lits_of_l A ⊨ {#}› and L_A: ‹- L ∉ lits_of_l A›
then have ‹atm_of L ∈ atm_of ` lits_of_l A›
using assms(1) by (simp add: atm_of_lit_in_atms_of lits_of_def)
then have ‹L ∈ lits_of_l A ∨ -L ∈ lits_of_l A›
using atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set by metis
then have ‹L ∈ lits_of_l A› using L_A by auto
then show False
using LB assms(2) unfolding true_annot_def true_lit_def true_cls_def Bex_def
by blast
qed
lemma CNot_union_mset[simp]:
‹CNot (A ∪# B) = CNot A ∪ CNot B›
unfolding CNot_def by auto
lemma true_clss_clss_true_clss_cls_true_clss_clss:
assumes
‹A ⊨ps unmark_l M› and ‹M ⊨as D›
shows ‹A ⊨ps D›
by (meson assms total_over_m_union true_annots_true_cls true_annots_true_clss_clss
true_clss_clss_def true_clss_clss_left_right true_clss_clss_union_and
true_clss_clss_union_l_r)
lemma true_clss_clss_CNot_true_clss_cls_unsatisfiable:
assumes ‹A ⊨ps CNot D› and ‹A ⊨p D›
shows ‹unsatisfiable A›
using assms(2) unfolding true_clss_clss_def true_clss_cls_def satisfiable_def
by (metis (full_types) Un_absorb Un_empty_right assms(1) atms_of_empty
atms_of_ms_emtpy_set total_over_m_def total_over_m_insert total_over_m_union
true_cls_empty true_clss_cls_def true_clss_clss_generalise_true_clss_clss
true_clss_clss_true_clss_cls true_clss_clss_union_false_true_clss_clss_cnot)
lemma true_clss_cls_neg:
‹N ⊨p I ⟷ N ∪ (λL. {#-L#}) ` set_mset I ⊨p {#}›
proof -
have [simp]: ‹(λL. {#- L#}) ` set_mset I = CNot I› for I
by (auto simp: CNot_def)
have [iff]: ‹ total_over_m Ia ((λL. {#- L#}) ` set_mset I) ⟷
total_over_set Ia (atms_of I)› for Ia
by (auto simp: total_over_m_def
total_over_set_def atms_of_ms_def atms_of_def)
show ?thesis
by (auto simp: true_clss_cls_def consistent_CNot_not
total_not_CNot)
qed
lemma all_decomposition_implies_conflict_DECO_clause:
assumes ‹all_decomposition_implies N (get_all_ann_decomposition M)› and
‹M ⊨as CNot C› and
‹C ∈ N›
shows ‹N ⊨p (uminus o lit_of) `# (filter_mset is_decided (mset M))›
(is ‹?I ⊨p ?A›)
proof -
have ‹{unmark m |m. is_decided m ∧ m ∈ set M} =
unmark_s {L ∈ set M. is_decided L}›
by auto
have ‹N ∪ unmark_s {L ∈ set M. is_decided L} ⊨p {#}›
by (metis (mono_tags, lifting) UnCI
‹{unmark m |m. is_decided m ∧ m ∈ set M} = unmark_s {L ∈ set M. is_decided L}›
all_decomposition_implies_propagated_lits_are_implied assms
true_clss_clss_contradiction_true_clss_cls_false true_clss_clss_true_clss_cls_true_clss_clss)
then show ?thesis
apply (subst true_clss_cls_neg)
by (auto simp: image_image)
qed
subsection ‹Other›
definition ‹no_dup L ≡ distinct (map (λl. atm_of (lit_of l)) L)›
lemma no_dup_nil[simp]:
‹no_dup []›
by (auto simp: no_dup_def)
lemma no_dup_cons[simp]:
‹no_dup (L # M) ⟷ undefined_lit M (lit_of L) ∧ no_dup M›
by (auto simp: no_dup_def defined_lit_map)
lemma no_dup_append_cons[iff]:
‹no_dup (M @ L # M') ⟷ undefined_lit (M @ M') (lit_of L) ∧ no_dup (M @ M')›
by (auto simp: no_dup_def defined_lit_map)
lemma no_dup_append_append_cons[iff]:
‹no_dup (M0 @ M @ L # M') ⟷ undefined_lit (M0 @ M @ M') (lit_of L) ∧ no_dup (M0 @ M @ M')›
by (auto simp: no_dup_def defined_lit_map)
lemma no_dup_rev[simp]:
‹no_dup (rev M) ⟷ no_dup M›
by (auto simp: rev_map[symmetric] no_dup_def)
lemma no_dup_appendD:
‹no_dup (a @ b) ⟹ no_dup b›
by (auto simp: no_dup_def)
lemma no_dup_appendD1:
‹no_dup (a @ b) ⟹ no_dup a›
by (auto simp: no_dup_def)
lemma no_dup_length_eq_card_atm_of_lits_of_l:
assumes ‹no_dup M›
shows ‹length M = card (atm_of ` lits_of_l M)›
using assms unfolding lits_of_def by (induct M) (auto simp add: image_image no_dup_def)
lemma distinct_consistent_interp:
‹no_dup M ⟹ consistent_interp (lits_of_l M)›
proof (induct M)
case Nil
show ?case by auto
next
case (Cons L M)
then have a1: ‹consistent_interp (lits_of_l M)› by auto
have ‹undefined_lit M (lit_of L)›
using Cons.prems by auto
then show ?case
using a1 by simp
qed
lemma same_mset_no_dup_iff:
‹mset M = mset M' ⟹ no_dup M ⟷ no_dup M'›
by (auto simp: no_dup_def same_mset_distinct_iff)
lemma distinct_get_all_ann_decomposition_no_dup:
assumes ‹(a, b) ∈ set (get_all_ann_decomposition M)›
and ‹no_dup M›
shows ‹no_dup (a @ b)›
using assms by (force simp: no_dup_def)
lemma true_annots_lit_of_notin_skip:
assumes ‹L # M ⊨as CNot A›
and ‹-lit_of L ∉# A›
and ‹no_dup (L # M)›
shows ‹M ⊨as CNot A›
proof -
have ‹∀l ∈# A. -l ∈ lits_of_l (L # M)›
using assms(1) in_CNot_implies_uminus(2) by blast
moreover {
have ‹undefined_lit M (lit_of L)›
using assms(3) by force
then have ‹- lit_of L ∉ lits_of_l M›
by (simp add: Decided_Propagated_in_iff_in_lits_of_l) }
ultimately have ‹∀ l ∈# A. -l ∈ lits_of_l M›
using assms(2) by (metis insert_iff list.simps(15) lits_of_insert uminus_of_uminus_id)
then show ?thesis by (auto simp add: true_annots_def)
qed
lemma no_dup_imp_distinct: ‹no_dup M ⟹ distinct M›
by (induction M) (auto simp: defined_lit_map)
lemma no_dup_tlD: ‹no_dup a ⟹ no_dup (tl a)›
unfolding no_dup_def by (cases a) auto
lemma defined_lit_no_dupD:
‹defined_lit M1 L ⟹ no_dup (M2 @ M1) ⟹ undefined_lit M2 L›
‹defined_lit M1 L ⟹ no_dup (M2' @ M2 @ M1) ⟹ undefined_lit M2' L›
‹defined_lit M1 L ⟹ no_dup (M2' @ M2 @ M1) ⟹ undefined_lit M2 L›
by (auto simp: defined_lit_map no_dup_def)
lemma no_dup_consistentD:
‹no_dup M ⟹ L ∈ lits_of_l M ⟹ -L ∉ lits_of_l M›
using consistent_interp_def distinct_consistent_interp by blast
lemma no_dup_not_tautology: ‹no_dup M ⟹ ¬tautology (image_mset lit_of (mset M))›
by (induction M) (auto simp: tautology_add_mset uminus_lit_swap defined_lit_def
dest: atm_imp_decided_or_proped)
lemma no_dup_distinct: ‹no_dup M ⟹ distinct_mset (image_mset lit_of (mset M))›
by (induction M) (auto simp: uminus_lit_swap defined_lit_def
dest: atm_imp_decided_or_proped)
lemma no_dup_not_tautology_uminus: ‹no_dup M ⟹ ¬tautology {#-lit_of L. L ∈# mset M#}›
by (induction M) (auto simp: tautology_add_mset uminus_lit_swap defined_lit_def
dest: atm_imp_decided_or_proped)
lemma no_dup_distinct_uminus: ‹no_dup M ⟹ distinct_mset {#-lit_of L. L ∈# mset M#}›
by (induction M) (auto simp: uminus_lit_swap defined_lit_def
dest: atm_imp_decided_or_proped)
lemma no_dup_map_lit_of: ‹no_dup M ⟹ distinct (map lit_of M)›
apply (induction M)
apply (auto simp: dest: no_dup_imp_distinct)
by (meson distinct.simps(2) no_dup_cons no_dup_imp_distinct)
lemma no_dup_alt_def:
‹no_dup M ⟷ distinct_mset {#atm_of (lit_of x). x ∈# mset M#}›
by (auto simp: no_dup_def simp flip: distinct_mset_mset_distinct)
lemma no_dup_append_in_atm_notin:
assumes ‹no_dup (M @ M')› and ‹L ∈ lits_of_l M'›
shows ‹undefined_lit M L›
using assms by (auto simp add: atm_lit_of_set_lits_of_l no_dup_def
defined_lit_map)
lemma no_dup_uminus_append_in_atm_notin:
assumes ‹no_dup (M @ M')› and ‹-L ∈ lits_of_l M'›
shows ‹undefined_lit M L›
using Decided_Propagated_in_iff_in_lits_of_l assms defined_lit_no_dupD(1) by blast
subsection ‹Extending Entailments to multisets›
text ‹We have defined previous entailment with respect to sets, but we also need a multiset version
depending on the context. The conversion is simple using the function @{term set_mset} (in this
direction, there is no loss of information).›
abbreviation true_annots_mset (infix "⊨asm" 50) where
‹I ⊨asm C ≡ I ⊨as (set_mset C)›
abbreviation true_clss_clss_m :: ‹'v clause multiset ⇒ 'v clause multiset ⇒ bool› (infix "⊨psm" 50)
where
‹I ⊨psm C ≡ set_mset I ⊨ps (set_mset C)›
text ‹Analog of theorem @{thm [source] true_clss_clss_subsetE}›
lemma true_clss_clssm_subsetE: ‹N ⊨psm B ⟹ A ⊆# B ⟹ N ⊨psm A›
using set_mset_mono true_clss_clss_subsetE by blast
abbreviation true_clss_cls_m:: ‹'a clause multiset ⇒ 'a clause ⇒ bool› (infix "⊨pm" 50) where
‹I ⊨pm C ≡ set_mset I ⊨p C›
abbreviation distinct_mset_mset :: ‹'a multiset multiset ⇒ bool› where
‹distinct_mset_mset Σ ≡ distinct_mset_set (set_mset Σ)›
abbreviation all_decomposition_implies_m where
‹all_decomposition_implies_m A B ≡ all_decomposition_implies (set_mset A) B›
abbreviation atms_of_mm :: ‹'a clause multiset ⇒ 'a set› where
‹atms_of_mm U ≡ atms_of_ms (set_mset U)›
text ‹Other definition using @{term ‹Union_mset›}›
lemma atms_of_mm_alt_def: ‹atms_of_mm U = set_mset (⋃# (image_mset (image_mset atm_of) U))›
unfolding atms_of_ms_def by (auto simp: atms_of_def)
abbreviation true_clss_m:: ‹'a partial_interp ⇒ 'a clause multiset ⇒ bool› (infix "⊨sm" 50) where
‹I ⊨sm C ≡ I ⊨s set_mset C›
abbreviation true_clss_ext_m (infix "⊨sextm" 49) where
‹I ⊨sextm C ≡ I ⊨sext set_mset C›
lemma true_clss_cls_cong_set_mset:
‹N ⊨pm D ⟹ set_mset D = set_mset D' ⟹ N ⊨pm D'›
by (auto simp add: true_clss_cls_def true_cls_def atms_of_cong_set_mset[of D D'])
subsection ‹More Lemmas›
lemma no_dup_cannot_not_lit_and_uminus:
‹no_dup M ⟹ - lit_of xa = lit_of x ⟹ x ∈ set M ⟹ xa ∉ set M›
by (metis atm_of_uminus distinct_map inj_on_eq_iff uminus_not_id' no_dup_def)
lemma atms_of_ms_single_atm_of[simp]:
‹atms_of_ms {unmark L |L. P L} = atm_of ` {lit_of L |L. P L}›
unfolding atms_of_ms_def by force
lemma true_cls_mset_restrict:
‹{L ∈ I. atm_of L ∈ atms_of_mm N} ⊨m N ⟷ I ⊨m N›
by (auto simp: true_cls_mset_def true_cls_def
dest!: multi_member_split)
lemma true_clss_restrict:
‹{L ∈ I. atm_of L ∈ atms_of_mm N} ⊨sm N ⟷ I ⊨sm N›
by (auto simp: true_clss_def true_cls_def
dest!: multi_member_split)
lemma total_over_m_atms_incl:
assumes ‹total_over_m M (set_mset N)›
shows
‹x ∈ atms_of_mm N ⟹ x ∈ atms_of_s M›
by (meson assms contra_subsetD total_over_m_alt_def)
lemma true_clss_restrict_iff:
assumes ‹¬tautology χ›
shows ‹N ⊨p χ ⟷ N ⊨p {#L ∈# χ. atm_of L ∈ atms_of_ms N#}› (is ‹?A ⟷ ?B›)
apply (subst true_clss_alt_def2[OF assms])
apply (subst true_clss_alt_def2)
subgoal using not_tautology_mono[OF _ assms] by (auto dest: not_tautology_minus)
apply (rule HOL.iff_allI)
apply (auto 5 5 simp: true_cls_def atms_of_s_def dest!: multi_member_split)
done
subsection ‹Negation of annotated clauses›
definition negate_ann_lits :: ‹('v literal, 'v literal, 'mark) annotated_lits ⇒ 'v literal multiset› where
‹negate_ann_lits M = (λL. - lit_of L) `# mset M›
lemma negate_ann_lits_empty[simp]: ‹negate_ann_lits [] = {#}›
by (auto simp: negate_ann_lits_def)
lemma entails_CNot_negate_ann_lits:
‹M ⊨as CNot D ⟷ set_mset D ⊆ set_mset (negate_ann_lits M)›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model
negate_ann_lits_def lits_of_def uminus_lit_swap
dest!: multi_member_split)
text ‹Pointwise negation of a clause:›
definition pNeg :: ‹'v clause ⇒ 'v clause› where
‹pNeg C = {#-D. D ∈# C#}›
lemma pNeg_simps:
‹pNeg (add_mset A C) = add_mset (-A) (pNeg C)›
‹pNeg (C + D) = pNeg C + pNeg D›
by (auto simp: pNeg_def)
lemma atms_of_pNeg[simp]: ‹atms_of (pNeg C) = atms_of C›
by (auto simp: pNeg_def atms_of_def image_image)
lemma negate_ann_lits_pNeg_lit_of: ‹negate_ann_lits = pNeg o image_mset lit_of o mset›
by (intro ext) (auto simp: negate_ann_lits_def pNeg_def)
lemma negate_ann_lits_empty_iff: ‹negate_ann_lits M ≠ {#} ⟷ M ≠ []›
by (auto simp: negate_ann_lits_def)
lemma atms_of_negate_ann_lits[simp]: ‹atms_of (negate_ann_lits M) = atm_of ` (lits_of_l M)›
unfolding negate_ann_lits_def lits_of_def atms_of_def by (auto simp: image_image)
lemma tautology_pNeg[simp]:
‹tautology (pNeg C) ⟷ tautology C›
by (auto 5 5 simp: tautology_decomp pNeg_def
uminus_lit_swap add_mset_eq_add_mset eq_commute[of ‹Neg _› ‹- _›] eq_commute[of ‹Pos _› ‹- _›]
dest!: multi_member_split)
lemma pNeg_convolution[simp]:
‹pNeg (pNeg C) = C›
by (auto simp: pNeg_def)
lemma pNeg_minus[simp]: ‹pNeg (A - B) = pNeg A - pNeg B›
unfolding pNeg_def
by (subst image_mset_minus_inj_on) (auto simp: inj_on_def)
lemma pNeg_empty[simp]: ‹pNeg {#} = {#}›
unfolding pNeg_def
by (auto simp: inj_on_def)
lemma pNeg_replicate_mset[simp]: ‹pNeg (replicate_mset n L) = replicate_mset n (-L)›
unfolding pNeg_def by auto
lemma distinct_mset_pNeg_iff[iff]: ‹distinct_mset (pNeg x) ⟷ distinct_mset x›
unfolding pNeg_def
by (rule distinct_image_mset_inj) (auto simp: inj_on_def)
lemma pNeg_simple_clss_iff[simp]:
‹pNeg M ∈ simple_clss N ⟷ M ∈ simple_clss N›
by (auto simp: simple_clss_def)
lemma atms_of_ms_pNeg[simp]: ‹atms_of_ms (pNeg ` N) = atms_of_ms N›
unfolding atms_of_ms_def pNeg_def by (auto simp: image_image atms_of_def)
definition DECO_clause :: ‹('v, 'a) ann_lits ⇒ 'v clause› where
‹DECO_clause M = (uminus o lit_of) `# (filter_mset is_decided (mset M))›
lemma
DECO_clause_cons_Decide[simp]:
‹DECO_clause (Decided L # M) = add_mset (-L) (DECO_clause M)› and
DECO_clause_cons_Proped[simp]:
‹DECO_clause (Propagated L C # M) = DECO_clause M›
by (auto simp: DECO_clause_def)
lemma no_dup_distinct_mset[intro!]:
assumes n_d: ‹no_dup M›
shows ‹distinct_mset (negate_ann_lits M)›
unfolding negate_ann_lits_def no_dup_def
proof (subst distinct_image_mset_inj)
show ‹inj_on (λL. - lit_of L) (set_mset (mset M))›
unfolding inj_on_def Ball_def
proof (intro allI impI, rule ccontr)
fix L L'
assume
L: ‹L ∈# mset M› and
L': ‹L' ∈# mset M› and
lit: ‹- lit_of L = - lit_of L'› and
LL': ‹L ≠ L'›
have ‹atm_of (lit_of L) = atm_of (lit_of L')›
using lit by auto
moreover have ‹atm_of (lit_of L) ∈# (λl. atm_of (lit_of l)) `# mset M›
using L by auto
moreover have ‹atm_of (lit_of L') ∈# (λl. atm_of (lit_of l)) `# mset M›
using L' by auto
ultimately show False
using assms LL' L L' unfolding distinct_mset_mset_distinct[symmetric] mset_map no_dup_def
apply - apply (rule distinct_image_mset_not_equal[of L L' ‹(λl. atm_of (lit_of l))›])
by auto
qed
next
show ‹distinct_mset (mset M)›
using no_dup_imp_distinct[OF n_d] by simp
qed
lemma in_negate_trial_iff: ‹L ∈# negate_ann_lits M ⟷ - L ∈ lits_of_l M›
unfolding negate_ann_lits_def lits_of_def by (auto simp: uminus_lit_swap)
lemma negate_ann_lits_cons[simp]:
‹negate_ann_lits (L # M) = add_mset (- lit_of L) (negate_ann_lits M)›
by (auto simp: negate_ann_lits_def)
lemma uminus_simple_clss_iff[simp]:
‹uminus `# M ∈ simple_clss N ⟷ M ∈ simple_clss N›
by (metis pNeg_simple_clss_iff pNeg_def)
lemma pNeg_mono: ‹C ⊆# C' ⟹ pNeg C ⊆# pNeg C'›
by (auto simp: image_mset_subseteq_mono pNeg_def)
end