(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*
Based on src/HOL/ex/Unification.thy packaged with Isabelle/HOL 2015 having the following license:

ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.

Copyright (c) 1986-2015,
  University of Cambridge,
  Technische Universitaet Muenchen,
  and contributors.

  All rights reserved.

Redistribution and use in source and binary forms, with or without 
modification, are permitted provided that the following conditions are 
met:

* Redistributions of source code must retain the above copyright 
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above copyright 
notice, this list of conditions and the following disclaimer in the 
documentation and/or other materials provided with the distribution.

* Neither the name of the University of Cambridge or the Technische
Universitaet Muenchen nor the names of their contributors may be used
to endorse or promote products derived from this software without
specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS 
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED 
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A 
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)


(*  Title:      Unification.thy
    Author:     Andreas Viktor Hess, DTU

    Originally based on src/HOL/ex/Unification.thy (Isabelle/HOL 2015) by:
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
    Author:     Alexander Krauss, TUM

    These theories depend on the IsaFoR library v2.27 (licensed under the LGPLv3) available at:
    http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/23ac5f5c26ed
    Download into the directory IsaFoR and move it to your Isabelle installation or change the path in the imports.
*)

section {* Theory: Substitution and Unification *}

theory Unification2
imports Messages
        "~~/IsaFoR/thys/Rewriting/Unification" (* Path to IsaFoR *)
begin

subsection {* Substitutions *}

abbreviation subst_more_general_than (infixl "\<preceq>\<^sub>\<circ>" 50) where
  "\<theta> \<preceq>\<^sub>\<circ> \<theta>' \<equiv> \<exists>\<gamma>. \<theta>' = \<theta> \<circ>\<^sub>s \<gamma>"

abbreviation subst_support (infix "supports" 50) where
  "\<theta> supports \<delta> \<equiv> (\<forall>x. \<theta> x \<cdot> \<delta> = \<delta> x)"

abbreviation rm_var where
  "rm_var v s \<equiv> s(v := Var v)"

abbreviation rm_vars where
  "rm_vars vs \<sigma> \<equiv> (\<lambda>v. if v \<in> vs then Var v else \<sigma> v)"

definition elim where
  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> FV (t \<cdot> \<sigma>)"

definition Idem where
  "Idem s \<equiv> s \<circ>\<^sub>s s = s"

declare elim_def[simp]

lemma subst_support_def: "\<theta> supports \<tau> \<longleftrightarrow> \<tau> = \<theta> \<circ>\<^sub>s \<tau>"
unfolding subst_compose_def by metis

lemma subst_supportD: "\<theta> supports \<delta> \<Longrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<delta>"
using assms subst_support_def by auto

lemma rm_vars_empty: "rm_vars {} s = s"
by simp

lemma rm_vars_singleton: "rm_vars {v} s = rm_var v s"
by auto

lemma var_subst_id: "t \<cdot> Var = t"
by (induct t) (auto simp add: map_idI)

lemma var_subst_id_set: "M \<cdot>set Var = M"
by simp

lemma subst_agreement: "(t \<cdot> r = t \<cdot> s) \<longleftrightarrow> (\<forall>v \<in> FV t. Var v \<cdot> r = Var v \<cdot> s)"
by (induct t) auto

lemma repl_invariance[dest?]: "v \<notin> FV t \<Longrightarrow> t \<cdot> s(v := u) = t \<cdot> s"
by (simp add: subst_agreement)

lemma subst_remove_var: "v \<notin> FV s \<Longrightarrow> v \<notin> FV (t \<cdot> Var(v := s))"
by (induct t) simp_all

lemma subst_set_map: "x \<in> set X \<Longrightarrow> x \<cdot> s \<in> set (map (\<lambda>x. x \<cdot> s) X)"
by simp

lemma subst_all_member: "x \<in> M \<Longrightarrow> x \<cdot> \<theta> \<in> (M \<cdot>set \<theta>)"
by simp

lemma subst_all_union: "(M \<union> N) \<cdot>set \<I> = (M \<cdot>set \<I>) \<union> (N \<cdot>set \<I>)"
by auto

lemma subst_allE:
  assumes "t \<in> M \<cdot>set s"
  obtains t' where "t' \<in> M" "t = t' \<cdot> s"
using assms by (rule imageE)

lemma subst_mono: "t \<sqsubseteq> u \<Longrightarrow> t \<cdot> s \<sqsubseteq> u \<cdot> s"
by (induct u) auto

lemma subst_mono_neq:
  assumes "t \<sqsubset> u"
  shows "t \<cdot> s \<sqsubset> u \<cdot> s"
proof (cases u)
  case (Var v)
  hence False using \<open>t \<sqsubset> u\<close> by simp
  thus ?thesis ..
next
  case (Fun f X)
  then obtain x where "x \<in> set X" "t \<sqsubseteq> x" using \<open>t \<sqsubset> u\<close> by auto
  hence "t \<cdot> s \<sqsubseteq> x \<cdot> s" using subst_mono by simp

  obtain Y where "Fun f X \<cdot> s = Fun f Y" by auto
  hence "x \<cdot> s \<in> set Y" using \<open>x \<in> set X\<close> by auto
  hence "x \<cdot> s \<sqsubset> Fun f X \<cdot> s" using \<open>Fun f X \<cdot> s = Fun f Y\<close> Fun_param_is_subterm by simp
  hence "t \<cdot> s \<sqsubset> Fun f X \<cdot> s" using \<open>t \<cdot> s \<sqsubseteq> x \<cdot> s\<close> by (metis subtermeq_subterm_trans)
  thus ?thesis using \<open>u = Fun f X\<close> \<open>t \<sqsubset> u\<close> by metis
qed

lemma subst_no_occs[dest]: "\<not>Var v \<sqsubseteq> t \<Longrightarrow> t \<cdot> Var(v := s) = t"
by (induct t) (simp_all add: map_idI)

lemma var_comp[simp]: "\<sigma> \<circ>\<^sub>s Var = \<sigma>" "Var \<circ>\<^sub>s \<sigma> = \<sigma>"
unfolding subst_compose_def by simp_all

lemma subst_comp[simp]: "t \<cdot> (r \<circ>\<^sub>s s) = t \<cdot> r \<cdot> s"
unfolding subst_compose_def by (induct t) auto

lemma subst_comp_all: "M \<cdot>set (\<delta> \<circ>\<^sub>s \<theta>) = (M \<cdot>set \<delta>) \<cdot>set \<theta>"
using subst_comp[of _ \<delta> \<theta>] by auto

lemma subst_all_mono: "M \<subseteq> M' \<Longrightarrow> M \<cdot>set s \<subseteq> M' \<cdot>set s"
by auto

lemma subst_ground_ident[dest?]: "FV t = {} \<Longrightarrow> t \<cdot> s = t"
by (induct t, simp, metis subst_agreement empty_iff var_subst_id)

lemma subst_all_ground_ident[dest?]: "ground M \<Longrightarrow> M \<cdot>set s = M"
proof -
  assume "ground M"
  hence "\<And>t. t \<in> M \<Longrightarrow> FV t = {}" unfolding ground_def FV\<^sub>s\<^sub>e\<^sub>t_def by auto
  hence "\<And>t. t \<in> M \<Longrightarrow> t \<cdot> s = t" by (metis subst_ground_ident)
  moreover have "\<And>t. t \<in> M \<Longrightarrow> t \<cdot> s \<in> M \<cdot>set s" by (metis subst_all_member)
  ultimately show "M \<cdot>set s = M" by (simp add: image_cong)
qed

lemma subst_eqI[intro]: "(\<And>t. t \<cdot> \<sigma> = t \<cdot> \<theta>) \<Longrightarrow> \<sigma> = \<theta>"
proof -
  assume "\<And>t. t \<cdot> \<sigma> = t \<cdot> \<theta>"
  hence "\<And>v. Var v \<cdot> \<sigma> = Var v \<cdot> \<theta>" by auto
  thus "\<sigma> = \<theta>" by auto
qed

lemma comp_assoc: "(a \<circ>\<^sub>s b) \<circ>\<^sub>s c = a \<circ>\<^sub>s (b \<circ>\<^sub>s c)"
by auto

lemma subst_cong: "\<lbrakk>\<sigma> = \<sigma>'; \<theta> = \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<circ>\<^sub>s \<theta>) = (\<sigma>' \<circ>\<^sub>s \<theta>')"
by auto

lemma subst_mgt_bot[simp]: "Var \<preceq>\<^sub>\<circ> \<theta>"
by simp

lemma subst_mgt_refl[simp]: "\<theta> \<preceq>\<^sub>\<circ> \<theta>"
by (metis var_comp(1))

lemma subst_mgt_trans: "\<lbrakk>\<theta> \<preceq>\<^sub>\<circ> \<delta>; \<delta> \<preceq>\<^sub>\<circ> \<sigma>\<rbrakk> \<Longrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<sigma>"
by (metis comp_assoc)

lemma subst_mgt_comp: "\<theta> \<preceq>\<^sub>\<circ> \<theta> \<circ>\<^sub>s \<delta>"
by auto

lemma subst_mgt_comp': "\<theta> \<circ>\<^sub>s \<delta> \<preceq>\<^sub>\<circ> \<sigma> \<Longrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<sigma>"
using comp_assoc by metis

lemma var_self: "(\<lambda>w. if w = v then Var v else Var w) = Var"
using subst_agreement by auto

lemma var_same[simp]: "Var(v := t) = Var \<longleftrightarrow> t = Var v"
by (intro iffI, metis fun_upd_same, simp add: var_self)

lemma subst_eq_if_eq_vars: "(\<And>v. (Var v) \<cdot> \<theta> = (Var v) \<cdot> \<sigma>) \<Longrightarrow> \<theta> = \<sigma>"
by (auto simp add: subst_agreement)

lemma subst_all_empty[simp]: "{} \<cdot>set \<theta> = {}"
by simp

lemma subst_all_insert:"(insert t M) \<cdot>set \<delta> = insert (t \<cdot> \<delta>) (M \<cdot>set \<delta>)"
by auto

lemma subst_apply_FV_subset: "FV t \<subseteq> V \<Longrightarrow> FV (t \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by (induct t) auto

lemma subst_apply_FV_unfold: "FV (t \<cdot> \<delta>) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV t)"
by (induct t) auto

lemma subst_apply_FV_unfold': "FV (t \<cdot> \<delta>) = (\<Union>v \<in> FV t. FV (\<delta> v))"
by (simp add: subst_apply_FV_unfold)

lemma subst_apply_FV_union: "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV (t \<cdot> \<delta>) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> FV t))"
proof -
  have "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> FV t)) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV t)" by auto
  thus ?thesis using subst_apply_FV_unfold by metis
qed

lemma elimI[intro]: "(\<And>t. v \<notin> FV (t \<cdot> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
by auto

lemma elim_intro'[intro]: "(\<And>w. v \<notin> FV (Var w \<cdot> \<theta>)) \<Longrightarrow> elim \<theta> v"
by (simp add: subst_apply_FV_unfold') 

lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> FV (t \<cdot> \<sigma>)"
by auto

lemma elim_dest'[dest]: "elim \<sigma> v \<Longrightarrow> \<sigma> v \<noteq> Var v"
by (metis elim_def subst_apply_term.simps(1) term.set_intros(3))

lemma elim_dest''[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> FV (\<sigma> w)"
by (metis elim_def subst_apply_term.simps(1))

lemma elim_rm_vars_dest[dest]: "elim (\<sigma>::('a,'b) subst) v \<Longrightarrow> v \<notin> vs \<Longrightarrow> elim (rm_vars vs \<sigma>) v"
proof -
  assume assms: "elim \<sigma> v" "v \<notin> vs"
  obtain f::"('a, 'b) subst \<Rightarrow> 'b \<Rightarrow> 'b" where
      "\<forall>\<sigma> v. (\<exists>w. v \<in> FV (Var w \<cdot> \<sigma>)) = (v \<in> FV (Var (f \<sigma> v) \<cdot> \<sigma>))"
    by moura
  hence *: "\<forall>a \<sigma>. a \<in> FV (Var (f \<sigma> a) \<cdot> \<sigma>) \<or> elim \<sigma> a" by blast
  have "Var (f (rm_vars vs \<sigma>) v) \<cdot> \<sigma> \<noteq> Var (f (rm_vars vs \<sigma>) v) \<cdot> rm_vars vs \<sigma>
        \<or> v \<notin> FV (Var (f (rm_vars vs \<sigma>) v) \<cdot> rm_vars vs \<sigma>)"
    using assms(1) by fastforce
  moreover
  { assume "Var (f (rm_vars vs \<sigma>) v) \<cdot> \<sigma> \<noteq> Var (f (rm_vars vs \<sigma>) v) \<cdot> rm_vars vs \<sigma>"
    hence "rm_vars vs \<sigma> (f (rm_vars vs \<sigma>) v) \<noteq> \<sigma> (f (rm_vars vs \<sigma>) v)" by auto
    hence "f (rm_vars vs \<sigma>) v \<in> vs" by meson
    hence ?thesis using * assms(2) by force
  }
  ultimately show ?thesis using * by blast
qed

lemma occs_elim: "\<not>Var v \<sqsubset> t \<Longrightarrow> elim (Var(v := t)) v \<or> (Var(v := t)) = Var"
proof (cases "Var v = t")
  assume "Var v \<noteq> t" "\<not>Var v \<sqsubset> t"
  hence "v \<notin> FV t" by (simp add: vars_iff_subterm_or_eq)
  thus ?thesis by (auto simp add: subst_remove_var)
qed auto

lemma occs_elim': "\<not>Var v \<sqsubseteq> t \<Longrightarrow> elim (Var(v := t)) v"
proof -
  assume "\<not>Var v \<sqsubseteq> t"
  hence "v \<notin> FV t" by (auto simp add: vars_iff_subterm_or_eq)
  thus "elim (Var(v := t)) v" by (simp add: subst_remove_var)
qed

lemma elim_comp: "elim \<theta> v \<Longrightarrow> elim (\<delta> \<circ>\<^sub>s \<theta>) v"
by auto

lemma var_Idem: "Idem Var"
by (simp add: Idem_def)

lemma var_upd_Idem:
  assumes "\<not>Var v \<sqsubseteq> t" shows "Idem (Var(v := t))"
unfolding Idem_def
proof
  let ?\<theta> = "Var(v := t)"
  from assms have t_\<theta>_id: "t \<cdot> ?\<theta> = t" by blast
  fix s show "s \<cdot> (?\<theta> \<circ>\<^sub>s ?\<theta>) = s \<cdot> ?\<theta>"
    unfolding subst_compose_def by (induction s, metis t_\<theta>_id fun_upd_def subst_apply_term.simps(1), simp) 
qed


subsection {* Domain and image of substitutions *}
definition dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \<Rightarrow> 'v set" where
  "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<equiv> {v. s v \<noteq> Var v}"

definition img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \<Rightarrow> ('f,'v) terms" where
  "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<equiv> s ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"

abbreviation FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('f,'v) subst \<Rightarrow> 'v set" where
  "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<equiv> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)"

declare dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def[simp]

lemma subst_dom_var_empty[simp]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var = {}" by simp
lemma subst_dom_var_finite[simp]: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var)" by simp

lemma finite_subst_img_if_finite_dom: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> finite (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma finite_subst_img_if_finite_dom': "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> finite (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_img_alt_def: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {t. \<exists>v. s v = t \<and> t \<noteq> Var v}" using img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_FV_img_alt_def: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = (\<Union>t \<in> {t. \<exists>v. s v = t \<and> t \<noteq> Var v}. FV t)"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_domI[intro]: "\<sigma> v \<noteq> Var v \<Longrightarrow> v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" by simp
lemma subst_imgI[intro]: "\<sigma> v \<noteq> Var v \<Longrightarrow> \<sigma> v \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
lemma subst_FV_imgI[intro]: "\<sigma> v \<noteq> Var v \<Longrightarrow> FV (\<sigma> v) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_FV_dom_img_subset: "FV t \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> FV (t \<cdot> \<theta>) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
by (induct t) auto

lemma subst_FV_dom_img_subset_set: "FV\<^sub>s\<^sub>e\<^sub>t M \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
proof -
  assume assms: "FV\<^sub>s\<^sub>e\<^sub>t M \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  obtain f::"'a set \<Rightarrow> (('b, 'a) term \<Rightarrow> 'a set) \<Rightarrow> ('b, 'a) terms \<Rightarrow> ('b, 'a) term" where
      "\<forall>x y z. (\<exists>v. v \<in> z \<and> \<not> y v \<subseteq> x) \<longleftrightarrow> (f x y z \<in> z \<and> \<not> y (f x y z) \<subseteq> x)"
    by moura
  hence *:
      "\<forall>T g A. (\<not> UNION T g \<subseteq> A \<or> (\<forall>t. t \<notin> T \<or> g t \<subseteq> A)) \<and>
               (UNION T g \<subseteq> A \<or> f A g T \<in> T \<and> \<not> g (f A g T) \<subseteq> A)"
    by (metis (no_types) SUP_le_iff)
  hence **: "\<forall>t. t \<notin> M \<or> FV t \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" by (metis (no_types) assms FV\<^sub>s\<^sub>e\<^sub>t_def)
  have "\<forall>t::('b, 'a) term. \<forall>f T. t \<notin> f ` T \<or> (\<exists>t'::('b, 'a) term. t = f t' \<and> t' \<in> T)" by blast
  hence "f (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) FV (M \<cdot>set \<theta>) \<notin> M \<cdot>set \<theta> \<or>
         FV (f (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) FV (M \<cdot>set \<theta>)) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    by (metis (full_types) ** subst_FV_dom_img_subset)
  thus ?thesis by (metis (no_types) * FV\<^sub>s\<^sub>e\<^sub>t_def)
qed

lemma subst_FV_dom_ground_if_ground_img:
  assumes "FV t \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)"
  shows "FV (t \<cdot> s) = {}"
using subst_FV_dom_img_subset[OF assms(1)] assms(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force

lemma subst_FV_dom_ground_if_ground_img':
  assumes "FV t \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "\<And>x. x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<Longrightarrow> FV (s x) = {}"
  shows "FV (t \<cdot> s) = {}"
using subst_FV_dom_ground_if_ground_img[OF assms(1)] assms(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto


lemma subst_FV_unfold: "FV (t \<cdot> s) = (FV t - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \<union> FV\<^sub>s\<^sub>e\<^sub>t (s ` (FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s))"
proof (induction t)
  case (Var v) thus ?case
  proof (cases "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s")
    case False
    hence "FV (Var v \<cdot> s) = {v}" "FV (Var v) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}" by auto
    thus ?thesis by auto
  qed auto
qed auto

lemma subst_FV_unfold_ground_img: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {} \<Longrightarrow> FV (t \<cdot> s) = FV t - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
using assms subst_FV_unfold[of t s] by auto

lemma subst_img_update:
  "\<lbrakk>\<sigma> v = Var v; t \<noteq> Var v\<rbrakk> \<Longrightarrow> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<union> FV t"
proof -
  assume "\<sigma> v = Var v" "t \<noteq> Var v"
  hence "(\<Union>s \<in> {s. \<exists>w. (\<sigma>(v := t)) w = s \<and> s \<noteq> Var w}. FV s) = FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  thus "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<union> FV t" by (metis Un_commute subst_FV_img_alt_def)
qed

lemma subst_dom_update1: "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := Var v)) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" by auto
lemma subst_dom_update2: "t \<noteq> Var v \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" by auto
lemma subst_dom_update3: "t = Var v \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> - {v}" by auto

lemma var_not_in_subst_dom[elim]: "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<Longrightarrow> s v = Var v" by simp
lemma subst_dom_vars_in_subst[elim]: "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<Longrightarrow> s v \<noteq> Var v" by simp

lemma subst_not_dom_fixed: "\<lbrakk>v \<in> FV t; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<rbrakk> \<Longrightarrow> v \<in> FV (t \<cdot> s)" by (induct t) auto

lemma subst_not_img_fixed: "\<lbrakk>v \<in> FV (t \<cdot> s); v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<rbrakk> \<Longrightarrow> v \<in> FV t" by (induct t) force+

lemma ground_subst_no_var[intro]: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \<Longrightarrow> x \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by simp

lemma subst_Var_notin_img: "x \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<Longrightarrow> t \<cdot> s = Var x \<Longrightarrow> t = Var x"
using subst_not_img_fixed[of x t s] by (induct t) auto

lemma FV_in_subst_img: "\<lbrakk>s v = t; t \<noteq> Var v\<rbrakk> \<Longrightarrow> FV t \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma empty_dom_iff_empty_subst: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<longleftrightarrow> \<theta> = Var" by auto

lemma subst_dom_cong: "(\<And>v t. \<theta> v = t \<Longrightarrow> \<delta> v = t) \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by auto

lemma subst_img_cong: "(\<And>v t. \<theta> v = t \<Longrightarrow> \<delta> v = t) \<Longrightarrow> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_dom_elim: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {} \<Longrightarrow> FV (t \<cdot> s) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}"
proof (induction t)
  case (Var v) thus ?case using FV_in_subst_img[of s] by (cases "s v = Var v") auto
qed auto

lemma subst_dom_insert_finite: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) = finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))"
proof
  assume "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)"
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)) \<subseteq> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" by auto
  thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))"
    by (meson \<open>finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)\<close> finite_insert rev_finite_subset)
next
  assume *: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (s(v := t)))"
  hence "finite (insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s))"
  proof (cases "t = Var v")
    case True
    hence "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s - {v})" by (metis * subst_dom_update3)
    thus ?thesis by simp
  qed (metis * subst_dom_update2[of t v s])
  thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" by simp
qed

lemma trm_subst_disj: "t \<cdot> \<theta> = t \<Longrightarrow> FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
proof (induction t)
  case (Fun f X)
  hence "map (\<lambda>x. x \<cdot> \<theta>) X = X" by simp
  hence "\<And>x. x \<in> set X \<Longrightarrow> x \<cdot> \<theta> = x" using map_eq_conv by fastforce
  thus ?case using Fun.IH by auto
qed simp

lemma trm_subst_ident[intro]: "FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<Longrightarrow> t \<cdot> \<theta> = t"
proof -
  assume "FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
  hence "\<forall>v \<in> FV t. \<forall>w \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. v \<noteq> w" by auto
  thus ?thesis by (metis subst_agreement subst_apply_term.simps(1) var_subst_id subst_domI)
qed

lemma trm_subst_ident'[intro]: "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> (Var v) \<cdot> \<theta> = Var v" using trm_subst_ident by simp

lemma trm_subst_ident''[intro]: "(\<And>x. x \<in> FV t \<Longrightarrow> \<theta> x = Var x) \<Longrightarrow> t \<cdot> \<theta> = t"
proof -
  assume "\<And>x. x \<in> FV t \<Longrightarrow> \<theta> x = Var x"
  hence "FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" by auto
  thus ?thesis using trm_subst_ident by auto
qed

lemma set_subst_ident: "FV\<^sub>s\<^sub>e\<^sub>t M \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<Longrightarrow> M \<cdot>set \<theta> = M"
proof -
  assume "FV\<^sub>s\<^sub>e\<^sub>t M \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
  hence "\<forall>t \<in> M. t \<cdot> \<theta> = t" unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by blast
  thus ?thesis by force
qed

lemma set_subst_all_ident: "FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {} \<Longrightarrow> M \<cdot>set (\<theta> \<circ>\<^sub>s \<delta>) = M \<cdot>set \<theta>"
by (metis set_subst_ident subst_comp_all)

lemma rm_vars_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s - V" by auto

lemma rm_vars_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) = s ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s)"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma rm_vars_img_subset: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) \<subseteq> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma rm_vars_apply: "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars V s) \<Longrightarrow> (rm_vars V s) v = s v"
by auto

lemma rm_vars_apply': "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> vs = {} \<Longrightarrow> rm_vars vs \<delta> = \<delta>"
by force

lemma rm_vars_ident: "FV t \<inter> vs = {} \<Longrightarrow> t \<cdot> (rm_vars vs \<theta>) = t \<cdot> \<theta>"
by (induct t) auto

lemma rm_vars_ground_supports:
  assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"
  shows "rm_vars X \<theta> supports \<theta>"
proof
  fix x
  have *: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<theta>))" using rm_vars_img_subset[of X \<theta>] assms by auto
  show "rm_vars X \<theta> x \<cdot> \<theta> = \<theta> x "
  proof (cases "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<theta>)")
    case True
    hence "FV (rm_vars X \<theta> x) = {}" using * unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    thus ?thesis using True by auto
  qed simp
qed

lemma subst_apply_dom_ident: "t \<cdot> \<theta> = t \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> t \<cdot> \<delta> = t"
proof (induction t)
  case (Fun f T) thus ?case by (induct T) auto
qed auto

lemma rm_vars_subst_apply_ident:
  assumes "t \<cdot> \<theta> = t"
  shows "t \<cdot> (rm_vars vs \<theta>) = t"
using rm_vars_dom[of vs \<theta>] subst_apply_dom_ident[OF assms, of "rm_vars vs \<theta>"] by auto

lemma rm_vars_comp:
  assumes "FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> vs = {}"
  shows "t \<cdot> rm_vars vs (\<delta> \<circ>\<^sub>s \<theta>) = t \<cdot> (rm_vars vs \<delta> \<circ>\<^sub>s rm_vars vs \<theta>)"
using assms
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x \<in> vs")
    case False
    have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars vs \<theta>) \<inter> vs = {}" by auto
    moreover have "FV (\<delta> x) \<inter> vs = {}" using Var False by force
    ultimately have "\<delta> x \<cdot> (rm_vars vs \<theta>) = \<delta> x \<cdot> \<theta>" using rm_vars_ident by simp
    moreover have "(rm_vars vs (\<delta> \<circ>\<^sub>s \<theta>)) x = (\<delta> \<circ>\<^sub>s \<theta>) x" by (metis False)
    ultimately show ?thesis using subst_compose by auto
  qed auto
qed auto

lemma disj_dom_img_var_notin:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" "\<theta> v = t" "t \<noteq> Var v"
  shows "v \<notin> FV t" "\<forall>v \<in> FV (t \<cdot> \<theta>). v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
proof -
  have "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "FV t \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
     using FV_in_subst_img[of \<theta> v t, OF assms(2)] assms(2,3) by simp_all
  thus "v \<notin> FV t" using assms(1) by auto

  have *: "FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" using assms(1) \<open>FV t \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> by auto
  hence "t \<cdot> \<theta> = t" by blast
  thus "\<forall>v \<in> FV (t \<cdot> \<theta>). v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using * by auto
qed

lemma subst_sends_dom_to_img: "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> FV (Var v \<cdot> \<theta>) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_sends_FV_to_img: "FV (t \<cdot> s) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
proof (induction t)
  case (Var v) thus ?case
  proof (cases "Var v \<cdot> s = Var v")
    case False
    hence "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by (meson trm_subst_ident') 
    hence "FV (Var v \<cdot> s) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" using subst_sends_dom_to_img by simp
    thus ?thesis by auto
  qed simp
qed auto

lemma ident_comp_subst_trm_if_disj:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  shows "(\<theta> \<circ>\<^sub>s \<sigma>) v = \<theta> v"
proof -
  from assms have " dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV (\<theta> v) = {}" using FV_in_subst_img by fastforce
  thus "(\<theta> \<circ>\<^sub>s \<sigma>) v = \<theta> v" unfolding subst_compose_def by blast
qed

lemma ident_comp_subst_trm_if_disj': "FV (\<theta> v) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {} \<Longrightarrow> (\<theta> \<circ>\<^sub>s \<sigma>) v = \<theta> v"
unfolding subst_compose_def by blast

lemma IdemI[intro]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {} \<Longrightarrow> Idem \<sigma>"
using ident_comp_subst_trm_if_disj[of \<sigma> \<sigma>]
      var_not_in_subst_dom[of _ \<sigma>]
      subst_eq_if_eq_vars[of \<sigma>]
by (metis Idem_def subst_compose_def var_comp(2)) 

lemma IdemI'[intro]: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> Idem \<sigma>"
unfolding ground_def by auto

lemma IdemE: "Idem \<sigma> \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}"
proof -
  assume "Idem \<sigma>"
  hence "\<And>v. FV (\<sigma> v) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}"
    unfolding Idem_def subst_compose_def by (metis trm_subst_disj)
  thus ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
qed

lemma Idem_rm_vars: "Idem \<theta> \<Longrightarrow> Idem (rm_vars X \<theta>)"
proof -
  assume "Idem \<theta>"
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" by (metis IdemE)
  moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<theta>) \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<theta>) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately show ?thesis by (fastforce intro!: IdemI)
qed

lemma subst_FV_bounded_if_img_bounded: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> FV t \<union> V \<Longrightarrow> FV (t \<cdot> \<theta>) \<subseteq> FV t \<union> V"
proof (induction t)
  case (Var v) thus ?case by (cases "\<theta> v = Var v") auto
qed (metis (no_types, lifting) Un_assoc Un_commute subst_sends_FV_to_img sup.absorb_iff2)

lemma subst_FV_bound_singleton: "FV (t \<cdot> Var(v := t')) \<subseteq> FV t \<union> FV t'"
using subst_FV_bounded_if_img_bounded[of "Var(v := t')" t "FV t'"] unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma subst_FV_bounded_if_img_bounded':
  assumes "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
  shows "FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
proof
  fix v assume *:  "v \<in> FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)"
  
  obtain t where t: "t \<in> M" "t \<cdot> \<theta> \<in> M \<cdot>set \<theta>" "v \<in> FV (t \<cdot> \<theta>)"
  proof -
    assume **: "\<And>t. \<lbrakk>t \<in> M; t \<cdot> \<theta> \<in> M \<cdot>set \<theta>; v \<in> FV (t \<cdot> \<theta>)\<rbrakk> \<Longrightarrow> thesis"
    have "v \<in> UNION ((\<lambda>t. t \<cdot> \<theta>) ` M) FV" using * unfolding FV\<^sub>s\<^sub>e\<^sub>t_def by metis
    hence "\<exists>t. t \<in> M \<and> v \<in> FV (t \<cdot> \<theta>)" by blast
    thus ?thesis using ** subst_all_member by blast
  qed

  from \<open>t \<in> M\<close> obtain M' where "t \<notin> M'" "M = insert t M'" by (meson Set.set_insert) 
  hence "FV\<^sub>s\<^sub>e\<^sub>t M = FV t \<union> FV\<^sub>s\<^sub>e\<^sub>t M'" by simp
  hence "FV (t \<cdot> \<theta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M" using subst_FV_bounded_if_img_bounded assms by simp
  thus "v \<in> FV\<^sub>s\<^sub>e\<^sub>t M" using assms \<open>v \<in> FV (t \<cdot> \<theta>)\<close> by auto
qed

lemma ground_img_if_ground_subst: "(\<And>v t. s v = t \<Longrightarrow> FV t = {}) \<Longrightarrow> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = {}"
unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma ground_subst_FV_subset: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<Longrightarrow> FV (t \<cdot> \<theta>) \<subseteq> FV t"
using subst_FV_bounded_if_img_bounded by fastforce

lemma ground_subst_FV_subset': "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<Longrightarrow> FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
using subst_FV_bounded_if_img_bounded'[of \<theta> M] unfolding ground_def by auto

lemma subst_to_var_is_var[elim]: "t \<cdot> s = Var v \<Longrightarrow> \<exists>w. t = Var w"
using subst_apply_term.elims by blast

lemma subst_dom_comp_subset[simp]: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2) \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2"
unfolding subst_compose_def by auto

lemma subst_dom_comp_eq:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}"
  shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
proof (rule ccontr)
  assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>) \<noteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>) \<subset> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    using subst_dom_comp_subset[of \<theta> \<sigma>] by simp
  then obtain v where "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>)" "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" by auto
  hence v_in_some_subst: "\<theta> v \<noteq> Var v \<or> \<sigma> v \<noteq> Var v" and "\<theta> v \<cdot> \<sigma> = Var v"
    unfolding subst_compose_def by auto
  then obtain w where "\<theta> v = Var w" using subst_to_var_is_var by fastforce
  show False
  proof (cases "v = w")
    case True
    hence "\<theta> v = Var v" using \<open>\<theta> v = Var w\<close> by simp
    hence "\<sigma> v \<noteq> Var v" using v_in_some_subst by simp
    thus False using \<open>\<theta> v = Var v\<close> \<open>\<theta> v \<cdot> \<sigma> = Var v\<close> by simp
  next
    case False
    hence "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using v_in_some_subst \<open>\<theta> v \<cdot> \<sigma> = Var v\<close> by auto 
    hence "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using assms by auto
    moreover have "\<sigma> w = Var v" using \<open>\<theta> v \<cdot> \<sigma> = Var v\<close> \<open>\<theta> v = Var w\<close> by simp
    hence "v \<in> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using \<open>v \<noteq> w\<close> subst_FV_imgI[of \<sigma> w] by simp
    ultimately show False ..
  qed
qed

lemma subst_img_comp_subset[simp]: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2"
proof
  let ?img = "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t"
  fix x assume "x \<in> ?img (\<theta>1 \<circ>\<^sub>s \<theta>2)"
  then obtain v t where vt: "x \<in> FV t" "t = (\<theta>1 \<circ>\<^sub>s \<theta>2) v" "t \<noteq> Var v" 
    unfolding subst_compose_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

  { assume "x \<notin> ?img \<theta>1" hence "x \<in> ?img \<theta>2"
      by (metis (no_types, hide_lams) FV_in_subst_img Un_iff subst_compose_def 
                vt subsetCE subst_apply_term.simps(1) subst_sends_FV_to_img) 
  }
  thus "x \<in> ?img \<theta>1 \<union> ?img \<theta>2" by auto
qed

lemma subst_img_comp_subset':
  assumes "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2)"
  shows "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 \<or> (\<exists>t' \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1. t = t' \<cdot> \<theta>2)"
proof -
  obtain x where x: "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2)" "(\<theta>1 \<circ>\<^sub>s \<theta>2) x = t" "t \<noteq> Var x"
    using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  { assume "x \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1"
    hence "(\<theta>1 \<circ>\<^sub>s \<theta>2) x = \<theta>2 x" unfolding subst_compose_def by auto
    hence ?thesis using x by auto
  } moreover {
    assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1" hence ?thesis using subst_compose x(2) by fastforce 
  } ultimately show ?thesis by metis
qed

lemma subst_img_comp_subset_const:
  assumes "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2)"
  shows "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 \<or> Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<or>
         (\<exists>x. Var x \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<and> \<theta>2 x = Fun c [])"
proof (cases "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2")
  case False
  then obtain t where t: "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1" "Fun c [] = t \<cdot> \<theta>2" 
    using subst_img_comp_subset'[OF assms] by auto
  thus ?thesis by (cases t) auto
qed (simp add: subst_img_comp_subset'[OF assms])

lemma subst_img_comp_subset_const':
  fixes \<delta> \<tau>::"('f,'v) subst"
  assumes "(\<delta> \<circ>\<^sub>s \<tau>) x = Fun c []"
  shows "\<delta> x = Fun c [] \<or> (\<exists>z. \<delta> x = Var z \<and> \<tau> z = Fun c [])"
proof (cases "\<delta> x = Fun c []")
  case False
  then obtain t where "\<delta> x = t" "t \<cdot> \<tau> = Fun c []" using assms unfolding subst_compose_def by auto
  thus ?thesis by (cases t) auto
qed simp

lemma subst_FV_dom_img_single:
  assumes "v \<notin> FV t" "\<sigma> v = t" "\<And>w. v \<noteq> w \<Longrightarrow> \<sigma> w = Var w"
  shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {v}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = FV t"
proof -
  show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {v}" using assms by fastforce
  have "FV t \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" by (metis FV_in_subst_img assms(1,2) vars_iff_subterm_or_eq) 
  moreover have "\<And>v. \<sigma> v \<noteq> Var v \<Longrightarrow> \<sigma> v = t" using assms by fastforce
  ultimately show "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = FV t" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
qed

lemma subst_comp_upd1: "\<theta>(v := t) \<circ>\<^sub>s \<sigma> = (\<theta> \<circ>\<^sub>s \<sigma>)(v := t \<cdot> \<sigma>)" unfolding subst_compose_def by auto
lemma subst_comp_upd2:
  assumes "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
  shows "s(v := t) = s \<circ>\<^sub>s (Var(v := t))"
unfolding subst_compose_def
proof -
  { fix w
    have "(s(v := t)) w = s w \<cdot> Var(v := t)"
    proof (cases "w = v")
      case True
      hence "s w = Var w" using \<open>v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<close> by simp
      thus ?thesis using \<open>w = v\<close> by simp
    next
      case False
      hence "(s(v := t)) w = s w" by simp
      moreover have "s w \<cdot> Var(v := t) = s w" using \<open>w \<noteq> v\<close> \<open>v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<close> 
        by (metis FV_in_subst_img fun_upd_apply insert_absorb insert_subset
                  repl_invariance subst_apply_term.simps(1) var_subst_id)
      ultimately show ?thesis ..
    qed
  }
  thus "s(v := t) = (\<lambda>w. s w \<cdot> Var(v := t))" by auto
qed

lemma ground_subst_dom_iff_img: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<longleftrightarrow> \<sigma> x \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
using assms by auto

lemma finite_dom_subst_exists:
  "finite S \<Longrightarrow> \<exists>\<sigma>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S"
proof (induction S rule: finite.induct)
  case (insertI A a)
  then obtain \<sigma>::"('f,'v) subst" where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = A" by blast
  fix f::'f
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(a := Fun f [])) = insert a A" using \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = A\<close> by auto
  thus ?case by metis
qed auto

lemma subst_inj_is_bij_betw_dom_img_if_ground_img:
  assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
  shows "inj \<sigma> \<longleftrightarrow> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" (is "?A \<longleftrightarrow> ?B")
proof
  show "?A \<Longrightarrow> ?B" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (meson bij_betw_def injD inj_onI) 
next
  assume ?B
  hence "inj_on \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" unfolding bij_betw_def by auto
  moreover have "\<And>x. x \<in> UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> \<sigma> x = Var x" by auto
  hence "inj_on \<sigma> (UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" using inj_onI[of "UNIV - dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"] by (metis term.inject(1))
  moreover have "\<And>x y. x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> y \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> \<sigma> x \<noteq> \<sigma> y"
    using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately show ?A by (metis injI inj_onD subst_domI term.inject(1))
qed

lemma bij_finite_ground_subst_exists:
  assumes "finite (S::'v set)" "infinite (U::('f,'v) term set)" "ground U"
  shows "\<exists>\<sigma>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                          \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                          \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> U"
proof -
  obtain T' where "T' \<subseteq> U" "card T' = card S" "finite T'"
    by (meson assms(2) finite_Diff2 infinite_arbitrarily_large)
  then obtain f::"'v \<Rightarrow> ('f,'v) term" where f_bij: "bij_betw f S T'"
    using finite_same_card_bij[OF assms(1)] by metis
  hence *: "\<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v" using \<open>ground U\<close> \<open>T' \<subseteq> U\<close> bij_betwE by fastforce

  let ?\<sigma> = "\<lambda>v. if v \<in> S then f v else Var v"
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S"
  proof
    show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> \<subseteq> S" by auto

    { fix v assume "v \<in> S" "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>"
      hence "f v = Var v" by simp
      hence False using *[OF \<open>v \<in> S\<close>] by metis
    }
    thus "S \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>" by blast
  qed
  hence "\<And>v w. \<lbrakk>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>; w \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>\<rbrakk> \<Longrightarrow> ?\<sigma> w \<noteq> ?\<sigma> v"
    using \<open>ground U\<close> bij_betwE[OF f_bij] set_rev_mp[OF _ \<open>T' \<subseteq> U\<close>]
    unfolding ground_def FV\<^sub>s\<^sub>e\<^sub>t_def
    by (metis (no_types, lifting) UN_iff empty_iff vars_iff_subterm_or_eq) 
  hence "inj_on ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    using f_bij \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S\<close>
    unfolding bij_betw_def inj_on_def
    by metis
  hence "bij_betw ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\<sigma>] by simp
  moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = T'"
    using \<open>bij_betw f S T'\<close> \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S\<close>
    unfolding bij_betw_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto 
  hence "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> \<subseteq> U" using \<open>T' \<subseteq> U\<close> by auto
  ultimately show ?thesis using \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S\<close> by (metis (lifting))
qed

lemma bij_finite_const_subst_exists:
  assumes "finite (S::'v set)" "finite (T::'f set)" "infinite (U::'f set)"
  shows "\<exists>\<sigma>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                          \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                          \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> (\<lambda>c. Fun c []) ` (U - T)"
proof -
  obtain T' where "T' \<subseteq> U - T" "card T' = card S" "finite T'"
    by (meson assms(2,3) finite_Diff2 infinite_arbitrarily_large)
  then obtain f::"'v \<Rightarrow> 'f" where f_bij: "bij_betw f S T'"
    using finite_same_card_bij[OF assms(1)] by metis

  let ?\<sigma> = "\<lambda>v. if v \<in> S then Fun (f v) [] else Var v"
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S" by simp
  moreover have "\<And>v w. \<lbrakk>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>; w \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>\<rbrakk> \<Longrightarrow> ?\<sigma> w \<noteq> ?\<sigma> v" by auto
  hence "inj_on ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    using f_bij unfolding bij_betw_def inj_on_def
    by (metis \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S\<close> term.inject(2))
  hence "bij_betw ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\<sigma>] by simp
  moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = ((\<lambda>c. Fun c []) ` T')"
    using \<open>bij_betw f S T'\<close> unfolding bij_betw_def inj_on_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  hence "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> \<subseteq> ((\<lambda>c. Fun c []) ` (U - T))" using \<open>T' \<subseteq> U - T\<close> by auto
  ultimately show ?thesis by (metis (lifting))
qed

lemma bij_finite_const_subst_exists':
  assumes "finite (S::'v set)" "finite (T::('f,'v) terms)" "infinite (U::'f set)"
  shows "\<exists>\<sigma>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                          \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                          \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) ` U) - T"
proof -
  have "finite (\<Union>(funs_term ` T))" using assms(2) by auto
  then obtain \<sigma> where \<sigma>:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S" "bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
      "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> (\<lambda>c. Fun c []) ` (U - (\<Union>(funs_term ` T)))"
    using bij_finite_const_subst_exists[OF assms(1) _ assms(3)] by blast
  moreover have "(\<lambda>c. Fun c []) ` (U - (\<Union>(funs_term ` T))) \<subseteq> ((\<lambda>c. Fun c []) ` U) - T" by auto
  ultimately show ?thesis by blast
qed

lemma bij_betw_countably_infinite:
  assumes "countable (S::'a set)" "infinite S"
  and     "countable (T::'b set)" "infinite T"
  obtains f::"'a \<Rightarrow> 'b" where "bij_betw f S T"
proof -
  have "bij_betw (to_nat_on S) S UNIV" by (fact to_nat_on_infinite[OF assms(1,2)])
  moreover have "bij_betw (from_nat_into T) UNIV T" by (fact bij_betw_from_nat_into[OF assms(3,4)])
  ultimately have "bij_betw (from_nat_into T \<circ> to_nat_on S) S T" by (simp add: bij_betw_trans)
  thus "(\<And>f. bij_betw f S T \<Longrightarrow> thesis) \<Longrightarrow> thesis" ..
qed

lemma bij_betw_iteI:
  assumes "bij_betw f A B" "bij_betw g C D" "A \<inter> C = {}" "B \<inter> D = {}"
  shows "bij_betw (\<lambda>x. if x \<in> A then f x else g x) (A \<union> C) (B \<union> D)"
proof -
  have "bij_betw (\<lambda>x. if x \<in> A then f x else g x) A B"
       "bij_betw (\<lambda>x. if x \<in> A then f x else g x) C D"
    apply (metis bij_betw_cong[of A f "\<lambda>x. if x \<in> A then f x else g x" B] assms(1))
    using bij_betw_cong[of C g "\<lambda>x. if x \<in> A then f x else g x" D] assms(2,3) by force
  thus ?thesis using bij_betw_combine[OF _ _ assms(4)] by metis
qed

lemma bij_countable_infinite_nonvar_subst_exists:
  assumes "countable (S::'v set)" "infinite S"
  and     "countable (T::('f,'v) term set)" "infinite T"
  and nonvar: "\<And>x. Var x \<notin> T"
  obtains \<sigma>::"('f,'v) subst"
  where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = T" "bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
proof -
  obtain f::"'v \<Rightarrow> ('f,'v) term" where f_bij: "bij_betw f S T"
    by (fact bij_betw_countably_infinite[OF assms(1,2,3,4)])
  hence f_nonvar: "\<And>x y. x \<in> S \<Longrightarrow> f x \<noteq> Var y" using nonvar unfolding bij_betw_def by force
 
  let ?\<sigma> = "\<lambda>v. if v \<in> S then f v else Var v"
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S" using f_nonvar by simp 
  moreover have "\<And>v w. \<lbrakk>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>; w \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>\<rbrakk> \<Longrightarrow> ?\<sigma> w \<noteq> ?\<sigma> v" using f_nonvar by auto
  hence "inj_on ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    using f_bij unfolding bij_betw_def inj_on_def by (metis \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = S\<close>)
  hence "bij_betw ?\<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma>)"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using inj_on_imp_bij_betw[of ?\<sigma>] by simp
  moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<sigma> = T"
    using f_bij f_nonvar unfolding bij_betw_def inj_on_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately show thesis using that by (metis (lifting))
qed

lemma bij_countable_infinite_const_subst_exists:
  assumes "countable (S::'v set)" "infinite S"
  and     "countable (T::'f set)" "infinite T"
  shows "\<exists>\<sigma>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                          \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                          \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = (\<lambda>c. Fun c []) ` T"
proof -
  from assms(3,4) have *: "countable ((\<lambda>c. Fun c []) ` T)" "infinite ((\<lambda>c. Fun c []) ` T)"
    using finite_imageD unfolding inj_on_def by (blast, auto)
  show ?thesis by (blast intro: bij_countable_infinite_nonvar_subst_exists[OF assms(1,2) *])
qed

lemma subst_comp_split:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
  shows "\<theta> = (rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> - V) \<theta>) \<circ>\<^sub>s (rm_vars V \<theta>)" (is ?P)
  and   "\<theta> = (rm_vars V \<theta>) \<circ>\<^sub>s (rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> - V) \<theta>)" (is ?Q)
proof -
  let ?rm1 = "rm_vars (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> - V) \<theta>" and ?rm2 = "rm_vars V \<theta>"
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 = {}"
       "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 = {}"
    using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
  hence *: "\<And>v. v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \<Longrightarrow> (?rm1 \<circ>\<^sub>s ?rm2) v = \<theta> v"
           "\<And>v. v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \<Longrightarrow> (?rm2 \<circ>\<^sub>s ?rm1) v = \<theta> v"
    using ident_comp_subst_trm_if_disj[of ?rm2 ?rm1]
          ident_comp_subst_trm_if_disj[of ?rm1 ?rm2]
    by auto
  hence "\<And>v. v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm1 \<Longrightarrow> (?rm1 \<circ>\<^sub>s ?rm2) v = \<theta> v"
        "\<And>v. v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?rm2 \<Longrightarrow> (?rm2 \<circ>\<^sub>s ?rm1) v = \<theta> v"
    unfolding subst_compose_def by auto
  hence "\<And>v. (?rm1 \<circ>\<^sub>s ?rm2) v = \<theta> v" "\<And>v. (?rm2 \<circ>\<^sub>s ?rm1) v = \<theta> v" using * by blast+
  thus ?P ?Q by auto
qed

lemma subst_comp_eq_if_disjoint_vars:
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) = {}"
  shows "\<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
proof -
  { fix x assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>"
    hence "(\<gamma> \<circ>\<^sub>s \<delta>) x = \<gamma> x" "(\<delta> \<circ>\<^sub>s \<gamma>) x = \<gamma> x"
      using assms by (force simp add: subst_compose)+
    hence "(\<gamma> \<circ>\<^sub>s \<delta>) x = (\<delta> \<circ>\<^sub>s \<gamma>) x" by metis
  } moreover
  { fix x assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    hence "(\<gamma> \<circ>\<^sub>s \<delta>) x = \<delta> x" "(\<delta> \<circ>\<^sub>s \<gamma>) x = \<delta> x"
      using assms by (auto simp add: subst_compose)
    hence "(\<gamma> \<circ>\<^sub>s \<delta>) x = (\<delta> \<circ>\<^sub>s \<gamma>) x" by metis
  } moreover
  { fix x assume "x \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>" "x \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    hence "(\<gamma> \<circ>\<^sub>s \<delta>) x = (\<delta> \<circ>\<^sub>s \<gamma>) x" by (simp add: subst_compose)
  } ultimately show ?thesis by auto
qed

lemma subst_eq_if_disjoint_vars_ground:
  fixes \<xi> \<delta>::"('f,'v) subst"
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<xi> = {}" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<xi>)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)" 
  shows "t \<cdot> \<delta> \<cdot> \<xi> = t \<cdot> \<xi> \<cdot> \<delta>"
by (metis assms ground_def subst_comp_eq_if_disjoint_vars
          subst_compose_apply_term_distrib sup_bot.right_neutral)

lemma subst_img_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t \<Longrightarrow> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV (t \<cdot> \<delta>)"
proof -
  assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t"
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t" by blast
  thus ?thesis
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by (metis (no_types) le_iff_sup subst_apply_FV_unfold subst_apply_FV_union)
qed

lemma subst_all_FV_subset: "FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> FV (t \<cdot> \<theta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)"
proof -
  assume *: "FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
  { fix v assume "v \<in> FV t"
    hence "v \<in> FV\<^sub>s\<^sub>e\<^sub>t M" using * by auto
    then obtain t' where "t' \<in> M" "v \<in> FV t'" by auto
    hence "FV (\<theta> v) \<subseteq> FV (t' \<cdot> \<theta>)"
      by (metis subst_apply_term.simps(1) subst_apply_FV_subset subst_apply_FV_unfold
                subtermeq_vars_subset vars_iff_subtermeq) 
    hence "FV (\<theta> v) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)" using \<open>t' \<in> M\<close> by auto
  }
  thus ?thesis by (auto simp add: subst_apply_FV_unfold)
qed

lemma subst_support_if_mgt_Idem:
  assumes "\<theta> \<preceq>\<^sub>\<circ> \<delta>" "Idem \<theta>"
  shows "\<theta> supports \<delta>"
proof -
  from \<open>\<theta> \<preceq>\<^sub>\<circ> \<delta>\<close> obtain \<sigma> where \<sigma>: "\<delta> = \<theta> \<circ>\<^sub>s \<sigma>" by blast
  hence "\<And>v. \<theta> v \<cdot> \<delta> = Var v \<cdot> (\<theta> \<circ>\<^sub>s \<theta> \<circ>\<^sub>s \<sigma>)" by simp
  hence "\<And>v. \<theta> v \<cdot> \<delta> = Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma>)" using \<open>Idem \<theta> \<close> unfolding Idem_def by simp
  hence "\<And>v. \<theta> v \<cdot> \<delta> = Var v \<cdot> \<delta>" using \<sigma> by simp
  thus "\<theta> supports \<delta>" by simp
qed

lemma subst_support_iff_mgt_if_Idem:
  assumes "Idem \<theta>"
  shows "\<theta> \<preceq>\<^sub>\<circ> \<delta> \<longleftrightarrow> \<theta> supports \<delta>"
proof
  show "\<theta> \<preceq>\<^sub>\<circ> \<delta> \<Longrightarrow> \<theta> supports \<delta>" by (fact subst_support_if_mgt_Idem[OF _ \<open>Idem \<theta>\<close>])
  show "\<theta> supports \<delta> \<Longrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<delta>" by (fact subst_supportD)
qed

lemma subst_support_comp:
  fixes \<theta> \<delta> \<I>::"('a,'b) subst"
  assumes "\<theta> supports \<I>" "\<delta> supports \<I>"
  shows "(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>"
by (metis (no_types) assms subst_agreement subst_apply_term.simps(1) subst_comp)

lemma subst_support_comp':
  fixes \<theta> \<delta> \<sigma>::"('a,'b) subst"
  assumes "\<theta> supports \<delta>"
  shows "\<theta> supports (\<delta> \<circ>\<^sub>s \<sigma>)" "\<sigma> supports \<delta> \<Longrightarrow> \<theta> supports (\<sigma> \<circ>\<^sub>s \<delta>)"
using assms unfolding subst_support_def by (metis comp_assoc, metis)

lemma subst_support_comp_split:
  fixes \<theta> \<delta> \<I>::"('a,'b) subst"
  assumes "(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>"
  shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<Longrightarrow> \<theta> supports \<I>"
  and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {} \<Longrightarrow> \<delta> supports \<I>"
proof -
  assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
  hence "Idem \<theta>" by (metis IdemI)
  have "\<theta> \<preceq>\<^sub>\<circ> \<I>" using assms comp_assoc[of \<theta> \<delta> \<I>] unfolding subst_compose_def by metis
  show "\<theta> supports \<I>" using subst_support_if_mgt_Idem[OF \<open>\<theta> \<preceq>\<^sub>\<circ> \<I>\<close> \<open>Idem \<theta>\<close>] by auto
next
  assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}"
  moreover have "\<forall>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>). (\<theta> \<circ>\<^sub>s \<delta>) v \<cdot> \<I> = \<I> v" using assms by metis
  ultimately have "\<forall>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>. \<delta> v \<cdot> \<I> = \<I> v"
    using var_not_in_subst_dom unfolding subst_compose_def
    by (metis IntI empty_iff subst_apply_term.simps(1))
  thus "\<delta> supports \<I>" by force
qed

lemma Idem_support: "Idem \<theta> \<Longrightarrow> \<theta> supports \<theta> \<circ>\<^sub>s \<delta>"
unfolding Idem_def by (metis subst_support_def comp_assoc)

lemma Idem_iff_self_support: "Idem \<theta> \<longleftrightarrow> \<theta> supports \<theta>"
using subst_support_def[of \<theta> \<theta>] unfolding Idem_def by auto

lemma subterm_subst_neq: "t \<sqsubset> t' \<Longrightarrow> t \<cdot> s \<noteq> t' \<cdot> s"
by (metis subst_mono_neq subterm_def)

lemma subterm_subst_unfold:
  assumes "t \<sqsubseteq> s \<cdot> \<theta>"
  shows "(\<exists>s'. s' \<sqsubseteq> s \<and> t = s' \<cdot> \<theta>) \<or> (\<exists>x \<in> FV s. t \<sqsubset> \<theta> x)"
using assms
proof (induction s)
  case (Fun f T) thus ?case
  proof (cases "t = Fun f T \<cdot> \<theta>")
    case True thus ?thesis using Fun by auto
  next
    case False
    then obtain s' where s': "s' \<in> set T" "t \<sqsubseteq> s' \<cdot> \<theta>" using Fun by auto
    hence "(\<exists>s''. s'' \<sqsubseteq> s' \<and> t = s'' \<cdot> \<theta>) \<or> (\<exists>x \<in> FV s'. t \<sqsubset> \<theta> x)" by (metis Fun.IH)
    thus ?thesis using s'(1) by auto
  qed
qed simp

lemma subterm_subst_img_subterm:
  assumes "t \<sqsubseteq> s \<cdot> \<theta>" "\<And>s'. s' \<sqsubseteq> s \<Longrightarrow> t \<noteq> s' \<cdot> \<theta>"
  shows "\<exists>w \<in> FV s. t \<sqsubset> \<theta> w"
using subterm_subst_unfold[OF assms(1)] assms(2) by force

lemma subterm_subst_not_img_subterm:
  assumes "t \<sqsubseteq> s \<cdot> \<I>" "\<not>(\<exists>w \<in> FV s. t \<sqsubseteq> \<I> w)"
  shows "\<exists>f T. Fun f T \<sqsubseteq> s \<and> t = Fun f T \<cdot> \<I>"
proof (rule ccontr)
  assume "\<not>(\<exists>f T. Fun f T \<sqsubseteq> s \<and> t = Fun f T \<cdot> \<I>)"
  hence "\<And>f T. Fun f T \<sqsubseteq> s \<Longrightarrow> t \<noteq> Fun f T \<cdot> \<I>" by simp
  moreover have "\<And>x. Var x \<sqsubseteq> s \<Longrightarrow> t \<noteq> Var x \<cdot> \<I>"
    using assms(2) vars_iff_subtermeq by force
  ultimately have "\<And>s'. s' \<sqsubseteq> s \<Longrightarrow> t \<noteq> s' \<cdot> \<I>" by (metis "term.exhaust")
  thus False using assms subterm_subst_img_subterm by force
qed

lemma subst_apply_img_var:
  assumes "v \<in> FV (t \<cdot> \<delta>)" "v \<notin> FV t"
  obtains w where "w \<in> FV t" "v \<in> FV (\<delta> w)"
using assms by (induct t) auto


subsection {* Finite Substitutions *}
inductive_set fsubst::"('a,'b) subst set" where
  FVar:     "Var \<in> fsubst"
| FUpdate:  "\<lbrakk>\<theta> \<in> fsubst; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; t \<noteq> Var v\<rbrakk> \<Longrightarrow> \<theta>(v := t) \<in> fsubst"

lemma finite_dom_iff_fsubst:
  "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<longleftrightarrow> \<theta> \<in> fsubst"
proof
  assume "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" thus "\<theta> \<in> fsubst"
  proof (induction "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" arbitrary: \<theta> rule: finite.induct)
    case emptyI
    hence "\<theta> = Var" using empty_dom_iff_empty_subst by metis
    thus ?case using FVar by simp
  next
    case (insertI \<theta>'\<^sub>d\<^sub>o\<^sub>m v) thus ?case
    proof (cases "v \<in> \<theta>'\<^sub>d\<^sub>o\<^sub>m")
      case True
      hence "\<theta>'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using \<open>insert v \<theta>'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> by auto
      thus ?thesis using insertI.hyps(2) by metis
    next
      case False
      let ?\<theta>' = "\<lambda>w. if w \<in> \<theta>'\<^sub>d\<^sub>o\<^sub>m then \<theta> w else Var w"
      have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<theta>' = \<theta>'\<^sub>d\<^sub>o\<^sub>m" using \<open>v \<notin> \<theta>'\<^sub>d\<^sub>o\<^sub>m\<close> \<open>insert v \<theta>'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> by auto
      hence "?\<theta>' \<in> fsubst" using insertI.hyps(2) by simp
      moreover have "?\<theta>'(v := \<theta> v) = (\<lambda>w. if w \<in> insert v \<theta>'\<^sub>d\<^sub>o\<^sub>m then \<theta> w else Var w)" by auto
      hence "?\<theta>'(v := \<theta> v) = \<theta>" using \<open>insert v \<theta>'\<^sub>d\<^sub>o\<^sub>m = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> by auto
      ultimately show ?thesis using FUpdate[of ?\<theta>' v "\<theta> v"] using False insertI.hyps(3) by auto 
    qed
  qed
next
  assume "\<theta> \<in> fsubst" thus "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"
  by (induct \<theta>, simp, metis subst_dom_insert_finite)
qed

lemma fsubst_induct[case_names FVar FUpdate, induct set: finite]:
  assumes "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)" "P Var"
  and "\<And>\<theta> v t. \<lbrakk>finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>); v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; t \<noteq> Var v; P \<theta>\<rbrakk> \<Longrightarrow> P (\<theta>(v := t))"
  shows "P \<delta>"
using assms finite_dom_iff_fsubst fsubst.induct by metis

lemma fun_upd_fsubst: "s(v := t) \<in> fsubst \<longleftrightarrow> s \<in> fsubst"
using subst_dom_insert_finite[of s] finite_dom_iff_fsubst by blast 

lemma finite_img_if_fsubst: "s \<in> fsubst \<Longrightarrow> finite (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)"
using finite_dom_iff_fsubst finite_subst_img_if_finite_dom' by blast


subsection {* Unifiers and Most General Unifiers *}

abbreviation Unifier::"('f,'v) subst \<Rightarrow> ('f,'v) term \<Rightarrow> ('f,'v) term \<Rightarrow> bool" where
  "Unifier \<sigma> t u \<equiv> (t \<cdot> \<sigma> = u \<cdot> \<sigma>)"

abbreviation MGU::"('f,'v) subst \<Rightarrow> ('f,'v) term \<Rightarrow> ('f,'v) term \<Rightarrow> bool" where
  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> \<sigma> \<preceq>\<^sub>\<circ> \<theta>)"

lemma MGUI[intro]:
  shows "\<lbrakk>t \<cdot> \<sigma> = u \<cdot> \<sigma>; \<And>\<theta>::('f,'v) subst. t \<cdot> \<theta> = u \<cdot> \<theta> \<Longrightarrow> \<sigma> \<preceq>\<^sub>\<circ> \<theta>\<rbrakk> \<Longrightarrow> MGU \<sigma> t u"
by auto

lemma UnifierD[dest]:
  fixes \<sigma>::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list"
  assumes "Unifier \<sigma> (Fun f X) (Fun g Y)"
  shows "f = g" "length X = length Y"
proof -
  from assms show "f = g" by auto

  from assms have "Fun f X \<cdot> \<sigma> = Fun g Y \<cdot> \<sigma>" by auto
  hence "length (map (\<lambda>x. x \<cdot> \<sigma>) X) = length (map (\<lambda>x. x \<cdot> \<sigma>) Y)" by auto
  thus "length X = length Y" by auto
qed

lemma UnifierD'[dest]:
  fixes \<sigma>::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list"
  assumes "Fun f X \<cdot> \<sigma> = Fun g Y \<cdot> \<sigma>"
  shows "f = g" "length X = length Y"
using assms UnifierD by simp_all

lemma MGUD[dest]:
  fixes \<sigma>::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list"
  assumes "MGU \<sigma> (Fun f X) (Fun g Y)"
  shows "f = g" "length X = length Y"
using assms by (auto intro!: UnifierD[of f X \<sigma> g Y])

lemma MGU_sym[sym]: "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s" by auto
lemma Unifier_sym[sym]: "Unifier \<sigma> s t \<Longrightarrow> Unifier \<sigma> t s" by auto

lemma MGU_nil: "MGU Var s t \<longleftrightarrow> s = t" by fastforce

lemma Unifier_comp: "Unifier (\<theta> \<circ>\<^sub>s \<delta>) t u \<Longrightarrow> Unifier \<delta> (t \<cdot> \<theta>) (u \<cdot> \<theta>)"
by simp

lemma Unifier_comp': "Unifier \<delta> (t \<cdot> \<theta>) (u \<cdot> \<theta>) \<Longrightarrow> Unifier (\<theta> \<circ>\<^sub>s \<delta>) t u"
by simp

lemma Unifier_excludes_subterm:
  assumes \<theta>: "Unifier \<theta> t u"
  shows "\<not>t \<sqsubset> u"
proof
  assume "t \<sqsubset> u"
  hence "t \<cdot> \<theta> \<sqsubset> u \<cdot> \<theta>" using subst_mono_neq by simp
  hence "t \<cdot> \<theta> \<noteq> u \<cdot> \<theta>" by simp
  moreover from \<theta> have "t \<cdot> \<theta> = u \<cdot> \<theta>" by auto
  ultimately show False ..
qed

lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u" by (rule conjunct1)

lemma MGU_Var1:
  assumes "\<not>Var v \<sqsubset> t"
  shows "MGU (Var(v := t)) (Var v) t"
proof (intro MGUI exI)
  show "Var v \<cdot> (Var(v := t)) = t \<cdot> (Var(v := t))" using assms subst_no_occs by fastforce
next
  fix \<theta>::"('a,'b) subst" assume th: "Var v \<cdot> \<theta> = t \<cdot> \<theta>" 
  show "\<theta> = (Var(v := t)) \<circ>\<^sub>s \<theta>" 
  proof
    fix s show "s \<cdot> \<theta> = s \<cdot> ((Var(v := t)) \<circ>\<^sub>s \<theta>)" using th by (induct s) auto
  qed
qed

lemma MGU_Var2: "v \<notin> FV t \<Longrightarrow> MGU (Var(v := t)) (Var v) t"
by (metis (no_types) MGU_Var1 vars_iff_subterm_or_eq)

lemma MGU_Var3: "MGU Var (Var v) (Var w) \<longleftrightarrow> v = w" by fastforce

lemma MGU_Const1: "MGU Var (Fun c []) (Fun d []) \<longleftrightarrow> c = d" by fastforce

lemma MGU_Const2: "MGU \<theta> (Fun c []) (Fun d []) \<Longrightarrow> c = d" by auto

lemma MGU_Fun:
  assumes "MGU \<theta> (Fun f X) (Fun g Y)"
  shows "f = g" "length X = length Y"
proof -
  let ?F = "\<lambda>\<theta> X. map (\<lambda>x. x \<cdot> \<theta>) X"
  from assms have
    "\<lbrakk>f = g; ?F \<theta> X = ?F \<theta> Y; \<forall>\<theta>'. f = g \<and> ?F \<theta>' X = ?F \<theta>' Y \<longrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<theta>'\<rbrakk> \<Longrightarrow> length X = length Y"
    using map_eq_imp_length_eq by auto
  thus "f = g" "length X = length Y" using assms by auto
qed

lemma Unifier_Fun:
  assumes "Unifier \<theta> (Fun f (x#X)) (Fun g (y#Y))"
  shows "Unifier \<theta> x y" "Unifier \<theta> (Fun f X) (Fun g Y)"
using assms by simp_all

lemma Unifier_Idem_subst: 
  "Idem r \<Longrightarrow> Unifier s (t \<cdot> r) (u \<cdot> r) \<Longrightarrow> Unifier (r \<circ>\<^sub>s s) (t \<cdot> r) (u \<cdot> r)"
by (metis (no_types, lifting) Idem_def subst_comp)

lemma Idem_comp:
  "Idem r \<Longrightarrow> Unifier s (t \<cdot> r) (u \<cdot> r) \<Longrightarrow> 
    (\<And>q. Unifier q (t \<cdot> r) (u \<cdot> r) \<Longrightarrow> s \<circ>\<^sub>s q = q) \<Longrightarrow>
    Idem (r \<circ>\<^sub>s s)"
by (frule Unifier_Idem_subst, blast, metis Idem_def comp_assoc)

lemma Unifier_mgt: "\<lbrakk>Unifier \<delta> t u; \<delta> \<preceq>\<^sub>\<circ> \<theta>\<rbrakk> \<Longrightarrow> Unifier \<theta> t u" by auto

lemma Unifier_support: "\<lbrakk>Unifier \<delta> t u; \<delta> supports \<theta>\<rbrakk> \<Longrightarrow> Unifier \<theta> t u"
using subst_supportD Unifier_mgt by metis

lemma MGU_mgt: "\<lbrakk>MGU \<sigma> t u; MGU \<delta> t u\<rbrakk> \<Longrightarrow> \<sigma> \<preceq>\<^sub>\<circ> \<delta>" by auto

lemma Unifier_trm_FV_bound:
  "\<lbrakk>Unifier s t u; v \<in> FV t\<rbrakk> \<Longrightarrow> v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<union> FV u"
proof (induction t arbitrary: s u)
  case Var thus ?case
    by (metis UnI1 UnI2 subsetCE no_var_subterm subst_sends_dom_to_img
              subst_to_var_is_var trm_subst_ident' vars_iff_subterm_or_eq)
next
  case (Fun f X)
  hence "v \<in> FV (u \<cdot> s) \<or> v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by (metis subst_not_dom_fixed)
  thus ?case by (metis (no_types) Un_iff contra_subsetD subst_sends_FV_to_img)
qed

lemma Unifier_rm_var: "\<lbrakk>Unifier \<theta> s t; v \<notin> FV s \<union> FV t\<rbrakk> \<Longrightarrow> Unifier (rm_var v \<theta>) s t"
using assms by (auto simp add: repl_invariance)

lemma Unifier_ground_rm_vars:
  assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" "Unifier (rm_vars X s) t t'"
  shows "Unifier s t t'"
by (rule Unifier_support[OF assms(2) rm_vars_ground_supports[OF assms(1)]])

lemma Unifier_dom_restrict:
  assumes "Unifier s t t'" "FV t \<union> FV t' \<subseteq> S"
  shows "Unifier (rm_vars (UNIV - S) s) t t'"
proof -
  let ?s = "rm_vars (UNIV - S) s"
  show ?thesis using term_subst_eq_conv[of t s ?s] term_subst_eq_conv[of t' s ?s] assms by auto
qed


subsection {* Term positions and substitutions *}
lemma subst_Fun_index_eq:
  assumes "i < length T" "Fun f T \<cdot> \<delta> = Fun g T' \<cdot> \<delta>"
  shows "T ! i \<cdot> \<delta> = T' ! i \<cdot> \<delta>"
proof -
  have "map (\<lambda>x. x \<cdot> \<delta>) T = map (\<lambda>x. x \<cdot> \<delta>) T'" using assms by simp
  thus ?thesis by (metis assms(1) length_map nth_map)
qed

lemma poss_unified_iff_unifiable:
  fixes t t'::"('a,'b) term" and \<delta>::"('a,'b) subst"
  shows "t \<cdot> \<delta> = t' \<cdot> \<delta> \<longleftrightarrow> (\<forall>p \<in> poss t \<inter> poss t'. (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>)"
proof
  { fix p assume "p \<in> poss t \<inter> poss t'" hence "t \<cdot> \<delta> = t' \<cdot> \<delta> \<Longrightarrow> t |_ p \<cdot> \<delta> = t' |_ p \<cdot> \<delta>"
    proof (induction p arbitrary: t t')
      case (PCons i p)
      hence *: "i <# p \<in> poss t" "i <# p \<in> poss t'" by auto
      from *(1) obtain f T where t_fun: "t = Fun f T" by (cases t) auto
      from *(2) obtain g S where t'_fun: "t' = Fun g S" by (cases t') auto
    
      have "t |_ <i> = T ! i" "t' |_ <i> = S ! i" by (auto simp add: t'_fun t_fun)
      hence "t |_ <i> \<cdot> \<delta> = t' |_ <i> \<cdot> \<delta>"
        by (metis * PCons.prems(1) empty_pos_in_poss poss_PCons_poss subt_at_subst) 
      moreover have "p \<in> poss (t |_ <i>)" "p \<in> poss (t' |_ <i>)" using * poss_cons_param by metis+
      ultimately have "(t |_ <i>) |_ p \<cdot> \<delta> = (t' |_ <i>) |_ p \<cdot> \<delta>" using PCons.IH by blast
      thus ?case by (simp add: t'_fun t_fun)
    qed simp
  }
  thus "t \<cdot> \<delta> = t' \<cdot> \<delta> \<Longrightarrow> (\<forall>p \<in> poss t \<inter> poss t'. (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>)" by auto

  show "(\<forall>p \<in> poss t \<inter> poss t'. (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>) \<Longrightarrow> t \<cdot> \<delta> = t' \<cdot> \<delta>"
    by (metis Int_iff empty_pos_in_poss subt_at.simps(1))
qed

lemma varposs_unified_if_unifiable:
  fixes t t'::"('a,'b) term" and \<delta>::"('a,'b) subst"
  assumes "t \<cdot> \<delta> = t' \<cdot> \<delta>"
  shows "\<forall>p \<in> (varposs t \<inter> poss t') \<union> (poss t \<inter> varposs t'). (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>"
using assms poss_unified_iff_unifiable[of t \<delta> t'] varposs_imp_poss by auto

lemma varposs_funposs_unified_iff_unifiable:
  fixes t t'::"('a,'b) term" and \<delta>::"('a,'b) subst"
  shows "t \<cdot> \<delta> = t' \<cdot> \<delta> \<longleftrightarrow> (
    (\<forall>p \<in> (varposs t \<inter> poss t') \<union> (poss t \<inter> varposs t'). (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>) \<and>
    (\<forall>p \<in> funposs t \<inter> funposs t'. (t |_ p) \<cdot> \<delta> = (t' |_ p) \<cdot> \<delta>))"
by (metis IntE IntI UnCI Un_iff funposs_imp_poss poss_simps(1) poss_unified_iff_unifiable)

lemma poss_neq_if_poss_neq_subst:
  assumes "t \<cdot> s |_ p \<noteq> t' \<cdot> s |_ p"
  obtains p' where "p' \<in> poss t \<inter> poss t'" "t |_ p' \<noteq> t' |_ p'"
by (metis assms poss_unified_iff_unifiable subst_apply_term_empty)

lemma subst_neq_if_varposs_neq:
  fixes t t'::"('a,'b) term" and \<delta>::"('a,'b) subst"
  assumes "p \<in> poss t \<inter> poss t'" "t |_ p = Var x" "t |_ p \<cdot> \<delta> \<noteq> t' |_ p \<cdot> \<delta>"
  shows "t \<cdot> \<delta> \<noteq> t' \<cdot> \<delta>"
proof -
  have "p \<in> varposs t \<inter> poss t'" using assms(1,2) varposs_iff by auto
  thus ?thesis using varposs_unified_if_unifiable[of t \<delta> t'] assms(3) by auto
qed

lemma FV_exists_if_unifiable_and_neq:
  fixes t t'::"('a,'b) term" and \<delta> \<theta>::"('a,'b) subst"
  assumes "t \<noteq> t'" "t \<cdot> \<theta> = t' \<cdot> \<theta>"
  shows "FV t \<union> FV t' \<noteq> {}"
proof
  assume "FV t \<union> FV t' = {}"
  hence "FV t = {}" "FV t' = {}" by auto
  hence "t \<cdot> \<theta> = t" "t' \<cdot> \<theta> = t'" by auto
  hence "t = t'" using assms(2) by metis
  thus False using assms(1) by auto
qed

lemma poss_funs_ident_if_unifiable:
  fixes t t'::"('a,'b) term" and \<delta>::"('a,'b) subst" and p::pos
  assumes "t \<cdot> \<delta> = t' \<cdot> \<delta>" "p \<in> poss t \<inter> poss t'" "t |_p = Fun f T" "t |_p = Fun g S"
  shows "f = g" "length T = length S"
using assms poss_unified_iff_unifiable by auto

lemma term_eq_if_varposs_poss_eq:
  fixes t t'::"('a,'b) term" and \<theta>::"('a,'b) subst"
  assumes "\<forall>p \<in> (varposs t \<inter> poss t') \<union> (poss t \<inter> varposs t'). (t |_ p) = (t' |_ p)"
  and "t \<cdot> \<theta> = t' \<cdot> \<theta>"
  shows "t = t'"
using assms
proof (induction t arbitrary: t')
  case (Fun f T t')
  let ?S = "\<lambda>t t'. (varposs t \<inter> poss t') \<union> (poss t \<inter> varposs t')"
  note IH = Fun.IH
  note prems = Fun.prems
  thus ?case
  proof (cases t')
    case (Fun g S)
    hence *: "f = g" "length S = length T" "Fun f T \<cdot> \<theta> = Fun g S \<cdot> \<theta>"
      using prems UnifierD[of f T \<theta> g S] by metis+
    hence "map (\<lambda>t. t \<cdot> \<theta>) T = map (\<lambda>t. t \<cdot> \<theta>) S" by auto
    with * have **:
        "\<And>i. i < length T \<Longrightarrow> (Fun f T |_ <i>) \<cdot> \<theta> =  (Fun g S |_ <i>) \<cdot> \<theta>"
        "\<And>i. i < length T \<Longrightarrow> (T ! i) \<cdot> \<theta> =  (S ! i) \<cdot> \<theta>"
      using map_nth_conv by force+
    from * have "\<And>i p. i < length T \<Longrightarrow> p \<in> ?S (Fun f T |_ <i>) (Fun g S |_ <i>)
              \<Longrightarrow> i<#p \<in> ?S (Fun f T) (Fun g S)"
      by auto
    with Fun prems(1) have ***: "\<And>i. i < length T \<Longrightarrow>
            \<forall>p \<in> ?S (Fun f T |_ <i>) (Fun g S |_ <i>).
              Fun f T |_ (i<#p) = Fun g S |_ (i<#p)"
      by blast
    have "\<And>i. i < length T \<Longrightarrow> Fun f T |_ <i> = Fun g S |_ <i>"
      using IH * ** *** by force
    thus ?thesis using Fun * by (simp add: nth_equalityI)
  qed auto
qed auto

lemma inj_const_subst_neq_aux:
  assumes "inj_on \<sigma> (FV (Var x) \<union> FV t)" "Var x \<noteq> t"
          "\<forall>s \<in> subterms (Var x) \<union> subterms t. s \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
          "\<forall>s \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. \<exists>c. s = Fun c []"
  shows "Var x \<cdot> \<sigma> \<noteq> t \<cdot> \<sigma>"
using assms
proof (cases t)
  case (Fun f T)
  hence *: "Fun f T \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using assms by auto
  show ?thesis
  proof (cases "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>")
    case True
    then obtain c where c: "Var x \<cdot> \<sigma> = Fun c []" "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
      using Fun assms(4) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    hence "Fun c [] \<noteq> Fun f T \<cdot> \<sigma>" using * by auto
    thus ?thesis by (metis Fun c(1))
  qed (auto simp add: Fun)
qed simp

lemma inj_const_subst_neq:
  assumes "inj_on \<sigma> (FV t \<union> FV t')" "t \<noteq> t'"
          "\<forall>s \<in> subterms t \<union> subterms t'. s \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
          "\<forall>s \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. \<exists>c. s = Fun c []"
  shows "t \<cdot> \<sigma> \<noteq> t' \<cdot> \<sigma>"
proof -
  { fix p assume p: "p \<in> (varposs t \<inter> poss t') \<union> (poss t \<inter> varposs t')" "t |_ p \<noteq> t' |_ p"
    then obtain x where x: "t |_ p = Var x \<or> t' |_ p = Var x" by (meson Int_iff UnE varposs_iff)
    have subt: "t |_ p \<sqsubseteq> t" "t' |_ p \<sqsubseteq> t'"
      using p(1) poss_is_subtermeq varposs_imp_poss by auto
    hence "FV (t |_ p) \<union> FV (t' |_ p) \<subseteq> FV t \<union> FV t'"
          "subterms (t |_ p) \<union> subterms (t' |_ p) \<subseteq> subterms t \<union> subterms t'"
      using subterms_subset subtermeq_vars_subset by fastforce+
    hence *: "inj_on \<sigma> (FV (t |_ p) \<union> FV (t' |_ p))"
             "\<forall>s \<in> subterms (t |_ p) \<union> subterms (t' |_ p). s \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
      using assms(1,3) unfolding inj_on_def by blast+
    have "t |_ p \<cdot> \<sigma> \<noteq> t' |_ p \<cdot> \<sigma>" using x
    proof
      assume **: "t |_ p = Var x"
      hence "inj_on \<sigma> (FV (Var x) \<union> FV (t' |_ p))" "Var x \<noteq> t' |_ p"
            "\<forall>s \<in> subterms (Var x) \<union> subterms (t' |_ p). s \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
        using * p(2) by simp_all
      thus "t |_ p \<cdot> \<sigma> \<noteq> t' |_ p \<cdot> \<sigma>" using inj_const_subst_neq_aux[OF _ _ _ assms(4)] ** by metis
    next
      assume **: "t' |_ p = Var x"
      hence "inj_on \<sigma> (FV (Var x) \<union> FV (t |_ p))" "Var x \<noteq> t |_ p"
            "\<forall>s \<in> subterms (Var x) \<union> subterms (t |_ p). s \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
        using * p(2) by simp_all
      thus "t |_ p \<cdot> \<sigma> \<noteq> t' |_ p \<cdot> \<sigma>" using inj_const_subst_neq_aux[OF _ _ _ assms(4)] ** by metis
    qed
    hence ?thesis using p(1) varposs_unified_if_unifiable[of t \<sigma> t'] by auto
  }
  thus ?thesis using term_eq_if_varposs_poss_eq[of t t' \<sigma>] assms(2) by auto
qed

lemma varposs_ground_empty: assumes "FV t = {}" shows "varposs t = {}"
using assms by (induct t) auto

lemma varposs_poss_ground_subst_subset:
  "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s) \<Longrightarrow> varposs (t \<cdot> s) \<inter> poss (t \<cdot> s) \<subseteq> varposs t \<inter> poss t"
using assms varposs_ground_empty by (induct t rule: varposs.induct) fastforce+

lemma varposs_ground_subst_subset: assumes "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s)" shows "varposs (t \<cdot> s) \<subseteq> varposs t"
proof (induction t rule: varposs.induct)
  case (1 x) thus ?case
  proof (cases "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s")
    case True thus ?thesis using assms varposs_ground_empty by fastforce
  qed simp
qed auto

lemma subt_at_subst':
  assumes "p \<in> poss t \<inter> poss t'" "t \<cdot> s = t' \<cdot> s" shows "t |_ p \<cdot> s = t' |_ p \<cdot> s"
using assms subt_at_subst[of p t s] subt_at_subst[of p t' s] by simp

lemma poss_subst_var:
  assumes "p \<in> poss (t \<cdot> s)" "t \<cdot> s  |_ p = Var x" "x \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
  shows "p \<in> poss t"
using assms(1,2)
proof (induction t arbitrary: p rule: poss.induct)
  case (1 y p) thus ?case using assms(3) subst_FV_imgI vars_term_subt_at by fastforce
next
  case (2 f T p)
  then obtain i p' where *: "p = i <# p'" "i < length T" by auto
  hence **: "p' \<in> poss (T ! i \<cdot> s)" "T ! i \<cdot> s |_ p' = Var x" using 2 by fastforce+
  have IH: "p' \<in> poss (T ! i)" by (rule "2.IH"[OF * **])
  thus ?case using * by auto
qed

lemma preordered_finite_set_has_maxima:
  assumes "finite A" "A \<noteq> {}"
  shows "\<exists>a::'a::{preorder} \<in> A. \<forall>b \<in> A. \<not>(a < b)"
using assms 
proof (induction A rule: finite_induct)
  case (insert a A) thus ?case
    by (cases "A = {}", simp, metis insert_iff order_trans less_le_not_le)
qed simp

lemma pos_deep_neq_if_term_neq:
  fixes t t'::"('f,'v) term"
  assumes "t \<noteq> t'"
  obtains p where
    "p \<in> poss t \<inter> poss t'" "t |_ p \<noteq> t' |_ p"
    "\<forall>p' \<in> poss t \<inter> poss t'. p < p' \<longrightarrow> t |_ p' = t' |_ p'"
proof -
  { fix Q M
    let ?P = "\<lambda>M p. \<forall>p' \<in> M. p < p' \<longrightarrow> t |_ p' = t' |_ p'"
    assume Q: "Q = (\<exists>p \<in> poss t \<inter> poss t'. t |_ p \<noteq> t' |_ p \<and> ?P (poss t \<inter> poss t') p)"
    assume M[simp]: "M = {p \<in> poss t \<inter> poss t'. t |_ p \<noteq> t' |_ p}"
    have "Q" 
    proof (rule ccontr)
      assume "\<not>Q"
      hence "\<forall>p \<in> M. \<exists>p' \<in> M. p < p'" using Q by auto
      moreover have "finite M" by simp
      moreover have "\<epsilon> \<in> M" using assms(1) by simp
      hence "M \<noteq> {}" by fastforce
      ultimately show False using preordered_finite_set_has_maxima by metis
    qed
  }
  thus ?thesis by (metis that)
qed

lemma const_subst_poss_eq:
  assumes "\<forall>s \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<exists>c. s = Fun c []"
  shows "poss t = poss (t \<cdot> \<theta>)"
proof (induction t)
  case (Var x) show ?case
  proof (cases "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>")
    case True
    then obtain c where "\<theta> x = Fun c []" using assms by auto
    thus ?thesis by auto
  qed auto
qed auto


subsection {* Well-formedness of substitutions and unifiers *}
inductive_set wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set::"('a,'b) subst set" where
  Empty[simp]: "Var \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set"
| Insert[simp]:
    "\<lbrakk>\<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>;
      v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; FV t \<inter> (insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)) = {}\<rbrakk>
      \<Longrightarrow> \<theta>(v := t) \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set"

definition wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('a,'b) subst \<Rightarrow> bool" where
  "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<equiv> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<and> finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"

definition wf\<^sub>M\<^sub>G\<^sub>U::"('a,'b) subst \<Rightarrow> ('a,'b) term \<Rightarrow> ('a,'b) term \<Rightarrow> bool" where
  "wf\<^sub>M\<^sub>G\<^sub>U \<theta> s t \<equiv> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> MGU \<theta> s t \<and> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> FV s \<union> FV t"

declare wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def[simp] wf\<^sub>M\<^sub>G\<^sub>U_def[simp]

lemma wf_subst_Idem: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> Idem \<theta>" using IdemI by auto

lemma wf_subst_properties: "\<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set = wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
proof
  show "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> \<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
  proof -
    assume "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {} \<and> finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"
    hence "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" by auto
    thus "\<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set"
    proof (induction \<theta> rule: fsubst_induct)
      case (FUpdate \<delta> v t)
      have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta>(v := t))" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta>(v := t))"
        using FUpdate.hyps(2,3) subst_img_update by fastforce+
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" using FUpdate.prems(1) by blast
      hence "\<delta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set" using FUpdate.IH by metis

      have *: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta>(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV t"
        using FUpdate.hyps(2) subst_img_update[OF _ FUpdate.hyps(3)] by fastforce
      hence "FV t \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
        using FUpdate.prems subst_dom_update2[OF FUpdate.hyps(3)] by blast
      moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta>(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
        by (meson FUpdate.hyps(3) subst_dom_update2)
      hence "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using FUpdate.prems * by blast
      ultimately show ?case using Insert[OF \<open>\<delta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set\<close> \<open>v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>] by metis
    qed simp
  qed

  show "\<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set \<Longrightarrow> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
  proof (induction \<theta> rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.induct)
    case (Insert \<sigma> v t)
    hence 1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}" by simp
    hence 2: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}" using Insert.hyps(3) by auto
    have 3: "FV t \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = {}" using Insert.hyps(4) by auto
    have 4: "\<sigma> v = Var v" using \<open>v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>\<close> by simp
  
    from Insert.IH have "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" by simp
    hence 5: "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)))" using subst_dom_insert_finite[of \<sigma>] by simp
  
    have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = {}"
    proof (cases "t = Var v")
      case True
      hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
        using 4 fun_upd_triv term.inject(1) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto 
      thus "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = {}" using 1 2 3 by auto
    next
      case False
      hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = FV t \<union> (FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
        using 4 subst_img_update[of \<sigma> v] by auto
      thus "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>(v := t)) = {}" using 1 2 3 by blast
    qed
    thus ?case using 5 unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
  qed simp
qed

lemma wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct[consumes 1, case_names Empty Insert]:
  assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "P Var"
  and "\<And>\<theta> v t. \<lbrakk>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; P \<theta>; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>;
                FV t \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) = {}\<rbrakk>
                \<Longrightarrow> P (\<theta>(v := t))"
  shows "P \<delta>"
proof -
  from assms(1,3) wf_subst_properties have
    "\<delta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set"
    "\<And>\<theta> v t. \<lbrakk>\<theta> \<in> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set; P \<theta>; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>; v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>;
              FV t \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) = {}\<rbrakk>
              \<Longrightarrow> P (\<theta>(v := t))"
    by blast+
  thus "P \<delta>" using wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.induct assms(2) by blast
qed  

lemma wf_subst_fsubst: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> \<delta> \<in> fsubst"
unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using finite_dom_iff_fsubst by blast 

lemma wf_subst_nil: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" by simp

lemma wf_MGU_nil: "MGU Var s t \<Longrightarrow> wf\<^sub>M\<^sub>G\<^sub>U Var s t"
using subst_FV_img_alt_def[of Var] by fastforce

lemma wf_MGU_dom_bound: "wf\<^sub>M\<^sub>G\<^sub>U \<theta> s t \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> FV s \<union> FV t" unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by blast

lemma wf_subst_single:
  assumes "v \<notin> FV t" "\<sigma> v = t" "\<And>w. v \<noteq> w \<Longrightarrow> \<sigma> w = Var w"
  shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
proof -
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {v}" using subst_FV_dom_img_single[of v t \<sigma>, OF assms] by simp
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = {}" "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
    using assms(1,2,3) subst_FV_dom_img_single(2)
    by (metis inf_bot_left insert_disjoint(1), simp)
  thus ?thesis by simp
qed

lemma wf_subst_reduction:
  "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s \<Longrightarrow> wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s)"
proof -
  assume "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
  moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s" by auto
  moreover have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) = {}"
    by (meson compl_le_compl_iff disjoint_eq_subset_Compl subset_trans wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
  moreover have "finite (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s))"
    using \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s) \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<close> \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s\<close> rev_finite_subset
    unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast
  ultimately show "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_var v s)" by simp
qed

lemma wf_subst_compose:
  assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2"
    and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
    and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
  shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>1 \<circ>\<^sub>s \<theta>2)"
using assms
proof (induction \<theta>1 rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct)
  case (Insert \<sigma>1 v t)
  have "t \<noteq> Var v" using Insert.hyps(4) by auto
  hence dom1v_unfold: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1)"
    using subst_dom_update2 by metis
  hence doms_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" 
    using Insert.prems(2) disjoint_insert(1) by blast
  moreover have dom_img_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
    using Insert.hyps(2) Insert.prems(3) by fastforce
  ultimately have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2)" using Insert.IH[OF \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2\<close>] by metis

  have dom_comp_is_union: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2) = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2"
    using subst_dom_comp_eq[OF dom_img_disj] .

  have "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" using Insert.prems(2) \<open>t \<noteq> Var v\<close> by fastforce
  hence "\<theta>2 v = Var v" "\<sigma>1 v = Var v" using Insert.hyps(2) by simp_all
  hence "(\<sigma>1 \<circ>\<^sub>s \<theta>2) v = Var v" "(\<sigma>1(v := t) \<circ>\<^sub>s \<theta>2) v = t \<cdot> \<theta>2" "((\<sigma>1 \<circ>\<^sub>s \<theta>2)(v := t)) v = t"
    unfolding subst_compose_def by simp_all
  
  have FV_t2_bound: "FV (t \<cdot> \<theta>2) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" by (meson subst_sends_FV_to_img)

  have 1: "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2)" using \<open>(\<sigma>1 \<circ>\<^sub>s \<theta>2) v = Var v\<close> by auto

  have "insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1) \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
    using Insert.prems(3) dom1v_unfold by blast
  hence "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" using Insert.hyps(3) by blast
  hence 2: "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2)" by (meson set_rev_mp subst_img_comp_subset)

  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" using \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2\<close> by simp
  hence "FV (t \<cdot> \<theta>2) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" using subst_dom_elim by simp
  moreover have "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" using Insert.prems(3) dom1v_unfold by blast
  hence "v \<notin> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" using Insert.hyps(4) by blast
  hence "v \<notin> FV (t \<cdot> \<theta>2)" using \<open>FV (t \<cdot> \<theta>2) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2\<close> by blast
  moreover have "FV (t \<cdot> \<theta>2) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 = {}"
    using dom_img_disj FV_t2_bound \<open>FV t \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1) = {}\<close> by blast
  ultimately have 3: "FV (t \<cdot> \<theta>2) \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2)) = {}"
    using dom_comp_is_union by blast

  have "\<sigma>1(v := t) \<circ>\<^sub>s \<theta>2 = (\<sigma>1 \<circ>\<^sub>s \<theta>2)(v := t \<cdot> \<theta>2)" using subst_comp_upd1[of \<sigma>1 v t \<theta>2] .
  moreover have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ((\<sigma>1 \<circ>\<^sub>s \<theta>2)(v := t \<cdot> \<theta>2))"
    using "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.Insert"[OF _ 1 2 3] \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1 \<circ>\<^sub>s \<theta>2)\<close> wf_subst_properties by metis
  ultimately show ?case by presburger
qed simp

lemma wf_subst_append:
  fixes \<theta>1 \<theta>2::"('f,'v) subst"
  assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2"
    and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
    and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
    and "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}"
  shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<lambda>v. if \<theta>1 v = Var v then \<theta>2 v else \<theta>1 v)"
using assms
proof (induction \<theta>1 rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct)
  case (Insert \<sigma>1 v t)
  let ?if = "\<lambda>w. if \<sigma>1 w = Var w then \<theta>2 w else \<sigma>1 w"
  let ?if_upd = "\<lambda>w. if (\<sigma>1(v := t)) w = Var w then \<theta>2 w else (\<sigma>1(v := t)) w"

  from Insert.hyps(4) have "?if_upd = ?if(v := t)" by fastforce

  have dom_insert: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1(v := t)) = insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1)"
    using Insert.hyps(4) by auto

  have "\<sigma>1 v = Var v" "t \<noteq> Var v" using Insert.hyps(2,4) by auto
  hence img_insert: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma>1(v := t)) = FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<union> FV t"
    using subst_img_update by metis

  from Insert.prems(2) dom_insert have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" by auto
  moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" using Insert.prems(3) dom_insert by simp
  moreover have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 = {}" using Insert.prems(4) img_insert
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if" using Insert.IH[OF Insert.prems(1)] by metis
  
  have dom_union: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>1 \<union> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" by auto
  hence "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if" using Insert.hyps(2) Insert.prems(2) dom_insert by auto
  moreover have "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if"
    using Insert.prems(3) Insert.hyps(3) dom_insert unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  moreover have "FV t \<inter> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if) = {}"
    using Insert.hyps(4) Insert.prems(4) img_insert unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately show ?case
    using wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_set.Insert \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?if\<close> \<open>?if_upd = ?if(v := t)\<close> wf_subst_properties
    by (metis (no_types, lifting))  
qed simp

lemma wf_subst_elim_append:
  assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "elim \<theta> v" "v \<notin> FV t"
  shows "elim (\<theta>(w := t)) v"
using assms
proof (induction \<theta> rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct)
  case (Insert \<theta> v' t')
  hence "\<And>q. v \<notin> FV (Var q \<cdot> \<theta>(v' := t'))" using elim_dest by blast
  hence "\<And>q. v \<notin> FV (Var q \<cdot> \<theta>(v' := t', w := t))" using \<open>v \<notin> FV t\<close> by simp
  thus ?case by (metis elim_intro' subst_apply_term.simps(1)) 
qed simp

lemma wf_subst_elim_dom:
  assumes "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  shows "\<forall>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. elim \<theta> v"
using assms
proof (induction \<theta> rule: wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_induct)
  case (Insert \<theta> w t)
  have dom_insert: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>(w := t)) \<subseteq> insert w (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" by auto
  hence "\<forall>v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. elim (\<theta>(w := t)) v" using Insert.IH Insert.hyps(2,4)
    by (metis Insert.hyps(1) IntI disjoint_insert(2) empty_iff wf_subst_elim_append) 
  moreover have "w \<notin> FV t" using Insert.hyps(4) by simp
  hence "\<And>q. w \<notin> FV (Var q \<cdot> \<theta>(w := t))"
    by (metis FV_simps(1) FV_in_subst_img Insert.hyps(3) contra_subsetD 
              fun_upd_def singletonD subst_apply_term.simps(1)) 
  hence "elim (\<theta>(w := t)) w" by (metis elim_intro')
  ultimately show ?case using dom_insert by blast
qed simp

lemma wf_subst_support_iff_mgt: "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> \<theta> supports \<delta> \<longleftrightarrow> \<theta> \<preceq>\<^sub>\<circ> \<delta>"
using subst_support_def subst_support_if_mgt_Idem wf_subst_Idem by blast 


subsection {* Interpretations *}
abbreviation interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t::"('a,'b) subst \<Rightarrow> bool" where
  "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<equiv> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = UNIV \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"

lemma interpretation_substI:
  "(\<And>v. FV (\<theta> v) = {}) \<Longrightarrow> interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
proof -
  assume "\<And>v. FV (\<theta> v) = {}"
  moreover { fix v assume "FV (\<theta> v) = {}" hence "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" by auto }
  ultimately show ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
qed

lemma interpretation_grounds[simp]: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> FV (t \<cdot> \<theta>) = {}"
by (simp add: subst_FV_dom_ground_if_ground_img)

lemma interpretation_grounds_all:
  "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> (\<And>v. FV (\<theta> v) = {})"
unfolding ground_def
by (metis UNIV_I FV_in_subst_img subset_empty subst_dom_vars_in_subst)

lemma interpretation_grounds_all':
  "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> ground (M \<cdot>set \<theta>)"
by (simp add: subst_FV_dom_ground_if_ground_img)

lemma interpretation_comp:
  assumes "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" 
  shows "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma> \<circ>\<^sub>s \<theta>)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>)"
proof -
  have \<theta>_FV: "\<And>v. FV (\<theta> v) = {}" using interpretation_grounds_all[OF assms] by simp
  hence \<theta>_FV': "\<And>t. FV (t \<cdot> \<theta>) = {}"
    by (metis all_not_in_conv elim_dest elim_intro' subst_apply_term.simps(1))

  from assms have "\<And>v. (\<sigma> \<circ>\<^sub>s \<theta>) v \<noteq> Var v"
    unfolding subst_compose_def by (metis FV_simps(1) \<theta>_FV' insert_not_empty)
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma> \<circ>\<^sub>s \<theta>) = UNIV" by simp
  moreover have "\<And>v. FV ((\<sigma> \<circ>\<^sub>s \<theta>) v) = {}" unfolding subst_compose_def using \<theta>_FV' by simp
  hence "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma> \<circ>\<^sub>s \<theta>))" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
  ultimately show "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<sigma> \<circ>\<^sub>s \<theta>)" ..

  from assms have "\<And>v. (\<theta> \<circ>\<^sub>s \<sigma>) v \<noteq> Var v"
    unfolding subst_compose_def by (metis FV_simps(1) \<theta>_FV insert_not_empty subst_to_var_is_var)
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>) = UNIV" by simp
  moreover have "\<And>v. FV ((\<theta> \<circ>\<^sub>s \<sigma>) v) = {}"
    unfolding subst_compose_def by (simp add: \<theta>_FV trm_subst_ident) 
  hence "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>))" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
  ultimately show "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma>)" ..
qed

lemma interpretation_subst_exists:
  "\<exists>\<I>::('f,'v) subst. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
proof -
  obtain c::"'f" where "c \<in> UNIV" by simp
  then obtain \<I>::"('f,'v) subst" where "\<And>v. \<I> v = Fun c []" by simp
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = UNIV" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)" by (simp_all add: img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
  thus ?thesis by auto
qed

lemma interpretation_subst_exists':
  "\<exists>\<theta>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"
proof -
  obtain \<I>::"('f,'v) subst" where \<I>: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = UNIV" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)"
    using interpretation_subst_exists by moura
  let ?\<theta> = "rm_vars (UNIV - X) \<I>"
  have 1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<theta> = X" using \<I> by auto
  hence 2: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<theta>)" using \<I> unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force
  show ?thesis using 1 2 by metis
qed

lemma interpretation_Idem:
  "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> Idem \<theta>"
unfolding Idem_def using interpretation_grounds_all[of \<theta>]
by (simp add: trm_subst_ident subst_eq_if_eq_vars)

lemma Idem_comp_upd_eq:
  assumes "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "Idem \<theta>"
  shows "\<I> \<circ>\<^sub>s \<theta> = \<I>(v := \<theta> v) \<circ>\<^sub>s \<theta>"
proof -
  from assms(1) have "(\<I> \<circ>\<^sub>s \<theta>) v = \<theta> v" unfolding subst_compose_def by auto
  moreover have "\<And>w. w \<noteq> v \<Longrightarrow> (\<I> \<circ>\<^sub>s \<theta>) w = (\<I>(v := \<theta> v) \<circ>\<^sub>s \<theta>) w" unfolding subst_compose_def by auto
  moreover have "(\<I>(v := \<theta> v) \<circ>\<^sub>s \<theta>) v = \<theta> v" using assms(2) unfolding Idem_def subst_compose_def
    by (metis fun_upd_same) 
  ultimately show ?thesis by (metis fun_upd_same fun_upd_triv subst_comp_upd1)
qed

lemma interpretation_dom_img_disjoint: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = {}"
by simp


subsection {* IsaFoR Unification Theory Linking *}
lemma MGU_is_mgu_singleton: "MGU \<theta> t u = is_mgu \<theta> {(t,u)}"
unfolding is_mgu_def unifiers_def by auto

lemma Unifier_in_unifiers_singleton: "Unifier \<theta> s t \<longleftrightarrow> \<theta> \<in> unifiers {(s,t)}"
unfolding unifiers_def by auto

lemma subst_dom_conv: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = subst_domain s"
by (metis subst_domain_def dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)

lemma subst_ran_img_conv: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = subst_range s"
by (metis subst_range.simps img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_dom_conv)

lemma subst_range_vars_img_FV_conv: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t s = range_vars s"
by (simp add: range_vars_def subst_ran_img_conv)

declare subst_list_def[simp]

lemma subst_list_singleton_FV_subset:
  "(\<Union>x \<in> set (subst_list (subst v t) E). FV (fst x) \<union> FV (snd x))
    \<subseteq> FV t \<union> (\<Union>x \<in> set E. FV (fst x) \<union> FV (snd x))"
proof (induction E)
  case (Cons x E)
  let ?FVs = "\<lambda>L. \<Union>x \<in> set L. FV (fst x) \<union> FV (snd x)"
  let ?FVx = "FV (fst x) \<union> FV (snd x)"
  let ?FVxsubst = "FV (fst x \<cdot> Var(v := t)) \<union> FV (snd x \<cdot> Var(v := t))"
  have "?FVs (subst_list (subst v t) (x#E)) = ?FVxsubst \<union> ?FVs (subst_list (subst v t) E)"
    unfolding subst_list_def subst_def by auto
  hence "?FVs (subst_list (subst v t) (x#E)) \<subseteq> ?FVxsubst \<union> FV t \<union> ?FVs E"
    using Cons.IH by blast
  moreover have "?FVs (x#E) = ?FVx \<union> ?FVs E" by auto
  moreover have "?FVxsubst \<subseteq> ?FVx \<union> FV t" using subst_FV_bound_singleton[of _ v t] by blast
  ultimately show ?case by blast
qed simp

lemma subst_of_dom_subset: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of L) \<subseteq> set (map fst L)"
proof (induction L rule: List.rev_induct)
  case (snoc x L)
  then obtain v t where x: "x = (v,t)" by (metis surj_pair)
  hence "subst_of (L@[x]) = Var(v := t) \<circ>\<^sub>s subst_of L"
    using subst_of_simps(3)[of x "[]"] unfolding subst_def by auto
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of (L@[x])) \<subseteq> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of L))"
    using x subst_dom_comp_subset[of "Var(v := t)" "subst_of L"] by auto
  thus ?case using snoc.IH x by auto
qed simp

lemma wf_MGU_is_imgu_singleton: "wf\<^sub>M\<^sub>G\<^sub>U \<theta> s t \<Longrightarrow> is_imgu \<theta> {(s,t)}"
proof -
  assume "wf\<^sub>M\<^sub>G\<^sub>U \<theta> s t"
  hence "Idem \<theta>" "\<forall>\<theta>' \<in> unifiers {(s,t)}. \<theta> \<preceq>\<^sub>\<circ> \<theta>'" "\<theta> \<in> unifiers {(s,t)}"
    using wf_subst_Idem Unifier_in_unifiers_singleton
    unfolding wf\<^sub>M\<^sub>G\<^sub>U_def
    by auto
  hence "\<forall>\<tau> \<in> unifiers {(s,t)}. \<tau> = \<theta> \<circ>\<^sub>s \<tau>" by (metis Idem_def comp_assoc)
  thus "is_imgu \<theta> {(s,t)}" by (metis is_imgu_def \<open>\<theta> \<in> unifiers {(s,t)}\<close>)
qed

lemma mgu_subst_range_vars:
  assumes "mgu s t = Some \<sigma>" shows "range_vars \<sigma> \<subseteq> vars_term s \<union> vars_term t"
proof -
  obtain xs where *: "Unification.unify [(s, t)] [] = Some xs" and [simp]: "subst_of xs = \<sigma>"
    using assms by (simp split: option.splits)
  from unify_Some_UNIF [OF *] obtain ss
    where "compose ss = \<sigma>" and "UNIF ss {#(s, t)#} {#}" by auto
  with UNIF_range_vars_subset [of ss "{#(s, t)#}" "{#}"]
    show ?thesis by simp
qed

lemma mgu_subst_domain_range_vars_disjoint:
  assumes "mgu s t = Some \<sigma>" shows "subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
proof -
  have "is_imgu \<sigma> {(s, t)}" using assms mgu_sound by simp
  hence "\<sigma> = \<sigma> \<circ>\<^sub>s \<sigma>" unfolding is_imgu_def by blast
  thus ?thesis by (metis \<open>\<sigma> = \<sigma> \<circ>\<^sub>s \<sigma>\<close> subst_idemp_iff) 
qed

lemma mgu_gives_wellformed_subst:
  assumes "mgu s t = Some \<theta>" shows "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
using mgu_finite_subst_domain[OF assms] mgu_subst_domain_range_vars_disjoint[OF assms]
      subst_range_vars_img_FV_conv[of \<theta>] subst_dom_conv[of \<theta>]
unfolding wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
by auto

lemma mgu_gives_wellformed_MGU:
  assumes "mgu s t = Some \<theta>" shows "wf\<^sub>M\<^sub>G\<^sub>U \<theta> s t"
using mgu_subst_domain[OF assms] mgu_sound[OF assms] mgu_subst_range_vars[OF assms]
      subst_range_vars_img_FV_conv[of \<theta>] subst_dom_conv[of \<theta>] MGU_is_mgu_singleton[of s \<theta> t]
      is_imgu_imp_is_mgu[of \<theta> "{(s,t)}"] mgu_gives_wellformed_subst[OF assms]
unfolding wf\<^sub>M\<^sub>G\<^sub>U_def
by auto

lemma mgu_vars_bounded[dest?]:
  "mgu M N = Some \<sigma> \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> FV M \<union> FV N"
using mgu_gives_wellformed_MGU unfolding wf\<^sub>M\<^sub>G\<^sub>U_def by blast

lemma mgu_gives_Idem: "mgu s t = Some \<theta> \<Longrightarrow> Idem \<theta>"
using mgu_sound[of s t \<theta>] unfolding is_imgu_def Idem_def by auto

lemma mgu_always_unifies: "Unifier \<theta> M N \<Longrightarrow> \<exists>\<delta>. mgu M N = Some \<delta>"
using mgu_complete Unifier_in_unifiers_singleton by blast

lemma mgu_gives_MGU: "mgu s t = Some \<theta> \<Longrightarrow> MGU \<theta> s t"
using mgu_sound[of s t \<theta>, THEN is_imgu_imp_is_mgu] MGU_is_mgu_singleton by metis

lemma mgu_same_empty: "mgu (t::('a,'b) term) t = Some Var"
proof -
  { fix E::"('a,'b) equation list" and U::"('b \<times> ('a,'b) term) list"
    assume "\<forall>(s,t) \<in> set E. s = t"
    hence "Unification.unify E U = Some U"
    proof (induction E U rule: Unification.unify.induct)
      case (2 f S g T E U)
      hence *: "f = g" "S = T" by auto
      moreover have "\<forall>(s,t) \<in> set (zip T T). s = t" by (induct T) auto
      hence "\<forall>(s,t) \<in> set (zip T T@E). s = t" using "2.prems"(1) by auto
      moreover have "zip_option S T = Some (zip S T)"
        using \<open>S = T\<close> by (induct S T rule: zip_induct) auto
      hence **: "decompose (Fun f S) (Fun g T) = Some (zip S T)"
        using \<open>f = g\<close> unfolding decompose_def by auto
      ultimately have "Unification.unify (zip S T@E) U = Some U" using "2.IH" * by auto
      thus ?case using ** by auto
    qed auto
  }
  hence "Unification.unify [(t,t)] [] = Some []" by auto
  thus ?thesis by auto
qed

lemma mgu_var: assumes "x \<notin> FV t" shows "mgu (Var x) t = Some (Var(x := t))"
proof -
  have "unify [(Var x,t)] [] = Some [(x,t)]" using assms by auto
  moreover have "subst_of [(x,t)] = Var(x := t)" unfolding subst_of_def subst_def by simp
  ultimately show ?thesis by simp
qed

lemma mgu_eliminates[dest?]:
  assumes "mgu M N = Some \<sigma>"
  shows "(\<exists>v \<in> FV M \<union> FV N. elim \<sigma> v) \<or> \<sigma> = Var"
  (is "?P M N \<sigma>")
proof (cases "\<sigma> = Var")
  case False
  then obtain v where v: "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" by auto
  hence "v \<in> FV M \<union> FV N" using mgu_vars_bounded[OF assms] by auto
  thus ?thesis using wf_subst_elim_dom[OF mgu_gives_wellformed_subst[OF assms]] v by blast
qed simp

lemma mgu_eliminates_dom:
  assumes "mgu x y = Some \<theta>" "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  shows "elim \<theta> v"
using mgu_gives_wellformed_subst[OF assms(1)]
unfolding wf\<^sub>M\<^sub>G\<^sub>U_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def elim_def
by (metis disjoint_iff_not_equal subst_dom_elim assms(2))

lemma unify_list_distinct:
  assumes "Unification.unify E B = Some U" "distinct (map fst B)"
  and "(\<Union>x \<in> set E. FV (fst x) \<union> FV (snd x)) \<inter> set (map fst B) = {}"
  shows "distinct (map fst U)"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case 1 thus ?case by simp
next
  case (2 f X g Y E B U)
  let ?FVs = "\<lambda>L. \<Union>x \<in> set L. FV (fst x) \<union> FV (snd x)"
  from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'"
    and [simp]: "f = g" "length X = length Y" "E' = zip X Y"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  hence "\<And>t t'. (t,t') \<in> set E' \<Longrightarrow> FV t \<subseteq> FV (Fun f X) \<and> FV t' \<subseteq> FV (Fun g Y)"
    by (metis zip_arg_subterm subtermseq_if_subterms subtermeq_vars_subset)
  hence "?FVs E' \<subseteq> FV (Fun f X) \<union> FV (Fun g Y)" by fastforce
  moreover have "FV (Fun f X) \<inter> set (map fst B) = {}" "FV (Fun g Y) \<inter> set (map fst B) = {}"
    using "2.prems"(3) by auto
  ultimately have "?FVs E' \<inter> set (map fst B) = {}" by blast
  moreover have "?FVs E \<inter> set (map fst B) = {}" using "2.prems"(3) by auto
  ultimately have "?FVs (E'@E) \<inter> set (map fst B) = {}" by auto
  thus ?case using "2.IH"[OF * ** "2.prems"(2)] by metis
next
  case (3 v t E B)
  let ?FVs = "\<lambda>L. \<Union>x \<in> set L. FV (fst x) \<union> FV (snd x)"
  let ?E' = "subst_list (subst v t) E"
  from "3.prems"(3) have "v \<notin> set (map fst B)" "FV t \<inter> set (map fst B) = {}" by force+
  hence *: "distinct (map fst ((v, t)#B))" using "3.prems"(2) by auto

  show ?case
  proof (cases "t = Var v")
    case True thus ?thesis using "3.prems" "3.IH"(1) by auto
  next
    case False
    hence "v \<notin> FV t" using "3.prems"(1) by auto
    hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using \<open>t \<noteq> Var v\<close> "3.prems"(1) by auto
    moreover have "?FVs ?E' \<inter> set (map fst ((v, t)#B)) = {}"
    proof -
      have "v \<notin> ?FVs ?E'"
        unfolding subst_list_def subst_def
        by (simp add: \<open>v \<notin> FV t\<close> subst_remove_var)
      moreover have "?FVs ?E' \<subseteq> FV t \<union> ?FVs E" by (metis subst_list_singleton_FV_subset)
      hence "?FVs ?E' \<inter> set (map fst B) = {}" using "3.prems"(3) by auto
      ultimately show ?thesis by auto
    qed 
    ultimately show ?thesis using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> FV t\<close> _ *] by metis
  qed
next
  case (4 f X v E B U)
  let ?FVs = "\<lambda>L. \<Union>x \<in> set L. FV (fst x) \<union> FV (snd x)"
  let ?E' = "subst_list (subst v (Fun f X)) E"
  have *: "?FVs E \<inter> set (map fst B) = {}" using "4.prems"(3) by auto
  from "4.prems"(1) have "v \<notin> FV (Fun f X)" by force
  from "4.prems"(3) have **: "v \<notin> set (map fst B)" "FV (Fun f X) \<inter> set (map fst B) = {}" by force+
  hence ***: "distinct (map fst ((v, Fun f X)#B))" using "4.prems"(2) by auto
  from "4.prems"(3) have ****: "?FVs ?E' \<inter> set (map fst ((v, Fun f X)#B)) = {}"
  proof -
    have "v \<notin> ?FVs ?E'"
      unfolding subst_list_def subst_def
      using \<open>v \<notin> FV (Fun f X)\<close> subst_remove_var[of v "Fun f X"] by simp
    moreover have "?FVs ?E' \<subseteq> FV (Fun f X) \<union> ?FVs E" by (metis subst_list_singleton_FV_subset)
    hence "?FVs ?E' \<inter> set (map fst B) = {}" using * ** by blast
    ultimately show ?thesis by auto
  qed
  have "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, Fun f X) # B) = Some U"
    using \<open>v \<notin> FV (Fun f X)\<close> "4.prems"(1) by auto
  thus ?case using "4.IH"[OF \<open>v \<notin> FV (Fun f X)\<close> _ *** ****] by metis
qed

lemma mgu_None_is_subst_neq:
  fixes s t::"('a,'b) term" and \<delta>::"('a,'b) subst"
  assumes "mgu s t = None"
  shows "s \<cdot> \<delta> \<noteq> t \<cdot> \<delta>"
using assms mgu_always_unifies by force

lemma mgu_None_if_neq_ground:
  assumes "t \<noteq> t'" "FV t = {}" "FV t' = {}"
  shows "mgu t t' = None"
proof (rule ccontr)
  assume "mgu t t' \<noteq> None"
  then obtain \<delta> where \<delta>: "mgu t t' = Some \<delta>" by auto
  hence "t \<cdot> \<delta> = t" "t' \<cdot> \<delta> = t'" using assms subst_ground_ident by auto
  thus False using assms(1) MGU_is_Unifier[OF mgu_gives_MGU[OF \<delta>]] by auto
qed

lemma const_subst_subterm:
  assumes "Fun c [] \<sqsubseteq> t \<cdot> \<theta>"
  shows "Fun c [] \<sqsubseteq> t \<or> (\<exists>s \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. Fun c [] \<sqsubseteq> s)"
using assms unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (induction t) force+

lemma subst_of_const:
  assumes "(subst_of D) z = Fun c []"
  shows "\<exists>z. (z, Fun c []) \<in> set D"
using assms
proof (induction D arbitrary: z)
  case (Cons d D)
  then obtain x t where d: "d = (x, t)" by moura
  hence *: "subst_of (d#D) = subst_of D \<circ>\<^sub>s Var(x := t)"
    using subst_of_simps(3)[of d D] unfolding subst_def by simp
  from Cons show ?case
  proof (cases "\<exists>z. subst_of D z = Fun c []")
    case False
    hence "Fun c [] \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of D)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    moreover have "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_of D \<circ>\<^sub>s Var(x := t))"
      using * Cons.prems unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    moreover have "\<And>y. (Var(x := t)) y = Fun c [] \<Longrightarrow> t = Fun c []"
      by (metis fun_upd_apply term.distinct(1)) 
    ultimately have "t = Fun c []"
      using subst_img_comp_subset_const[of c "subst_of D" "Var(x := t)"]
      by (metis imageE img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
    thus ?thesis using d by auto
  qed auto
qed simp

lemma mgu_img_consts:
  fixes \<delta>::"('f,'v) subst" and s t::"('f,'v) term" and c::'f and z::'v
  assumes "mgu s t = Some \<delta>" "\<delta> z = Fun c []"
  shows "Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t"
proof -
  { fix E::"('f,'v) equation list" and B U::"('v \<times> ('f,'v) term) list" and z::'v
    assume "Unification.unify E B = Some U" "(z, Fun c []) \<in> set U"
    hence "(z,Fun c []) \<in> set B \<or> (\<exists>(s,t) \<in> set E. Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t)"
    proof (induction E B arbitrary: U rule: Unification.unify.induct)
      case 1 thus ?case by simp
    next
      case (2 f X g Y E B U)
      from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'"
        and **[simp]: "f = g" "length X = length Y" "E' = zip X Y"
        and ***: "Unification.unify (E'@E) B = Some U"
        by (auto split: option.splits)
      hence IH: "(z,Fun c []) \<in> set B \<or> (\<exists>(s,t) \<in> set (E'@E). Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t)"
        using "2.IH" "2.prems" by blast
      moreover have "\<exists>(s,t) \<in> set E'. (Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t) \<Longrightarrow> Fun c [] \<sqsubseteq> Fun f X \<or> Fun c [] \<sqsubseteq> Fun g Y"
      proof -
        assume "\<exists>(s, t)\<in>set E'. Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t"
        then obtain p::"('f, 'v) equation" where f1:
            "p \<in> set E' \<and> (case p of (t, t') \<Rightarrow> Fun c [] \<sqsubseteq> t \<or> Fun c [] \<sqsubseteq> t')"
          by blast
        have f2: "\<And>p. (fst p::('f,'v) term, snd p::('f,'v) Term.term) = p" by auto
        have f3: "Fun c [] \<sqsubseteq> fst p \<or> Fun c [] \<sqsubseteq> snd p" using f1 by force
        have f4: "\<And>p f. p \<notin> set E' \<or> snd p \<sqsubset> Fun f Y"
          by (metis (lifting) f2 **(3) zip_arg_subterm(2))
        have "fst p \<sqsubset> Fun f X" by (metis (no_types) f2 f1 **(3) zip_arg_subterm(1))
        thus ?thesis using f4 f3 f1 by (meson subtermeq_trans subtermseq_if_subterms)
      qed
      ultimately show ?case using \<open>E' = zip X Y\<close> by auto
    next
      case (3 v t E B) show ?case
      proof (cases "t = Var v")
        case True thus ?thesis using "3.prems" "3.IH"(1) by auto
      next
        case False
        hence "v \<notin> FV t" using "3.prems"(1) by auto
        hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
          using \<open>t \<noteq> Var v\<close> "3.prems"(1) by auto
        hence IH: "(z, Fun c []) \<in> set ((v, t)#B) \<or>
                   (\<exists>(s,t) \<in> set (subst_list (subst v t) E). Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t)"
          using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> FV t\<close> _ "3.prems"(2)] by metis
        show ?thesis
        proof (cases "(z, Fun c []) \<in> set ((v, t)#B)")
          case False
          hence "\<exists>p \<in> set E.
                  Fun c [] \<sqsubseteq> fst p \<cdot> Var(v := t) \<or>
                  Fun c [] \<sqsubseteq> snd p \<cdot> Var(v := t)"
            using IH unfolding subst_list_def subst_def by auto
          then obtain s s' where *:
              "(s, s') \<in> set E" "Fun c [] \<sqsubseteq> s \<cdot> Var(v := t) \<or> Fun c [] \<sqsubseteq> s' \<cdot> Var(v := t)"
            by auto
          moreover {
            assume "\<not>Fun c [] \<sqsubseteq> t"
            hence "\<not>(\<exists>s\<in>img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (Var(v := t)). Fun c [] \<sqsubseteq> s)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
            hence "Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> s'"
              using *(2) const_subst_subterm[of c _ "Var(v := t)"] by metis
          } ultimately show ?thesis by auto
        qed auto
      qed
    next
      case (4 f X v E B U)
      have "v \<notin> FV (Fun f X)" using "4.prems"(1) not_None_eq by fastforce
      hence "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U"
        using "4.prems"(1) by auto
      hence IH: "(z, Fun c []) \<in> set ((v, Fun f X)#B) \<or>
                 (\<exists>(s,s') \<in> set (subst_list (subst v (Fun f X)) E). Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> s')"
        using "4.IH"[OF \<open>v \<notin> FV (Fun f X)\<close> _ "4.prems"(2)] by metis
      show ?case
      proof (cases "(z, Fun c []) \<in> set ((v, Fun f X)#B)")
        case False
        hence "\<exists>p \<in> set E.
                Fun c [] \<sqsubseteq> fst p \<cdot> Var(v := Fun f X) \<or>
                Fun c [] \<sqsubseteq> snd p \<cdot> Var(v := Fun f X)"
          using IH unfolding subst_list_def subst_def by auto
        then obtain s s' where *:
            "(s, s') \<in> set E" "Fun c [] \<sqsubseteq> s \<cdot> Var(v := Fun f X) \<or> Fun c [] \<sqsubseteq> s' \<cdot> Var(v := Fun f X)"
          by auto
        moreover {
          assume "\<not>Fun c [] \<sqsubseteq> Fun f X"
          hence "\<not>(\<exists>s\<in>img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (Var(v := Fun f X)). Fun c [] \<sqsubseteq> s)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
          hence "Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> s'"
            using *(2) const_subst_subterm[of c _ "Var(v := Fun f X)"] by metis
        } ultimately show ?thesis by auto
      qed auto
    qed
  } moreover obtain D where "unify [(s, t)] [] = Some D" "\<delta> = subst_of D"
      using assms(1) by (cases "unify [(s, t)] []") auto
  moreover have "\<exists>z. (z,Fun c []) \<in> set D" using \<open>\<delta> = subst_of D\<close> assms(2) subst_of_const by metis
  ultimately show ?thesis by fastforce
qed

lemma inj_const_subst_unif:
  fixes \<I> \<theta> \<sigma>::"('f,'v) subst" and s t::"('f,'v) term"
  assumes \<theta>: "inj \<theta>" "\<forall>u \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<exists>c. u = Fun c []"
             "\<forall>u \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. u \<notin> subterms s \<union> subterms t"
  and \<I>: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  and unif: "Unifier \<sigma> (s \<cdot> \<theta>) (t \<cdot> \<theta>)"
  shows "\<exists>\<delta>. Unifier \<delta> (s \<cdot> \<I>) (t \<cdot> \<I>)"
proof -
  let ?xs = "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  let ?ys = "(FV s \<union> FV t) - ?xs"

  have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" using \<theta>(2) by auto

  have "\<exists>\<delta>::('f,'v) subst. s \<cdot> \<delta> = t \<cdot> \<delta>" by (metis subst_comp unif)
  then obtain \<delta>::"('f,'v) subst" where \<delta>: "mgu s t = Some \<delta>"
    using mgu_always_unifies by moura
  have 1: "\<exists>\<sigma>::('f,'v) subst. s \<cdot> \<theta> \<cdot> \<sigma> = t \<cdot> \<theta> \<cdot> \<sigma>" by (metis unif)
  have 2: "\<And>\<gamma>::('f,'v) subst. s \<cdot> \<theta> \<cdot> \<gamma> = t \<cdot> \<theta> \<cdot> \<gamma> \<Longrightarrow> \<delta> \<preceq>\<^sub>\<circ> \<theta> \<circ>\<^sub>s \<gamma>" using mgu_gives_MGU[OF \<delta>] by simp
  have 3: "\<And>(z::'v) (c::'f). \<delta> z = Fun c [] \<Longrightarrow> Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t"
    by (rule mgu_img_consts[OF \<delta>])
  have 4: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" using mgu_gives_wellformed_subst[OF \<delta>] by auto
  have 5: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV s \<union> FV t" using mgu_gives_wellformed_MGU[OF \<delta>] by auto

  { fix x and \<gamma>::"('f,'v) subst" assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    hence "(\<theta> \<circ>\<^sub>s \<gamma>) x = \<theta> x" using \<open>ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)\<close> by (simp add: ident_comp_subst_trm_if_disj) 
  }
  then obtain \<tau>::"('f,'v) subst" where \<tau>: "\<forall>x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<theta> x = (\<delta> \<circ>\<^sub>s \<tau>) x" using 1 2 by moura

  have *: "\<And>x. x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<Longrightarrow> \<exists>y \<in> ?ys. \<delta> x = Var y"
  proof -
    fix x assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs"
    hence x: "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" by auto
    then obtain c where c: "\<theta> x = Fun c []" using \<theta>(2) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by moura
    hence *: "(\<delta> \<circ>\<^sub>s \<tau>) x = Fun c []" using \<tau> x by fastforce
    hence **: "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta> \<circ>\<^sub>s \<tau>)" "Fun c [] \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta> \<circ>\<^sub>s \<tau>)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    have "\<delta> x = Fun c [] \<or> (\<exists>z. \<delta> x = Var z \<and> \<tau> z = Fun c [])"
      by (rule subst_img_comp_subset_const'[OF *])
    moreover have "\<delta> x \<noteq> Fun c []"
    proof (rule ccontr)
      assume "\<not>\<delta> x \<noteq> Fun c []"
      hence "Fun c [] \<sqsubseteq> s \<or> Fun c [] \<sqsubseteq> t" using 3 by metis
      moreover have "Fun c [] \<notin> subterms s \<union> subterms t"
        by (metis c \<open>ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)\<close> \<theta>(3) x(2) ground_subst_dom_iff_img) 
      ultimately show False by auto
    qed
    moreover have "\<forall>x' \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<delta> x \<noteq> Var x'"
    proof (rule ccontr)
      assume "\<not>(\<forall>x' \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<delta> x \<noteq> Var x')"
      then obtain x' where x': "x' \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<delta> x = Var x'" by moura
      hence "\<tau> x' = Fun c []" "(\<delta> \<circ>\<^sub>s \<tau>) x = Fun c []" using * unfolding subst_compose_def by auto
      moreover have "x \<noteq> x'" using x(1) x'(2) 4 by auto
      moreover have "x' \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
        using x'(2) mgu_eliminates_dom[OF \<delta>]
        by (metis (no_types) elim_def subst_apply_term.simps(1) vars_iff_subterm_or_eq )
      moreover have "(\<delta> \<circ>\<^sub>s \<tau>) x = \<theta> x" "(\<delta> \<circ>\<^sub>s \<tau>) x' = \<theta> x'" using \<tau> x(2) x'(1) by auto
      ultimately show False using \<theta>(1) * unfolding inj_on_def by (simp add: subst_compose_def x'(2))
    qed
    ultimately show "\<exists>y \<in> ?ys. \<delta> x = Var y"
      by (metis 5 x(2) DiffI Un_iff subst_FV_imgI subtermeqI' sup.orderE vars_iff_subtermeq)
  qed

  have **: "inj_on \<delta> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs)"
  proof (intro inj_onI)
    fix x y assume *: "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<delta> x = \<delta> y"
    hence "(\<delta> \<circ>\<^sub>s \<tau>) x = (\<delta> \<circ>\<^sub>s \<tau>) y" unfolding subst_compose_def by auto
    hence "\<theta> x = \<theta> y" using \<tau> * by auto
    thus "x = y" using \<theta>(1) inj_onD[of \<theta> UNIV x y] by simp
  qed

  def \<alpha> \<equiv> "\<lambda>y'. if Var y' \<in> \<delta> ` (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs)
                 then Var ((inv_into (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs) \<delta>) (Var y'))
                 else Var y'::('f,'v) term"
  have a1: "Unifier (\<delta> \<circ>\<^sub>s \<alpha>) s t" using mgu_gives_MGU[OF \<delta>] by auto

  def \<delta>' \<equiv> "\<delta> \<circ>\<^sub>s \<alpha>"
  have d1: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>' \<subseteq> ?ys"
  proof
    fix z assume z: "z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>'"
    have "z \<in> ?xs \<Longrightarrow> z \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>'"
    proof (cases "z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>")
      case True
      moreover assume "z \<in> ?xs"
      ultimately have z_in: "z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs" by simp
      then obtain y where y: "\<delta> z = Var y" "y \<in> ?ys" using * by moura
      hence "\<alpha> y = Var ((inv_into (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> ?xs) \<delta>) (Var y))"
        using \<alpha>_def z_in by simp
      hence "\<alpha> y = Var z" by (metis y(1) z_in ** inv_into_f_eq)
      hence "\<delta>' z = Var z" using \<delta>'_def y(1) subst_compose_def[of \<delta> \<alpha>] by simp
      thus ?thesis by auto
    next
      case False
      hence "\<delta> z = Var z" by simp
      moreover assume "z \<in> ?xs"
      hence "\<alpha> z = Var z" using \<alpha>_def * by force
      ultimately show ?thesis using \<delta>'_def subst_compose_def[of \<delta> \<alpha>] by simp
    qed
    moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<alpha> \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" unfolding \<delta>'_def \<alpha>_def by auto
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>' \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using subst_dom_comp_subset \<delta>'_def by fastforce
    ultimately show "z \<in> ?ys" using 5 z by auto
  qed
  have d2: "Unifier (\<delta>' \<circ>\<^sub>s \<I>) s t" using a1 \<delta>'_def by auto
  have d3: "\<I> \<circ>\<^sub>s \<delta>' \<circ>\<^sub>s \<I> = \<delta>' \<circ>\<^sub>s \<I>"
  proof -
    { fix z::'v assume z: "z \<in> ?xs"
      then obtain u where u: "\<I> z = u" "FV u = {}" using \<I> by auto
      hence "(\<I> \<circ>\<^sub>s \<delta>' \<circ>\<^sub>s \<I>) z = u" by (simp add: subst_compose subst_ground_ident)
      moreover have "z \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>'" using d1 z by auto
      hence "\<delta>' z = Var z" by simp
      hence "(\<delta>' \<circ>\<^sub>s \<I>) z = u" using u(1) by (simp add: subst_compose)
      ultimately have "(\<I> \<circ>\<^sub>s \<delta>' \<circ>\<^sub>s \<I>) z = (\<delta>' \<circ>\<^sub>s \<I>) z" by metis
    } moreover {
      fix z::'v assume "z \<in> ?ys"
      hence "z \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" using \<I>(2) by auto
      hence "(\<I> \<circ>\<^sub>s \<delta>' \<circ>\<^sub>s \<I>) z = (\<delta>' \<circ>\<^sub>s \<I>) z" by (simp add: subst_compose)
    } moreover {
      fix z::'v assume "z \<notin> ?xs" "z \<notin> ?ys"
      hence "\<I> z = Var z" "\<delta>' z = Var z" using \<I>(2) d1 by blast+
      hence "(\<I> \<circ>\<^sub>s \<delta>' \<circ>\<^sub>s \<I>) z = (\<delta>' \<circ>\<^sub>s \<I>) z" by (simp add: subst_compose)
    } ultimately show ?thesis by auto
  qed

  from d2 d3 have "Unifier (\<delta>' \<circ>\<^sub>s \<I>) (s \<cdot> \<I>) (t \<cdot> \<I>)" by (metis subst_comp) 
  thus ?thesis by metis
qed

lemma sat_ineq_inj_const_subst_aux:
  fixes \<I>::"('f,'v) subst"
  assumes "Unifier \<sigma> (s \<cdot> \<I>) (t \<cdot> \<I>)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)"
          "(FV s \<union> FV t) - X \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<inter> X = {}"
  shows "\<exists>\<delta>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<and> s \<cdot> \<delta> \<cdot> \<I> = t \<cdot> \<delta> \<cdot> \<I>"
proof -
  have "\<exists>\<sigma>. Unifier \<sigma> (s \<cdot> \<I>) (t \<cdot> \<I>) \<and> interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
  proof -
    obtain \<I>'::"('f,'v) subst" where *: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>'"
      using interpretation_subst_exists by metis
    hence "Unifier (\<sigma> \<circ>\<^sub>s \<I>') (s \<cdot> \<I>) (t \<cdot> \<I>)" using assms(1) by simp
    thus ?thesis using * interpretation_comp by blast
  qed
  then obtain \<sigma>' where \<sigma>': "Unifier \<sigma>' (s \<cdot> \<I>) (t \<cdot> \<I>)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>'" by moura
  
  def \<sigma>'' \<equiv> "rm_vars (UNIV - X) \<sigma>'"
  
  have *: "FV (s \<cdot> \<I>) \<subseteq> X" "FV (t \<cdot> \<I>) \<subseteq> X" using assms(2,3)
    by (simp_all add: Diff_subset_conv Un_commute subst_FV_unfold_ground_img)
  hence **: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>'' = X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>'')"
    using rm_vars_img_subset[of "UNIV - X" \<sigma>'] rm_vars_dom[of "UNIV - X" \<sigma>'] \<sigma>'(2) \<sigma>''_def by auto
  hence "\<And>t. t \<cdot> \<I> \<cdot> \<sigma>'' = t \<cdot> \<sigma>'' \<cdot> \<I>"
    using subst_eq_if_disjoint_vars_ground[OF _ _ assms(2)] assms(4) by blast
  moreover have "Unifier \<sigma>'' (s \<cdot> \<I>) (t \<cdot> \<I>)"
    using Unifier_dom_restrict[OF \<sigma>'(1)] \<sigma>''_def * by blast
  ultimately show ?thesis using ** by auto
qed

lemma sat_ineq_inj_const_subst:
  fixes \<theta> \<I> \<delta>::"('f,'v) subst"
  assumes \<theta>: "inj \<theta>"
             "\<forall>t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. \<exists>c. t = Fun c []"
             "\<forall>u \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. u \<notin> subterms s \<union> subterms t"
             "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> X = {}"
  and \<I>: "\<forall>\<delta>::('f,'v) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<longrightarrow> s \<cdot> \<delta> \<cdot> \<I> \<noteq> t \<cdot> \<delta> \<cdot> \<I>"
         "(FV s \<union> FV t) - X \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<inter> X = {}" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)"
         "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
  and \<delta>: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
  shows "s \<cdot> \<delta> \<cdot> \<theta> \<noteq> t \<cdot> \<delta> \<cdot> \<theta>"
proof -
  have "\<forall>\<sigma>. \<not>Unifier \<sigma> (s \<cdot> \<I>) (t \<cdot> \<I>)" by (metis \<I>(1) sat_ineq_inj_const_subst_aux[OF _ \<I>(4,2,3)])
  hence "\<not>Unifier \<delta> (s \<cdot> \<theta>) (t \<cdot> \<theta>)" by (metis inj_const_subst_unif[OF \<theta>(1,2,3) \<I>(4,5)])
  moreover have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" using \<theta>(2,4) \<delta>(1) by auto
  ultimately show ?thesis using \<delta> subst_eq_if_disjoint_vars_ground[OF _ _ \<delta>(2)] by metis
qed

end
