Session Stateful_Protocol_Composition_and_Typing

Theory Miscellaneous

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

All Rights Reserved.

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

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

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

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

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

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

section ‹Miscellaneous Lemmata›
theory Miscellaneous
imports Main "HOL-Library.Sublist" "HOL-Library.While_Combinator"
begin

subsection ‹List: zip, filter, map›
lemma zip_arg_subterm_split:
  assumes "(x,y) ∈ set (zip xs ys)"
  obtains xs' xs'' ys' ys'' where "xs = xs'@x#xs''" "ys = ys'@y#ys''" "length xs' = length ys'"
proof -
  from assms have "∃zs zs' vs vs'. xs = zs@x#zs' ∧ ys = vs@y#vs' ∧ length zs = length vs"
  proof (induction ys arbitrary: xs)
    case (Cons y' ys' xs)
    then obtain x' xs' where x': "xs = x'#xs'"
      by (metis empty_iff list.exhaust list.set(1) set_zip_leftD)
    show ?case
      by (cases "(x, y) ∈ set (zip xs' ys')",
          metis ‹xs = x'#xs'› Cons.IH[of xs'] Cons_eq_appendI list.size(4),
          use Cons.prems x' in fastforce)
  qed simp
  thus ?thesis using that by blast
qed

lemma zip_arg_index:
  assumes "(x,y) ∈ set (zip xs ys)"
  obtains i where "xs ! i = x" "ys ! i = y" "i < length xs" "i < length ys"
proof -
  obtain xs1 xs2 ys1 ys2 where "xs = xs1@x#xs2" "ys = ys1@y#ys2" "length xs1 = length ys1"
    using zip_arg_subterm_split[OF assms] by moura
  thus ?thesis using nth_append_length[of xs1 x xs2] nth_append_length[of ys1 y ys2] that by simp
qed

lemma filter_nth: "i < length (filter P xs) ⟹ P (filter P xs ! i)"
using nth_mem by force

lemma list_all_filter_eq: "list_all P xs ⟹ filter P xs = xs"
by (metis list_all_iff filter_True)

lemma list_all_filter_nil:
  assumes "list_all P xs"
    and "⋀x. P x ⟹ ¬Q x"
  shows "filter Q xs = []"
using assms by (induct xs) simp_all

lemma list_all_concat: "list_all (list_all f) P ⟷ list_all f (concat P)"
by (induct P) auto

lemma map_upt_index_eq:
  assumes "j < length xs"
  shows "(map (λi. xs ! is i) [0..<length xs]) ! j = xs ! is j"
using assms by (simp add: map_nth)

lemma map_snd_list_insert_distrib:
  assumes "∀(i,p) ∈ insert x (set xs). ∀(i',p') ∈ insert x (set xs). p = p' ⟶ i = i'"
  shows "map snd (List.insert x xs) = List.insert (snd x) (map snd xs)"
using assms
proof (induction xs rule: List.rev_induct)
  case (snoc y xs)
  hence IH: "map snd (List.insert x xs) = List.insert (snd x) (map snd xs)" by fastforce

  obtain iy py where y: "y = (iy,py)" by (metis surj_pair)
  obtain ix px where x: "x = (ix,px)" by (metis surj_pair)

  have "(ix,px) ∈ insert x (set (y#xs))" "(iy,py) ∈ insert x (set (y#xs))" using y x by auto
  hence *: "iy = ix" when "py = px" using that snoc.prems by auto

  show ?case
  proof (cases "px = py")
    case True
    hence "y = x" using * y x by auto
    thus ?thesis using IH by simp
  next
    case False
    hence "y ≠ x" using y x by simp
    have "List.insert x (xs@[y]) = (List.insert x xs)@[y]"
    proof -
      have 1: "insert y (set xs) = set (xs@[y])" by simp
      have 2: "x ∉ insert y (set xs) ∨ x ∈ set xs" using ‹y ≠ x› by blast
      show ?thesis using 1 2 by (metis (no_types) List.insert_def append_Cons insertCI)
    qed
    thus ?thesis using IH y x False by (auto simp add: List.insert_def)
  qed
qed simp

lemma map_append_inv: "map f xs = ys@zs ⟹ ∃vs ws. xs = vs@ws ∧ map f vs = ys ∧ map f ws = zs"
proof (induction xs arbitrary: ys zs)
  case (Cons x xs')
  note prems = Cons.prems
  note IH = Cons.IH

  show ?case
  proof (cases ys)
    case (Cons y ys') 
    then obtain vs' ws where *: "xs' = vs'@ws" "map f vs' = ys'" "map f ws = zs"
      using prems IH[of ys' zs] by auto
    hence "x#xs' = (x#vs')@ws" "map f (x#vs') = y#ys'" using Cons prems by force+
    thus ?thesis by (metis Cons *(3))
  qed (use prems in simp)
qed simp


subsection ‹List: subsequences›
lemma subseqs_set_subset:
  assumes "ys ∈ set (subseqs xs)"
  shows "set ys ⊆ set xs"
using assms subseqs_powset[of xs] by auto

lemma subset_sublist_exists:
  "ys ⊆ set xs ⟹ ∃zs. set zs = ys ∧ zs ∈ set (subseqs xs)"
proof (induction xs arbitrary: ys)
  case Cons thus ?case by (metis (no_types, lifting) Pow_iff imageE subseqs_powset) 
qed simp

lemma map_subseqs: "map (map f) (subseqs xs) = subseqs (map f xs)"
proof (induct xs)
  case (Cons x xs)
  have "map (Cons (f x)) (map (map f) (subseqs xs)) = map (map f) (map (Cons x) (subseqs xs))"
    by (induct "subseqs xs") auto
  thus ?case by (simp add: Let_def Cons)
qed simp

lemma subseqs_Cons:
  assumes "ys ∈ set (subseqs xs)"
  shows "ys ∈ set (subseqs (x#xs))"
by (metis assms Un_iff set_append subseqs.simps(2))

lemma subseqs_subset:
  assumes "ys ∈ set (subseqs xs)"
  shows "set ys ⊆ set xs"
using assms by (metis Pow_iff image_eqI subseqs_powset)


subsection ‹List: prefixes, suffixes›
lemma suffix_Cons': "suffix [x] (y#ys) ⟹ suffix [x] ys ∨ (y = x ∧ ys = [])"
using suffix_Cons[of "[x]"] by auto

lemma prefix_Cons': "prefix (x#xs) (x#ys) ⟹ prefix xs ys"
by simp

lemma prefix_map: "prefix xs (map f ys) ⟹ ∃zs. prefix zs ys ∧ map f zs = xs"
using map_append_inv unfolding prefix_def by fast

lemma length_prefix_ex:
  assumes "n ≤ length xs"
  shows "∃ys zs. xs = ys@zs ∧ length ys = n"
  using assms
proof (induction n)
  case (Suc n)
  then obtain ys zs where IH: "xs = ys@zs" "length ys = n" by moura
  hence "length zs > 0" using Suc.prems(1) by auto
  then obtain v vs where v: "zs = v#vs" by (metis Suc_length_conv gr0_conv_Suc)
  hence "length (ys@[v]) = Suc n" using IH(2) by simp
  thus ?case using IH(1) v by (metis append.assoc append_Cons append_Nil)
qed simp

lemma length_prefix_ex':
  assumes "n < length xs"
  shows "∃ys zs. xs = ys@xs ! n#zs ∧ length ys = n"
proof -
  obtain ys zs where xs: "xs = ys@zs" "length ys = n" using assms length_prefix_ex[of n xs] by moura
  hence "length zs > 0" using assms by auto
  then obtain v vs where v: "zs = v#vs" by (metis Suc_length_conv gr0_conv_Suc)
  hence "(ys@zs) ! n = v" using xs by auto
  thus ?thesis using v xs by auto
qed

lemma length_prefix_ex2:
  assumes "i < length xs" "j < length xs" "i < j"
  shows "∃ys zs vs. xs = ys@xs ! i#zs@xs ! j#vs ∧ length ys = i ∧ length zs = j - i - 1"
by (smt assms length_prefix_ex' nth_append append.assoc append.simps(2) add_diff_cancel_left'
        diff_Suc_1 length_Cons length_append)


subsection ‹List: products›
lemma product_lists_Cons:
  "x#xs ∈ set (product_lists (y#ys)) ⟷ (xs ∈ set (product_lists ys) ∧ x ∈ set y)"
by auto

lemma product_lists_in_set_nth:
  assumes "xs ∈ set (product_lists ys)"
  shows "∀i<length ys. xs ! i ∈ set (ys ! i)"
proof -
  have 0: "length ys = length xs" using assms(1) by (simp add: in_set_product_lists_length)
  thus ?thesis using assms
  proof (induction ys arbitrary: xs)
    case (Cons y ys)
    obtain x xs' where xs: "xs = x#xs'" using Cons.prems(1) by (metis length_Suc_conv)
    hence "xs' ∈ set (product_lists ys) ⟹ ∀i<length ys. xs' ! i ∈ set (ys ! i)"
          "length ys = length xs'" "x#xs' ∈ set (product_lists (y#ys))"
      using Cons by simp_all
    thus ?case using xs product_lists_Cons[of x xs' y ys] by (simp add: nth_Cons')
  qed simp
qed

lemma product_lists_in_set_nth':
  assumes "∀i<length xs. ys ! i ∈ set (xs ! i)"
    and "length xs = length ys"
  shows "ys ∈ set (product_lists xs)"
using assms
proof (induction xs arbitrary: ys)
  case (Cons x xs)
  obtain y ys' where ys: "ys = y#ys'" using Cons.prems(2) by (metis length_Suc_conv)
  hence "ys' ∈ set (product_lists xs)" "y ∈ set x" "length xs = length ys'"
    using Cons by fastforce+
  thus ?case using ys product_lists_Cons[of y ys' x xs] by (simp add: nth_Cons')
qed simp


subsection ‹Other Lemmata›
lemma inv_set_fset: "finite M ⟹ set (inv set M) = M"
unfolding inv_def by (metis (mono_tags) finite_list someI_ex)

lemma lfp_eqI':
  assumes "mono f"
    and "f C = C"
    and "∀X ∈ Pow C. f X = X ⟶ X = C"
  shows "lfp f = C"
by (metis PowI assms lfp_lowerbound lfp_unfold subset_refl)

lemma lfp_while':
  fixes f::"'a set ⇒ 'a set" and M::"'a set"
  defines "N ≡ while (λA. f A ≠ A) f {}"
  assumes f_mono: "mono f"
    and N_finite: "finite N"
    and N_supset: "f N ⊆ N"
  shows "lfp f = N"
proof -
  have *: "f X ⊆ N" when "X ⊆ N" for X using N_supset monoD[OF f_mono that] by blast
  show ?thesis
    using lfp_while[OF f_mono * N_finite]
    by (simp add: N_def)
qed

lemma lfp_while'':
  fixes f::"'a set ⇒ 'a set" and M::"'a set"
  defines "N ≡ while (λA. f A ≠ A) f {}"
  assumes f_mono: "mono f"
    and lfp_finite: "finite (lfp f)"
  shows "lfp f = N"
proof -
  have *: "f X ⊆ lfp f" when "X ⊆ lfp f" for X
    using lfp_fixpoint[OF f_mono] monoD[OF f_mono that]
    by blast
  show ?thesis
    using lfp_while[OF f_mono * lfp_finite]
    by (simp add: N_def)
qed

lemma preordered_finite_set_has_maxima:
  assumes "finite A" "A ≠ {}"
  shows "∃a::'a::{preorder} ∈ A. ∀b ∈ A. ¬(a < b)"
using assms 
proof (induction A rule: finite_induct)
  case (insert a A) thus ?case
    by (cases "A = {}", simp, metis insert_iff order_trans less_le_not_le)
qed simp

lemma partition_index_bij:
  fixes n::nat
  obtains I k where
    "bij_betw I {0..<n} {0..<n}" "k ≤ n"
    "∀i. i < k ⟶ P (I i)"
    "∀i. k ≤ i ∧ i < n ⟶ ¬(P (I i))"
proof -
  define A where "A = filter P [0..<n]"
  define B where "B = filter (λi. ¬P i) [0..<n]"
  define k where "k = length A"
  define I where "I = (λn. (A@B) ! n)"

  note defs = A_def B_def k_def I_def
  
  have k1: "k ≤ n" by (metis defs(1,3) diff_le_self dual_order.trans length_filter_le length_upt)

  have "i < k ⟹ P (A ! i)" for i by (metis defs(1,3) filter_nth)
  hence k2: "i < k ⟹ P ((A@B) ! i)" for i by (simp add: defs nth_append) 

  have "i < length B ⟹ ¬(P (B ! i))" for i by (metis defs(2) filter_nth)
  hence "i < length B ⟹ ¬(P ((A@B) ! (k + i)))" for i using k_def by simp 
  hence "k ≤ i ∧ i < k + length B ⟹ ¬(P ((A@B) ! i))" for i
    by (metis add.commute add_less_imp_less_right le_add_diff_inverse2)
  hence k3: "k ≤ i ∧ i < n ⟹ ¬(P ((A@B) ! i))" for i by (simp add: defs sum_length_filter_compl)

  have *: "length (A@B) = n" "set (A@B) = {0..<n}" "distinct (A@B)"
    by (metis defs(1,2) diff_zero length_append length_upt sum_length_filter_compl)
       (auto simp add: defs)

  have I: "bij_betw I {0..<n} {0..<n}"
  proof (intro bij_betwI')
    fix x y show "x ∈ {0..<n} ⟹ y ∈ {0..<n} ⟹ (I x = I y) = (x = y)"
      by (metis *(1,3) defs(4) nth_eq_iff_index_eq atLeastLessThan_iff)
  next
    fix x show "x ∈ {0..<n} ⟹ I x ∈ {0..<n}"
      by (metis *(1,2) defs(4) atLeastLessThan_iff nth_mem)
  next
    fix y show "y ∈ {0..<n} ⟹ ∃x ∈ {0..<n}. y = I x"
      by (metis * defs(4) atLeast0LessThan distinct_Ex1 lessThan_iff)
  qed

  show ?thesis using k1 k2 k3 I that by (simp add: defs)
qed

lemma finite_lists_length_eq':
  assumes "⋀x. x ∈ set xs ⟹ finite {y. P x y}"
  shows "finite {ys. length xs = length ys ∧ (∀y ∈ set ys. ∃x ∈ set xs. P x y)}"
proof -
  define Q where "Q ≡ λys. ∀y ∈ set ys. ∃x ∈ set xs. P x y"
  define M where "M ≡ {y. ∃x ∈ set xs. P x y}"

  have 0: "finite M" using assms unfolding M_def by fastforce

  have "Q ys ⟷ set ys ⊆ M"
       "(Q ys ∧ length ys = length xs) ⟷ (length xs = length ys ∧ Q ys)"
    for ys
    unfolding Q_def M_def by auto
  thus ?thesis
    using finite_lists_length_eq[OF 0, of "length xs"]
    unfolding Q_def by presburger
qed

lemma trancl_eqI:
  assumes "∀(a,b) ∈ A. ∀(c,d) ∈ A. b = c ⟶ (a,d) ∈ A"
  shows "A = A+"
proof
  show "A+ ⊆ A"
  proof
    fix x assume x: "x ∈ A+"
    then obtain a b where ab: "x = (a,b)" by (metis surj_pair)
    hence "(a,b) ∈ A+" using x by metis
    hence "(a,b) ∈ A" using assms by (induct rule: trancl_induct) auto
    thus "x ∈ A" using ab by metis
  qed
qed auto

lemma trancl_eqI':
  assumes "∀(a,b) ∈ A. ∀(c,d) ∈ A. b = c ∧ a ≠ d ⟶ (a,d) ∈ A"
    and "∀(a,b) ∈ A. a ≠ b"
  shows "A = {(a,b) ∈ A+. a ≠ b}"
proof
  show "{(a,b) ∈ A+. a ≠ b} ⊆ A"
  proof
    fix x assume x: "x ∈ {(a,b) ∈ A+. a ≠ b}"
    then obtain a b where ab: "x = (a,b)" by (metis surj_pair)
    hence "(a,b) ∈ A+" "a ≠ b" using x by blast+
    hence "(a,b) ∈ A"
    proof (induction rule: trancl_induct)
      case base thus ?case by blast
    next
      case step thus ?case using assms(1) by force
    qed
    thus "x ∈ A" using ab by metis
  qed
qed (use assms(2) in auto)

lemma distinct_concat_idx_disjoint:
  assumes xs: "distinct (concat xs)"
    and ij: "i < length xs" "j < length xs" "i < j"
  shows "set (xs ! i) ∩ set (xs ! j) = {}"
proof -
  obtain ys zs vs where ys: "xs = ys@xs ! i#zs@xs ! j#vs" "length ys = i" "length zs = j - i - 1"
    using length_prefix_ex2[OF ij] by moura
  thus ?thesis
    using xs concat_append[of "ys@xs ! i#zs" "xs ! j#vs"]
          distinct_append[of "concat (ys@xs ! i#zs)" "concat (xs ! j#vs)"]
    by auto
qed

lemma remdups_ex2:
  "length (remdups xs) > 1 ⟹ ∃a ∈ set xs. ∃b ∈ set xs. a ≠ b"
by (metis distinct_Ex1 distinct_remdups less_trans nth_mem set_remdups zero_less_one zero_neq_one)

lemma trancl_minus_refl_idem:
  defines "cl ≡ λts. {(a,b) ∈ ts+. a ≠ b}"
  shows "cl (cl ts) = cl ts"
proof -
  have 0: "(ts+)+ = ts+" "cl ts ⊆ ts+" "(cl ts)+ ⊆ (ts+)+"
  proof -
    show "(ts+)+ = ts+" "cl ts ⊆ ts+" unfolding cl_def by auto
    thus "(cl ts)+ ⊆ (ts+)+" using trancl_mono[of _ "cl ts" "ts+"] by blast
  qed

  have 1: "t ∈ cl (cl ts)" when t: "t ∈ cl ts" for t
    using t 0 unfolding cl_def by fast

  have 2: "t ∈ cl ts" when t: "t ∈ cl (cl ts)" for t
  proof -
    obtain a b where ab: "t = (a,b)" by (metis surj_pair)
    have "t ∈ (cl ts)+" and a_neq_b: "a ≠ b" using t unfolding cl_def ab by force+
    hence "t ∈ ts+" using 0 by blast
    thus ?thesis using a_neq_b unfolding cl_def ab by blast
  qed

  show ?thesis using 1 2 by blast
qed


subsection ‹Infinite Paths in Relations as Mappings from Naturals to States›
context
begin

private fun rel_chain_fun::"nat ⇒ 'a ⇒ 'a ⇒ ('a × 'a) set ⇒ 'a" where
  "rel_chain_fun 0 x _ _ = x"
| "rel_chain_fun (Suc i) x y r = (if i = 0 then y else SOME z. (rel_chain_fun i x y r, z) ∈ r)"

lemma infinite_chain_intro:
  fixes r::"('a × 'a) set"
  assumes "∀(a,b) ∈ r. ∃c. (b,c) ∈ r" "r ≠ {}"
  shows "∃f. ∀i::nat. (f i, f (Suc i)) ∈ r"
proof -
  from assms(2) obtain a b where "(a,b) ∈ r" by auto

  let ?P = "λi. (rel_chain_fun i a b r, rel_chain_fun (Suc i) a b r) ∈ r"
  let ?Q = "λi. ∃z. (rel_chain_fun i a b r, z) ∈ r"

  have base: "?P 0" using ‹(a,b) ∈ r› by auto

  have step: "?P (Suc i)" when i: "?P i" for i
  proof -
    have "?Q (Suc i)" using assms(1) i by auto
    thus ?thesis using someI_ex[OF ‹?Q (Suc i)›] by auto
  qed

  have "∀i::nat. (rel_chain_fun i a b r, rel_chain_fun (Suc i) a b r) ∈ r"
    using base step nat_induct[of ?P] by simp
  thus ?thesis by fastforce
qed

end

lemma infinite_chain_intro':
  fixes r::"('a × 'a) set"
  assumes base: "∃b. (x,b) ∈ r" and step: "∀b. (x,b) ∈ r+ ⟶ (∃c. (b,c) ∈ r)" 
  shows "∃f. ∀i::nat. (f i, f (Suc i)) ∈ r"
proof -
  let ?s = "{(a,b) ∈ r. a = x ∨ (x,a) ∈ r+}"

  have "?s ≠ {}" using base by auto

  have "∃c. (b,c) ∈ ?s" when ab: "(a,b) ∈ ?s" for a b
  proof (cases "a = x")
    case False
    hence "(x,a) ∈ r+" using ab by auto
    hence "(x,b) ∈ r+" using ‹(a,b) ∈ ?s› by auto
    thus ?thesis using step by auto
  qed (use ab step in auto)
  hence "∃f. ∀i. (f i, f (Suc i)) ∈ ?s" using infinite_chain_intro[of ?s] ‹?s ≠ {}› by blast
  thus ?thesis by auto
qed

lemma infinite_chain_mono:
  assumes "S ⊆ T" "∃f. ∀i::nat. (f i, f (Suc i)) ∈ S"
  shows "∃f. ∀i::nat. (f i, f (Suc i)) ∈ T"
using assms by auto

end

Theory Messages

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

All Rights Reserved.

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

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

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

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

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

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

section ‹Protocol Messages as (First-Order) Terms›

theory Messages
  imports Miscellaneous "First_Order_Terms.Term"
begin

subsection ‹Term-related definitions: subterms and free variables›
abbreviation "the_Fun ≡ un_Fun1"
lemmas the_Fun_def = un_Fun1_def

fun subterms::"('a,'b) term ⇒ ('a,'b) terms" where
  "subterms (Var x) = {Var x}"
| "subterms (Fun f T) = {Fun f T} ∪ (⋃t ∈ set T. subterms t)"

abbreviation subtermeq (infix "⊑" 50) where "t' ⊑ t ≡ (t' ∈ subterms t)"
abbreviation subterm (infix "⊏" 50) where "t' ⊏ t ≡ (t' ⊑ t ∧ t' ≠ t)"

abbreviation "subtermsset M ≡ ⋃(subterms ` M)"
abbreviation subtermeqset (infix "⊑set" 50) where "t ⊑set M ≡ (t ∈ subtermsset M)"

abbreviation fv where "fv ≡ vars_term"
lemmas fv_simps = term.simps(17,18)

fun fvset where "fvset M = ⋃(fv ` M)"

abbreviation fvpair where "fvpair p ≡ case p of (t,t') ⇒ fv t ∪ fv t'"

fun fvpairs where "fvpairs F = ⋃(fvpair ` set F)"

abbreviation ground where "ground M ≡ fvset M = {}"


subsection ‹Variants that return lists insteads of sets›
fun fv_list where
  "fv_list (Var x) = [x]"
| "fv_list (Fun f T) = concat (map fv_list T)"

definition fv_listpairs where
  "fv_listpairs F ≡ concat (map (λ(t,t'). fv_list t@fv_list t') F)"

fun subterms_list::"('a,'b) term ⇒ ('a,'b) term list" where
  "subterms_list (Var x) = [Var x]"
| "subterms_list (Fun f T) = remdups (Fun f T#concat (map subterms_list T))"

lemma fv_list_is_fv: "fv t = set (fv_list t)"
by (induct t) auto

lemma fv_listpairs_is_fvpairs: "fvpairs F = set (fv_listpairs F)"
by (induct F) (auto simp add: fv_list_is_fv fv_listpairs_def)

lemma subterms_list_is_subterms: "subterms t = set (subterms_list t)"
by (induct t) auto


subsection ‹The subterm relation defined as a function›
fun subterm_of where
  "subterm_of t (Var y) = (t = Var y)"
| "subterm_of t (Fun f T) = (t = Fun f T ∨ list_ex (subterm_of t) T)"

lemma subterm_of_iff_subtermeq[code_unfold]: "t ⊑ t' = subterm_of t t'"
proof (induction t')
  case (Fun f T) thus ?case
  proof (cases "t = Fun f T")
    case False thus ?thesis
      using Fun.IH subterm_of.simps(2)[of t f T]
      unfolding list_ex_iff by fastforce
  qed simp
qed simp

lemma subterm_of_ex_set_iff_subtermeqset[code_unfold]: "t ⊑set M = (∃t' ∈ M. subterm_of t t')"
using subterm_of_iff_subtermeq by blast


subsection ‹The subterm relation is a partial order on terms›

interpretation "term": ordering "(⊑)" "(⊏)"
proof
  show "s ⊑ s" for s :: "('a,'b) term"
    by (induct s rule: subterms.induct) auto

  show trans: "s ⊑ t ⟹ t ⊑ u ⟹ s ⊑ u" for s t u :: "('a,'b) term"
    by (induct u rule: subterms.induct) auto

  show "s ⊑ t ⟹ t ⊑ s ⟹ s = t" for s t :: "('a,'b) term"
  proof (induction s arbitrary: t rule: subterms.induct[case_names Var Fun])
    case (Fun f T)
    { assume 0: "t ≠ Fun f T"
      then obtain u::"('a,'b) term" where u: "u ∈ set T" "t ⊑ u" using Fun.prems(2) by auto
      hence 1: "Fun f T ⊑ u" using trans[OF Fun.prems(1)] by simp
   
      have 2: "u ⊑ Fun f T"
        by (cases u) (use u(1) in force, use u(1) subterms.simps(2)[of f T] in fastforce)
      hence 3: "u = Fun f T" using Fun.IH[OF u(1) _ 1] by simp

      have "u ⊑ t" using trans[OF 2 Fun.prems(1)] by simp
      hence 4: "u = t" using Fun.IH[OF u(1) _ u(2)] by simp
  
      have "t = Fun f T" using 3 4 by simp
      hence False using 0 by simp
    }
    thus ?case by auto
  qed simp
  show ‹s ⊏ t ⟷ s ⊏ t› for s t :: "('a,'b) term" ..
qed

interpretation "term": order "(⊑)" "(⊏)"
  by (rule ordering_orderI) (fact term.ordering_axioms)

subsection ‹Lemmata concerning subterms and free variables›
lemma fv_listpairs_append: "fv_listpairs (F@G) = fv_listpairs F@fv_listpairs G"
by (simp add: fv_listpairs_def)

lemma distinct_fv_list_idx_fv_disjoint:
  assumes t: "distinct (fv_list t)" "Fun f T ⊑ t"
    and ij: "i < length T" "j < length T" "i < j"
  shows "fv (T ! i) ∩ fv (T ! j) = {}"
using t
proof (induction t rule: fv_list.induct)
  case (2 g S)
  have "distinct (fv_list s)" when s: "s ∈ set S" for s
    by (metis (no_types, lifting) s "2.prems"(1) concat_append distinct_append 
          map_append split_list fv_list.simps(2) concat.simps(2) list.simps(9))
  hence IH: "fv (T ! i) ∩ fv (T ! j) = {}"
    when s: "s ∈ set S" "Fun f T ⊑ s" for s
    using "2.IH" s by blast

  show ?case
  proof (cases "Fun f T = Fun g S")
    case True
    define U where "U ≡ map fv_list T"

    have a: "distinct (concat U)"
      using "2.prems"(1) True unfolding U_def by auto
    
    have b: "i < length U" "j < length U"
      using ij(1,2) unfolding U_def by simp_all

    show ?thesis
      using b distinct_concat_idx_disjoint[OF a b ij(3)]
            fv_list_is_fv[of "T ! i"] fv_list_is_fv[of "T ! j"]
      unfolding U_def by force
  qed (use IH "2.prems"(2) in auto)
qed force

lemmas subtermeqI'[intro] = term.eq_refl

lemma subtermeqI''[intro]: "t ∈ set T ⟹ t ⊑ Fun f T"
by force

lemma finite_fv_set[intro]: "finite M ⟹ finite (fvset M)"
by auto

lemma finite_fun_symbols[simp]: "finite (funs_term t)"
by (induct t) simp_all

lemma fv_set_mono: "M ⊆ N ⟹ fvset M ⊆ fvset N"
by auto

lemma subtermsset_mono: "M ⊆ N ⟹ subtermsset M ⊆ subtermsset N"
by auto

lemma ground_empty[simp]: "ground {}"
by simp

lemma ground_subset: "M ⊆ N ⟹ ground N ⟹ ground M"
by auto

lemma fv_map_fv_set: "⋃(set (map fv L)) = fvset (set L)"
by (induct L) auto

lemma fvset_union: "fvset (M ∪ N) = fvset M ∪ fvset N"
by auto

lemma finite_subset_Union:
  fixes A::"'a set" and f::"'a ⇒ 'b set"
  assumes "finite (⋃a ∈ A. f a)"
  shows "∃B. finite B ∧ B ⊆ A ∧ (⋃b ∈ B. f b) = (⋃a ∈ A. f a)"
by (metis assms eq_iff finite_subset_image finite_UnionD)

lemma inv_set_fv: "finite M ⟹ ⋃(set (map fv (inv set M))) = fvset M"
using fv_map_fv_set[of "inv set M"] inv_set_fset by auto

lemma ground_subterm: "fv t = {} ⟹ t' ⊑ t ⟹ fv t' = {}" by (induct t) auto

lemma empty_fv_not_var: "fv t = {} ⟹ t ≠ Var x" by auto

lemma empty_fv_exists_fun: "fv t = {} ⟹ ∃f X. t = Fun f X" by (cases t) auto

lemma vars_iff_subtermeq: "x ∈ fv t ⟷ Var x ⊑ t" by (induct t) auto

lemma vars_iff_subtermeq_set: "x ∈ fvset M ⟷ Var x ∈ subtermsset M"
using vars_iff_subtermeq[of x] by auto

lemma vars_if_subtermeq_set: "Var x ∈ subtermsset M ⟹ x ∈ fvset M"
by (metis vars_iff_subtermeq_set)

lemma subtermeq_set_if_vars: "x ∈ fvset M ⟹ Var x ∈ subtermsset M"
by (metis vars_iff_subtermeq_set)

lemma vars_iff_subterm_or_eq: "x ∈ fv t ⟷ Var x ⊏ t ∨ Var x = t"
by (induct t) (auto simp add: vars_iff_subtermeq)

lemma var_is_subterm: "x ∈ fv t ⟹ Var x ∈ subterms t"
by (simp add: vars_iff_subtermeq)

lemma subterm_is_var: "Var x ∈ subterms t ⟹ x ∈ fv t"
by (simp add: vars_iff_subtermeq)

lemma no_var_subterm: "¬t ⊏ Var v" by auto

lemma fun_if_subterm: "t ⊏ u ⟹ ∃f X. u = Fun f X" by (induct u) simp_all

lemma subtermeq_vars_subset: "M ⊑ N ⟹ fv M ⊆ fv N" by (induct N) auto

lemma fv_subterms[simp]: "fvset (subterms t) = fv t"
by (induct t) auto

lemma fv_subterms_set[simp]: "fvset (subtermsset M) = fvset M"
using subtermeq_vars_subset by auto

lemma fv_subset: "t ∈ M ⟹ fv t ⊆ fvset M"
by auto

lemma fv_subset_subterms: "t ∈ subtermsset M ⟹ fv t ⊆ fvset M"
using fv_subset fv_subterms_set by metis

lemma subterms_finite[simp]: "finite (subterms t)" by (induction rule: subterms.induct) auto

lemma subterms_union_finite: "finite M ⟹ finite (⋃t ∈ M. subterms t)"
by (induction rule: subterms.induct) auto

lemma subterms_subset: "t' ⊑ t ⟹ subterms t' ⊆ subterms t"
by (induction rule: subterms.induct) auto

lemma subterms_subset_set: "M ⊆ subterms t ⟹ subtermsset M ⊆ subterms t"
by (metis SUP_least contra_subsetD subterms_subset)

lemma subset_subterms_Union[simp]: "M ⊆ subtermsset M" by auto

lemma in_subterms_Union: "t ∈ M ⟹ t ∈ subtermsset M" using subset_subterms_Union by blast

lemma in_subterms_subset_Union: "t ∈ subtermsset M ⟹ subterms t ⊆ subtermsset M"
using subterms_subset by auto

lemma subterm_param_split: 
  assumes "t ⊏ Fun f X"
  shows "∃pre x suf. t ⊑ x ∧ X = pre@x#suf"
proof -
  obtain x where "t ⊑ x" "x ∈ set X" using assms by auto
  then obtain pre suf where "X = pre@x#suf" "x ∉ set pre ∨ x ∉ set suf"
    by (meson split_list_first split_list_last)
  thus ?thesis using ‹t ⊑ x› by auto
qed

lemma ground_iff_no_vars: "ground (M::('a,'b) terms) ⟷ (∀v. Var v ∉ (⋃m ∈ M. subterms m))"
proof
  assume "ground M"
  hence "∀v. ∀m ∈ M. v ∉ fv m" by auto
  hence "∀v. ∀m ∈ M. Var v ∉ subterms m" by (simp add: vars_iff_subtermeq)
  thus "(∀v. Var v ∉ (⋃m ∈ M. subterms m))" by simp
next
  assume no_vars: "∀v. Var v ∉ (⋃m ∈ M. subterms m)"
  moreover
  { assume "¬ground M"
    then obtain v and m::"('a,'b) term" where "m ∈ M" "fv m ≠ {}" "v ∈ fv m" by auto
    hence "Var v ∈ (subterms m)" by (simp add: vars_iff_subtermeq)
    hence "∃v. Var v ∈ (⋃t ∈ M. subterms t)" using ‹m ∈ M› by auto
    hence False using no_vars by simp
  }
  ultimately show "ground M" by blast
qed

lemma index_Fun_subterms_subset[simp]: "i < length T ⟹ subterms (T ! i) ⊆ subterms (Fun f T)"
by auto

lemma index_Fun_fv_subset[simp]: "i < length T ⟹ fv (T ! i) ⊆ fv (Fun f T)"
using subtermeq_vars_subset by fastforce

lemma subterms_union_ground:
  assumes "ground M"
  shows "ground (subtermsset M)"
proof -
  { fix t assume "t ∈ M"
    hence "fv t = {}"
      using ground_iff_no_vars[of M] assms
      by auto
    hence "∀t' ∈ subterms t. fv t' = {}" using subtermeq_vars_subset[of _ t] by simp
    hence "ground (subterms t)" by auto
  }
  thus ?thesis by auto
qed

lemma Var_subtermeq: "t ⊑ Var v ⟹ t = Var v" by simp

lemma subtermeq_imp_funs_term_subset: "s ⊑ t ⟹ funs_term s ⊆ funs_term t"
by (induct t arbitrary: s) auto

lemma subterms_const: "subterms (Fun f []) = {Fun f []}" by simp

lemma subterm_subtermeq_neq: "⟦t ⊏ u; u ⊑ v⟧ ⟹ t ≠ v"
by (metis term.eq_iff)

lemma subtermeq_subterm_neq: "⟦t ⊑ u; u ⊏ v⟧ ⟹ t ≠ v"
by (metis term.eq_iff)

lemma subterm_size_lt: "x ⊏ y ⟹ size x < size y"
using not_less_eq size_list_estimation by (induct y, simp, fastforce)

lemma in_subterms_eq: "⟦x ∈ subterms y; y ∈ subterms x⟧ ⟹ subterms x = subterms y"
using term.antisym by auto

lemma Fun_gt_params: "Fun f X ∉ (⋃x ∈ set X. subterms x)"
proof -
  have "size_list size X < size (Fun f X)" by simp
  hence "Fun f X ∉ set X" by (meson less_not_refl size_list_estimation) 
  hence "∀x ∈ set X. Fun f X ∉ subterms x ∨ x ∉ subterms (Fun f X)"
    by (metis term.antisym[of "Fun f X" _])
  moreover have "∀x ∈ set X. x ∈ subterms (Fun f X)" by fastforce
  ultimately show ?thesis by auto
qed

lemma params_subterms[simp]: "set X ⊆ subterms (Fun f X)" by auto

lemma params_subterms_Union[simp]: "subtermsset (set X) ⊆ subterms (Fun f X)" by auto

lemma Fun_subterm_inside_params: "t ⊏ Fun f X ⟷ t ∈ (⋃x ∈ (set X). subterms x)"
using Fun_gt_params by fastforce

lemma Fun_param_is_subterm: "x ∈ set X ⟹ x ⊏ Fun f X"
using Fun_subterm_inside_params by fastforce

lemma Fun_param_in_subterms: "x ∈ set X ⟹ x ∈ subterms (Fun f X)"
using Fun_subterm_inside_params by fastforce

lemma Fun_not_in_param: "x ∈ set X ⟹ ¬Fun f X ⊏ x"
using term.antisym by fast

lemma Fun_ex_if_subterm: "t ⊏ s ⟹ ∃f T. Fun f T ⊑ s ∧ t ∈ set T"
proof (induction s)
  case (Fun f T)
  then obtain s' where s': "s' ∈ set T" "t ⊑ s'" by auto
  show ?case
  proof (cases "t = s'")
    case True thus ?thesis using s' by blast
  next
    case False
    thus ?thesis
      using Fun.IH[OF s'(1)] s'(2) term.order_trans[OF _ Fun_param_in_subterms[OF s'(1), of f]]
      by metis
  qed
qed simp

lemma const_subterm_obtain:
  assumes "fv t = {}"
  obtains c where "Fun c [] ⊑ t"
using assms
proof (induction t)
  case (Fun f T) thus ?case by (cases "T = []") force+
qed simp

lemma const_subterm_obtain': "fv t = {} ⟹ ∃c. Fun c [] ⊑ t"
by (metis const_subterm_obtain)

lemma subterms_singleton:
  assumes "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
  shows "subterms t = {t}"
using assms by (cases t) auto

lemma subtermeq_Var_const:
  assumes "s ⊑ t"
  shows "t = Var v ⟹ s = Var v" "t = Fun f [] ⟹ s = Fun f []"
using assms by fastforce+

lemma subterms_singleton':
  assumes "subterms t = {t}"
  shows "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
proof (cases t)
  case (Fun f T)
  { fix s S assume "T = s#S"
    hence "s ∈ subterms t" using Fun by auto
    hence "s = t" using assms by auto
    hence False
      using Fun_param_is_subterm[of s "s#S" f] ‹T = s#S› Fun
      by auto
  }
  hence "T = []" by (cases T) auto
  thus ?thesis using Fun by simp
qed (simp add: assms)

lemma funs_term_subterms_eq[simp]:
  "(⋃s ∈ subterms t. funs_term s) = funs_term t" 
  "(⋃s ∈ subtermsset M. funs_term s) = ⋃(funs_term ` M)"
proof -
  show "⋀t. ⋃(funs_term ` subterms t) = funs_term t"
    using term.order_refl subtermeq_imp_funs_term_subset by blast
  thus "⋃(funs_term ` (subtermsset M)) = ⋃(funs_term ` M)" by force
qed

lemmas subtermI'[intro] = Fun_param_is_subterm

lemma funs_term_Fun_subterm: "f ∈ funs_term t ⟹ ∃T. Fun f T ∈ subterms t"
proof (induction t)
  case (Fun g T)
  hence "f = g ∨ (∃s ∈ set T. f ∈ funs_term s)" by simp
  thus ?case
  proof
    assume "∃s ∈ set T. f ∈ funs_term s"
    then obtain s where "s ∈ set T" "∃T. Fun f T ∈ subterms s" using Fun.IH by auto
    thus ?thesis by auto
  qed (auto simp add: Fun)
qed simp

lemma funs_term_Fun_subterm': "Fun f T ∈ subterms t ⟹ f ∈ funs_term t"
by (induct t) auto

lemma zip_arg_subterm:
  assumes "(s,t) ∈ set (zip X Y)"
  shows "s ⊏ Fun f X" "t ⊏ Fun g Y"
proof -
  from assms have *: "s ∈ set X" "t ∈ set Y" by (meson in_set_zipE)+
  show "s ⊏ Fun f X" by (metis Fun_param_is_subterm[OF *(1)])
  show "t ⊏ Fun g Y" by (metis Fun_param_is_subterm[OF *(2)])
qed

lemma fv_disj_Fun_subterm_param_cases:
  assumes "fv t ∩ X = {}" "Fun f T ∈ subterms t"
  shows "T = [] ∨ (∃s∈set T. s ∉ Var ` X)"
proof (cases T)
  case (Cons s S)
  hence "s ∈ subterms t"
    using assms(2) term.order_trans[of _ "Fun f T" t]
    by auto
  hence "fv s ∩ X = {}" using assms(1) fv_subterms by force
  thus ?thesis using Cons by auto
qed simp

lemma fv_eq_FunI:
  assumes "length T = length S" "⋀i. i < length T ⟹ fv (T ! i) = fv (S ! i)"
  shows "fv (Fun f T) = fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  thus ?case using Cons by fastforce
qed simp

lemma fv_eq_FunI':
  assumes "length T = length S" "⋀i. i < length T ⟹ x ∈ fv (T ! i) ⟷ x ∈ fv (S ! i)"
  shows "x ∈ fv (Fun f T) ⟷ x ∈ fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  thus ?case using Cons by fastforce
qed simp

lemma finite_fvpairs[simp]: "finite (fvpairs x)" by auto

lemma fvpairs_Nil[simp]: "fvpairs [] = {}" by simp

lemma fvpairs_singleton[simp]: "fvpairs [(t,s)] = fv t ∪ fv s" by simp

lemma fvpairs_Cons: "fvpairs ((s,t)#F) = fv s ∪ fv t ∪ fvpairs F" by simp

lemma fvpairs_append: "fvpairs (F@G) = fvpairs F ∪ fvpairs G" by simp

lemma fvpairs_mono: "set M ⊆ set N ⟹ fvpairs M ⊆ fvpairs N" by auto

lemma fvpairs_inI[intro]:
  "f ∈ set F ⟹ x ∈ fvpair f ⟹ x ∈ fvpairs F"
  "f ∈ set F ⟹ x ∈ fv (fst f) ⟹ x ∈ fvpairs F"
  "f ∈ set F ⟹ x ∈ fv (snd f) ⟹ x ∈ fvpairs F"
  "(t,s) ∈ set F ⟹ x ∈ fv t ⟹ x ∈ fvpairs F"
  "(t,s) ∈ set F ⟹ x ∈ fv s ⟹ x ∈ fvpairs F"
using UN_I by fastforce+

lemma fvpairs_cons_subset: "fvpairs F ⊆ fvpairs (f#F)"
by auto


subsection ‹Other lemmata›
lemma nonvar_term_has_composed_shallow_term:
  fixes t::"('f,'v) term"
  assumes "¬(∃x. t = Var x)"
  shows "∃f T. Fun f T ⊑ t ∧ (∀s ∈ set T. (∃c. s = Fun c []) ∨ (∃x. s = Var x))"
proof -
  let ?Q = "λS. ∀s ∈ set S. (∃c. s = Fun c []) ∨ (∃x. s = Var x)"
  let ?P = "λt. ∃g S. Fun g S ⊑ t ∧ ?Q S"
  { fix t::"('f,'v) term"
    have "(∃x. t = Var x) ∨ ?P t"
    proof (induction t)
      case (Fun h R) show ?case
      proof (cases "R = [] ∨ (∀r ∈ set R. ∃x. r = Var x)")
        case False
        then obtain r g S where "r ∈ set R" "?P r" "Fun g S ⊑ r" "?Q S" using Fun.IH by fast
        thus ?thesis by auto
      qed force
    qed simp
  } thus ?thesis using assms by blast
qed

end

Theory More_Unification

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

All Rights Reserved.

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

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

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

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

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

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

ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.

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

  All rights reserved.

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

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

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

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

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


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

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

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.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': "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


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_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_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, hide_lams) fv_in_subst_img Un_iff subst_compose_def 
                vt subsetCE subst_apply_term.simps(1) subst_sends_fv_to_img) 
  }
  thus "x ∈ ?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 (metis subst_apply_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 using subst_apply_fv_unfold[of t θ] by auto
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
  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 subst_apply_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 subst_apply_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[of f T t θ] assms
    by fastforce
qed


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 moura
  thus ?thesis by (cases "x ∈ subst_domain σ") auto
qed simp

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 moura
  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 δ"
    using subst_apply_fv_unfold[of _ δ] 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 moura
  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


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 intro!: UnifierD[of f X σ g Y])

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 θ" 
  proof
    fix s show "s ⋅ θ = s ⋅ ((Var(v := t)) ∘s θ)" using th by (induct s) auto
  qed
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