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 moura

  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 θ"
using subst_subst_compose[of _ δ θ] 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 ⋅ σ"
using subst_subst_compose[of t σ θ]
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_eqI[intro]: "(⋀t. t ⋅ σ = t ⋅ θ) ⟹ σ = θ"
proof -
  assume "⋀t. t ⋅ σ = t ⋅ θ"
  hence "⋀v. Var v ⋅ σ = Var v ⋅ θ" by auto
  thus "σ = θ" by auto
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 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 subst_apply_term.simps(1) term.set_intros(3))

lemma subst_elimD''[dest]: "subst_elim σ v ⟹ v ∉ fv (σ w)"
by (metis subst_elim_def subst_apply_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))"
unfolding subst_idem_def
proof
  let ?θ = "Var(v := t)"
  from assms have t_θ_id: "t ⋅ ?θ = t" by blast
  fix s show "s ⋅ (?θ ∘s ?θ) = s ⋅ ?θ"
    unfolding subst_compose_def
    by (induction s, metis t_θ_id fun_upd_def subst_apply_term.simps(1), simp) 
qed

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"
using subst_fv_unfold[of t s] unfolding range_vars_alt_def by auto

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

lemma trm_subst_ident[intro]: "fv t ∩ subst_domain θ = {} ⟹ t ⋅ θ = t"
proof -
  assume "fv t ∩ subst_domain θ = {}"
  hence "∀v ∈ fv t. ∀w ∈ subst_domain θ. v ≠ w" by auto
  thus ?thesis
    by (metis subst_agreement subst_apply_term.simps(1) subst_apply_term_empty subst_domI)
qed

lemma trm_subst_ident'[intro]: "v ∉ subst_domain θ ⟹ (Var v) ⋅ θ = Var v"
using trm_subst_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 trm_subst_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 auto
  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 using subst_compose by auto
  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"
using subst_apply_term.elims by blast

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 subst_apply_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) subterms_subst[of "θ1 x" θ2]
      unfolding subst_compose[of θ1 θ2 x] by auto
    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 moura
      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 subst_apply_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