diff --git a/thys/First_Order_Terms/Lists_are_Infinite.thy b/thys/First_Order_Terms/Lists_are_Infinite.thy
new file mode 100644
--- /dev/null
+++ b/thys/First_Order_Terms/Lists_are_Infinite.thy
@@ -0,0 +1,15 @@
+(*
+Author:  Christian Sternagel <c.sternagel@gmail.com>
+Author:  René Thiemann <rene.thiemann@uibk.ac.at>
+License: LGPL
+*)
+subsection \<open>Make lists instances of the infinite-class.\<close>
+
+theory Lists_are_Infinite
+  imports Fresh_Identifiers.Fresh
+begin
+
+instance list :: (type) infinite
+  by (intro_classes, rule infinite_UNIV_listI)
+
+end
\ No newline at end of file
diff --git a/thys/First_Order_Terms/ROOT b/thys/First_Order_Terms/ROOT
--- a/thys/First_Order_Terms/ROOT
+++ b/thys/First_Order_Terms/ROOT
@@ -1,21 +1,24 @@
 chapter AFP
 
 session First_Order_Terms = "Abstract-Rewriting" +
   description "First-Order Terms"
   options [timeout = 300]
   sessions
     "HOL-Library"
+    Fresh_Identifiers
   theories
     Transitive_Closure_More
   theories
+    Renaming2_String
+  theories
     Seq_More
     Fun_More
     Option_Monad
   theories
     Matching
-    Unification
+    Unification_String
     Subsumption
     Subterm_and_Context
   document_files
     "root.tex"
     "root.bib"
diff --git a/thys/First_Order_Terms/Renaming2.thy b/thys/First_Order_Terms/Renaming2.thy
new file mode 100644
--- /dev/null
+++ b/thys/First_Order_Terms/Renaming2.thy
@@ -0,0 +1,45 @@
+(*
+Author:  Christian Sternagel <c.sternagel@gmail.com>
+Author:  René Thiemann <rene.thiemann@uibk.ac.at>
+License: LGPL
+*)
+
+subsection \<open>Rename names in two ways.\<close>
+
+theory Renaming2
+  imports 
+    Fresh_Identifiers.Fresh
+begin
+
+typedef ('v :: infinite) renaming2 = "{ (v1 :: 'v \<Rightarrow> 'v, v2 :: 'v \<Rightarrow> 'v) | v1 v2. inj v1 \<and> inj v2 \<and> range v1 \<inter> range v2 = {} }" 
+proof -
+  let ?U = "UNIV :: 'v set" 
+  have inf: "infinite ?U" by (rule infinite_UNIV)
+  have "ordLeq3 (card_of ?U) (card_of ?U)" 
+    using card_of_refl ordIso_iff_ordLeq by blast
+  from card_of_Plus_infinite1[OF inf this, folded card_of_ordIso] 
+  obtain f where bij: "bij_betw f (?U <+> ?U) ?U" by auto
+  hence injf: "inj f" by (simp add: bij_is_inj)
+  define v1 where "v1 = f o Inl" 
+  define v2 where "v2 = f o Inr" 
+  have inj: "inj v1" "inj v2" unfolding v1_def v2_def by (intro inj_compose[OF injf], auto)+
+  have "range v1 \<inter> range v2 = {}" 
+  proof (rule ccontr)
+    assume "\<not> ?thesis" 
+    then obtain x where "v1 x = v2 x" 
+      using injD injf v1_def v2_def by fastforce
+    hence "f (Inl x) = f (Inr x)" unfolding v1_def v2_def by auto
+    with injf show False unfolding inj_on_def by blast
+  qed
+  with inj show ?thesis by blast
+qed
+
+setup_lifting type_definition_renaming2
+
+lift_definition rename_1 :: "'v :: infinite renaming2 \<Rightarrow> 'v \<Rightarrow> 'v" is fst .
+lift_definition rename_2 :: "'v :: infinite renaming2 \<Rightarrow> 'v \<Rightarrow> 'v" is snd .
+
+lemma rename_12: "inj (rename_1 r)" "inj (rename_2 r)" "range (rename_1 r) \<inter> range (rename_2 r) = {}" 
+  by (transfer, auto)+
+
+end
diff --git a/thys/First_Order_Terms/Renaming2_String.thy b/thys/First_Order_Terms/Renaming2_String.thy
new file mode 100644
--- /dev/null
+++ b/thys/First_Order_Terms/Renaming2_String.thy
@@ -0,0 +1,14 @@
+subsection \<open>Renaming strings apart\<close>
+
+theory Renaming2_String
+  imports 
+    Renaming2
+    Lists_are_Infinite
+begin
+
+lift_definition string_rename :: "string renaming2" is "(Cons (CHR ''x''), Cons (CHR ''y''))" 
+  by auto
+
+end
+
+  
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,718 +1,749 @@
 (*
 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
     "HOL-Library.Multiset"
 begin
 
 datatype (funs_term : 'f, vars_term : 'v) "term" =
   is_Var: Var (the_Var: 'v) |
   Fun 'f (args : "('f, 'v) term list")
 where
   "args (Var _) = []"
 
 abbreviation "is_Fun t \<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
 
 lemma inj_on_Var[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "inj_on Var A"
   by (rule inj_onI) simp
 
 lemma member_image_the_Var_image_subst: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes is_var_\<sigma>: "\<forall>x. is_Var (\<sigma> x)"
   shows "x \<in> the_Var ` \<sigma> ` V \<longleftrightarrow> Var x \<in> \<sigma> ` V"
   using is_var_\<sigma> image_iff
   by (metis (no_types, opaque_lifting) term.collapse(1) term.sel(1))
 
 lemma image_the_Var_image_subst_renaming_eq: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes is_var_\<sigma>: "\<forall>x. is_Var (\<rho> x)"
   shows "the_Var ` \<rho> ` V = (\<Union>x \<in> V. vars_term (\<rho> x))"
 proof (rule Set.equalityI; rule Set.subsetI)
   from is_var_\<sigma> show "\<And>x. x \<in> the_Var ` \<rho> ` V \<Longrightarrow> x \<in> (\<Union>x\<in>V. vars_term (\<rho> x))"
     using term.set_sel(3) by force
 next
   from is_var_\<sigma> show "\<And>x. x \<in> (\<Union>x\<in>V. vars_term (\<rho> x)) \<Longrightarrow> x \<in> the_Var ` \<rho> ` V"
     by (smt (verit, best) Term.term.simps(17) UN_iff image_eqI singletonD term.collapse(1))
 qed
 
 text \<open>The variables of a term as multiset.\<close>
 fun vars_term_ms :: "('f, 'v) term \<Rightarrow> 'v multiset"
   where
     "vars_term_ms (Var x) = {#x#}" |
     "vars_term_ms (Fun f ts) = \<Sum>\<^sub># (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 \<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") = \<open>K Reorient_Proc.proc\<close>
 simproc_setup reorient_Fun ("Fun f ss = t") = \<open>K Reorient_Proc.proc\<close>
 
 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>"
 
 lemma vars_term_ms_subst [simp]:
   "vars_term_ms (t \<cdot> \<sigma>) =
     (\<Sum>x\<in>#vars_term_ms t. vars_term_ms (\<sigma> x))" (is "_ = ?V t")
 proof (induct t)
   case (Fun f ts)
   have IH: "map (\<lambda> t. vars_term_ms (t \<cdot> \<sigma>)) ts = map (\<lambda> 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 \<subseteq># vars_term_ms t"
   shows "vars_term_ms (s \<cdot> \<sigma>) \<subseteq># vars_term_ms (t \<cdot> \<sigma>)"
 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 \<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 mem_range_varsI: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "\<sigma> x = Var y" and "x \<noteq> y"
   shows "y \<in> range_vars \<sigma>"
   unfolding range_vars_def UN_iff
 proof (rule bexI[of _ "Var y"])
   show "y \<in> vars_term (Var y)"
     by simp
 next
   from assms show "Var y \<in> subst_range \<sigma>"
     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]: \<^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>\<open>\<open>Lemma 4.5.7\<close> in "AllThat"\<close>.)\<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>Restrict the Domain of a Substitution\<close>
 
 definition restrict_subst_domain where \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "restrict_subst_domain V \<sigma> x \<equiv> (if x \<in> V then \<sigma> x else Var x)"
 
 lemma restrict_subst_domain_empty[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "restrict_subst_domain {} \<sigma> = Var"
   unfolding restrict_subst_domain_def by auto
 
 lemma restrict_subst_domain_Var[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "restrict_subst_domain V Var = Var"
   unfolding restrict_subst_domain_def by auto
 
 lemma subst_domain_restrict_subst_domain[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "subst_domain (restrict_subst_domain V \<sigma>) = V \<inter> subst_domain \<sigma>"
   unfolding restrict_subst_domain_def subst_domain_def by auto
 
 lemma subst_apply_term_restrict_subst_domain: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "vars_term t \<subseteq> V \<Longrightarrow> t \<cdot> restrict_subst_domain V \<sigma> = t \<cdot> \<sigma>"
   by (rule term_subst_eq) (simp add: restrict_subst_domain_def subsetD)
 
 
 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_lhs[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain Var \<sigma> = \<sigma>"
   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]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain \<rho> Var = Var"
   by (rule ext) (simp add: rename_subst_domain_def)
 
 lemma subst_domain_rename_subst_domain_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes is_var_\<rho>: "\<forall>x. is_Var (\<rho> x)"
   shows "subst_domain (rename_subst_domain \<rho> \<sigma>) \<subseteq> the_Var ` \<rho> ` subst_domain \<sigma>"
   by (auto simp add: subst_domain_def rename_subst_domain_def
       member_image_the_Var_image_subst[OF is_var_\<rho>])
 
 lemma subst_range_rename_subst_domain_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "inj \<rho>"
   shows "subst_range (rename_subst_domain \<rho> \<sigma>) \<subseteq> subst_range \<sigma>"
 proof (intro Set.equalityI Set.subsetI)
   fix t assume "t \<in> subst_range (rename_subst_domain \<rho> \<sigma>)"
   then obtain x where
     t_def: "t = rename_subst_domain \<rho> \<sigma> x" and
     "rename_subst_domain \<rho> \<sigma> x \<noteq> Var x"
     by (auto simp: image_iff subst_domain_def)
 
   show "t \<in> subst_range \<sigma>"
   proof (cases \<open>Var x \<in> \<rho> ` subst_domain \<sigma>\<close>)
     case True
     then obtain x' where "\<rho> x' = Var x" and "x' \<in> subst_domain \<sigma>"
       by auto
     then show ?thesis
       using the_inv_f_f[OF \<open>inj \<rho>\<close>, of x']
       by (simp add: t_def rename_subst_domain_def)
   next
     case False
     hence False
       using \<open>rename_subst_domain \<rho> \<sigma> x \<noteq> Var x\<close>
       by (simp add: t_def rename_subst_domain_def)
     thus ?thesis ..
   qed
 qed
 
 lemma range_vars_rename_subst_domain_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "inj \<rho>"
   shows "range_vars (rename_subst_domain \<rho> \<sigma>) \<subseteq> range_vars \<sigma>"
   unfolding range_vars_def
   using subst_range_rename_subst_domain_subset[OF \<open>inj \<rho>\<close>]
   by (metis Union_mono image_mono)
 
 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 rename_subst_domain_range_Var_lhs[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain_range Var \<sigma> = \<sigma>"
   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]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "rename_subst_domain_range \<rho> Var = Var"
   by (rule ext) (simp add: rename_subst_domain_range_def)
 
 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)
 
 
 text \<open>A term is called \<^emph>\<open>ground\<close> if it does not contain any variables.\<close>
 fun ground :: "('f, 'v) term \<Rightarrow> bool"
   where
     "ground (Var x) \<longleftrightarrow> False" |
     "ground (Fun f ts) \<longleftrightarrow> (\<forall>t \<in> set ts. ground t)"
 
 lemma ground_vars_term_empty:
   "ground t \<longleftrightarrow> vars_term t = {}"
   by (induct t) simp_all
 
 lemma ground_subst [simp]:
   "ground (t \<cdot> \<sigma>) \<longleftrightarrow> (\<forall>x \<in> vars_term t. ground (\<sigma> x))"
   by (induct t) simp_all
 
 lemma ground_subst_apply:
   assumes "ground t"
   shows "t \<cdot> \<sigma> = t"
 proof -
   have "t = t \<cdot> Var" by simp
   also have "\<dots> = t \<cdot> \<sigma>"
     by (rule term_subst_eq, insert assms[unfolded ground_vars_term_empty], auto)
   finally show ?thesis by simp
 qed
 
+text \<open>Just changing the variables in a term\<close>
+
+abbreviation "map_vars_term f \<equiv> term.map_term (\<lambda>x. x) f"
+
+lemma map_vars_term_as_subst:
+  "map_vars_term f t = t \<cdot> (\<lambda> x. Var (f x))"
+  by (induct t) simp_all
+
+lemma map_vars_term_eq:
+  "map_vars_term f s = s \<cdot> (Var \<circ> 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 \<cdot> \<sigma>) = t \<cdot> (\<lambda> x. map_vars_term f (\<sigma> x))"
+  by (induct t) simp_all
+
+lemma map_vars_term_compose:
+  "map_vars_term m1 (map_vars_term m2 t) = map_vars_term (m1 o m2) t"
+  by (induct t) simp_all
+
+lemma map_vars_term_id [simp]:
+  "map_vars_term id t = t"
+  by (induct t) (auto intro: map_idI)
+
+lemma apply_subst_map_vars_term:
+  "map_vars_term m t \<cdot> \<sigma> = t \<cdot> (\<sigma> \<circ> m)"
+  by (induct t) (auto)
 
 
 end
diff --git a/thys/First_Order_Terms/Unification.thy b/thys/First_Order_Terms/Unification.thy
--- a/thys/First_Order_Terms/Unification.thy
+++ b/thys/First_Order_Terms/Unification.thy
@@ -1,704 +1,894 @@
 (*
 Author:  Christian Sternagel <c.sternagel@gmail.com>
 Author:  René Thiemann <rene.thiemann@uibk.ac.at>
 License: LGPL
 *)
 subsection \<open>A Concrete Unification Algorithm\<close>
 
 theory Unification
   imports
     Abstract_Unification
     Option_Monad
+    Renaming2
 begin
 
 definition
   "decompose s t =
     (case (s, t) of
       (Fun f ss, Fun g ts) \<Rightarrow> if f = g then zip_option ss ts else None
     | _ \<Rightarrow> None)"
 
 lemma decompose_same_Fun[simp]: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "decompose (Fun f ss) (Fun f ss) = Some (zip ss ss)"
   by (simp add: decompose_def)
 
 lemma decompose_Some [dest]:
   "decompose (Fun f ss) (Fun g ts) = Some E \<Longrightarrow>
     f = g \<and> length ss = length ts \<and> E = zip ss ts"
   by (cases "f = g") (auto simp: decompose_def)
 
 lemma decompose_None [dest]:
   "decompose (Fun f ss) (Fun g ts) = None \<Longrightarrow> f \<noteq> g \<or> length ss \<noteq> length ts"
   by (cases "f = g") (auto simp: decompose_def)
 
 text \<open>Applying a substitution to a list of equations.\<close>
 definition
   subst_list :: "('f, 'v) subst \<Rightarrow> ('f, 'v) equation list \<Rightarrow> ('f, 'v) equation list"
   where
     "subst_list \<sigma> ys = map (\<lambda>p. (fst p \<cdot> \<sigma>, snd p \<cdot> \<sigma>)) ys"
 
 lemma mset_subst_list [simp]:
   "mset (subst_list (subst x t) ys) = subst_mset (subst x t) (mset ys)"
   by (auto simp: subst_mset_def subst_list_def)
 
 lemma subst_list_append:
   "subst_list \<sigma> (xs @ ys) = subst_list \<sigma> xs @ subst_list \<sigma> ys"
 by (auto simp: subst_list_def)
 
 function (sequential)
   unify ::
     "('f, 'v) equation list \<Rightarrow> ('v \<times> ('f, 'v) term) list \<Rightarrow> ('v \<times> ('f, 'v) term) list option"
 where
   "unify [] bs = Some bs"
 | "unify ((Fun f ss, Fun g ts) # E) bs =
     (case decompose (Fun f ss) (Fun g ts) of
       None \<Rightarrow> None
     | Some us \<Rightarrow> unify (us @ E) bs)"
 | "unify ((Var x, t) # E) bs =
     (if t = Var x then unify E bs
     else if x \<in> vars_term t then None
     else unify (subst_list (subst x t) E) ((x, t) # bs))"
 | "unify ((t, Var x) # E) bs =
     (if x \<in> vars_term t then None
     else unify (subst_list (subst x t) E) ((x, t) # bs))"
   by pat_completeness auto
 termination
   by (standard, rule wf_inv_image [of "unif\<inverse>" "mset \<circ> fst", OF wf_converse_unif])
      (force intro: UNIF1.intros simp: unif_def union_commute)+
 
 lemma unify_append_prefix_same: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "(\<forall>e \<in> set es1. fst e = snd e) \<Longrightarrow> unify (es1 @ es2) bs = unify es2 bs"
 proof (induction "es1 @ es2" bs arbitrary: es1 es2 bs rule: unify.induct)
   case (1 bs)
   thus ?case by simp
 next
   case (2 f ss g ts E bs)
   show ?case
   proof (cases es1)
     case Nil
     thus ?thesis by simp
   next
     case (Cons e es1')
     hence e_def: "e = (Fun f ss, Fun g ts)" and E_def: "E = es1' @ es2"
       using "2" by simp_all
     hence "f = g" and "ss = ts"
       using "2.prems" local.Cons by auto
     hence "unify (es1 @ es2) bs = unify ((zip ts ts @ es1') @ es2) bs"
       by (simp add: Cons e_def)
     also have "\<dots> = unify es2 bs"
     proof (rule "2.hyps"(1))
       show "decompose (Fun f ss) (Fun g ts) = Some (zip ts ts)"
         by (simp add: \<open>f = g\<close> \<open>ss = ts\<close>)
     next
       show "zip ts ts @ E = (zip ts ts @ es1') @ es2"
         by (simp add: E_def)
     next
       show "\<forall>e\<in>set (zip ts ts @ es1'). fst e = snd e"
         using "2.prems" by (auto simp: Cons zip_same)
     qed
     finally show ?thesis .
   qed
 next
   case (3 x t E bs)
   show ?case
   proof (cases es1)
     case Nil
     thus ?thesis by simp
   next
     case (Cons e es1')
     hence e_def: "e = (Var x, t)" and E_def: "E = es1' @ es2"
       using 3 by simp_all
     show ?thesis
     proof (cases "t = Var x")
       case True
       show ?thesis
         using 3(1)[OF True E_def]
         using "3.hyps"(3) "3.prems" local.Cons by fastforce
     next
       case False
       thus ?thesis
         using "3.prems" e_def local.Cons by force
     qed
   qed
 next
   case (4 v va x E bs)
   then show ?case
   proof (cases es1)
     case Nil
     thus ?thesis by simp
   next
     case (Cons e es1')
     hence e_def: "e = (Fun v va, Var x)" and E_def: "E = es1' @ es2"
       using 4 by simp_all
     thus ?thesis
       using "4.prems" local.Cons by fastforce
   qed
 qed
 
 corollary unify_Cons_same: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "fst e = snd e \<Longrightarrow> unify (e # es) bs = unify es bs"
   by (rule unify_append_prefix_same[of "[_]", simplified])
 
 corollary unify_same: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "(\<forall>e \<in> set es. fst e = snd e) \<Longrightarrow> unify es bs = Some bs"
   by (rule unify_append_prefix_same[of _ "[]", simplified])
 
 definition subst_of :: "('v \<times> ('f, 'v) term) list \<Rightarrow> ('f, 'v) subst"
   where
     "subst_of ss = List.foldr (\<lambda>(x, t) \<sigma>. \<sigma> \<circ>\<^sub>s subst x t) ss Var"
 
 text \<open>Computing the mgu of two terms.\<close>
 definition mgu :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> ('f, 'v) subst option" where
   "mgu s t =
     (case unify [(s, t)] [] of
       None \<Rightarrow> None
     | Some res \<Rightarrow> Some (subst_of res))"
 
 lemma subst_of_simps [simp]:
   "subst_of [] = Var"
   "subst_of ((x, Var x) # ss) = subst_of ss"
   "subst_of (b # ss) = subst_of ss \<circ>\<^sub>s subst (fst b) (snd b)"
   by (simp_all add: subst_of_def split: prod.splits)
 
 lemma subst_of_append [simp]:
   "subst_of (ss @ ts) = subst_of ts \<circ>\<^sub>s subst_of ss"
   by (induct ss) (auto simp: ac_simps)
 
 text \<open>The concrete algorithm \<open>unify\<close> can be simulated by the inference
   rules of \<open>UNIF\<close>.\<close>
 lemma unify_Some_UNIF:
   assumes "unify E bs = Some cs"
   shows "\<exists>ds ss. cs = ds @ bs \<and> subst_of ds = compose ss \<and> UNIF ss (mset E) {#}"
 using assms
 proof (induction E bs arbitrary: cs rule: unify.induct)
   case (2 f ss g ts E bs)
   then obtain us where "decompose (Fun f ss) (Fun g ts) = Some us"
     and [simp]: "f = g" "length ss = length ts" "us = zip ss ts"
     and "unify (us @ E) bs = Some cs" by (auto split: option.splits)
   from "2.IH" [OF this(1, 5)] obtain xs ys
     where "cs = xs @ bs"
     and [simp]: "subst_of xs = compose ys"
     and *: "UNIF ys (mset (us @ E)) {#}" by auto
   then have "UNIF (Var # ys) (mset ((Fun f ss, Fun g ts) # E)) {#}"
     by (force intro: UNIF1.decomp simp: ac_simps)
   moreover have "cs = xs @ bs" by fact
   moreover have "subst_of xs = compose (Var # ys)" by simp
   ultimately show ?case by blast
 next
   case (3 x t E bs)
   show ?case
   proof (cases "t = Var x")
     assume "t = Var x"
     then show ?case
       using 3 by auto (metis UNIF.step compose_simps(2) UNIF1.trivial)
   next
     assume "t \<noteq> Var x"
     with 3 obtain xs ys
       where [simp]: "cs = (ys @ [(x, t)]) @ bs"
       and [simp]: "subst_of ys = compose xs"
       and "x \<notin> vars_term t"
       and "UNIF xs (mset (subst_list (subst x t) E)) {#}"
         by (cases "x \<in> vars_term t") force+
     then have "UNIF (subst x t # xs) (mset ((Var x, t) # E)) {#}"
       by (force intro: UNIF1.Var_left simp: ac_simps)
     moreover have "cs = (ys @ [(x, t)]) @ bs" by simp
     moreover have "subst_of (ys @ [(x, t)]) = compose (subst x t # xs)" by simp
     ultimately show ?case by blast
   qed
 next
   case (4 f ss x E bs)
   with 4 obtain xs ys
     where [simp]: "cs = (ys @ [(x, Fun f ss)]) @ bs"
     and [simp]: "subst_of ys = compose xs"
     and "x \<notin> vars_term (Fun f ss)"
     and "UNIF xs (mset (subst_list (subst x (Fun f ss)) E)) {#}"
       by (cases "x \<in> vars_term (Fun f ss)") force+
   then have "UNIF (subst x (Fun f ss) # xs) (mset ((Fun f ss, Var x) # E)) {#}"
     by (force intro: UNIF1.Var_right simp: ac_simps)
   moreover have "cs = (ys @ [(x, Fun f ss)]) @ bs" by simp
   moreover have "subst_of (ys @ [(x, Fun f ss)]) = compose (subst x (Fun f ss) # xs)" by simp
   ultimately show ?case by blast
 qed force
 
 lemma unify_sound:
   assumes "unify E [] = Some cs"
   shows "is_imgu (subst_of cs) (set E)"
 proof -
   from unify_Some_UNIF [OF assms] obtain ss
     where "subst_of cs = compose ss"
     and "UNIF ss (mset E) {#}" by auto
   with UNIF_empty_imp_is_mgu_compose [OF this(2)]
     and UNIF_idemp [OF this(2)]
     show ?thesis
       by (auto simp add: is_imgu_def is_mgu_def)
          (metis subst_compose_assoc)
 qed
 
 lemma mgu_sound:
   assumes "mgu s t = Some \<sigma>"
   shows "is_imgu \<sigma> {(s, t)}"
 proof -
   obtain ss where "unify [(s, t)] [] = Some ss"
     and "\<sigma> = subst_of ss"
     using assms by (auto simp: mgu_def split: option.splits)
   then have "is_imgu \<sigma> (set [(s, t)])" by (metis unify_sound)
   then show ?thesis by simp
 qed
 
 text \<open>If \<open>unify\<close> gives up, then the given set of equations
   cannot be reduced to the empty set by \<open>UNIF\<close>.\<close>
 lemma unify_None:
   assumes "unify E ss = None"
   shows "\<exists>E'. E' \<noteq> {#} \<and> (mset E, E') \<in> unif\<^sup>!"
 using assms
 proof (induction E ss rule: unify.induct)
   case (1 bs)
   then show ?case by simp
 next
   case (2 f ss g ts E bs)
   moreover
   { assume *: "decompose (Fun f ss) (Fun g ts) = None"
     have ?case
     proof (cases "unifiable (set E)")
       case True
       then have "(mset E, {#}) \<in> unif\<^sup>*"
         by (simp add: unifiable_imp_empty)
       from unif_rtrancl_mono [OF this, of "{#(Fun f ss, Fun g ts)#}"] obtain \<sigma>
         where "(mset E + {#(Fun f ss, Fun g ts)#}, {#(Fun f ss \<cdot> \<sigma>, Fun g ts \<cdot> \<sigma>)#}) \<in> unif\<^sup>*"
         by (auto simp: subst_mset_def)
       moreover have "{#(Fun f ss \<cdot> \<sigma>, Fun g ts \<cdot> \<sigma>)#} \<in> NF unif"
         using decompose_None [OF *]
         by (auto simp: single_is_union NF_def unif_def elim!: UNIF1.cases)
            (metis length_map)
       ultimately show ?thesis
         by auto (metis normalizability_I add_mset_not_empty)
     next
       case False
       moreover have "\<not> unifiable {(Fun f ss, Fun g ts)}"
         using * by (auto simp: unifiable_def)
       ultimately have "\<not> unifiable (set ((Fun f ss, Fun g ts) # E))" by (auto simp: unifiable_def unifiers_def)
       then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF)
     qed }
   moreover
   { fix us
     assume *: "decompose (Fun f ss) (Fun g ts) = Some us"
       and "unify (us @ E) bs = None"
     from "2.IH" [OF this] obtain E'
       where "E' \<noteq> {#}" and "(mset (us @ E), E') \<in> unif\<^sup>!" by blast
     moreover have "(mset ((Fun f ss, Fun g ts) # E), mset (us @ E)) \<in> unif"
     proof -
       have "g = f" and "length ss = length ts" and "us = zip ss ts"
         using * by auto
       then show ?thesis
         by (auto intro: UNIF1.decomp simp: unif_def ac_simps)
     qed
     ultimately have ?case by auto }
   ultimately show ?case by (auto split: option.splits)
 next
   case (3 x t E bs)
   { assume [simp]: "t = Var x"
     obtain E' where "E' \<noteq> {#}" and "(mset E, E') \<in> unif\<^sup>!" using 3 by auto
     moreover have "(mset ((Var x, t) # E), mset E) \<in> unif"
       by (auto intro: UNIF1.trivial simp: unif_def)
     ultimately have ?case by auto }
   moreover
   { assume *: "t \<noteq> Var x" "x \<notin> vars_term t"
     then obtain E' where "E' \<noteq> {#}"
       and "(mset (subst_list (subst x t) E), E') \<in> unif\<^sup>!" using 3 by auto
     moreover have "(mset ((Var x, t) # E), mset (subst_list (subst x t) E)) \<in> unif"
       using * by (auto intro: UNIF1.Var_left simp: unif_def)
     ultimately have ?case by auto }
   moreover
   { assume *: "t \<noteq> Var x" "x \<in> vars_term t"
     then have "x \<in> vars_term t" "is_Fun t" by auto
     then have "\<not> unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable)
     then have **: "\<not> unifiable {(Var x \<cdot> \<sigma>, t \<cdot> \<sigma>)}" for \<sigma> :: "('b, 'a) subst"
       using subst_set_reflects_unifiable [of \<sigma> "{(Var x, t)}"] by (auto simp: subst_set_def)
     have ?case
     proof (cases "unifiable (set E)")
       case True
       then have "(mset E, {#}) \<in> unif\<^sup>*"
         by (simp add: unifiable_imp_empty)
       from unif_rtrancl_mono [OF this, of "{#(Var x, t)#}"] obtain \<sigma>
         where "(mset E + {#(Var x, t)#}, {#(Var x \<cdot> \<sigma>, t \<cdot> \<sigma>)#}) \<in> unif\<^sup>*"
         by (auto simp: subst_mset_def)
       moreover obtain E' where "E' \<noteq> {#}"
         and "({#(Var x \<cdot> \<sigma>, t \<cdot> \<sigma>)#}, E') \<in> unif\<^sup>!"
         using not_unifiable_imp_not_empty_NF and **
           by (metis set_mset_single)
       ultimately show ?thesis by auto
     next
       case False
       moreover have "\<not> unifiable {(Var x, t)}"
         using * by (force simp: unifiable_def)
       ultimately have "\<not> unifiable (set ((Var x, t) # E))" by (auto simp: unifiable_def unifiers_def)
       then show ?thesis
         by (simp add: not_unifiable_imp_not_empty_NF)
     qed }
   ultimately show ?case by blast
 next
   case (4 f ss x E bs)
   define t where "t = Fun f ss"
   { assume *: "x \<notin> vars_term t"
     then obtain E' where "E' \<noteq> {#}"
       and "(mset (subst_list (subst x t) E), E') \<in> unif\<^sup>!" using 4 by (auto simp: t_def)
     moreover have "(mset ((t, Var x) # E), mset (subst_list (subst x t) E)) \<in> unif"
       using * by (auto intro: UNIF1.Var_right simp: unif_def)
     ultimately have ?case by (auto simp: t_def) }
   moreover
   { assume "x \<in> vars_term t"
     then have *: "x \<in> vars_term t" "t \<noteq> Var x" by (auto simp: t_def)
     then have "x \<in> vars_term t" "is_Fun t" by auto
     then have "\<not> unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable)
     then have **: "\<not> unifiable {(Var x \<cdot> \<sigma>, t \<cdot> \<sigma>)}" for \<sigma> :: "('b, 'a) subst"
       using subst_set_reflects_unifiable [of \<sigma> "{(Var x, t)}"] by (auto simp: subst_set_def)
     have ?case
     proof (cases "unifiable (set E)")
       case True
       then have "(mset E, {#}) \<in> unif\<^sup>*"
         by (simp add: unifiable_imp_empty)
       from unif_rtrancl_mono [OF this, of "{#(t, Var x)#}"] obtain \<sigma>
         where "(mset E + {#(t, Var x)#}, {#(t \<cdot> \<sigma>, Var x \<cdot> \<sigma>)#}) \<in> unif\<^sup>*"
         by (auto simp: subst_mset_def)
       moreover obtain E' where "E' \<noteq> {#}"
         and "({#(t \<cdot> \<sigma>, Var x \<cdot> \<sigma>)#}, E') \<in> unif\<^sup>!"
         using not_unifiable_imp_not_empty_NF and **
           by (metis unifiable_insert_swap set_mset_single)
       ultimately show ?thesis by (auto simp: t_def)
     next
       case False
       moreover have "\<not> unifiable {(t, Var x)}"
         using * by (simp add: unifiable_def)
       ultimately have "\<not> unifiable (set ((t, Var x) # E))" by (auto simp: unifiable_def unifiers_def)
       then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF t_def)
     qed }
   ultimately show ?case by blast
 qed
 
 lemma unify_complete:
   assumes "unify E bs = None"
   shows "unifiers (set E) = {}"
 proof -
   from unify_None [OF assms] obtain E'
     where "E' \<noteq> {#}" and "(mset E, E') \<in> unif\<^sup>!" by blast
   then have "\<not> unifiable (set E)"
     using irreducible_reachable_imp_not_unifiable by force
   then show ?thesis
     by (auto simp: unifiable_def)
 qed
 
 corollary ex_unify_if_unifiers_not_empty: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "unifiers es \<noteq> {} \<Longrightarrow> set xs = es \<Longrightarrow> \<exists>ys. unify xs [] = Some ys"
   using unify_complete by auto
 
 lemma mgu_complete:
   "mgu s t = None \<Longrightarrow> unifiers {(s, t)} = {}"
 proof -
   assume "mgu s t = None"
   then have "unify [(s, t)] [] = None" by (cases "unify [(s, t)] []", auto simp: mgu_def)
   then have "unifiers (set [(s, t)]) = {}" by (rule unify_complete)
   then show ?thesis by simp
 qed
 
 corollary ex_mgu_if_unifiers_not_empty: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "unifiers {(t,u)} \<noteq> {} \<Longrightarrow> \<exists>\<mu>. mgu t u = Some \<mu>"
   using mgu_complete by auto
 
 corollary ex_mgu_if_subst_apply_term_eq_subst_apply_term: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes t u :: "('f, 'v) Term.term" and \<sigma> :: "('f, 'v) subst"
   assumes t_eq_u: "t \<cdot> \<sigma> = u \<cdot> \<sigma>"
   shows "\<exists>\<mu> :: ('f, 'v) subst. Unification.mgu t u = Some \<mu>"
 proof -
   from t_eq_u have "unifiers {(t, u)} \<noteq> {}"
     unfolding unifiers_def by auto
   thus ?thesis
     by (rule ex_mgu_if_unifiers_not_empty)
 qed
 
 lemma finite_subst_domain_subst_of:
   "finite (subst_domain (subst_of xs))"
 proof (induct xs)
   case (Cons x xs)
   moreover have "finite (subst_domain (subst (fst x) (snd x)))" by (metis finite_subst_domain_subst)
   ultimately show ?case
     using subst_domain_compose [of "subst_of xs" "subst (fst x) (snd x)"]
     by (simp del: subst_subst_domain) (metis finite_subset infinite_Un)
 qed simp
 
 lemma unify_subst_domain: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes unif: "unify E [] = Some xs"
   shows "subst_domain (subst_of xs) \<subseteq> (\<Union>e \<in> set E. vars_term (fst e) \<union> vars_term (snd e))"
 proof -
   from unify_Some_UNIF[OF unif] obtain xs' where
     "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
     by auto
   thus ?thesis
     using UNIF_subst_domain_subset
     by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def)
 qed
 
 lemma mgu_subst_domain:
   assumes "mgu s t = Some \<sigma>"
   shows "subst_domain \<sigma> \<subseteq> vars_term s \<union> vars_term t"
 proof -
   obtain xs where "unify [(s, t)] [] = Some xs" and "\<sigma> = subst_of xs"
     using assms by (simp add: mgu_def split: option.splits)
   thus ?thesis
     using unify_subst_domain by fastforce
 qed
 
 lemma mgu_finite_subst_domain:
   "mgu s t = Some \<sigma> \<Longrightarrow> finite (subst_domain \<sigma>)"
   by (drule mgu_subst_domain) (simp add: finite_subset)
 
 lemma unify_range_vars: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes unif: "unify E [] = Some xs"
   shows "range_vars (subst_of xs) \<subseteq> (\<Union>e \<in> set E. vars_term (fst e) \<union> vars_term (snd e))"
 proof -
   from unify_Some_UNIF[OF unif] obtain xs' where
     "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
     by auto
   thus ?thesis
     using UNIF_range_vars_subset
     by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def)
 qed
 
 lemma mgu_range_vars: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "mgu s t = Some \<mu>"
   shows "range_vars \<mu> \<subseteq> vars_term s \<union> vars_term t"
 proof -
   obtain xs where "unify [(s, t)] [] = Some xs" and "\<mu> = subst_of xs"
     using assms by (simp add: mgu_def split: option.splits)
   thus ?thesis
     using unify_range_vars by fastforce
 qed
 
 lemma unify_subst_domain_range_vars_disjoint: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes unif: "unify E [] = Some xs"
   shows "subst_domain (subst_of xs) \<inter> range_vars (subst_of xs) = {}"
 proof -
   from unify_Some_UNIF[OF unif] obtain xs' where
     "subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
     by auto
   thus ?thesis
     using UNIF_subst_domain_range_vars_Int by metis
 qed
 
 lemma mgu_subst_domain_range_vars_disjoint: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes "mgu s t = Some \<mu>"
   shows "subst_domain \<mu> \<inter> range_vars \<mu> = {}"
 proof -
   obtain xs where "unify [(s, t)] [] = Some xs" and "\<mu> = subst_of xs"
     using assms by (simp add: mgu_def split: option.splits)
   thus ?thesis
     using unify_subst_domain_range_vars_disjoint by metis
 qed
 
 corollary subst_apply_term_eq_subst_apply_term_if_mgu: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   assumes mgu_t_u: "mgu t u = Some \<mu>"
   shows "t \<cdot> \<mu> = u \<cdot> \<mu>"
   using mgu_sound[OF mgu_t_u]
   by (simp add: is_imgu_def unifiers_def)
 
 lemma mgu_same: "mgu t t = Some Var" \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   by (simp add: mgu_def unify_same)
 
 lemma mgu_is_Var_if_not_in_equations: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes \<mu> :: "('f, 'v) subst" and E :: "('f, 'v) equations" and x :: 'v
   assumes
     mgu_\<mu>: "is_mgu \<mu> E" and
     x_not_in: "x \<notin> (\<Union>e\<in>E. vars_term (fst e) \<union> vars_term (snd e))"
   shows "is_Var (\<mu> x)"
 proof -
   from mgu_\<mu> have unif_\<mu>: "\<mu> \<in> unifiers E" and minimal_\<mu>: "\<forall>\<tau> \<in> unifiers E. \<exists>\<gamma>. \<tau> = \<mu> \<circ>\<^sub>s \<gamma>"
     by (simp_all add: is_mgu_def)
 
   define \<tau> :: "('f, 'v) subst" where
     "\<tau> = (\<lambda>x. if x \<in> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e)) then \<mu> x else Var x)"
 
   have \<open>\<tau> \<in> unifiers E\<close>
     unfolding unifiers_def mem_Collect_eq
   proof (rule ballI)
     fix e assume "e \<in> E"
     with unif_\<mu> have "fst e \<cdot> \<mu> = snd e \<cdot> \<mu>"
       by blast
     moreover from \<open>e \<in> E\<close> have "fst e \<cdot> \<tau> = fst e \<cdot> \<mu>" and "snd e \<cdot> \<tau> = snd e \<cdot> \<mu>"
       unfolding term_subst_eq_conv
       by (auto simp: \<tau>_def)
     ultimately show "fst e \<cdot> \<tau> = snd e \<cdot> \<tau>"
       by simp
   qed
   with minimal_\<mu> obtain \<gamma> where "\<mu> \<circ>\<^sub>s \<gamma> = \<tau>"
     by auto
   with x_not_in have "(\<mu> \<circ>\<^sub>s \<gamma>) x = Var x"
     by (simp add: \<tau>_def)
   thus "is_Var (\<mu> x)"
     by (metis subst_apply_eq_Var subst_compose term.disc(1))
 qed
 
 corollary mgu_ball_is_Var: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   "is_mgu \<mu> E \<Longrightarrow> \<forall>x \<in> - (\<Union>e\<in>E. vars_term (fst e) \<union> vars_term (snd e)). is_Var (\<mu> x)"
   by (rule ballI) (rule mgu_is_Var_if_not_in_equations[folded Compl_iff])
 
 lemma mgu_inj_on: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes \<mu> :: "('f, 'v) subst" and E :: "('f, 'v) equations"
   assumes mgu_\<mu>: "is_mgu \<mu> E"
   shows "inj_on \<mu> (- (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e)))"
 proof (rule inj_onI)
   fix x y
   assume
     x_in: "x \<in> - (\<Union>e\<in>E. vars_term (fst e) \<union> vars_term (snd e))" and
     y_in: "y \<in> - (\<Union>e\<in>E. vars_term (fst e) \<union> vars_term (snd e))" and
     "\<mu> x = \<mu> y"
 
   from mgu_\<mu> have unif_\<mu>: "\<mu> \<in> unifiers E" and minimal_\<mu>: "\<forall>\<tau> \<in> unifiers E. \<exists>\<gamma>. \<tau> = \<mu> \<circ>\<^sub>s \<gamma>"
     by (simp_all add: is_mgu_def)
 
   define \<tau> :: "('f, 'v) subst" where
     "\<tau> = (\<lambda>x. if x \<in> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e)) then \<mu> x else Var x)"
 
   have \<open>\<tau> \<in> unifiers E\<close>
     unfolding unifiers_def mem_Collect_eq
   proof (rule ballI)
     fix e assume "e \<in> E"
     with unif_\<mu> have "fst e \<cdot> \<mu> = snd e \<cdot> \<mu>"
       by blast
     moreover from \<open>e \<in> E\<close> have "fst e \<cdot> \<tau> = fst e \<cdot> \<mu>" and "snd e \<cdot> \<tau> = snd e \<cdot> \<mu>"
       unfolding term_subst_eq_conv
       by (auto simp: \<tau>_def)
     ultimately show "fst e \<cdot> \<tau> = snd e \<cdot> \<tau>"
       by simp
   qed
   with minimal_\<mu> obtain \<gamma> where "\<mu> \<circ>\<^sub>s \<gamma> = \<tau>"
     by auto
   hence "(\<mu> \<circ>\<^sub>s \<gamma>) x = Var x" and "(\<mu> \<circ>\<^sub>s \<gamma>) y = Var y"
     using ComplD[OF x_in] ComplD[OF y_in]
     by (simp_all add: \<tau>_def)
   with \<open>\<mu> x = \<mu> y\<close> show "x = y"
     by (simp add: subst_compose_def)
 qed
 
 lemma imgu_subst_domain_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes \<mu> :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
   assumes imgu_\<mu>: "is_imgu \<mu> E" and fin_E: "finite E"
   defines "Evars \<equiv> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e))"
   shows "subst_domain \<mu> \<subseteq> Evars"
 proof (intro Set.subsetI)
   from imgu_\<mu> have unif_\<mu>: "\<mu> \<in> unifiers E" and minimal_\<mu>: "\<forall>\<tau> \<in> unifiers E. \<mu> \<circ>\<^sub>s \<tau> = \<tau>"
     by (simp_all add: is_imgu_def)
 
   from fin_E obtain es :: "('f, 'v) equation list" where
     "set es = E"
     using finite_list by auto
   then obtain xs :: "('v \<times> ('f, 'v) Term.term) list" where
     unify_es: "unify es [] = Some xs"
     using unif_\<mu> ex_unify_if_unifiers_not_empty by blast
 
   define \<tau> :: "('f, 'v) subst" where
     "\<tau> = subst_of xs"
 
   have dom_\<tau>: "subst_domain \<tau> \<subseteq> Evars"
     using unify_subst_domain[OF unify_es, unfolded \<open>set es = E\<close>, folded Evars_def \<tau>_def] .
   have range_vars_\<tau>: "range_vars \<tau> \<subseteq> Evars"
     using unify_range_vars[OF unify_es, unfolded \<open>set es = E\<close>, folded Evars_def \<tau>_def] .
 
   have "\<tau> \<in> unifiers E"
     using \<open>set es = E\<close> unify_es \<tau>_def is_imgu_def unify_sound by blast
   with minimal_\<mu> have \<mu>_comp_\<tau>: "\<And>x. (\<mu> \<circ>\<^sub>s \<tau>) x = \<tau> x"
     by auto
 
   fix x :: 'v assume "x \<in> subst_domain \<mu>"
   hence "\<mu> x \<noteq> Var x"
     by (simp add: subst_domain_def)
 
   show "x \<in> Evars"
   proof (cases "x \<in> subst_domain \<tau>")
     case True
     thus ?thesis
       using dom_\<tau> by auto
   next
     case False
     hence "\<tau> x = Var x"
       by (simp add: subst_domain_def)
     hence "\<mu> x \<cdot> \<tau> = Var x"
       using \<mu>_comp_\<tau>[of x] by (simp add: subst_compose)
     thus ?thesis
     proof (rule subst_apply_eq_Var[of "\<mu> x" \<tau> x])
       show "\<And>y. \<mu> x = Var y \<Longrightarrow> \<tau> y = Var x \<Longrightarrow> ?thesis"
         using \<open>\<mu> x \<noteq> Var x\<close> range_vars_\<tau> mem_range_varsI[of \<tau> _ x] by auto
     qed
   qed
 qed
 
 lemma imgu_range_vars_of_equations_vars_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes \<mu> :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
   assumes imgu_\<mu>: "is_imgu \<mu> E" and fin_E: "finite E"
   defines "Evars \<equiv> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e))"
   shows "(\<Union>x \<in> Evars. vars_term (\<mu> x)) \<subseteq> Evars"
 proof (rule Set.subsetI)
   from imgu_\<mu> have unif_\<mu>: "\<mu> \<in> unifiers E" and minimal_\<mu>: "\<forall>\<tau> \<in> unifiers E. \<mu> \<circ>\<^sub>s \<tau> = \<tau>"
     by (simp_all add: is_imgu_def)
 
   from fin_E obtain es :: "('f, 'v) equation list" where
     "set es = E"
     using finite_list by auto
   then obtain xs :: "('v \<times> ('f, 'v) Term.term) list" where
     unify_es: "unify es [] = Some xs"
     using unif_\<mu> ex_unify_if_unifiers_not_empty by blast
 
   define \<tau> :: "('f, 'v) subst" where
     "\<tau> = subst_of xs"
 
   have dom_\<tau>: "subst_domain \<tau> \<subseteq> Evars"
     using unify_subst_domain[OF unify_es, unfolded \<open>set es = E\<close>, folded Evars_def \<tau>_def] .
   have range_vars_\<tau>: "range_vars \<tau> \<subseteq> Evars"
     using unify_range_vars[OF unify_es, unfolded \<open>set es = E\<close>, folded Evars_def \<tau>_def] .
   hence ball_vars_apply_\<tau>_subset: "\<forall>x \<in> subst_domain \<tau>. vars_term (\<tau> x) \<subseteq> Evars"
     unfolding range_vars_def
     by (simp add: SUP_le_iff)
 
   have "\<tau> \<in> unifiers E"
     using \<open>set es = E\<close> unify_es \<tau>_def is_imgu_def unify_sound by blast
   with minimal_\<mu> have \<mu>_comp_\<tau>: "\<And>x. (\<mu> \<circ>\<^sub>s \<tau>) x = \<tau> x"
     by auto
 
   fix y :: 'v assume "y \<in> (\<Union>x \<in> Evars. vars_term (\<mu> x))"
   then obtain x :: 'v where
     x_in: "x \<in> Evars" and y_in: "y \<in> vars_term (\<mu> x)"
     by (auto simp: subst_domain_def)
   have vars_\<tau>_x: "vars_term (\<tau> x) \<subseteq> Evars"
     using ball_vars_apply_\<tau>_subset subst_domain_def x_in by fastforce
 
   show "y \<in> Evars"
   proof (rule ccontr)
     assume "y \<notin> Evars"
     hence "y \<notin> vars_term (\<tau> x)"
       using vars_\<tau>_x by blast
     moreover have "y \<in> vars_term ((\<mu> \<circ>\<^sub>s \<tau>) x)"
     proof -
       have "\<tau> y = Var y"
         using \<open>y \<notin> Evars\<close> dom_\<tau>
         by (auto simp add: subst_domain_def)
       thus ?thesis
         unfolding subst_compose_def vars_term_subst_apply_term UN_iff
         using y_in by force
     qed
     ultimately show False
       using \<mu>_comp_\<tau>[of x] by simp
   qed
 qed
 
 lemma imgu_range_vars_subset: \<^marker>\<open>contributor \<open>Martin Desharnais\<close>\<close>
   fixes \<mu> :: "('f, 'v) subst" and E :: "('f, 'v) equations"
   assumes imgu_\<mu>: "is_imgu \<mu> E" and fin_E: "finite E"
   shows "range_vars \<mu> \<subseteq> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e))"
 proof -
   have "range_vars \<mu> = (\<Union>x \<in> subst_domain \<mu>. vars_term (\<mu> x))"
     by (simp add: range_vars_def)
   also have "\<dots> \<subseteq> (\<Union>x \<in> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e)). vars_term (\<mu> x))"
     using imgu_subst_domain_subset[OF imgu_\<mu> fin_E] by fast
   also have "\<dots> \<subseteq> (\<Union>e \<in> E. vars_term (fst e) \<union> vars_term (snd e))"
     using imgu_range_vars_of_equations_vars_subset[OF imgu_\<mu> fin_E] by metis
   finally show ?thesis .
 qed
 
+
+definition the_mgu :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> ('f ,'v) subst" where
+  "the_mgu s t = (case mgu s t of None \<Rightarrow> Var | Some \<delta> \<Rightarrow> \<delta>)"
+
+lemma the_mgu_is_imgu:
+  fixes \<sigma> :: "('f, 'v) subst"
+  assumes "s \<cdot> \<sigma> = t \<cdot> \<sigma>"
+  shows "is_imgu (the_mgu s t) {(s, t)}"
+proof -
+  from assms have "unifiers {(s, t)} \<noteq> {}" by (force simp: unifiers_def)
+  then obtain \<tau> where "mgu s t = Some \<tau>"
+    and "the_mgu s t = \<tau>"
+    using mgu_complete by (auto simp: the_mgu_def)
+  with mgu_sound show ?thesis by blast
+qed
+
+lemma the_mgu:
+  fixes \<sigma> :: "('f, 'v) subst"
+  assumes "s \<cdot> \<sigma> = t \<cdot> \<sigma>"
+  shows "s \<cdot> the_mgu s t = t \<cdot> the_mgu s t \<and> \<sigma> = the_mgu s t \<circ>\<^sub>s \<sigma>" 
+proof -
+  have *: "\<sigma> \<in> unifiers {(s, t)}" by (force simp: assms unifiers_def)
+  show ?thesis
+  proof (cases "mgu s t")
+    assume "mgu s t = None"
+    then have "unifiers {(s, t)} = {}" by (rule mgu_complete)
+    with * show ?thesis by simp
+  next
+    fix \<tau>
+    assume "mgu s t = Some \<tau>"
+    moreover then have "is_imgu \<tau> {(s, t)}" by (rule mgu_sound)
+    ultimately have "is_imgu (the_mgu s t) {(s, t)}" by (unfold the_mgu_def, simp)
+    with * show ?thesis by (auto simp: is_imgu_def unifiers_def)
+  qed
+qed
+
+subsubsection \<open>Unification of two terms where variables should be considered disjoint\<close>
+
+definition
+  mgu_var_disjoint_generic ::
+    "('v \<Rightarrow> 'u) \<Rightarrow> ('w \<Rightarrow> 'u) \<Rightarrow> ('f, 'v) term \<Rightarrow> ('f, 'w) term \<Rightarrow>
+      (('f, 'v, 'u) gsubst \<times> ('f, 'w, 'u) gsubst) option"
+where
+  "mgu_var_disjoint_generic vu wu s t =
+    (case mgu (map_vars_term vu s) (map_vars_term wu t) of
+      None \<Rightarrow> None 
+    | Some \<gamma> \<Rightarrow> Some (\<gamma> \<circ> vu, \<gamma> \<circ> wu))"
+
+lemma mgu_var_disjoint_generic_sound: 
+  assumes unif: "mgu_var_disjoint_generic vu wu s t = Some (\<gamma>1, \<gamma>2)"
+  shows "s \<cdot> \<gamma>1 = t \<cdot> \<gamma>2"
+proof -
+  from unif[unfolded mgu_var_disjoint_generic_def] obtain \<gamma> where
+    unif2: "mgu (map_vars_term vu s) (map_vars_term wu t) = Some \<gamma>"
+    by (cases "mgu (map_vars_term vu s) (map_vars_term wu t)", auto)
+  from mgu_sound[OF unif2[unfolded mgu_var_disjoint_generic_def], unfolded is_imgu_def unifiers_def]
+  have "map_vars_term vu s \<cdot> \<gamma> = map_vars_term wu t \<cdot> \<gamma>" by auto
+  from this[unfolded apply_subst_map_vars_term] unif[unfolded mgu_var_disjoint_generic_def unif2] 
+  show ?thesis by simp
+qed
+
+(* if terms s and t can become identical via two substitutions \<sigma> and \<delta> 
+   then mgu_var_disjoint yields two more general substitutions \<mu>1 \<mu>2 *)
+lemma mgu_var_disjoint_generic_complete:
+  fixes \<sigma> :: "('f, 'v, 'u) gsubst" and \<tau> :: "('f, 'w, 'u) gsubst" 
+    and vu :: "'v \<Rightarrow> 'u" and wu:: "'w \<Rightarrow> 'u"
+  assumes inj: "inj vu" "inj wu"
+    and vwu: "range vu \<inter> range wu = {}"
+    and unif_disj: "s \<cdot> \<sigma> = t \<cdot> \<tau>"
+  shows "\<exists>\<mu>1 \<mu>2 \<delta>. mgu_var_disjoint_generic vu wu s t = Some (\<mu>1, \<mu>2) \<and> 
+    \<sigma> = \<mu>1 \<circ>\<^sub>s \<delta> \<and>
+    \<tau> = \<mu>2 \<circ>\<^sub>s \<delta> \<and>
+    s \<cdot> \<mu>1 = t \<cdot> \<mu>2"
+proof -
+  note inv1[simp] = the_inv_f_f[OF inj(1)]
+  note inv2[simp] = the_inv_f_f[OF inj(2)]
+  obtain \<gamma> :: "('f,'u)subst" where gamma: "\<gamma> = (\<lambda> x. if x \<in> range vu then \<sigma> (the_inv vu x) else \<tau> (the_inv wu x))" by auto 
+  have ids: "s \<cdot> \<sigma> = map_vars_term vu s \<cdot> \<gamma>" unfolding gamma
+    by (induct s, auto)
+  have idt: "t \<cdot> \<tau> = map_vars_term wu t \<cdot> \<gamma>" unfolding gamma
+    by (induct t, insert vwu, auto)
+  from unif_disj ids idt
+  have unif: "map_vars_term vu s \<cdot> \<gamma> = map_vars_term wu t \<cdot> \<gamma>" (is "?s \<cdot> \<gamma> = ?t \<cdot> \<gamma>") by auto
+  from the_mgu[OF unif] have unif2: "?s \<cdot> the_mgu ?s ?t = ?t \<cdot> the_mgu ?s ?t" and inst: "\<gamma> = the_mgu ?s ?t \<circ>\<^sub>s \<gamma>" by auto
+  have "mgu ?s ?t = Some (the_mgu ?s ?t)" unfolding the_mgu_def
+    using mgu_complete[unfolded unifiers_def] unif
+    by (cases "mgu ?s ?t", auto)
+  with inst obtain \<mu> where mu: "mgu ?s ?t = Some \<mu>" and gamma_mu: "\<gamma> = \<mu> \<circ>\<^sub>s \<gamma>" by auto
+  let ?tau1 = "\<mu> \<circ> vu"
+  let ?tau2 = "\<mu> \<circ> wu"
+  show ?thesis unfolding mgu_var_disjoint_generic_def mu option.simps
+  proof (intro exI conjI, rule refl)
+    show "\<sigma> = ?tau1 \<circ>\<^sub>s \<gamma>"
+    proof (rule ext)
+      fix x
+      have "(?tau1 \<circ>\<^sub>s \<gamma>) x = \<gamma> (vu x)" using fun_cong[OF gamma_mu, of "vu x"] by (simp add: subst_compose_def)
+      also have "... = \<sigma> x" unfolding gamma by simp
+      finally show "\<sigma> x = (?tau1 \<circ>\<^sub>s \<gamma>) x" by simp
+    qed
+  next
+    show "\<tau> = ?tau2 \<circ>\<^sub>s \<gamma>"
+    proof (rule ext)
+      fix x
+      have "(?tau2 \<circ>\<^sub>s \<gamma>) x = \<gamma> (wu x)" using fun_cong[OF gamma_mu, of "wu x"] by (simp add: subst_compose_def)
+      also have "... = \<tau> x" unfolding gamma using vwu by auto
+      finally show "\<tau> x = (?tau2 \<circ>\<^sub>s \<gamma>) x" by simp
+    qed
+  next
+    have "s \<cdot> ?tau1 = map_vars_term vu s \<cdot> \<mu>" unfolding apply_subst_map_vars_term ..
+    also have "... = map_vars_term wu t \<cdot> \<mu>"
+      unfolding unif2[unfolded the_mgu_def mu option.simps] ..
+    also have "... = t \<cdot> ?tau2" unfolding apply_subst_map_vars_term ..
+    finally show "s \<cdot> ?tau1 = t \<cdot> ?tau2" .
+  qed
+qed
+
+abbreviation "mgu_var_disjoint_sum \<equiv> mgu_var_disjoint_generic Inl Inr"
+
+lemma mgu_var_disjoint_sum_sound: 
+  "mgu_var_disjoint_sum s t = Some (\<gamma>1, \<gamma>2) \<Longrightarrow> s \<cdot> \<gamma>1 = t \<cdot> \<gamma>2"
+  by (rule mgu_var_disjoint_generic_sound)
+
+lemma mgu_var_disjoint_sum_complete:
+  fixes \<sigma> :: "('f, 'v, 'v + 'w) gsubst" and \<tau> :: "('f, 'w, 'v + 'w) gsubst"
+  assumes unif_disj: "s \<cdot> \<sigma> = t \<cdot> \<tau>"
+  shows "\<exists>\<mu>1 \<mu>2 \<delta>. mgu_var_disjoint_sum s t = Some (\<mu>1, \<mu>2) \<and> 
+    \<sigma> = \<mu>1 \<circ>\<^sub>s \<delta> \<and>
+    \<tau> = \<mu>2 \<circ>\<^sub>s \<delta> \<and>
+    s \<cdot> \<mu>1 = t \<cdot> \<mu>2"
+  by (rule mgu_var_disjoint_generic_complete[OF _ _ _ unif_disj], auto simp: inj_on_def)
+
+fun map_vars_subst_ran :: "('w \<Rightarrow> 'u) \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'v, 'u) gsubst" where
+  "map_vars_subst_ran m \<sigma> = (\<lambda>v. map_vars_term m (\<sigma> v))"
+
+lemma map_vars_subst_ran:
+  shows "map_vars_term m (t \<cdot> \<sigma>) = t \<cdot> map_vars_subst_ran m \<sigma>"
+  by (induct t) (auto)
+
+lemma mgu_var_disjoint_sum_instance:
+  fixes \<sigma> :: "('f, 'v) subst" and \<delta> :: "('f, 'v) subst"
+  assumes unif_disj: "s \<cdot> \<sigma> = t \<cdot> \<delta>"
+  shows "\<exists>\<mu>1 \<mu>2 \<tau>. mgu_var_disjoint_sum s t = Some (\<mu>1, \<mu>2) \<and>
+    \<sigma> = \<mu>1 \<circ>\<^sub>s \<tau> \<and>
+    \<delta> = \<mu>2 \<circ>\<^sub>s \<tau> \<and> 
+    s \<cdot> \<mu>1 = t \<cdot> \<mu>2"
+proof -
+  let ?m = "map_vars_subst_ran (Inl :: ('v \<Rightarrow> 'v + 'v))"
+  let ?m' = "map_vars_subst_ran (case_sum (\<lambda> x. x) (\<lambda> x. x))"
+  from unif_disj have id: "map_vars_term Inl (s \<cdot> \<sigma>) = map_vars_term Inl (t \<cdot> \<delta>)" by simp
+  from mgu_var_disjoint_sum_complete[OF id[unfolded map_vars_subst_ran]]
+  obtain \<mu>1 \<mu>2 \<tau> where mgu: "mgu_var_disjoint_sum s t = Some (\<mu>1,\<mu>2)"
+    and \<sigma>: "?m \<sigma> = \<mu>1 \<circ>\<^sub>s \<tau>" 
+    and \<delta>: "?m \<delta> = \<mu>2 \<circ>\<^sub>s \<tau>"
+    and unif: "s \<cdot> \<mu>1 = t \<cdot> \<mu>2" by blast
+  {
+    fix \<sigma> :: "('f, 'v) subst"
+    have "?m' (?m \<sigma>) = \<sigma>" by (simp add: map_vars_term_compose o_def term.map_ident)
+  } note id = this
+  {
+    fix \<mu> :: "('f,'v,'v+'v)gsubst" and \<tau> :: "('f,'v + 'v)subst"
+    have "?m' (\<mu> \<circ>\<^sub>s \<tau>) = \<mu> \<circ>\<^sub>s ?m' \<tau>"
+      by (rule ext, unfold subst_compose_def, simp add: map_vars_subst_ran)
+  } note id' = this
+  from arg_cong[OF \<sigma>, of ?m', unfolded id id'] have \<sigma>: "\<sigma> = \<mu>1 \<circ>\<^sub>s ?m' \<tau>" .
+  from arg_cong[OF \<delta>, of ?m', unfolded id id'] have \<delta>: "\<delta> = \<mu>2 \<circ>\<^sub>s ?m' \<tau>" .
+  show ?thesis
+    by (intro exI conjI, rule mgu, rule \<sigma>, rule \<delta>, rule unif)
+qed
+
+subsubsection \<open>A variable disjoint unification algorithm without changing the type\<close>
+
+text \<open>We pass the renaming function as additional argument\<close>
+
+definition mgu_vd :: "'v :: infinite renaming2 \<Rightarrow> _ \<Rightarrow> _" where
+  "mgu_vd r = mgu_var_disjoint_generic (rename_1 r) (rename_2 r)" 
+
+lemma mgu_vd_sound: "mgu_vd r s t = Some (\<gamma>1, \<gamma>2) \<Longrightarrow> s \<cdot> \<gamma>1 = t \<cdot> \<gamma>2"
+  unfolding mgu_vd_def by (rule mgu_var_disjoint_generic_sound)
+
+lemma mgu_vd_complete: 
+  fixes \<sigma> :: "('f, 'v :: infinite) subst" and \<tau> :: "('f, 'v) subst" 
+  assumes unif_disj: "s \<cdot> \<sigma> = t \<cdot> \<tau>"
+  shows "\<exists>\<mu>1 \<mu>2 \<delta>. mgu_vd r s t = Some (\<mu>1, \<mu>2) \<and>
+    \<sigma> = \<mu>1 \<circ>\<^sub>s \<delta> \<and>
+    \<tau> = \<mu>2 \<circ>\<^sub>s \<delta> \<and>
+    s \<cdot> \<mu>1 = t \<cdot> \<mu>2"
+  unfolding mgu_vd_def
+  by (rule mgu_var_disjoint_generic_complete[OF rename_12 unif_disj])
+
 end
diff --git a/thys/First_Order_Terms/Unification_String.thy b/thys/First_Order_Terms/Unification_String.thy
new file mode 100644
--- /dev/null
+++ b/thys/First_Order_Terms/Unification_String.thy
@@ -0,0 +1,27 @@
+subsection \<open>A variable disjoint unification algorithm for terms with string variables\<close>
+
+theory Unification_String
+imports
+  Unification
+  Renaming2_String
+begin
+definition "mgu_vd_string = mgu_vd string_rename" 
+
+lemma mgu_vd_string_code[code]: "mgu_vd_string = mgu_var_disjoint_generic (Cons (CHR ''x'')) (Cons (CHR ''y''))" 
+  unfolding mgu_vd_string_def mgu_vd_def
+  by (transfer, auto)
+
+lemma mgu_vd_string_sound: 
+  "mgu_vd_string s t = Some (\<gamma>1, \<gamma>2) \<Longrightarrow> s \<cdot> \<gamma>1 = t \<cdot> \<gamma>2"
+  unfolding mgu_vd_string_def by (rule mgu_vd_sound)
+
+lemma mgu_vd_string_complete:
+  fixes \<sigma> :: "('f, string) subst" and \<tau> :: "('f, string) subst" 
+  assumes "s \<cdot> \<sigma> = t \<cdot> \<tau>"
+  shows "\<exists>\<mu>1 \<mu>2 \<delta>. mgu_vd_string s t = Some (\<mu>1, \<mu>2) \<and>
+    \<sigma> = \<mu>1 \<circ>\<^sub>s \<delta> \<and>
+    \<tau> = \<mu>2 \<circ>\<^sub>s \<delta> \<and>
+    s \<cdot> \<mu>1 = t \<cdot> \<mu>2"
+  unfolding mgu_vd_string_def
+  by (rule mgu_vd_complete[OF assms])
+end
\ No newline at end of file
diff --git a/thys/Regular_Tree_Relations/Util/Term_Context.thy b/thys/Regular_Tree_Relations/Util/Term_Context.thy
--- a/thys/Regular_Tree_Relations/Util/Term_Context.thy
+++ b/thys/Regular_Tree_Relations/Util/Term_Context.thy
@@ -1,526 +1,525 @@
 section \<open>Preliminaries\<close>
 
 theory Term_Context
   imports First_Order_Terms.Term
     First_Order_Terms.Subterm_and_Context
     Polynomial_Factorization.Missing_List
 begin
 
 subsection \<open>Additional functionality on @{type term} and @{type ctxt}\<close>
 subsubsection \<open>Positions\<close>
 
 type_synonym pos = "nat list"
 context
   notes conj_cong [fundef_cong]
 begin
 
 fun poss :: "('f, 'v) term \<Rightarrow> pos set" where
   "poss (Var x) = {[]}"
 | "poss (Fun f ss) = {[]} \<union> {i # p | i p. i < length ss \<and> p \<in> poss (ss ! i)}"
 end
 
 fun hole_pos where
   "hole_pos \<box> = []"
 | "hole_pos (More f ss D ts) = length ss # hole_pos D"
 
 definition position_less_eq (infixl "\<le>\<^sub>p" 67) where
   "p \<le>\<^sub>p q \<longleftrightarrow> (\<exists> r. p @ r = q)"
 
 abbreviation position_less (infixl "<\<^sub>p" 67) where
   "p <\<^sub>p q \<equiv> p \<noteq> q \<and> p \<le>\<^sub>p q"
 
 definition position_par  (infixl "\<bottom>" 67) where
   "p \<bottom> q \<longleftrightarrow> \<not> (p \<le>\<^sub>p q) \<and> \<not> (q \<le>\<^sub>p p)"
 
 fun remove_prefix where
   "remove_prefix (x # xs) (y # ys) = (if x = y then remove_prefix xs ys else None)"
 | "remove_prefix [] ys = Some ys"
 | "remove_prefix xs [] = None"
 
 definition pos_diff  (infixl "-\<^sub>p" 67) where
   "p -\<^sub>p q = the (remove_prefix q p)"
 
 fun subt_at :: "('f, 'v) term \<Rightarrow> pos \<Rightarrow> ('f, 'v) term" (infixl "|'_" 67) where
   "s |_ [] = s"
 | "Fun f ss |_ (i # p) = (ss ! i) |_ p"
 | "Var x |_ _ = undefined"
 
 fun ctxt_at_pos where
   "ctxt_at_pos s [] = \<box>"
 | "ctxt_at_pos (Fun f ss) (i # p) = More f (take i ss) (ctxt_at_pos (ss ! i) p) (drop (Suc i) ss)"
 | "ctxt_at_pos (Var x) _ = undefined"
 
 fun replace_term_at ("_[_ \<leftarrow> _]" [1000, 0, 0] 1000) where
   "replace_term_at s [] t = t"
 | "replace_term_at (Var x) ps t = (Var x)"
 | "replace_term_at (Fun f ts) (i # ps) t =
     (if i < length ts then Fun f (ts[i:=(replace_term_at (ts ! i) ps t)]) else Fun f ts)"
 
 fun fun_at :: "('f, 'v) term \<Rightarrow> pos \<Rightarrow> ('f + 'v) option" where
   "fun_at (Var x) [] = Some (Inr x)"
 | "fun_at (Fun f ts) [] = Some (Inl f)"
 | "fun_at (Fun f ts) (i # p) = (if i < length ts then fun_at (ts ! i) p else None)"
 | "fun_at _ _ = None"
 
 subsubsection \<open>Computing the signature\<close>
 
 fun funas_term where
   "funas_term (Var x) = {}"
 | "funas_term (Fun f ts) = insert (f, length ts) (\<Union> (set (map funas_term ts)))"
 
 fun funas_ctxt where
   "funas_ctxt \<box> = {}"
 | "funas_ctxt (More f ss C ts) = (\<Union> (set (map funas_term ss))) \<union>
     insert (f, Suc (length ss + length ts)) (funas_ctxt C) \<union> (\<Union> (set (map funas_term ts)))"
 
 subsubsection \<open>Groundness\<close>
 
 fun ground where
   "ground (Var x) = False"
 | "ground (Fun f ts) = (\<forall> t \<in> set ts. ground t)"
 
 fun ground_ctxt where
   "ground_ctxt \<box> \<longleftrightarrow> True"
 | "ground_ctxt (More f ss C ts) \<longleftrightarrow> (\<forall> t \<in> set ss. ground t) \<and> ground_ctxt C \<and> (\<forall> t \<in> set ts. ground t)"
 
 subsubsection \<open>Depth\<close>
 fun depth where
   "depth (Var x) = 0"
 | "depth (Fun f []) = 0"
 | "depth (Fun f ts) = Suc (Max (depth ` set ts))"
 
 subsubsection \<open>Type conversion\<close>
 
 text \<open>We require a function which adapts the type of variables of a term,
    so that states of the automaton and variables in the term language can be
    chosen independently.\<close>
 
-abbreviation "map_vars_term f \<equiv> map_term (\<lambda> x. x) f"
 abbreviation "map_funs_term f \<equiv> map_term f (\<lambda> x. x)"
 abbreviation "map_both f \<equiv> map_prod f f"
 
 definition adapt_vars :: "('f, 'q) term \<Rightarrow> ('f,'v)term" where 
   [code del]: "adapt_vars \<equiv> map_vars_term (\<lambda>_. undefined)"
 
 abbreviation "map_vars_ctxt f \<equiv> map_ctxt (\<lambda>x. x) f"
 definition adapt_vars_ctxt :: "('f,'q)ctxt \<Rightarrow> ('f,'v)ctxt" where
   [code del]: "adapt_vars_ctxt = map_vars_ctxt (\<lambda>_. undefined)"
 
 
 subsection \<open>Properties of @{type pos}\<close>
 
 lemma position_less_eq_induct [consumes 1]:
   assumes "p \<le>\<^sub>p q" and "\<And> p. P p p"
     and "\<And> p q r. p \<le>\<^sub>p q \<Longrightarrow> P p q \<Longrightarrow> P p (q @ r)"
   shows "P p q" using assms
 proof (induct p arbitrary: q)
   case Nil then show ?case
     by (metis append_Nil position_less_eq_def)
 next
   case (Cons a p)
   then show ?case
     by (metis append_Nil2 position_less_eq_def)
 qed
 
 text \<open>We show the correspondence between the function @{const remove_prefix} and
 the order on positions @{const position_less_eq}. Moreover how it can be used to
 compute the difference of positions.\<close>
 
 lemma remove_prefix_Nil [simp]:
   "remove_prefix xs xs = Some []"
   by (induct xs) auto
 
 lemma remove_prefix_Some:
   assumes "remove_prefix xs ys = Some zs"
   shows "ys = xs @ zs" using assms
 proof (induct xs arbitrary: ys)
   case (Cons x xs)
   show ?case using Cons(1)[of "tl ys"] Cons(2)
     by (cases ys) (auto split: if_splits)
 qed auto
 
 lemma remove_prefix_append:
   "remove_prefix xs (xs @ ys) = Some ys"
   by (induct xs) auto
 
 lemma remove_prefix_iff:
   "remove_prefix xs ys = Some zs \<longleftrightarrow> ys = xs @ zs"
   using remove_prefix_Some remove_prefix_append
   by blast
 
 lemma position_less_eq_remove_prefix:
   "p \<le>\<^sub>p q \<Longrightarrow> remove_prefix p q \<noteq> None"
   by (induct rule: position_less_eq_induct) (auto simp: remove_prefix_iff)
 
 text \<open>Simplification rules on @{const position_less_eq}, @{const pos_diff},
   and @{const position_par}.\<close>
 
 lemma position_less_refl [simp]: "p \<le>\<^sub>p p"
   by (auto simp: position_less_eq_def)
 
 lemma position_less_eq_Cons [simp]:
   "(i # ps) \<le>\<^sub>p (j # qs) \<longleftrightarrow> i = j \<and> ps \<le>\<^sub>p qs"
   by (auto simp: position_less_eq_def)
 
 lemma position_less_Nil_is_bot [simp]: "[] \<le>\<^sub>p p"
   by (auto simp: position_less_eq_def)
 
 lemma position_less_Nil_is_bot2 [simp]: "p \<le>\<^sub>p [] \<longleftrightarrow> p = []"
   by (auto simp: position_less_eq_def)
 
 lemma position_diff_Nil [simp]: "q -\<^sub>p [] = q"
   by (auto simp: pos_diff_def)
 
 lemma position_diff_Cons [simp]:
   "(i # ps) -\<^sub>p (i # qs) = ps -\<^sub>p qs"
   by (auto simp: pos_diff_def)
 
 lemma Nil_not_par [simp]:
   "[] \<bottom> p \<longleftrightarrow> False"
   "p \<bottom> [] \<longleftrightarrow> False"
   by (auto simp: position_par_def)
 
 lemma par_not_refl [simp]: "p \<bottom> p \<longleftrightarrow> False"
   by (auto simp: position_par_def)
 
 lemma par_Cons_iff:
   "(i # ps) \<bottom> (j # qs) \<longleftrightarrow> (i \<noteq> j \<or> ps \<bottom> qs)"
   by (auto simp: position_par_def)
 
 
 text \<open>Simplification rules on @{const poss}.\<close>
 
 lemma Nil_in_poss [simp]: "[] \<in> poss t"
   by (cases t) auto
 
 lemma poss_Cons [simp]:
   "i # p \<in> poss t \<Longrightarrow> [i] \<in> poss t"
   by (cases t) auto
 
 lemma poss_Cons_poss:
   "i # q \<in> poss t \<longleftrightarrow> i < length (args t) \<and> q \<in> poss (args t ! i)"
   by (cases t) auto
 
 lemma poss_append_poss:
   "p @ q \<in> poss t \<longleftrightarrow> p \<in> poss t \<and> q \<in> poss (t |_ p)"
 proof (induct p arbitrary: t)
   case (Cons i p)
   from Cons[of "args t ! i"] show ?case
     by (cases t) auto
 qed auto
 
 
 text \<open>Simplification rules on @{const hole_pos}\<close>
 
 lemma hole_pos_map_vars [simp]:
   "hole_pos (map_vars_ctxt f C) = hole_pos C"
   by (induct C) auto
 
 lemma hole_pos_in_ctxt_apply [simp]: "hole_pos C \<in> poss C\<langle>u\<rangle>"
   by (induct C) auto
 
 subsection \<open>Properties of @{const ground} and @{const ground_ctxt}\<close>
 
 lemma ground_vars_term_empty [simp]:
   "ground t \<Longrightarrow> vars_term t = {}"
   by (induct t) auto
 
 lemma ground_map_term [simp]:
   "ground (map_term f h t) = ground t"
   by (induct t) auto
 
 lemma ground_ctxt_apply [simp]:
   "ground C\<langle>t\<rangle> \<longleftrightarrow> ground_ctxt C \<and> ground t"
   by (induct C) auto
 
 lemma ground_ctxt_comp [intro]:
   "ground_ctxt C \<Longrightarrow> ground_ctxt D \<Longrightarrow> ground_ctxt (C \<circ>\<^sub>c D)"
   by (induct C) auto
 
 lemma ctxt_comp_n_pres_ground [intro]:
   "ground_ctxt C \<Longrightarrow> ground_ctxt (C^n)"
   by (induct n arbitrary: C) auto
 
 lemma subterm_eq_pres_ground:
   assumes "ground s" and "s \<unrhd> t"
   shows "ground t" using assms(2,1)
   by (induct) auto
 
 lemma ground_substD:
   "ground (l \<cdot> \<sigma>) \<Longrightarrow> x \<in> vars_term l \<Longrightarrow> ground (\<sigma> x)"
   by (induct l) auto
 
 lemma ground_substI:
   "(\<And> x. x \<in> vars_term s \<Longrightarrow> ground (\<sigma> x)) \<Longrightarrow> ground (s \<cdot> \<sigma>)"
   by (induct s) auto
 
 
 subsection \<open>Properties on signature induced by a term @{type term}/context @{type ctxt}\<close>
 
 lemma funas_ctxt_apply [simp]:
   "funas_term C\<langle>t\<rangle> = funas_ctxt C \<union> funas_term t"
   by (induct C) auto
 
 lemma funas_term_map [simp]:
   "funas_term (map_term f h t) = (\<lambda> (g, n). (f g, n)) ` funas_term t"
   by (induct t) auto
 
 lemma funas_term_subst:
   "funas_term (l \<cdot> \<sigma>) = funas_term l \<union> (\<Union> (funas_term ` \<sigma> ` vars_term l))"
   by (induct l) auto
 
 lemma funas_ctxt_comp [simp]:
   "funas_ctxt (C \<circ>\<^sub>c D) = funas_ctxt C \<union> funas_ctxt D"
   by (induct C) auto
 
 lemma ctxt_comp_n_funas [simp]:
   "(f, v) \<in> funas_ctxt (C^n) \<Longrightarrow> (f, v) \<in> funas_ctxt C"
   by (induct n arbitrary: C) auto
 
 lemma ctxt_comp_n_pres_funas [intro]:
   "funas_ctxt C \<subseteq> \<F> \<Longrightarrow> funas_ctxt (C^n) \<subseteq> \<F>"
   by (induct n arbitrary: C) auto
 
 subsection \<open>Properties on subterm at given position @{const subt_at}\<close>
 
 lemma subt_at_Cons_comp:
   "i # p \<in> poss s \<Longrightarrow> (s |_ [i]) |_ p = s |_ (i # p)"
   by (cases s) auto
 
 lemma ctxt_at_pos_subt_at_pos:
   "p \<in> poss t \<Longrightarrow> (ctxt_at_pos t p)\<langle>u\<rangle> |_ p = u"
 proof (induct p arbitrary: t)
   case (Cons i p)
   then show ?case using id_take_nth_drop
     by (cases t) (auto simp: nth_append)
 qed auto
 
 lemma ctxt_at_pos_subt_at_id:
   "p \<in> poss t \<Longrightarrow> (ctxt_at_pos t p)\<langle>t |_ p\<rangle> = t"
 proof (induct p arbitrary: t)
   case (Cons i p)
   then show ?case using id_take_nth_drop
     by (cases t) force+ 
 qed auto
 
 lemma subst_at_ctxt_at_eq_termD:
   assumes "s = t" "p \<in> poss t"
   shows "s |_ p = t |_ p \<and> ctxt_at_pos s p = ctxt_at_pos t p" using assms
   by auto
 
 lemma subst_at_ctxt_at_eq_termI:
   assumes "p \<in> poss s" "p \<in> poss t"
     and "s |_p = t |_ p"
     and "ctxt_at_pos s p = ctxt_at_pos t p"
   shows "s = t" using assms
   by (metis ctxt_at_pos_subt_at_id)
 
 lemma subt_at_subterm_eq [intro!]:
   "p \<in> poss t \<Longrightarrow> t \<unrhd> t |_ p"
 proof (induct p arbitrary: t)
   case (Cons i p)
   from Cons(1)[of "args t ! i"] Cons(2) show ?case
     by (cases t) force+
 qed auto
 
 lemma subt_at_subterm [intro!]:
   "p \<in> poss t \<Longrightarrow> p \<noteq> [] \<Longrightarrow>  t \<rhd> t |_ p"
 proof (induct p arbitrary: t)
   case (Cons i p)
   from Cons(1)[of "args t ! i"] Cons(2) show ?case
     by (cases t) force+
 qed auto
 
 
 lemma ctxt_at_pos_hole_pos [simp]: "ctxt_at_pos C\<langle>s\<rangle> (hole_pos C) = C"
   by (induct C) auto
 
 subsection \<open>Properties on replace terms at a given position
   @{const replace_term_at}\<close>
 
 lemma replace_term_at_not_poss [simp]:
   "p \<notin> poss s \<Longrightarrow> s[p \<leftarrow> t] = s"
 proof (induct s arbitrary: p)
   case (Var x) then show ?case by (cases p) auto
 next
   case (Fun f ts) show ?case using Fun(1)[OF nth_mem] Fun(2)
     by (cases p) (auto simp: min_def intro!: nth_equalityI)
 qed
 
 lemma replace_term_at_replace_at_conv:
   "p \<in> poss s \<Longrightarrow> (ctxt_at_pos s p)\<langle>t\<rangle> = s[p \<leftarrow> t]"
   by (induct s arbitrary: p) (auto simp: upd_conv_take_nth_drop)
 
 lemma parallel_replace_term_commute [ac_simps]:
   "p \<bottom> q \<Longrightarrow> s[p \<leftarrow> t][q \<leftarrow> u] = s[q \<leftarrow> u][p \<leftarrow> t]"
 proof (induct s arbitrary: p q)
   case (Var x) then show ?case
     by (cases p; cases q) auto
 next
   case (Fun f ts)
   from Fun(2) have "p \<noteq> []" "q \<noteq> []" by auto
   then obtain i j ps qs where [simp]: "p = i # ps" "q = j # qs"
     by (cases p; cases q) auto
   have "i \<noteq> j \<Longrightarrow> (Fun f ts)[p \<leftarrow> t][q \<leftarrow> u] = (Fun f ts)[q \<leftarrow> u][p \<leftarrow> t]"
     by (auto simp: list_update_swap)
   then show ?case using Fun(1)[OF nth_mem, of j ps qs] Fun(2)
     by (cases "i = j") (auto simp: par_Cons_iff)
 qed
 
 lemma replace_term_at_above [simp]:
   "p \<le>\<^sub>p q \<Longrightarrow> s[q \<leftarrow> t][p \<leftarrow> u] = s[p \<leftarrow> u]"
 proof (induct p arbitrary: s q)
   case (Cons i p)
   show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
     by (cases q; cases s) auto
 qed auto
 
 lemma replace_term_at_below [simp]:
   "p <\<^sub>p q \<Longrightarrow> s[p \<leftarrow> t][q \<leftarrow> u] = s[p \<leftarrow> t[q -\<^sub>p p \<leftarrow> u]]"
 proof (induct p arbitrary: s q)
   case (Cons i p)
   show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
     by (cases q; cases s) auto
 qed auto
 
 lemma replace_at_hole_pos [simp]: "C\<langle>s\<rangle>[hole_pos C \<leftarrow> t] = C\<langle>t\<rangle>"
   by (induct C) auto
 
 subsection \<open>Properties on @{const adapt_vars} and @{const adapt_vars_ctxt}\<close>
 
 lemma adapt_vars2:
   "adapt_vars (adapt_vars t) = adapt_vars t"
   by (induct t) (auto simp add: adapt_vars_def)
 
 lemma adapt_vars_simps[code, simp]: "adapt_vars (Fun f ts) = Fun f (map adapt_vars ts)"
   by (induct ts, auto simp: adapt_vars_def)
 
 lemma adapt_vars_reverse: "ground t \<Longrightarrow> adapt_vars t' = t \<Longrightarrow> adapt_vars t = t'"
   unfolding adapt_vars_def 
 proof (induct t arbitrary: t')
   case (Fun f ts)
   then show ?case by (cases t') (auto simp add: map_idI)
 qed auto
 
 lemma ground_adapt_vars [simp]: "ground (adapt_vars t) = ground t"
   by (simp add: adapt_vars_def)
 lemma funas_term_adapt_vars[simp]: "funas_term (adapt_vars t) = funas_term t" by (simp add: adapt_vars_def)
 
 lemma adapt_vars_adapt_vars[simp]: fixes t :: "('f,'v)term"
   assumes g: "ground t"
   shows "adapt_vars (adapt_vars t :: ('f,'w)term) = t"
 proof -
   let ?t' = "adapt_vars t :: ('f,'w)term"
   have gt': "ground ?t'" using g by auto
   from adapt_vars_reverse[OF gt', of t] show ?thesis by blast
 qed
 
 lemma adapt_vars_inj:
   assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
   shows "x = y"
   using adapt_vars_adapt_vars assms by metis
 
 lemma adapt_vars_ctxt_simps[simp, code]: 
   "adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"
   "adapt_vars_ctxt Hole = Hole" unfolding adapt_vars_ctxt_def adapt_vars_def by auto
 
 lemma adapt_vars_ctxt[simp]: "adapt_vars (C \<langle> t \<rangle> ) = (adapt_vars_ctxt C) \<langle> adapt_vars t \<rangle>"
   by (induct C, auto)
 
 lemma adapt_vars_subst[simp]: "adapt_vars (l \<cdot> \<sigma>) = l \<cdot> (\<lambda> x. adapt_vars (\<sigma> x))"
   unfolding adapt_vars_def
   by (induct l) auto
 
 lemma adapt_vars_gr_map_vars [simp]:
   "ground t \<Longrightarrow> map_vars_term f t = adapt_vars t"
   by (induct t) auto
 
 
 lemma adapt_vars_gr_ctxt_of_map_vars [simp]:
   "ground_ctxt C \<Longrightarrow> map_vars_ctxt f C = adapt_vars_ctxt C"
   by (induct C) auto
 
 subsubsection \<open>Equality on ground terms/contexts by positions and symbols\<close>
 
 lemma fun_at_def':
   "fun_at t p = (if p \<in> poss t then
     (case t |_ p of Var x \<Rightarrow> Some (Inr x) | Fun f ts \<Rightarrow> Some (Inl f)) else None)"
   by (induct t p rule: fun_at.induct) auto
 
 lemma fun_at_None_nposs_iff:
   "fun_at t p = None \<longleftrightarrow> p \<notin> poss t"
   by (auto simp: fun_at_def') (meson term.case_eq_if)
 
 lemma eq_term_by_poss_fun_at:
   assumes "poss s = poss t" "\<And>p. p \<in> poss s \<Longrightarrow> fun_at s p = fun_at t p"
   shows "s = t"
   using assms
 proof (induct s arbitrary: t)
   case (Var x) then show ?case
     by (cases t) simp_all
 next
   case (Fun f ss) note Fun' = this
   show ?case
   proof (cases t)
     case (Var x) show ?thesis using Fun'(3)[of "[]"] by (simp add: Var)
   next
     case (Fun g ts)
     have *: "length ss = length ts"
       using Fun'(3) arg_cong[OF Fun'(2), of "\<lambda>P. card {i |i p. i # p \<in> P}"]
       by (auto simp: Fun exI[of "\<lambda>x. x \<in> poss _", OF Nil_in_poss])
     then have "i < length ss \<Longrightarrow> poss (ss ! i) = poss (ts ! i)" for i
       using arg_cong[OF Fun'(2), of "\<lambda>P. {p. i # p \<in> P}"] by (auto simp: Fun)
     then show ?thesis using * Fun'(2) Fun'(3)[of "[]"] Fun'(3)[of "_ # _ :: pos"]
       by (auto simp: Fun intro!: nth_equalityI Fun'(1)[OF nth_mem, of n "ts ! n" for n])
   qed
 qed
 
 lemma eq_ctxt_at_pos_by_poss:
   assumes "p \<in> poss s" "p \<in> poss t"
     and "\<And> q. \<not> (p \<le>\<^sub>p q) \<Longrightarrow> q \<in> poss s \<longleftrightarrow> q \<in> poss t"
     and "(\<And> q. q \<in> poss s \<Longrightarrow> \<not> (p \<le>\<^sub>p q) \<Longrightarrow> fun_at s q = fun_at t q)"
   shows "ctxt_at_pos s p = ctxt_at_pos t p" using assms
 proof (induct p arbitrary: s t)
   case (Cons i p)
   from Cons(2, 3) Cons(4, 5)[of "[]"] obtain f ss ts where [simp]: "s = Fun f ss" "t = Fun f ts"
     by (cases s; cases t) auto
   have flt: "j < i \<Longrightarrow> j # q \<in> poss s \<Longrightarrow> fun_at s (j # q) = fun_at t (j # q)" for j q
     by (intro Cons(5)) auto
   have fgt: "i < j \<Longrightarrow> j # q \<in> poss s \<Longrightarrow> fun_at s (j # q) = fun_at t (j # q)" for j q
     by (intro Cons(5)) auto
   have lt: "j < i \<Longrightarrow> j # q \<in> poss s \<longleftrightarrow> j # q \<in> poss t" for j q by (intro Cons(4)) auto
   have gt: "i < j \<Longrightarrow> j # q \<in> poss s \<longleftrightarrow> j # q \<in> poss t" for j q by (intro Cons(4)) auto
   from this[of _ "[]"] have "i < j \<Longrightarrow> j < length ss \<longleftrightarrow> j < length ts" for j by auto
   from this Cons(2, 3) have l: "length ss = length ts" by auto (meson nat_neq_iff)
   have "ctxt_at_pos (ss ! i) p = ctxt_at_pos (ts ! i) p" using Cons(2, 3) Cons(4-)[of "i # q" for q] 
     by (intro Cons(1)[of "ss ! i" "ts ! i"]) auto
   moreover have "take i ss = take i ts" using l lt Cons(2, 3) flt
     by (intro nth_equalityI) (auto intro!: eq_term_by_poss_fun_at)
   moreover have "drop (Suc i) ss = drop (Suc i) ts" using l Cons(2, 3) fgt gt[of "Suc i + j" for j]
     by (intro nth_equalityI) (auto simp: nth_map intro!: eq_term_by_poss_fun_at, fastforce+)
   ultimately show ?case by auto
 qed auto
 
 
 subsection \<open>Misc\<close>
 
 lemma fun_at_hole_pos_ctxt_apply [simp]:
   "fun_at C\<langle>t\<rangle> (hole_pos C) = fun_at t []"
   by (induct C) auto
 
 lemma vars_term_ctxt_apply [simp]:
   "vars_term C\<langle>t\<rangle> = vars_ctxt C \<union> vars_term t"
   by (induct C arbitrary: t) auto
 
 lemma map_vars_term_ctxt_apply:
   "map_vars_term f C\<langle>t\<rangle> = (map_vars_ctxt f C)\<langle>map_vars_term f t\<rangle>"
   by (induct C) auto
 
 lemma map_term_replace_at_dist:
   "p \<in> poss s \<Longrightarrow> (map_term f g s)[p \<leftarrow> (map_term f g t)] = map_term f g (s[p \<leftarrow> t])"
 proof (induct p arbitrary: s)
   case (Cons i p) then show ?case
     by (cases s) (auto simp: nth_list_update intro!: nth_equalityI)
 qed auto
 
 end