Theory First_Order_Terms.Term

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
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 _) = []"

lemmas is_VarI = term.disc(1)
lemmas is_FunI = term.disc(2)

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 contributor ‹Martin Desharnais›
  inj_on_Fun_fun[simp]: "A ts. inj_on (λf. Fun f ts) A" and
  inj_on_Fun_args[simp]: "A f. inj_on (λts. Fun f ts) A" and
  inj_on_Fun[simp]: "A. inj_on Fun A"
  unfolding atomize_conj atomize_all
  by (metis (mono_tags, lifting) inj_on_def term.inject(2))

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  (xV. vars_term (ρ x))"
    using term.set_sel(3) by force
next
  from is_var_σ show "x. x  (xV. 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 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") = 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
  "IVar xα = α x"
| "IFun f ssα = I f [Isα. 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 "Isα = Isβ"
  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 "Isα = Itβ"
  by (fold ref, rule eval_same_vars, auto dest:v)

lemma eval_with_fresh_var: "x  vars_term s  Isα(x:=a) = Isα"
  by (auto intro: eval_same_vars)

lemma eval_map_term: "Imap_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)"
  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)"
  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 σ"
    by (simp_all add: subst_domain_def)
qed

lemma subst_domain_Var [simp]:
  "subst_domain Var = {}"
  by (simp add: subst_domain_def)

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

lemma range_vars_Var[simp]: contributor ‹Martin Desharnais›
  "range_vars Var = {}"
  by (simp add: range_vars_def)

lemma subst_apply_term_ident: contributor ‹Martin Desharnais›
  "vars_term t  subst_domain σ = {}  t  σ = t"
proof (induction t)
  case (Var x)
  thus ?case
    by (simp add: subst_domain_def)
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 "set" 60)
  where
    "T set σ  (λ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.
  (See also "Term Rewriting and All That" cite‹Lemma 4.5.7› in "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. yvars_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. yvars_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"
      by (simp add: disjoint_iff subst_domain_def)
    ultimately show ?thesis
      by (simp add: subst_compose_def)
  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 σ"
        by (simp_all add: subst_domain_def)
    qed
    hence "y  subst_domain δ"
      using range_vars σ  subst_domain δ = {}
      by (simp add: disjoint_iff)
    with Var show ?thesis
      unfolding subst_compose_def
      by (simp add: subst_domain_def)
  qed
next
  case (Fun f ys)
  hence "Fun f ys  subst_range σ  (yset 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 δ = {}
    by (simp add: disjoint_iff subst_domain_def)
  from this[unfolded subst_apply_term_empty] Fun show ?thesis
    by (simp add: subst_compose_def)
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']
      by (simp add: t_def rename_subst_domain_def)
  next
    case False
    hence False
      using rename_subst_domain ρ σ x  Var x
      by (simp add: t_def rename_subst_domain_def)
    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 ρ σ"
    by (simp add: subst_compose_def)
  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))"
    by (simp add: ρ_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 eval_map_vars: "Imap_vars_term f tα = It(αf)"
  by (simp add: eval_map_term o_def)

lemma apply_subst_map_vars_term:
  "map_vars_term m t  σ = t  (σ  m)" using eval_map_vars.

lemmas eval_o = eval_map_vars[symmetric]

lemma eval_eq_map_vars:
  assumes 1: "t = map_vars_term f s" and 2: "x. x  vars_term s  α x = β (f x)"
  shows "Isα = Itβ"
  by (unfold 1, insert 2, unfold eval_map_vars, rule eval_same_vars, auto)

lemma ground_term_subst: "vars_term t = {}  tθ = t"
  by (induct t, auto simp: list_eq_iff_nth_eq)

end