section ‹First-Order Terms›
theory Term
imports Main
begin
datatype (funs_term : 'f, vars_term : 'v) "term" =
is_Var: Var (the_Var: 'v) |
Fun 'f (args : "('f, 'v) term list")
where
"args (Var _) = []"
abbreviation "is_Fun t ≡ ¬ is_Var t"
lemma is_VarE [elim]:
"is_Var t ⟹ (⋀x. t = Var x ⟹ P) ⟹ P"
by (cases t) auto
lemma is_FunE [elim]:
"is_Fun t ⟹ (⋀f ts. t = Fun f ts ⟹ P) ⟹ P"
by (cases t) auto
text ‹Reorient equations of the form @{term "Var x = t"} and @{term "Fun f ss = t"} to facilitate
simplification.›
setup ‹
Reorient_Proc.add
(fn Const (@{const_name Var}, _) $ _ => true | _ => false)
#> Reorient_Proc.add
(fn Const (@{const_name Fun}, _) $ _ $ _ => true | _ => false)
›
simproc_setup reorient_Var ("Var x = t") = Reorient_Proc.proc
simproc_setup reorient_Fun ("Fun f ss = t") = Reorient_Proc.proc
text ‹The \emph{root symbol} of a term is defined by:›
fun root :: "('f, 'v) term ⇒ ('f × nat) option"
where
"root (Var x) = None" |
"root (Fun f ts) = Some (f, length ts)"
lemma finite_vars_term [simp]:
"finite (vars_term t)"
by (induct t) simp_all
lemma finite_Union_vars_term:
"finite (⋃t ∈ set ts. vars_term t)"
by auto
text ‹A substitution is a mapping ‹σ› from variables to terms. We call a substitution that
alters the type of variables a generalized substitution, since it does not have all properties
that are expected of (standard) substitutions (e.g., there is no empty substitution).›
type_synonym ('f, 'v, 'w) gsubst = "'v ⇒ ('f, 'w) term"
type_synonym ('f, 'v) subst = "('f, 'v, 'v) gsubst"
fun subst_apply_term :: "('f, 'v) term ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term" (infixl "⋅" 67)
where
"Var x ⋅ σ = σ x"
| "Fun f ss ⋅ σ = Fun f (map (λt. t ⋅ σ) ss)"
definition
subst_compose :: "('f, 'u, 'v) gsubst ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'u, 'w) gsubst"
(infixl "∘⇩s" 75)
where
"σ ∘⇩s τ = (λx. (σ x) ⋅ τ)"
lemma subst_subst_compose [simp]:
"t ⋅ (σ ∘⇩s τ) = t ⋅ σ ⋅ τ"
by (induct t σ rule: subst_apply_term.induct) (simp_all add: subst_compose_def)
lemma subst_compose_assoc:
"σ ∘⇩s τ ∘⇩s μ = σ ∘⇩s (τ ∘⇩s μ)"
proof (rule ext)
fix x show "(σ ∘⇩s τ ∘⇩s μ) x = (σ ∘⇩s (τ ∘⇩s μ)) x"
proof -
have "(σ ∘⇩s τ ∘⇩s μ) x = σ(x) ⋅ τ ⋅ μ" by (simp add: subst_compose_def)
also have "… = σ(x) ⋅ (τ ∘⇩s μ)" by simp
finally show ?thesis by (simp add: subst_compose_def)
qed
qed
lemma subst_apply_term_empty [simp]:
"t ⋅ Var = t"
proof (induct t)
case (Fun f ts)
from map_ext [rule_format, of ts _ id, OF Fun] show ?case by simp
qed simp
interpretation subst_monoid_mult: monoid_mult "Var" "(∘⇩s)"
by (unfold_locales) (simp add: subst_compose_assoc, simp_all add: subst_compose_def)
lemma term_subst_eq:
assumes "⋀x. x ∈ vars_term t ⟹ σ x = τ x"
shows "t ⋅ σ = t ⋅ τ"
using assms by (induct t) (auto)
lemma term_subst_eq_rev:
"t ⋅ σ = t ⋅ τ ⟹ ∀x ∈ vars_term t. σ x = τ x"
by (induct t) simp_all
lemma term_subst_eq_conv:
"t ⋅ σ = t ⋅ τ ⟷ (∀x ∈ vars_term t. σ x = τ x)"
using term_subst_eq [of t σ τ] and term_subst_eq_rev [of t σ τ] by auto
lemma subst_term_eqI:
assumes "(⋀t. t ⋅ σ = t ⋅ τ)"
shows "σ = τ"
using assms [of "Var x" for x] by (intro ext) simp
definition subst_domain :: "('f, 'v) subst ⇒ 'v set"
where
"subst_domain σ = {x. σ x ≠ Var x}"
fun subst_range :: "('f, 'v) subst ⇒ ('f, 'v) term set"
where
"subst_range σ = σ ` subst_domain σ"
text ‹The variables introduced by a substitution.›
definition range_vars :: "('f, 'v) subst ⇒ 'v set"
where
"range_vars σ = ⋃(vars_term ` subst_range σ)"
definition is_renaming :: "('f, 'v) subst ⇒ bool"
where
"is_renaming σ ⟷ (∀x. is_Var (σ x)) ∧ inj_on σ (subst_domain σ)"
lemma vars_term_subst:
"vars_term (t ⋅ σ) = ⋃(vars_term ` σ ` vars_term t)"
by (induct t) simp_all
lemma range_varsE [elim]:
assumes "x ∈ range_vars σ"
and "⋀t. x ∈ vars_term t ⟹ t ∈ subst_range σ ⟹ P"
shows "P"
using assms by (auto simp: range_vars_def)
lemma range_vars_subst_compose_subset:
"range_vars (σ ∘⇩s τ) ⊆ (range_vars σ - subst_domain τ) ∪ range_vars τ" (is "?L ⊆ ?R")
proof
fix x
assume "x ∈ ?L"
then obtain y where "y ∈ subst_domain (σ ∘⇩s τ)"
and "x ∈ vars_term ((σ ∘⇩s τ) y)" by (auto simp: range_vars_def)
then show "x ∈ ?R"
proof (cases)
assume "y ∈ subst_domain σ" and "x ∈ vars_term ((σ ∘⇩s τ) y)"
moreover then obtain v where "v ∈ vars_term (σ y)"
and "x ∈ vars_term (τ v)" by (auto simp: subst_compose_def vars_term_subst)
ultimately show ?thesis
by (cases "v ∈ subst_domain τ") (auto simp: range_vars_def subst_domain_def)
qed (auto simp: range_vars_def subst_compose_def subst_domain_def)
qed
definition "subst x t = Var (x := t)"
lemma subst_simps [simp]:
"subst x t x = t"
"subst x (Var x) = Var"
by (auto simp: subst_def)
lemma subst_subst_domain [simp]:
"subst_domain (subst x t) = (if t = Var x then {} else {x})"
proof -
{ fix y
have "y ∈ {y. subst x t y ≠ Var y} ⟷ y ∈ (if t = Var x then {} else {x})"
by (cases "x = y", auto simp: subst_def) }
then show ?thesis by (simp add: subst_domain_def)
qed
lemma subst_subst_range [simp]:
"subst_range (subst x t) = (if t = Var x then {} else {t})"
by (cases "t = Var x") (auto simp: subst_domain_def subst_def)
lemma subst_apply_left_idemp [simp]:
assumes "σ x = t ⋅ σ"
shows "s ⋅ subst x t ⋅ σ = s ⋅ σ"
using assms by (induct s) (auto simp: subst_def)
lemma subst_compose_left_idemp [simp]:
assumes "σ x = t ⋅ σ"
shows "subst x t ∘⇩s σ = σ"
by (rule subst_term_eqI) (simp add: assms)
lemma subst_ident [simp]:
assumes "x ∉ vars_term t"
shows "t ⋅ subst x u = t"
proof -
have "t ⋅ subst x u = t ⋅ Var"
by (rule term_subst_eq) (auto simp: assms subst_def)
then show ?thesis by simp
qed
lemma subst_self_idemp [simp]:
"x ∉ vars_term t ⟹ subst x t ∘⇩s subst x t = subst x t"
by (metis subst_simps(1) subst_compose_left_idemp subst_ident)
type_synonym ('f, 'v) terms = "('f, 'v) term set"
text ‹Applying a substitution to every term of a given set.›
abbreviation
subst_apply_set :: "('f, 'v) terms ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) terms" (infixl "⋅⇩s⇩e⇩t" 60)
where
"T ⋅⇩s⇩e⇩t σ ≡ (λt. t ⋅ σ) ` T"
text ‹Composition of substitutions›
lemma subst_compose: "(σ ∘⇩s τ) x = σ x ⋅ τ" by (auto simp: subst_compose_def)
lemmas subst_subst = subst_subst_compose [symmetric]
lemma subst_domain_Var [simp]:
"subst_domain Var = {}"
by (simp add: subst_domain_def)
lemma subst_apply_eq_Var:
assumes "s ⋅ σ = Var x"
obtains y where "s = Var y" and "σ y = Var x"
using assms by (induct s) auto
lemma subst_domain_subst_compose:
"subst_domain (σ ∘⇩s τ) =
(subst_domain σ - {x. ∃y. σ x = Var y ∧ τ y = Var x}) ∪
(subst_domain τ - subst_domain σ)"
by (auto simp: subst_domain_def subst_compose_def elim: subst_apply_eq_Var)
text ‹A substitution is idempotent iff the variables in its range are disjoint from its domain.
(See also "Term Rewriting and All That" \cite[Lemma 4.5.7]{AllThat}.)›
lemma subst_idemp_iff:
"σ ∘⇩s σ = σ ⟷ subst_domain σ ∩ range_vars σ = {}"
proof
assume "σ ∘⇩s σ = σ"
then have "⋀x. σ x ⋅ σ = σ x ⋅ Var" by simp (metis subst_compose_def)
then have *: "⋀x. ∀y∈vars_term (σ x). σ y = Var y"
unfolding term_subst_eq_conv by simp
{ fix x y
assume "σ x ≠ Var x" and "x ∈ vars_term (σ y)"
with * [of y] have False by simp }
then show "subst_domain σ ∩ range_vars σ = {}"
by (auto simp: subst_domain_def range_vars_def)
next
assume "subst_domain σ ∩ range_vars σ = {}"
then have *: "⋀x y. σ x = Var x ∨ σ y = Var y ∨ x ∉ vars_term (σ y)"
by (auto simp: subst_domain_def range_vars_def)
have "⋀x. ∀y∈vars_term (σ x). σ y = Var y"
proof
fix x y
assume "y ∈ vars_term (σ x)"
with * [of y x] show "σ y = Var y" by auto
qed
then show "σ ∘⇩s σ = σ"
by (simp add: subst_compose_def term_subst_eq_conv [symmetric])
qed
fun num_funs :: "('f, 'v) term ⇒ nat"
where
"num_funs (Var x) = 0" |
"num_funs (Fun f ts) = Suc (sum_list (map num_funs ts))"
lemma num_funs_0:
assumes "num_funs t = 0"
obtains x where "t = Var x"
using assms by (induct t) auto
lemma num_funs_subst:
"num_funs (t ⋅ σ) ≥ num_funs t"
by (induct t) (simp_all, metis comp_apply sum_list_mono)
lemma sum_list_map_num_funs_subst:
assumes "sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts) = sum_list (map num_funs ts)"
shows "∀i < length ts. num_funs (ts ! i ⋅ σ) = num_funs (ts ! i)"
using assms
proof (induct ts)
case (Cons t ts)
then have "num_funs (t ⋅ σ) + sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts)
= num_funs t + sum_list (map num_funs ts)" by (simp add: o_def)
moreover have "num_funs (t ⋅ σ) ≥ num_funs t" by (metis num_funs_subst)
moreover have "sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts) ≥ sum_list (map num_funs ts)"
using num_funs_subst [of _ σ] by (induct ts) (auto intro: add_mono)
ultimately show ?case using Cons by (auto) (case_tac i, auto)
qed simp
lemma is_Fun_num_funs_less:
assumes "x ∈ vars_term t" and "is_Fun t"
shows "num_funs (σ x) < num_funs (t ⋅ σ)"
using assms
proof (induct t)
case (Fun f ts)
then obtain u where u: "u ∈ set ts" "x ∈ vars_term u" by auto
then have "num_funs (u ⋅ σ) ≤ sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts)"
by (intro member_le_sum_list) simp
moreover have "num_funs (σ x) ≤ num_funs (u ⋅ σ)"
using Fun.hyps [OF u] and u by (cases u; simp)
ultimately show ?case by simp
qed simp
lemma finite_subst_domain_subst:
"finite (subst_domain (subst x y))"
by simp
lemma subst_domain_compose:
"subst_domain (σ ∘⇩s τ) ⊆ subst_domain σ ∪ subst_domain τ"
by (auto simp: subst_domain_def subst_compose_def)
lemma vars_term_disjoint_imp_unifier:
fixes σ :: "('f, 'v, 'w) gsubst"
assumes "vars_term s ∩ vars_term t = {}"
and "s ⋅ σ = t ⋅ τ"
shows "∃μ :: ('f, 'v, 'w) gsubst. s ⋅ μ = t ⋅ μ"
proof -
let ?μ = "λx. if x ∈ vars_term s then σ x else τ x"
have "s ⋅ σ = s ⋅ ?μ"
unfolding term_subst_eq_conv
by (induct s) (simp_all)
moreover have "t ⋅ τ = t ⋅ ?μ"
using assms(1)
unfolding term_subst_eq_conv
by (induct s arbitrary: t) (auto)
ultimately have "s ⋅ ?μ = t ⋅ ?μ" using assms(2) by simp
then show ?thesis by blast
qed
lemma vars_term_subset_subst_eq:
assumes "vars_term t ⊆ vars_term s"
and "s ⋅ σ = s ⋅ τ"
shows "t ⋅ σ = t ⋅ τ"
using assms by (induct t) (induct s, auto)
end