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 ∈ (⋃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 ‹
  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
  "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 eval_subst (‹_⟦_⟧⇩s _› [999,1,100]100) where
  "(I⟦θ⟧⇩s α) ≡ λx. I⟦θ x⟧α"

lemma eval_subst: "I⟦s⋅θ⟧α = I⟦s⟧ I⟦θ⟧⇩s α"
  apply (induct s) by (auto simp: eval_subst_def cong:map_cong)

abbreviation
  subst_compose :: "('f, 'u, 'v) gsubst ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'u, 'w) gsubst"
  (infixl ‹∘⇩s› 75)
  where
    "σ ∘⇩s θ ≡ Fun⟦σ⟧⇩s θ"

lemmas subst_compose_def = eval_subst_def[of Fun]

lemma subst_subst_compose [simp]:
  "t ⋅ (σ ∘⇩s τ) = t ⋅ σ ⋅ τ"
  by (induct t) (simp_all add: eval_subst_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: eval_subst_def)
    also have "… = σ(x) ⋅ (τ ∘⇩s μ)" by simp
    finally show ?thesis by (simp add: eval_subst_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: eval_subst_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 eval_subst_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:  eval_subst_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  eval_subst_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: eval_subst_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 eval_subst_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 eval_subst_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: eval_subst_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: eval_subst_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 eval_subst_def
      by (simp add: subst_domain_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 δ = {}›
    by (simp add: disjoint_iff subst_domain_def)
  from this[unfolded subst_apply_term_empty] Fun show ?thesis
    by (simp add: eval_subst_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 eval_subst_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: eval_subst_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 eval_subst_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 eval_subst_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: eval_subst_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: "I⟦map_vars_term f t⟧α = I⟦t⟧(α∘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 "I⟦s⟧α = I⟦t⟧β"
  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