Theory Nonground_Context
theory Nonground_Context
imports
Generic_Context
Nonground_Term
begin
section ‹Nonground Contexts and Substitutions›
locale ground_context = "context" where
hole = ground_hole and apply_context = apply_ground_context and
compose_context = compose_ground_context
for ground_hole apply_ground_context compose_ground_context
begin
notation compose_ground_context (infixl ‹∘⇩c⇩G› 75)
notation ground_hole (‹□⇩G›)
notation apply_ground_context (‹_⟨_⟩⇩G› [1000, 0] 1000)
end
locale nonground_context =
term_based_lifting where
sub_vars = "term_vars :: 't ⇒ 'v set" and sub_subst = "term_subst :: 't ⇒ 'subst ⇒ 't" and
sub_from_ground = term_from_ground and sub_to_ground = "term_to_ground :: 't ⇒ 't⇩G" and
to_ground_map = to_ground_context_map and ground_map = ground_context_map and
from_ground_map = from_ground_context_map and map = map_context and to_set = context_to_set and
to_set_ground = ground_context_to_set +
"context" +
ground_context: ground_context where apply_ground_context = apply_ground_context
for
map_context :: "('t ⇒ 't) ⇒ 'c ⇒ 'c" and
to_ground_context_map :: "('t ⇒ 't⇩G) ⇒ 'c ⇒ 'c⇩G" and
from_ground_context_map :: "('t⇩G ⇒ 't) ⇒ 'c⇩G ⇒ 'c" and
ground_context_map :: "('t⇩G ⇒ 't⇩G) ⇒ 'c⇩G ⇒ 'c⇩G" and
context_to_set ground_context_to_set and
apply_ground_context :: "'c⇩G ⇒ 't⇩G ⇒ 't⇩G" +
assumes
hole_if_context_ident [simp]: "c⟨t⟩ = t ⟹ c = □" and
compose_hole [simp]: "c = c ∘⇩c □" and
term_to_ground_context_to_ground [simp]:
"⋀c t. term.to_ground c⟨t⟩ = (to_ground c)⟨term.to_ground t⟩⇩G" and
term_from_ground_context_from_ground [simp]:
"⋀c⇩G t⇩G. term.from_ground c⇩G⟨t⇩G⟩⇩G = (from_ground c⇩G)⟨term.from_ground t⇩G⟩" and
apply_context_is_ground [simp]: "⋀c t. term.is_ground c⟨t⟩ ⟷ is_ground c ∧ term.is_ground t" and
map_compose [simp]: "⋀f c c'. map_context f (c ∘⇩c c') = map_context f c ∘⇩c map_context f c'" and
from_ground_compose [simp]:
"⋀c c'. from_ground (c ∘⇩c⇩G c') = from_ground c ∘⇩c from_ground c'" and
apply_context_vars [simp]: "⋀c t. term.vars c⟨t⟩ = vars c ∪ term.vars t" and
apply_context_subst [simp]: "⋀c t σ. c⟨t⟩ ⋅t σ = (subst c σ)⟨t ⋅t σ⟩" and
context_Var: "⋀x t. x ∈ term.vars t ⟷ (∃c. t = c⟨term.Var x⟩)" and
subst_to_context: "t ⋅t γ = c⇩G⟨t⇩G⟩ ⟹ term.is_ground (t ⋅t γ) ⟹
(∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ subst c γ = c⇩G) ∨
(∃c c⇩G' x. t = c⟨term.Var x⟩ ∧ c⇩G = (subst c γ) ∘⇩c c⇩G')"
begin
notation subst (infixl "⋅t⇩c" 67)
lemma term_from_ground_context_to_ground:
assumes "is_ground c"
shows "term.from_ground (to_ground c)⟨t⇩G⟩⇩G = c⟨term.from_ground t⇩G⟩"
unfolding to_ground_def
by (metis assms term_from_ground_context_from_ground to_ground_def to_ground_inverse)
lemmas safe_unfolds =
term_to_ground_context_to_ground
term_from_ground_context_from_ground
lemma composed_context_is_ground [simp]: "is_ground (c ∘⇩c c') ⟷ is_ground c ∧ is_ground c'"
by (metis term.ground_exists apply_context_is_ground compose_context_iff)
lemma ground_context_ident_iff_hole [simp]: "c⟨t⟩⇩G = t ⟷ c = □⇩G"
by (metis hole_if_context_ident from_ground_eq ground_context.apply_hole
term_from_ground_context_from_ground)
lemma from_ground_hole [simp]: "from_ground c⇩G = □ ⟷ c⇩G = □⇩G"
by (metis apply_hole apply_context_is_ground from_ground_inverse ground_context_ident_iff_hole
term.ground_exists term_to_ground_context_to_ground to_ground_inverse)
lemma hole_simps [simp]: "from_ground □⇩G = □" "to_ground □ = □⇩G"
using from_ground_inverse from_ground_hole
by metis+
lemma to_ground_compose [simp]: "to_ground (c ∘⇩c c') = to_ground c ∘⇩c⇩G to_ground c'"
using from_ground_compose
unfolding to_ground_def
by (metis conversion_map_comp from_ground_def from_ground_inverse map_compose)
lemma hole_subst [simp]: "□ ⋅t⇩c σ = □"
by (metis all_subst_ident_if_ground apply_hole apply_context_is_ground term.ground_exists)
lemma subst_into_Var:
assumes
t_γ: "t ⋅t γ = c⇩G⟨t⇩G⟩" and
t_grounding: "term.is_ground (t ⋅t γ)" and
not_subst_into_Fun: "∄c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G ∧ ¬ term.is_Var t'"
shows "∃c t' c⇩G'. t = c⟨t'⟩ ∧ term.is_Var t' ∧ c⇩G = (c ⋅t⇩c γ) ∘⇩c c⇩G'"
proof (cases "∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G")
case True
then obtain c t' where t: "t = c⟨t'⟩" and "t' ⋅t γ = t⇩G" "c ⋅t⇩c γ = c⇩G"
by metis
have "is_ground c⇩G"
using t_γ t_grounding
by auto
obtain x where t': "t' = term.Var x"
using ‹c ⋅t⇩c γ = c⇩G› ‹t' ⋅t γ = t⇩G› not_subst_into_Fun t
by blast
show ?thesis
proof (intro exI conjI)
show "t = c⟨t'⟩"
using t .
next
show "t' = term.Var x"
using t' .
next
show "c⇩G = (c ⋅t⇩c γ) ∘⇩c □"
by (simp add: ‹c ⋅t⇩c γ = c⇩G›)
qed
next
case False
then show ?thesis
using subst_to_context[OF t_γ t_grounding]
by metis
qed
end
locale occurences =
nonground_context where map_context = map_context and term_vars = term_vars
for
map_context :: "('t ⇒ 't) ⇒ 'c ⇒ 'c" and term_vars :: "'t ⇒ 'v set" +
fixes occurences :: "'t ⇒ 'v ⇒ nat"
assumes
occurences:
"⋀t⇩G c x. term.is_ground t⇩G ⟹ occurences (c⟨term.Var x⟩) x = Suc (occurences (c⟨t⇩G⟩) x)" and
vars_occurences: "⋀x t. x ∈ term.vars t ⟷ 0 < occurences t x"
begin
lemma is_ground_no_occurences: "term.is_ground t ⟹ occurences t x = 0"
using vars_occurences
by auto
lemma occurences_obtain_context:
assumes update: "term.is_ground t⇩G" and occurences_in_t: "occurences t x = Suc n"
obtains c where
"t = c⟨term.Var x⟩"
"occurences c⟨t⇩G⟩ x = n"
proof -
obtain c where t: "t = c⟨term.Var x⟩"
using occurences_in_t context_Var vars_occurences zero_less_Suc
by presburger
moreover have "occurences c⟨t⇩G⟩ x = n"
using assms
unfolding t occurences[OF update]
by linarith
ultimately show ?thesis
using that
by metis
qed
lemma one_occurence_obtain_context:
assumes "occurences t x = 1"
obtains c where
"t = c⟨term.Var x⟩"
"x ∉ vars c"
using term.ground_exists occurences_obtain_context[OF _ assms[unfolded One_nat_def]]
by (metis Un_iff apply_context_vars order_less_irrefl vars_occurences)
end
locale nonground_term_with_context =
"term": nonground_term +
"context": nonground_context +
occurences
begin
notation context.subst (infixl "⋅t⇩c" 67)
end
end