Theory Ground_Superposition_Compatibility
theory Ground_Superposition_Compatibility
imports
Abstract_Substitution.Noop_Substitution
Ground_Superposition
Untyped_Superposition
begin
locale noop_lifting = term_based_lifting where
comp_subst = noop_comp_subst and id_subst = noop_id_subst and term_vars = noop_vars and
term_is_ground = noop_is_ground and subst_update = noop_subst_update and
apply_subst = noop_apply_subst and term_subst = noop_subst and
subst_updates = noop_subst_updates and term_to_ground = id and
term_from_ground = id and to_ground_map = map and from_ground_map = map and
ground_map = map and to_set_ground = to_set
begin
lemma noop_is_ground [simp]: "is_ground expr"
unfolding is_ground_def
using sub.exists_nonground_iff_base_exists_nonground
by auto
lemma noop_vars [simp]: "vars expr = {}"
using no_vars_if_is_ground
by force
end
context nonground_clause
begin
sublocale atom.noop: noop_lifting where
sub_vars = noop_vars and sub_subst = noop_subst and map = map_uprod and
to_set = set_uprod and sub_to_ground = id and sub_from_ground = id and
sub_is_ground = noop_is_ground
using unit.neutral_is_right_invertible
by unfold_locales (auto simp: abstract_substitution_ops.is_ground_subst_def)
sublocale literal.noop: noop_lifting where
sub_vars = atom.noop.vars and sub_subst = atom.noop.subst and map = map_literal and
to_set = set_literal and sub_to_ground = id and sub_from_ground = id and
sub_is_ground = atom.noop.is_ground
by unfold_locales (use atom.exists_nonground_iff_sub_exists_nonground in auto)
sublocale clause.noop: noop_lifting where
sub_vars = literal.noop.vars and sub_subst = literal.noop.subst and map = image_mset and
to_set = set_mset and sub_to_ground = id and sub_from_ground = id and
sub_is_ground = literal.noop.is_ground
by unfold_locales (use literal.exists_nonground_iff_sub_exists_nonground in auto)
end
context nonground_term_with_context
begin
sublocale context.noop: noop_lifting where
sub_vars = noop_vars and sub_subst = noop_subst and map = map_context and
to_set = context_to_set and sub_to_ground = id and sub_from_ground = id and
sub_is_ground = noop_is_ground
using unit.neutral_is_right_invertible
by unfold_locales (auto simp: abstract_substitution_ops.is_ground_subst_def)
end
locale ground_superposition_compatibility = untyped_superposition_calculus where
comp_subst = noop_comp_subst and id_subst = noop_id_subst and term_vars = noop_vars and
subst_update = noop_subst_update and apply_subst = noop_apply_subst and
term_subst = noop_subst and subst_updates = noop_subst_updates and term_to_ground = id and
term_from_ground = id and ground_hole = hole and compose_ground_context = compose_context and
from_ground_context_map = map_context and to_ground_context_map = map_context and
ground_context_map = map_context and ground_context_to_set = context_to_set and
apply_ground_context = apply_context and occurences = "λ_ _. 0" and
term_is_ground = noop_is_ground
begin
interpretation grounded: ground_superposition_calculus where
subterms = ground_subterms and fun_sym = ground_fun_sym and extra = ground_extra and
subterms⇩l = ground_subterms⇩l and subcontext = ground_subcontext and
subterms⇩r = ground_subterms⇩r and Fun = GFun and More = GMore and fun_sym⇩c = ground_fun_sym⇩c and
extra⇩c = ground_extra⇩c and size = ground_size and hole_position = ground_hole_position and
context_at = ground_context_at and size⇩c = ground_size⇩c
proof unfold_locales
show "wfp (≺⇩t)"
using term.order.wfp
by simp
next
show "totalp (≺⇩t)"
using term.order.totalp
by simp
next
fix t c
assume "c ≠ □"
then show "t ≺⇩t c⟨t⟩"
by (metis id_apply term.order.less⇩r_def term.restriction.subterm_property)
qed simp
lemma eq_resolution_compatibility: "eq_resolution D C ⟷ grounded.eq_resolution D C"
proof (rule iffI)
assume "grounded.eq_resolution D C"
then show "eq_resolution D C"
proof(cases rule: grounded.eq_resolution.cases)
case grounded_eq_resolutionI: (eq_resolutionI l D' t)
show ?thesis
proof (intro eq_resolutionI; (rule grounded_eq_resolutionI)?)
show "term.noop.is_imgu noop_id_subst {{t, t}}"
using term.is_imgu_id_subst_empty
by auto
next
show "select D = {#} ⟹ is_maximal (l ⋅l noop_id_subst) (D ⋅ noop_id_subst)"
using grounded_eq_resolutionI(3) is_maximal_not_empty
by auto
next
show "select D ≠ {#} ⟹ is_maximal (l ⋅l noop_id_subst) (select D ⋅ noop_id_subst)"
using grounded_eq_resolutionI(3)
by simp
next
show "C = D' ⋅ noop_id_subst"
using grounded_eq_resolutionI(4)
by simp
qed
qed
next
assume "eq_resolution D C"
then show "grounded.eq_resolution D C"
proof(cases rule: eq_resolution.cases)
case (eq_resolutionI μ t t' l D')
show ?thesis
proof (intro grounded.eq_resolutionI; (rule eq_resolutionI)?)
show "D = add_mset l (D' ⋅ μ)"
by (simp add: eq_resolutionI(4))
next
show "l = t !≈ t"
using eq_resolutionI(1,5)
unfolding term.noop.is_imgu_def
by auto
next
show "select D = {#} ∧ is_maximal l D ∨ is_maximal l (select D)"
using eq_resolutionI(2, 3)
by fastforce
qed
qed
qed
lemma eq_factoring_compatibility: "eq_factoring D C ⟷ grounded.eq_factoring D C"
proof (rule iffI)
assume "grounded.eq_factoring D C"
then show "eq_factoring D C"
proof(cases rule: grounded.eq_factoring.cases)
case grounded_eq_factoringI: (eq_factoringI l⇩1 l⇩2 D' t t' t'')
show ?thesis
proof (intro eq_factoringI[where l⇩1 = l⇩1 and l⇩2 = l⇩2]; (rule grounded_eq_factoringI)?)
show "is_maximal (l⇩1 ⋅l noop_id_subst) (D ⋅ noop_id_subst)"
by (simp add: grounded_eq_factoringI(5))
next
show "¬ noop_subst t noop_id_subst ≼⇩t noop_subst t' noop_id_subst"
using grounded_eq_factoringI(6)
by force
next
show "term.noop.is_imgu noop_id_subst {{t, t}}"
using unit.noop.is_imgu_id_subst_empty
by simp
next
show "C = add_mset (t ≈ t'') (add_mset (t' !≈ t'') D') ⋅ noop_id_subst"
using grounded_eq_factoringI(7)
by simp
qed
qed
next
assume "eq_factoring D C"
then show "grounded.eq_factoring D C"
proof (cases rule: eq_factoring.cases)
case (eq_factoringI l⇩1 μ t⇩1 t⇩1' t⇩2 l⇩2 D' t⇩2')
show ?thesis
proof (intro grounded.eq_factoringI; (rule eq_factoringI(1, 5))?)
show "is_maximal l⇩1 D"
using eq_factoringI(2)
by auto
next
show "t⇩1' ≺⇩t t⇩1"
using eq_factoringI(3)
by auto
next
show "C = add_mset (t⇩1' !≈ t⇩2') (add_mset (t⇩1 ≈ t⇩2') D')"
by (simp add: local.eq_factoringI(8))
next
show "l⇩1 = t⇩1 ≈ t⇩1'"
using eq_factoringI(6) .
next
show "l⇩2 = t⇩1 ≈ t⇩2'"
using eq_factoringI(4,7) term.subst_imgu_eq_subst_imgu
by auto
qed
qed
qed
lemma superposition_compatibility: "superposition D E C ⟷ grounded.superposition D E C"
proof (rule iffI)
assume "grounded.superposition D E C"
then show "superposition D E C"
proof (cases rule: grounded.superposition.cases)
case grounded_superpositionI: (superpositionI l⇩1 E' l⇩2 D' 𝒫 c⇩1 t⇩1 t⇩1' t⇩2')
show ?thesis
proof (intro superpositionI; (rule grounded_superpositionI(4))?)
show "term.is_renaming noop_id_subst" "term.is_renaming noop_id_subst"
using unit.is_right_invertible_def
by simp_all
next
show "term.noop.is_imgu noop_id_subst
{{noop_subst t⇩1 noop_id_subst, noop_subst t⇩1 noop_id_subst}}"
using term.is_imgu_id_subst_empty
by simp
next
show "¬ E ⋅ noop_comp_subst noop_id_subst noop_id_subst ≼⇩c
D ⋅ noop_comp_subst noop_id_subst noop_id_subst"
using grounded_superpositionI(3)
by auto
next
show "¬ noop_subst c⇩1⟨t⇩1⟩ (noop_comp_subst noop_id_subst noop_id_subst) ≼⇩t
noop_subst t⇩1' (noop_comp_subst noop_id_subst noop_id_subst)"
using grounded_superpositionI(7)
by auto
next
show "¬ noop_subst t⇩1 (noop_comp_subst noop_id_subst noop_id_subst) ≼⇩t
noop_subst t⇩2' (noop_comp_subst noop_id_subst noop_id_subst)"
using grounded_superpositionI(8)
by auto
next
show "𝒫 = Pos ⟹ select E = {#}"
using grounded_superpositionI(9)
by auto
next
show "𝒫 = Pos ⟹
is_strictly_maximal
(l⇩1 ⋅l noop_comp_subst noop_id_subst noop_id_subst)
(E ⋅ noop_comp_subst noop_id_subst noop_id_subst)"
using grounded_superpositionI(9)
by auto
next
assume "select E = {#}"
then show "is_maximal
(l⇩1 ⋅l noop_comp_subst noop_id_subst noop_id_subst)
(E ⋅ noop_comp_subst noop_id_subst noop_id_subst)"
using grounded_superpositionI(9) is_maximal_not_empty
by auto
next
assume "select E ≠ {#}"
then show "is_maximal
(l⇩1 ⋅l noop_comp_subst noop_id_subst noop_id_subst)
(select E ⋅ noop_comp_subst noop_id_subst noop_id_subst)"
using grounded_superpositionI(9)
by auto
next
show "select D = {#}"
by (simp add: grounded_superpositionI(10))
next
show "is_strictly_maximal
(l⇩2 ⋅l noop_comp_subst noop_id_subst noop_id_subst)
(D ⋅ noop_comp_subst noop_id_subst noop_id_subst)"
by (simp add: grounded_superpositionI(11))
next
show "E = add_mset l⇩1 E'" "D = add_mset l⇩2 D'" "l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1')" "l⇩2 = t⇩1 ≈ t⇩2'"
using grounded_superpositionI(1, 2, 5, 6) .
next
show "C = add_mset
(𝒫 (Upair (c⇩1 ⋅t⇩c noop_id_subst)⟨noop_subst t⇩2' noop_id_subst⟩
(noop_subst t⇩1' noop_id_subst)))
(E' ⋅ noop_id_subst + D' ⋅ noop_id_subst) ⋅ noop_id_subst"
using grounded_superpositionI(12)
by auto
qed auto
qed
next
assume "superposition D E C"
then show "grounded.superposition D E C"
proof (cases rule: superposition.cases)
case (superpositionI 𝒫 ρ⇩1 ρ⇩2 t⇩1 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 E' D')
have t⇩1_t⇩2: "t⇩1 = t⇩2"
using superpositionI(6) term.subst_imgu_eq_subst_imgu
by simp
show ?thesis
proof (intro grounded.superpositionI)
show "𝒫 ∈ {Pos, Neg}"
using superpositionI(1)
by blast
next
show "E = add_mset l⇩1 E'" "D = add_mset l⇩2 D'" "l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1')"
using superpositionI(16-18) .
next
show "l⇩2 = t⇩1 ≈ t⇩2'"
using superpositionI(19)
unfolding t⇩1_t⇩2 .
next
show "D ≺⇩c E"
using superpositionI(7)
by auto
next
show "t⇩1' ≺⇩t c⇩1⟨t⇩1⟩"
using superpositionI(8)
by auto
next
show "t⇩2' ≺⇩t t⇩1"
using superpositionI(9) t⇩1_t⇩2
by fastforce
next
show "𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal l⇩1 E ∨
𝒫 = Neg ∧ (select E = {#} ∧ is_maximal l⇩1 E ∨ is_maximal l⇩1 (select E))"
using superpositionI(1, 10-13)
by auto
next
show "select D = {#}"
by (simp add: superpositionI(14))
next
show "is_strictly_maximal l⇩2 D"
using superpositionI(15)
by auto
next
show "C = add_mset (𝒫 (Upair c⇩1⟨t⇩2'⟩ t⇩1')) (E' + D')"
by (simp add: superpositionI(20))
qed
qed
qed
end
end