Theory Superposition
theory Superposition
imports
First_Order_Clause.Nonground_Order
First_Order_Clause.Nonground_Selection_Function
First_Order_Clause.Nonground_Typing
First_Order_Clause.Typed_Tiebreakers
First_Order_Clause.Welltyped_IMGU
Ground_Superposition
begin
section ‹Nonground Layer›
locale superposition_calculus =
nonground_inhabited_typing ℱ +
nonground_equality_order less⇩t +
nonground_selection_function select +
typed_tiebreakers tiebreakers +
ground_critical_pair_theorem "TYPE('f)"
for
select :: "('f, 'v :: infinite) select" and
less⇩t :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" and
ℱ :: "('f, 'ty) fun_types" and
tiebreakers :: "('f, 'v) tiebreakers" +
assumes
types_ordLeq_variables: "|UNIV :: 'ty set| ≤o |UNIV :: 'v set|"
begin
interpretation term_order_notation.
inductive eq_resolution :: "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool" where
eq_resolutionI:
"D = add_mset l D' ⟹
l = t !≈ t' ⟹
welltyped_imgu_on (clause.vars D) 𝒱 t t' μ ⟹
select D = {#} ∧ is_maximal (l ⋅l μ) (D ⋅ μ) ∨ is_maximal (l ⋅l μ) (select D ⋅ μ) ⟹
C = D' ⋅ μ ⟹
eq_resolution (D, 𝒱) (C, 𝒱)"
inductive eq_factoring :: "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool" where
eq_factoringI:
"D = add_mset l⇩1 (add_mset l⇩2 D') ⟹
l⇩1 = t⇩1 ≈ t⇩1' ⟹
l⇩2 = t⇩2 ≈ t⇩2' ⟹
select D = {#} ⟹
is_maximal (l⇩1 ⋅l μ) (D ⋅ μ) ⟹
¬ (t⇩1 ⋅t μ ≼⇩t t⇩1' ⋅t μ) ⟹
welltyped_imgu_on (clause.vars D) 𝒱 t⇩1 t⇩2 μ ⟹
C = add_mset (t⇩1 ≈ t⇩2') (add_mset (t⇩1' !≈ t⇩2') D') ⋅ μ ⟹
eq_factoring (D, 𝒱) (C, 𝒱)"
inductive superposition ::
"('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
superpositionI:
"infinite_variables_per_type 𝒱⇩1 ⟹
infinite_variables_per_type 𝒱⇩2 ⟹
term_subst.is_renaming ρ⇩1 ⟹
term_subst.is_renaming ρ⇩2 ⟹
clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
E = add_mset l⇩1 E' ⟹
D = add_mset l⇩2 D' ⟹
𝒫 ∈ {Pos, Neg} ⟹
l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1') ⟹
l⇩2 = t⇩2 ≈ t⇩2' ⟹
¬ is_Var t⇩1 ⟹
welltyped_imgu_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
(⋀τ τ'. typed 𝒱⇩2 t⇩2 τ ⟹ typed 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
(𝒫 = Pos ⟹ select E = {#}) ⟹
(𝒫 = Pos ⟹ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)) ⟹
(𝒫 = Neg ⟹ select E = {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)) ⟹
(𝒫 = Neg ⟹ select E ≠ {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ)) ⟹
select D = {#} ⟹
is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
C = add_mset (𝒫 (Upair (c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ (t⇩1' ⋅t ρ⇩1))) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
abbreviation eq_factoring_inferences where
"eq_factoring_inferences ≡ { Infer [D] C | D C. eq_factoring D C }"
abbreviation eq_resolution_inferences where
"eq_resolution_inferences ≡ { Infer [D] C | D C. eq_resolution D C }"
abbreviation superposition_inferences where
"superposition_inferences ≡ { Infer [D, E] C | D E C. superposition D E C}"
definition inferences :: "('f, 'v, 'ty) typed_clause inference set" where
"inferences ≡ superposition_inferences ∪ eq_resolution_inferences ∪ eq_factoring_inferences"
abbreviation bottom⇩F :: "('f, 'v, 'ty) typed_clause set" ("⊥⇩F") where
"bottom⇩F ≡ {({#}, 𝒱) | 𝒱. infinite_variables_per_type 𝒱 }"
subsubsection ‹Alternative Specification of the Superposition Rule›
inductive superposition' ::
"('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
superposition'I:
"infinite_variables_per_type 𝒱⇩1 ⟹
infinite_variables_per_type 𝒱⇩2 ⟹
term_subst.is_renaming ρ⇩1 ⟹
term_subst.is_renaming ρ⇩2 ⟹
clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
E = add_mset l⇩1 E' ⟹
D = add_mset l⇩2 D' ⟹
𝒫 ∈ {Pos, Neg} ⟹
l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1') ⟹
l⇩2 = t⇩2 ≈ t⇩2' ⟹
¬ is_Var t⇩1 ⟹
welltyped_imgu_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
(⋀τ τ'. typed 𝒱⇩2 t⇩2 τ ⟹ typed 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
(𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
𝒫 = Neg ∧ (select E = {#} ∧ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ))) ⟹
select D = {#} ⟹
is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
C = add_mset (𝒫 (Upair (c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ (t⇩1' ⋅t ρ⇩1))) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
superposition' (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
lemma superposition_eq_superposition': "superposition = superposition'"
proof (intro ext iffI)
fix D E C
assume "superposition D E C"
then show "superposition' D E C"
proof (cases D E C rule: superposition.cases)
case (superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' 𝒫 c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)
show ?thesis
proof (unfold superpositionI(1-3), rule superposition'I[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2]; (rule superpositionI)?)
show "𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
𝒫 = Neg ∧ (select E = {#} ∧ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (select E ⋅ ρ⇩1 ⊙ μ))"
using superpositionI(11,22-25)
by fastforce
qed
qed
next
fix D E C
assume "superposition' D E C"
then show "superposition D E C"
proof (cases D E C rule: superposition'.cases)
case (superposition'I 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' 𝒫 c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)
show ?thesis
proof (unfold superposition'I(1-3), rule superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2]; (rule superposition'I)?)
show
"𝒫 = Pos ⟹ select E = {#}"
"𝒫 = Pos ⟹ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
"𝒫 = Neg ⟹ select E = {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
"𝒫 = Neg ⟹ select E ≠ {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (select E ⋅ ρ⇩1 ⊙ μ)"
using superposition'I(22) is_maximal_not_empty
by auto
qed
qed
qed
inductive pos_superposition ::
"('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
pos_superpositionI:
"infinite_variables_per_type 𝒱⇩1 ⟹
infinite_variables_per_type 𝒱⇩2 ⟹
term_subst.is_renaming ρ⇩1 ⟹
term_subst.is_renaming ρ⇩2 ⟹
clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
E = add_mset l⇩1 E' ⟹
D = add_mset l⇩2 D' ⟹
l⇩1 = c⇩1⟨t⇩1⟩ ≈ t⇩1' ⟹
l⇩2 = t⇩2 ≈ t⇩2' ⟹
¬ is_Var t⇩1 ⟹
welltyped_imgu_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
(⋀τ τ'. typed 𝒱⇩2 t⇩2 τ ⟹ typed 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
select E = {#} ⟹
is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ⟹
select D = {#} ⟹
is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
C = add_mset ((c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ ≈ (t⇩1' ⋅t ρ⇩1)) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
pos_superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
lemma superposition_if_pos_superposition:
assumes "pos_superposition D E C"
shows "superposition D E C"
using assms
proof (cases rule: pos_superposition.cases)
case (pos_superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' μ 𝒱⇩3 C)
then show ?thesis
using superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' Pos c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' μ 𝒱⇩3 C]
by blast
qed
inductive neg_superposition ::
"('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
neg_superpositionI:
"infinite_variables_per_type 𝒱⇩1 ⟹
infinite_variables_per_type 𝒱⇩2 ⟹
term_subst.is_renaming ρ⇩1 ⟹
term_subst.is_renaming ρ⇩2 ⟹
clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
E = add_mset l⇩1 E' ⟹
D = add_mset l⇩2 D' ⟹
l⇩1 = c⇩1⟨t⇩1⟩ !≈ t⇩1' ⟹
l⇩2 = t⇩2 ≈ t⇩2' ⟹
¬ is_Var t⇩1 ⟹
welltyped_imgu_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
(⋀τ τ'. typed 𝒱⇩2 t⇩2 τ ⟹ typed 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
(select E = {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)) ⟹
(select E ≠ {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ)) ⟹
select D = {#} ⟹
is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
C = add_mset ((c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ !≈ (t⇩1' ⋅t ρ⇩1)) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
neg_superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
lemma superposition_if_neg_superposition:
assumes "neg_superposition E D C"
shows "superposition E D C"
using assms
proof (cases E D C rule: neg_superposition.cases)
case (neg_superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' μ 𝒱⇩3 C)
then show ?thesis
using
superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' Neg c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' μ 𝒱⇩3 C]
literals_distinct(2)
by blast
qed
lemma superposition_iff_pos_or_neg:
"superposition D E C ⟷ pos_superposition D E C ∨ neg_superposition D E C"
proof (rule iffI)
assume "superposition D E C"
thus "pos_superposition D E C ∨ neg_superposition D E C"
proof (cases D E C rule: superposition.cases)
case (superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' 𝒫 c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)
show ?thesis
proof(cases "𝒫 = Pos")
case True
then have "pos_superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
using
superpositionI
pos_superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C]
by argo
then show ?thesis
unfolding superpositionI(1-3)
by simp
next
case False
then have "𝒫 = Neg"
using superpositionI(11)
by blast
then have "neg_superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C, 𝒱⇩3)"
using
superpositionI
neg_superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C]
by argo
then show ?thesis
unfolding superpositionI(1-3)
by simp
qed
qed
next
assume "pos_superposition D E C ∨ neg_superposition D E C"
thus "superposition D E C"
using superposition_if_neg_superposition superposition_if_pos_superposition
by metis
qed
end
end