section ‹Partial Clausal Logic›
text ‹We here define decided literals (that will be used in both DPLL and CDCL) and the entailment
corresponding to it.›
theory Partial_Annotated_Clausal_Logic
imports Partial_Clausal_Logic
begin
subsection ‹Decided Literals›
subsubsection ‹Definition›
datatype ('v, 'lvl, 'mark) ann_literal =
is_decided: Decided (lit_of: "'v literal") (level_of: "'lvl") |
is_proped: Propagated (lit_of: "'v literal") (mark_of: 'mark)
lemma ann_literal_list_induct[case_names nil decided proped]:
assumes "P []" and
"⋀L l xs. P xs ⟹ P (Decided L 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 lvl. L = Decided K lvl"
by (cases L) auto
type_synonym ('v, 'l, 'm) ann_literals = "('v, 'l, 'm) ann_literal list"
definition lits_of :: "('a, 'b, 'c) ann_literal list ⇒ 'a literal set" where
"lits_of Ls = lit_of ` (set Ls)"
lemma lits_of_empty[simp]:
"lits_of [] = {}" unfolding lits_of_def by auto
lemma lits_of_cons[simp]:
"lits_of (L # Ls) = insert (lit_of L) (lits_of Ls)"
unfolding lits_of_def by auto
lemma lits_of_append[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)"
unfolding lits_of_def by auto
lemma lits_of_rev[simp]: "lits_of (rev M) = lits_of M"
unfolding lits_of_def by auto
lemma set_map_lit_of_lits_of[simp]:
"set (map lit_of T) = lits_of T"
unfolding lits_of_def by auto
text ‹Remove annotation and transform to a set of single literals.›
abbreviation unmark :: "('a, 'b, 'c) ann_literal list ⇒ 'a literal multiset set" where
"unmark M ≡ (λa. {#lit_of a#}) ` set M"
lemma atms_of_ms_lambda_lit_of_is_atm_of_lit_of[simp]:
"atms_of_ms (unmark M') = atm_of ` lits_of M'"
unfolding atms_of_ms_def lits_of_def by auto
lemma lits_of_empty_is_empty[iff]:
"lits_of M = {} ⟷ M = []"
by (induct M) auto
subsubsection ‹Entailment›
definition true_annot :: "('a, 'l, 'm) ann_literals ⇒ 'a clause ⇒ bool" (infix "⊨a" 49) where
"I ⊨a C ⟷ (lits_of I) ⊨ C"
definition true_annots :: "('a, 'l, 'm) ann_literals ⇒ 'a clauses ⇒ 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
text ‹Link between ‹⊨as› and ‹⊨s›:›
lemma true_annots_true_cls:
"I ⊨as CC ⟷ (lits_of 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 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 MLs ⟹ lits_of MLs ⊆ I"
unfolding true_clss_def lits_of_def by auto
lemma true_annot_true_clss_cls:
"MLs ⊨a ψ ⟹ set (map (λa. {#lit_of a#}) 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 (λa. {#lit_of a#}) 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 (λM. Decided M a) M ⊨as N ⟷ set M ⊨s N"
proof -
have *: "lits_of (map (λM. Decided M a) M) = set M" unfolding lits_of_def by force
show ?thesis by (simp add: true_annots_true_cls *)
qed
lemma true_annot_singleton[iff]: "M ⊨a {#L#} ⟷ L ∈ lits_of M"
unfolding true_annot_def lits_of_def by auto
lemma true_annots_true_clss_clss:
"A ⊨as Ψ ⟹ unmark 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, 'l, 'm) ann_literal list ⇒ 'a literal ⇒ bool"
where
"defined_lit I L ⟷ (∃l. Decided L l ∈ set I) ∨ (∃P. Propagated L P ∈ set I)
∨ (∃l. Decided (-L) l ∈ set I) ∨ (∃P. Propagated (-L) P ∈ set I)"
abbreviation undefined_lit :: "('a, 'l, 'm) ann_literal list ⇒ '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
"(∃l. Decided (- lit_of x) l ∈ set I)
∨ (∃l. Decided (lit_of x) l ∈ set I)
∨ (∃l. Propagated (- lit_of x) l ∈ set I)
∨ (∃l. Propagated (lit_of x) l ∈ set I)"
using assms ann_literal.exhaust_sel by metis
lemma literal_is_lit_of_decided:
assumes "L = lit_of x"
shows "(∃l. x = Decided L 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 I) ⊨l L ∨ (lits_of 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 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:
"defined_lit I L ⟷ (L ∈ lits_of I ∨ -L ∈ lits_of 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 Ls)" and
"undefined_lit Ls L"
shows "consistent_interp (insert L (lits_of Ls))"
using assms unfolding consistent_interp_def by (auto simp: Decided_Propagated_in_iff_in_lits_of)
lemma decided_empty[simp]:
"¬defined_lit [] L"
unfolding defined_lit_def by simp
subsection ‹Backtracking›
fun backtrack_split :: "('v, 'l, 'm) ann_literals
⇒ ('v, 'l, 'm) ann_literals × ('v, 'l, 'm) ann_literals" where
"backtrack_split [] = ([], [])" |
"backtrack_split (Propagated L P # mlits) = apfst ((op #) (Propagated L P)) (backtrack_split mlits)" |
"backtrack_split (Decided L l # mlits) = ([], Decided L l # mlits)"
lemma backtrack_split_fst_not_decided: "a ∈ set (fst (backtrack_split l)) ⟹ ¬is_decided a"
by (induct l rule: ann_literal_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_literal_list_induct) auto
lemma backtrack_split_list_eq[simp]:
"fst (backtrack_split l) @ (snd (backtrack_split l)) = l"
by (induct l rule: ann_literal_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_literal_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_decided_decomposition [] = [([], [])]"} is necessary otherwise, we
can call the @{term hd} function in the other pattern. ›
fun get_all_decided_decomposition :: "('a, 'l, 'm) ann_literals
⇒ (('a, 'l, 'm) ann_literals × ('a, 'l, 'm) ann_literals) list" where
"get_all_decided_decomposition (Decided L l # Ls) =
(Decided L l # Ls, []) # get_all_decided_decomposition Ls" |
"get_all_decided_decomposition (Propagated L P# Ls) =
(apsnd ((op #) (Propagated L P)) (hd (get_all_decided_decomposition Ls)))
# tl (get_all_decided_decomposition Ls)" |
"get_all_decided_decomposition [] = [([], [])]"
value "get_all_decided_decomposition [Propagated A5 B5, Decided C4 D4, Propagated A3 B3,
Propagated A2 B2, Decided C1 D1, Propagated A0 B0]"
text ‹Now we can prove several simple properties about the function.›
lemma get_all_decided_decomposition_never_empty[iff]:
"get_all_decided_decomposition M = [] ⟷ False"
by (induct M, simp) (rename_tac a xs, case_tac a, auto)
lemma get_all_decided_decomposition_never_empty_sym[iff]:
"[] = get_all_decided_decomposition M ⟷ False"
using get_all_decided_decomposition_never_empty[of M] by presburger
lemma get_all_decided_decomposition_decomp:
"hd (get_all_decided_decomposition S) = (a, c) ⟹ S = c @ a"
proof (induct S arbitrary: a c)
case Nil
thus ?case by simp
next
case (Cons x A)
thus ?case by (cases x; cases "hd (get_all_decided_decomposition A)") auto
qed
lemma get_all_decided_decomposition_backtrack_split:
"backtrack_split S = (M, M') ⟷ hd (get_all_decided_decomposition S) = (M', M)"
proof (induction S arbitrary: M M')
case Nil
thus ?case by auto
next
case (Cons a S)
thus ?case using backtrack_split_takeWhile_dropWhile by (cases a) force+
qed
lemma get_all_decided_decomposition_nil_backtrack_split_snd_nil:
"get_all_decided_decomposition S = [([], A)] ⟹ snd (backtrack_split S) = []"
by (simp add: get_all_decided_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_decided_decomposition_length_1_fst_empty_or_length_1:
assumes "get_all_decided_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)
case Nil thus ?case by simp
next
case (Cons m M)
show ?case
proof (cases m)
case (Decided l mark)
thus ?thesis using Cons by simp
next
case (Propagated l mark)
thus ?thesis using Cons by (cases "get_all_decided_decomposition M") force+
qed
qed
lemma get_all_decided_decomposition_fst_empty_or_hd_in_M:
assumes "get_all_decided_decomposition M = (a, b) # l"
shows "a = [] ∨ (is_decided (hd a) ∧ hd a ∈ set M)"
using assms apply (induct M arbitrary: a b rule: ann_literal_list_induct)
apply auto[2]
by (metis UnCI backtrack_split_snd_hd_decided get_all_decided_decomposition_backtrack_split
get_all_decided_decomposition_decomp hd_in_set list.sel(1) set_append snd_conv)
lemma get_all_decided_decomposition_snd_not_decided:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
and "L ∈ set b"
shows "¬is_decided L"
using assms apply (induct M arbitrary: a b rule: ann_literal_list_induct, simp)
by (rename_tac L' l xs a b, case_tac "get_all_decided_decomposition xs"; fastforce)+
lemma tl_get_all_decided_decomposition_skip_some:
assumes "x ∈ set (tl (get_all_decided_decomposition M1))"
shows "x ∈ set (tl (get_all_decided_decomposition (M0 @ M1)))"
using assms
by (induct M0 rule: ann_literal_list_induct)
(auto simp add: list.set_sel(2))
lemma hd_get_all_decided_decomposition_skip_some:
assumes "(x, y) = hd (get_all_decided_decomposition M1)"
shows "(x, y) ∈ set (get_all_decided_decomposition (M0 @ Decided K i # M1))"
using assms
proof (induction M0 rule: ann_literal_list_induct)
case nil
then show ?case by auto
next
case (decided L m M0)
then show ?case by auto
next
case (proped L C M0) note xy = this(1)[OF this(2-)] and hd = this(2)
then show ?case
by (cases "get_all_decided_decomposition (M0 @ Decided K i # M1)")
(auto dest!: get_all_decided_decomposition_decomp
arg_cong[of "get_all_decided_decomposition _" _ hd])
qed
lemma in_get_all_decided_decomposition_in_get_all_decided_decomposition_prepend:
"(a, b) ∈ set (get_all_decided_decomposition M') ⟹
∃b'. (a, b' @ b) ∈ set (get_all_decided_decomposition (M @ M'))"
apply (induction M rule: ann_literal_list_induct)
apply (metis append_Nil)
apply auto[]
by (rename_tac L' m xs, case_tac "get_all_decided_decomposition (xs @ M')") auto
lemma get_all_decided_decomposition_remove_undecided_length:
assumes "∀l ∈ set M'. ¬is_decided l"
shows "length (get_all_decided_decomposition (M' @ M''))
= length (get_all_decided_decomposition M'')"
using assms by (induct M' arbitrary: M'' rule: ann_literal_list_induct) auto
lemma get_all_decided_decomposition_not_is_decided_length:
assumes "∀l ∈ set M'. ¬is_decided l"
shows "1 + length (get_all_decided_decomposition (Propagated (-L) P # M))
= length (get_all_decided_decomposition (M' @ Decided L l # M))"
using assms get_all_decided_decomposition_remove_undecided_length by fastforce
lemma get_all_decided_decomposition_last_choice:
assumes "tl (get_all_decided_decomposition (M' @ Decided L l # M)) ≠ []"
and "∀l ∈ set M'. ¬is_decided l"
and "hd (tl (get_all_decided_decomposition (M' @ Decided L l # M))) = (M0', M0)"
shows "hd (get_all_decided_decomposition (Propagated (-L) P # M)) = (M0', Propagated (-L) P # M0)"
using assms by (induct M' rule: ann_literal_list_induct) auto
lemma get_all_decided_decomposition_except_last_choice_equal:
assumes "∀l ∈ set M'. ¬is_decided l"
shows "tl (get_all_decided_decomposition (Propagated (-L) P # M))
= tl (tl (get_all_decided_decomposition (M' @ Decided L l # M)))"
using assms by (induct M' rule: ann_literal_list_induct) auto
lemma get_all_decided_decomposition_hd_hd:
assumes "get_all_decided_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
thus ?case by simp
next
case (Cons a Ls M C M0 M0' l) note IH = this(1) and g = this(2)
{ fix L level
assume a: "a = Decided L level"
have "Ls = M0' @ M0"
using g a by (force intro: get_all_decided_decomposition_decomp)
hence "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_decided_decomposition Ls") auto
}
ultimately show ?case by (cases a) auto
qed
lemma get_all_decided_decomposition_exists_prepend[dest]:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
shows "∃c. M = c @ b @ a"
using assms apply (induct M rule: ann_literal_list_induct)
apply simp
by (rename_tac L' m xs, case_tac "get_all_decided_decomposition xs";
auto dest!: arg_cong[of "get_all_decided_decomposition _" _ hd]
get_all_decided_decomposition_decomp)+
lemma get_all_decided_decomposition_incl:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
shows "set b ⊆ set M" and "set a ⊆ set M"
using assms get_all_decided_decomposition_exists_prepend by fastforce+
lemma get_all_decided_decomposition_exists_prepend':
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
obtains c where "M = c @ b @ a"
using assms apply (induct M rule: ann_literal_list_induct)
apply auto[1]
by (rename_tac L' m xs, case_tac "hd (get_all_decided_decomposition xs)",
auto dest!: get_all_decided_decomposition_decomp simp add: list.set_sel(2))+
lemma union_in_get_all_decided_decomposition_is_subset:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
shows "set a ∪ set b ⊆ set M"
using assms by force
subsubsection ‹Entailment of the Propagated by the Decided Literal›
lemma get_all_decided_decomposition_snd_union:
"set M = ⋃(set ` snd ` set (get_all_decided_decomposition M)) ∪ {L |L. is_decided L ∧ L ∈ set M}"
(is "?M M = ?U M ∪ ?Ls M")
proof (induct M rule: ann_literal_list_induct)
case nil
then show ?case by simp
next
case (decided L l M) note IH = this(1)
then have "Decided L l ∈ ?Ls (Decided L l #M)" by auto
moreover have "?U (Decided L 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 (proped L m M)
then show ?case by (cases "(get_all_decided_decomposition M)") auto
qed
definition all_decomposition_implies :: "'a literal multiset set
⇒ (('a, 'l, 'm) ann_literal list × ('a, 'l, 'm) ann_literal list) list ⇒ bool" where
"all_decomposition_implies N S
⟷ (∀(Ls, seen) ∈ set S. unmark Ls ∪ N ⊨ps unmark 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 Ls ∪ N ⊨ps unmark 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 (fst l) ∪ N ⊨ps unmark (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_decided_decomposition M)"
shows "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}
⊨ps (λa. {#lit_of a#}) ` ⋃(set ` snd ` set (get_all_decided_decomposition M))"
using assms
proof (induct "length (get_all_decided_decomposition M)" arbitrary: M)
case 0
thus ?case by auto
next
case (Suc n) note IH = this(1) and length = this(2)
{
assume "length (get_all_decided_decomposition M) ≤ 1"
then obtain a b where g: "get_all_decided_decomposition M = (a, b) # []"
by (cases "get_all_decided_decomposition M") auto
moreover {
assume "a = []"
hence ?case using Suc.prems g by auto
}
moreover {
assume l: "length a = 1" and m: "is_decided (hd a)" and hd: "hd a ∈ set M"
hence "(λa. {#lit_of a#}) (hd a) ∈ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}" by auto
hence H: "unmark a ∪ N ⊆ N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}"
using l by (cases a) auto
have f1: "(λm. {#lit_of m#}) ` set a ∪ N ⊨ps (λm. {#lit_of m#}) ` set b"
using Suc.prems unfolding all_decomposition_implies_def g by simp
have ?case
unfolding g apply (rule true_clss_clss_subset) using f1 H by auto
}
ultimately have ?case using get_all_decided_decomposition_length_1_fst_empty_or_length_1 by blast
}
moreover {
assume "length (get_all_decided_decomposition M) > 1"
then obtain Ls0 seen0 M' where
Ls0: "get_all_decided_decomposition M = (Ls0, seen0) # get_all_decided_decomposition M'" and
length': "length (get_all_decided_decomposition M') = n" and
M'_in_M: "set M' ⊆ set M"
using length apply (induct M)
apply simp
by (rename_tac a M, case_tac a, case_tac "hd (get_all_decided_decomposition M)")
(auto simp add: subset_insertI2)
{
assume "n = 0"
hence "get_all_decided_decomposition M' = []" using length' by auto
hence ?case 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_decided_decomposition M' = (Ls1, seen1) # l"
using length' by (induct M', simp) (rename_tac a xs, case_tac a, auto)
have "all_decomposition_implies N (get_all_decided_decomposition M')"
using Suc.prems unfolding Ls0 all_decomposition_implies_def by auto
hence N: "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'}
⊨ps (λa. {#lit_of a#}) ` ⋃(set ` snd ` set (get_all_decided_decomposition M'))"
using IH length' by auto
have l: "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'}
⊆ N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}"
using M'_in_M by auto
hence ΨN: "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}
⊨ps (λa. {#lit_of a#}) ` ⋃(set ` snd ` set (get_all_decided_decomposition M'))"
using true_clss_clss_subset[OF l N] by auto
have "is_decided (hd Ls0)" and LS: "tl Ls0 = seen1 @ Ls1"
using get_all_decided_decomposition_hd_hd[of M] unfolding Ls0 Ls1 by auto
have LSM: "seen1 @ Ls1 = M'" using get_all_decided_decomposition_decomp[of M'] Ls1 by auto
have M': "set M' = Union (set ` snd ` set (get_all_decided_decomposition M'))
∪ {L |L. is_decided L ∧ L ∈ set M'}"
using get_all_decided_decomposition_snd_union by auto
{
assume "Ls0 ≠ []"
hence "hd Ls0 ∈ set M" using get_all_decided_decomposition_fst_empty_or_hd_in_M Ls0 by blast
hence "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M} ⊨p (λa. {#lit_of a#}) (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: "(λa. {#lit_of a#}) ` (⋃(set ` snd ` set (get_all_decided_decomposition M'))
∪ {L |L. is_decided L ∧ L ∈ set M'})
= (λa. {#lit_of a#}) `
⋃(set ` snd ` set (get_all_decided_decomposition M'))
∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'}"
by auto
have "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'} ⊨ps
(λa. {#lit_of a#}) ` (⋃(set ` snd ` set (get_all_decided_decomposition M'))
∪ {L |L. is_decided L ∧ L ∈ set M'})"
unfolding l using N by (auto simp add: all_in_true_clss_clss)
hence "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'} ⊨ps unmark (tl Ls0)"
using M' unfolding LS LSM by auto
hence t: "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M'}
⊨ps unmark (tl Ls0)"
by (blast intro: all_in_true_clss_clss)
hence "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}
⊨ps unmark (tl Ls0)"
using M'_in_M true_clss_clss_subset[OF _ t,
of "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}"]
by auto
hence "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M} ⊨ps unmark Ls0"
using hd_Ls0 by (cases Ls0, auto)
moreover have "unmark Ls0 ∪ N ⊨ps unmark seen0"
using Suc.prems unfolding Ls0 all_decomposition_implies_def by simp
moreover have "⋀M Ma. (M::'a literal multiset set) ∪ Ma ⊨ps M"
by (simp add: all_in_true_clss_clss)
ultimately have Ψ: "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M} ⊨ps
unmark seen0"
by (meson true_clss_clss_left_right true_clss_clss_union_and true_clss_clss_union_l_r)
have "(λa. {#lit_of a#})`(set seen0
∪ (⋃x∈set (get_all_decided_decomposition M'). set (snd x)))
= unmark seen0
∪ (λa. {#lit_of a#}) ` (⋃x∈set (get_all_decided_decomposition M'). set (snd x))"
by auto
hence ?case unfolding Ls0 using Ψ ΨN by simp
}
ultimately have ?case by auto
}
ultimately show ?case by arith
qed
lemma all_decomposition_implies_propagated_lits_are_implied:
assumes "all_decomposition_implies N (get_all_decided_decomposition M)"
shows "N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M} ⊨ps unmark M"
(is "?I ⊨ps ?A")
proof -
have "?I ⊨ps (λa. {#lit_of a#}) ` {L |L. is_decided L ∧ L ∈ set M}"
by (auto intro: all_in_true_clss_clss)
moreover have "?I ⊨ps (λa. {#lit_of a#}) ` ⋃(set ` snd ` set (get_all_decided_decomposition M))"
using all_decomposition_implies_trail_is_implied assms by blast
ultimately have "N ∪ {{#lit_of m#} |m. is_decided m ∧ m ∈ set M}
⊨ps (λm. {#lit_of m#}) ` ⋃(set ` snd ` set (get_all_decided_decomposition M))
∪ (λm. {#lit_of m#}) ` {m |m. is_decided m ∧ m ∈ set M}"
by blast
thus ?thesis
by (metis (no_types) get_all_decided_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
subsection ‹Negation of Clauses›
text ‹We define the negation of a @{typ "'a clause"}: it converts it from the a single clause to
a set of clauses, wherein each clause is a single negated literal.›
definition CNot :: "'v clause ⇒ 'v clauses" where
"CNot ψ = { {#-L#} | L. L ∈# ψ }"
lemma in_CNot_uminus[iff]:
shows "{#L#} ∈ CNot ψ ⟷ -L ∈# ψ"
using assms unfolding CNot_def by force
lemma CNot_singleton[simp]: "CNot {#L#} = {{#-L#}}" unfolding CNot_def by auto
lemma CNot_empty[simp]: "CNot {#} = {}" unfolding CNot_def by auto
lemma 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 M"
using assms by (auto simp add: 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 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
hence "¬I ⊨s insert {#L#} B"
using assms cons unfolding true_clss_cls_def by simp
thus "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 M)"
unfolding CNot_def true_annots_true_cls true_clss_def by 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 uminus_lit_swap: "-(a::'a literal) = i ⟷ a = -i"
by auto
lemma true_clss_cls_plus_CNot:
assumes
CC_L: "A ⊨p CC + {#L#}" 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 add: 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 add: total_over_m_def total_over_set_def)
hence tot_I_A_CC_L: "total_over_m ?I (A ∪ {CC + {#L#}})"
using tot unfolding total_over_m_def total_over_set_atm_of by auto
hence "?I ⊨ CC + {#L#}" 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
hence "¬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)
hence "¬?I ⊨ CC" using ‹?I ⊨s CNot CC› cons' consistent_CNot_not by blast
ultimately have "?I ⊨ {#L#}" by blast
thus "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"
hence "L # M ⊨a l" by auto
thus "M ⊨a l" using LA l by (cases L) (auto simp add: 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 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 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 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 " ¬ lits_of A ⊨l - L"
hence "atm_of L ∈ atm_of ` lits_of A"
using assms(1) by (simp add: atm_of_lit_in_atms_of lits_of_def)
hence "L ∈ lits_of A ∨ -L ∈ lits_of A"
using atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set by metis
hence "L ∈ lits_of A" using ‹ ¬ lits_of A ⊨l - L› by auto
thus False
using LB assms(2) unfolding true_annot_def true_lit_def true_cls_def Bex_mset_def
by blast
qed
lemma CNot_union_mset[simp]:
"CNot (A #∪ B) = CNot A ∪ CNot B"
unfolding CNot_def by auto
subsection ‹Other›
abbreviation "no_dup L ≡ distinct (map (λl. atm_of (lit_of l)) L)"
lemma no_dup_rev[simp]:
"no_dup (rev M) ⟷ no_dup M"
by (auto simp: rev_map[symmetric])
lemma no_dup_length_eq_card_atm_of_lits_of:
assumes "no_dup M"
shows "length M = card (atm_of ` lits_of M)"
using assms unfolding lits_of_def by (induct M) (auto simp add: image_image)
lemma distinctconsistent_interp:
"no_dup M ⟹ consistent_interp (lits_of M)"
proof (induct M)
case Nil
show ?case by auto
next
case (Cons L M)
hence a1: "consistent_interp (lits_of M)" by auto
have a2: "atm_of (lit_of L) ∉ (λl. atm_of (lit_of l)) ` set M" using Cons.prems by auto
have "undefined_lit M (lit_of L)"
using a2 unfolding defined_lit_map by fastforce
then show ?case
using a1 by simp
qed
lemma distinct_get_all_decided_decomposition_no_dup:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
and "no_dup M"
shows "no_dup (a @ b)"
using assms by force
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 # M)"
using assms(1) in_CNot_implies_uminus(2) by blast
moreover
have "atm_of (lit_of L) ∉ atm_of ` lits_of M"
using assms(3) unfolding lits_of_def by force
hence "- lit_of L ∉ lits_of M" unfolding lits_of_def
by (metis (no_types) atm_of_uminus imageI)
ultimately have "∀ l ∈# A. -l ∈ lits_of M"
using assms(2) unfolding Ball_mset_def by (metis insertE lits_of_cons uminus_of_uminus_id)
thus ?thesis by (auto simp add: true_annots_def)
qed
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).›
type_synonym 'v clauses = "'v clause multiset"
abbreviation true_annots_mset (infix "⊨asm" 50) where
"I ⊨asm C ≡ I ⊨as (set_mset C)"
abbreviation true_clss_clss_m:: "'a clauses ⇒ 'a clauses ⇒ bool" (infix "⊨psm" 50) where
"I ⊨psm C ≡ set_mset I ⊨ps (set_mset C)"
text ‹Analog of @{thm 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 clauses ⇒ '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_msu where
"atms_of_msu U ≡ atms_of_ms (set_mset U)"
abbreviation true_clss_m:: "'a interp ⇒ 'a clauses ⇒ 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"
end