Theory Ground_Superposition
theory Ground_Superposition
imports
Ground_Critical_Pairs
First_Order_Clause.Selection_Function
First_Order_Clause.Ground_Order
First_Order_Clause.Ground_Clause
begin
section ‹Superposition Calculus›
locale ground_superposition_calculus =
ground_order_with_equality where less⇩t = less⇩t +
selection_function select +
ground_critical_pair_theorem "TYPE('f)"
for
less⇩t :: "'f gterm ⇒ 'f gterm ⇒ bool" and
select :: "'f gatom clause ⇒ 'f gatom clause"
begin
subsection ‹Ground Rules›
inductive superposition ::
"'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
superpositionI: "
E = add_mset L⇩E E' ⟹
D = add_mset L⇩D D' ⟹
D ≺⇩c E ⟹
𝒫 ∈ {Pos, Neg} ⟹
L⇩E = 𝒫 (Upair κ⟨t⟩⇩G u) ⟹
L⇩D = t ≈ t' ⟹
u ≺⇩t κ⟨t⟩⇩G ⟹
t' ≺⇩t t ⟹
(𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal L⇩E E) ∨
(𝒫 = Neg ∧ (select E = {#} ∧ is_maximal L⇩E E ∨ is_maximal L⇩E (select E))) ⟹
select D = {#} ⟹
is_strictly_maximal L⇩D D ⟹
C = add_mset (𝒫 (Upair κ⟨t'⟩⇩G u)) (E' + D') ⟹
superposition D E C"
inductive eq_resolution :: "'f gatom clause ⇒ 'f gatom clause ⇒ bool" where
eq_resolutionI: "
D = add_mset L D' ⟹
L = t !≈ t ⟹
select D = {#} ∧ is_maximal L D ∨ is_maximal L (select D) ⟹
C = D' ⟹
eq_resolution D C"
inductive eq_factoring :: "'f gatom clause ⇒ 'f gatom clause ⇒ bool" where
eq_factoringI: "
D = add_mset L⇩1 (add_mset L⇩2 D') ⟹
L⇩1 = t ≈ t' ⟹
L⇩2 = t ≈ t'' ⟹
select D = {#} ⟹
is_maximal L⇩1 D ⟹
t' ≺⇩t t ⟹
C = add_mset (t' !≈ t'') (add_mset (t ≈ t'') D') ⟹
eq_factoring D C"
abbreviation eq_resolution_inferences where
"eq_resolution_inferences ≡ {Infer [D] C | D C. eq_resolution D C}"
abbreviation eq_factoring_inferences where
"eq_factoring_inferences ≡ {Infer [D] C | D C. eq_factoring D C}"
abbreviation superposition_inferences where
"superposition_inferences ≡ {Infer [D, E] C | D E C. superposition D E C}"
subsubsection ‹Alternative Specification of the Superposition Rule›
inductive superposition' ::
"'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
superposition'I: "
P⇩1 = add_mset L⇩1 P⇩1' ⟹
P⇩2 = add_mset L⇩2 P⇩2' ⟹
P⇩2 ≺⇩c P⇩1 ⟹
𝒫 ∈ {Pos, Neg} ⟹
L⇩1 = 𝒫 (Upair s⟨t⟩⇩G s') ⟹
L⇩2 = t ≈ t' ⟹
s' ≺⇩t s⟨t⟩⇩G ⟹
t' ≺⇩t t ⟹
(𝒫 = Pos ⟶ select P⇩1 = {#} ∧ is_strictly_maximal L⇩1 P⇩1) ⟹
(𝒫 = Neg ⟶ (select P⇩1 = {#} ∧ is_maximal L⇩1 P⇩1 ∨ is_maximal L⇩1 (select P⇩1))) ⟹
select P⇩2 = {#} ⟹
is_strictly_maximal L⇩2 P⇩2 ⟹
C = add_mset (𝒫 (Upair s⟨t'⟩⇩G s')) (P⇩1' + P⇩2') ⟹
superposition' P⇩2 P⇩1 C"
lemma "superposition' = superposition"
proof (intro ext iffI)
fix P1 P2 C
assume "superposition' P2 P1 C"
thus "superposition P2 P1 C"
proof (cases P2 P1 C rule: superposition'.cases)
case (superposition'I L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
thus ?thesis
using superpositionI
by force
qed
next
fix P1 P2 C
assume "superposition P1 P2 C"
thus "superposition' P1 P2 C"
proof (cases P1 P2 C rule: superposition.cases)
case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
thus ?thesis
using superposition'I
by (metis literals_distinct(2))
qed
qed
inductive pos_superposition ::
"'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
pos_superpositionI: "
P⇩1 = add_mset L⇩1 P⇩1' ⟹
P⇩2 = add_mset L⇩2 P⇩2' ⟹
P⇩2 ≺⇩c P⇩1 ⟹
L⇩1 = s⟨t⟩⇩G ≈ s' ⟹
L⇩2 = t ≈ t' ⟹
s' ≺⇩t s⟨t⟩⇩G ⟹
t' ≺⇩t t ⟹
select P⇩1 = {#} ⟹
is_strictly_maximal L⇩1 P⇩1 ⟹
select P⇩2 = {#} ⟹
is_strictly_maximal L⇩2 P⇩2 ⟹
C = add_mset (s⟨t'⟩⇩G ≈ s') (P⇩1' + P⇩2') ⟹
pos_superposition P⇩2 P⇩1 C"
lemma superposition_if_pos_superposition:
assumes step: "pos_superposition P⇩2 P⇩1 C"
shows "superposition P⇩2 P⇩1 C"
using step
proof (cases P⇩2 P⇩1 C rule: pos_superposition.cases)
case (pos_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
thus ?thesis
using superpositionI
by (metis insert_iff)
qed
inductive neg_superposition ::
"'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
neg_superpositionI:
"P⇩1 = add_mset L⇩1 P⇩1' ⟹
P⇩2 = add_mset L⇩2 P⇩2' ⟹
P⇩2 ≺⇩c P⇩1 ⟹
L⇩1 = s⟨t⟩⇩G !≈ s' ⟹
L⇩2 = t ≈ t' ⟹
s' ≺⇩t s⟨t⟩⇩G ⟹
t' ≺⇩t t ⟹
select P⇩1 = {#} ∧ is_maximal L⇩1 P⇩1 ∨ is_maximal L⇩1 (select P⇩1) ⟹
select P⇩2 = {#} ⟹
is_strictly_maximal L⇩2 P⇩2 ⟹
C = add_mset (Neg (Upair s⟨t'⟩⇩G s')) (P⇩1' + P⇩2') ⟹
neg_superposition P⇩2 P⇩1 C"
lemma superposition_if_neg_superposition:
assumes "neg_superposition P⇩2 P⇩1 C"
shows "superposition P⇩2 P⇩1 C"
using assms
proof (cases P⇩2 P⇩1 C rule: neg_superposition.cases)
case (neg_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
then show ?thesis
using superpositionI
by (metis insert_iff)
qed
lemma superposition_iff_pos_or_neg:
"superposition P⇩2 P⇩1 C ⟷
pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
proof (rule iffI)
assume "superposition P⇩2 P⇩1 C"
thus "pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
proof (cases P⇩2 P⇩1 C rule: superposition.cases)
case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
then show ?thesis
using pos_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
using neg_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
by metis
qed
next
assume "pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
thus "superposition P⇩2 P⇩1 C"
using
superposition_if_neg_superposition
superposition_if_pos_superposition
by metis
qed
subsection ‹Ground Layer›
definition G_Inf :: "'f gatom clause inference set" where
"G_Inf =
{Infer [P⇩2, P⇩1] C | P⇩2 P⇩1 C. superposition P⇩2 P⇩1 C} ∪
{Infer [P] C | P C. eq_resolution P C} ∪
{Infer [P] C | P C. eq_factoring P C}"
abbreviation G_Bot :: "'f gatom clause set" where
"G_Bot ≡ {{#}}"
definition G_entails :: "'f gatom clause set ⇒ 'f gatom clause set ⇒ bool" where
"G_entails N⇩1 N⇩2 ⟷ (∀(I :: 'f gterm rel). refl I ⟶ trans I ⟶ sym I ⟶
compatible_with_gctxt I ⟶ upair ` I ⊫s N⇩1 ⟶ upair ` I ⊫s N⇩2)"
lemma superposition_smaller_conclusion:
assumes
step: "superposition P1 P2 C"
shows "C ≺⇩c P2"
using step
proof (cases P1 P2 C rule: superposition.cases)
case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
have "P⇩1' + add_mset (𝒫 (Upair s⟨t'⟩⇩G s')) P⇩2' ≺⇩c P⇩1' + {#𝒫 (Upair s⟨t⟩⇩G s')#}"
unfolding less⇩c_def
proof (intro one_step_implies_multp ballI)
fix K assume "K ∈# add_mset (𝒫 (Upair s⟨t'⟩⇩G s')) P⇩2'"
moreover have "𝒫 (Upair s⟨t'⟩⇩G s') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
proof -
have "s⟨t'⟩⇩G ≺⇩t s⟨t⟩⇩G"
using ‹t' ≺⇩t t›
by simp
hence "multp (≺⇩t) {#s⟨t'⟩⇩G, s'#} {#s⟨t⟩⇩G, s'#}"
by (simp add: add_mset_commute multp_cancel_add_mset)
have ?thesis if "𝒫 = Pos"
unfolding that less⇩l_def
using ‹multp (≺⇩t) {#s⟨t'⟩⇩G, s'#} {#s⟨t⟩⇩G, s'#}›
by simp
moreover have ?thesis if "𝒫 = Neg"
unfolding that less⇩l_def
using ‹multp (≺⇩t) {#s⟨t'⟩⇩G, s'#} {#s⟨t⟩⇩G, s'#}› multp_double_doubleI
by force
ultimately show ?thesis
using ‹𝒫 ∈ {Pos, Neg}›
by auto
qed
moreover have "∀K ∈# P⇩2'. K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
proof -
have "is_strictly_maximal L⇩2 P1"
using superpositionI
by argo
hence "∀K ∈# P⇩2'. ¬ Pos (Upair t t') ≺⇩l K ∧ Pos (Upair t t') ≠ K"
unfolding
is_strictly_maximal_def
‹P1 = add_mset L⇩2 P⇩2'› ‹L⇩2 = t ≈ t'›
by simp
hence "∀K ∈# P⇩2'. K ≺⇩l Pos (Upair t t')"
by auto
have thesis_if_Neg: "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
if "𝒫 = Neg"
proof -
have "t ≼⇩t s⟨t⟩⇩G"
using term.order.less_eq_subterm_property .
hence "multp (≺⇩t) {#t, t'#} {#s⟨t⟩⇩G, s', s⟨t⟩⇩G, s'#}"
unfolding reflclp_iff
proof (elim disjE)
assume "t ≺⇩t s⟨t⟩⇩G"
moreover hence "t' ≺⇩t s⟨t⟩⇩G"
using superpositionI(8)
by order
ultimately show ?thesis
by (auto intro: one_step_implies_multp[of _ _ _ "{#}", simplified])
next
assume "t = s⟨t⟩⇩G"
thus ?thesis
using ‹t' ≺⇩t t›
by simp
qed
thus "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
using ‹𝒫 = Neg›
by (simp add: less⇩l_def)
qed
have thesis_if_Pos: "Pos (Upair t t') ≼⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
if "𝒫 = Pos" and "is_maximal L⇩1 P2"
proof (cases "s")
case Hole
show ?thesis
proof (cases "t' ≼⇩t s'")
case True
hence "(multp (≺⇩t))⇧=⇧= {#t, t'#} {#s⟨t⟩⇩G, s'#}"
unfolding Hole
by (simp add: multp_cancel_add_mset)
thus ?thesis
unfolding Hole ‹𝒫 = Pos›
by (auto simp: less⇩l_def)
next
case False
hence "s' ≺⇩t t'"
by order
hence "multp (≺⇩t) {#s⟨t⟩⇩G, s'#} {#t, t'#}"
by (simp add: Hole multp_cancel_add_mset)
hence "𝒫 (Upair s⟨t⟩⇩G s') ≺⇩l Pos (Upair t t')"
using ‹𝒫 = Pos›
by (simp add: less⇩l_def)
moreover have "∀K ∈# P⇩1'. K ≼⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
using that
unfolding superpositionI is_maximal_def
by auto
ultimately have "∀K ∈# P⇩1'. K ≼⇩l Pos (Upair t t')"
by auto
hence "P2 ≺⇩c P1"
using
‹𝒫 (Upair s⟨t⟩⇩G s') ≺⇩l Pos (Upair t t')›
one_step_implies_multp[of P1 P2 "(≺⇩l)" "{#}", simplified]
literal.order.multp_if_maximal_less_that_maximal
superpositionI
that
unfolding less⇩c_def
by blast
hence False
using ‹P1 ≺⇩c P2› by order
thus ?thesis ..
qed
next
case (More f ts1 ctxt ts2)
hence "t ≺⇩t s⟨t⟩⇩G"
using term.order.subterm_property[of s t]
by simp
moreover hence "t' ≺⇩t s⟨t⟩⇩G"
using ‹t' ≺⇩t t›
by order
ultimately have "multp (≺⇩t) {#t, t'#} {#s⟨t⟩⇩G, s'#}"
using one_step_implies_multp[of "{#s⟨t⟩⇩G, s'#}" "{#t, t'#}" "(≺⇩t)" "{#}"]
by simp
hence "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
using ‹𝒫 = Pos›
by (simp add: less⇩l_def)
thus ?thesis
by order
qed
have "𝒫 = Pos ∨ 𝒫 = Neg"
using ‹𝒫 ∈ {Pos, Neg}›
by simp
thus ?thesis
proof (elim disjE; intro ballI)
fix K assume "𝒫 = Pos" "K ∈# P⇩2'"
have "K ≺⇩l t ≈ t'"
using ‹∀K∈#P⇩2'. K ≺⇩l t ≈ t'› ‹K ∈# P⇩2'›
by metis
also have "t ≈ t' ≼⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
proof (rule thesis_if_Pos[OF ‹𝒫 = Pos›])
have "is_strictly_maximal L⇩1 P2"
using ‹𝒫 = Pos› superpositionI
by simp
thus "is_maximal L⇩1 P2"
by blast
qed
finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')" .
next
fix K assume "𝒫 = Neg" "K ∈# P⇩2'"
have "K ≺⇩l t ≈ t'"
using ‹∀K∈#P⇩2'. K ≺⇩l t ≈ t'› ‹K ∈# P⇩2'›
by metis
also have "t ≈ t' ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
using thesis_if_Neg[OF ‹𝒫 = Neg›] .
finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')" .
qed
qed
ultimately show "∃j ∈# {#𝒫 (Upair s⟨t⟩⇩G s')#}. K ≺⇩l j"
by auto
qed simp
moreover have "C = add_mset (𝒫 (Upair s⟨t'⟩⇩G s')) (P⇩1' + P⇩2')"
unfolding superpositionI ..
moreover have "P2 = P⇩1' + {#𝒫 (Upair s⟨t⟩⇩G s')#}"
unfolding superpositionI by simp
ultimately show ?thesis
by simp
qed
lemma ground_eq_resolution_smaller_conclusion:
assumes step: "eq_resolution P C"
shows "C ≺⇩c P"
using step
proof (cases P C rule: eq_resolution.cases)
case (eq_resolutionI L t)
then show ?thesis
unfolding less⇩c_def
by (metis add.left_neutral add_mset_add_single empty_not_add_mset multi_member_split
one_step_implies_multp union_commute)
qed
lemma ground_eq_factoring_smaller_conclusion:
assumes step: "eq_factoring P C"
shows "C ≺⇩c P"
using step
proof (cases P C rule: eq_factoring.cases)
case (eq_factoringI L⇩1 L⇩2 P' t t' t'')
have "is_maximal L⇩1 P"
using eq_factoringI
by simp
hence "∀K ∈# add_mset (Pos (Upair t t'')) P'. ¬ Pos (Upair t t') ≺⇩l K"
unfolding eq_factoringI is_maximal_def
by auto
hence "¬ Pos (Upair t t') ≺⇩l Pos (Upair t t'')"
by simp
hence "Pos (Upair t t'') ≼⇩l Pos (Upair t t')"
by order
hence "t'' ≼⇩t t'"
unfolding reflclp_iff
by (auto simp: less⇩l_def multp_cancel_add_mset)
have "C = add_mset (Neg (Upair t' t'')) (add_mset (Pos (Upair t t'')) P')"
using eq_factoringI
by argo
moreover have "add_mset (Neg (Upair t' t'')) (add_mset (Pos (Upair t t'')) P') ≺⇩c P"
unfolding eq_factoringI less⇩c_def
proof (intro one_step_implies_multp[of "{#_#}" "{#_#}", simplified])
have "t'' ≺⇩t t"
using ‹t' ≺⇩t t› ‹t'' ≼⇩t t'›
by order
hence "multp (≺⇩t) {#t', t'', t', t''#} {#t, t'#}"
using one_step_implies_multp[of _ _ _ "{#}", simplified]
by (metis ‹t' ≺⇩t t› diff_empty id_remove_1_mset_iff_notin insert_iff
set_mset_add_mset_insert)
thus "Neg (Upair t' t'') ≺⇩l Pos (Upair t t')"
by (simp add: less⇩l_def)
qed
ultimately show ?thesis
by argo
qed
sublocale consequence_relation where Bot = G_Bot and entails = G_entails
proof unfold_locales
show "G_Bot ≠ {}"
by simp
next
show "⋀B N. B ∈ G_Bot ⟹ G_entails {B} N"
by (simp add: G_entails_def)
next
show "⋀N2 N1. N2 ⊆ N1 ⟹ G_entails N1 N2"
by (auto simp: G_entails_def elim!: true_clss_mono[rotated])
next
fix N1 N2 assume ball_G_entails: "∀C ∈ N2. G_entails N1 {C}"
show "G_entails N1 N2"
unfolding G_entails_def
proof (intro allI impI)
fix I :: "'f gterm rel"
assume "refl I" and "trans I" and "sym I" and "compatible_with_gctxt I" and
"(λ(x, y). Upair x y) ` I ⊫s N1"
hence "∀C ∈ N2. (λ(x, y). Upair x y) ` I ⊫s {C}"
using ball_G_entails
by (simp add: G_entails_def)
then show "(λ(x, y). Upair x y) ` I ⊫s N2"
by (simp add: true_clss_def)
qed
next
show "⋀N1 N2 N3. G_entails N1 N2 ⟹ G_entails N2 N3 ⟹ G_entails N1 N3"
using G_entails_def
by simp
qed
subsection ‹Redundancy Criterion›
sublocale calculus_with_finitary_standard_redundancy where
Inf = G_Inf and
Bot = G_Bot and
entails = G_entails and
less = "(≺⇩c)"
defines GRed_I = Red_I and GRed_F = Red_F
proof unfold_locales
show "transp (≺⇩c)"
by simp
next
show "wfP (≺⇩c)"
by auto
next
show "⋀ι. ι ∈ G_Inf ⟹ prems_of ι ≠ []"
by (auto simp: G_Inf_def)
next
fix ι
have "concl_of ι ≺⇩c main_prem_of ι"
if ι_def: "ι = Infer [P⇩2, P⇩1] C" and
infer: "superposition P⇩2 P⇩1 C"
for P⇩2 P⇩1 C
unfolding ι_def
using infer
using superposition_smaller_conclusion
by simp
moreover have "concl_of ι ≺⇩c main_prem_of ι"
if ι_def: "ι = Infer [P] C" and
infer: "eq_resolution P C"
for P C
unfolding ι_def
using infer
using ground_eq_resolution_smaller_conclusion
by simp
moreover have "concl_of ι ≺⇩c main_prem_of ι"
if ι_def: "ι = Infer [P] C" and
infer: "eq_factoring P C"
for P C
unfolding ι_def
using infer
using ground_eq_factoring_smaller_conclusion
by simp
ultimately show "ι ∈ G_Inf ⟹ concl_of ι ≺⇩c main_prem_of ι"
unfolding G_Inf_def
by fast
qed
lemma redundant_infer_singleton:
assumes "∃D∈N. G_entails (insert D (set (side_prems_of ι))) {concl_of ι} ∧ D ≺⇩c main_prem_of ι"
shows "redundant_infer N ι"
proof-
obtain D where D:
"D ∈ N"
"G_entails (insert D (set (side_prems_of ι))) {concl_of ι}"
"D ≺⇩c main_prem_of ι"
using assms
by blast
show ?thesis
unfolding redundant_infer_def
by (rule exI[of _ "{D}"]) (auto simp: D)
qed
end
end