Theory 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
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