Theory Superposition_Soundness
theory Superposition_Soundness
imports
First_Order_Clause.Nonground_Entailment
Grounded_Superposition
Superposition_Welltypedness_Preservation
begin
subsection ‹Soundness›
context grounded_superposition_calculus
begin
notation lifting.entails_𝒢 (infix "⊫⇩F" 50)
lemma eq_resolution_sound:
assumes eq_resolution: "eq_resolution D C"
shows "{D} ⊫⇩F {C}"
using eq_resolution
proof (cases D C rule: eq_resolution.cases)
case (eq_resolutionI D l D' t t' 𝒱 μ C)
{
fix I :: "'f ground_term rel" and γ :: "('f, 'v) subst"
let ?I = "upair ` I"
assume
refl_I: "refl I" and
entails_groundings: "∀D⇩G ∈ clause_groundings (D, 𝒱). ?I ⊫ D⇩G" and
C_is_ground: "clause.is_ground (C ⋅ γ)" and
C_is_welltyped: "clause.is_welltyped 𝒱 C" and
γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱 γ" and
𝒱: "infinite_variables_per_type 𝒱"
obtain γ' where
γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
γ'_is_welltyped: "term.subst.is_welltyped 𝒱 γ'" and
γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].
let ?D⇩G = "clause.to_ground (D ⋅ μ ⋅ γ')"
let ?l⇩G = "literal.to_ground (l ⋅l μ ⋅l γ')"
let ?D⇩G' = "clause.to_ground (D' ⋅ μ ⋅ γ')"
let ?t⇩G = "term.to_ground (t ⋅t μ ⋅t γ')"
let ?t⇩G' = "term.to_ground (t' ⋅t μ ⋅t γ')"
have μ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 μ"
using eq_resolutionI
by meson
have "?D⇩G ∈ clause_groundings (D, 𝒱)"
proof(unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, intro exI conjI 𝒱)
show "clause.to_ground (D ⋅ μ ⋅ γ') = clause.to_ground (D ⋅ μ ⊙ γ')"
by simp
next
show "clause.is_ground (D ⋅ μ ⊙ γ')"
using γ'_is_ground_subst clause.is_ground_subst_is_ground
by auto
next
show "clause.is_welltyped 𝒱 D"
using C_is_welltyped
unfolding
eq_resolution_preserves_typing[OF eq_resolution[unfolded eq_resolutionI(1, 2)]].
next
show "term.subst.is_welltyped_on (clause.vars D) 𝒱 (μ ⊙ γ')"
using γ'_is_welltyped μ_is_welltyped
by (simp add: subst_compose_def)
qed
then have "?I ⊫ ?D⇩G"
using entails_groundings
by auto
then obtain l⇩G where l⇩G_in_D: "l⇩G ∈# ?D⇩G" and I_models_l⇩G: "?I ⊫l l⇩G"
by (auto simp: true_cls_def)
have "l⇩G ≠ ?l⇩G"
proof(rule notI)
assume "l⇩G = ?l⇩G"
then have [simp]: "l⇩G = ?t⇩G !≈ ?t⇩G'"
unfolding eq_resolutionI
by simp
moreover have "atm_of l⇩G ∈ ?I"
proof-
have "?t⇩G = ?t⇩G'"
using eq_resolutionI(5) term_subst.is_imgu_unifies_pair
by metis
then show ?thesis
using reflD[OF refl_I, of ?t⇩G]
by auto
qed
ultimately show False
using I_models_l⇩G
by auto
qed
then have "l⇩G ∈# clause.to_ground (C ⋅ γ')"
using l⇩G_in_D
unfolding eq_resolutionI
by simp
then have "?I ⊫ clause.to_ground (C ⋅ γ)"
using clause.subst_eq[OF γ'_γ[rule_format]] I_models_l⇩G
by auto
}
then show ?thesis
unfolding
true_clss_def
eq_resolutionI(1,2)
clause_groundings_def
ground.G_entails_def
by auto
qed
lemma eq_factoring_sound:
assumes eq_factoring: "eq_factoring D C"
shows "{D} ⊫⇩F {C}"
using eq_factoring
proof (cases D C rule: eq_factoring.cases)
case (eq_factoringI D l⇩1 l⇩2 D' t⇩1 t⇩1' t⇩2 t⇩2' μ 𝒱 C)
{
fix I :: "'f ground_term rel" and γ :: "('f, 'v) subst"
let ?I = "upair ` I"
assume
trans_I: "trans I" and
sym_I: "sym I" and
entails_groundings: "∀D⇩G ∈ clause_groundings (D, 𝒱). ?I ⊫ D⇩G" and
C_is_ground: "clause.is_ground (C ⋅ γ)" and
C_is_welltyped: "clause.is_welltyped 𝒱 C" and
γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱 γ" and
𝒱: "infinite_variables_per_type 𝒱"
obtain γ' where
γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
γ'_is_welltyped: "term.subst.is_welltyped 𝒱 γ'" and
γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].
let ?D⇩G = "clause.to_ground (D ⋅ μ ⋅ γ')"
let ?D⇩G' = "clause.to_ground (D' ⋅ μ ⋅ γ')"
let ?l⇩G⇩1 = "literal.to_ground (l⇩1 ⋅l μ ⋅l γ')"
let ?l⇩G⇩2 = "literal.to_ground (l⇩2 ⋅l μ ⋅l γ')"
let ?t⇩G⇩1 = "term.to_ground (t⇩1 ⋅t μ ⋅t γ')"
let ?t⇩G⇩1' = "term.to_ground (t⇩1' ⋅t μ ⋅t γ')"
let ?t⇩G⇩2 = "term.to_ground (t⇩2 ⋅t μ ⋅t γ')"
let ?t⇩G⇩2' = "term.to_ground (t⇩2' ⋅t μ ⋅t γ')"
let ?C⇩G = "clause.to_ground (C ⋅ γ')"
have μ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 μ"
using eq_factoringI(9)
by blast
have "?D⇩G ∈ clause_groundings (D, 𝒱)"
proof(unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv, intro exI conjI 𝒱)
show "clause.to_ground (D ⋅ μ ⋅ γ') = clause.to_ground (D ⋅ μ ⊙ γ')"
by simp
next
show "clause.is_ground (D ⋅ μ ⊙ γ')"
using γ'_is_ground_subst clause.is_ground_subst_is_ground
by auto
next
show "clause.is_welltyped 𝒱 D"
using C_is_welltyped
unfolding eq_factoring_preserves_typing[OF eq_factoring[unfolded eq_factoringI(1, 2)]].
next
show "term.subst.is_welltyped_on (clause.vars D) 𝒱 (μ ⊙ γ')"
using μ_is_welltyped γ'_is_welltyped
by (simp add: subst_compose_def)
qed
then have "?I ⊫ ?D⇩G"
using entails_groundings
by blast
then obtain l⇩G where l⇩G_in_D⇩G: "l⇩G ∈# ?D⇩G" and I_models_l⇩G: "?I ⊫l l⇩G"
by (auto simp: true_cls_def)
have [simp]: "?t⇩G⇩2 = ?t⇩G⇩1"
using eq_factoringI(9) term_subst.is_imgu_unifies_pair
by metis
have [simp]: "?l⇩G⇩1 = ?t⇩G⇩1 ≈ ?t⇩G⇩1'"
unfolding eq_factoringI
by simp
have [simp]: "?l⇩G⇩2 = ?t⇩G⇩2 ≈ ?t⇩G⇩2'"
unfolding eq_factoringI
by simp
have [simp]: "?C⇩G = add_mset (?t⇩G⇩1 ≈ ?t⇩G⇩2') (add_mset (?t⇩G⇩1' !≈ ?t⇩G⇩2') ?D⇩G')"
unfolding eq_factoringI
by simp
have "?I ⊫ clause.to_ground (C ⋅ γ)"
proof(cases "l⇩G = ?l⇩G⇩1 ∨ l⇩G = ?l⇩G⇩2")
case True
then have "?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩1' ∨ ?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩2'"
using I_models_l⇩G sym_I
by(auto elim: symE)
then have "?I ⊫l ?t⇩G⇩1 ≈ ?t⇩G⇩2' ∨ ?I ⊫l ?t⇩G⇩1' !≈ ?t⇩G⇩2'"
using sym_I trans_I
by(auto dest: transD)
then show ?thesis
using clause.subst_eq[OF γ'_γ[rule_format]] sym_I
by auto
next
case False
then have "l⇩G ∈# ?D⇩G'"
using l⇩G_in_D⇩G
unfolding eq_factoringI
by simp
then have "l⇩G ∈# clause.to_ground (C ⋅ γ)"
using clause.subst_eq[OF γ'_γ[rule_format]]
by simp
then show ?thesis
using I_models_l⇩G
by blast
qed
}
then show ?thesis
unfolding
eq_factoringI(1, 2)
ground.G_entails_def
true_clss_def
clause_groundings_def
by auto
qed
lemma superposition_sound:
assumes superposition: "superposition D E C"
shows "{E, D} ⊫⇩F {C}"
using superposition
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)
{
fix I :: "'f gterm rel" and γ :: "'v ⇒ ('f, 'v) Term.term"
let ?I = "(λ(x, y). Upair x y) ` I"
assume
refl_I: "refl I" and
trans_I: "trans I" and
sym_I: "sym I" and
compatible_with_ground_context_I: "compatible_with_gctxt I" and
E_entails_groundings: "∀E⇩G ∈ clause_groundings (E, 𝒱⇩1). ?I ⊫ E⇩G" and
D_entails_groundings: "∀D⇩G ∈ clause_groundings (D, 𝒱⇩2). ?I ⊫ D⇩G" and
C_is_ground: "clause.is_ground (C ⋅ γ)" and
C_is_welltyped: "clause.is_welltyped 𝒱⇩3 C" and
γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars C) 𝒱⇩3 γ"
obtain γ' where
γ'_is_ground_subst: "term_subst.is_ground_subst γ'" and
γ'_is_welltyped: "term.subst.is_welltyped 𝒱⇩3 γ'" and
γ'_γ: "∀x ∈ clause.vars C. γ x = γ' x"
using clause.is_welltyped.ground_subst_extension[OF C_is_ground γ_is_welltyped].
let ?E⇩G = "clause.to_ground (E ⋅ ρ⇩1 ⋅ μ ⋅ γ')"
let ?D⇩G = "clause.to_ground (D ⋅ ρ⇩2 ⋅ μ ⋅ γ')"
let ?l⇩G⇩1 = "literal.to_ground (l⇩1 ⋅l ρ⇩1 ⋅l μ ⋅l γ')"
let ?l⇩G⇩2 = "literal.to_ground (l⇩2 ⋅l ρ⇩2 ⋅l μ ⋅l γ')"
let ?E⇩G' = "clause.to_ground (E' ⋅ ρ⇩1 ⋅ μ ⋅ γ')"
let ?D⇩G' = "clause.to_ground (D' ⋅ ρ⇩2 ⋅ μ ⋅ γ')"
let ?c⇩G⇩1 = "context.to_ground (c⇩1 ⋅t⇩c ρ⇩1 ⋅t⇩c μ ⋅t⇩c γ')"
let ?t⇩G⇩1 = "term.to_ground (t⇩1 ⋅t ρ⇩1 ⋅t μ ⋅t γ')"
let ?t⇩G⇩1' = "term.to_ground (t⇩1' ⋅t ρ⇩1 ⋅t μ ⋅t γ')"
let ?t⇩G⇩2 = "term.to_ground (t⇩2 ⋅t ρ⇩2 ⋅t μ ⋅t γ')"
let ?t⇩G⇩2' = "term.to_ground (t⇩2' ⋅t ρ⇩2 ⋅t μ ⋅t γ')"
let ?𝒫⇩G = "if 𝒫 = Pos then Pos else Neg"
let ?C⇩G = "clause.to_ground (C ⋅ γ')"
have 𝒫_subst [simp]: "⋀a σ. 𝒫 a ⋅l σ = 𝒫 (a ⋅a σ)"
using superpositionI(11)
by auto
have [simp]: "⋀𝒱 a. literal.is_welltyped 𝒱 (𝒫 a) ⟷ atom.is_welltyped 𝒱 a"
using superpositionI(11)
by (auto simp: literal_is_welltyped_iff_atm_of)
have [simp]: "⋀a. literal.vars (𝒫 a) = atom.vars a"
using superpositionI(11)
by auto
have μ_γ'_is_ground_subst:
"term_subst.is_ground_subst (μ ⊙ γ')"
using term.is_ground_subst_comp_right[OF γ'_is_ground_subst].
have μ_is_welltyped:
"term.subst.is_welltyped_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ"
using superpositionI(15)
by blast
have D_is_welltyped: "clause.is_welltyped 𝒱⇩2 D"
using superposition_preserves_typing_D[OF
superposition[unfolded superpositionI(1-3)]
C_is_welltyped].
have E_is_welltyped: "clause.is_welltyped 𝒱⇩1 E"
using superposition_preserves_typing_E[OF
superposition[unfolded superpositionI(1-3)]
C_is_welltyped].
have is_welltyped_μ_γ:
"term.subst.is_welltyped_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (μ ⊙ γ')"
using γ'_is_welltyped μ_is_welltyped
by (simp add: term.welltyped.typed_subst_compose)
note is_welltyped_ρ_μ_γ = term.welltyped.renaming_ground_subst[OF _ _ _ μ_γ'_is_ground_subst]
have "?E⇩G ∈ clause_groundings (E, 𝒱⇩1)"
proof(
unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv,
intro exI conjI E_is_welltyped superpositionI)
show "clause.to_ground (E ⋅ ρ⇩1 ⋅ μ ⋅ γ') = clause.to_ground (E ⋅ ρ⇩1 ⊙ μ ⊙ γ')"
by simp
next
show "clause.is_ground (E ⋅ ρ⇩1 ⊙ μ ⊙ γ')"
using γ'_is_ground_subst clause.is_ground_subst_is_ground
by auto
next
show "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ μ ⊙ γ')"
using
is_welltyped_μ_γ
is_welltyped_ρ_μ_γ[OF
superpositionI(6) _ superpositionI(18, 16)[unfolded clause.vars_subst]]
by (simp add: subst_compose_assoc clause.vars_subst)
qed
then have entails_E⇩G: "?I ⊫ ?E⇩G"
using E_entails_groundings
by blast
have "?D⇩G ∈ clause_groundings (D, 𝒱⇩2)"
proof(
unfold clause_groundings_def mem_Collect_eq fst_conv snd_conv,
intro exI conjI D_is_welltyped superpositionI)
show "clause.to_ground (D ⋅ ρ⇩2 ⋅ μ ⋅ γ') = clause.to_ground (D ⋅ ρ⇩2 ⊙ μ ⊙ γ')"
by simp
next
show "clause.is_ground (D ⋅ ρ⇩2 ⊙ μ ⊙ γ')"
using γ'_is_ground_subst clause.is_ground_subst_is_ground
by auto
next
show "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ μ ⊙ γ')"
using
is_welltyped_μ_γ
is_welltyped_ρ_μ_γ[OF
superpositionI(7) _ superpositionI(19, 17)[unfolded clause.vars_subst]]
by (simp add: subst_compose_assoc clause.vars_subst)
qed
then have entails_D⇩G: "?I ⊫ ?D⇩G"
using D_entails_groundings
by blast
have "?I ⊫ clause.to_ground (C ⋅ γ')"
proof(cases "?I ⊫l literal.to_ground (𝒫 (Upair (c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ (t⇩1' ⋅t ρ⇩1)) ⋅l μ ⋅l γ')")
case True
then show ?thesis
unfolding superpositionI
by simp
next
case False
have imgu: "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}}"
using superpositionI(15)
by blast
interpret clause_entailment I
by unfold_locales (rule trans_I sym_I compatible_with_ground_context_I)+
note unfolds =
superpositionI
context.safe_unfolds
clause_safe_unfolds
literal_entails_unfolds
term.is_imgu_unifies_pair[OF imgu]
from literal_cases[OF superpositionI(11)]
have "¬ ?I ⊫l ?l⇩G⇩1 ∨ ¬ ?I ⊫l ?l⇩G⇩2"
proof cases
case Pos: 1
show ?thesis
using False symmetric_upair_context_congruence
unfolding Pos unfolds
by blast
next
case Neg: 2
show ?thesis
using False symmetric_upair_context_congruence
unfolding Neg unfolds
by blast
qed
then have "?I ⊫ ?E⇩G' ∨ ?I ⊫ ?D⇩G'"
using entails_D⇩G entails_E⇩G
unfolding superpositionI
by auto
then show ?thesis
unfolding superpositionI
by simp
qed
then have "?I ⊫ clause.to_ground (C ⋅ γ)"
by (metis γ'_γ clause.subst_eq)
}
then show ?thesis
unfolding ground.G_entails_def clause_groundings_def true_clss_def superpositionI(1-3)
by auto
qed
end
sublocale grounded_superposition_calculus ⊆ sound_inference_system inferences "⊥⇩F" "(⊫⇩F)"
proof unfold_locales
fix ι
assume "ι ∈ inferences"
then show "set (prems_of ι) ⊫⇩F {concl_of ι}"
using
eq_factoring_sound
eq_resolution_sound
superposition_sound
unfolding inferences_def ground.G_entails_def
by auto
qed
sublocale superposition_calculus ⊆ sound_inference_system inferences "⊥⇩F" entails_𝒢
proof unfold_locales
obtain select⇩G where select⇩G: "select⇩G ∈ select⇩G⇩s"
using Q_nonempty by blast
then interpret grounded_superposition_calculus
where select⇩G = select⇩G
by unfold_locales (simp add: select⇩G⇩s_def)
fix ι
assume "ι ∈ inferences"
then show "entails_𝒢 (set (prems_of ι)) {concl_of ι}"
unfolding entails_def
using sound
by blast
qed
end