Theory More_Unification

(*
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:      More_Unification.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause

    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
*)

section ‹Definitions and Properties Related to Substitutions and Unification›

theory More_Unification
  imports Messages "First_Order_Terms.Unification"
begin

subsection ‹Substitutions›

abbreviation subst_apply_list (infix "⋅list" 51) where
  "T ⋅list θ ≡ map (λt. t ⋅ θ) T"  

abbreviation subst_apply_pair (infixl "⋅p" 60) where
  "d ⋅p θ ≡ (case d of (t,t') ⇒ (t ⋅ θ, t' ⋅ θ))"

abbreviation subst_apply_pair_set (infixl "⋅pset" 60) where
  "M ⋅pset θ ≡ (λd. d ⋅p θ) ` M"

definition subst_apply_pairs (infix "⋅pairs" 51) where
  "F ⋅pairs θ ≡ map (λf. f ⋅p θ) F"

abbreviation subst_more_general_than (infixl "≼∘" 50) where
  "σ ≼∘ θ ≡ ∃γ. θ = σ ∘s γ"

abbreviation subst_support (infix "supports" 50) where
  "θ supports δ ≡ (∀x. θ x ⋅ δ = δ x)"

abbreviation rm_var where
  "rm_var v s ≡ s(v := Var v)"

abbreviation rm_vars where
  "rm_vars vs σ ≡ (λv. if v ∈ vs then Var v else σ v)"

definition subst_elim where
  "subst_elim σ v ≡ ∀t. v ∉ fv (t ⋅ σ)"

definition subst_idem where
  "subst_idem s ≡ s ∘s s = s"

lemma subst_support_def: "θ supports τ ⟷ τ = θ ∘s τ"
unfolding subst_compose_def by metis

lemma subst_supportD: "θ supports δ ⟹ θ ≼∘ δ"
using subst_support_def by auto

lemma rm_vars_empty[simp]: "rm_vars {} s = s" "rm_vars (set []) s = s"
by simp_all

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

lemma subst_apply_terms_empty: "M ⋅set Var = M"
by simp

lemma subst_agreement: "(t ⋅ r = t ⋅ s) ⟷ (∀v ∈ fv t. Var v ⋅ r = Var v ⋅ s)"
by (induct t) auto

lemma repl_invariance[dest?]: "v ∉ fv t ⟹ t ⋅ s(v := u) = t ⋅ s"
by (simp add: subst_agreement)

lemma subst_idx_map:
  assumes "∀i ∈ set I. i < length T"
  shows "(map ((!) T) I) ⋅list δ = map ((!) (map (λt. t ⋅ δ) T)) I"
using assms by auto

lemma subst_idx_map':
  assumes "∀i ∈ fvset (set K). i < length T"
  shows "(K ⋅list (!) T) ⋅list δ = K ⋅list ((!) (map (λt. t ⋅ δ) T))" (is "?A = ?B")
proof -
  have "T ! i ⋅ δ = (map (λt. t ⋅ δ) T) ! i"
    when "i < length T" for i
    using that by auto
  hence "T ! i ⋅ δ = (map (λt. t ⋅ δ) T) ! i"
    when "i ∈ fvset (set K)" for i
    using that assms by auto
  hence "k ⋅ (!) T ⋅ δ = k ⋅ (!) (map (λt. t ⋅ δ) T)"
    when "fv k ⊆ fvset (set K)" for k
    using that by (induction k) force+
  thus ?thesis by auto
qed

lemma subst_remove_var: "v ∉ fv s ⟹ v ∉ fv (t ⋅ Var(v := s))"
by (induct t) simp_all

lemma subst_set_map: "x ∈ set X ⟹ x ⋅ s ∈ set (map (λx. x ⋅ s) X)"
by simp

lemma subst_set_idx_map:
  assumes "∀i ∈ I. i < length T"
  shows "(!) T ` I ⋅set δ = (!) (map (λt. t ⋅ δ) T) ` I" (is "?A = ?B")
proof
  have *: "T ! i ⋅ δ = (map (λt. t ⋅ δ) T) ! i"
    when "i < length T" for i
    using that by auto
  
  show "?A ⊆ ?B" using * assms by blast
  show "?B ⊆ ?A" using * assms by auto
qed

lemma subst_set_idx_map':
  assumes "∀i ∈ fvset K. i < length T"
  shows "K ⋅set (!) T ⋅set δ = K ⋅set (!) (map (λt. t ⋅ δ) T)" (is "?A = ?B")
proof
  have "T ! i ⋅ δ = (map (λt. t ⋅ δ) T) ! i"
    when "i < length T" for i
    using that by auto
  hence "T ! i ⋅ δ = (map (λt. t ⋅ δ) T) ! i"
    when "i ∈ fvset K" for i
    using that assms by auto
  hence *: "k ⋅ (!) T ⋅ δ = k ⋅ (!) (map (λt. t ⋅ δ) T)"
    when "fv k ⊆ fvset K" for k
    using that by (induction k) force+

  show "?A ⊆ ?B" using * by auto
  show "?B ⊆ ?A" using * by force
qed

lemma subst_term_list_obtain:
  assumes "∀i < length T. ∃s. P (T ! i) s ∧ S ! i = s ⋅ δ"
    and "length T = length S"
  shows "∃U. length T = length U ∧ (∀i < length T. P (T ! i) (U ! i)) ∧ S = map (λu. u ⋅ δ) U"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') auto

  have "∀i < length T. ∃s. P (T ! i) s ∧ S ! i = s ⋅ δ" "length T = length S"
    using Cons.prems S' by force+
  then obtain U where U:
      "length T = length U" "∀i < length T. P (T ! i) (U ! i)" "S = map (λu. u ⋅ δ) U"
    using Cons.IH by atomize_elim auto

  obtain u where u: "P t u" "s = u ⋅ δ"
    using Cons.prems(1) S' by auto

  have 1: "length (t#T) = length (u#U)"
    using Cons.prems(2) U(1) by fastforce

  have 2: "∀i < length (t#T). P ((t#T) ! i) ((u#U) ! i)"
    using u(1) U(2) by (simp add: nth_Cons')

  have 3: "S' = map (λu. u ⋅ δ) (u#U)"
    using U u S' by simp

  show ?case using 1 2 3 by blast
qed simp

lemma subst_mono: "t ⊑ u ⟹ t ⋅ s ⊑ u ⋅ s"
by (induct u) auto

lemma subst_mono_fv: "x ∈ fv t ⟹ s x ⊑ t ⋅ s"
by (induct t) auto

lemma subst_mono_neq:
  assumes "t ⊏ u"
  shows "t ⋅ s ⊏ u ⋅ s"
proof (cases u)
  case (Var v)
  hence False using ‹t ⊏ u› by simp
  thus ?thesis ..
next
  case (Fun f X)
  then obtain x where "x ∈ set X" "t ⊑ x" using ‹t ⊏ u› by auto
  hence "t ⋅ s ⊑ x ⋅ s" using subst_mono by metis

  obtain Y where "Fun f X ⋅ s = Fun f Y" by auto
  hence "x ⋅ s ∈ set Y" using ‹x ∈ set X› by auto
  hence "x ⋅ s ⊏ Fun f X ⋅ s" using ‹Fun f X ⋅ s = Fun f Y› Fun_param_is_subterm by simp
  hence "t ⋅ s ⊏ Fun f X ⋅ s" using ‹t ⋅ s ⊑ x ⋅ s› by (metis term.dual_order.trans term.order.eq_iff)
  thus ?thesis using ‹u = Fun f X› ‹t ⊏ u› by metis
qed

lemma subst_no_occs[dest]: "¬Var v ⊑ t ⟹ t ⋅ Var(v := s) = t"
by (induct t) (simp_all add: map_idI)

lemma var_comp[simp]: "σ ∘s Var = σ" "Var ∘s σ = σ"
unfolding subst_compose_def by simp_all

lemma subst_comp_all: "M ⋅set (δ ∘s θ) = (M ⋅set δ) ⋅set θ"
unfolding subst_subst_compose by auto

lemma subst_all_mono: "M ⊆ M' ⟹ M ⋅set s ⊆ M' ⋅set s"
by auto

lemma subst_comp_set_image: "(δ ∘s θ) ` X = δ ` X ⋅set θ"
using subst_compose by fastforce

lemma subst_ground_ident[dest?]: "fv t = {} ⟹ t ⋅ s = t"
by (induct t, simp, metis subst_agreement empty_iff subst_apply_term_empty)

lemma subst_ground_ident_compose:
  "fv (σ x) = {} ⟹ (σ ∘s θ) x = σ x"
  "fv (t ⋅ σ) = {} ⟹ t ⋅ (σ ∘s θ) = t ⋅ σ"
unfolding subst_subst_compose
by (simp_all add: subst_compose_def subst_ground_ident)

lemma subst_all_ground_ident[dest?]: "ground M ⟹ M ⋅set s = M"
proof -
  assume "ground M"
  hence "⋀t. t ∈ M ⟹ fv t = {}" by auto
  hence "⋀t. t ∈ M ⟹ t ⋅ s = t" by (metis subst_ground_ident)
  moreover have "⋀t. t ∈ M ⟹ t ⋅ s ∈ M ⋅set s" by (metis imageI)
  ultimately show "M ⋅set s = M" by (simp add: image_cong)
qed

lemma subst_cong: "⟦σ = σ'; θ = θ'⟧ ⟹ (σ ∘s θ) = (σ' ∘s θ')"
by auto

lemma subst_mgt_bot[simp]: "Var ≼∘ θ"
by simp

lemma subst_mgt_refl[simp]: "θ ≼∘ θ"
by (metis var_comp(1))

lemma subst_mgt_trans: "⟦θ ≼∘ δ; δ ≼∘ σ⟧ ⟹ θ ≼∘ σ"
by (metis subst_compose_assoc)

lemma subst_mgt_comp: "θ ≼∘ θ ∘s δ"
by auto

lemma subst_mgt_comp': "θ ∘s δ ≼∘ σ ⟹ θ ≼∘ σ"
by (metis subst_compose_assoc)

lemma var_self: "(λw. if w = v then Var v else Var w) = Var"
using subst_agreement by auto

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

lemma subst_eq_if_eq_vars: "(⋀v. (Var v) ⋅ θ = (Var v) ⋅ σ) ⟹ θ = σ"
by (auto simp add: subst_agreement)

lemma subst_all_empty[simp]: "{} ⋅set θ = {}"
by simp

lemma subst_all_insert:"(insert t M) ⋅set δ = insert (t ⋅ δ) (M ⋅set δ)"
by auto

lemma subst_apply_fv_subset: "fv t ⊆ V ⟹ fv (t ⋅ δ) ⊆ fvset (δ ` V)"
by (induct t) auto

lemma subst_apply_fv_empty:
  assumes "fv t = {}"
  shows "fv (t ⋅ σ) = {}"
using assms subst_apply_fv_subset[of t "{}" σ]
by auto

lemma subst_compose_fv:
  assumes "fv (θ x) = {}"
  shows "fv ((θ ∘s σ) x) = {}"
using assms subst_apply_fv_empty
unfolding subst_compose_def by fast

lemma subst_compose_fv':
  fixes θ σ::"('a,'b) subst"
  assumes "y ∈ fv ((θ ∘s σ) x)"
  shows "∃z. z ∈ fv (θ x)"
using assms subst_compose_fv
by fast

lemma subst_apply_fv_unfold: "fv (t ⋅ δ) = fvset (δ ` fv t)"
by (induct t) auto

lemma subst_apply_fv_unfold_set: "fvset (δ ` fvset (set ts)) = fvset (set ts ⋅set δ)"
by (simp add: subst_apply_fv_unfold)

lemma subst_apply_fv_unfold': "fv (t ⋅ δ) = (⋃v ∈ fv t. fv (δ v))"
using subst_apply_fv_unfold by simp

lemma subst_apply_fv_union: "fvset (δ ` V) ∪ fv (t ⋅ δ) = fvset (δ ` (V ∪ fv t))"
proof -
  have "fvset (δ ` (V ∪ fv t)) = fvset (δ ` V) ∪ fvset (δ ` fv t)" by auto
  thus ?thesis using subst_apply_fv_unfold by metis
qed

lemma fvset_subst:
  "fvset (M ⋅set θ) = fvset (θ ` fvset M)"
by (simp add: subst_apply_fv_unfold)

lemma subst_list_set_fv:
  "fvset (set (ts ⋅list θ)) = fvset (θ ` fvset (set ts))"
using subst_apply_fv_unfold_set[of θ ts] by simp

lemma subst_elimI[intro]: "(⋀t. v ∉ fv (t ⋅ σ)) ⟹ subst_elim σ v"
by (auto simp add: subst_elim_def)

lemma subst_elimI'[intro]: "(⋀w. v ∉ fv (Var w ⋅ θ)) ⟹ subst_elim θ v"
by (simp add: subst_elim_def subst_apply_fv_unfold') 

lemma subst_elimD[dest]: "subst_elim σ v ⟹ v ∉ fv (t ⋅ σ)"
by (auto simp add: subst_elim_def)

lemma subst_elimD'[dest]: "subst_elim σ v ⟹ σ v ≠ Var v"
by (metis subst_elim_def eval_term.simps(1) term.set_intros(3))

lemma subst_elimD''[dest]: "subst_elim σ v ⟹ v ∉ fv (σ w)"
by (metis subst_elim_def eval_term.simps(1))

lemma subst_elim_rm_vars_dest[dest]:
  "subst_elim (σ::('a,'b) subst) v ⟹ v ∉ vs ⟹ subst_elim (rm_vars vs σ) v"
proof -
  assume assms: "subst_elim σ v" "v ∉ vs"
  obtain f::"('a, 'b) subst ⇒ 'b ⇒ 'b" where
      "∀σ v. (∃w. v ∈ fv (Var w ⋅ σ)) = (v ∈ fv (Var (f σ v) ⋅ σ))"
    by moura
  hence *: "∀a σ. a ∈ fv (Var (f σ a) ⋅ σ) ∨ subst_elim σ a" by blast
  have "Var (f (rm_vars vs σ) v) ⋅ σ ≠ Var (f (rm_vars vs σ) v) ⋅ rm_vars vs σ
        ∨ v ∉ fv (Var (f (rm_vars vs σ) v) ⋅ rm_vars vs σ)"
    using assms(1) by fastforce
  moreover
  { assume "Var (f (rm_vars vs σ) v) ⋅ σ ≠ Var (f (rm_vars vs σ) v) ⋅ rm_vars vs σ"
    hence "rm_vars vs σ (f (rm_vars vs σ) v) ≠ σ (f (rm_vars vs σ) v)" by auto
    hence "f (rm_vars vs σ) v ∈ vs" by meson
    hence ?thesis using * assms(2) by force
  }
  ultimately show ?thesis using * by blast
qed

lemma occs_subst_elim: "¬Var v ⊏ t ⟹ subst_elim (Var(v := t)) v ∨ (Var(v := t)) = Var"
proof (cases "Var v = t")
  assume "Var v ≠ t" "¬Var v ⊏ t"
  hence "v ∉ fv t" by (simp add: vars_iff_subterm_or_eq)
  thus ?thesis by (auto simp add: subst_remove_var)
qed auto

lemma occs_subst_elim': "¬Var v ⊑ t ⟹ subst_elim (Var(v := t)) v"
proof -
  assume "¬Var v ⊑ t"
  hence "v ∉ fv t" by (auto simp add: vars_iff_subterm_or_eq)
  thus "subst_elim (Var(v := t)) v" by (simp add: subst_elim_def subst_remove_var)
qed

lemma subst_elim_comp: "subst_elim θ v ⟹ subst_elim (δ ∘s θ) v"
by (auto simp add: subst_elim_def)

lemma var_subst_idem: "subst_idem Var"
by (simp add: subst_idem_def)

lemma var_upd_subst_idem:
  assumes "¬Var v ⊑ t" shows "subst_idem (Var(v := t))"
  using subst_no_occs[OF assms] by (simp add: subst_idem_def subst_def[symmetric])

lemma zip_map_subst:
  "zip xs (xs ⋅list δ) = map (λt. (t, t ⋅ δ)) xs"
by (induction xs) auto

lemma map2_map_subst:
  "map2 f xs (xs ⋅list δ) = map (λt. f t (t ⋅ δ)) xs"
by (induction xs) auto


subsection ‹Lemmata: Domain and Range of Substitutions›
lemma range_vars_alt_def: "range_vars s ≡ fvset (subst_range s)"
unfolding range_vars_def by simp

lemma subst_dom_var_finite[simp]: "finite (subst_domain Var)" by simp

lemma subst_range_Var[simp]: "subst_range Var = {}" by simp

lemma range_vars_Var[simp]: "range_vars Var = {}" by fastforce

lemma finite_subst_img_if_finite_dom: "finite (subst_domain σ) ⟹ finite (range_vars σ)"
unfolding range_vars_alt_def by auto

lemma finite_subst_img_if_finite_dom': "finite (subst_domain σ) ⟹ finite (subst_range σ)"
by auto

lemma subst_img_alt_def: "subst_range s = {t. ∃v. s v = t ∧ t ≠ Var v}"
by (auto simp add: subst_domain_def)

lemma subst_fv_img_alt_def: "range_vars s = (⋃t ∈ {t. ∃v. s v = t ∧ t ≠ Var v}. fv t)"
unfolding range_vars_alt_def by (auto simp add: subst_domain_def)

lemma subst_domI[intro]: "σ v ≠ Var v ⟹ v ∈ subst_domain σ"
by (simp add: subst_domain_def)

lemma subst_imgI[intro]: "σ v ≠ Var v ⟹ σ v ∈ subst_range σ"
by (simp add: subst_domain_def)

lemma subst_fv_imgI[intro]: "σ v ≠ Var v ⟹ fv (σ v) ⊆ range_vars σ"
unfolding range_vars_alt_def by auto

lemma subst_eqI':
  assumes "t ⋅ δ = t ⋅ θ" "subst_domain δ = subst_domain θ" "subst_domain δ ⊆ fv t"
  shows "δ = θ"
by (metis assms(2,3) term_subst_eq_rev[OF assms(1)] in_mono ext subst_domI)

lemma subst_domain_subst_Fun_single[simp]:
  "subst_domain (Var(x := Fun f T)) = {x}" (is "?A = ?B")
unfolding subst_domain_def by simp

lemma subst_range_subst_Fun_single[simp]:
  "subst_range (Var(x := Fun f T)) = {Fun f T}" (is "?A = ?B")
by simp

lemma range_vars_subst_Fun_single[simp]:
  "range_vars (Var(x := Fun f T)) = fv (Fun f T)"
unfolding range_vars_alt_def by force

lemma var_renaming_is_Fun_iff:
  assumes "subst_range δ ⊆ range Var"
  shows "is_Fun t = is_Fun (t ⋅ δ)"
proof (cases t)
  case (Var x)
  hence "∃y. δ x = Var y" using assms by auto
  thus ?thesis using Var by auto
qed simp

lemma subst_fv_dom_img_subset: "fv t ⊆ subst_domain θ ⟹ fv (t ⋅ θ) ⊆ range_vars θ"
unfolding range_vars_alt_def by (induct t) auto

lemma subst_fv_dom_img_subset_set: "fvset M ⊆ subst_domain θ ⟹ fvset (M ⋅set θ) ⊆ range_vars θ"
proof -
  assume assms: "fvset M ⊆ subst_domain θ"
  obtain f::"'a set ⇒ (('b, 'a) term ⇒ 'a set) ⇒ ('b, 'a) terms ⇒ ('b, 'a) term" where
      "∀x y z. (∃v. v ∈ z ∧ ¬ y v ⊆ x) ⟷ (f x y z ∈ z ∧ ¬ y (f x y z) ⊆ x)"
    by moura
  hence *:
      "∀T g A. (¬ ⋃ (g ` T) ⊆ A ∨ (∀t. t ∉ T ∨ g t ⊆ A)) ∧
               (⋃ (g ` T) ⊆ A ∨ f A g T ∈ T ∧ ¬ g (f A g T) ⊆ A)"
    by (metis (no_types) SUP_le_iff)
  hence **: "∀t. t ∉ M ∨ fv t ⊆ subst_domain θ" by (metis (no_types) assms fvset.simps)
  have "∀t::('b, 'a) term. ∀f T. t ∉ f ` T ∨ (∃t'::('b, 'a) term. t = f t' ∧ t' ∈ T)" by blast
  hence "f (range_vars θ) fv (M ⋅set θ) ∉ M ⋅set θ ∨
         fv (f (range_vars θ) fv (M ⋅set θ)) ⊆ range_vars θ"
    by (metis (full_types) ** subst_fv_dom_img_subset)
  thus ?thesis by (metis (no_types) * fvset.simps)
qed

lemma subst_fv_dom_ground_if_ground_img:
  assumes "fv t ⊆ subst_domain s" "ground (subst_range s)"
  shows "fv (t ⋅ s) = {}"
using subst_fv_dom_img_subset[OF assms(1)] assms(2) by force

lemma subst_fv_dom_ground_if_ground_img':
  assumes "fv t ⊆ subst_domain s" "⋀x. x ∈ subst_domain s ⟹ fv (s x) = {}"
  shows "fv (t ⋅ s) = {}"
using subst_fv_dom_ground_if_ground_img[OF assms(1)] assms(2) by auto

lemma subst_fv_unfold: "fv (t ⋅ s) = (fv t - subst_domain s) ∪ fvset (s ` (fv t ∩ subst_domain s))"
proof (induction t)
  case (Var v) thus ?case
  proof (cases "v ∈ subst_domain s")
    case True thus ?thesis by auto
  next
    case False
    hence "fv (Var v ⋅ s) = {v}" "fv (Var v) ∩ subst_domain s = {}" by auto
    thus ?thesis by auto
  qed
next
  case Fun thus ?case by auto
qed

lemma subst_fv_unfold_ground_img: "range_vars s = {} ⟹ fv (t ⋅ s) = fv t - subst_domain s"
by (auto simp: range_vars_alt_def subst_fv_unfold)

lemma subst_img_update:
  "⟦σ v = Var v; t ≠ Var v⟧ ⟹ range_vars (σ(v := t)) = range_vars σ ∪ fv t"
proof -
  assume "σ v = Var v" "t ≠ Var v"
  hence "(⋃s ∈ {s. ∃w. (σ(v := t)) w = s ∧ s ≠ Var w}. fv s) = fv t ∪ range_vars σ"
    unfolding range_vars_alt_def by (auto simp add: subst_domain_def)
  thus "range_vars (σ(v := t)) = range_vars σ ∪ fv t"
    by (metis Un_commute subst_fv_img_alt_def)
qed

lemma subst_dom_update1: "v ∉ subst_domain σ ⟹ subst_domain (σ(v := Var v)) = subst_domain σ"
by (auto simp add: subst_domain_def)

lemma subst_dom_update2: "t ≠ Var v ⟹ subst_domain (σ(v := t)) = insert v (subst_domain σ)"
by (auto simp add: subst_domain_def)

lemma subst_dom_update3: "t = Var v ⟹ subst_domain (σ(v := t)) = subst_domain σ - {v}"
by (auto simp add: subst_domain_def)

lemma var_not_in_subst_dom[elim]: "v ∉ subst_domain s ⟹ s v = Var v"
by (simp add: subst_domain_def)

lemma subst_dom_vars_in_subst[elim]: "v ∈ subst_domain s ⟹ s v ≠ Var v"
by (simp add: subst_domain_def)

lemma subst_not_dom_fixed: "⟦v ∈ fv t; v ∉ subst_domain s⟧ ⟹ v ∈ fv (t ⋅ s)" by (induct t) auto

lemma subst_not_img_fixed: "⟦v ∈ fv (t ⋅ s); v ∉ range_vars s⟧ ⟹ v ∈ fv t"
unfolding range_vars_alt_def by (induct t) force+

lemma ground_range_vars[intro]: "ground (subst_range s) ⟹ range_vars s = {}"
unfolding range_vars_alt_def by metis

lemma ground_subst_no_var[intro]: "ground (subst_range s) ⟹ x ∉ range_vars s"
using ground_range_vars[of s] by blast

lemma ground_img_obtain_fun:
  assumes "ground (subst_range s)" "x ∈ subst_domain s"
  obtains f T where "s x = Fun f T" "Fun f T ∈ subst_range s" "fv (Fun f T) = {}"
proof -
  from assms(2) obtain t where t: "s x = t" "t ∈ subst_range s" by atomize_elim auto
  hence "fv t = {}" using assms(1) by auto
  thus ?thesis using t that by (cases t) simp_all
qed

lemma ground_term_subst_domain_fv_subset:
  "fv (t ⋅ δ) = {} ⟹ fv t ⊆ subst_domain δ"
by (induct t) auto

lemma ground_subst_range_empty_fv:
  "ground (subst_range θ) ⟹ x ∈ subst_domain θ ⟹ fv (θ x) = {}"
by simp

lemma subst_Var_notin_img: "x ∉ range_vars s ⟹ t ⋅ s = Var x ⟹ t = Var x"
using subst_not_img_fixed[of x t s] by (induct t) auto

lemma fv_in_subst_img: "⟦s v = t; t ≠ Var v⟧ ⟹ fv t ⊆ range_vars s"
unfolding range_vars_alt_def by auto

lemma empty_dom_iff_empty_subst: "subst_domain θ = {} ⟷ θ = Var" by auto

lemma subst_dom_cong: "(⋀v t. θ v = t ⟹ δ v = t) ⟹ subst_domain θ ⊆ subst_domain δ"
by (auto simp add: subst_domain_def)

lemma subst_img_cong: "(⋀v t. θ v = t ⟹ δ v = t) ⟹ range_vars θ ⊆ range_vars δ"
unfolding range_vars_alt_def by (auto simp add: subst_domain_def)

lemma subst_dom_elim: "subst_domain s ∩ range_vars s = {} ⟹ fv (t ⋅ s) ∩ subst_domain s = {}"
proof (induction t)
  case (Var v) thus ?case
    using fv_in_subst_img[of s] 
    by (cases "s v = Var v") (auto simp add: subst_domain_def)
next
  case Fun thus ?case by auto
qed

lemma subst_dom_insert_finite: "finite (subst_domain s) = finite (subst_domain (s(v := t)))"
proof
  assume "finite (subst_domain s)"
  have "subst_domain (s(v := t)) ⊆ insert v (subst_domain s)" by (auto simp add: subst_domain_def)
  thus "finite (subst_domain (s(v := t)))"
    by (meson ‹finite (subst_domain s)› finite_insert rev_finite_subset)
next
  assume *: "finite (subst_domain (s(v := t)))"
  hence "finite (insert v (subst_domain s))"
  proof (cases "t = Var v")
    case True
    hence "finite (subst_domain s - {v})" by (metis * subst_dom_update3)
    thus ?thesis by simp
  qed (metis * subst_dom_update2[of t v s])
  thus "finite (subst_domain s)" by simp
qed

lemma trm_subst_disj: "t ⋅ θ = t ⟹ fv t ∩ subst_domain θ = {}"
proof (induction t)
  case (Fun f X)
  hence "map (λx. x ⋅ θ) X = X" by simp
  hence "⋀x. x ∈ set X ⟹ x ⋅ θ = x" using map_eq_conv by fastforce
  thus ?case using Fun.IH by auto
qed (simp add: subst_domain_def)

declare subst_apply_term_ident[intro]

lemma trm_subst_ident'[intro]: "v ∉ subst_domain θ ⟹ (Var v) ⋅ θ = Var v"
using subst_apply_term_ident by (simp add: subst_domain_def)

lemma trm_subst_ident''[intro]: "(⋀x. x ∈ fv t ⟹ θ x = Var x) ⟹ t ⋅ θ = t"
proof -
  assume "⋀x. x ∈ fv t ⟹ θ x = Var x"
  hence "fv t ∩ subst_domain θ = {}" by (auto simp add: subst_domain_def)
  thus ?thesis using subst_apply_term_ident by auto
qed

lemma set_subst_ident: "fvset M ∩ subst_domain θ = {} ⟹ M ⋅set θ = M"
proof -
  assume "fvset M ∩ subst_domain θ = {}"
  hence "∀t ∈ M. t ⋅ θ = t" by auto
  thus ?thesis by force
qed

lemma trm_subst_ident_subterms[intro]:
  "fv t ∩ subst_domain θ = {} ⟹ subterms t ⋅set θ = subterms t"
using set_subst_ident[of "subterms t" θ] fv_subterms[of t] by simp

lemma trm_subst_ident_subterms'[intro]:
  "v ∉ fv t ⟹ subterms t ⋅set Var(v := s) = subterms t"
using trm_subst_ident_subterms[of t "Var(v := s)"]
by (meson subst_no_occs trm_subst_disj vars_iff_subtermeq) 

lemma const_mem_subst_cases:
  assumes "Fun c [] ∈ M ⋅set θ"
  shows "Fun c [] ∈ M ∨ Fun c [] ∈ θ ` fvset M"
proof -
  obtain m where m: "m ∈ M" "m ⋅ θ = Fun c []" using assms by auto
  thus ?thesis by (cases m) force+
qed

lemma const_mem_subst_cases':
  assumes "Fun c [] ∈ M ⋅set θ"
  shows "Fun c [] ∈ M ∨ Fun c [] ∈ subst_range θ"
using const_mem_subst_cases[OF assms] by force

lemma fv_subterms_substI[intro]: "y ∈ fv t ⟹ θ y ∈ subterms t ⋅set θ"
using image_iff vars_iff_subtermeq by fastforce 

lemma fv_subterms_subst_eq[simp]: "fvset (subterms (t ⋅ θ)) = fvset (subterms t ⋅set θ)"
using fv_subterms by (induct t) force+

lemma fv_subterms_set_subst: "fvset (subtermsset M ⋅set θ) = fvset (subtermsset (M ⋅set θ))"
using fv_subterms_subst_eq[of _ θ] by auto

lemma fv_subterms_set_subst': "fvset (subtermsset M ⋅set θ) = fvset (M ⋅set θ)"
using fv_subterms_set[of "M ⋅set θ"] fv_subterms_set_subst[of θ M] by simp

lemma fv_subst_subset: "x ∈ fv t ⟹ fv (θ x) ⊆ fv (t ⋅ θ)"
by (metis fv_subset image_eqI subst_apply_fv_unfold)

lemma fv_subst_subset': "fv s ⊆ fv t ⟹ fv (s ⋅ θ) ⊆ fv (t ⋅ θ)"
using fv_subst_subset by (induct s) force+

lemma fv_subst_obtain_var:
  fixes δ::"('a,'b) subst"
  assumes "x ∈ fv (t ⋅ δ)"
  shows "∃y ∈ fv t. x ∈ fv (δ y)"
using assms by (induct t) force+

lemma set_subst_all_ident: "fvset (M ⋅set θ) ∩ subst_domain δ = {} ⟹ M ⋅set (θ ∘s δ) = M ⋅set θ"
by (metis set_subst_ident subst_comp_all)

lemma subterms_subst:
  "subterms (t ⋅ d) = (subterms t ⋅set d) ∪ subtermsset (d ` (fv t ∩ subst_domain d))"
by (induct t) (auto simp add: subst_domain_def)

lemma subterms_subst':
  fixes θ::"('a,'b) subst"
  assumes "∀x ∈ fv t. (∃f. θ x = Fun f []) ∨ (∃y. θ x = Var y)"
  shows "subterms (t ⋅ θ) = subterms t ⋅set θ"
using assms
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x ∈ subst_domain θ")
    case True
    hence "(∃f. θ x = Fun f []) ∨ (∃y. θ x = Var y)" using Var by simp
    hence "subterms (θ x) = {θ x}" by auto
    thus ?thesis by simp
  qed auto
qed auto

lemma subterms_subst'':
  fixes θ::"('a,'b) subst"
  assumes "∀x ∈ fvset M. (∃f. θ x = Fun f []) ∨ (∃y. θ x = Var y)"
  shows "subtermsset (M ⋅set θ) = subtermsset M ⋅set θ"
using subterms_subst'[of _ θ] assms by auto

lemma subterms_subst_subterm:
  fixes θ::"('a,'b) subst"
  assumes "∀x ∈ fv a. (∃f. θ x = Fun f []) ∨ (∃y. θ x = Var y)"
    and "b ∈ subterms (a ⋅ θ)"
  shows "∃c ∈ subterms a. c ⋅ θ = b"
using subterms_subst'[OF assms(1)] assms(2) by auto

lemma subterms_subst_subset: "subterms t ⋅set σ ⊆ subterms (t ⋅ σ)"
by (induct t) auto

lemma subterms_subst_subset': "subtermsset M ⋅set σ ⊆ subtermsset (M ⋅set σ)"
using subterms_subst_subset by fast

lemma subtermsset_subst:
  fixes θ::"('a,'b) subst"
  assumes "t ∈ subtermsset (M ⋅set θ)"
  shows "t ∈ subtermsset M ⋅set θ ∨ (∃x ∈ fvset M. t ∈ subterms (θ x))"
using assms subterms_subst[of _ θ] by auto

lemma rm_vars_dom: "subst_domain (rm_vars V s) = subst_domain s - V"
by (auto simp add: subst_domain_def)

lemma rm_vars_dom_subset: "subst_domain (rm_vars V s) ⊆ subst_domain s"
by (auto simp add: subst_domain_def)

lemma rm_vars_dom_eq':
  "subst_domain (rm_vars (UNIV - V) s) = subst_domain s ∩ V"
using rm_vars_dom[of "UNIV - V" s] by blast

lemma rm_vars_dom_eqI:
  assumes "t ⋅ δ = t ⋅ θ"
  shows "subst_domain (rm_vars (UNIV - fv t) δ) = subst_domain (rm_vars (UNIV - fv t) θ)"
by (meson assms Diff_iff UNIV_I term_subst_eq_rev)

lemma rm_vars_img: "subst_range (rm_vars V s) = s ` subst_domain (rm_vars V s)"
by (auto simp add: subst_domain_def)

lemma rm_vars_img_subset: "subst_range (rm_vars V s) ⊆ subst_range s"
by (auto simp add: subst_domain_def)

lemma rm_vars_img_fv_subset: "range_vars (rm_vars V s) ⊆ range_vars s"
unfolding range_vars_alt_def by (auto simp add: subst_domain_def)

lemma rm_vars_fv_obtain:
  assumes "x ∈ fv (t ⋅ rm_vars X θ) - X"
  shows "∃y ∈ fv t - X. x ∈ fv (rm_vars X θ y)"
using assms by (induct t) (fastforce, force)

lemma rm_vars_apply: "v ∈ subst_domain (rm_vars V s) ⟹ (rm_vars V s) v = s v"
by (auto simp add: subst_domain_def)

lemma rm_vars_apply': "subst_domain δ ∩ vs = {} ⟹ rm_vars vs δ = δ"
by force

lemma rm_vars_ident: "fv t ∩ vs = {} ⟹ t ⋅ (rm_vars vs θ) = t ⋅ θ"
by (induct t) auto

lemma rm_vars_fv_subset: "fv (t ⋅ rm_vars X θ) ⊆ fv t ∪ fv (t ⋅ θ)"
by (induct t) auto

lemma rm_vars_fv_disj:
  assumes "fv t ∩ X = {}" "fv (t ⋅ θ) ∩ X = {}"
  shows "fv (t ⋅ rm_vars X θ) ∩ X = {}"
using rm_vars_ident[OF assms(1)] assms(2) by auto

lemma rm_vars_ground_supports:
  assumes "ground (subst_range θ)"
  shows "rm_vars X θ supports θ"
proof
  fix x
  have *: "ground (subst_range (rm_vars X θ))"
    using rm_vars_img_subset[of X θ] assms
    by (auto simp add: subst_domain_def)
  show "rm_vars X θ x ⋅ θ = θ x "
  proof (cases "x ∈ subst_domain (rm_vars X θ)")
    case True
    hence "fv (rm_vars X θ x) = {}" using * by auto
    thus ?thesis using True by auto
  qed (simp add: subst_domain_def)
qed

lemma rm_vars_split:
  assumes "ground (subst_range θ)"
  shows "θ = rm_vars X θ ∘s rm_vars (subst_domain θ - X) θ"
proof -
  let ?s1 = "rm_vars X θ"
  let ?s2 = "rm_vars (subst_domain θ - X) θ"

  have doms: "subst_domain ?s1 ⊆ subst_domain θ" "subst_domain ?s2 ⊆ subst_domain θ"
    by (auto simp add: subst_domain_def)

  { fix x assume "x ∉ subst_domain θ"
    hence "θ x = Var x" "?s1 x = Var x" "?s2 x = Var x" using doms by auto
    hence "θ x = (?s1 ∘s ?s2) x" by (simp add: subst_compose_def)
  } moreover {
    fix x assume "x ∈ subst_domain θ" "x ∈ X"
    hence "?s1 x = Var x" "?s2 x = θ x" using doms by auto
    hence "θ x = (?s1 ∘s ?s2) x" by (simp add: subst_compose_def)
  } moreover {
    fix x assume "x ∈ subst_domain θ" "x ∉ X"
    hence "?s1 x = θ x" "fv (θ x) = {}" using assms doms by auto
    hence "θ x = (?s1 ∘s ?s2) x" by (simp add: subst_compose subst_ground_ident)
  } ultimately show ?thesis by blast
qed

lemma rm_vars_fv_img_disj:
  assumes "fv t ∩ X = {}" "X ∩ range_vars θ = {}"
  shows "fv (t ⋅ rm_vars X θ) ∩ X = {}"
using assms
proof (induction t)
  case (Var x)
  hence *: "(rm_vars X θ) x = θ x" by auto
  show ?case
  proof (cases "x ∈ subst_domain θ")
    case True
    hence "θ x ∈ subst_range θ" by auto
    hence "fv (θ x) ∩ X = {}" using Var.prems(2) unfolding range_vars_alt_def by fastforce
    thus ?thesis using * by auto
  next
    case False thus ?thesis using Var.prems(1) by auto
  qed
next
  case Fun thus ?case by auto
qed

lemma subst_apply_dom_ident: "t ⋅ θ = t ⟹ subst_domain δ ⊆ subst_domain θ ⟹ t ⋅ δ = t"
proof (induction t)
  case (Fun f T) thus ?case by (induct T) auto
qed (auto simp add: subst_domain_def)

lemma rm_vars_subst_apply_ident:
  assumes "t ⋅ θ = t"
  shows "t ⋅ (rm_vars vs θ) = t"
using rm_vars_dom[of vs θ] subst_apply_dom_ident[OF assms, of "rm_vars vs θ"] by auto

lemma rm_vars_subst_eq:
  "t ⋅ δ = t ⋅ rm_vars (subst_domain δ - subst_domain δ ∩ fv t) δ"
by (auto intro: term_subst_eq)

lemma rm_vars_subst_eq':
  "t ⋅ δ = t ⋅ rm_vars (UNIV - fv t) δ"
by (auto intro: term_subst_eq)

lemma rm_vars_comp:
  assumes "range_vars δ ∩ vs = {}"
  shows "t ⋅ rm_vars vs (δ ∘s θ) = t ⋅ (rm_vars vs δ ∘s rm_vars vs θ)"
using assms
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x ∈ vs")
    case True thus ?thesis using Var
      by (simp add: subst_compose_def)
  next
    case False
    have "subst_domain (rm_vars vs θ) ∩ vs = {}" by (auto simp add: subst_domain_def)
    moreover have "fv (δ x) ∩ vs = {}"
      using Var False unfolding range_vars_alt_def by force
    ultimately have "δ x ⋅ (rm_vars vs θ) = δ x ⋅ θ"
      using rm_vars_ident by (simp add: subst_domain_def)
    moreover have "(rm_vars vs (δ ∘s θ)) x = (δ ∘s θ) x" by (metis False)
    ultimately show ?thesis by (auto simp: subst_compose)
  qed
next
  case Fun thus ?case by auto
qed

lemma rm_vars_fvset_subst:
  assumes "x ∈ fvset (rm_vars X θ ` Y)"
  shows "x ∈ fvset (θ ` Y) ∨ x ∈ X"
using assms by auto

lemma disj_dom_img_var_notin:
  assumes "subst_domain θ ∩ range_vars θ = {}" "θ v = t" "t ≠ Var v"
  shows "v ∉ fv t" "∀v ∈ fv (t ⋅ θ). v ∉ subst_domain θ"
proof -
  have "v ∈ subst_domain θ" "fv t ⊆ range_vars θ"
    using fv_in_subst_img[of θ v t, OF assms(2)] assms(2,3)
    by (auto simp add: subst_domain_def)
  thus "v ∉ fv t" using assms(1) by auto

  have *: "fv t ∩ subst_domain θ = {}"
    using assms(1) ‹fv t ⊆ range_vars θ›
    by auto
  hence "t ⋅ θ = t" by blast
  thus "∀v ∈ fv (t ⋅ θ). v ∉ subst_domain θ" using * by auto
qed

lemma subst_sends_dom_to_img: "v ∈ subst_domain θ ⟹ fv (Var v ⋅ θ) ⊆ range_vars θ"
unfolding range_vars_alt_def by auto

lemma subst_sends_fv_to_img: "fv (t ⋅ s) ⊆ fv t ∪ range_vars s"
proof (induction t)
  case (Var v) thus ?case
  proof (cases "Var v ⋅ s = Var v")
    case True thus ?thesis by simp
  next
    case False
    hence "v ∈ subst_domain s" by (meson trm_subst_ident') 
    hence "fv (Var v ⋅ s) ⊆ range_vars s"
      using subst_sends_dom_to_img by simp
    thus ?thesis by auto
  qed
next
  case Fun thus ?case by auto
qed 

lemma ident_comp_subst_trm_if_disj:
  assumes "subst_domain σ ∩ range_vars θ = {}" "v ∈ subst_domain θ"
  shows "(θ ∘s σ) v = θ v"
proof -
  from assms have " subst_domain σ ∩ fv (θ v) = {}"
    using fv_in_subst_img unfolding range_vars_alt_def by auto
  thus "(θ ∘s σ) v = θ v" unfolding subst_compose_def by blast
qed

lemma ident_comp_subst_trm_if_disj': "fv (θ v) ∩ subst_domain σ = {} ⟹ (θ ∘s σ) v = θ v"
unfolding subst_compose_def by blast

lemma subst_idemI[intro]: "subst_domain σ ∩ range_vars σ = {} ⟹ subst_idem σ"
using ident_comp_subst_trm_if_disj[of σ σ]
      var_not_in_subst_dom[of _ σ]
      subst_eq_if_eq_vars[of σ]
by (metis subst_idem_def subst_compose_def var_comp(2)) 

lemma subst_idemI'[intro]: "ground (subst_range σ) ⟹ subst_idem σ"
proof (intro subst_idemI)
  assume "ground (subst_range σ)"
  hence "range_vars σ = {}" by (metis ground_range_vars)
  thus "subst_domain σ ∩ range_vars σ = {}" by blast
qed

lemma subst_idemE: "subst_idem σ ⟹ subst_domain σ ∩ range_vars σ = {}"
proof -
  assume "subst_idem σ"
  hence "⋀v. fv (σ v) ∩ subst_domain σ = {}"
    unfolding subst_idem_def subst_compose_def by (metis trm_subst_disj)
  thus ?thesis
    unfolding range_vars_alt_def by auto
qed

lemma subst_idem_rm_vars: "subst_idem θ ⟹ subst_idem (rm_vars X θ)"
proof -
  assume "subst_idem θ"
  hence "subst_domain θ ∩ range_vars θ = {}" by (metis subst_idemE)
  moreover have
      "subst_domain (rm_vars X θ) ⊆ subst_domain θ"
      "range_vars (rm_vars X θ) ⊆ range_vars θ"
    unfolding range_vars_alt_def by (auto simp add: subst_domain_def)
  ultimately show ?thesis by blast
qed

lemma subst_fv_bounded_if_img_bounded: "range_vars θ ⊆ fv t ∪ V ⟹ fv (t ⋅ θ) ⊆ fv t ∪ V"
proof (induction t)
  case (Var v) thus ?case unfolding range_vars_alt_def by (cases "θ 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 ⋅ Var(v := t')) ⊆ fv t ∪ fv t'"
using subst_fv_bounded_if_img_bounded[of "Var(v := t')" t "fv t'"]
unfolding range_vars_alt_def by (auto simp add: subst_domain_def)

lemma subst_fv_bounded_if_img_bounded':
  assumes "range_vars θ ⊆ fvset M"
  shows "fvset (M ⋅set θ) ⊆ fvset M"
proof
  fix v assume *:  "v ∈ fvset (M ⋅set θ)"
  
  obtain t where t: "t ∈ M" "t ⋅ θ ∈ M ⋅set θ" "v ∈ fv (t ⋅ θ)"
  proof -
    assume **: "⋀t. ⟦t ∈ M; t ⋅ θ ∈ M ⋅set θ; v ∈ fv (t ⋅ θ)⟧ ⟹ thesis"
    have "v ∈ ⋃ (fv ` ((λt. t ⋅ θ) ` M))" using * by (metis fvset.simps)
    hence "∃t. t ∈ M ∧ v ∈ fv (t ⋅ θ)" by blast
    thus ?thesis using ** imageI by blast
  qed

  from ‹t ∈ M› obtain M' where "t ∉ M'" "M = insert t M'" by (meson Set.set_insert) 
  hence "fvset M = fv t ∪ fvset M'" by simp
  hence "fv (t ⋅ θ) ⊆ fvset M" using subst_fv_bounded_if_img_bounded assms by simp
  thus "v ∈ fvset M" using assms ‹v ∈ fv (t ⋅ θ)› by auto
qed

lemma ground_img_if_ground_subst: "(⋀v t. s v = t ⟹ fv t = {}) ⟹ range_vars s = {}"
unfolding range_vars_alt_def by auto

lemma ground_subst_fv_subset: "ground (subst_range θ) ⟹ fv (t ⋅ θ) ⊆ fv t"
using subst_fv_bounded_if_img_bounded[of θ]
unfolding range_vars_alt_def by force

lemma ground_subst_fv_subset': "ground (subst_range θ) ⟹ fvset (M ⋅set θ) ⊆ fvset M"
using subst_fv_bounded_if_img_bounded'[of θ M]
unfolding range_vars_alt_def by auto

lemma subst_to_var_is_var[elim]: "t ⋅ s = Var v ⟹ ∃w. t = Var w"
by (auto elim!: eval_term.elims)

lemma subst_dom_comp_inI:
  assumes "y ∉ subst_domain σ"
    and "y ∈ subst_domain δ"
  shows "y ∈ subst_domain (σ ∘s δ)"
using assms subst_domain_subst_compose[of σ δ] by blast

lemma subst_comp_notin_dom_eq:
  "x ∉ subst_domain θ1 ⟹ (θ1 ∘s θ2) x = θ2 x"
unfolding subst_compose_def by fastforce

lemma subst_dom_comp_eq:
  assumes "subst_domain θ ∩ range_vars σ = {}"
  shows "subst_domain (θ ∘s σ) = subst_domain θ ∪ subst_domain σ"
proof (rule ccontr)
  assume "subst_domain (θ ∘s σ) ≠ subst_domain θ ∪ subst_domain σ"
  hence "subst_domain (θ ∘s σ) ⊂ subst_domain θ ∪ subst_domain σ"
    using subst_domain_compose[of θ σ] by (simp add: subst_domain_def)
  then obtain v where "v ∉ subst_domain (θ ∘s σ)" "v ∈ subst_domain θ ∪ subst_domain σ" by auto
  hence v_in_some_subst: "θ v ≠ Var v ∨ σ v ≠ Var v" and "θ v ⋅ σ = Var v"
    unfolding subst_compose_def by (auto simp add: subst_domain_def)
  then obtain w where "θ v = Var w" using subst_to_var_is_var by fastforce
  show False
  proof (cases "v = w")
    case True
    hence "θ v = Var v" using ‹θ v = Var w› by simp
    hence "σ v ≠ Var v" using v_in_some_subst by simp
    thus False using ‹θ v = Var v› ‹θ v ⋅ σ = Var v› by simp
  next
    case False
    hence "v ∈ subst_domain θ" using v_in_some_subst ‹θ v ⋅ σ = Var v› by auto 
    hence "v ∉ range_vars σ" using assms by auto
    moreover have "σ w = Var v" using ‹θ v ⋅ σ = Var v› ‹θ v = Var w› by simp
    hence "v ∈ range_vars σ" using ‹v ≠ w› subst_fv_imgI[of σ w] by simp
    ultimately show False ..
  qed
qed

lemma subst_img_comp_subset[simp]:
  "range_vars (θ1 ∘s θ2) ⊆ range_vars θ1 ∪ range_vars θ2"
proof
  let ?img = "range_vars"
  fix x assume "x ∈ ?img (θ1 ∘s θ2)"
  then obtain v t where vt: "x ∈ fv t" "t = (θ1 ∘s θ2) v" "t ≠ Var v"
    unfolding range_vars_alt_def subst_compose_def by (auto simp add: subst_domain_def)

  { assume "x ∉ ?img θ1" hence "x ∈ ?img θ2"
      by (metis (no_types, opaque_lifting) fv_in_subst_img Un_iff subst_compose_def 
                vt subsetCE eval_term.simps(1) subst_sends_fv_to_img)
  }
  thus "x ∈ ?img θ1 ∪ ?img θ2" by auto
qed

lemma subst_img_comp_subset':
  assumes "t ∈ subst_range (θ1 ∘s θ2)"
  shows "t ∈ subst_range θ2 ∨ (∃t' ∈ subst_range θ1. t = t' ⋅ θ2)"
proof -
  obtain x where x: "x ∈ subst_domain (θ1 ∘s θ2)" "(θ1 ∘s θ2) x = t" "t ≠ Var x"
    using assms by (auto simp add: subst_domain_def)
  { assume "x ∉ subst_domain θ1"
    hence "(θ1 ∘s θ2) x = θ2 x" unfolding subst_compose_def by auto
    hence ?thesis using x by auto
  } moreover {
    assume "x ∈ subst_domain θ1" hence ?thesis using subst_compose x(2) by fastforce 
  } ultimately show ?thesis by metis
qed

lemma subst_img_comp_subset'':
  "subtermsset (subst_range (θ1 ∘s θ2)) ⊆
   subtermsset (subst_range θ2) ∪ ((subtermsset (subst_range θ1)) ⋅set θ2)"
proof
  fix t assume "t ∈ subtermsset (subst_range (θ1 ∘s θ2))"
  then obtain x where x: "x ∈ subst_domain (θ1 ∘s θ2)" "t ∈ subterms ((θ1 ∘s θ2) x)"
    by auto
  show "t ∈ subtermsset (subst_range θ2) ∪ (subtermsset (subst_range θ1) ⋅set θ2)"
  proof (cases "x ∈ subst_domain θ1")
    case True thus ?thesis
      using subst_compose[of θ1 θ2] x(2) subterms_subst
      by fastforce
  next
    case False
    hence "(θ1 ∘s θ2) x = θ2 x" unfolding subst_compose_def by auto
    thus ?thesis using x by (auto simp add: subst_domain_def)
  qed
qed

lemma subst_img_comp_subset''':
  "subtermsset (subst_range (θ1 ∘s θ2)) - range Var ⊆
   subtermsset (subst_range θ2) - range Var ∪ ((subtermsset (subst_range θ1) - range Var) ⋅set θ2)"
proof
  fix t assume t: "t ∈ subtermsset (subst_range (θ1 ∘s θ2)) - range Var"
  then obtain f T where fT: "t = Fun f T" by (cases t) simp_all
  then obtain x where x: "x ∈ subst_domain (θ1 ∘s θ2)" "Fun f T ∈ subterms ((θ1 ∘s θ2) x)"
    using t by auto
  have "Fun f T ∈ subtermsset (subst_range θ2) ∪ (subtermsset (subst_range θ1) - range Var ⋅set θ2)"
  proof (cases "x ∈ subst_domain θ1")
    case True
    hence "Fun f T ∈ (subtermsset (subst_range θ2)) ∪ (subterms (θ1 x) ⋅set θ2)"
      using x(2)
      by (auto simp: subst_compose subterms_subst)
    moreover have ?thesis when *: "Fun f T ∈ subterms (θ1 x) ⋅set θ2"
    proof -
      obtain s where s: "s ∈ subterms (θ1 x)" "Fun f T = s ⋅ θ2" using * by atomize_elim auto
      show ?thesis
      proof (cases s)
        case (Var y)
        hence "Fun f T ∈ subst_range θ2" using s by force
        thus ?thesis by blast
      next
        case (Fun g S)
        hence "Fun f T ∈ (subterms (θ1 x) - range Var) ⋅set θ2" using s by blast
        thus ?thesis using True by auto
      qed
    qed
    ultimately show ?thesis by blast
  next
    case False
    hence "(θ1 ∘s θ2) x = θ2 x" unfolding subst_compose_def by auto
    thus ?thesis using x by (auto simp add: subst_domain_def)
  qed
  thus "t ∈ subtermsset (subst_range θ2) - range Var ∪
            (subtermsset (subst_range θ1) - range Var ⋅set θ2)"
    using fT by auto
qed

lemma subst_img_comp_subset_const:
  assumes "Fun c [] ∈ subst_range (θ1 ∘s θ2)"
  shows "Fun c [] ∈ subst_range θ2 ∨ Fun c [] ∈ subst_range θ1 ∨
         (∃x. Var x ∈ subst_range θ1 ∧ θ2 x = Fun c [])"
proof (cases "Fun c [] ∈ subst_range θ2")
  case False
  then obtain t where t: "t ∈ subst_range θ1" "Fun c [] = t ⋅ θ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 δ τ::"('f,'v) subst"
  assumes "(δ ∘s τ) x = Fun c []"
  shows "δ x = Fun c [] ∨ (∃z. δ x = Var z ∧ τ z = Fun c [])"
proof (cases "δ x = Fun c []")
  case False
  then obtain t where "δ x = t" "t ⋅ τ = Fun c []" using assms unfolding subst_compose_def by auto
  thus ?thesis by (cases t) auto
qed simp

lemma subst_img_comp_subset_ground:
  assumes "ground (subst_range θ1)"
  shows "subst_range (θ1 ∘s θ2) ⊆ subst_range θ1 ∪ subst_range θ2"
proof
  fix t assume t: "t ∈ subst_range (θ1 ∘s θ2)"
  then obtain x where x: "x ∈ subst_domain (θ1 ∘s θ2)" "t = (θ1 ∘s θ2) x" by auto

  show "t ∈ subst_range θ1 ∪ subst_range θ2"
  proof (cases "x ∈ subst_domain θ1")
    case True
    hence "fv (θ1 x) = {}" using assms ground_subst_range_empty_fv by fast
    hence "t = θ1 x" using x(2) unfolding subst_compose_def by blast
    thus ?thesis using True by simp
  next
    case False
    hence "t = θ2 x" "x ∈ subst_domain θ2"
      using x subst_domain_compose[of θ1 θ2]
      by (metis subst_comp_notin_dom_eq, blast)
    thus ?thesis using x by simp
  qed
qed

lemma subst_fv_dom_img_single:
  assumes "v ∉ fv t" "σ v = t" "⋀w. v ≠ w ⟹ σ w = Var w"
  shows "subst_domain σ = {v}" "range_vars σ = fv t"
proof -
  show "subst_domain σ = {v}" using assms by (fastforce simp add: subst_domain_def)
  have "fv t ⊆ range_vars σ" by (metis fv_in_subst_img assms(1,2) vars_iff_subterm_or_eq) 
  moreover have "⋀v. σ v ≠ Var v ⟹ σ v = t" using assms by fastforce
  ultimately show "range_vars σ = fv t"
    unfolding range_vars_alt_def
    by (auto simp add: subst_domain_def)
qed

lemma subst_comp_upd1:
  "θ(v := t) ∘s σ = (θ ∘s σ)(v := t ⋅ σ)"
unfolding subst_compose_def by auto

lemma subst_comp_upd2:
  assumes "v ∉ subst_domain s" "v ∉ range_vars s"
  shows "s(v := t) = s ∘s (Var(v := t))"
unfolding subst_compose_def
proof -
  { fix w
    have "(s(v := t)) w = s w ⋅ Var(v := t)"
    proof (cases "w = v")
      case True
      hence "s w = Var w" using ‹v ∉ subst_domain s› by (simp add: subst_domain_def)
      thus ?thesis using ‹w = v› by simp
    next
      case False
      hence "(s(v := t)) w = s w" by simp
      moreover have "s w ⋅ Var(v := t) = s w" using ‹w ≠ v› ‹v ∉ range_vars s› 
        by (metis fv_in_subst_img fun_upd_apply insert_absorb insert_subset
                  repl_invariance eval_term.simps(1) subst_apply_term_empty)
      ultimately show ?thesis ..
    qed
  }
  thus "s(v := t) = (λw. s w ⋅ Var(v := t))" by auto
qed

lemma ground_subst_dom_iff_img:
  "ground (subst_range σ) ⟹ x ∈ subst_domain σ ⟷ σ x ∈ subst_range σ"
by (auto simp add: subst_domain_def)

lemma finite_dom_subst_exists:
  "finite S ⟹ ∃σ::('f,'v) subst. subst_domain σ = S"
proof (induction S rule: finite.induct)
  case (insertI A a)
  then obtain σ::"('f,'v) subst" where "subst_domain σ = A" by blast
  fix f::'f
  have "subst_domain (σ(a := Fun f [])) = insert a A"
    using ‹subst_domain σ = A›
    by (auto simp add: subst_domain_def)
  thus ?case by metis
qed (auto simp add: subst_domain_def)

lemma subst_inj_is_bij_betw_dom_img_if_ground_img:
  assumes "ground (subst_range σ)"
  shows "inj σ ⟷ bij_betw σ (subst_domain σ) (subst_range σ)" (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B" by (metis bij_betw_def injD inj_onI subst_range.simps)
next
  assume ?B
  hence "inj_on σ (subst_domain σ)" unfolding bij_betw_def by auto
  moreover have "⋀x. x ∈ UNIV - subst_domain σ ⟹ σ x = Var x" by auto
  hence "inj_on σ (UNIV - subst_domain σ)"
    using inj_onI[of "UNIV - subst_domain σ"]
    by (metis term.inject(1))
  moreover have "⋀x y. x ∈ subst_domain σ ⟹ y ∉ subst_domain σ ⟹ σ x ≠ σ y"
    using assms by (auto simp add: subst_domain_def)
  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 "∃σ::('f,'v) subst. subst_domain σ = S
                          ∧ bij_betw σ (subst_domain σ) (subst_range σ)
                          ∧ subst_range σ ⊆ U"
proof -
  obtain T' where "T' ⊆ U" "card T' = card S" "finite T'"
    by (meson assms(2) finite_Diff2 infinite_arbitrarily_large)
  then obtain f::"'v ⇒ ('f,'v) term" where f_bij: "bij_betw f S T'"
    using finite_same_card_bij[OF assms(1)] by metis
  hence *: "⋀v. v ∈ S ⟹ f v ≠ Var v"
    using ‹ground U› ‹T' ⊆ U› bij_betwE
    by fastforce

  let ?σ = "λv. if v ∈ S then f v else Var v"
  have "subst_domain ?σ = S"
  proof
    show "subst_domain ?σ ⊆ S" by (auto simp add: subst_domain_def)

    { fix v assume "v ∈ S" "v ∉ subst_domain ?σ"
      hence "f v = Var v" by (simp add: subst_domain_def)
      hence False using *[OF ‹v ∈ S›] by metis
    }
    thus "S ⊆ subst_domain ?σ" by blast
  qed
  hence "⋀v w. ⟦v ∈ subst_domain ?σ; w ∉ subst_domain ?σ⟧ ⟹ ?σ w ≠ ?σ v"
    using ‹ground U› bij_betwE[OF f_bij] set_rev_mp[OF _ ‹T' ⊆ U›]
    by (metis (no_types, lifting) UN_iff empty_iff vars_iff_subterm_or_eq fvset.simps) 
  hence "inj_on ?σ (subst_domain ?σ)"
    using f_bij ‹subst_domain ?σ = S›
    unfolding bij_betw_def inj_on_def
    by metis
  hence "bij_betw ?σ (subst_domain ?σ) (subst_range ?σ)"
    using inj_on_imp_bij_betw[of ?σ] by simp
  moreover have "subst_range ?σ = T'"
    using ‹bij_betw f S T'› ‹subst_domain ?σ = S›
    unfolding bij_betw_def by auto 
  hence "subst_range ?σ ⊆ U" using ‹T' ⊆ U› by auto
  ultimately show ?thesis using ‹subst_domain ?σ = S› by (metis (lifting))
qed

lemma bij_finite_const_subst_exists:
  assumes "finite (S::'v set)" "finite (T::'f set)" "infinite (U::'f set)"
  shows "∃σ::('f,'v) subst. subst_domain σ = S
                          ∧ bij_betw σ (subst_domain σ) (subst_range σ)
                          ∧ subst_range σ ⊆ (λc. Fun c []) ` (U - T)"
proof -
  obtain T' where "T' ⊆ U - T" "card T' = card S" "finite T'"
    by (meson assms(2,3) finite_Diff2 infinite_arbitrarily_large)
  then obtain f::"'v ⇒ 'f" where f_bij: "bij_betw f S T'"
    using finite_same_card_bij[OF assms(1)] by metis

  let ?σ = "λv. if v ∈ S then Fun (f v) [] else Var v"
  have "subst_domain ?σ = S" by (simp add: subst_domain_def)
  moreover have "⋀v w. ⟦v ∈ subst_domain ?σ; w ∉ subst_domain ?σ⟧ ⟹ ?σ w ≠ ?σ v" by auto
  hence "inj_on ?σ (subst_domain ?σ)"
    using f_bij unfolding bij_betw_def inj_on_def
    by (metis ‹subst_domain ?σ = S› term.inject(2))
  hence "bij_betw ?σ (subst_domain ?σ) (subst_range ?σ)"
    using inj_on_imp_bij_betw[of ?σ] by simp
  moreover have "subst_range ?σ = ((λc. Fun c []) ` T')"
    using ‹bij_betw f S T'› unfolding bij_betw_def inj_on_def by (auto simp add: subst_domain_def)
  hence "subst_range ?σ ⊆ ((λc. Fun c []) ` (U - T))" using ‹T' ⊆ U - T› 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 "∃σ::('f,'v) subst. subst_domain σ = S
                          ∧ bij_betw σ (subst_domain σ) (subst_range σ)
                          ∧ subst_range σ ⊆ ((λc. Fun c []) ` U) - T"
proof -
  have "finite (⋃(funs_term ` T))" using assms(2) by auto
  then obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subst_range σ ⊆ (λc. Fun c []) ` (U - (⋃(funs_term ` T)))"
    using bij_finite_const_subst_exists[OF assms(1) _ assms(3)] by blast
  moreover have "(λc. Fun c []) ` (U - (⋃(funs_term ` T))) ⊆ ((λc. Fun c []) ` U) - T" by auto
  ultimately show ?thesis by blast
qed

lemma bij_betw_iteI:
  assumes "bij_betw f A B" "bij_betw g C D" "A ∩ C = {}" "B ∩ D = {}"
  shows "bij_betw (λx. if x ∈ A then f x else g x) (A ∪ C) (B ∪ D)"
proof -
  have "bij_betw (λx. if x ∈ A then f x else g x) A B"
    by (metis bij_betw_cong[of A f "λx. if x ∈ A then f x else g x" B] assms(1))
  moreover have "bij_betw (λx. if x ∈ A then f x else g x) C D"
    using bij_betw_cong[of C g "λx. if x ∈ A then f x else g x" D] assms(2,3) by force
  ultimately show ?thesis using bij_betw_combine[OF _ _ assms(4)] by metis
qed

lemma subst_comp_split:
  assumes "subst_domain θ ∩ range_vars θ = {}"
  shows "θ = (rm_vars (subst_domain θ - V) θ) ∘s (rm_vars V θ)" (is ?P)
    and "θ = (rm_vars V θ) ∘s (rm_vars (subst_domain θ - V) θ)" (is ?Q)
proof -
  let ?rm1 = "rm_vars (subst_domain θ - V) θ" and ?rm2 = "rm_vars V θ"
  have "subst_domain ?rm2 ∩ range_vars ?rm1 = {}"
       "subst_domain ?rm1 ∩ range_vars ?rm2 = {}"
    using assms unfolding range_vars_alt_def by (force simp add: subst_domain_def)+
  hence *: "⋀v. v ∈ subst_domain ?rm1 ⟹ (?rm1 ∘s ?rm2) v = θ v"
           "⋀v. v ∈ subst_domain ?rm2 ⟹ (?rm2 ∘s ?rm1) v = θ v"
    using ident_comp_subst_trm_if_disj[of ?rm2 ?rm1]
          ident_comp_subst_trm_if_disj[of ?rm1 ?rm2]
    by (auto simp add: subst_domain_def)
  hence "⋀v. v ∉ subst_domain ?rm1 ⟹ (?rm1 ∘s ?rm2) v = θ v"
        "⋀v. v ∉ subst_domain ?rm2 ⟹ (?rm2 ∘s ?rm1) v = θ v"
    unfolding subst_compose_def by (auto simp add: subst_domain_def)
  hence "⋀v. (?rm1 ∘s ?rm2) v = θ v" "⋀v. (?rm2 ∘s ?rm1) v = θ v" using * by blast+
  thus ?P ?Q by auto
qed

lemma subst_comp_eq_if_disjoint_vars:
  assumes "(subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
  shows "γ ∘s δ = δ ∘s γ"
proof -
  { fix x assume "x ∈ subst_domain γ"
    hence "(γ ∘s δ) x = γ x" "(δ ∘s γ) x = γ x"
      using assms unfolding range_vars_alt_def by (force simp add: subst_compose)+
    hence "(γ ∘s δ) x = (δ ∘s γ) x" by metis
  } moreover
  { fix x assume "x ∈ subst_domain δ"
    hence "(γ ∘s δ) x = δ x" "(δ ∘s γ) x = δ x"
      using assms
      unfolding range_vars_alt_def by (auto simp add: subst_compose subst_domain_def)
    hence "(γ ∘s δ) x = (δ ∘s γ) x" by metis
  } moreover
  { fix x assume "x ∉ subst_domain γ" "x ∉ subst_domain δ"
    hence "(γ ∘s δ) x = (δ ∘s γ) x" by (simp add: subst_compose subst_domain_def)
  } ultimately show ?thesis by auto
qed

lemma subst_eq_if_disjoint_vars_ground:
  fixes ξ δ::"('f,'v) subst"
  assumes "subst_domain δ ∩ subst_domain ξ = {}" "ground (subst_range ξ)" "ground (subst_range δ)" 
  shows "t ⋅ δ ⋅ ξ = t ⋅ ξ ⋅ δ"
by (metis assms subst_comp_eq_if_disjoint_vars range_vars_alt_def
          subst_subst_compose sup_bot.right_neutral)

lemma subst_img_bound: "subst_domain δ ∪ range_vars δ ⊆ fv t ⟹ range_vars δ ⊆ fv (t ⋅ δ)"
proof -
  assume "subst_domain δ ∪ range_vars δ ⊆ fv t"
  hence "subst_domain δ ⊆ fv t" by blast
  thus ?thesis
    by (metis (no_types) range_vars_alt_def le_iff_sup subst_apply_fv_unfold
              subst_apply_fv_union subst_range.simps)
qed

lemma subst_all_fv_subset: "fv t ⊆ fvset M ⟹ fv (t ⋅ θ) ⊆ fvset (M ⋅set θ)"
proof -
  assume *: "fv t ⊆ fvset M"
  { fix v assume "v ∈ fv t"
    hence "v ∈ fvset M" using * by auto
    then obtain t' where "t' ∈ M" "v ∈ fv t'" by auto
    hence "fv (θ v) ⊆ fv (t' ⋅ θ)"
      by (metis eval_term.simps(1) subst_apply_fv_subset subst_apply_fv_unfold
                subtermeq_vars_subset vars_iff_subtermeq) 
    hence "fv (θ v) ⊆ fvset (M ⋅set θ)" using ‹t' ∈ M› by auto
  }
  thus ?thesis by (auto simp: subst_apply_fv_unfold)
qed

lemma subst_support_if_mgt_subst_idem:
  assumes "θ ≼∘ δ" "subst_idem θ"
  shows "θ supports δ"
proof -
  from ‹θ ≼∘ δ› obtain σ where σ: "δ = θ ∘s σ" by blast
  hence "⋀v. θ v ⋅ δ = Var v ⋅ (θ ∘s θ ∘s σ)" by (simp add: subst_compose)
  hence "⋀v. θ v ⋅ δ = Var v ⋅ (θ ∘s σ)" using ‹subst_idem θ › unfolding subst_idem_def by simp
  hence "⋀v. θ v ⋅ δ = Var v ⋅ δ" using σ by simp
  thus "θ supports δ" by simp
qed

lemma subst_support_iff_mgt_if_subst_idem:
  assumes "subst_idem θ"
  shows "θ ≼∘ δ ⟷ θ supports δ"
proof
  show "θ ≼∘ δ ⟹ θ supports δ" by (fact subst_support_if_mgt_subst_idem[OF _ ‹subst_idem θ›])
  show "θ supports δ ⟹ θ ≼∘ δ" by (fact subst_supportD)
qed

lemma subst_support_comp:
  fixes θ δ ℐ::"('a,'b) subst"
  assumes "θ supports ℐ" "δ supports ℐ"
  shows "(θ ∘s δ) supports ℐ"
by (metis (no_types) assms subst_agreement eval_term.simps(1) subst_subst_compose)

lemma subst_support_comp':
  fixes θ δ σ::"('a,'b) subst"
  assumes "θ supports δ"
  shows "θ supports (δ ∘s σ)" "σ supports δ ⟹ θ supports (σ ∘s δ)"
using assms unfolding subst_support_def by (metis subst_compose_assoc, metis)

lemma subst_support_comp_split:
  fixes θ δ ℐ::"('a,'b) subst"
  assumes "(θ ∘s δ) supports ℐ"
  shows "subst_domain θ ∩ range_vars θ = {} ⟹ θ supports ℐ"
  and "subst_domain θ ∩ subst_domain δ = {} ⟹ δ supports ℐ"
proof -
  assume "subst_domain θ ∩ range_vars θ = {}"
  hence "subst_idem θ" by (metis subst_idemI)
  have "θ ≼∘ ℐ" using assms subst_compose_assoc[of θ δ ℐ] unfolding subst_compose_def by metis
  show "θ supports ℐ" using subst_support_if_mgt_subst_idem[OF ‹θ ≼∘ ℐ› ‹subst_idem θ›] by auto
next
  assume "subst_domain θ ∩ subst_domain δ = {}"
  moreover have "∀v ∈ subst_domain (θ ∘s δ). (θ ∘s δ) v ⋅ ℐ = ℐ v" using assms by metis
  ultimately have "∀v ∈ subst_domain δ. δ v ⋅ ℐ = ℐ v"
    using var_not_in_subst_dom unfolding subst_compose_def
    by (metis IntI empty_iff eval_term.simps(1))
  thus "δ supports ℐ" by force
qed

lemma subst_idem_support: "subst_idem θ ⟹ θ supports θ ∘s δ"
unfolding subst_idem_def by (metis subst_support_def subst_compose_assoc)

lemma subst_idem_iff_self_support: "subst_idem θ ⟷ θ supports θ"
using subst_support_def[of θ θ] unfolding subst_idem_def by auto

lemma subterm_subst_neq: "t ⊏ t' ⟹ t ⋅ s ≠ t' ⋅ s"
by (metis subst_mono_neq)

lemma fv_Fun_subst_neq: "x ∈ fv (Fun f T) ⟹ σ x ≠ Fun f T ⋅ σ"
using subterm_subst_neq[of "Var x" "Fun f T"] vars_iff_subterm_or_eq[of x "Fun f T"] by auto

lemma subterm_subst_unfold:
  assumes "t ⊑ s ⋅ θ"
  shows "(∃s'. s' ⊑ s ∧ t = s' ⋅ θ) ∨ (∃x ∈ fv s. t ⊏ θ x)"
using assms
proof (induction s)
  case (Fun f T) thus ?case
  proof (cases "t = Fun f T ⋅ θ")
    case True thus ?thesis using Fun by auto
  next
    case False
    then obtain s' where s': "s' ∈ set T" "t ⊑ s' ⋅ θ" using Fun by auto
    hence "(∃s''. s'' ⊑ s' ∧ t = s'' ⋅ θ) ∨ (∃x ∈ fv s'. t ⊏ θ x)" by (metis Fun.IH)
    thus ?thesis using s'(1) by auto
  qed
qed simp

lemma subterm_subst_img_subterm:
  assumes "t ⊑ s ⋅ θ" "⋀s'. s' ⊑ s ⟹ t ≠ s' ⋅ θ"
  shows "∃w ∈ fv s. t ⊏ θ w"
using subterm_subst_unfold[OF assms(1)] assms(2) by force

lemma subterm_subst_not_img_subterm:
  assumes "t ⊑ s ⋅ ℐ" "¬(∃w ∈ fv s. t ⊑ ℐ w)"
  shows "∃f T. Fun f T ⊑ s ∧ t = Fun f T ⋅ ℐ"
proof (rule ccontr)
  assume "¬(∃f T. Fun f T ⊑ s ∧ t = Fun f T ⋅ ℐ)"
  hence "⋀f T. Fun f T ⊑ s ⟹ t ≠ Fun f T ⋅ ℐ" by simp
  moreover have "⋀x. Var x ⊑ s ⟹ t ≠ Var x ⋅ ℐ"
    using assms(2) vars_iff_subtermeq by force
  ultimately have "⋀s'. s' ⊑ s ⟹ t ≠ s' ⋅ ℐ" by (metis "term.exhaust")
  thus False using assms subterm_subst_img_subterm by blast
qed

lemma subst_apply_img_var:
  assumes "v ∈ fv (t ⋅ δ)" "v ∉ fv t"
  obtains w where "w ∈ fv t" "v ∈ fv (δ w)"
using assms by (induct t) auto

lemma subst_apply_img_var':
  assumes "x ∈ fv (t ⋅ δ)" "x ∉ fv t"
  shows "∃y ∈ fv t. x ∈ fv (δ y)"
by (metis assms subst_apply_img_var)

lemma nth_map_subst:
  fixes θ::"('f,'v) subst" and T::"('f,'v) term list" and i::nat
  shows "i < length T ⟹ (map (λt. t ⋅ θ) T) ! i = (T ! i) ⋅ θ"
by (fact nth_map)

lemma subst_subterm:
  assumes "Fun f T ⊑ t ⋅ θ"
  shows "(∃S. Fun f S ⊑ t ∧ Fun f S ⋅ θ = Fun f T) ∨
         (∃s ∈ subst_range θ. Fun f T ⊑ s)"
using assms subterm_subst_not_img_subterm by (cases "∃s ∈ subst_range θ. Fun f T ⊑ s") fastforce+

lemma subst_subterm':
  assumes "Fun f T ⊑ t ⋅ θ"
  shows "∃S. length S = length T ∧ (Fun f S ⊑ t ∨ (∃s ∈ subst_range θ. Fun f S ⊑ s))"
using subst_subterm[OF assms] by auto

lemma subst_subterm'':
  assumes "s ∈ subterms (t ⋅ θ)"
  shows "(∃u ∈ subterms t. s = u ⋅ θ) ∨ s ∈ subtermsset (subst_range θ)"
proof (cases s)
  case (Var x)
  thus ?thesis
    using assms subterm_subst_not_img_subterm vars_iff_subtermeq
    by (cases "s = t ⋅ θ") fastforce+
next
  case (Fun f T)
  thus ?thesis
    using subst_subterm assms
    by fastforce
qed

lemma fv_ground_subst_compose:
  assumes "subst_domain δ = subst_domain σ"
    and "range_vars δ = {}" "range_vars σ = {}"
  shows "fv (t ⋅ δ ∘s θ) = fv (t ⋅ σ ∘s θ)"
proof (induction t)
  case (Var x) show ?case
  proof (cases "x ∈ subst_domain δ")
    case True thus ?thesis
      using assms unfolding range_vars_alt_def by (auto simp: subst_compose subst_apply_fv_empty)
  next
    case False
    hence "δ x = Var x" "σ x = Var x" using assms(1) by (blast,blast)
    thus ?thesis by (simp add: subst_compose)
  qed
qed simp


subsection ‹More Small Lemmata›
lemma funs_term_subst: "funs_term (t ⋅ θ) = funs_term t ∪ (⋃x ∈ fv t. funs_term (θ x))"
by (induct t) auto

lemma fvset_subst_img_eq:
  assumes "X ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fvset (δ ` (Y - X)) = fvset (δ ` Y) - X"
using assms unfolding range_vars_alt_def by force

lemma subst_Fun_index_eq:
  assumes "i < length T" "Fun f T ⋅ δ = Fun g T' ⋅ δ"
  shows "T ! i ⋅ δ = T' ! i ⋅ δ"
proof -
  have "map (λx. x ⋅ δ) T = map (λx. x ⋅ δ) T'" using assms by simp
  thus ?thesis by (metis assms(1) length_map nth_map)
qed

lemma fv_exists_if_unifiable_and_neq:
  fixes t t'::"('a,'b) term" and δ θ::"('a,'b) subst"
  assumes "t ≠ t'" "t ⋅ θ = t' ⋅ θ"
  shows "fv t ∪ fv t' ≠ {}"
proof
  assume "fv t ∪ fv t' = {}"
  hence "fv t = {}" "fv t' = {}" by auto
  hence "t ⋅ θ = t" "t' ⋅ θ = t'" by auto
  hence "t = t'" using assms(2) by metis
  thus False using assms(1) by auto
qed

lemma const_subterm_subst: "Fun c [] ⊑ t ⟹ Fun c [] ⊑ t ⋅ σ"
by (induct t) auto

lemma const_subterm_subst_var_obtain:
  assumes "Fun c [] ⊑ t ⋅ σ" "¬Fun c [] ⊑ t"
  obtains x where "x ∈ fv t" "Fun c [] ⊑ σ x"
using assms by (induct t) auto

lemma const_subterm_subst_cases:
  assumes "Fun c [] ⊑ t ⋅ σ"
  shows "Fun c [] ⊑ t ∨ (∃x ∈ fv t. x ∈ subst_domain σ ∧ Fun c [] ⊑ σ x)"
proof (cases "Fun c [] ⊑ t")
  case False
  then obtain x where "x ∈ fv t" "Fun c [] ⊑ σ x"
    using const_subterm_subst_var_obtain[OF assms] by atomize_elim auto
  thus ?thesis by (cases "x ∈ subst_domain σ") auto
qed simp

lemma const_subterms_subst_cases:
  assumes "Fun c [] ⊑set M ⋅set σ"
  shows "Fun c [] ⊑set M ∨ (∃x ∈ fvset M. x ∈ subst_domain σ ∧ Fun c [] ⊑ σ x)"
using assms const_subterm_subst_cases[of c _ σ] by auto

lemma const_subterms_subst_cases':
  assumes "Fun c [] ⊑set M ⋅set σ"
  shows "Fun c [] ⊑set M ∨ Fun c [] ⊑set subst_range σ"
using const_subterms_subst_cases[OF assms] by auto

lemma fvpairs_subst_fv_subset:
  assumes "x ∈ fvpairs F"
  shows "fv (θ x) ⊆ fvpairs (F ⋅pairs θ)"
  using assms
proof (induction F)
  case (Cons f F)
  then obtain t t' where f: "f = (t,t')" by (metis surj_pair)
  show ?case
  proof (cases "x ∈ fvpairs F")
    case True thus ?thesis
      using Cons.IH
      unfolding subst_apply_pairs_def
      by auto
  next
    case False
    hence "x ∈ fv t ∪ fv t'" using Cons.prems f by simp
    hence "fv (θ x) ⊆ fv (t ⋅ θ) ∪ fv (t' ⋅ θ)" using fv_subst_subset[of x] by force
    thus ?thesis using f unfolding subst_apply_pairs_def by auto
  qed
qed simp

lemma fvpairs_step_subst: "fvset (δ ` fvpairs F) = fvpairs (F ⋅pairs δ)"
proof (induction F)
  case (Cons f F)
  obtain t t' where "f = (t,t')" by atomize_elim auto
  thus ?case
    using Cons
    by (simp add: subst_apply_pairs_def subst_apply_fv_unfold)
qed (simp_all add: subst_apply_pairs_def)

lemma fvpairs_subst_obtain_var:
  fixes δ::"('a,'b) subst"
  assumes "x ∈ fvpairs (F ⋅pairs δ)"
  shows "∃y ∈ fvpairs F. x ∈ fv (δ y)"
  using assms 
proof (induction F)
  case (Cons f F)
  then obtain t s where f: "f = (t,s)" by (metis surj_pair)

  from Cons.IH show ?case
  proof (cases "x ∈ fvpairs (F ⋅pairs δ)")
    case False
    hence "x ∈ fv (t ⋅ δ) ∨ x ∈ fv (s ⋅ δ)"
      using f Cons.prems
      by (simp add: subst_apply_pairs_def)
    hence "(∃y ∈ fv t. x ∈ fv (δ y)) ∨ (∃y ∈ fv s. x ∈ fv (δ y))" by (metis fv_subst_obtain_var)
    thus ?thesis using f by (auto simp add: subst_apply_pairs_def)
  qed (auto simp add: Cons.IH)
qed (simp add: subst_apply_pairs_def)

lemma pair_subst_ident[intro]: "(fv t ∪ fv t') ∩ subst_domain θ = {} ⟹ (t,t') ⋅p θ = (t,t')"
by auto

lemma pairs_substI[intro]:
  assumes "subst_domain θ ∩ (⋃(s,t) ∈ M. fv s ∪ fv t) = {}"
  shows "M ⋅pset θ = M"
proof -
  { fix m assume M: "m ∈ M"
    then obtain s t where m: "m = (s,t)" by (metis surj_pair)
    hence "(fv s ∪ fv t) ∩ subst_domain θ = {}" using assms M by auto
    hence "m ⋅p θ = m" using m by auto
  } thus ?thesis by (simp add: image_cong) 
qed

lemma fvpairs_subst: "fvpairs (F ⋅pairs θ) = fvset (θ ` (fvpairs F))"
proof (induction F)
  case (Cons g G)
  obtain t t' where "g = (t,t')" by (metis surj_pair)
  thus ?case
    using Cons.IH
    by (simp add: subst_apply_pairs_def subst_apply_fv_unfold)
qed (simp add: subst_apply_pairs_def)

lemma fvpairs_subst_subset:
  assumes "fvpairs (F ⋅pairs δ) ⊆ subst_domain σ"
  shows  "fvpairs F ⊆ subst_domain σ ∪ subst_domain δ"
  using assms
proof (induction F)
  case (Cons g G)
  hence IH: "fvpairs G ⊆ subst_domain σ ∪ subst_domain δ"
    by (simp add: subst_apply_pairs_def)
  obtain t t' where g: "g = (t,t')" by (metis surj_pair)
  hence "fv (t ⋅ δ) ⊆ subst_domain σ" "fv (t' ⋅ δ) ⊆ subst_domain σ"
    using Cons.prems by (simp_all add: subst_apply_pairs_def)
  hence "fv t ⊆ subst_domain σ ∪ subst_domain δ" "fv t' ⊆ subst_domain σ ∪ subst_domain δ"
    unfolding subst_apply_fv_unfold by force+
  thus ?case using IH g by (simp add: subst_apply_pairs_def)
qed (simp add: subst_apply_pairs_def)

lemma pairs_subst_comp: "F ⋅pairs δ ∘s θ = ((F ⋅pairs δ) ⋅pairs θ)"
by (induct F) (auto simp add: subst_apply_pairs_def)

lemma pairs_substI'[intro]:
  "subst_domain θ ∩ fvpairs F = {} ⟹ F ⋅pairs θ = F"
by (induct F) (force simp add: subst_apply_pairs_def)+

lemma subst_pair_compose[simp]: "d ⋅p (δ ∘s ℐ) = d ⋅p δ ⋅p ℐ"
proof -
  obtain t s where "d = (t,s)" by atomize_elim auto
  thus ?thesis by auto
qed

lemma subst_pairs_compose[simp]: "D ⋅pset (δ ∘s ℐ) = D ⋅pset δ ⋅pset ℐ"
by auto

lemma subst_apply_pair_pair: "(t, s) ⋅p ℐ = (t ⋅ ℐ, s ⋅ ℐ)"
by (rule prod.case)

lemma subst_apply_pairs_nil[simp]: "[] ⋅pairs δ = []"
unfolding subst_apply_pairs_def by simp

lemma subst_apply_pairs_singleton[simp]: "[(t,s)] ⋅pairs δ = [(t ⋅ δ,s ⋅ δ)]"
unfolding subst_apply_pairs_def by simp

lemma subst_apply_pairs_Var[iff]: "F ⋅pairs Var = F" by (simp add: subst_apply_pairs_def)

lemma subst_apply_pairs_pset_subst: "set (F ⋅pairs θ) = set F ⋅pset θ"
unfolding subst_apply_pairs_def by force

lemma subst_subterms:
  "t ⊑set M ⟹ t ⋅ θ ⊑set M ⋅set θ"
using subst_mono_neq by fastforce

lemma subst_subterms_fv:
  "x ∈ fvset M ⟹ θ x ∈ subtermsset M ⋅set θ"
using fv_subterms_substI by fastforce

lemma subst_subterms_Var:
  "Var x ⊑set M ⟹ θ x ∈ subtermsset M ⋅set θ"
using subst_subterms_fv[of x M θ] by force

lemma fv_subset_subterms_subset:
  "δ ` fvset M ⊆ subtermsset M ⋅set δ"
using subst_subterms_fv by fast

lemma subst_const_swap_eq:
  fixes θ σ::"('a,'b) subst"
  assumes t: "t ⋅ θ = s ⋅ θ"
    and θ: "∀x ∈ fv t ∪ fv s. ∃k. θ x = Fun k []"
           "∀x ∈ fv t. ¬(θ x ⊑ s)"
           "∀x ∈ fv s. ¬(θ x ⊑ t)"
    and σ_def: "σ ≡ λx. p (θ x)"
  shows "t ⋅ σ = s ⋅ σ"
using t θ
proof (induction t arbitrary: s)
  case (Var x) thus ?case unfolding σ_def by (cases s) auto
next
  case (Fun f ts)
  note prems = Fun.prems

  obtain ss where s: "s = Fun f ss" and ss: "ts ⋅list θ = ss ⋅list θ" using prems by (cases s) auto

  have "ts ! i ⋅ σ = ss ! i ⋅ σ" when i: "i < length ts" for i
  proof -
    have *: "ts ! i ∈ set ts" using i by simp
    have **: "ts ! i ⋅ θ = ss ! i ⋅ θ" using i prems(1) unfolding s by (metis subst_Fun_index_eq)
    have ***: "ss ! i ∈ set ss" using i ss by (metis length_map nth_mem)

    show ?thesis using Fun.IH[OF * **] prems(2,3,4) * *** unfolding s by auto
  qed
  hence IH: "ts ⋅list σ = ss ⋅list σ"
    using ss by (metis (mono_tags, lifting) length_map nth_equalityI nth_map)

  show ?case using IH unfolding s by auto
qed

lemma term_subst_set_eq:
  assumes "⋀x. x ∈ fvset M ⟹ δ x = σ x"
  shows "M ⋅set δ = M ⋅set σ"
proof -
  have "t ⋅ δ = t ⋅ σ" when "t ∈ M" for t
    using that assms term_subst_eq[of _ δ σ] by fastforce
  thus ?thesis by simp
qed

lemma subst_const_swap_eq':
  assumes "t ⋅ θ = s ⋅ θ"
    and "∀x ∈ fv t ∪ fv s. θ x = σ x ∨ ¬(θ x ⊑ t) ∧ ¬(θ x ⊑ s)" (is "?A t s")
    and "∀x ∈ fv t ∪ fv s. ∃c. θ x = Fun c []" (is "?B t s")
    and "∀x ∈ fv t ∪ fv s. ∃c. σ x = Fun c []" (is "?C t s")
    and "∀x ∈ fv t ∪ fv s. ∀y ∈ fv t ∪ fv s. θ x = θ y ⟷ σ x = σ y" (is "?D t s")
  shows "t ⋅ σ = s ⋅ σ"
using assms
proof (induction t arbitrary: s)
  case (Var x)
  note prems = Var.prems
  have "(∃y. s = Var y) ∨ (∃c. s = Fun c [])" using prems(1,3) by (cases s) auto
  thus ?case
  proof
    assume "∃y. s = Var y"
    then obtain y where y: "s = Var y" by blast
    hence "θ x = θ y" using prems(1) by simp
    hence "σ x = σ y" using prems(5) y by fastforce
    thus ?thesis using y by force
  next
    assume "∃c. s = Fun c []"
    then obtain c where c: "s = Fun c []" by blast
    have "θ x = σ x ∨ ¬(θ x ⊑ Fun c [])" using prems(2) c by auto
    thus ?thesis using prems(1) c by simp
  qed
next
  case (Fun f ts)
  note prems = Fun.prems
  note IH = Fun.IH

  show ?case
  proof (cases s)
    case (Var x)
    note s = this
    hence ts: "ts = []" using prems(1,3) by auto
    show ?thesis using prems unfolding s ts by auto
  next
    case (Fun g ss)
    note s = this
    hence g: "f = g" using prems(1) by fastforce

    have ss: "ts ⋅list θ = ss ⋅list θ" using prems(1) unfolding s by (cases s) auto

    have len: "length ts = length ss" using ss by (metis length_map)

    have "ts ! i ⋅ σ = ss ! i ⋅ σ" when i: "i < length ts" for i
    proof -
      have 0: "ts ! i ∈ set ts" using i by simp
      have 1: "ts ! i ⋅ θ = ss ! i ⋅ θ" using i prems(1) unfolding s by (metis subst_Fun_index_eq)
      have 2: "ss ! i ∈ set ss" using i by (metis len nth_mem)

      have 3: "fv (ts ! i) ⊆ fv (Fun f ts)" "fv (ss ! i) ⊆ fv (Fun g ss)"
              "subterms (ts ! i) ⊆ subterms (Fun f ts)" "subterms (ss ! i) ⊆ subterms (Fun g ss)"
        subgoal by (meson index_Fun_fv_subset i)
        subgoal by (metis index_Fun_fv_subset i len)
        subgoal using ss i by fastforce
        subgoal using ss i len by fastforce
        done
      
      have 4: "?A (ts ! i) (ss ! i)" "?B (ts ! i) (ss ! i)"
              "?C (ts ! i) (ss ! i)" "?D (ts ! i) (ss ! i)"
        subgoal using 3 prems(2) unfolding s by blast
        subgoal using 3(1,2) prems(3) unfolding s by blast
        subgoal using 3(1,2) prems(4) unfolding s by blast
        subgoal using 3(1,2) prems(5) unfolding s by blast
        done
        
      thus ?thesis using IH[OF 0 1 4] prems(2-) 0 2 unfolding s by blast
    qed
    hence "ts ⋅list σ = ss ⋅list σ" by (metis (mono_tags, lifting) ss length_map nth_equalityI nth_map)
    thus ?thesis unfolding s g by auto
  qed
qed

lemma subst_const_swap_eq_mem:
  assumes "t ⋅ θ ∈ M ⋅set θ"
    and "∀x ∈ fvset M ∪ fv t. θ x = σ x ∨ ¬(θ x ⊑set insert t M)"
    and "∀x ∈ fvset M ∪ fv t. ∃c. θ x = Fun c []" (is "?B (fvset M ∪ fv t)")
    and "∀x ∈ fvset M ∪ fv t. ∃c. σ x = Fun c []" (is "?C (fvset M ∪ fv t)")
    and "∀x ∈ fvset M ∪ fv t. ∀y ∈ fvset M ∪ fv t. θ x = θ y ⟷ σ x = σ y" (is "?D (fvset M ∪ fv t)")
  shows "t ⋅ σ ∈ M ⋅set σ"
proof -
  let ?A = "λt s. ∀x ∈ fv t ∪ fv s. θ x = σ x ∨ ¬(θ x ⊑ t) ∧ ¬(θ x ⊑ s)" 

  obtain s where s: "s ∈ M" "s ⋅ θ = t ⋅ θ" using assms(1) by fastforce

  have 0: "fv s ⊆ fvset M" "subterms s ⊆ subtermsset (insert t M)"
          "subterms t ⊆ subtermsset (insert t M)"
    using s(1) by auto

  have 1: "?A s t" "?B (fv s ∪ fv t)" "?C (fv s ∪ fv t)" "?D (fv s ∪ fv t)"
    subgoal using assms(2) 0 by fast
    subgoal using assms(3) 0 by blast
    subgoal using assms(4) 0 by blast
    subgoal using assms(5) 0 by blast
    done

  have "s ⋅ σ = t ⋅ σ" by (rule subst_const_swap_eq'[OF s(2) 1])
  thus ?thesis by (metis s(1) imageI)
qed


subsection ‹Finite Substitutions›
inductive_set fsubst::"('a,'b) subst set" where
  fvar:     "Var ∈ fsubst"
| FUpdate:  "⟦θ ∈ fsubst; v ∉ subst_domain θ; t ≠ Var v⟧ ⟹ θ(v := t) ∈ fsubst"

lemma finite_dom_iff_fsubst:
  "finite (subst_domain θ) ⟷ θ ∈ fsubst"
proof
  assume "finite (subst_domain θ)" thus "θ ∈ fsubst"
  proof (induction "subst_domain θ" arbitrary: θ rule: finite.induct)
    case emptyI
    hence "θ = Var" using empty_dom_iff_empty_subst by metis
    thus ?case using fvar by simp
  next
    case (insertI θ'dom v) thus ?case
    proof (cases "v ∈ θ'dom")
      case True
      hence "θ'dom = subst_domain θ" using ‹insert v θ'dom = subst_domain θ› by auto
      thus ?thesis using insertI.hyps(2) by metis
    next
      case False
      let ?θ' = "λw. if w ∈ θ'dom then θ w else Var w"
      have "subst_domain ?θ' = θ'dom"
        using ‹v ∉ θ'dom› ‹insert v θ'dom = subst_domain θ›
        by (auto simp add: subst_domain_def)
      hence "?θ' ∈ fsubst" using insertI.hyps(2) by simp
      moreover have "?θ'(v := θ v) = (λw. if w ∈ insert v θ'dom then θ w else Var w)" by auto
      hence "?θ'(v := θ v) = θ"
        using ‹insert v θ'dom = subst_domain θ›
        by (auto simp add: subst_domain_def)
      ultimately show ?thesis
        using FUpdate[of ?θ' v "θ v"] False insertI.hyps(3)
        by (auto simp add: subst_domain_def)
    qed
  qed
next
  assume "θ ∈ fsubst" thus "finite (subst_domain θ)"
  by (induct θ, simp, metis subst_dom_insert_finite)
qed

lemma fsubst_induct[case_names fvar FUpdate, induct set: finite]:
  assumes "finite (subst_domain δ)" "P Var"
  and "⋀θ v t. ⟦finite (subst_domain θ); v ∉ subst_domain θ; t ≠ Var v; P θ⟧ ⟹ P (θ(v := t))"
  shows "P δ"
using assms finite_dom_iff_fsubst fsubst.induct by metis

lemma fun_upd_fsubst: "s(v := t) ∈ fsubst ⟷ s ∈ fsubst"
using subst_dom_insert_finite[of s] finite_dom_iff_fsubst by blast 

lemma finite_img_if_fsubst: "s ∈ fsubst ⟹ finite (subst_range s)"
using finite_dom_iff_fsubst finite_subst_img_if_finite_dom' by blast


subsection ‹Unifiers and Most General Unifiers (MGUs)›

abbreviation Unifier::"('f,'v) subst ⇒ ('f,'v) term ⇒ ('f,'v) term ⇒ bool" where
  "Unifier σ t u ≡ (t ⋅ σ = u ⋅ σ)"

abbreviation MGU::"('f,'v) subst ⇒ ('f,'v) term ⇒ ('f,'v) term ⇒ bool" where
  "MGU σ t u ≡ Unifier σ t u ∧ (∀θ. Unifier θ t u ⟶ σ ≼∘ θ)"

lemma MGUI[intro]:
  shows "⟦t ⋅ σ = u ⋅ σ; ⋀θ::('f,'v) subst. t ⋅ θ = u ⋅ θ ⟹ σ ≼∘ θ⟧ ⟹ MGU σ t u"
by auto

lemma UnifierD[dest]:
  fixes σ::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list"
  assumes "Unifier σ (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 ⋅ σ = Fun g Y ⋅ σ" by auto
  hence "length (map (λx. x ⋅ σ) X) = length (map (λx. x ⋅ σ) Y)" by auto
  thus "length X = length Y" by auto
qed

lemma MGUD[dest]:
  fixes σ::"('f,'v) subst" and f g::'f and X Y::"('f,'v) term list"
  assumes "MGU σ (Fun f X) (Fun g Y)"
  shows "f = g" "length X = length Y"
using assms by (auto dest: map_eq_imp_length_eq)

lemma MGU_sym[sym]: "MGU σ s t ⟹ MGU σ t s" by auto
lemma Unifier_sym[sym]: "Unifier σ s t ⟹ Unifier σ t s" by auto

lemma MGU_nil: "MGU Var s t ⟷ s = t" by fastforce

lemma Unifier_comp: "Unifier (θ ∘s δ) t u ⟹ Unifier δ (t ⋅ θ) (u ⋅ θ)"
by simp

lemma Unifier_comp': "Unifier δ (t ⋅ θ) (u ⋅ θ) ⟹ Unifier (θ ∘s δ) t u"
by simp

lemma Unifier_excludes_subterm:
  assumes θ: "Unifier θ t u"
  shows "¬t ⊏ u"
proof
  assume "t ⊏ u"
  hence "t ⋅ θ ⊏ u ⋅ θ" using subst_mono_neq by metis
  hence "t ⋅ θ ≠ u ⋅ θ" by simp
  moreover from θ have "t ⋅ θ = u ⋅ θ" by auto
  ultimately show False ..
qed

lemma MGU_is_Unifier: "MGU σ t u ⟹ Unifier σ t u" by (rule conjunct1)

lemma MGU_Var1:
  assumes "¬Var v ⊏ t"
  shows "MGU (Var(v := t)) (Var v) t"
proof (intro MGUI exI)
  show "Var v ⋅ (Var(v := t)) = t ⋅ (Var(v := t))" using assms subst_no_occs by fastforce
next
  fix θ::"('a,'b) subst" assume th: "Var v ⋅ θ = t ⋅ θ" 
  show "θ = (Var(v := t)) ∘s θ" 
    using th by (auto simp: subst_compose_def)
qed

lemma MGU_Var2: "v ∉ fv t ⟹ 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) ⟷ v = w" by fastforce

lemma MGU_Const1: "MGU Var (Fun c []) (Fun d []) ⟷ c = d" by fastforce

lemma MGU_Const2: "MGU θ (Fun c []) (Fun d []) ⟹ c = d" by auto

lemma MGU_Fun:
  assumes "MGU θ (Fun f X) (Fun g Y)"
  shows "f = g" "length X = length Y"
proof -
  let ?F = "λθ X. map (λx. x ⋅ θ) X"
  from assms have
    "⟦f = g; ?F θ X = ?F θ Y; ∀θ'. f = g ∧ ?F θ' X = ?F θ' Y ⟶ θ ≼∘ θ'⟧ ⟹ 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 θ (Fun f (x#X)) (Fun g (y#Y))"
  shows "Unifier θ x y" "Unifier θ (Fun f X) (Fun g Y)"
using assms by simp_all

lemma Unifier_subst_idem_subst: 
  "subst_idem r ⟹ Unifier s (t ⋅ r) (u ⋅ r) ⟹ Unifier (r ∘s s) (t ⋅ r) (u ⋅ r)"
by (metis (no_types, lifting) subst_idem_def subst_subst_compose)

lemma subst_idem_comp:
  "subst_idem r ⟹ Unifier s (t ⋅ r) (u ⋅ r) ⟹ 
    (⋀q. Unifier q (t ⋅ r) (u ⋅ r) ⟹ s ∘s q = q) ⟹
    subst_idem (r ∘s s)"
by (frule Unifier_subst_idem_subst, blast, metis subst_idem_def subst_compose_assoc)

lemma Unifier_mgt: "⟦Unifier δ t u; δ ≼∘ θ⟧ ⟹ Unifier θ t u" by auto

lemma Unifier_support: "⟦Unifier δ t u; δ supports θ⟧ ⟹ Unifier θ t u"
using subst_supportD Unifier_mgt by metis

lemma MGU_mgt: "⟦MGU σ t u; MGU δ t u⟧ ⟹ σ ≼∘ δ" by auto

lemma Unifier_trm_fv_bound:
  "⟦Unifier s t u; v ∈ fv t⟧ ⟹ v ∈ subst_domain s ∪ range_vars s ∪ fv u"
proof (induction t arbitrary: s u)
  case (Fun f X)
  hence "v ∈ fv (u ⋅ s) ∨ v ∈ subst_domain s" by (metis subst_not_dom_fixed)
  thus ?case by (metis (no_types) Un_iff contra_subsetD subst_sends_fv_to_img)
qed (metis (no_types) UnI1 UnI2 subsetCE no_var_subterm subst_sends_dom_to_img
            subst_to_var_is_var trm_subst_ident' vars_iff_subterm_or_eq)

lemma Unifier_rm_var: "⟦Unifier θ s t; v ∉ fv s ∪ fv t⟧ ⟹ Unifier (rm_var v θ) s t"
by (auto simp add: repl_invariance)

lemma Unifier_ground_rm_vars:
  assumes "ground (subst_range 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 ∪ fv t' ⊆ 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 ‹Well-formedness of Substitutions and Unifiers›
inductive_set wfsubst_set::"('a,'b) subst set" where
  Empty[simp]: "Var ∈ wfsubst_set"
| Insert[simp]:
    "⟦θ ∈ wfsubst_set; v ∉ subst_domain θ;
      v ∉ range_vars θ; fv t ∩ (insert v (subst_domain θ)) = {}⟧
      ⟹ θ(v := t) ∈ wfsubst_set"

definition wfsubst::"('a,'b) subst ⇒ bool" where
  "wfsubst θ ≡ subst_domain θ ∩ range_vars θ = {} ∧ finite (subst_domain θ)"

definition wfMGU::"('a,'b) subst ⇒ ('a,'b) term ⇒ ('a,'b) term ⇒ bool" where
  "wfMGU θ s t ≡ wfsubst θ ∧ MGU θ s t ∧ subst_domain θ ∪ range_vars θ ⊆ fv s ∪ fv t"

lemma wf_subst_subst_idem: "wfsubst θ ⟹ subst_idem θ" using subst_idemI[of θ] unfolding wfsubst_def by fast

lemma wf_subst_properties: "θ ∈ wfsubst_set = wfsubst θ"
proof
  show "wfsubst θ ⟹ θ ∈ wfsubst_set" unfolding wfsubst_def
  proof -
    assume "subst_domain θ ∩ range_vars θ = {} ∧ finite (subst_domain θ)"
    hence "finite (subst_domain θ)" "subst_domain θ ∩ range_vars θ = {}"
      by auto
    thus "θ ∈ wfsubst_set"
    proof (induction θ rule: fsubst_induct)
      case fvar thus ?case by simp
    next
      case (FUpdate δ v t)
      have "subst_domain δ ⊆ subst_domain (δ(v := t))" "range_vars δ ⊆ range_vars (δ(v := t))"
        using FUpdate.hyps(2,3) subst_img_update
        unfolding range_vars_alt_def by (fastforce simp add: subst_domain_def)+
      hence "subst_domain δ ∩ range_vars δ = {}" using FUpdate.prems(1) by blast
      hence "δ ∈ wfsubst_set" using FUpdate.IH by metis

      have *: "range_vars (δ(v := t)) = range_vars δ ∪ fv t"
        using FUpdate.hyps(2) subst_img_update[OF _ FUpdate.hyps(3)]
        by fastforce
      hence "fv t ∩ insert v (subst_domain δ) = {}"
        using FUpdate.prems subst_dom_update2[OF FUpdate.hyps(3)] by blast
      moreover have "subst_domain (δ(v := t)) = insert v (subst_domain δ)"
        by (meson FUpdate.hyps(3) subst_dom_update2)
      hence "v ∉ range_vars δ" using FUpdate.prems * by blast
      ultimately show ?case using Insert[OF ‹δ ∈ wfsubst_set› ‹v ∉ subst_domain δ›] by metis
    qed
  qed

  show "θ ∈ wfsubst_set ⟹ wfsubst θ" unfolding wfsubst_def
  proof (induction θ rule: wfsubst_set.induct)
    case Empty thus ?case by simp
  next
    case (Insert σ v t)
    hence 1: "subst_domain σ ∩ range_vars σ = {}" by simp
    hence 2: "subst_domain (σ(v := t)) ∩ range_vars σ = {}"
      using Insert.hyps(3) by (auto simp add: subst_domain_def)
    have 3: "fv t ∩ subst_domain (σ(v := t)) = {}"
      using Insert.hyps(4) by (auto simp add: subst_domain_def)
    have 4: "σ v = Var v" using ‹v ∉ subst_domain σ› by (simp add: subst_domain_def)
  
    from Insert.IH have "finite (subst_domain σ)" by simp
    hence 5: "finite (subst_domain (σ(v := t)))" using subst_dom_insert_finite[of σ] by simp
  
    have "subst_domain (σ(v := t)) ∩ range_vars (σ(v := t)) = {}"
    proof (cases "t = Var v")
      case True
      hence "range_vars (σ(v := t)) = range_vars σ"
        using 4 fun_upd_triv term.inject(1)
        unfolding range_vars_alt_def by (auto simp add: subst_domain_def) 
      thus "subst_domain (σ(v := t)) ∩ range_vars (σ(v := t)) = {}"
        using 1 2 3 by auto
    next
      case False
      hence "range_vars (σ(v := t)) = fv t ∪ (range_vars σ)"
        using 4 subst_img_update[of σ v] by auto
      thus "subst_domain (σ(v := t)) ∩ range_vars (σ(v := t)) = {}" using 1 2 3 by blast
    qed
    thus ?case using 5 by blast 
  qed
qed

lemma wfsubst_induct[consumes 1, case_names Empty Insert]:
  assumes "wfsubst δ" "P Var"
  and "⋀θ v t. ⟦wfsubst θ; P θ; v ∉ subst_domain θ; v ∉ range_vars θ;
                fv t ∩ insert v (subst_domain θ) = {}⟧
                ⟹ P (θ(v := t))"
  shows "P δ"
proof -
  from assms(1,3) wf_subst_properties have
    "δ ∈ wfsubst_set"
    "⋀θ v t. ⟦θ ∈ wfsubst_set; P θ; v ∉ subst_domain θ; v ∉ range_vars θ;
              fv t ∩ insert v (subst_domain θ) = {}⟧
              ⟹ P (θ(v := t))"
    by blast+
  thus "P δ" using wfsubst_set.induct assms(2) by blast
qed  

lemma wf_subst_fsubst: "wfsubst δ ⟹ δ ∈ fsubst"
unfolding wfsubst_def using finite_dom_iff_fsubst by blast 

lemma wf_subst_nil: "wfsubst Var" unfolding wfsubst_def by simp

lemma wf_MGU_nil: "MGU Var s t ⟹ wfMGU Var s t"
using wf_subst_nil subst_domain_Var range_vars_Var
unfolding wfMGU_def by fast

lemma wf_MGU_dom_bound: "wfMGU θ s t ⟹ subst_domain θ ⊆ fv s ∪ fv t" unfolding wfMGU_def by blast

lemma wf_subst_single:
  assumes "v ∉ fv t" "σ v = t" "⋀w. v ≠ w ⟹ σ w = Var w"
  shows "wfsubst σ"
proof -
  have *: "subst_domain σ = {v}" by (metis subst_fv_dom_img_single(1)[OF assms])

  have "subst_domain σ ∩ range_vars σ = {}"
    using * assms subst_fv_dom_img_single(2)
    by (metis inf_bot_left insert_disjoint(1))
  moreover have "finite (subst_domain σ)" using * by simp
  ultimately show ?thesis by (metis wfsubst_def)
qed

lemma wf_subst_reduction:
  "wfsubst s ⟹ wfsubst (rm_var v s)"
proof -
  assume "wfsubst s"
  moreover have "subst_domain (rm_var v s) ⊆ subst_domain s" by (auto simp add: subst_domain_def)
  moreover have "range_vars (rm_var v s) ⊆ range_vars s"
    unfolding range_vars_alt_def by (auto simp add: subst_domain_def)
  ultimately have "subst_domain (rm_var v s) ∩ range_vars (rm_var v s) = {}"
    by (meson compl_le_compl_iff disjoint_eq_subset_Compl subset_trans wfsubst_def)
  moreover have "finite (subst_domain (rm_var v s))"
    using ‹subst_domain (rm_var v s) ⊆ subst_domain s› ‹wfsubst s› rev_finite_subset
    unfolding wfsubst_def by blast
  ultimately show "wfsubst (rm_var v s)" by (metis wfsubst_def)
qed

lemma wf_subst_compose:
  assumes "wfsubst θ1" "wfsubst θ2"
    and "subst_domain θ1 ∩ subst_domain θ2 = {}"
    and "subst_domain θ1 ∩ range_vars θ2 = {}"
  shows "wfsubst (θ1 ∘s θ2)"
using assms
proof (induction θ1 rule: wfsubst_induct)
  case Empty thus ?case unfolding wfsubst_def by simp
next
  case (Insert σ1 v t)
  have "t ≠ Var v" using Insert.hyps(4) by auto
  hence dom1v_unfold: "subst_domain (σ1(v := t)) = insert v (subst_domain σ1)"
    using subst_dom_update2 by metis
  hence doms_disj: "subst_domain σ1 ∩ subst_domain θ2 = {}" 
    using Insert.prems(2) disjoint_insert(1) by blast
  moreover have dom_img_disj: "subst_domain σ1 ∩ range_vars θ2 = {}"
    using Insert.hyps(2) Insert.prems(3)
    by (fastforce simp add: subst_domain_def)
  ultimately have "wfsubst (σ1 ∘s θ2)" using Insert.IH[OF ‹wfsubst θ2›] by metis

  have dom_comp_is_union: "subst_domain (σ1 ∘s θ2) = subst_domain σ1 ∪ subst_domain θ2"
    using subst_dom_comp_eq[OF dom_img_disj] .

  have "v ∉ subst_domain θ2"
    using Insert.prems(2) ‹t ≠ Var v›
    by (fastforce simp add: subst_domain_def)
  hence "θ2 v = Var v" "σ1 v = Var v" using Insert.hyps(2) by (simp_all add: subst_domain_def)
  hence "(σ1 ∘s θ2) v = Var v" "(σ1(v := t) ∘s θ2) v = t ⋅ θ2" "((σ1 ∘s θ2)(v := t)) v = t"
    unfolding subst_compose_def by simp_all
  
  have fv_t2_bound: "fv (t ⋅ θ2) ⊆ fv t ∪ range_vars θ2" by (meson subst_sends_fv_to_img)

  have 1: "v ∉ subst_domain (σ1 ∘s θ2)"
    using ‹(σ1 ∘s θ2) v = Var v›
    by (auto simp add: subst_domain_def)

  have "insert v (subst_domain σ1) ∩ range_vars θ2 = {}"
    using Insert.prems(3) dom1v_unfold by blast
  hence "v ∉ range_vars σ1 ∪ range_vars θ2" using Insert.hyps(3) by blast
  hence 2: "v ∉ range_vars (σ1 ∘s θ2)" by (meson set_rev_mp subst_img_comp_subset)

  have "subst_domain θ2 ∩ range_vars θ2 = {}"
    using ‹wfsubst θ2› unfolding wfsubst_def by simp
  hence "fv (t ⋅ θ2) ∩ subst_domain θ2 = {}"
    using subst_dom_elim unfolding range_vars_alt_def by simp
  moreover have "v ∉ range_vars θ2" using Insert.prems(3) dom1v_unfold by blast
  hence "v ∉ fv t ∪ range_vars θ2" using Insert.hyps(4) by blast
  hence "v ∉ fv (t ⋅ θ2)" using ‹fv (t ⋅ θ2) ⊆ fv t ∪ range_vars θ2› by blast
  moreover have "fv (t ⋅ θ2) ∩ subst_domain σ1 = {}"
    using dom_img_disj fv_t2_bound ‹fv t ∩ insert v (subst_domain σ1) = {}› by blast
  ultimately have 3: "fv (t ⋅ θ2) ∩ insert v (subst_domain (σ1 ∘s θ2)) = {}"
    using dom_comp_is_union by blast

  have "σ1(v := t) ∘s θ2 = (σ1 ∘s θ2)(v := t ⋅ θ2)" using subst_comp_upd1[of σ1 v t θ2] .
  moreover have "wfsubst ((σ1 ∘s θ2)(v := t ⋅ θ2))"
    using "wfsubst_set.Insert"[OF _ 1 2 3] ‹wfsubst (σ1 ∘s θ2)› wf_subst_properties by metis
  ultimately show ?case by presburger
qed

lemma wf_subst_append:
  fixes θ1 θ2::"('f,'v) subst"
  assumes "wfsubst θ1" "wfsubst θ2"
    and "subst_domain θ1 ∩ subst_domain θ2 = {}"
    and "subst_domain θ1 ∩ range_vars θ2 = {}"
    and "range_vars θ1 ∩ subst_domain θ2 = {}"
  shows "wfsubst (λv. if θ1 v = Var v then θ2 v else θ1 v)"
using assms
proof (induction θ1 rule: wfsubst_induct)
  case Empty thus ?case unfolding wfsubst_def by simp
next
  case (Insert σ1 v t)
  let ?if = "λw. if σ1 w = Var w then θ2 w else σ1 w"
  let ?if_upd = "λw. if (σ1(v := t)) w = Var w then θ2 w else (σ1(v := t)) w"

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

  have dom_insert: "subst_domain (σ1(v := t)) = insert v (subst_domain σ1)"
    using Insert.hyps(4) by (auto simp add: subst_domain_def)

  have "σ1 v = Var v" "t ≠ Var v" using Insert.hyps(2,4) by auto
  hence img_insert: "range_vars (σ1(v := t)) = range_vars σ1 ∪ fv t"
    using subst_img_update by metis

  from Insert.prems(2) dom_insert have "subst_domain σ1 ∩ subst_domain θ2 = {}"
    by (auto simp add: subst_domain_def)
  moreover have "subst_domain σ1 ∩ range_vars θ2 = {}"
    using Insert.prems(3) dom_insert
    by (simp add: subst_domain_def)
  moreover have "range_vars σ1 ∩ subst_domain θ2 = {}"
    using Insert.prems(4) img_insert
    by blast
  ultimately have "wfsubst ?if" using Insert.IH[OF Insert.prems(1)] by metis
  
  have dom_union: "subst_domain ?if = subst_domain σ1 ∪ subst_domain θ2"
    by (auto simp add: subst_domain_def)
  hence "v ∉ subst_domain ?if"
    using Insert.hyps(2) Insert.prems(2) dom_insert
    by (auto simp add: subst_domain_def)
  moreover have "v ∉ range_vars ?if"
    using Insert.prems(3) Insert.hyps(3) dom_insert
    unfolding range_vars_alt_def by (auto simp add: subst_domain_def)
  moreover have "fv t ∩ insert v (subst_domain ?if) = {}"
    using Insert.hyps(4) Insert.prems(4) img_insert
    unfolding range_vars_alt_def by (fastforce simp add: subst_domain_def)
  ultimately show ?case
    using wfsubst_set.Insert ‹wfsubst ?if› ‹?if_upd = ?if(v := t)› wf_subst_properties
    by (metis (no_types, lifting))  
qed

lemma wf_subst_elim_append:
  assumes "wfsubst θ" "subst_elim θ v" "v ∉ fv t"
  shows "subst_elim (θ(w := t)) v"
using assms
proof (induction θ rule: wfsubst_induct)
  case (Insert θ v' t')
  hence "⋀q. v ∉ fv (Var q ⋅ θ(v' := t'))" using subst_elimD by blast
  hence "⋀q. v ∉ fv (Var q ⋅ θ(v' := t', w := t))" using ‹v ∉ fv t› by simp
  thus ?case by (metis subst_elimI' eval_term.simps(1)) 
qed (simp add: subst_elim_def)

lemma wf_subst_elim_dom:
  assumes "wfsubst θ"
  shows "∀v ∈ subst_domain θ. subst_elim θ v"
using assms
proof (induction θ rule: wfsubst_induct)
  case (Insert θ w t)
  have dom_insert: "subst_domain (θ(w := t)) ⊆ insert w (subst_domain θ)"
    by (auto simp add: subst_domain_def)
  hence "∀v ∈ subst_domain θ. subst_elim (θ(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 ∉ fv t" using Insert.hyps(4) by simp
  hence "⋀q. w ∉ fv (Var q ⋅ θ(w := t))"
    by (metis fv_simps(1) fv_in_subst_img Insert.hyps(3) contra_subsetD 
              fun_upd_def singletonD eval_term.simps(1)) 
  hence "subst_elim (θ(w := t)) w" by (metis subst_elimI')
  ultimately show ?case using dom_insert by blast
qed simp

lemma wf_subst_support_iff_mgt: "wfsubst θ ⟹ θ supports δ ⟷ θ ≼∘ δ"
using subst_support_def subst_support_if_mgt_subst_idem wf_subst_subst_idem by blast 


subsection ‹Interpretations›
abbreviation interpretationsubst::"('a,'b) subst ⇒ bool" where
  "interpretationsubst θ ≡ subst_domain θ = UNIV ∧ ground (subst_range θ)"

lemma interpretation_substI:
  "(⋀v. fv (θ v) = {}) ⟹ interpretationsubst θ"
proof -
  assume "⋀v. fv (θ v) = {}"
  moreover { fix v assume "fv (θ v) = {}" hence "v ∈ subst_domain θ" by auto }
  ultimately show ?thesis by auto
qed

lemma interpretation_grounds[simp]:
  "interpretationsubst θ ⟹ fv (t ⋅ θ) = {}"
using subst_fv_dom_ground_if_ground_img[of t θ] by blast

lemma interpretation_grounds_all:
  "interpretationsubst θ ⟹ (⋀v. fv (θ v) = {})"
by (metis range_vars_alt_def UNIV_I fv_in_subst_img subset_empty subst_dom_vars_in_subst)

lemma interpretation_grounds_all':
  "interpretationsubst θ ⟹ ground (M ⋅set θ)"
using subst_fv_dom_ground_if_ground_img[of _ θ]
by simp

lemma interpretation_comp:
  assumes "interpretationsubst θ" 
  shows "interpretationsubst (σ ∘s θ)" "interpretationsubst (θ ∘s σ)"
proof -
  have θ_fv: "fv (θ v) = {}" for v using interpretation_grounds_all[OF assms] by simp
  hence θ_fv': "fv (t ⋅ θ) = {}" for t
    by (metis all_not_in_conv subst_elimD subst_elimI' eval_term.simps(1))

  from assms have "(σ ∘s θ) v ≠ Var v" for v
    unfolding subst_compose_def by (metis fv_simps(1) θ_fv' insert_not_empty)
  hence "subst_domain (σ ∘s θ) = UNIV" by (simp add: subst_domain_def)
  moreover have "fv ((σ ∘s θ) v) = {}" for v unfolding subst_compose_def using θ_fv' by simp
  hence "ground (subst_range (σ ∘s θ))" by simp
  ultimately show "interpretationsubst (σ ∘s θ)" ..

  from assms have "(θ ∘s σ) v ≠ Var v" for v
    unfolding subst_compose_def by (metis fv_simps(1) θ_fv insert_not_empty subst_to_var_is_var)
  hence "subst_domain (θ ∘s σ) = UNIV" by (simp add: subst_domain_def)
  moreover have "fv ((θ ∘s σ) v) = {}" for v
    unfolding subst_compose_def by (simp add: θ_fv subst_apply_term_ident) 
  hence "ground (subst_range (θ ∘s σ))" by simp
  ultimately show "interpretationsubst (θ ∘s σ)" ..
qed

lemma interpretation_subst_exists:
  "∃ℐ::('f,'v) subst. interpretationsubst ℐ"
proof -
  obtain c::"'f" where "c ∈ UNIV" by simp
  then obtain ℐ::"('f,'v) subst" where "⋀v. ℐ v = Fun c []" by simp
  hence "subst_domain ℐ = UNIV" "ground (subst_range ℐ)"
    by (simp_all add: subst_domain_def)
  thus ?thesis by auto
qed

lemma interpretation_subst_exists':
  "∃θ::('f,'v) subst. subst_domain θ = X ∧ ground (subst_range θ)"
proof -
  obtain ℐ::"('f,'v) subst" where ℐ: "subst_domain ℐ = UNIV" "ground (subst_range ℐ)"
    using interpretation_subst_exists by atomize_elim auto
  let ?θ = "rm_vars (UNIV - X) ℐ"
  have 1: "subst_domain ?θ = X" using ℐ by (auto simp add: subst_domain_def)
  hence 2: "ground (subst_range ?θ)" using ℐ by force
  show ?thesis using 1 2 by blast
qed

lemma interpretation_subst_idem:
  "interpretationsubst θ ⟹ subst_idem θ"
unfolding subst_idem_def
  using interpretation_grounds_all[of θ] subst_apply_term_ident subst_eq_if_eq_vars
by (fastforce simp: subst_compose)

lemma subst_idem_comp_upd_eq:
  assumes "v ∉ subst_domain ℐ" "subst_idem θ"
  shows "ℐ ∘s θ = ℐ(v := θ v) ∘s θ"
proof -
  from assms(1) have "(ℐ ∘s θ) v = θ v" unfolding subst_compose_def by auto
  moreover have "⋀w. w ≠ v ⟹ (ℐ ∘s θ) w = (ℐ(v := θ v) ∘s θ) w" unfolding subst_compose_def by auto
  moreover have "(ℐ(v := θ v) ∘s θ) v = θ v" using assms(2) unfolding subst_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:
  "interpretationsubst ℐ ⟹ subst_domain ℐ ∩ range_vars ℐ = {}"
unfolding range_vars_alt_def by auto


subsection ‹Basic Properties of MGUs›
lemma MGU_is_mgu_singleton: "MGU θ t u = is_mgu θ {(t,u)}"
unfolding is_mgu_def unifiers_def by auto

lemma Unifier_in_unifiers_singleton: "Unifier θ s t ⟷ θ ∈ unifiers {(s,t)}"
unfolding unifiers_def by auto

lemma subst_list_singleton_fv_subset:
  "(⋃x ∈ set (subst_list (subst v t) E). fv (fst x) ∪ fv (snd x))
    ⊆ fv t ∪ (⋃x ∈ set E. fv (fst x) ∪ fv (snd x))"
proof (induction E)
  case (Cons x E)
  let ?fvs = "λL. ⋃x ∈ set L. fv (fst x) ∪ fv (snd x)"
  let ?fvx = "fv (fst x) ∪ fv (snd x)"
  let ?fvxsubst = "fv (fst x ⋅ Var(v := t)) ∪ fv (snd x ⋅ Var(v := t))"
  have "?fvs (subst_list (subst v t) (x#E)) = ?fvxsubst ∪ ?fvs (subst_list (subst v t) E)"
    unfolding subst_list_def subst_def by auto
  hence "?fvs (subst_list (subst v t) (x#E)) ⊆ ?fvxsubst ∪ fv t ∪ ?fvs E"
    using Cons.IH by blast
  moreover have "?fvs (x#E) = ?fvx ∪ ?fvs E" by auto
  moreover have "?fvxsubst ⊆ ?fvx ∪ fv t" using subst_fv_bound_singleton[of _ v t] by blast
  ultimately show ?case unfolding range_vars_alt_def by auto
qed (simp add: subst_list_def)

lemma subst_of_dom_subset: "subst_domain (subst_of L) ⊆ 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) ∘s subst_of L"
    unfolding subst_of_def subst_def by (induct L) (auto simp: subst_compose)
  hence "subst_domain (subst_of (L@[x])) ⊆ insert v (subst_domain (subst_of L))"
    using x subst_domain_compose[of "Var(v := t)" "subst_of L"]
    by (auto simp add: subst_domain_def)
  thus ?case using snoc.IH x by auto
qed simp

lemma wf_MGU_is_imgu_singleton: "wfMGU θ s t ⟹ is_imgu θ {(s,t)}"
proof -
  assume 1: "wfMGU θ s t"

  have 2: "subst_idem θ" by (metis wf_subst_subst_idem 1 wfMGU_def)

  have 3: "∀θ' ∈ unifiers {(s,t)}. θ ≼∘ θ'" "θ ∈ unifiers {(s,t)}"
    by (metis 1 Unifier_in_unifiers_singleton wfMGU_def)+

  have "∀τ ∈ unifiers {(s,t)}. τ = θ ∘s τ" by (metis 2 3 subst_idem_def subst_compose_assoc)
  thus "is_imgu θ {(s,t)}" by (metis is_imgu_def ‹θ ∈ unifiers {(s,t)}›)
qed

lemmas mgu_subst_range_vars = mgu_range_vars

lemmas mgu_same_empty = mgu_same

lemma mgu_var: assumes "x ∉ fv t" shows "mgu (Var x) t = Some (Var(x := t))"
proof -
  have "unify [(Var x,t)] [] = Some [(x,t)]" using assms by (auto simp add: subst_list_def)
  moreover have "subst_of [(x,t)] = Var(x := t)" unfolding subst_of_def subst_def by simp
  ultimately show ?thesis by (simp add: mgu_def)
qed

lemma mgu_gives_wellformed_subst:
  assumes "mgu s t = Some θ" shows "wfsubst θ"
using mgu_finite_subst_domain[OF assms] mgu_subst_domain_range_vars_disjoint[OF assms]
unfolding wfsubst_def
by auto

lemma mgu_gives_wellformed_MGU:
  assumes "mgu s t = Some θ" shows "wfMGU θ s t"
using mgu_subst_domain[OF assms] mgu_sound[OF assms] mgu_subst_range_vars [OF assms]
      MGU_is_mgu_singleton[of s θ t] is_imgu_imp_is_mgu[of θ "{(s,t)}"]
      mgu_gives_wellformed_subst[OF assms]
unfolding wfMGU_def by blast

lemma mgu_gives_subst_idem: "mgu s t = Some θ ⟹ subst_idem θ"
using mgu_sound[of s t θ] unfolding is_imgu_def subst_idem_def by auto

lemma mgu_always_unifies: "Unifier θ M N ⟹ ∃δ. mgu M N = Some δ"
using mgu_complete Unifier_in_unifiers_singleton by blast

lemma mgu_gives_MGU: "mgu s t = Some θ ⟹ MGU θ s t"
using mgu_sound[of s t θ, THEN is_imgu_imp_is_mgu] MGU_is_mgu_singleton by metis

lemma mgu_vars_bounded[dest?]:
  "mgu M N = Some σ ⟹ subst_domain σ ∪ range_vars σ ⊆ fv M ∪ fv N"
using mgu_gives_wellformed_MGU unfolding wfMGU_def by blast

lemma mgu_vars_bounded':
  assumes σ: "mgu M N = Some σ"
    and MN: "fv M = {} ∨ fv N = {}"
  shows "subst_domain σ = fv M ∪ fv N" (is ?A)
    and "range_vars σ = {}" (is ?B)
proof -
  let ?C = "λt. subst_domain σ = fv t"

  have 0: "fv N = {} ⟹ subst_domain σ ⊆ fv M" "fv N = {} ⟹ range_vars σ ⊆ fv M"
          "fv M = {} ⟹ subst_domain σ ⊆ fv N" "fv M = {} ⟹ range_vars σ ⊆ fv N"
    using mgu_vars_bounded[OF σ] by simp_all

  note 1 = mgu_gives_MGU[OF σ] mgu_subst_domain_range_vars_disjoint[OF σ]
  note 2 = subst_fv_imgI[of σ] subst_dom_vars_in_subst[of _ σ]
  note 3 = ground_term_subst_domain_fv_subset[of _ σ]
  note 4 = subst_apply_fv_empty[of _ σ]

  have "fv (σ x) = {}" when x: "x ∈ fv M" and N: "fv N = {}" for x
    using x N 0(1,2) 1 2[of x] 3[of M] 4[of N] by auto
  hence "?C M" ?B when N: "fv N = {}" using 0(1,2)[OF N] N by (fastforce, fastforce)
  moreover have "fv (σ x) = {}" when x: "x ∈ fv N" and M: "fv M = {}" for x
    using x M 0(3,4) 1 2[of x] 3[of N] 4[of M] by auto
  hence "?C N" ?B when M: "fv M = {}" using 0(3,4)[OF M] M by (fastforce, fastforce)
  ultimately show ?A ?B using MN by auto
qed

lemma mgu_eliminates[dest?]:
  assumes "mgu M N = Some σ"
  shows "(∃v ∈ fv M ∪ fv N. subst_elim σ v) ∨ σ = Var"
  (is "?P M N σ")
proof (cases "σ = Var")
  case False
  then obtain v where v: "v ∈ subst_domain σ" by auto
  hence "v ∈ fv M ∪ fv N" using mgu_vars_bounded[OF assms] by blast
  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 θ" "v ∈ subst_domain θ"
  shows "subst_elim θ v"
using mgu_gives_wellformed_subst[OF assms(1)]
unfolding wfMGU_def wfsubst_def subst_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 "(⋃x ∈ set E. fv (fst x) ∪ fv (snd x)) ∩ 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 = "λL. ⋃x ∈ set L. fv (fst x) ∪ 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 "⋀t t'. (t,t') ∈ set E' ⟹ fv t ⊆ fv (Fun f X) ∧ fv t' ⊆ fv (Fun g Y)"
    by (metis zip_arg_subterm subtermeq_vars_subset)
  hence "?fvs E' ⊆ fv (Fun f X) ∪ fv (Fun g Y)" by fastforce
  moreover have "fv (Fun f X) ∩ set (map fst B) = {}" "fv (Fun g Y) ∩ set (map fst B) = {}"
    using "2.prems"(3) by auto
  ultimately have "?fvs E' ∩ set (map fst B) = {}" by blast
  moreover have "?fvs E ∩ set (map fst B) = {}" using "2.prems"(3) by auto
  ultimately have "?fvs (E'@E) ∩ 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 = "λL. ⋃x ∈ set L. fv (fst x) ∪ fv (snd x)"
  let ?E' = "subst_list (subst v t) E"
  from "3.prems"(3) have "v ∉ set (map fst B)" "fv t ∩ 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 ∉ fv t" using "3.prems"(1) by auto
    hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using ‹t ≠ Var v› "3.prems"(1) by auto
    moreover have "?fvs ?E' ∩ set (map fst ((v, t)#B)) = {}"
    proof -
      have "v ∉ ?fvs ?E'"
        unfolding subst_list_def subst_def
        by (simp add: ‹v ∉ fv t› subst_remove_var)
      moreover have "?fvs ?E' ⊆ fv t ∪ ?fvs E" by (metis subst_list_singleton_fv_subset)
      hence "?fvs ?E' ∩ set (map fst B) = {}" using "3.prems"(3) by auto
      ultimately show ?thesis by auto
    qed 
    ultimately show ?thesis using "3.IH"(2)[OF ‹t ≠ Var v› ‹v ∉ fv t› _ *] by metis
  qed
next
  case (4 f X v E B U)
  let ?fvs = "λL. ⋃x ∈ set L. fv (fst x) ∪ fv (snd x)"
  let ?E' = "subst_list (subst v (Fun f X)) E"
  have *: "?fvs E ∩ set (map fst B) = {}" using "4.prems"(3) by auto
  from "4.prems"(1) have "v ∉ fv (Fun f X)" by force
  from "4.prems"(3) have **: "v ∉ set (map fst B)" "fv (Fun f X) ∩ 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' ∩ set (map fst ((v, Fun f X)#B)) = {}"
  proof -
    have "v ∉ ?fvs ?E'"
      unfolding subst_list_def subst_def
      using ‹v ∉ fv (Fun f X)› subst_remove_var[of v "Fun f X"] by simp
    moreover have "?fvs ?E' ⊆ fv (Fun f X) ∪ ?fvs E" by (metis subst_list_singleton_fv_subset)
    hence "?fvs ?E' ∩ 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 ‹v ∉ fv (Fun f X)› "4.prems"(1) by auto
  thus ?case using "4.IH"[OF ‹v ∉ fv (Fun f X)› _ *** ****] by metis
qed

lemma mgu_None_is_subst_neq:
  fixes s t::"('a,'b) term" and δ::"('a,'b) subst"
  assumes "mgu s t = None"
  shows "s ⋅ δ ≠ t ⋅ δ"
using assms mgu_always_unifies by force

lemma mgu_None_if_neq_ground:
  assumes "t ≠ t'" "fv t = {}" "fv t' = {}"
  shows "mgu t t' = None"
proof (rule ccontr)
  assume "mgu t t' ≠ None"
  then obtain δ where δ: "mgu t t' = Some δ" by auto
  hence "t ⋅ δ = t" "t' ⋅ δ = t'" using assms subst_ground_ident by auto
  thus False using assms(1) MGU_is_Unifier[OF mgu_gives_MGU[OF δ]] by auto
qed

lemma mgu_None_commutes:
  "mgu s t = None ⟹ mgu t s = None"
  thm mgu_complete[of s t] Unifier_in_unifiers_singleton[of ]
using mgu_complete[of s t]
      Unifier_in_unifiers_singleton[of s _ t]
      Unifier_sym[of t _ s]
      Unifier_in_unifiers_singleton[of t _ s]
      mgu_sound[of t s]
unfolding is_imgu_def
by fastforce

lemma mgu_img_subterm_subst:
  fixes δ::"('f,'v) subst" and s t u::"('f,'v) term"
  assumes "mgu s t = Some δ" "u ∈ subtermsset (subst_range δ) - range Var"
  shows "u ∈ ((subterms s ∪ subterms t) - range Var) ⋅set δ"
proof -
  define subterms_tuples::"('f,'v) equation list ⇒ ('f,'v) terms" where subtt_def:
    "subterms_tuples ≡ λE. subtermsset (fst ` set E) ∪ subtermsset (snd ` set E)"
  define subterms_img::"('f,'v) subst ⇒ ('f,'v) terms" where subti_def:
    "subterms_img ≡ λd. subtermsset (subst_range d)"

  define d where "d ≡ λv t. subst v t::('f,'v) subst"
  define V where "V ≡ range Var::('f,'v) terms"
  define R where "R ≡ λd::('f,'v) subst. ((subterms s ∪ subterms t) - V) ⋅set d"
  define M where "M ≡ λE d. subterms_tuples E ∪ subterms_img d"
  define Q where "Q ≡ (λE d. M E d - V ⊆ R d - V)"
  define Q' where "Q' ≡ (λE d d'. (M E d - V) ⋅set d' ⊆ (R d - V) ⋅set (d'::('f,'v) subst))"

  have Q_subst: "Q (subst_list (subst v t') E) (subst_of ((v, t')#B))" 
    when v_fv: "v ∉ fv t'" and Q_assm: "Q ((Var v, t')#E) (subst_of B)"
    for v t' E B
  proof -
    define E' where "E' ≡ subst_list (subst v t') E"
    define B' where "B' ≡ subst_of ((v, t')#B)"

    have E': "E' = subst_list (d v t') E"
        and B': "B' = subst_of B ∘s d v t'"
      using subst_of_simps(3)[of "(v, t')"]
      unfolding subst_def E'_def B'_def d_def by simp_all

    have vt_img_subt: "subtermsset (subst_range (d v t')) = subterms t'"
         and vt_dom: "subst_domain (d v t') = {v}"
      using v_fv by (auto simp add: subst_domain_def d_def subst_def)

    have *: "subterms u1 ⊆ subtermsset (fst ` set E)" "subterms u2 ⊆ subtermsset (snd ` set E)"
      when "(u1,u2) ∈ set E" for u1 u2
      using that by auto

    have **: "subtermsset (d v t' ` (fv u ∩ subst_domain (d v t'))) ⊆ subterms t'"
      for u::"('f,'v) term"
      using vt_dom unfolding d_def by force

    have 1: "subterms_tuples E' - V ⊆ (subterms t' - V) ∪ (subterms_tuples E - V ⋅set d v t')"
      (is "?A ⊆ ?B")
    proof
      fix u assume "u ∈ ?A"
      then obtain u1 u2 where u12:
          "(u1,u2) ∈ set E"
          "u ∈ (subterms (u1 ⋅ (d v t')) - V) ∪ (subterms (u2 ⋅ (d v t')) - V)"
        unfolding subtt_def subst_list_def E'_def d_def by atomize_elim force
      hence "u ∈ (subterms t' - V) ∪ (((subterms_tuples E) ⋅set d v t') - V)"
        using subterms_subst[of u1 "d v t'"] subterms_subst[of u2 "d v t'"]
              *[OF u12(1)] **[of u1] **[of u2]
        unfolding subtt_def subst_list_def by auto
      moreover have
          "(subterms_tuples E ⋅set d v t') - V ⊆
           (subterms_tuples E - V ⋅set d v t') ∪ {t'}"
        unfolding subst_def subtt_def V_def d_def by force
      ultimately show "u ∈ ?B" using u12 v_fv by auto
    qed

    have 2: "subterms_img B' - V ⊆
             (subterms t' - V) ∪ (subterms_img (subst_of B) - V ⋅set d v t')"
      using B' vt_img_subt subst_img_comp_subset'''[of "subst_of B" "d v t'"]
      unfolding subti_def subst_def V_def by argo

    have 3: "subterms_tuples ((Var v, t')#E) - V = (subterms t' - V) ∪ (subterms_tuples E - V)"
      by (auto simp add: subst_def subtt_def V_def)

    have "fvset (subterms t' - V) ∩ subst_domain (d v t') = {}"
      using v_fv vt_dom fv_subterms[of t'] by fastforce
    hence 4: "subterms t' - V ⋅set d v t' = subterms t' - V"
      using set_subst_ident[of "subterms t' - range Var" "d v t'"] by (simp add: V_def)

    have "M E' B' - V ⊆ M ((Var v, t')#E) (subst_of B) - V ⋅set d v t'"
      using 1 2 3 4 unfolding M_def by blast
    moreover have "Q' ((Var v, t')#E) (subst_of B) (d v t')"
      using Q_assm unfolding Q_def Q'_def by auto
    moreover have "R (subst_of B) ⋅set d v t' = R (subst_of ((v,t')#B))"
      unfolding R_def d_def by auto 
    ultimately have
      "M (subst_list (d v t') E) (subst_of ((v, t')#B)) - V ⊆ R (subst_of ((v, t')#B)) - V"
      unfolding Q'_def E'_def B'_def d_def by blast
    thus ?thesis unfolding Q_def M_def R_def d_def by blast
  qed

  have "u ∈ subterms s ∪ subterms t - V ⋅set subst_of U"
    when assms':
      "unify E B = Some U"
      "u ∈ subtermsset (subst_range (subst_of U)) - V"
      "Q E (subst_of B)"
    for E B U and T::"('f,'v) term list"
    using assms'
  proof (induction E B arbitrary: U rule: Unification.unify.induct)
    case (1 B) thus ?case by (auto simp add: Q_def M_def R_def subti_def)
  next
    case (2 g X h Y E B U)
    from "2.prems"(1) obtain E' where E':
        "decompose (Fun g X) (Fun h Y) = Some E'"
        "g = h" "length X = length Y" "E' = zip X Y"
        "Unification.unify (E'@E) B = Some U"
      by (auto split: option.splits)
    moreover have "subterms_tuples (E'@E) ⊆ subterms_tuples ((Fun g X, Fun h Y)#E)"
    proof
      fix u assume "u ∈ subterms_tuples (E'@E)"
      then obtain u1 u2 where u12: "(u1,u2) ∈ set (E'@E)" "u ∈ subterms u1 ∪ subterms u2"
        unfolding subtt_def by fastforce
      thus "u ∈ subterms_tuples ((Fun g X, Fun h Y)#E)"
      proof (cases "(u1,u2) ∈ set E'")
        case True
        hence "subterms u1 ⊆ subterms (Fun g X)" "subterms u2 ⊆ subterms (Fun h Y)"
          using E'(4) subterms_subset params_subterms subsetCE
          by (metis set_zip_leftD, metis set_zip_rightD)
        thus ?thesis using u12 unfolding subtt_def by auto
      next
        case False thus ?thesis using u12 unfolding subtt_def by fastforce
      qed
     qed
    hence "Q (E'@E) (subst_of B)" using "2.prems"(3) unfolding Q_def M_def by blast
    ultimately show ?case using "2.IH"[of E' U] "2.prems" by meson
  next
    case (3 v t' E B)
    show ?case
    proof (cases "t' = Var v")
      case True thus ?thesis
        using "3.prems" "3.IH"(1) unfolding Q_def M_def V_def subtt_def by auto
    next
      case False
      hence 1: "v ∉ fv t'" using "3.prems"(1) by auto
      hence "unify (subst_list (subst v t') E) ((v, t')#B) = Some U"
        using False "3.prems"(1) by auto
      thus ?thesis
        using Q_subst[OF 1 "3.prems"(3)]
              "3.IH"(2)[OF False 1 _ "3.prems"(2)]
        by metis
    qed
  next
    case (4 g X v E B U)
    have 1: "v ∉ fv (Fun g X)" using "4.prems"(1) not_None_eq by fastforce
    hence 2: "unify (subst_list (subst v (Fun g X)) E) ((v, Fun g X)#B) = Some U"
      using "4.prems"(1) by auto

    have 3: "Q ((Var v, Fun g X)#E) (subst_of B)"
      using "4.prems"(3) unfolding Q_def M_def subtt_def by auto
    
    show ?case
      using Q_subst[OF 1 3] "4.IH"[OF 1 2 "4.prems"(2)]
      by metis
  qed
  moreover obtain D where "unify [(s, t)] [] = Some D" "δ = subst_of D"
    using assms(1) by (auto simp: mgu_def split: option.splits)
  moreover have "Q [(s,t)] (subst_of [])"
    unfolding Q_def M_def R_def subtt_def subti_def
    by force
  ultimately show ?thesis using assms(2) unfolding V_def by auto
qed

lemma mgu_img_consts:
  fixes δ::"('f,'v) subst" and s t::"('f,'v) term" and c::'f and z::'v
  assumes "mgu s t = Some δ" "Fun c [] ∈ subtermsset (subst_range δ)"
  shows "Fun c [] ∈ subterms s ∪ subterms t"
proof -
  obtain u where "u ∈ (subterms s ∪ subterms t) - range Var" "u ⋅ δ = Fun c []"
    using mgu_img_subterm_subst[OF assms(1), of "Fun c []"] assms(2) by force
  thus ?thesis by (cases u) auto
qed

lemma mgu_img_consts':
  fixes δ::"('f,'v) subst" and s t::"('f,'v) term" and c::'f and z::'v
  assumes "mgu s t = Some δ" "δ z = Fun c []"
  shows "Fun c [] ⊑ s ∨ Fun c [] ⊑ t"
using mgu_img_consts[OF assms(1)] assms(2)
by (metis Un_iff in_subterms_Union subst_imgI term.distinct(1)) 

lemma mgu_img_composed_var_term:
  fixes δ::"('f,'v) subst" and s t::"('f,'v) term" and f::'f and Z::"'v list"
  assumes "mgu s t = Some δ" "Fun f (map Var Z) ∈ subtermsset (subst_range δ)"
  shows "∃Z'. map δ Z' = map Var Z ∧ Fun f (map Var Z') ∈ subterms s ∪ subterms t"
proof -
  obtain u where u: "u ∈ (subterms s ∪ subterms t) - range Var" "u ⋅ δ = Fun f (map Var Z)"
    using mgu_img_subterm_subst[OF assms(1), of "Fun f (map Var Z)"] assms(2) by fastforce
  then obtain T where T: "u = Fun f T" "map (λt. t ⋅ δ) T = map Var Z" by (cases u) auto
  have "∀t ∈ set T. ∃x. t = Var x" using T(2) by (induct T arbitrary: Z) auto
  then obtain Z' where Z': "map Var Z' = T" by (metis ex_map_conv) 
  hence "map δ Z' = map Var Z" using T(2) by (induct Z' arbitrary: T Z) auto
  thus ?thesis using u(1) T(1) Z' by auto
qed

lemma mgu_ground_instance_case:
  assumes t: "fv (t ⋅ δ) = {}"
  shows "mgu t (t ⋅ δ) = Some (rm_vars (UNIV - fv t) δ)" (is ?A)
    and mgu_ground_commutes: "mgu t (t ⋅ δ) = mgu (t ⋅ δ) t" (is ?B)
proof -
  define θ where "θ ≡ rm_vars (UNIV - fv t) δ"

  have δ: "t ⋅ δ = t ⋅ θ"
    using rm_vars_subst_eq'[of t δ] unfolding θ_def by metis

  have 0: "Unifier θ t (t ⋅ δ)"
    using subst_ground_ident[OF t, of θ] term_subst_eq[of t δ θ]
    unfolding θ_def by (metis Diff_iff)

  obtain σ where σ: "mgu t (t ⋅ θ) = Some σ" "MGU σ t (t ⋅ θ)"
    using mgu_always_unifies[OF 0] mgu_gives_MGU[of t "t ⋅ θ"]
    unfolding δ by blast

  have 1: "subst_domain σ = fv t"
    using t MGU_is_Unifier[OF σ(2)]
          subset_antisym[OF mgu_subst_domain[OF σ(1)]]
          ground_term_subst_domain_fv_subset[of t σ]
          subst_apply_fv_empty[OF t, of σ]
    unfolding δ by auto

  have 2: "subst_domain θ = fv t"
    using 0 rm_vars_dom[of "UNIV - fv t" δ]
          ground_term_subst_domain_fv_subset[of t θ]
          subst_apply_fv_empty[OF t, of θ]
    unfolding θ_def by auto

  have "σ x = θ x" for x
    using 1 2 MGU_is_Unifier[OF σ(2)] term_subst_eq_conv[of t σ θ]
          subst_ground_ident[OF t[unfolded δ], of σ] subst_domI[of _ x]
    by metis
  hence "σ = θ" by presburger
  thus A: ?A using σ(1) unfolding δ θ_def by blast

  have "Unifier θ (t ⋅ δ) t" using 0 by simp
  then obtain σ' where σ': "mgu (t ⋅ θ) t = Some σ'" "MGU σ' (t ⋅ θ) t"
    using mgu_always_unifies mgu_gives_MGU[of "t ⋅ θ" t]
    unfolding δ by fastforce

  have 3: "subst_domain σ' = fv t"
    using t MGU_is_Unifier[OF σ'(2)]
          subset_antisym[OF mgu_subst_domain[OF σ'(1)]]
          ground_term_subst_domain_fv_subset[of t σ']
          subst_apply_fv_empty[OF t, of σ']
    unfolding δ by auto

  have "σ' x = θ x" for x
    using 2 3 MGU_is_Unifier[OF σ'(2)] term_subst_eq_conv[of t σ' θ]
          subst_ground_ident[OF t[unfolded δ], of σ'] subst_domI[of _ x]
    by metis
  hence "σ' = θ" by presburger
  thus ?B using A σ'(1) unfolding δ θ_def by argo
qed


subsection ‹Lemmata: The "Inequality Lemmata"›
text ‹Subterm injectivity (a stronger injectivity property)›
definition subterm_inj_on where
  "subterm_inj_on f A ≡ ∀x∈A. ∀y∈A. (∃v. v ⊑ f x ∧ v ⊑ f y) ⟶ x = y"

lemma subterm_inj_on_imp_inj_on: "subterm_inj_on f A ⟹ inj_on f A"
unfolding subterm_inj_on_def inj_on_def by fastforce

lemma subst_inj_on_is_bij_betw:
  "inj_on θ (subst_domain θ) = bij_betw θ (subst_domain θ) (subst_range θ)"
unfolding inj_on_def bij_betw_def by auto

lemma subterm_inj_on_alt_def:
    "subterm_inj_on f A ⟷
     (inj_on f A ∧ (∀s ∈ f`A. ∀u ∈ f`A. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u))"
    (is "?A ⟷ ?B")
unfolding subterm_inj_on_def inj_on_def by fastforce

lemma subterm_inj_on_alt_def':
    "subterm_inj_on θ (subst_domain θ) ⟷
     (inj_on θ (subst_domain θ) ∧
      (∀s ∈ subst_range θ. ∀u ∈ subst_range θ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u))"
    (is "?A ⟷ ?B")
by (metis subterm_inj_on_alt_def subst_range.simps)

lemma subterm_inj_on_subset:
  assumes "subterm_inj_on f A"
    and "B ⊆ A"
  shows "subterm_inj_on f B"
proof -
  have "inj_on f A" "∀s∈f ` A. ∀u∈f ` A. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
    using subterm_inj_on_alt_def[of f A] assms(1) by auto
  moreover have "f ` B ⊆ f ` A" using assms(2) by auto
  ultimately have "inj_on f B" "∀s∈f ` B. ∀u∈f ` B. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
    using inj_on_subset[of f A] assms(2) by blast+
  thus ?thesis by (metis subterm_inj_on_alt_def)
qed

lemma inj_subst_unif_consts:
  fixes ℐ θ σ::"('f,'v) subst" and s t::"('f,'v) term"
  assumes θ: "subterm_inj_on θ (subst_domain θ)" "∀x ∈ (fv s ∪ fv t) - X. ∃c. θ x = Fun c []"
             "subtermsset (subst_range θ) ∩ (subterms s ∪ subterms t) = {}" "ground (subst_range θ)"
             "subst_domain θ ∩ X = {}"
  and ℐ: "ground (subst_range ℐ)" "subst_domain ℐ = subst_domain θ"
  and unif: "Unifier σ (s ⋅ θ) (t ⋅ θ)"
  shows "∃δ. Unifier δ (s ⋅ ℐ) (t ⋅ ℐ)"
proof -
  let ?xs = "subst_domain θ"
  let ?ys = "(fv s ∪ fv t) - ?xs"

  have "∃δ::('f,'v) subst. s ⋅ δ = t ⋅ δ" by (metis subst_subst_compose unif)
  then obtain δ::"('f,'v) subst" where δ: "mgu s t = Some δ"
    using mgu_always_unifies by atomize_elim auto
  have 1: "∃σ::('f,'v) subst. s ⋅ θ ⋅ σ = t ⋅ θ ⋅ σ" by (metis unif)
  have 2: "⋀γ::('f,'v) subst. s ⋅ θ ⋅ γ = t ⋅ θ ⋅ γ ⟹ δ ≼∘ θ ∘s γ" using mgu_gives_MGU[OF δ] by simp
  have 3: "⋀(z::'v) (c::'f). δ z = Fun c [] ⟹ Fun c [] ⊑ s ∨ Fun c [] ⊑ t"
    by (rule mgu_img_consts'[OF δ])
  have 4: "subst_domain δ ∩ range_vars δ = {}"
    by (metis mgu_gives_wellformed_subst[OF δ] wfsubst_def)
  have 5: "subst_domain δ ∪ range_vars δ ⊆ fv s ∪ fv t"
    by (metis mgu_gives_wellformed_MGU[OF δ] wfMGU_def)

  { fix x and γ::"('f,'v) subst" assume "x ∈ subst_domain θ"
    hence "(θ ∘s γ) x = θ x"
      using θ(4) ident_comp_subst_trm_if_disj[of γ θ]
      unfolding range_vars_alt_def by fast
  }
  then obtain τ::"('f,'v) subst" where τ: "∀x ∈ subst_domain θ. θ x = (δ ∘s τ) x" using 1 2 by metis

  have *: "⋀x. x ∈ subst_domain δ ∩ subst_domain θ ⟹ ∃y ∈ ?ys. δ x = Var y"
  proof -
    fix x assume "x ∈ subst_domain δ ∩ ?xs"
    hence x: "x ∈ subst_domain δ" "x ∈ subst_domain θ" by auto
    then obtain c where c: "θ x = Fun c []" using θ(2,5) 5 by atomize_elim auto
    hence *: "(δ ∘s τ) x = Fun c []" using τ x by fastforce
    hence **: "x ∈ subst_domain (δ ∘s τ)" "Fun c [] ∈ subst_range (δ ∘s τ)"
      by (auto simp add: subst_domain_def)
    have "δ x = Fun c [] ∨ (∃z. δ x = Var z ∧ τ z = Fun c [])"
      by (rule subst_img_comp_subset_const'[OF *])
    moreover have "δ x ≠ Fun c []"
    proof (rule ccontr)
      assume "¬δ x ≠ Fun c []"
      hence "Fun c [] ⊑ s ∨ Fun c [] ⊑ t" using 3 by metis
      moreover have "∀u ∈ subst_range θ. u ∉ subterms s ∪ subterms t"
        using θ(3) by force
      hence "Fun c [] ∉ subterms s ∪ subterms t"
        by (metis c ‹ground (subst_range θ)›x(2) ground_subst_dom_iff_img) 
      ultimately show False by auto
    qed
    moreover have "∀x' ∈ subst_domain θ. δ x ≠ Var x'"
    proof (rule ccontr)
      assume "¬(∀x' ∈ subst_domain θ. δ x ≠ Var x')"
      then obtain x' where x': "x' ∈ subst_domain θ" "δ x = Var x'" by atomize_elim auto
      hence "τ x' = Fun c []" "(δ ∘s τ) x = Fun c []" using * unfolding subst_compose_def by auto
      moreover have "x ≠ x'"
        using x(1) x'(2) 4
        by (auto simp add: subst_domain_def)
      moreover have "x' ∉ subst_domain δ"
        using x'(2) mgu_eliminates_dom[OF δ]
        by (metis (no_types) subst_elim_def eval_term.simps(1) vars_iff_subterm_or_eq)
      moreover have "(δ ∘s τ) x = θ x" "(δ ∘s τ) x' = θ x'" using τ x(2) x'(1) by auto
      ultimately show False
        using subterm_inj_on_imp_inj_on[OF θ(1)] *
        by (simp add: inj_on_def subst_compose_def x'(2) subst_domain_def)
    qed
    ultimately show "∃y ∈ ?ys. δ x = Var y"
      by (metis 5 x(2) subtermeqI' vars_iff_subtermeq DiffI Un_iff subst_fv_imgI sup.orderE)
  qed

  have **: "inj_on δ (subst_domain δ ∩ ?xs)"
  proof (intro inj_onI)
    fix x y assume *:
      "x ∈ subst_domain δ ∩ subst_domain θ" "y ∈ subst_domain δ ∩ subst_domain θ" "δ x = δ y"
    hence "(δ ∘s τ) x = (δ ∘s τ) y" unfolding subst_compose_def by auto
    hence "θ x = θ y" using τ * by auto
    thus "x = y" using inj_onD[OF subterm_inj_on_imp_inj_on[OF θ(1)]] *(1,2) by simp
  qed

  define α where "α = (λy'. if Var y' ∈ δ ` (subst_domain δ ∩ ?xs)
                            then Var ((inv_into (subst_domain δ ∩ ?xs) δ) (Var y'))
                            else Var y'::('f,'v) term)"
  have a1: "Unifier (δ ∘s α) s t" using mgu_gives_MGU[OF δ] by auto

  define δ' where "δ' = δ ∘s α"
  have d1: "subst_domain δ' ⊆ ?ys"
  proof
    fix z assume z: "z ∈ subst_domain δ'"
    have "z ∈ ?xs ⟹ z ∉ subst_domain δ'"
    proof (cases "z ∈ subst_domain δ")
      case True
      moreover assume "z ∈ ?xs"
      ultimately have z_in: "z ∈ subst_domain δ ∩ ?xs" by simp
      then obtain y where y: "δ z = Var y" "y ∈ ?ys" using * by atomize_elim auto
      hence "α y = Var ((inv_into (subst_domain δ ∩ ?xs) δ) (Var y))"
        using α_def z_in by simp
      hence "α y = Var z" by (metis y(1) z_in ** inv_into_f_eq)
      hence "δ' z = Var z" using δ'_def y(1) subst_compose_def[of δ α] by simp
      thus ?thesis by (simp add: subst_domain_def)
    next
      case False
      hence "δ z = Var z" by (simp add: subst_domain_def)
      moreover assume "z ∈ ?xs"
      hence "α z = Var z" using α_def * by force
      ultimately show ?thesis
        using δ'_def subst_compose_def[of δ α]
        by (simp add: subst_domain_def)
    qed
    moreover have "subst_domain α ⊆ range_vars δ"
      unfolding δ'_def α_def range_vars_alt_def
      by (auto simp add: subst_domain_def)
    hence "subst_domain δ' ⊆ subst_domain δ ∪ range_vars δ"
      using subst_domain_compose[of δ α] unfolding δ'_def by blast
    ultimately show "z ∈ ?ys" using 5 z by auto
  qed
  have d2: "Unifier (δ' ∘s ℐ) s t" using a1 δ'_def by auto
  have d3: "ℐ ∘s δ' ∘s ℐ = δ' ∘s ℐ"
  proof -
    { fix z::'v assume z: "z ∈ ?xs"
      then obtain u where u: "ℐ z = u" "fv u = {}" using ℐ by auto
      hence "(ℐ ∘s δ' ∘s ℐ) z = u" by (simp add: subst_compose subst_ground_ident)
      moreover have "z ∉ subst_domain δ'" using d1 z by auto
      hence "δ' z = Var z" by (simp add: subst_domain_def)
      hence "(δ' ∘s ℐ) z = u" using u(1) by (simp add: subst_compose)
      ultimately have "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by metis
    } moreover {
      fix z::'v assume "z ∈ ?ys"
      hence "z ∉ subst_domain ℐ" using ℐ(2) by auto
      hence "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by (simp add: subst_compose subst_domain_def)
    } moreover {
      fix z::'v assume "z ∉ ?xs" "z ∉ ?ys"
      hence "ℐ z = Var z" "δ' z = Var z" using ℐ(2) d1 by blast+
      hence "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by (simp add: subst_compose)
    } ultimately show ?thesis by auto
  qed

  from d2 d3 have "Unifier (δ' ∘s ℐ) (s ⋅ ℐ) (t ⋅ ℐ)" by (metis subst_subst_compose) 
  thus ?thesis by metis
qed

lemma inj_subst_unif_comp_terms:
  fixes ℐ θ σ::"('f,'v) subst" and s t::"('f,'v) term"
  assumes θ: "subterm_inj_on θ (subst_domain θ)" "ground (subst_range θ)"
             "subtermsset (subst_range θ) ∩ (subterms s ∪ subterms t) = {}"
             "(fv s ∪ fv t) - subst_domain θ ⊆ X"
  and tfr: "∀f U. Fun f U ∈ subterms s ∪ subterms t ⟶ U = [] ∨ (∃u ∈ set U. u ∉ Var ` X)"
  and ℐ: "ground (subst_range ℐ)" "subst_domain ℐ = subst_domain θ"
  and unif: "Unifier σ (s ⋅ θ) (t ⋅ θ)"
  shows "∃δ. Unifier δ (s ⋅ ℐ) (t ⋅ ℐ)"
proof -
  let ?xs = "subst_domain θ"
  let ?ys = "(fv s ∪ fv t) - ?xs"

  have "ground (subst_range θ)" using θ(2) by auto

  have "∃δ::('f,'v) subst. s ⋅ δ = t ⋅ δ" by (metis subst_subst_compose unif)
  then obtain δ::"('f,'v) subst" where δ: "mgu s t = Some δ"
    using mgu_always_unifies by atomize_elim auto
  have 1: "∃σ::('f,'v) subst. s ⋅ θ ⋅ σ = t ⋅ θ ⋅ σ" by (metis unif)
  have 2: "⋀γ::('f,'v) subst. s ⋅ θ ⋅ γ = t ⋅ θ ⋅ γ ⟹ δ ≼∘ θ ∘s γ" using mgu_gives_MGU[OF δ] by simp
  have 3: "⋀(z::'v) (c::'f).  Fun c [] ⊑ δ z ⟹ Fun c [] ⊑ s ∨ Fun c [] ⊑ t"
    using mgu_img_consts[OF δ] by force
  have 4: "subst_domain δ ∩ range_vars δ = {}"
    using mgu_gives_wellformed_subst[OF δ]
    by (metis wfsubst_def)
  have 5: "subst_domain δ ∪ range_vars δ ⊆ fv s ∪ fv t"
    using mgu_gives_wellformed_MGU[OF δ]
    by (metis wfMGU_def)

  { fix x and γ::"('f,'v) subst" assume "x ∈ subst_domain θ"
    hence "(θ ∘s γ) x = θ x"
      using ‹ground (subst_range θ)› ident_comp_subst_trm_if_disj[of γ θ x]
      unfolding range_vars_alt_def by blast
  }
  then obtain τ::"('f,'v) subst" where τ: "∀x ∈ subst_domain θ. θ x = (δ ∘s τ) x" using 1 2 by metis

  have ***: "⋀x. x ∈ subst_domain δ ∩ subst_domain θ ⟹ fv (δ x) ⊆ ?ys"
  proof -
    fix x assume "x ∈ subst_domain δ ∩ ?xs"
    hence x: "x ∈ subst_domain δ" "x ∈ subst_domain θ" by auto
    moreover have "¬(∃x' ∈ ?xs. x' ∈ fv (δ x))"
    proof (rule ccontr)
      assume "¬¬(∃x' ∈ ?xs. x' ∈ fv (δ x))"
      then obtain x' where x': "x' ∈ fv (δ x)" "x' ∈ ?xs" by metis
      have "x ≠ x'" "x' ∉ subst_domain δ" "δ x' = Var x'"
        using 4 x(1) x'(1) unfolding range_vars_alt_def by auto
      hence "(δ ∘s τ) x' ⊑ (δ ∘s τ) x" "τ x' = (δ ∘s τ) x'"
        using τ x(2) x'(2)
        by (metis subst_compose subst_mono vars_iff_subtermeq x'(1),
            metis eval_term.simps(1) subst_compose_def)
      hence "θ x' ⊑ θ x" using τ x(2) x'(2) by auto
      thus False
        using θ(1) x'(2) x(2) ‹x ≠ x'›
        unfolding subterm_inj_on_def 
        by (meson subtermeqI') 
    qed
    ultimately show "fv (δ x) ⊆ ?ys"
      using 5 subst_dom_vars_in_subst[of x δ] subst_fv_imgI[of δ x]
      by blast
  qed

  have **: "inj_on δ (subst_domain δ ∩ ?xs)"
  proof (intro inj_onI)
    fix x y assume *:
      "x ∈ subst_domain δ ∩ subst_domain θ" "y ∈ subst_domain δ ∩ subst_domain θ" "δ x = δ y"
    hence "(δ ∘s τ) x = (δ ∘s τ) y" unfolding subst_compose_def by auto
    hence "θ x = θ y" using τ * by auto
    thus "x = y" using inj_onD[OF subterm_inj_on_imp_inj_on[OF θ(1)]] *(1,2) by simp
  qed

  have *: "⋀x. x ∈ subst_domain δ ∩ subst_domain θ ⟹ ∃y ∈ ?ys. δ x = Var y"
  proof (rule ccontr)
    fix xi assume xi_assms: "xi ∈ subst_domain δ ∩ subst_domain θ" "¬(∃y ∈ ?ys. δ xi = Var y)"
    hence xi_θ: "xi ∈ subst_domain θ" and δ_xi_comp: "¬(∃y. δ xi = Var y)"
      using ***[of xi] 5 by auto
    then obtain f T where f: "δ xi = Fun f T" by (cases "δ xi") auto

    have "∃g Y'. Y' ≠ [] ∧ Fun g (map Var Y') ⊑ δ xi ∧ set Y' ⊆ ?ys"
    proof -
      have "∀c. Fun c [] ⊑ δ xi ⟶ Fun c [] ⊑ θ xi"
        using τ xi_θ by (metis const_subterm_subst subst_compose)
      hence 1: "∀c. ¬(Fun c [] ⊑ δ xi)"
        using 3[of _ xi] xi_θ θ(3)
        by auto
      
      have "¬(∃x. δ xi = Var x)" using f by auto
      hence "∃g S. Fun g S ⊑ δ xi ∧ (∀s ∈ set S. (∃c. s = Fun c []) ∨ (∃x. s = Var x))"
        using nonvar_term_has_composed_shallow_term[of "δ xi"] by auto
      then obtain g S where gS: "Fun g S ⊑ δ xi" "∀s ∈ set S. (∃c. s = Fun c []) ∨ (∃x. s = Var x)"
        by atomize_elim auto

      have "∀s ∈ set S. ∃x. s = Var x"
        using 1 term.order_trans gS
        by (metis (no_types, lifting) UN_I term.order_refl subsetCE subterms.simps(2) sup_ge2)
      then obtain S' where 2: "map Var S' = S" by (metis ex_map_conv)

      have "S ≠ []" using 1 term.order_trans[OF _ gS(1)] by fastforce
      hence 3: "S' ≠ []" "Fun g (map Var S') ⊑ δ xi" using gS(1) 2 by auto

      have "set S' ⊆ fv (Fun g (map Var S'))" by simp
      hence 4: "set S' ⊆ fv (δ xi)" using 3(2) fv_subterms by force
      
      show ?thesis using ***[OF xi_assms(1)] 2 3 4 by auto
    qed
    then obtain g Y' where g: "Y' ≠ []" "Fun g (map Var Y') ⊑ δ xi" "set Y' ⊆ ?ys" by atomize_elim auto
    then obtain X where X: "map δ X = map Var Y'" "Fun g (map Var X) ∈ subterms s ∪ subterms t"
      using mgu_img_composed_var_term[OF δ, of g Y'] by force
    hence "∃(u::('f,'v) term) ∈ set (map Var X). u ∉ Var ` ?ys"
      using θ(4) tfr g(1) by fastforce
    then obtain j where j: "j < length X" "X ! j ∉ ?ys"
      by (metis image_iff[of _ Var "fv s ∪ fv t - subst_domain θ"] nth_map[of _ X Var]
                in_set_conv_nth[of _ "map Var X"] length_map[of Var X])

    define yj' where yj': "yj' ≡ Y' ! j"
    define xj where xj: "xj ≡ X ! j"

    have "xj ∈ fv s ∪ fv t"
      using j X(1) g(3) 5 xj yj'
      by (metis length_map nth_map term.simps(1) in_set_conv_nth le_supE subsetCE subst_domI) 
    hence xj_θ: "xj ∈ subst_domain θ" using j unfolding xj by simp

    have len: "length X = length Y'" by (rule map_eq_imp_length_eq[OF X(1)])
    
    have "Var yj' ⊑ δ xi"
      using term.order_trans[OF _ g(2)] j(1) len unfolding yj' by auto
    hence "τ yj' ⊑ θ xi"
      using τ xi_θ by (metis eval_term.simps(1) subst_compose_def subst_mono) 
    moreover have δ_xj_var: "Var yj' = δ xj"
      using X(1) len j(1) nth_map
      unfolding xj yj' by metis
    hence "τ yj' = θ xj" using τ xj_θ by (metis eval_term.simps(1) subst_compose_def) 
    moreover have "xi ≠ xj" using δ_xi_comp δ_xj_var by auto
    ultimately show False using θ(1) xi_θ xj_θ unfolding subterm_inj_on_def by blast
  qed

  define α where "α = (λy'. if Var y' ∈ δ ` (subst_domain δ ∩ ?xs)
                            then Var ((inv_into (subst_domain δ ∩ ?xs) δ) (Var y'))
                            else Var y'::('f,'v) term)"
  have a1: "Unifier (δ ∘s α) s t" using mgu_gives_MGU[OF δ] by auto

  define δ' where "δ' = δ ∘s α"
  have d1: "subst_domain δ' ⊆ ?ys"
  proof
    fix z assume z: "z ∈ subst_domain δ'"
    have "z ∈ ?xs ⟹ z ∉ subst_domain δ'"
    proof (cases "z ∈ subst_domain δ")
      case True
      moreover assume "z ∈ ?xs"
      ultimately have z_in: "z ∈ subst_domain δ ∩ ?xs" by simp
      then obtain y where y: "δ z = Var y" "y ∈ ?ys" using * by atomize_elim auto
      hence "α y = Var ((inv_into (subst_domain δ ∩ ?xs) δ) (Var y))"
        using α_def z_in by simp
      hence "α y = Var z" by (metis y(1) z_in ** inv_into_f_eq)
      hence "δ' z = Var z" using δ'_def y(1) subst_compose_def[of δ α] by simp
      thus ?thesis by (simp add: subst_domain_def)
    next
      case False
      hence "δ z = Var z" by (simp add: subst_domain_def)
      moreover assume "z ∈ ?xs"
      hence "α z = Var z" using α_def * by force
      ultimately show ?thesis using δ'_def subst_compose_def[of δ α] by (simp add: subst_domain_def)
    qed
    moreover have "subst_domain α ⊆ range_vars δ"
      unfolding δ'_def α_def range_vars_alt_def subst_domain_def
      by auto
    hence "subst_domain δ' ⊆ subst_domain δ ∪ range_vars δ"
      using subst_domain_compose[of δ α]
      unfolding δ'_def by blast
    ultimately show "z ∈ ?ys" using 5 z by blast
  qed
  have d2: "Unifier (δ' ∘s ℐ) s t" using a1 δ'_def by auto
  have d3: "ℐ ∘s δ' ∘s ℐ = δ' ∘s ℐ"
  proof -
    { fix z::'v assume z: "z ∈ ?xs"
      then obtain u where u: "ℐ z = u" "fv u = {}" using ℐ by auto
      hence "(ℐ ∘s δ' ∘s ℐ) z = u" by (simp add: subst_compose subst_ground_ident)
      moreover have "z ∉ subst_domain δ'" using d1 z by auto
      hence "δ' z = Var z" by (simp add: subst_domain_def)
      hence "(δ' ∘s ℐ) z = u" using u(1) by (simp add: subst_compose)
      ultimately have "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by metis
    } moreover {
      fix z::'v assume "z ∈ ?ys"
      hence "z ∉ subst_domain ℐ" using ℐ(2) by auto
      hence "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by (simp add: subst_compose subst_domain_def)
    } moreover {
      fix z::'v assume "z ∉ ?xs" "z ∉ ?ys"
      hence "ℐ z = Var z" "δ' z = Var z" using ℐ(2) d1 by blast+
      hence "(ℐ ∘s δ' ∘s ℐ) z = (δ' ∘s ℐ) z" by (simp add: subst_compose)
    } ultimately show ?thesis by auto
  qed

  from d2 d3 have "Unifier (δ' ∘s ℐ) (s ⋅ ℐ) (t ⋅ ℐ)" by (metis subst_subst_compose) 
  thus ?thesis by metis
qed

context
begin
private lemma sat_ineq_subterm_inj_subst_aux:
  fixes ℐ::"('f,'v) subst"
  assumes "Unifier σ (s ⋅ ℐ) (t ⋅ ℐ)" "ground (subst_range ℐ)"
          "(fv s ∪ fv t) - X ⊆ subst_domain ℐ" "subst_domain ℐ ∩ X = {}"
  shows "∃δ::('f,'v) subst. subst_domain δ = X ∧ ground (subst_range δ) ∧ s ⋅ δ ⋅ ℐ = t ⋅ δ ⋅ ℐ"
proof -
  have "∃σ. Unifier σ (s ⋅ ℐ) (t ⋅ ℐ) ∧ interpretationsubst σ"
  proof -
    obtain ℐ'::"('f,'v) subst" where *: "interpretationsubst ℐ'"
      using interpretation_subst_exists by metis
    hence "Unifier (σ ∘s ℐ') (s ⋅ ℐ) (t ⋅ ℐ)" using assms(1) by simp
    thus ?thesis using * interpretation_comp by blast
  qed
  then obtain σ' where σ': "Unifier σ' (s ⋅ ℐ) (t ⋅ ℐ)" "interpretationsubst σ'" by atomize_elim auto
  
  define σ'' where "σ'' = rm_vars (UNIV - X) σ'"
  
  have *: "fv (s ⋅ ℐ) ⊆ X" "fv (t ⋅ ℐ) ⊆ X"
    using assms(2,3) subst_fv_unfold_ground_img[of ℐ]
    unfolding range_vars_alt_def
    by (simp_all add: Diff_subset_conv Un_commute)
  hence **: "subst_domain σ'' = X" "ground (subst_range σ'')"
    using rm_vars_img_subset[of "UNIV - X" σ'] rm_vars_dom[of "UNIV - X" σ'] σ'(2)
    unfolding σ''_def by auto
  hence "⋀t. t ⋅ ℐ ⋅ σ'' = t ⋅ σ'' ⋅ ℐ"
    using subst_eq_if_disjoint_vars_ground[OF _ _ assms(2)] assms(4) by blast
  moreover have "Unifier σ'' (s ⋅ ℐ) (t ⋅ ℐ)"
    using Unifier_dom_restrict[OF σ'(1)] σ''_def * by blast
  ultimately show ?thesis using ** by auto
qed

text ‹
  The "inequality lemma": This lemma gives sufficient syntactic conditions for finding substitutions
  ‹θ› under which terms ‹s› and ‹t› are not unifiable.

  This is useful later when establishing the typing results since we there want to find well-typed
  solutions to inequality constraints / "negative checks" constraints, and this lemma gives
  conditions for protocols under which such constraints are well-typed satisfiable if satisfiable.
›
lemma sat_ineq_subterm_inj_subst:
  fixes θ ℐ δ::"('f,'v) subst"
  assumes θ: "subterm_inj_on θ (subst_domain θ)"
             "ground (subst_range θ)"
             "subst_domain θ ∩ X = {}"
             "subtermsset (subst_range θ) ∩ (subterms s ∪ subterms t) = {}"
             "(fv s ∪ fv t) - subst_domain θ ⊆ X"
  and tfr: "(∀x ∈ (fv s ∪ fv t) - X. ∃c. θ x = Fun c []) ∨
            (∀f U. Fun f U ∈ subterms s ∪ subterms t ⟶ U = [] ∨ (∃u ∈ set U. u ∉ Var ` X))"
  and ℐ: "∀δ::('f,'v) subst. subst_domain δ = X ∧ ground (subst_range δ) ⟶ s ⋅ δ ⋅ ℐ ≠ t ⋅ δ ⋅ ℐ"
         "(fv s ∪ fv t) - X ⊆ subst_domain ℐ" "subst_domain ℐ ∩ X = {}" "ground (subst_range ℐ)"
         "subst_domain ℐ = subst_domain θ"
  and δ: "subst_domain δ = X" "ground (subst_range δ)"
  shows "s ⋅ δ ⋅ θ ≠ t ⋅ δ ⋅ θ"
proof -
  have "∀σ. ¬Unifier σ (s ⋅ ℐ) (t ⋅ ℐ)"
    by (metis ℐ(1) sat_ineq_subterm_inj_subst_aux[OF _ ℐ(4,2,3)])
  hence "¬Unifier δ (s ⋅ θ) (t ⋅ θ)"
    using inj_subst_unif_consts[OF θ(1) _ θ(4,2,3) ℐ(4,5)]
          inj_subst_unif_comp_terms[OF θ(1,2,4,5) _ ℐ(4,5)]
          tfr
    by metis
  moreover have "subst_domain δ ∩ subst_domain θ = {}" using θ(2,3) δ(1) by auto
  ultimately show ?thesis using δ subst_eq_if_disjoint_vars_ground[OF _ θ(2) δ(2)] by metis
qed
end

lemma ineq_subterm_inj_cond_subst:
  assumes "X ∩ range_vars θ = {}"
  and "∀f T. Fun f T ∈ subtermsset S ⟶ T = [] ∨ (∃u ∈ set T. u ∉ Var`X)"
  shows "∀f T. Fun f T ∈ subtermsset (S ⋅set θ) ⟶ T = [] ∨ (∃u ∈ set T. u ∉ Var`X)"
proof (intro allI impI)
  let ?M = "λS. subtermsset S ⋅set θ"
  let ?N = "λS. subtermsset (θ ` (fvset S ∩ subst_domain θ))"

  fix f T assume "Fun f T ∈ subtermsset (S ⋅set θ)"
  hence 1: "Fun f T ∈ ?M S ∨ Fun f T ∈ ?N S"
    using subterms_subst[of _ θ] by auto

  have 2: "Fun f T ∈ subtermsset (subst_range θ) ⟹ ∀u ∈ set T. u ∉ Var`X"
    using fv_subset_subterms[of "Fun f T" "subst_range θ"] assms(1)
    unfolding range_vars_alt_def by force

  have 3: "∀x ∈ subst_domain θ. θ x ∉ Var`X"
  proof
    fix x assume "x ∈ subst_domain θ"
    hence "fv (θ x) ⊆ range_vars θ"
      using subst_dom_vars_in_subst subst_fv_imgI
      unfolding range_vars_alt_def by auto
    thus "θ x ∉ Var`X" using assms(1) by auto
  qed

  show "T = [] ∨ (∃s ∈ set T. s ∉ Var`X)" using 1
  proof
    assume "Fun f T ∈ ?M S"
    then obtain u where u: "u ∈ subtermsset S" "u ⋅ θ = Fun f T" by fastforce
    show ?thesis
    proof (cases u)
      case (Var x)
      hence "Fun f T ∈ subst_range θ" using u(2) by (simp add: subst_domain_def)
      hence "∀u ∈ set T. u ∉ Var`X" using 2 by force
      thus ?thesis by auto
    next
      case (Fun g S)
      hence "S = [] ∨ (∃u ∈ set S. u ∉ Var`X)" using assms(2) u(1) by metis
      thus ?thesis
      proof
        assume "S = []" thus ?thesis using u(2) Fun by simp
      next
        assume "∃u ∈ set S. u ∉ Var`X"
        then obtain u' where u': "u' ∈ set S" "u' ∉ Var`X" by atomize_elim auto
        hence "u' ⋅ θ ∈ set T" using u(2) Fun by auto
        thus ?thesis using u'(2) 3 by (cases u') force+
      qed
    qed
  next
    assume "Fun f T ∈ ?N S"
    thus ?thesis using 2 by force
  qed
qed


subsection ‹Lemmata: Sufficient Conditions for Term Matching›
definition subst_var_inv::"('a,'b) subst ⇒ 'b set ⇒ ('a,'b) subst" where
  "subst_var_inv δ X ≡ (λx. if Var x ∈ δ ` X then Var ((inv_into X δ) (Var x)) else Var x)"

lemma subst_var_inv_subst_domain:
  assumes "x ∈ subst_domain (subst_var_inv δ X)"
  shows "Var x ∈ δ ` X"
by (meson assms subst_dom_vars_in_subst subst_var_inv_def)

lemma subst_var_inv_subst_domain':
  assumes "X ⊆ subst_domain δ"
  shows "x ∈ subst_domain (subst_var_inv δ X) ⟷ Var x ∈ δ ` X"
proof
  show "Var x ∈ δ ` X ⟹ x ∈ subst_domain (subst_var_inv δ X)"
    by (metis (no_types, lifting) assms f_inv_into_f in_mono inv_into_into
          subst_domI subst_dom_vars_in_subst subst_var_inv_def term.inject(1))
qed (rule subst_var_inv_subst_domain)

lemma subst_var_inv_Var_range:
  "subst_range (subst_var_inv δ X) ⊆ range Var"
unfolding subst_var_inv_def by auto

text ‹Injective substitutions from variables to variables are invertible›
lemma inj_var_ran_subst_is_invertible:
  assumes δ_inj_on_X: "inj_on δ X"
    and δ_var_on_X: "δ ` X ⊆ range Var"
    and fv_t: "fv t ⊆ X"
  shows "t = t ⋅ δ ∘s subst_var_inv δ X"
proof -
  have "δ x ⋅ subst_var_inv δ X = Var x" when x: "x ∈ X" for x
  proof -
    obtain y where y: "δ x = Var y" using x δ_var_on_X fv_t by auto
    hence "Var y ∈ δ ` X" using x by simp
    thus ?thesis using y inv_into_f_eq[OF δ_inj_on_X x y] unfolding subst_var_inv_def by simp
  qed
  thus ?thesis using fv_t by (simp add: subst_compose_def trm_subst_ident'' subset_eq)
qed

lemma inj_var_ran_subst_is_invertible':
  assumes δ_inj_on_t: "inj_on δ (fv t)"
    and δ_var_on_t: "δ ` fv t ⊆ range Var"
  shows "t = t ⋅ δ ∘s subst_var_inv δ (fv t)"
using assms inj_var_ran_subst_is_invertible by fast

text ‹Sufficient conditions for matching unifiable terms›
lemma inj_var_ran_unifiable_has_subst_match:
  assumes "t ⋅ δ = s ⋅ δ" "inj_on δ (fv t)" "δ ` fv t ⊆ range Var"
  shows "t = s ⋅ δ ∘s subst_var_inv δ (fv t)"
using assms inj_var_ran_subst_is_invertible by fastforce

end