# Theory First_Order_Terms.Term

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)
section ‹First-Order Terms›

theory Term
imports
Main
"HOL-Library.Multiset"
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

lemma inj_on_Var[simp]: ✐‹contributor ‹Martin Desharnais››
"inj_on Var A"
by (rule inj_onI) simp

lemma member_image_the_Var_image_subst: ✐‹contributor ‹Martin Desharnais››
assumes is_var_σ: "∀x. is_Var (σ x)"
shows "x ∈ the_Var  σ  V ⟷ Var x ∈ σ  V"
using is_var_σ image_iff
by (metis (no_types, opaque_lifting) term.collapse(1) term.sel(1))

lemma image_the_Var_image_subst_renaming_eq: ✐‹contributor ‹Martin Desharnais››
assumes is_var_σ: "∀x. is_Var (ρ x)"
shows "the_Var  ρ  V = (⋃x ∈ V. vars_term (ρ x))"
proof (rule Set.equalityI; rule Set.subsetI)
from is_var_σ show "⋀x. x ∈ the_Var  ρ  V ⟹ x ∈ (⋃x∈V. vars_term (ρ x))"
using term.set_sel(3) by force
next
from is_var_σ show "⋀x. x ∈ (⋃x∈V. vars_term (ρ x)) ⟹ x ∈ the_Var  ρ  V"
by (smt (verit, best) Term.term.simps(17) UN_iff image_eqI singletonD term.collapse(1))
qed

text ‹The variables of a term as multiset.›
fun vars_term_ms :: "('f, 'v) term ⇒ 'v multiset"
where
"vars_term_ms (Var x) = {#x#}" |
"vars_term_ms (Fun f ts) = ∑⇩# (mset (map vars_term_ms ts))"

lemma set_mset_vars_term_ms [simp]:
"set_mset (vars_term_ms t) = vars_term t"
by (induct t) auto

text ‹Reorient equations of the form @{term "Var x = t"} and @{term "Fun f ss = t"} to facilitate
simplification.›
setup ‹
(fn Const (@{const_name Var}, _) $_ => true | _ => false) #> Reorient_Proc.add (fn Const (@{const_name Fun}, _)$ _ \$ _ => true | _ => false)
›

simproc_setup reorient_Var ("Var x = t") = ‹K Reorient_Proc.proc›
simproc_setup reorient_Fun ("Fun f ss = t") = ‹K 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 ‹We define the evaluation of terms, under interpretation of function symbols and assignment of
variables, as follows:›

fun eval_term ("_⟦(2_)⟧_" [999,1,100]100) where
"I⟦Var x⟧α = α x"
| "I⟦Fun f ss⟧α = I f [I⟦s⟧α. s ← ss]"

notation eval_term ("_⟦(2_)⟧" [999,1]100)
notation eval_term ("_⟦(2_)⟧_" [999,1,100]100)

lemma eval_same_vars:
assumes "∀x ∈ vars_term s. α x = β x"
shows "I⟦s⟧α = I⟦s⟧β"
by (insert assms, induct s, auto intro!:map_cong[OF refl] cong[of "I _"])

lemma eval_same_vars_cong:
assumes ref: "s = t" and v: "⋀x. x ∈ vars_term s ⟹ α x = β x"
shows "I⟦s⟧α = I⟦t⟧β"
by (fold ref, rule eval_same_vars, auto dest:v)

lemma eval_with_fresh_var: "x ∉ vars_term s ⟹ I⟦s⟧α(x:=a) = I⟦s⟧α"
by (auto intro: eval_same_vars)

lemma eval_map_term: "I⟦map_term ff fv s⟧α = (I ∘ ff)⟦s⟧(α ∘ fv)"
by (induct s, auto intro: cong[of "I _"])

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"

abbreviation subst_apply_term :: "('f, 'v) term ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term"  (infixl "⋅" 67)
where "subst_apply_term ≡ eval_term Fun"

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) (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)"

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)"
by (auto intro!: term_subst_eq term_subst_eq_rev)

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 σ"

lemma vars_term_ms_subst [simp]:
"vars_term_ms (t ⋅ σ) =
(∑x∈#vars_term_ms t. vars_term_ms (σ x))" (is "_ = ?V t")
proof (induct t)
case (Fun f ts)
have IH: "map (λ t. vars_term_ms (t ⋅ σ)) ts = map (λ t. ?V t) ts"
by (rule map_cong[OF refl Fun])
show ?case by (simp add: o_def IH, induct ts, auto)
qed simp

lemma vars_term_ms_subst_mono:
assumes "vars_term_ms s ⊆# vars_term_ms t"
shows "vars_term_ms (s ⋅ σ) ⊆# vars_term_ms (t ⋅ σ)"
proof -
from assms[unfolded mset_subset_eq_exists_conv] obtain u where t: "vars_term_ms t = vars_term_ms s + u" by auto
show ?thesis unfolding vars_term_ms_subst unfolding t by auto
qed

text ‹The variables introduced by a substitution.›
definition range_vars :: "('f, 'v) subst ⇒ 'v set"
where
"range_vars σ = ⋃(vars_term  subst_range σ)"

lemma mem_range_varsI: ✐‹contributor ‹Martin Desharnais››
assumes "σ x = Var y" and "x ≠ y"
shows "y ∈ range_vars σ"
unfolding range_vars_def UN_iff
proof (rule bexI[of _ "Var y"])
show "y ∈ vars_term (Var y)"
by simp
next
from assms show "Var y ∈ subst_range σ"
qed

lemma subst_domain_Var [simp]:
"subst_domain Var = {}"

lemma subst_range_Var[simp]: ✐‹contributor ‹Martin Desharnais››
"subst_range Var = {}"
by simp

lemma range_vars_Var[simp]: ✐‹contributor ‹Martin Desharnais››
"range_vars Var = {}"

lemma subst_apply_term_ident: ✐‹contributor ‹Martin Desharnais››
"vars_term t ∩ subst_domain σ = {} ⟹ t ⋅ σ = t"
proof (induction t)
case (Var x)
thus ?case
next
case (Fun f ts)
thus ?case
by (auto intro: list.map_ident_strong)
qed

lemma vars_term_subst_apply_term: ✐‹contributor ‹Martin Desharnais››
"vars_term (t ⋅ σ) = (⋃x ∈ vars_term t. vars_term (σ x))"
by (induction t) (auto simp add: insert_Diff_if subst_domain_def)

corollary vars_term_subst_apply_term_subset: ✐‹contributor ‹Martin Desharnais››
"vars_term (t ⋅ σ) ⊆ vars_term t - subst_domain σ ∪ range_vars σ"
unfolding vars_term_subst_apply_term
proof (induction t)
case (Var x)
show ?case
by (cases "σ x = Var x") (auto simp add: range_vars_def subst_domain_def)
next
case (Fun f xs)
thus ?case by auto
qed

definition is_renaming :: "('f, 'v) subst ⇒ bool"
where
"is_renaming σ ⟷ (∀x. is_Var (σ x)) ∧ inj_on σ (subst_domain σ)"

lemma inv_renaming_sound: ✐‹contributor ‹Martin Desharnais››
assumes is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
shows "ρ ∘⇩s (Var ∘ (inv (the_Var ∘ ρ))) = Var"
proof -
define ρ' where "ρ' = the_Var ∘ ρ"
have ρ_def: "ρ = Var ∘ ρ'"
unfolding ρ'_def using is_var_ρ by auto

from is_var_ρ ‹inj ρ› have "inj ρ'"
unfolding inj_def ρ_def comp_def by fast
hence "inv ρ' ∘ ρ' = id"
using inv_o_cancel[of ρ'] by simp
hence "Var ∘ (inv ρ' ∘ ρ') = Var"
by simp
hence "∀x. (Var ∘ (inv ρ' ∘ ρ')) x = Var x"
by metis
hence "∀x. ((Var ∘ ρ') ∘⇩s (Var ∘ (inv ρ'))) x = Var x"
unfolding subst_compose_def by auto
thus "ρ ∘⇩s (Var ∘ (inv ρ')) = Var"
using ρ_def by auto
qed

lemma ex_inverse_of_renaming: ✐‹contributor ‹Martin Desharnais››
assumes "∀x. is_Var (ρ x)" and "inj ρ"
shows "∃τ. ρ ∘⇩s τ = Var"
using inv_renaming_sound[OF assms] by blast

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_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.
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

lemma subst_compose_apply_eq_apply_lhs: ✐‹contributor ‹Martin Desharnais››
assumes
"range_vars σ ∩ subst_domain δ = {}"
"x ∉ subst_domain δ"
shows "(σ ∘⇩s δ) x = σ x"
proof (cases "σ x")
case (Var y)
show ?thesis
proof (cases "x = y")
case True
with Var have ‹σ x = Var x›
by simp
moreover from ‹x ∉ subst_domain δ› have "δ x = Var x"
ultimately show ?thesis
next
case False
have "y ∈ range_vars σ"
unfolding range_vars_def UN_iff
proof (rule bexI)
show "y ∈ vars_term (Var y)"
by simp
next
from Var False show "Var y ∈ subst_range σ"
qed
hence "y ∉ subst_domain δ"
using ‹range_vars σ ∩ subst_domain δ = {}›
with Var show ?thesis
unfolding subst_compose_def
qed
next
case (Fun f ys)
hence "Fun f ys ∈ subst_range σ ∨ (∀y∈set ys. y ∈ subst_range σ)"
using subst_domain_def by fastforce
hence "∀x ∈ vars_term (Fun f ys). x ∈ range_vars σ"
by (metis UN_I range_vars_def term.distinct(1) term.sel(4) term.set_cases(2))
hence "Fun f ys ⋅ δ = Fun f ys ⋅ Var"
unfolding term_subst_eq_conv
using ‹range_vars σ ∩ subst_domain δ = {}›
from this[unfolded subst_apply_term_empty] Fun show ?thesis
qed

lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs: ✐‹contributor ‹Martin Desharnais››
assumes "range_vars σ ∩ subst_domain δ = {}" and "vars_term t ∩ subst_domain δ = {}"
shows "t ⋅ σ ⋅ δ = t ⋅ σ"
proof -
from assms have "⋀x. x ∈ vars_term t ⟹ (σ ∘⇩s δ) x = σ x"
using subst_compose_apply_eq_apply_lhs by fastforce
hence "t ⋅ σ ∘⇩s δ = t ⋅ σ"
using term_subst_eq_conv by metis
thus ?thesis
by simp
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)

subsection ‹Restrict the Domain of a Substitution›

definition restrict_subst_domain where ✐‹contributor ‹Martin Desharnais››
"restrict_subst_domain V σ x ≡ (if x ∈ V then σ x else Var x)"

lemma restrict_subst_domain_empty[simp]: ✐‹contributor ‹Martin Desharnais››
"restrict_subst_domain {} σ = Var"
unfolding restrict_subst_domain_def by auto

lemma restrict_subst_domain_Var[simp]: ✐‹contributor ‹Martin Desharnais››
"restrict_subst_domain V Var = Var"
unfolding restrict_subst_domain_def by auto

lemma subst_domain_restrict_subst_domain[simp]: ✐‹contributor ‹Martin Desharnais››
"subst_domain (restrict_subst_domain V σ) = V ∩ subst_domain σ"
unfolding restrict_subst_domain_def subst_domain_def by auto

lemma subst_apply_term_restrict_subst_domain: ✐‹contributor ‹Martin Desharnais››
"vars_term t ⊆ V ⟹ t ⋅ restrict_subst_domain V σ = t ⋅ σ"
by (rule term_subst_eq) (simp add: restrict_subst_domain_def subsetD)

subsection ‹Rename the Domain of a Substitution›

definition rename_subst_domain where ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain ρ σ x =
(if Var x ∈ ρ  subst_domain σ then
σ (the_inv ρ (Var x))
else
Var x)"

lemma rename_subst_domain_Var_lhs[simp]: ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain Var σ = σ"
by (rule ext) (simp add: rename_subst_domain_def inj_image_mem_iff the_inv_f_f subst_domain_def)

lemma rename_subst_domain_Var_rhs[simp]: ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain ρ Var = Var"
by (rule ext) (simp add: rename_subst_domain_def)

lemma subst_domain_rename_subst_domain_subset: ✐‹contributor ‹Martin Desharnais››
assumes is_var_ρ: "∀x. is_Var (ρ x)"
shows "subst_domain (rename_subst_domain ρ σ) ⊆ the_Var  ρ  subst_domain σ"
by (auto simp add: subst_domain_def rename_subst_domain_def
member_image_the_Var_image_subst[OF is_var_ρ])

lemma subst_range_rename_subst_domain_subset: ✐‹contributor ‹Martin Desharnais››
assumes "inj ρ"
shows "subst_range (rename_subst_domain ρ σ) ⊆ subst_range σ"
proof (intro Set.equalityI Set.subsetI)
fix t assume "t ∈ subst_range (rename_subst_domain ρ σ)"
then obtain x where
t_def: "t = rename_subst_domain ρ σ x" and
"rename_subst_domain ρ σ x ≠ Var x"
by (auto simp: image_iff subst_domain_def)

show "t ∈ subst_range σ"
proof (cases ‹Var x ∈ ρ  subst_domain σ›)
case True
then obtain x' where "ρ x' = Var x" and "x' ∈ subst_domain σ"
by auto
then show ?thesis
using the_inv_f_f[OF ‹inj ρ›, of x']
next
case False
hence False
using ‹rename_subst_domain ρ σ x ≠ Var x›
thus ?thesis ..
qed
qed

lemma range_vars_rename_subst_domain_subset: ✐‹contributor ‹Martin Desharnais››
assumes "inj ρ"
shows "range_vars (rename_subst_domain ρ σ) ⊆ range_vars σ"
unfolding range_vars_def
using subst_range_rename_subst_domain_subset[OF ‹inj ρ›]
by (metis Union_mono image_mono)

lemma renaming_cancels_rename_subst_domain: ✐‹contributor ‹Martin Desharnais››
assumes is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ" and vars_t: "vars_term t ⊆ subst_domain σ"
shows "t ⋅ ρ ⋅ rename_subst_domain ρ σ = t ⋅ σ"
unfolding subst_subst
proof (intro term_subst_eq ballI)
fix x assume "x ∈ vars_term t"
with vars_t have x_in: "x ∈ subst_domain σ"
by blast

obtain x' where ρ_x: "ρ x = Var x'"
using is_var_ρ by (meson is_Var_def)
with x_in have x'_in: "Var x' ∈ ρ  subst_domain σ"
by (metis image_eqI)

have "(ρ ∘⇩s rename_subst_domain ρ σ) x = ρ x ⋅ rename_subst_domain ρ σ"
also have "… = rename_subst_domain ρ σ x'"
using ρ_x by simp
also have "… = σ (the_inv ρ (Var x'))"
by (simp add: rename_subst_domain_def if_P[OF x'_in])
also have "… = σ (the_inv ρ (ρ x))"
also have "… = σ x"
using ‹inj ρ› by (simp add: the_inv_f_f)
finally show "(ρ ∘⇩s rename_subst_domain ρ σ) x = σ x"
by simp
qed

subsection ‹Rename the Domain and Range of a Substitution›

definition rename_subst_domain_range where ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain_range ρ σ x =
(if Var x ∈ ρ  subst_domain σ then
((Var o the_inv ρ) ∘⇩s σ ∘⇩s ρ) (Var x)
else
Var x)"

lemma rename_subst_domain_range_Var_lhs[simp]: ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain_range Var σ = σ"
by (rule ext) (simp add: rename_subst_domain_range_def inj_image_mem_iff the_inv_f_f
subst_domain_def subst_compose_def)

lemma rename_subst_domain_range_Var_rhs[simp]: ✐‹contributor ‹Martin Desharnais››
"rename_subst_domain_range ρ Var = Var"
by (rule ext) (simp add: rename_subst_domain_range_def)

lemma subst_compose_renaming_rename_subst_domain_range: ✐‹contributor ‹Martin Desharnais››
fixes σ ρ :: "('f, 'v) subst"
assumes is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
shows "ρ ∘⇩s rename_subst_domain_range ρ σ = σ ∘⇩s ρ"
proof (rule ext)
fix x
from is_var_ρ obtain x' where "ρ x = Var x'"
by (meson is_Var_def is_renaming_def)
with ‹inj ρ› have inv_ρ_x': "the_inv ρ (Var x') = x"
by (metis the_inv_f_f)

show "(ρ ∘⇩s rename_subst_domain_range ρ σ) x = (σ ∘⇩s ρ) x"
proof (cases "x ∈ subst_domain σ")
case True
hence "Var x' ∈ ρ  subst_domain σ"
using ‹ρ x = Var x'› by (metis imageI)
thus ?thesis
by (simp add: ‹ρ x = Var x'› rename_subst_domain_range_def subst_compose_def inv_ρ_x')
next
case False
hence "Var x' ∉ ρ  subst_domain σ"
proof (rule contrapos_nn)
assume "Var x' ∈ ρ  subst_domain σ"
hence "ρ x ∈ ρ  subst_domain σ"
unfolding ‹ρ x = Var x'› .
thus "x ∈ subst_domain σ"
unfolding inj_image_mem_iff[OF ‹inj ρ›] .
qed
with False ‹ρ x = Var x'› show ?thesis
by (simp add: subst_compose_def subst_domain_def rename_subst_domain_range_def)
qed
qed

corollary subst_apply_term_renaming_rename_subst_domain_range: ✐‹contributor ‹Martin Desharnais››
― ‹This might be easier to find with @{command find_theorems}.›
fixes t :: "('f, 'v) term" and σ ρ :: "('f, 'v) subst"
assumes is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
shows "t ⋅ ρ ⋅ rename_subst_domain_range ρ σ = t ⋅ σ ⋅ ρ"
unfolding subst_subst
unfolding subst_compose_renaming_rename_subst_domain_range[OF assms]
by (rule refl)

text ‹A term is called ∗‹ground› if it does not contain any variables.›
fun ground :: "('f, 'v) term ⇒ bool"
where
"ground (Var x) ⟷ False" |
"ground (Fun f ts) ⟷ (∀t ∈ set ts. ground t)"

lemma ground_vars_term_empty:
"ground t ⟷ vars_term t = {}"
by (induct t) simp_all

lemma ground_subst [simp]:
"ground (t ⋅ σ) ⟷ (∀x ∈ vars_term t. ground (σ x))"
by (induct t) simp_all

lemma ground_subst_apply:
assumes "ground t"
shows "t ⋅ σ = t"
proof -
have "t = t ⋅ Var" by simp
also have "… = t ⋅ σ"
by (rule term_subst_eq, insert assms[unfolded ground_vars_term_empty], auto)
finally show ?thesis by simp
qed

text ‹Just changing the variables in a term›

abbreviation "map_vars_term f ≡ term.map_term (λx. x) f"

lemma map_vars_term_as_subst:
"map_vars_term f t = t ⋅ (λ x. Var (f x))"
by (induct t) simp_all

lemma map_vars_term_eq:
"map_vars_term f s = s ⋅ (Var ∘ f)"
by (induct s) auto

lemma ground_map_vars_term [simp]:
"ground (map_vars_term f t) = ground t"
by (induct t) simp_all

lemma map_vars_term_subst [simp]:
"map_vars_term f (t ⋅ σ) = t ⋅ (λ x. map_vars_term f (σ x))"
by (induct t) simp_all

lemma map_vars_term_compose:
"map_vars_term m1 (map_vars_term m2 t) = map_vars_term (m1 o m2) t"
by (induct t) simp_all

lemma map_vars_term_id [simp]:
"map_vars_term id t = t"
by (induct t) (auto intro: map_idI)

lemma apply_subst_map_vars_term:
"map_vars_term m t ⋅ σ = t ⋅ (σ ∘ m)"
by (induct t) (auto)

end