diff --git a/thys/First_Order_Terms/Term.thy b/thys/First_Order_Terms/Term.thy
--- a/thys/First_Order_Terms/Term.thy
+++ b/thys/First_Order_Terms/Term.thy
@@ -1,499 +1,551 @@
 (*
 Author:  Christian Sternagel <c.sternagel@gmail.com>
 Author:  René Thiemann <rene.thiemann@uibk.ac.at>
 License: LGPL
 *)
 section \<open>First-Order Terms\<close>
 
 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 \<equiv> \<not> is_Var t"
 
 lemma is_VarE [elim]:
   "is_Var t \<Longrightarrow> (\<And>x. t = Var x \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases t) auto
 
 lemma is_FunE [elim]:
   "is_Fun t \<Longrightarrow> (\<And>f ts. t = Fun f ts \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases t) auto
 
 text \<open>Reorient equations of the form @{term "Var x = t"} and @{term "Fun f ss = t"} to facilitate
   simplification.\<close>
 setup \<open>
   Reorient_Proc.add
     (fn Const (@{const_name Var}, _) $ _ => true | _ => false)
   #> Reorient_Proc.add
     (fn Const (@{const_name Fun}, _) $ _ $ _ => true | _ => false)
 \<close>
 
 simproc_setup reorient_Var ("Var x = t") = Reorient_Proc.proc
 simproc_setup reorient_Fun ("Fun f ss = t") = Reorient_Proc.proc
 
 text \<open>The \emph{root symbol} of a term is defined by:\<close>
 fun root :: "('f, 'v) term \<Rightarrow> ('f \<times> 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 (\<Union>t \<in> set ts. vars_term t)"
   by auto
 
 text \<open>A substitution is a mapping \<open>\<sigma>\<close> 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).\<close>
 type_synonym ('f, 'v, 'w) gsubst = "'v \<Rightarrow> ('f, 'w) term"
 type_synonym ('f, 'v) subst  = "('f, 'v, 'v) gsubst"
 
 fun subst_apply_term :: "('f, 'v) term \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'w) term" (infixl "\<cdot>" 67)
   where
     "Var x \<cdot> \<sigma> = \<sigma> x"
   | "Fun f ss \<cdot> \<sigma> = Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ss)"
 
 definition
   subst_compose :: "('f, 'u, 'v) gsubst \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'u, 'w) gsubst"
   (infixl "\<circ>\<^sub>s" 75)
   where
     "\<sigma> \<circ>\<^sub>s \<tau> = (\<lambda>x. (\<sigma> x) \<cdot> \<tau>)"
 
 lemma subst_subst_compose [simp]:
   "t \<cdot> (\<sigma> \<circ>\<^sub>s \<tau>) = t \<cdot> \<sigma> \<cdot> \<tau>"
   by (induct t \<sigma> rule: subst_apply_term.induct) (simp_all add: subst_compose_def)
 
 lemma subst_compose_assoc:
   "\<sigma> \<circ>\<^sub>s \<tau> \<circ>\<^sub>s \<mu> = \<sigma> \<circ>\<^sub>s (\<tau> \<circ>\<^sub>s \<mu>)"
 proof (rule ext)
   fix x show "(\<sigma> \<circ>\<^sub>s \<tau> \<circ>\<^sub>s \<mu>) x = (\<sigma> \<circ>\<^sub>s (\<tau> \<circ>\<^sub>s \<mu>)) x"
   proof -
     have "(\<sigma> \<circ>\<^sub>s \<tau> \<circ>\<^sub>s \<mu>) x = \<sigma>(x) \<cdot> \<tau> \<cdot> \<mu>" by (simp add: subst_compose_def)
     also have "\<dots> = \<sigma>(x) \<cdot> (\<tau> \<circ>\<^sub>s \<mu>)" by simp
     finally show ?thesis by (simp add: subst_compose_def)
   qed
 qed
 
 lemma subst_apply_term_empty [simp]:
   "t \<cdot> 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" "(\<circ>\<^sub>s)"
   by (unfold_locales) (simp add: subst_compose_assoc, simp_all add: subst_compose_def)
 
 lemma term_subst_eq:
   assumes "\<And>x. x \<in> vars_term t \<Longrightarrow> \<sigma> x = \<tau> x"
   shows "t \<cdot> \<sigma> = t \<cdot> \<tau>"
   using assms by (induct t) (auto)
 
 lemma term_subst_eq_rev:
   "t \<cdot> \<sigma> = t \<cdot> \<tau> \<Longrightarrow> \<forall>x \<in> vars_term t. \<sigma> x = \<tau> x"
   by (induct t) simp_all
 
 lemma term_subst_eq_conv:
   "t \<cdot> \<sigma> = t \<cdot> \<tau> \<longleftrightarrow> (\<forall>x \<in> vars_term t. \<sigma> x = \<tau> x)"
   using term_subst_eq [of t \<sigma> \<tau>] and term_subst_eq_rev [of t \<sigma> \<tau>] by auto
 
 lemma subst_term_eqI:
   assumes "(\<And>t. t \<cdot> \<sigma> = t \<cdot> \<tau>)"
   shows "\<sigma> = \<tau>"
   using assms [of "Var x" for x] by (intro ext) simp
 
 definition subst_domain :: "('f, 'v) subst \<Rightarrow> 'v set"
   where
     "subst_domain \<sigma> = {x. \<sigma> x \<noteq> Var x}"
 
 fun subst_range :: "('f, 'v) subst \<Rightarrow> ('f, 'v) term set"
   where
     "subst_range \<sigma> = \<sigma> ` subst_domain \<sigma>"
 
 text \<open>The variables introduced by a substitution.\<close>
 definition range_vars :: "('f, 'v) subst \<Rightarrow> 'v set"
 where
   "range_vars \<sigma> = \<Union>(vars_term ` subst_range \<sigma>)"
 
 lemma subst_domain_Var [simp]:
   "subst_domain Var = {}"
   by (simp add: subst_domain_def)
 
 lemma subst_range_Var[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "subst_range Var = {}"
   by simp
 
 lemma range_vars_Var[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "range_vars Var = {}"
   by (simp add: range_vars_def)
 
 lemma subst_apply_term_ident: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "vars_term t \<inter> subst_domain \<sigma> = {} \<Longrightarrow> t \<cdot> \<sigma> = 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: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "vars_term (t \<cdot> \<sigma>) = (\<Union>x \<in> vars_term t. vars_term (\<sigma> x))"
   by (induction t) (auto simp add: insert_Diff_if subst_domain_def)
 
 corollary vars_term_subst_apply_term_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "vars_term (t \<cdot> \<sigma>) \<subseteq> vars_term t - subst_domain \<sigma> \<union> range_vars \<sigma>"
   unfolding vars_term_subst_apply_term
 proof (induction t)
   case (Var x)
   show ?case
     by (cases "\<sigma> 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 \<Rightarrow> bool"
   where
     "is_renaming \<sigma> \<longleftrightarrow> (\<forall>x. is_Var (\<sigma> x)) \<and> inj_on \<sigma> (subst_domain \<sigma>)"
 
 lemma inv_renaming_sound: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
   shows "\<rho> \<circ>\<^sub>s (Var \<circ> (inv (the_Var \<circ> \<rho>))) = Var"
 proof -
   define \<rho>' where "\<rho>' = the_Var \<circ> \<rho>"
   have \<rho>_def: "\<rho> = Var \<circ> \<rho>'"
     unfolding \<rho>'_def using is_var_\<rho> by auto
 
   from is_var_\<rho> \<open>inj \<rho>\<close> have "inj \<rho>'"
     unfolding inj_def \<rho>_def comp_def by fast
   hence "inv \<rho>' \<circ> \<rho>' = id"
     using inv_o_cancel[of \<rho>'] by simp
   hence "Var \<circ> (inv \<rho>' \<circ> \<rho>') = Var"
     by simp
   hence "\<forall>x. (Var \<circ> (inv \<rho>' \<circ> \<rho>')) x = Var x"
     by metis
   hence "\<forall>x. ((Var \<circ> \<rho>') \<circ>\<^sub>s (Var \<circ> (inv \<rho>'))) x = Var x"
     unfolding subst_compose_def by auto
   thus "\<rho> \<circ>\<^sub>s (Var \<circ> (inv \<rho>')) = Var"
     using \<rho>_def by auto
 qed
 
 lemma ex_inverse_of_renaming: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
   shows "\<exists>\<tau>. \<rho> \<circ>\<^sub>s \<tau> = Var"
   using inv_renaming_sound[OF assms] by blast
 
 lemma vars_term_subst:
   "vars_term (t \<cdot> \<sigma>) = \<Union>(vars_term ` \<sigma> ` vars_term t)"
   by (induct t) simp_all
 
 lemma range_varsE [elim]:
   assumes "x \<in> range_vars \<sigma>"
     and "\<And>t. x \<in> vars_term t \<Longrightarrow> t \<in> subst_range \<sigma> \<Longrightarrow> P"
   shows "P"
   using assms by (auto simp: range_vars_def)
 
 lemma range_vars_subst_compose_subset:
   "range_vars (\<sigma> \<circ>\<^sub>s \<tau>) \<subseteq> (range_vars \<sigma> - subst_domain \<tau>) \<union> range_vars \<tau>" (is "?L \<subseteq> ?R")
 proof
   fix x
   assume "x \<in> ?L"
   then obtain y where "y \<in> subst_domain (\<sigma> \<circ>\<^sub>s \<tau>)"
     and "x \<in> vars_term ((\<sigma> \<circ>\<^sub>s \<tau>) y)" by (auto simp: range_vars_def)
   then show "x \<in> ?R"
   proof (cases)
     assume "y \<in> subst_domain \<sigma>" and "x \<in> vars_term ((\<sigma> \<circ>\<^sub>s \<tau>) y)"
     moreover then obtain v where "v \<in> vars_term (\<sigma> y)"
       and "x \<in> vars_term (\<tau> v)" by (auto simp: subst_compose_def vars_term_subst)
     ultimately show ?thesis
       by (cases "v \<in> subst_domain \<tau>") (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 \<in> {y. subst x t y \<noteq> Var y} \<longleftrightarrow> y \<in> (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 "\<sigma> x = t \<cdot> \<sigma>"
   shows "s \<cdot> subst x t \<cdot> \<sigma> = s \<cdot> \<sigma>"
   using assms by (induct s) (auto simp: subst_def)
 
 lemma subst_compose_left_idemp [simp]:
   assumes "\<sigma> x = t \<cdot> \<sigma>"
   shows "subst x t \<circ>\<^sub>s \<sigma> = \<sigma>"
   by (rule subst_term_eqI) (simp add: assms)
 
 lemma subst_ident [simp]:
   assumes "x \<notin> vars_term t"
   shows "t \<cdot> subst x u = t"
 proof -
   have "t \<cdot> subst x u = t \<cdot> Var"
     by (rule term_subst_eq) (auto simp: assms subst_def)
   then show ?thesis by simp
 qed
 
 lemma subst_self_idemp [simp]:
   "x \<notin> vars_term t \<Longrightarrow> subst x t \<circ>\<^sub>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 \<open>Applying a substitution to every term of a given set.\<close>
 abbreviation
   subst_apply_set :: "('f, 'v) terms \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'w) terms" (infixl "\<cdot>\<^sub>s\<^sub>e\<^sub>t" 60)
   where
     "T \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma> \<equiv> (\<lambda>t. t \<cdot> \<sigma>) ` T"
 
 text \<open>Composition of substitutions\<close>
 lemma subst_compose: "(\<sigma> \<circ>\<^sub>s \<tau>) x = \<sigma> x \<cdot> \<tau>" by (auto simp: subst_compose_def)
 
 lemmas subst_subst = subst_subst_compose [symmetric]
 
 lemma subst_apply_eq_Var:
   assumes "s \<cdot> \<sigma> = Var x"
   obtains y where "s = Var y" and "\<sigma> y = Var x"
   using assms by (induct s) auto
 
 lemma subst_domain_subst_compose:
   "subst_domain (\<sigma> \<circ>\<^sub>s \<tau>) =
     (subst_domain \<sigma> - {x. \<exists>y. \<sigma> x = Var y \<and> \<tau> y = Var x}) \<union>
     (subst_domain \<tau> - subst_domain \<sigma>)"
   by (auto simp: subst_domain_def subst_compose_def elim: subst_apply_eq_Var)
 
 
 text \<open>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}.)\<close>
 lemma subst_idemp_iff:
   "\<sigma> \<circ>\<^sub>s \<sigma> = \<sigma> \<longleftrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
 proof
   assume "\<sigma> \<circ>\<^sub>s \<sigma> = \<sigma>"
   then have "\<And>x. \<sigma> x \<cdot> \<sigma> = \<sigma> x \<cdot> Var" by simp (metis subst_compose_def)
   then have *: "\<And>x. \<forall>y\<in>vars_term (\<sigma> x). \<sigma> y = Var y"
     unfolding term_subst_eq_conv by simp
   { fix x y
     assume "\<sigma> x \<noteq> Var x" and "x \<in> vars_term (\<sigma> y)"
     with * [of y] have False by simp }
   then show "subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
     by (auto simp: subst_domain_def range_vars_def)
 next
   assume "subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
   then have *: "\<And>x y. \<sigma> x = Var x \<or> \<sigma> y = Var y \<or> x \<notin> vars_term (\<sigma> y)"
     by (auto simp: subst_domain_def range_vars_def)
   have "\<And>x. \<forall>y\<in>vars_term (\<sigma> x). \<sigma> y = Var y"
   proof
     fix x y
     assume "y \<in> vars_term (\<sigma> x)"
     with * [of y x] show "\<sigma> y = Var y" by auto
   qed
   then show "\<sigma> \<circ>\<^sub>s \<sigma> = \<sigma>"
     by (simp add: subst_compose_def term_subst_eq_conv [symmetric])
 qed
 
 lemma subst_compose_apply_eq_apply_lhs: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes
     "range_vars \<sigma> \<inter> subst_domain \<delta> = {}"
     "x \<notin> subst_domain \<delta>"
   shows "(\<sigma> \<circ>\<^sub>s \<delta>) x = \<sigma> x"
 proof (cases "\<sigma> x")
   case (Var y)
   show ?thesis
   proof (cases "x = y")
     case True
     with Var have \<open>\<sigma> x = Var x\<close>
       by simp
     moreover from \<open>x \<notin> subst_domain \<delta>\<close> have "\<delta> 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 \<in> range_vars \<sigma>"
       unfolding range_vars_def UN_iff
     proof (rule bexI)
       show "y \<in> vars_term (Var y)"
         by simp
     next
       from Var False show "Var y \<in> subst_range \<sigma>"
         by (simp_all add: subst_domain_def)
     qed
     hence "y \<notin> subst_domain \<delta>"
       using \<open>range_vars \<sigma> \<inter> subst_domain \<delta> = {}\<close>
       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 \<in> subst_range \<sigma> \<or> (\<forall>y\<in>set ys. y \<in> subst_range \<sigma>)"
     using subst_domain_def by fastforce
   hence "\<forall>x \<in> vars_term (Fun f ys). x \<in> range_vars \<sigma>"
     by (metis UN_I range_vars_def term.distinct(1) term.sel(4) term.set_cases(2))
   hence "Fun f ys \<cdot> \<delta> = Fun f ys \<cdot> Var"
     unfolding term_subst_eq_conv
     using \<open>range_vars \<sigma> \<inter> subst_domain \<delta> = {}\<close>
     by (simp add: disjoint_iff subst_domain_def)
   hence "Fun f ys \<cdot> \<delta> = Fun f ys"
     by simp
   with Fun show ?thesis
     by (simp add: subst_compose_def)
 qed
 
 lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "range_vars \<sigma> \<inter> subst_domain \<delta> = {}" and "vars_term t \<inter> subst_domain \<delta> = {}"
   shows "t \<cdot> \<sigma> \<cdot> \<delta> = t \<cdot> \<sigma>"
 proof -
   from assms have "\<And>x. x \<in> vars_term t \<Longrightarrow> (\<sigma> \<circ>\<^sub>s \<delta>) x = \<sigma> x"
     using subst_compose_apply_eq_apply_lhs by fastforce
   hence "t \<cdot> \<sigma> \<circ>\<^sub>s \<delta> = t \<cdot> \<sigma>"
     using term_subst_eq_conv[of t "\<sigma> \<circ>\<^sub>s \<delta>" \<sigma>] by metis
   thus ?thesis
     by simp
 qed
 
 fun num_funs :: "('f, 'v) term \<Rightarrow> 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 \<cdot> \<sigma>) \<ge> 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 \<circ> (\<lambda>t. t \<cdot> \<sigma>)) ts) = sum_list (map num_funs ts)"
   shows "\<forall>i < length ts. num_funs (ts ! i \<cdot> \<sigma>) = num_funs (ts ! i)"
   using assms
 proof (induct ts)
   case (Cons t ts)
   then have "num_funs (t \<cdot> \<sigma>) + sum_list (map (num_funs \<circ> (\<lambda>t. t \<cdot> \<sigma>)) ts)
     = num_funs t + sum_list (map num_funs ts)" by (simp add: o_def)
   moreover have "num_funs (t \<cdot> \<sigma>) \<ge> num_funs t" by (metis num_funs_subst)
   moreover have "sum_list (map (num_funs \<circ> (\<lambda>t. t \<cdot> \<sigma>)) ts) \<ge> sum_list (map num_funs ts)"
     using num_funs_subst [of _ \<sigma>] 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 \<in> vars_term t" and "is_Fun t"
   shows "num_funs (\<sigma> x) < num_funs (t \<cdot> \<sigma>)"
   using assms
 proof (induct t)
   case (Fun f ts)
   then obtain u where u: "u \<in> set ts" "x \<in> vars_term u" by auto
   then have "num_funs (u \<cdot> \<sigma>) \<le> sum_list (map (num_funs \<circ> (\<lambda>t. t \<cdot> \<sigma>)) ts)"
     by (intro member_le_sum_list) simp
   moreover have "num_funs (\<sigma> x) \<le> num_funs (u \<cdot> \<sigma>)"
     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 (\<sigma> \<circ>\<^sub>s \<tau>) \<subseteq> subst_domain \<sigma> \<union> subst_domain \<tau>"
   by (auto simp: subst_domain_def subst_compose_def)
 
 lemma vars_term_disjoint_imp_unifier:
   fixes \<sigma> :: "('f, 'v, 'w) gsubst"
   assumes "vars_term s \<inter> vars_term t = {}"
     and "s \<cdot> \<sigma> = t \<cdot> \<tau>"
   shows "\<exists>\<mu> :: ('f, 'v, 'w) gsubst. s \<cdot> \<mu> = t \<cdot> \<mu>"
 proof -
   let ?\<mu> = "\<lambda>x. if x \<in> vars_term s then \<sigma> x else \<tau> x"
   have "s \<cdot> \<sigma> = s \<cdot> ?\<mu>"
     unfolding term_subst_eq_conv
     by (induct s) (simp_all)
   moreover have "t \<cdot> \<tau> = t \<cdot> ?\<mu>"
     using assms(1)
     unfolding term_subst_eq_conv
     by (induct s arbitrary: t) (auto)
   ultimately have "s \<cdot> ?\<mu> = t \<cdot> ?\<mu>" using assms(2) by simp
   then show ?thesis by blast
 qed
 
 lemma vars_term_subset_subst_eq:
   assumes "vars_term t \<subseteq> vars_term s"
     and "s \<cdot> \<sigma> = s \<cdot> \<tau>"
   shows "t \<cdot> \<sigma> = t \<cdot> \<tau>"
   using assms by (induct t) (induct s, auto)
 
 
 subsection \<open>Rename the Domain of a Substitution\<close>
 
 definition rename_subst_domain where \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain \<rho> \<sigma> x =
     (if Var x \<in> \<rho> ` subst_domain \<sigma> then
       \<sigma> (the_inv \<rho> (Var x))
     else
       Var x)"
 
 lemma rename_subst_domain_Var_rhs: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain \<rho> Var = Var"
   by (rule ext) (simp add: rename_subst_domain_def)
 
 lemma renaming_cancels_rename_subst_domain: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>" and vars_t: "vars_term t \<subseteq> subst_domain \<sigma>"
   shows "t \<cdot> \<rho> \<cdot> rename_subst_domain \<rho> \<sigma> = t \<cdot> \<sigma>"
   unfolding subst_subst
 proof (intro term_subst_eq ballI)
   fix x assume "x \<in> vars_term t"
   with vars_t have x_in: "x \<in> subst_domain \<sigma>"
     by blast
 
   obtain x' where \<rho>_x: "\<rho> x = Var x'"
     using is_var_\<rho> by (meson is_Var_def)
   with x_in have x'_in: "Var x' \<in> \<rho> ` subst_domain \<sigma>"
     by (metis image_eqI)
 
   have "(\<rho> \<circ>\<^sub>s rename_subst_domain \<rho> \<sigma>) x = \<rho> x \<cdot> rename_subst_domain \<rho> \<sigma>"
     by (simp add: subst_compose_def)
   also have "\<dots> = rename_subst_domain \<rho> \<sigma> x'"
     using \<rho>_x by simp
   also have "\<dots> = \<sigma> (the_inv \<rho> (Var x'))"
     by (simp add: rename_subst_domain_def if_P[OF x'_in])
   also have "\<dots> = \<sigma> (the_inv \<rho> (\<rho> x))"
     by (simp add: \<rho>_x)
   also have "\<dots> = \<sigma> x"
     using \<open>inj \<rho>\<close> by (simp add: the_inv_f_f)
   finally show "(\<rho> \<circ>\<^sub>s rename_subst_domain \<rho> \<sigma>) x = \<sigma> x"
     by simp
 qed
 
+
+subsection \<open>Rename the Domain and Range of a Substitution\<close>
+
+definition rename_subst_domain_range where \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
+  "rename_subst_domain_range \<rho> \<sigma> x =
+    (if Var x \<in> \<rho> ` subst_domain \<sigma> then
+      ((Var o the_inv \<rho>) \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<rho>) (Var x)
+    else
+      Var x)"
+
+lemma subst_compose_renaming_rename_subst_domain_range: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
+  fixes \<sigma> \<rho> :: "('f, 'v) subst"
+  assumes is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
+  shows "\<rho> \<circ>\<^sub>s rename_subst_domain_range \<rho> \<sigma> = \<sigma> \<circ>\<^sub>s \<rho>"
+proof (rule ext)
+  fix x
+  from is_var_\<rho> obtain x' where "\<rho> x = Var x'"
+    by (meson is_Var_def is_renaming_def)
+  with \<open>inj \<rho>\<close> have inv_\<rho>_x': "the_inv \<rho> (Var x') = x"
+    by (metis the_inv_f_f)
+
+  show "(\<rho> \<circ>\<^sub>s rename_subst_domain_range \<rho> \<sigma>) x = (\<sigma> \<circ>\<^sub>s \<rho>) x"
+  proof (cases "x \<in> subst_domain \<sigma>")
+    case True
+    hence "Var x' \<in> \<rho> ` subst_domain \<sigma>"
+      using \<open>\<rho> x = Var x'\<close> by (metis imageI)
+    thus ?thesis
+      by (simp add: \<open>\<rho> x = Var x'\<close> rename_subst_domain_range_def subst_compose_def inv_\<rho>_x')
+  next
+    case False
+    hence "Var x' \<notin> \<rho> ` subst_domain \<sigma>"
+    proof (rule contrapos_nn)
+      assume "Var x' \<in> \<rho> ` subst_domain \<sigma>"
+      hence "\<rho> x \<in> \<rho> ` subst_domain \<sigma>"
+        unfolding \<open>\<rho> x = Var x'\<close> .
+      thus "x \<in> subst_domain \<sigma>"
+        unfolding inj_image_mem_iff[OF \<open>inj \<rho>\<close>] .
+    qed
+    with False \<open>\<rho> x = Var x'\<close> 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: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
+  \<comment> \<open>This might be easier to find with @{command find_theorems}.\<close>
+  fixes t :: "('f, 'v) term" and \<sigma> \<rho> :: "('f, 'v) subst"
+  assumes is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
+  shows "t \<cdot> \<rho> \<cdot> rename_subst_domain_range \<rho> \<sigma> = t \<cdot> \<sigma> \<cdot> \<rho>"
+  unfolding subst_subst
+  unfolding subst_compose_renaming_rename_subst_domain_range[OF assms]
+  by (rule refl)
+
 end
diff --git a/thys/First_Order_Terms/Unifiers.thy b/thys/First_Order_Terms/Unifiers.thy
--- a/thys/First_Order_Terms/Unifiers.thy
+++ b/thys/First_Order_Terms/Unifiers.thy
@@ -1,217 +1,277 @@
 (*
 Author:  Christian Sternagel <c.sternagel@gmail.com>
 Author:  René Thiemann <rene.thiemann@uibk.ac.at>
 License: LGPL
 *)
 section \<open>Unification\<close>
 
 subsection \<open>Unifiers\<close>
 
 text \<open>Definition and properties of (most general) unifiers\<close>
 
 theory Unifiers
   imports Term
 begin
 
 (*TODO: move*)
 lemma map_eq_set_zipD [dest]:
   assumes "map f xs = map f ys"
     and "(x, y) \<in> set (zip xs ys)"
   shows "f x = f y"
 using assms
 proof (induct xs arbitrary: ys)
   case (Cons x xs)
   then show ?case by (cases ys) auto
 qed simp
 
 type_synonym ('f, 'v) equation = "('f, 'v) term \<times> ('f, 'v) term"
 type_synonym ('f, 'v) equations = "('f, 'v) equation set"
 
 text \<open>The set of unifiers for a given set of equations.\<close>
 definition unifiers :: "('f, 'v) equations \<Rightarrow> ('f, 'v) subst set"
   where
     "unifiers E = {\<sigma>. \<forall>p\<in>E. fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>}"
 
 text \<open>Check whether a set of equations is unifiable.\<close>
 definition "unifiable E \<longleftrightarrow> (\<exists>\<sigma>. \<sigma> \<in> unifiers E)"
 
 lemma in_unifiersE [elim]:
   "\<lbrakk>\<sigma> \<in> unifiers E; (\<And>e. e \<in> E \<Longrightarrow> fst e \<cdot> \<sigma> = snd e \<cdot> \<sigma>) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (force simp: unifiers_def)
 
 text \<open>Applying a substitution to a set of equations.\<close>
 definition subst_set :: "('f, 'v) subst \<Rightarrow> ('f, 'v) equations \<Rightarrow> ('f, 'v) equations"
   where
     "subst_set \<sigma> E = (\<lambda>e. (fst e \<cdot> \<sigma>, snd e \<cdot> \<sigma>)) ` E"
 
 text \<open>Check whether a substitution is a most-general unifier (mgu) of a set of equations.\<close>
 definition is_mgu :: "('f, 'v) subst \<Rightarrow> ('f, 'v) equations \<Rightarrow> bool"
   where
     "is_mgu \<sigma> E \<longleftrightarrow> \<sigma> \<in> unifiers E \<and> (\<forall>\<tau> \<in> unifiers E. (\<exists>\<gamma>. \<tau> = \<sigma> \<circ>\<^sub>s \<gamma>))"
 
 text \<open>The following property characterizes idempotent mgus, that is,
   mgus \<^term>\<open>\<sigma>\<close> for which \<^prop>\<open>\<sigma> \<circ>\<^sub>s \<sigma> = \<sigma>\<close> holds.\<close>
 definition is_imgu :: "('f, 'v) subst \<Rightarrow> ('f, 'v) equations \<Rightarrow> bool"
   where
     "is_imgu \<sigma> E \<longleftrightarrow> \<sigma> \<in> unifiers E \<and> (\<forall>\<tau> \<in> unifiers E. \<tau> = \<sigma> \<circ>\<^sub>s \<tau>)"
 
 
 subsubsection \<open>Properties of sets of unifiers\<close>
 
 lemma unifiers_Un [simp]:
   "unifiers (s \<union> t) = unifiers s \<inter> unifiers t"
   by (auto simp: unifiers_def)
 
 lemma unifiers_empty [simp]:
   "unifiers {} = UNIV"
   by (auto simp: unifiers_def)
 
 lemma unifiers_insert: (* "simp not added for readability (and termination)" *)
   "unifiers (insert p t) = {\<sigma>. fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>} \<inter> unifiers t"
   by (auto simp: unifiers_def)
 
 lemma unifiers_insert_ident [simp]:
   "unifiers (insert (t, t) E) = unifiers E" 
   by (auto simp: unifiers_insert)
 
 lemma unifiers_insert_swap:
   "unifiers (insert (s, t) E) = unifiers (insert (t, s) E)"
   by (auto simp: unifiers_insert)
 
 lemma unifiers_insert_Var_swap [simp]:
   "unifiers (insert (t, Var x) E) = unifiers (insert (Var x, t) E)"
   by (rule unifiers_insert_swap)
 
 lemma unifiers_subst_set [simp]:
   "\<tau> \<in> unifiers (subst_set \<sigma> E) \<longleftrightarrow> \<sigma> \<circ>\<^sub>s \<tau> \<in> unifiers E"
   by (auto simp: unifiers_def subst_set_def)
 
 lemma unifiers_insert_VarD:
   shows "\<sigma> \<in> unifiers (insert (Var x, t) E) \<Longrightarrow> subst x t \<circ>\<^sub>s \<sigma> = \<sigma>"
     and "\<sigma> \<in> unifiers (insert (t, Var x) E) \<Longrightarrow> subst x t \<circ>\<^sub>s \<sigma> = \<sigma>"
   by (auto simp: unifiers_def)
 
 lemma unifiers_insert_Var_left:
   "\<sigma> \<in> unifiers (insert (Var x, t) E) \<Longrightarrow> \<sigma> \<in> unifiers (subst_set (subst x t) E)"
   by (auto simp: unifiers_def subst_set_def)
 
 lemma unifiers_set_zip [simp]:
   assumes "length ss = length ts"
   shows "unifiers (set (zip ss ts)) = {\<sigma>. map (\<lambda>t. t \<cdot> \<sigma>) ss = map (\<lambda>t. t \<cdot> \<sigma>) ts}"
   using assms by (induct ss ts rule: list_induct2) (auto simp: unifiers_def)
 
 lemma unifiers_Fun [simp]:
   "\<sigma> \<in> unifiers {(Fun f ss, Fun g ts)} \<longleftrightarrow>
     length ss = length ts \<and> f = g \<and> \<sigma> \<in> unifiers (set (zip ss ts))"
   by (auto simp: unifiers_def dest: map_eq_imp_length_eq)
     (induct ss ts rule: list_induct2, simp_all)
 
 lemma unifiers_occur_left_is_Fun:
   fixes t :: "('f, 'v) term"
   assumes "x \<in> vars_term t" and "is_Fun t"
   shows "unifiers (insert (Var x, t) E) = {}"
 proof (rule ccontr)
   assume "\<not> ?thesis"
   then obtain \<sigma> :: "('f, 'v) subst" where "\<sigma> x = t \<cdot> \<sigma>" by (auto simp: unifiers_def)
   with is_Fun_num_funs_less [OF assms, of \<sigma>] show False by auto
 qed
 
 lemma unifiers_occur_left_not_Var:
   "x \<in> vars_term t \<Longrightarrow> t \<noteq> Var x \<Longrightarrow> unifiers (insert (Var x, t) E) = {}"
   using unifiers_occur_left_is_Fun [of x t] by (cases t) simp_all
 
 lemma unifiers_occur_left_Fun:
   "x \<in> (\<Union>t\<in>set ts. vars_term t) \<Longrightarrow> unifiers (insert (Var x, Fun f ts) E) = {}"
   using unifiers_occur_left_is_Fun [of x "Fun f ts"] by simp
 
 lemmas unifiers_occur_left_simps [simp] =
   unifiers_occur_left_is_Fun
   unifiers_occur_left_not_Var
   unifiers_occur_left_Fun
 
 
 subsubsection \<open>Properties of unifiability\<close>
 
 lemma in_vars_is_Fun_not_unifiable:
   assumes "x \<in> vars_term t" and "is_Fun t"
   shows "\<not> unifiable {(Var x, t)}"
 proof
   assume "unifiable {(Var x, t)}"
   then obtain \<sigma> where "\<sigma> \<in> unifiers {(Var x, t)}"
     by (auto simp: unifiable_def)
   then have "\<sigma> x = t \<cdot> \<sigma>" by (auto)
   moreover have "num_funs (\<sigma> x) < num_funs (t \<cdot> \<sigma>)"
     using is_Fun_num_funs_less [OF assms] by auto
   ultimately show False by auto
 qed
 
 lemma unifiable_insert_swap:
   "unifiable (insert (s, t) E) = unifiable (insert (t, s) E)"
   by (auto simp: unifiable_def unifiers_insert_swap)
 
 lemma subst_set_reflects_unifiable:
   fixes \<sigma> :: "('f, 'v) subst"
   assumes "unifiable (subst_set \<sigma> E)"
   shows "unifiable E"
 proof -
   { fix \<tau> :: "('f, 'v) subst" assume "\<forall>p\<in>E. fst p \<cdot> \<sigma> \<cdot> \<tau> = snd p \<cdot> \<sigma> \<cdot> \<tau>"
     then have "\<exists>\<sigma> :: ('f, 'v) subst. \<forall>p\<in>E. fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>"
       by (intro exI [of _ "\<sigma> \<circ>\<^sub>s \<tau>"]) auto }
   then show ?thesis using assms by (auto simp: unifiable_def unifiers_def subst_set_def)
 qed
 
 
 subsubsection \<open>Properties of \<^term>\<open>is_mgu\<close>\<close>
 
 lemma is_mgu_empty [simp]:
   "is_mgu Var {}"
   by (auto simp: is_mgu_def)
 
 lemma is_mgu_insert_trivial [simp]:
   "is_mgu \<sigma> (insert (t, t) E) = is_mgu \<sigma> E"
   by (auto simp: is_mgu_def)
 
 lemma is_mgu_insert_decomp [simp]:
   assumes "length ss = length ts"
   shows "is_mgu \<sigma> (insert (Fun f ss, Fun f ts) E) \<longleftrightarrow>
     is_mgu \<sigma> (E \<union> set (zip ss ts))"
   using assms by (auto simp: is_mgu_def unifiers_insert)
 
 lemma is_mgu_insert_swap:
   "is_mgu \<sigma> (insert (s, t) E) = is_mgu \<sigma> (insert (t, s) E)"
   by (auto simp: is_mgu_def unifiers_def)
 
 lemma is_mgu_insert_Var_swap [simp]:
   "is_mgu \<sigma> (insert (t, Var x) E) = is_mgu \<sigma> (insert (Var x, t) E)"
   by (rule is_mgu_insert_swap)
 
 lemma is_mgu_subst_set_subst:
   assumes "x \<notin> vars_term t"
     and "is_mgu \<sigma> (subst_set (subst x t) E)" (is "is_mgu \<sigma> ?E")
   shows "is_mgu (subst x t \<circ>\<^sub>s \<sigma>) (insert (Var x, t) E)" (is "is_mgu ?\<sigma> ?E'")
 proof -
   from \<open>is_mgu \<sigma> ?E\<close>
     have "?\<sigma> \<in> unifiers E"
     and *: "\<forall>\<tau>. (subst x t \<circ>\<^sub>s \<tau>) \<in> unifiers E \<longrightarrow> (\<exists>\<mu>. \<tau> = \<sigma> \<circ>\<^sub>s \<mu>)"
     by (auto simp: is_mgu_def)
   then have "?\<sigma> \<in> unifiers ?E'" using assms by (simp add: unifiers_insert subst_compose)
   moreover have "\<forall>\<tau>. \<tau> \<in> unifiers ?E' \<longrightarrow> (\<exists>\<mu>. \<tau> = ?\<sigma> \<circ>\<^sub>s \<mu>)"
   proof (intro allI impI)
     fix \<tau>
     assume **: "\<tau> \<in> unifiers ?E'"
     then have [simp]: "subst x t \<circ>\<^sub>s \<tau> = \<tau>" by (blast dest: unifiers_insert_VarD)
     from unifiers_insert_Var_left [OF **]
       have "subst x t \<circ>\<^sub>s \<tau> \<in> unifiers E" by (simp)
     with * obtain \<mu> where "\<tau> = \<sigma> \<circ>\<^sub>s \<mu>" by blast
     then have "subst x t \<circ>\<^sub>s \<tau> = subst x t \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<mu>" by (auto simp: ac_simps)
     then show "\<exists>\<mu>. \<tau> = subst x t \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<mu>" by auto
   qed
   ultimately show "is_mgu ?\<sigma> ?E'" by (simp add: is_mgu_def)
 qed
 
 lemma is_imgu_imp_is_mgu:
   assumes "is_imgu \<sigma> E"
   shows "is_mgu \<sigma> E"
   using assms by (auto simp: is_imgu_def is_mgu_def)
 
+
+subsection \<open>Properties of \<^term>\<open>is_imgu\<close>\<close>
+
+lemma rename_subst_domain_range_preserves_is_imgu: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
+  fixes E :: "('f, 'v) equations" and \<mu> \<rho> :: "('f, 'v) subst"
+  assumes imgu_\<mu>: "is_imgu \<mu> E" and is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
+  shows "is_imgu (rename_subst_domain_range \<rho> \<mu>) (subst_set \<rho> E)"
+proof (unfold is_imgu_def, intro conjI ballI)
+  from imgu_\<mu> have unif_\<mu>: "\<mu> \<in> unifiers E"
+    by (simp add: is_imgu_def)
+
+  show "rename_subst_domain_range \<rho> \<mu> \<in> unifiers (subst_set \<rho> E)"
+    unfolding unifiers_subst_set unifiers_def mem_Collect_eq
+  proof (rule ballI)
+    fix e\<^sub>\<rho> assume "e\<^sub>\<rho> \<in> subst_set \<rho> E"
+    then obtain e where "e \<in> E" and "e\<^sub>\<rho> = (fst e \<cdot> \<rho>, snd e \<cdot> \<rho>)"
+      by (auto simp: subst_set_def)
+    then show "fst e\<^sub>\<rho> \<cdot> rename_subst_domain_range \<rho> \<mu> = snd e\<^sub>\<rho> \<cdot> rename_subst_domain_range \<rho> \<mu>"
+      using unif_\<mu> subst_apply_term_renaming_rename_subst_domain_range[OF is_var_\<rho> \<open>inj \<rho>\<close>, of _ \<mu>]
+      by (simp add: unifiers_def)
+  qed
+next
+  fix \<upsilon> :: "('f, 'v) subst"
+  assume "\<upsilon> \<in> unifiers (subst_set \<rho> E)"
+  hence "(\<rho> \<circ>\<^sub>s \<upsilon>) \<in> unifiers E"
+    by (simp add: subst_set_def unifiers_def)
+  with imgu_\<mu> have \<mu>_\<rho>_\<upsilon>: "\<mu> \<circ>\<^sub>s \<rho> \<circ>\<^sub>s \<upsilon> = \<rho> \<circ>\<^sub>s \<upsilon>"
+    by (simp add: is_imgu_def subst_compose_assoc)
+
+  show "\<upsilon> = rename_subst_domain_range \<rho> \<mu> \<circ>\<^sub>s \<upsilon>"
+  proof (rule ext)
+    fix x
+    show "\<upsilon> x = (rename_subst_domain_range \<rho> \<mu> \<circ>\<^sub>s \<upsilon>) x"
+    proof (cases "Var x \<in> \<rho> ` subst_domain \<mu>")
+      case True
+      hence "(rename_subst_domain_range \<rho> \<mu> \<circ>\<^sub>s \<upsilon>) x = (\<mu> \<circ>\<^sub>s \<rho> \<circ>\<^sub>s \<upsilon>) (the_inv \<rho> (Var x))"
+        by (simp add: rename_subst_domain_range_def subst_compose_def)
+      also have "\<dots> = (\<rho> \<circ>\<^sub>s \<upsilon>) (the_inv \<rho> (Var x))"
+        by (simp add: \<mu>_\<rho>_\<upsilon>)
+      also have "\<dots> = (\<rho> (the_inv \<rho> (Var x))) \<cdot> \<upsilon>"
+        by (simp add: subst_compose)
+      also have "\<dots> = Var x \<cdot> \<upsilon>"
+        using True f_the_inv_into_f[OF \<open>inj \<rho>\<close>, of "Var x"] by force
+      finally show ?thesis
+        by simp
+    next
+      case False
+      thus ?thesis
+        by (simp add: rename_subst_domain_range_def subst_compose)
+    qed
+  qed
+qed
+
+corollary rename_subst_domain_range_preserves_is_imgu_singleton: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
+  fixes t u :: "('f, 'v) term" and \<mu> \<rho> :: "('f, 'v) subst"
+  assumes imgu_\<mu>: "is_imgu \<mu> {(t, u)}" and is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)" and "inj \<rho>"
+  shows "is_imgu (rename_subst_domain_range \<rho> \<mu>) {(t \<cdot> \<rho>, u \<cdot> \<rho>)}"
+  by (rule rename_subst_domain_range_preserves_is_imgu[OF imgu_\<mu> is_var_\<rho> \<open>inj \<rho>\<close>,
+        unfolded subst_set_def, simplified])
+
 end