section {* Clausal Logic *}
theory Clausal_Logic
imports "../lib/Multiset_More"
begin
text {*
Resolution operates of clauses, which are disjunctions of literals. The material formalized here
corresponds roughly to Sections 2.1 (``Formulas and Clauses'') of Bachmair and Ganzinger, excluding
the formula and term syntax.
*}
subsection {* Literals *}
text {*
Literals consist of a polarity (positive or negative) and an atom, of type @{typ 'a}.
*}
datatype 'a literal =
is_pos: Pos (atm_of: 'a)
| Neg (atm_of: 'a)
abbreviation is_neg :: "'a literal ⇒ bool" where "is_neg L ≡ ¬ is_pos L"
lemma Pos_atm_of_iff[simp]: "Pos (atm_of L) = L ⟷ is_pos L"
by auto (metis literal.disc(1))
lemma Neg_atm_of_iff[simp]: "Neg (atm_of L) = L ⟷ is_neg L"
by auto (metis literal.disc(2))
lemma ex_lit_cases: "(∃L. P L) ⟷ (∃A. P (Pos A) ∨ P (Neg A))"
by (metis literal.exhaust)
instantiation literal :: (type) uminus
begin
definition uminus_literal :: "'a literal ⇒ 'a literal" where
"uminus L = (if is_pos L then Neg else Pos) (atm_of L)"
instance ..
end
lemma
uminus_Pos[simp]: "- Pos A = Neg A" and
uminus_Neg[simp]: "- Neg A = Pos A"
unfolding uminus_literal_def by simp_all
lemma atm_of_uminus[simp]:
"atm_of (-L) = atm_of L"
by (case_tac L, auto)
lemma uminus_of_uminus_id[simp]:
"- (- (x:: 'v literal)) = x"
by (simp add: uminus_literal_def)
lemma uminus_not_id[simp]:
"x ≠ - (x:: 'v literal)"
by (case_tac x, auto)
lemma uminus_not_id'[simp]:
"- x ≠ (x:: 'v literal)"
by (case_tac x, auto)
lemma uminus_eq_inj[iff]:
"-(a::'v literal) = -b ⟷ a = b"
by (case_tac a; case_tac b) auto+
lemma uminus_lit_swap:
"(a::'a literal) = -b ⟷ -a = b"
by auto
instantiation literal :: (preorder) preorder
begin
definition less_literal :: "'a literal ⇒ 'a literal ⇒ bool" where
"less_literal L M ⟷ atm_of L < atm_of M ∨ atm_of L ≤ atm_of M ∧ is_neg L < is_neg M"
definition less_eq_literal :: "'a literal ⇒ 'a literal ⇒ bool" where
"less_eq_literal L M ⟷ atm_of L < atm_of M ∨ atm_of L ≤ atm_of M ∧ is_neg L ≤ is_neg M"
instance
apply intro_classes
unfolding less_literal_def less_eq_literal_def by (auto intro: order_trans simp: less_le_not_le)
end
instantiation literal :: (order) order
begin
instance
apply intro_classes
unfolding less_eq_literal_def by (auto intro: literal.expand)
end
lemma pos_less_neg[simp]: "Pos A < Neg A"
unfolding less_literal_def by simp
lemma pos_less_pos_iff[simp]: "Pos A < Pos B ⟷ A < B"
unfolding less_literal_def by simp
lemma pos_less_neg_iff[simp]: "Pos A < Neg B ⟷ A ≤ B"
unfolding less_literal_def by (auto simp: less_le_not_le)
lemma neg_less_pos_iff[simp]: "Neg A < Pos B ⟷ A < B"
unfolding less_literal_def by simp
lemma neg_less_neg_iff[simp]: "Neg A < Neg B ⟷ A < B"
unfolding less_literal_def by simp
lemma pos_le_neg[simp]: "Pos A ≤ Neg A"
unfolding less_eq_literal_def by simp
lemma pos_le_pos_iff[simp]: "Pos A ≤ Pos B ⟷ A ≤ B"
unfolding less_eq_literal_def by (auto simp: less_le_not_le)
lemma pos_le_neg_iff[simp]: "Pos A ≤ Neg B ⟷ A ≤ B"
unfolding less_eq_literal_def by (auto simp: less_imp_le)
lemma neg_le_pos_iff[simp]: "Neg A ≤ Pos B ⟷ A < B"
unfolding less_eq_literal_def by simp
lemma neg_le_neg_iff[simp]: "Neg A ≤ Neg B ⟷ A ≤ B"
unfolding less_eq_literal_def by (auto simp: less_imp_le)
lemma leq_imp_less_eq_atm_of: "L ≤ M ⟹ atm_of L ≤ atm_of M"
by (metis less_eq_literal_def less_le_not_le)
instantiation literal :: (linorder) linorder
begin
instance
apply intro_classes
unfolding less_eq_literal_def less_literal_def by auto
end
instantiation literal :: (wellorder) wellorder
begin
instance
proof intro_classes
fix P :: "'a literal ⇒ bool" and L :: "'a literal"
assume ih: "⋀L. (⋀M. M < L ⟹ P M) ⟹ P L"
have "⋀x. (⋀y. y < x ⟹ P (Pos y) ∧ P (Neg y)) ⟹ P (Pos x) ∧ P (Neg x)"
by (rule conjI[OF ih ih])
(auto simp: less_literal_def atm_of_def split: literal.splits intro: ih)
hence "⋀A. P (Pos A) ∧ P (Neg A)"
by (rule less_induct) blast
thus "P L"
by (cases L) simp+
qed
end
subsection {* Clauses *}
text {*
Clauses are (finite) multisets of literals.
*}
type_synonym 'a clause = "'a literal multiset"
abbreviation poss :: "'a multiset ⇒ 'a clause" where "poss AA ≡ {#Pos A. A ∈# AA#}"
abbreviation negs :: "'a multiset ⇒ 'a clause" where "negs AA ≡ {#Neg A. A ∈# AA#}"
lemma image_replicate_mset[simp]: "{#f A. A ∈# replicate_mset n A#} = replicate_mset n (f A)"
by (induct n) (simp, subst replicate_mset_Suc, simp)
lemma Max_in_lits: "C ≠ {#} ⟹ Max (set_mset C) ∈# C"
by (rule Max_in[OF finite_set_mset, unfolded mem_set_mset_iff set_mset_eq_empty_iff])
lemma Max_atm_of_set_mset_commute: "C ≠ {#} ⟹ Max (atm_of ` set_mset C) = atm_of (Max (set_mset C))"
by (rule mono_Max_commute[symmetric])
(auto simp: mono_def atm_of_def less_eq_literal_def less_literal_def)
lemma Max_pos_neg_less_multiset:
assumes max: "Max (set_mset C) = Pos A" and neg: "Neg A ∈# D"
shows "C #⊂# D"
proof -
have "Max (set_mset C) < Neg A"
using max by simp
thus ?thesis
using neg by (metis (no_types) ex_gt_imp_less_multiset Max_less_iff[OF finite_set_mset]
all_not_in_conv mem_set_mset_iff)
qed
lemma pos_Max_imp_neg_notin: "Max (set_mset C) = Pos A ⟹ ¬ Neg A ∈# C"
using Max_pos_neg_less_multiset[unfolded multiset_linorder.not_le[symmetric]] by blast
lemma less_eq_Max_lit: "C ≠ {#} ⟹ C #⊆# D ⟹ Max (set_mset C) ≤ Max (set_mset D)"
proof (unfold le_multiset⇩H⇩O)
assume ne: "C ≠ {#}" and ex_gt: "∀x. count D x < count C x ⟶ (∃y > x. count C y < count D y)"
from ne have "Max (set_mset C) ∈# C"
by (fast intro: Max_in_lits)
hence "∃l. l ∈# D ∧ ¬ l < Max (set_mset C)"
using ex_gt by (metis not_less0 not_less_iff_gr_or_eq)
hence "¬ Max (set_mset D) < Max (set_mset C)"
by (metis Max.coboundedI[OF finite_set_mset] le_less_trans mem_set_mset_iff)
thus ?thesis
by simp
qed
definition atms_of :: "'a clause ⇒ 'a set" where
"atms_of C = atm_of ` set_mset C"
lemma atms_of_empty[simp]: "atms_of {#} = {}"
unfolding atms_of_def by simp
lemma atms_of_singleton[simp]: "atms_of {#L#} = {atm_of L}"
unfolding atms_of_def by auto
lemma atms_of_union_mset[simp]:
"atms_of (A #∪ B) = atms_of A ∪ atms_of B"
unfolding atms_of_def by (auto simp: max_def split: split_if_asm)
lemma finite_atms_of[iff]: "finite (atms_of C)"
unfolding atms_of_def by simp
lemma atm_of_lit_in_atms_of: "L ∈# C ⟹ atm_of L ∈ atms_of C"
unfolding atms_of_def by simp
lemma atms_of_plus[simp]: "atms_of (C + D) = atms_of C ∪ atms_of D"
unfolding atms_of_def image_def by auto
lemma pos_lit_in_atms_of: "Pos A ∈# C ⟹ A ∈ atms_of C"
unfolding atms_of_def by (metis image_iff literal.sel(1) mem_set_mset_iff)
lemma neg_lit_in_atms_of: "Neg A ∈# C ⟹ A ∈ atms_of C"
unfolding atms_of_def by (metis image_iff literal.sel(2) mem_set_mset_iff)
lemma atm_imp_pos_or_neg_lit: "A ∈ atms_of C ⟹ Pos A ∈# C ∨ Neg A ∈# C"
unfolding atms_of_def image_def mem_Collect_eq
by (metis Neg_atm_of_iff Pos_atm_of_iff mem_set_mset_iff)
lemma atm_iff_pos_or_neg_lit: "A ∈ atms_of L ⟷ Pos A ∈# L ∨ Neg A ∈# L"
by (auto intro: pos_lit_in_atms_of neg_lit_in_atms_of dest: atm_imp_pos_or_neg_lit)
lemma atm_of_eq_atm_of:
"atm_of L = atm_of L' ⟷ (L = L' ∨ L = -L')"
by (cases L; cases L') auto
lemma atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set:
"atm_of L ∈ atm_of ` I ⟷ (L ∈ I ∨ -L ∈ I)"
by (auto intro: rev_image_eqI simp: atm_of_eq_atm_of)
lemma lits_subseteq_imp_atms_subseteq: "set_mset C ⊆ set_mset D ⟹ atms_of C ⊆ atms_of D"
unfolding atms_of_def by blast
lemma atms_empty_iff_empty[iff]: "atms_of C = {} ⟷ C = {#}"
unfolding atms_of_def image_def Collect_empty_eq
by (metis all_not_in_conv set_mset_eq_empty_iff)
lemma
atms_of_poss[simp]: "atms_of (poss AA) = set_mset AA" and
atms_of_negg[simp]: "atms_of (negs AA) = set_mset AA"
unfolding atms_of_def image_def by auto
lemma less_eq_Max_atms_of: "C ≠ {#} ⟹ C #⊆# D ⟹ Max (atms_of C) ≤ Max (atms_of D)"
unfolding atms_of_def
by (metis Max_atm_of_set_mset_commute le_multiset_empty_right leq_imp_less_eq_atm_of
less_eq_Max_lit)
lemma le_multiset_Max_in_imp_Max:
"Max (atms_of D) = A ⟹ C #⊆# D ⟹ A ∈ atms_of C ⟹ Max (atms_of C) = A"
by (metis Max.coboundedI[OF finite_atms_of] atms_of_def empty_iff eq_iff image_subsetI
less_eq_Max_atms_of set_mset_empty subset_Compl_self_eq)
lemma atm_of_Max_lit[simp]: "C ≠ {#} ⟹ atm_of (Max (set_mset C)) = Max (atms_of C)"
unfolding atms_of_def Max_atm_of_set_mset_commute ..
lemma Max_lit_eq_pos_or_neg_Max_atm:
"C ≠ {#} ⟹ Max (set_mset C) = Pos (Max (atms_of C)) ∨ Max (set_mset C) = Neg (Max (atms_of C))"
by (metis Neg_atm_of_iff Pos_atm_of_iff atm_of_Max_lit)
lemma atms_less_imp_lit_less_pos: "(⋀B. B ∈ atms_of C ⟹ B < A) ⟹ L ∈# C ⟹ L < Pos A"
unfolding atms_of_def less_literal_def by force
lemma atms_less_eq_imp_lit_less_eq_neg: "(⋀B. B ∈ atms_of C ⟹ B ≤ A) ⟹ L ∈# C ⟹ L ≤ Neg A"
unfolding less_eq_literal_def by (simp add: atm_of_lit_in_atms_of)
end