Theory Term_More

(*
Authors (in alph. order):  
  Guillaume Allais,
  Martin Avanzini
  Julian Nagele
  Christian Sternagel,  
  Thomas Sternagel
  René Thiemann
  Sarah Winkler
*)

section ‹More Results on Terms›

text ‹In this theory we introduce many more concepts of terms,
  we provide several results that link various notions, e.g., positions, 
  subterms, contexts, substitutions, etc.›

theory Term_More
  imports
    Position
    Subterm_and_Context
    Polynomial_Factorization.Missing_List
begin

text @{text "showl"}-Instance for Terms›

fun showsl_term' :: "('f  showsl)  ('v  showsl)  ('f, 'v) term  showsl"
where
  "showsl_term' fun var (Var x) = var x" |
  "showsl_term' fun var (Fun f ts) =
    fun f  showsl_list_gen id (STR '''') (STR ''('') (STR '', '') (STR '')'') (map (showsl_term' fun var) ts)"

abbreviation showsl_nat_var :: "nat  showsl"
  where
    "showsl_nat_var i  showsl_lit (STR ''x'')  showsl i"

abbreviation showsl_nat_term :: "('f::showl, nat) term  showsl"
  where
    "showsl_nat_term  showsl_term' showsl showsl_nat_var"

instantiation "term" :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)term) = showsl_term' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)term list) = default_showsl_list showsl xs"
instance ..
end


text @{class "showl"}-Instance for Contexts›

fun showsl_ctxt' :: "('f  showsl)  ('v  showsl)  ('f, 'v) ctxt  showsl" where
  "showsl_ctxt' fun var (Hole) = showsl_lit (STR ''[]'')"
| "showsl_ctxt' fun var (More f ss1 D ss2) = (
    fun f  showsl (STR ''('') 
    showsl_list_gen (showsl_term' fun var) (STR '''') (STR '''') (STR '', '') (STR '', '') ss1 
    showsl_ctxt' fun var D 
    showsl_list_gen (showsl_term' fun var) (STR '')'') (STR '', '') (STR '', '') (STR '')'') ss2
  )"

instantiation ctxt :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)ctxt) = showsl_ctxt' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)ctxt list) = default_showsl_list showsl xs"
instance ..
end


text ‹General Folds on Terms›

context
begin
qualified fun
  fold :: "('v  'a)  ('f  'a list  'a)  ('f, 'v) term  'a"
  where
    "fold var fun (Var x) = var x" |
    "fold var fun (Fun f ts) = fun f (map (fold var fun) ts)"
end

declare term.disc [intro]

abbreviation "num_args t  length (args t)"

definition funas_args_term :: "('f, 'v) term  'f sig"
  where
    "funas_args_term t = (set (map funas_term (args t)))"

fun eroot :: "('f, 'v) term  ('f × nat) + 'v"
  where
    "eroot (Fun f ts) = Inl (f, length ts)" |
    "eroot (Var x) = Inr x"

abbreviation "root_set  set_option  root"

lemma funas_term_conv:
  "funas_term t = set_option (root t)  funas_args_term t"
  by (cases t) (simp_all add: funas_args_term_def)

text ‹The \emph{depth} of a term is defined as follows:›
fun depth :: "('f, 'v) term  nat"
  where
    "depth (Var _) = 0" |
    "depth (Fun _ []) = 0" |
    "depth (Fun _ ts) = 1 + Max (set (map depth ts))"

declare conj_cong [fundef_cong]
text ‹The positions of a term›
fun poss :: "('f, 'v) term  pos set" where
  "poss (Var x) = {[]}" |
  "poss (Fun f ss) = {[]}  {i # p | i p. i < length ss  p  poss (ss ! i)}"
declare conj_cong [fundef_cong del]

lemma Cons_poss_Var [simp]:
  "i # p  poss (Var x)  False"
  by simp

lemma elem_size_size_list_size [termination_simp]:
  "x  set xs  size x < size_list size xs"
  by (induct xs) auto

text ‹The set of function positions of a term›
fun fun_poss :: "('f, 'v) term  pos set"
  where
    "fun_poss (Var x) = {}" |
    "fun_poss (Fun f ts) = {[]}  (i<length ts. {i # p | p. p  fun_poss (ts ! i)})"

lemma fun_poss_imp_poss:
  assumes "p  fun_poss t"
  shows "p  poss t"
  using assms by (induct t arbitrary: p) auto

lemma finite_fun_poss:
  "finite (fun_poss t)"
  by (induct t) auto

text ‹The set of variable positions of a term›
fun var_poss :: "('f, 'v) term  pos set"
  where
    "var_poss (Var x) = {[]}" |
    "var_poss (Fun f ts) = (i<length ts. {i # p | p. p  var_poss (ts ! i)})"

lemma var_poss_imp_poss:
  assumes "p  var_poss t"
  shows "p  poss t"
  using assms by (induct t arbitrary: p) auto

lemma finite_var_poss:
  "finite (var_poss t)"
  by (induct t) auto

lemma poss_simps [symmetric, simp]:
  "poss t = fun_poss t  var_poss t"
  "poss t = var_poss t  fun_poss t"
  "fun_poss t = poss t - var_poss t"
  "var_poss t = poss t - fun_poss t"
  by (induct_tac [!] t) auto

lemma finite_poss [simp]:
  "finite (poss t)"
  by (subst poss_simps [symmetric]) (metis finite_Un finite_fun_poss finite_var_poss)

text ‹The subterm of a term~@{text s} at position~@{text p} is defined as follows:›
fun subt_at :: "('f, 'v) term  pos  ('f, 'v) term" (infixl "|'_" 67)
  where
    "s |_ [] = s" |
    "Fun f ss |_ (i # p) = (ss ! i) |_ p"

lemma var_poss_iff:
  "p  var_poss t  (x. p  poss t  t |_ p = Var x)"
  by (induct t arbitrary: p) auto

lemma fun_poss_fun_conv:
  assumes "p  fun_poss t"
  shows " f ts. t |_ p = Fun f ts"
proof (cases "t |_ p")
  case (Var x)
  have p_in_t: "p  poss t" using fun_poss_imp_poss[OF assms].
  then have "p  poss t - fun_poss t" using Var(1) var_poss_iff by auto
  then show ?thesis using assms by blast
next
  case (Fun f ts) then show ?thesis by auto
qed

lemma pos_append_poss:
  "p  poss t  q  poss (t |_ p)  p @ q  poss t"
proof (induct t arbitrary: p q)
  case (Fun f ts p q)
  show ?case
  proof (cases p)
    case Nil then show ?thesis using Fun by auto
  next
    case (Cons i p')
    with Fun have i: "i < length ts" and p': "p'  poss (ts ! i)" by auto
    then have mem: "ts ! i  set ts" by auto
    from Fun(3) have "q  poss (ts ! i |_ p')" by (auto simp: Cons)
    from Fun(1) [OF mem p' this]
    show ?thesis by (auto simp: Cons i)
  qed
qed simp

text ‹Creating a context from a term by adding a hole at a specific position.›
fun
  ctxt_of_pos_term :: "pos  ('f, 'v) term  ('f, 'v) ctxt"
  where
    "ctxt_of_pos_term [] t = " |
    "ctxt_of_pos_term (i # ps) (Fun f ts) =
    More f (take i ts) (ctxt_of_pos_term ps (ts!i)) (drop (Suc i) ts)"

lemma ctxt_supt_id:
  assumes "p  poss t"
  shows "(ctxt_of_pos_term p t)t |_ p = t"
  using assms by (induct t arbitrary: p) (auto simp: id_take_nth_drop [symmetric])

text ‹
  Let @{text s} and @{text t} be terms. The following three statements are equivalent:
  \begin{enumerate}
   \item \label{A}@{text "s ⊵ t"}
   \item \label{B}@{text "∃p∈poss s. s|_p = t"}
   \item \label{C}@{text "∃C. s = C⟨t⟩"}
  \end{enumerate}
›

text ‹The position of the hole in a context is uniquely determined.›
fun
  hole_pos :: "('f, 'v) ctxt  pos"
  where
    "hole_pos  = []" |
    "hole_pos (More f ss D ts) = length ss # hole_pos D"

lemma hole_pos_ctxt_of_pos_term [simp]:
  assumes "p  poss t"
  shows "hole_pos (ctxt_of_pos_term p t) = p"
  using assms
proof (induct t arbitrary: p)
  case (Fun f ts)
  show ?case
  proof (cases p)
    case Nil
    then show ?thesis using Fun by auto
  next
    case (Cons i q)
    with Fun(2) have i: "i < length ts" and q: "q  poss (ts ! i)" by auto
    then have "ts ! i  set ts" by auto
    from Fun(1)[OF this q] Cons i show ?thesis by simp
  qed
qed simp

lemma hole_pos_id_ctxt:
  assumes "Cs = t"
  shows "ctxt_of_pos_term (hole_pos C) t = C"
  using assms
proof (induct C arbitrary: t)
  case (More f bef C aft)
  then show ?case
  proof (cases t)
    case (Fun g ts)
    with More have [simp]: "g = f" by simp
    from Fun More have bef: "take (length bef) ts = bef" by auto
    from Fun More have aft: "drop (Suc (length bef)) ts = aft" by auto
    from Fun More have Cs: "Cs = ts ! length bef" by auto
    from Fun More show ?thesis by (simp add: bef aft More(1)[OF Cs])
  qed simp
qed simp

lemma supteq_imp_subt_at:
  assumes "s  t" 
  shows "pposs s. s|_p = t"
  using assms proof (induct s t rule: supteq.induct)
  case (refl s)
  have "[]  poss s" by (induct s rule: term.induct) auto
  have "s|_[] = s" by simp
  from []  poss s and s|_[] = s show ?case by best
next
  case (subt u ss t f)
  then obtain p where "p  poss u" and "u|_p = t" by best
  from u  set ss obtain i
    where "i < length ss" and "u = ss!i" by (auto simp: in_set_conv_nth)
  from i < length ss and p  poss u
  have "i#p  poss (Fun f ss)" unfolding u = ss!i by simp
  have "Fun f ss|_ (i#p) = t"
    unfolding subt_at.simps unfolding u = ss!i[symmetric] by (rule u|_p = t)
  with i#p  poss (Fun f ss) show ?case by best
qed

lemma subt_at_imp_ctxt:
  assumes "p  poss s" 
  shows "C. Cs|_p = s"
  using assms proof (induct p arbitrary: s)
  case (Nil s)
  have "s|_[] = s" by simp
  then show ?case by best
next
  case (Cons i p s)
  then obtain f ss where "s = Fun f ss" by (cases s) auto
  with i#p  poss s obtain u :: "('a,'b) term"
    where "u = ss!i" and "p  poss u" and "i < length ss" by auto
  from Cons and pposs u obtain D where "Du|_p = u" by auto
  let ?ss1 = "take i ss" and ?ss2 = "drop (Suc i) ss"
  let ?E = "More f ?ss1 D ?ss2"
  have "?ss1@Du|_p#?ss2 = ss" (is "?ss = ss") unfolding Du|_p = u unfolding u = ss!i
    unfolding id_take_nth_drop[OF i < length ss, symmetric] ..
  have "s|_ (i#p) = u|_p" unfolding s = Fun f ss using u = ss!i by simp
  have "?Es|_(i#p) = s"
    unfolding ctxt_apply_term.simps s|_(i#p) = u|_p ?ss = ss unfolding s = Fun f ss ..
  then show ?case by best
qed

lemma subt_at_imp_supteq':
  assumes "p  poss s" and "s|_p = t" 
  shows "s  t"
proof -
  from p  poss s obtain C where "Cs|_p = s" using subt_at_imp_ctxt by best
  then show ?thesis unfolding s|_p = t using ctxt_imp_supteq by auto
qed

lemma subt_at_imp_supteq: "p  poss s  s  s|_p"
  by (simp add: subt_at_imp_supteq')

lemma fun_poss_ctxt_apply_term:
  assumes "p  fun_poss Cs"
  shows "(t. p  fun_poss Ct)  (q. p = (hole_pos C) @ q  q  fun_poss s)"
  using assms
proof (induct p arbitrary: C)
  case Nil then show ?case by (cases C) auto
next
  case (Cons i p)
  then show ?case
  proof (cases C)
    case (More f bef C' aft)
    with Cons(2) have "i < length (bef @ C's # aft)" by auto
    consider "i < length bef" | (C') "i = length bef" | "i > length bef"
      by (cases "i < length bef", auto, cases "i = length bef", auto)
    then show ?thesis
    proof (cases)
      case C'
      then have "p  fun_poss C's" using More Cons by auto
      from Cons(1)[OF this] More C' show ?thesis by auto
    qed (insert More Cons, auto simp: nth_append)
  qed auto
qed

text ‹Conversions between contexts and proper subterms.›

text ‹
By adding \emph{non-empty} to statements \ref{B} and \ref{C} a similar characterisation for
proper subterms is obtained:
\begin{enumerate}
 \item @{text "s ⊳ t"}
 \item @{text "∃i p. i#p∈poss s ∧ s|_(i#p) = t"}
 \item @{text "∃C. C ≠ □ ∧ s = C⟨t⟩"}
\end{enumerate}
›

lemma supt_imp_subt_at_nepos:
  assumes "s  t" shows "i p. i#p  poss s  s|_ (i#p) = t"
proof -
  from assms have "s  t" and "s  t" unfolding supt_supteq_conv by auto
  then obtain p where supteq: "p  poss s" "s|_p = t" using supteq_imp_subt_at by best
  have "p  []"
  proof
    assume "p = []" then have "s = t" using s|_p = t by simp
    then show False using s  t by simp
  qed
  then obtain i q where "p = i#q" by (cases p) simp
  with supteq show ?thesis by auto
qed


lemma arg_neq:
  assumes "i < length ss" and "ss!i = Fun f ss" shows "False"
proof -
  from i < length ss have "(ss!i)  set ss" by auto
  with assms show False by simp
qed

lemma subt_at_nepos_neq:
  assumes "i#p  poss s" shows "s|_(i#p)  s"
proof (cases s)
  fix x assume "s = Var x"
  then have "i#p  poss s" by simp
  with assms show ?thesis by simp
next
  fix f ss assume "s = Fun f ss" show ?thesis
  proof
    assume "s|_ (i#p) = s"
    from assms have "i < length ss" unfolding s = Fun f ss by auto
    then have "ss!i  set ss" by simp
    then have "Fun f ss  ss!i" by (rule supt.arg)
    then have "Fun f ss  ss!i" unfolding supt_supteq_conv by simp
    from s|_(i#p) = s and assms
    have "ss!i  Fun f ss" using subt_at_imp_supteq' unfolding s = Fun f ss by auto
    with supt_not_sym[OF Fun f ss  ss!i] have "ss!i = Fun f ss" by auto
    with i < length ss show False by (rule arg_neq)
  qed
qed

lemma subt_at_nepos_imp_supt:
  assumes "i#p  poss s" shows "s  s |_ (i#p)"
proof -
  from assms have "s  s|_(i#p)" by (rule subt_at_imp_supteq)
  from assms have "s|_(i#p)  s" by (rule subt_at_nepos_neq)
  from s  s|_(i#p) and s|_(i#p)  s show ?thesis by (auto simp: supt_supteq_conv)
qed

lemma subt_at_nepos_imp_nectxt:
  assumes "i#p  poss s" and "s|_(i#p) = t" shows "C. C    Ct = s"
proof -
  from assms obtain C where "Cs|_(i#p) = s" using subt_at_imp_ctxt by best
  from i#p  poss s
  have "t  s" unfolding s|_(i#p) = t[symmetric] using subt_at_nepos_neq by best
  from assms and Cs|_(i#p) = s have "Ct = s" by simp
  have "C  "
  proof
    assume "C = "
    with Ct = s have "t = s" by simp
    with t  s show False by simp
  qed
  with Ct = s show ?thesis by auto
qed

lemma supteq_subst_cases':
  "s  σ  t  ( u. s  u  is_Fun u  t = u  σ)  ( x. x  vars_term s  σ x  t)"
proof (induct s)
  case (Fun f ss)
  from Fun(2)
  show ?case
  proof (cases rule: supteq.cases)
    case refl
    show ?thesis
      by (intro disjI1 exI[of _ "Fun f ss"], auto simp: refl)
  next
    case (subt v ts g)
    then obtain si where si: "si  set ss" "si  σ  t" by auto
    from Fun(1)[OF this] si(1) show ?thesis by auto
  qed
qed simp

lemma size_const_subst[simp]: "size (t  (λ _ . Fun f [])) = size t"
proof (induct t)
  case (Fun f ts)
  then show ?case by (induct ts, auto)
qed simp

type_synonym ('f, 'v) terms = "('f, 'v) term set"

lemma supteq_subst_cases [consumes 1, case_names in_term in_subst]:
  "s  σ  t 
  ( u. s  u  is_Fun u  t = u  σ  P) 
  ( x. x  vars_term s  σ x  t  P) 
  P"
  using supteq_subst_cases' by blast

lemma poss_subst_apply_term:
  assumes "p  poss (t  σ)" and "p  fun_poss t"
  obtains q r x where "p = q @ r" and "q  poss t" and "t |_ q = Var x" and "r  poss (σ x)"
  using assms
proof (induct t arbitrary: p)
  case (Fun f ts)
  then show ?case by (auto) (metis append_Cons nth_mem subt_at.simps(2))
qed simp

lemma subt_at_subst [simp]:
  assumes "p  poss t" shows "(t  σ) |_ p = (t |_ p)  σ"
  using assms by (induct t arbitrary: p) auto

lemma vars_term_size:
  assumes "x  vars_term t"
  shows "size (σ x)  size (t  σ)"
  using assms
  by (induct t)
    (auto, metis (no_types) comp_apply le_SucI size_list_estimation')

text ‹Restrict a substitution to a set of variables.›

definition
  subst_restrict :: "('f, 'v) subst  'v set  ('f, 'v) subst"
  (infix "|s" 67)
  where
    "σ |s V = (λx. if x  V then σ(x) else Var x)"

lemma subst_restrict_Int [simp]:
  "(σ |s V ) |s W = σ |s (V  W)"
  by (rule ext) (simp add: subst_restrict_def)

lemma subst_domain_Var_conv [iff]:
  "subst_domain σ = {}  σ = Var"
proof
  assume "subst_domain σ = {}"
  show "σ = Var"
  proof (rule ext)
    fix x show "σ(x) = Var x"
    proof (rule ccontr)
      assume "σ(x)  Var x"
      then have "x  subst_domain σ" by (simp add: subst_domain_def)
      with subst_domain σ = {} show False by simp
    qed
  qed
next
  assume "σ = Var" then show "subst_domain σ = {}" by simp
qed

lemma subst_compose_Var[simp]: "σ s Var = σ" by (simp add: subst_compose_def)

lemma Var_subst_compose[simp]: "Var s σ = σ" by (simp add: subst_compose_def)

text ‹We use the same logical constant as for the power operations on
functions and relations, in order to share their syntax.›
overloading
  substpow  "compow :: nat  ('f, 'v) subst  ('f, 'v) subst"
begin

primrec substpow :: "nat  ('f, 'v) subst  ('f, 'v) subst" where
  "substpow 0 σ = Var"
| "substpow (Suc n) σ = σ s substpow n σ"

end

lemma subst_power_compose_distrib:
  "μ ^^ (m + n) = (μ ^^ m s μ ^^ n)" by (induct m) (simp_all add: ac_simps)

lemma subst_power_Suc: "μ ^^ (Suc i) = μ ^^ i s μ"
proof -
  have "μ ^^ (Suc i) = μ ^^ (i + Suc 0)" by simp
  then show ?thesis unfolding  subst_power_compose_distrib by simp
qed

lemma subst_pow_mult: "((σ :: ('f,'v)subst)^^ n) ^^ m = σ ^^ (n * m)"
  by (induct m arbitrary: n, auto simp: subst_power_compose_distrib)

lemma subst_domain_pow: "subst_domain (σ ^^ n)  subst_domain σ"
  unfolding subst_domain_def
  by (induct n, auto simp: subst_compose_def)

lemma subt_at_Cons_distr [simp]:
  assumes "i # p  poss t" and "p  []" (*avoid simplifier loop*)
  shows "t |_ (i # p) = (t |_ [i]) |_ p"
  using assms by (induct t) auto

lemma subt_at_append [simp]:
  "p  poss t  t |_ (p @ q) = (t |_ p) |_ q"
proof (induct t arbitrary: p)
  case (Fun f ts)
  show ?case
  proof (cases p)
    case (Cons i p')
    with Fun(2) have i: "i < length ts" and p': "p'  poss (ts ! i)" by auto
    from i have ti: "ts ! i  set ts" by auto
    show ?thesis using Fun(1)[OF ti p'] unfolding Cons by auto
  qed auto
qed auto

lemma subt_at_pos_diff:
  assumes "p <p q" and p: "p  poss s"
  shows "s |_ p |_ pos_diff q p = s |_ q"
  using assms unfolding subt_at_append [OF p, symmetric] by simp

lemma empty_pos_in_poss[simp]: "[]  poss t" by (induct t) auto

lemma poss_append_poss[simp]: "(p @ q  poss t) = (p  poss t  q  poss (t |_ p))" (is "?l = ?r")
proof
  assume ?r
  with pos_append_poss[of p t q] show ?l by auto
next
  assume ?l
  then show ?r
  proof (induct p arbitrary: t)
    case (Cons i p t)
    then obtain f ts where t: "t = Fun f ts" by (cases t, auto)
    note IH = Cons[unfolded t]
    from IH(2) have i: "i < length ts" and rec: "p @ q  poss (ts ! i)" by auto
    from IH(1)[OF rec] i show ?case unfolding t by auto
  qed auto
qed

lemma subterm_poss_conv:
  assumes "p  poss t" and [simp]: "p = q @ r" and "t |_ q = s"
  shows "t |_ p = s |_ r  r  poss s" (is "?A  ?B")
proof -
  have qr: "q @ r  poss t" using assms(1) by simp
  then have q_in_t: "q  poss t" using poss_append_poss by auto
  show ?thesis
  proof
    have "t |_ p = t |_ (q @ r)" by simp
    also have "... = s |_ r" using subt_at_append[OF q_in_t] assms(3) by simp
    finally show "?A" .
  next
    show "?B" using poss_append_poss qr assms(3) by auto
  qed
qed

lemma poss_imp_subst_poss [simp]:
  assumes "p  poss t"
  shows "p  poss (t  σ)"
  using assms by (induct t arbitrary: p) auto

lemma iterate_term:
  assumes id: "t  σ |_ p = t" and pos: "p  poss (t  σ)"
  shows "t  σ ^^ n |_ (p^n) = t  p ^ n  poss (t  σ ^^ n)"
proof (induct n)
  case (Suc n)
  then have p: "p ^ n  poss (t  σ ^^ n)" by simp
  note p' = poss_imp_subst_poss[OF p]
  note p'' = subt_at_append[OF p']
  have idt: "t  σ ^^ (Suc n) = t  σ^^ n  σ" unfolding subst_power_Suc by simp
  have "t  σ ^^ (Suc n) |_ (p ^ Suc n)
    = t  σ ^^ n  σ |_ (p ^ n @ p)" unfolding idt power_pos_Suc ..
  also have "... = ((t  σ ^^ n |_ p ^ n)  σ) |_ p" unfolding p'' subt_at_subst[OF p] ..
  also have "... = t  σ |_ p" unfolding Suc[THEN conjunct1] ..
  also have "... = t" unfolding id ..
  finally have one: "t  σ ^^ Suc n |_ (p ^ Suc n) = t" .
  show ?case
  proof (rule conjI[OF one])
    show "p ^ Suc n  poss (t  σ ^^ Suc n)"
      unfolding power_pos_Suc poss_append_poss idt
    proof (rule conjI[OF poss_imp_subst_poss[OF p]])
      have "t  σ ^^ n  σ |_ (p ^ n) = t  σ ^^ n |_ (p ^ n)  σ"
        by (rule subt_at_subst[OF p])
      also have "... = t  σ" using Suc by simp
      finally show "p  poss (t  σ ^^ n  σ |_ p ^ n)" using pos by auto
    qed
  qed
qed simp

lemma hole_pos_poss [simp]: "hole_pos C  poss (Ct)"
  by (induct C) auto

lemma hole_pos_poss_conv: "(hole_pos C @ q)  poss (Ct)  q  poss t"
  by (induct C) auto

lemma subt_at_hole_pos [simp]: "Ct |_ hole_pos C = t"
  by (induct C) auto

lemma hole_pos_power_poss [simp]: "(hole_pos C) ^ (n::nat)  poss ((C ^ n)t)"
  by (induct n) (auto simp: hole_pos_poss_conv)

lemma poss_imp_ctxt_subst_poss [simp]:
  assumes "p  poss (Ct)" 
  shows "p  poss ((C c σ)t  σ)"
proof -
  have "p  poss (Ct  σ)" by (rule poss_imp_subst_poss [OF assms])
  then show ?thesis by simp
qed

lemma poss_Cons_poss[simp]: "(i # p  poss t) = (i < length (args t)  p  poss (args t ! i))"
  by (cases t, auto)

lemma less_pos_imp_supt:
  assumes less: "p' <p p" and p: "p  poss t"
  shows "t |_ p  t |_ p'"
proof -
  from less obtain p'' where p'': "p = p' @ p''" unfolding less_pos_def less_eq_pos_def by auto
  with less have ne: "p''  []" by auto
  then obtain i q where ne: "p'' = i # q" by (cases p'', auto)
  from p have p': "p'  poss t" unfolding p'' by simp
  from p have "p''  poss (t |_ p')" unfolding p''  by simp
  from subt_at_nepos_imp_supt[OF this[unfolded ne]] have "t |_ p'  t |_ p' |_ p''" unfolding ne by simp
  then show "t |_ p'  t |_ p" unfolding p'' subt_at_append[OF p'] .
qed

lemma less_eq_pos_imp_supt_eq:
  assumes less_eq: "p' p p" and p: "p  poss t"
  shows "t |_ p  t |_ p'"
proof -
  from less_eq obtain p'' where p'': "p = p' @ p''" unfolding less_eq_pos_def by auto
  from p have p': "p'  poss t" unfolding p'' by simp
  from p have "p''  poss (t |_ p')" unfolding p'' by simp
  from subt_at_imp_supteq[OF this] have "t |_ p'  t |_ p' |_ p''" by simp
  then show "t |_ p'  t |_ p" unfolding p'' subt_at_append[OF p'] .
qed

lemma funas_term_poss_conv:
  "funas_term t = {(f, length ts) | p f ts. p  poss t  t|_p = Fun f ts}"
proof (induct t)
  case (Fun f ts)
  let ?f = "λ f ts. (f,length ts)"
  let ?fs = "λ t. {?f f ts | p f ts. p  poss t  t|_p = Fun f ts}"
  let ?l = "funas_term (Fun f ts)"
  let ?r = "?fs (Fun f ts)"
  {
    fix gn
    have "(gn  ?l) = (gn  ?r)"
    proof (cases "gn = (f,length ts)")
      case False
      obtain g n where gn: "gn = (g,n)" by force
      have "(gn  ?l) = ( t  set ts. gn  funas_term t)" using False by auto
      also have "... = ( i < length ts. gn  funas_term (ts ! i))" unfolding set_conv_nth by auto
      also have "... = ( i < length ts. (g,n)  ?fs (ts ! i))" using Fun[unfolded set_conv_nth] gn by blast
      also have "... = ((g,n)  ?fs (Fun f ts))" (is "?l' = ?r'")
      proof
        assume ?l'
        then obtain i p ss where p: "p  poss (ts ! i)" "ts ! i |_ p = Fun g ss" "n = length ss" "i < length ts" by auto
        show ?r'
          by (rule, rule exI[of _ "i # p"], intro exI conjI, unfold p(3), rule refl, insert p(1) p(2) p(4), auto)
      next
        assume ?r'
        then obtain p ss where p: "p  poss (Fun f ts)" "Fun f ts |_ p = Fun g ss" "n = length ss" by auto
        from p False gn obtain i p' where pp: "p = i # p'" by (cases p, auto)
        show ?l'
          by (rule exI[of _ i], insert p pp, auto)
      qed
      finally show ?thesis unfolding gn .
    qed force
  }
  then show ?case by blast
qed simp

inductive
  subst_instance :: "('f, 'v) term  ('f, 'v) term  bool" ("(_/  _)" [56, 56] 55)
  where
    subst_instanceI [intro]:
    "s  σ = t  s  t"

lemma subst_instance_trans[trans]:
  assumes "s  t" and "t  u" shows "s  u"
proof -
  from s  t obtain σ where "sσ = t" by (cases rule: subst_instance.cases) best
  from t  u obtain τ where "tτ = u" by (cases rule: subst_instance.cases) best
  then have "(sσ)τ = u" unfolding sσ = t .
  then have "s(σ s τ) = u" by simp
  then show ?thesis by (rule subst_instanceI)
qed

lemma subst_instance_refl: "s  s"
  using subst_instanceI[where σ = "Var" and s = s and t = s] by simp

lemma subst_neutral: "subst_domain σ  V  (Var x)(σ |s (V - {x})) = (Var x)"
  by (auto simp: subst_domain_def subst_restrict_def)

lemma subst_restrict_domain[simp]: "σ |s subst_domain σ = σ"
proof -
  have "σ |s subst_domain σ = (λx. if x  subst_domain σ then σ(x) else Var x)"
    by (simp add: subst_restrict_def)
  also have " = σ" by (rule ext) (simp add: subst_domain_def)
  finally show ?thesis .
qed

lemma notin_subst_domain_imp_Var:
  assumes "x  subst_domain σ" 
  shows "σ x = Var x"
  using assms by (auto simp: subst_domain_def)

lemma subst_domain_neutral[simp]:
  assumes "subst_domain σ  V" 
  shows "(σ |s V) = σ"
proof -
  {
    fix x
    have "(if x  V then σ(x) else Var x) = (if x  subst_domain σ then σ(x) else Var x)"
    proof (cases "x  subst_domain σ")
      case True
      then have x: "x  V = True" using assms by auto
      show ?thesis unfolding x using True by simp
    next
      case False
      then have x: "x  subst_domain (σ)" .
      show ?thesis unfolding notin_subst_domain_imp_Var[OF x] if_cancel ..
    qed
  }
  then have "x.(if x  V then σ x else Var x) = (if x  subst_domain σ then σ x else Var x)" .
  then have "x.(λx. if x  V then σ x else Var x) x = (λx. if x  subst_domain σ then σ x else Var x) x" .
  then have "x. (λx. if x  V then σ x else Var x) x = σ x" by (auto simp: subst_domain_def)
  then have "(λx. if x  V then σ x else Var x) = σ" by (rule ext)
  then have "σ |s V = σ" by (simp add: subst_restrict_def)
  then show ?thesis .
qed

lemma subst_restrict_UNIV[simp]: "σ |s UNIV = σ" by (auto simp: subst_restrict_def)

lemma subst_restrict_empty[simp]: "σ |s {} = Var" by (simp add: subst_restrict_def)

lemma vars_term_subst_pow:
  "vars_term (t  σ^^n)  vars_term t  (vars_term ` subst_range σ)" (is "_  ?R t")
  unfolding vars_term_subst
proof (induct n arbitrary: t)
  case (Suc n t)
  show ?case
  proof
    fix x
    assume "x  (vars_term ` (σ ^^ Suc n) ` vars_term t)"
    then obtain y u where 1: "y  vars_term t" "u = (σ ^^ Suc n) y" "x  vars_term u"
      by auto
    from 1(2) have "u = σ y  σ ^^ n" by (auto simp: subst_compose_def)
    from 1(3)[unfolded this, unfolded vars_term_subst]
    have "x  (vars_term ` (σ ^^ n) ` vars_term (σ y))" .
    with Suc[of "σ y"] have x: "x  ?R (σ y)" by auto
    then show "x  ?R t"
    proof
      assume "x  vars_term (σ y)"
      then show ?thesis using 1(1) by (cases "σ y = Var y", auto simp: subst_domain_def)
    qed auto
  qed
qed auto

lemma coincidence_lemma:
  "t  σ = t  (σ |s vars_term t)"
  unfolding term_subst_eq_conv subst_restrict_def by auto

lemma subst_domain_vars_term_subset:
  "subst_domain (σ  |s  vars_term t)  vars_term t"
  by (auto simp: subst_domain_def subst_restrict_def)

lemma subst_restrict_single_Var [simp]:
  assumes "x  subst_domain σ" shows "σ |s {x} = Var"
proof -
  have A: "x. x  subst_domain σ  σ x = Var x" by (simp add: subst_domain_def)
  have "σ |s {x} = (λy. if y  {x} then σ y else Var y)" by (simp add: subst_restrict_def)
  also have " = (λy. if y = x then σ y else Var y)" by simp
  also have " = (λy. if y = x then σ x else Var y)" by (simp cong: if_cong)
  also have " = (λy. if y = x then Var x else Var y)" unfolding A[OF assms] by simp
  also have " = (λy. if y = x then Var y else Var y)" by (simp cong: if_cong)
  also have " = (λy. Var y)" by simp
  finally show ?thesis by simp
qed

lemma subst_restrict_single_Var':
  assumes "x  subst_domain σ" and "σ |s V = Var" shows "σ |s ({x}  V) = Var"
proof -
  have "(λy. if y  V then σ y else Var y) = (λy. Var y)"
    using σ |s V = Var  by (simp add: subst_restrict_def)
  then have "(λy. if y  V then σ y else Var y) = (λy. Var y)" by simp
  then have A: "y. (if y  V then σ y else Var y) = Var y" by (rule fun_cong)
  {
    fix y
    have "(if y  {x}  V then σ y else Var y) = Var y"
    proof (cases "y = x")
      assume "y = x" then show ?thesis using x  subst_domain σ by (auto simp: subst_domain_def)
    next
      assume "y  x" then show ?thesis using A by simp
    qed
  }
  then have "y. (if y  {x}  V then σ y else Var y) = Var y" by simp
  then show ?thesis by (auto simp: subst_restrict_def)
qed

lemma subst_restrict_empty_set:
  "finite V  V  subst_domain σ = {}  σ |s V = Var"
proof (induct rule: finite.induct)
  case (insertI V x)
  then have "V  subst_domain σ = {}" by simp
  with insertI have "σ |s V = Var" by simp
  then show ?case using insertI subst_restrict_single_Var'[where σ = σ and x = x and V = V] by simp
qed auto

lemma subst_restrict_Var: "x  y  Var y  (σ |s (UNIV - {x})) = Var y  σ"
  by (auto simp: subst_restrict_def)

lemma var_cond_stable:
  assumes "vars_term r  vars_term l"
  shows "vars_term (r  μ)  vars_term (l  μ)"
  unfolding vars_term_subst using assms by blast

lemma instance_no_supt_imp_no_supt:
  assumes "¬ s  σ  t  σ"
  shows "¬ s  t"
proof 
  assume "s  t"
  hence "s  σ  t  σ" by (rule supt_subst)
  with assms show "False" by simp
qed

lemma subst_image_subterm:
  assumes "x  vars_term (Fun f ss)"
  shows "Fun f ss  σ  σ x"
proof -
  have "Fun f ss  Var x" using supteq_Var[OF assms(1)] .
  then have "Fun f ss  Var x" by cases auto
  from supt_subst [OF this]
  show ?thesis by simp
qed

lemma funas_term_subst_pow:
  "funas_term (t  σ^^n)  funas_term t  (funas_term ` subst_range σ)"
proof -
  {
    fix Xs
    have "(funas_term ` (σ ^^ n) ` Xs)  (funas_term ` subst_range σ)"
    proof (induct n arbitrary: Xs)
      case (Suc n Xs)
      show ?case (is " ?L  ?R")
      proof (rule subsetI)
        fix f
        assume "f   ?L"
        then obtain x where "f  funas_term ((σ ^^ Suc n) x)" by auto
        then have "f  funas_term (σ x  σ ^^ n)" by (auto simp: subst_compose_def)
        from this[unfolded funas_term_subst]
        show "f  ?R" using Suc[of "vars_term (σ x)"]
          unfolding subst_range.simps subst_domain_def by (cases "σ x = Var x", auto)
      qed
    qed auto
  }
  then show ?thesis unfolding funas_term_subst by auto
qed

lemma funas_term_subterm_args:
  assumes sF: "funas_term s  F"
    and q: "q  poss s"
  shows "(funas_term ` set (args (s |_ q)))  F"
proof -
  from subt_at_imp_ctxt[OF q] obtain C where s: "s = C  s |_ q " by metis
  from sF arg_cong[OF this, of "funas_term"] have "funas_term (s |_ q)  F" by auto
  then show ?thesis by (cases "s |_ q", auto)
qed

lemma get_var_or_const: " C t. s = Ct  args t = []"
proof (induct s)
  case (Var y)
  show ?case by (rule exI[of _ Hole], auto)
next
  case (Fun f ts)
  show ?case
  proof (cases ts)
    case Nil
    show ?thesis unfolding Nil
      by (rule exI[of _ Hole], auto)
  next
    case (Cons s ss)
    then have "s  set ts" by auto
    from Fun[OF this] obtain C where C: " t. s = Ct  args t = []" by auto
    show ?thesis unfolding Cons
      by (rule exI[of _ "More f [] C ss"], insert C, auto)
  qed
qed

lemma supteq_Var_id [simp]:
  assumes "Var x  s" shows "s = Var x"
  using assms by (cases)

lemma arg_not_term [simp]:
  assumes "t  set ts" shows "Fun f ts  t"
proof (rule ccontr)
  assume "¬ Fun f ts   t"
  then have "size (Fun f ts) = size t" by simp
  moreover have "size t < size_list size ts" using assms by (induct ts) auto
  ultimately show False by simp
qed

lemma arg_subteq [simp]: "t  set ts  Fun f ts  t"
  by auto

lemma supt_imp_args:
  assumes "t. s  t  P t" 
  shows "tset (args s). P t"
  using assms by (cases s) simp_all

lemma ctxt_apply_eq_False[simp]: "(More f ss1 D ss2)t  t" (is "?C_  _")
proof 
  assume eq: "?Ct = t" 
  have "?C  " by auto
  from ctxt_supt[OF this eq[symmetric]]
  have "t  t" .
  then show False by auto
qed

lemma supteq_imp_funs_term_subset: "t  s  funs_term s  funs_term t"
  by (induct rule:supteq.induct) auto

lemma funs_term_subst: "funs_term (t  σ) = funs_term t   ((λ x. funs_term (σ x)) ` (vars_term t))"
  by (induct t) auto

lemma set_set_cons:
  assumes "P x" and "y. y  set xs  P y"
  shows "y  set (x # xs)  P y"
  using assms by auto

lemma ctxt_power_compose_distr: "C ^ (m + n) = C ^ m c C ^ n"
  by (induct m) (simp_all add: ac_simps)

lemma subst_apply_id':
  assumes "vars_term t  V = {}" 
  shows "t  (σ |s V) = t"
  using assms
proof (induct t)
  case (Var x) then show ?case by (simp add: subst_restrict_def)
next
  case (Fun f ts)
  then have "sset ts. s  (σ |s V) = s" by auto
  with map_idI [of ts "λt. t  (σ |s V)"] show ?case by simp
qed

lemma subst_apply_ctxt_id:
  assumes "vars_ctxt C  V = {}" 
  shows "C c (σ |s V) = C"
  using assms
proof (induct C)
  case (More f ss1 D ss2)
  then have IH: "D c (σ |s V) = D" by auto
  from More have "sset(ss1@ss2). vars_term s  V = {}" by auto
  with subst_apply_id' have args: "sset(ss1@ss2). s(σ |s V) = s" by best
  from args have "sset ss1. s(σ |s V) = s" by simp
  with map_idI[of ss1 "λt. t(σ |s V)"] have ss1: "map (λs. s(σ |s V)) ss1 = ss1" by best
  from args have "sset ss2. s(σ |s V) = s" by simp
  with map_idI[of ss2 "λt. t(σ |s V)"] have ss2: "map (λs. s(σ |s V)) ss2 = ss2" by best
  show ?case by (simp add: ss1 ss2 IH)
qed simp

lemma vars_term_Var_id: "vars_term o Var = (λx. {x})"
  by (rule ext) simp

lemma ctxt_exhaust_rev[case_names Hole More]:
  assumes "C =   P" and 
    "D f ss1 ss2. C = D c (More f ss1  ss2)  P" 
  shows "P"
proof (cases C)
  case Hole with assms show ?thesis by simp
next
  case (More g ts1 E ts2)
  then have "D f ss1 ss2. C = D c (More f ss1  ss2)"
  proof (induct E arbitrary: C g ts1 ts2)
    case Hole then have "C =  c (More g ts1  ts2)" by simp
    then show ?case by best
  next
    case (More h us1 F us2)
    from More(1)[of "More h us1 F us2"]
    obtain G i vs1 vs2 where IH: "More h us1 F us2 = G c More i vs1  vs2" by force
    from More have "C = (More g ts1  ts2 c G) c More i vs1  vs2" unfolding IH by simp
    then show ?case by best
  qed
  then show ?thesis using assms by auto
qed

fun
  subst_extend :: "('f, 'v, 'w) gsubst  ('v × ('f, 'w) term) list  ('f, 'v, 'w) gsubst"
  where
    "subst_extend σ vts = (λx.
    (case map_of vts x of
      Some t  t
    | None    σ(x)))"

lemma subst_extend_id:
  assumes "V  set vs = {}" and "vars_term t  V"
  shows "t  subst_extend σ (zip vs ts) = t  σ"
  using assms
proof (induct t)
  case (Var x) then show ?case
    using map_of_SomeD[of "zip vs ts" x]
    using set_zip_leftD [of x _ vs ts]
    using IntI [of x V "set vs"]
    using emptyE
    by (case_tac "map_of (zip vs ts) x") auto
qed auto

lemma funas_term_args:
  "(funas_term ` set (args t))  funas_term t"
  by (cases t) auto

lemma subst_extend_absorb:
  assumes "distinct vs" and "length vs = length ss"
  shows "map (λt. t  subst_extend σ (zip vs ss)) (map Var vs) = ss" (is "?ss = _")
proof -
  let  = "subst_extend σ (zip vs ss)"
  from assms have "length vs  length ss" by simp
  from assms have "length ?ss = length ss" by simp
  moreover have "i<length ?ss. ?ss ! i = ss ! i"
  proof (intro allI impI)
    fix i assume "i < length ?ss"
    then have i: "i < length (map Var vs)" by simp
    then have len: "i < length vs" by simp
    have "?ss!i = (map Var vs ! i)  " unfolding nth_map[OF i, of "λt. t"] by simp
    also have " = Var(vs!i)" unfolding nth_map[OF len] by simp
    also have " = (case map_of (zip vs ss) (vs ! i) of None  σ (vs ! i) | Some t  t)" by simp
    also have " = ss ! i" using distinct vs length vs  length ss len 
      by (simp add: assms(2) map_of_zip_nth)
    finally show "?ss!i = ss!i" by simp
  qed
  ultimately show ?thesis by (metis nth_equalityI)
qed

abbreviation "map_funs_term f  term.map_term f (λx. x)"
abbreviation "map_funs_ctxt f  ctxt.map_ctxt f (λx. x)"

lemma funs_term_map_funs_term_id: "( f. f  funs_term t  h f = f)  map_funs_term h t = t"
proof (induct t)
  case (Fun f ts)
  then have " t. t  set ts  map_funs_term h t = t" by auto
  with Fun(2)[of f] show ?case
    by (auto intro: nth_equalityI)
qed simp

lemma funs_term_map_funs_term:
  "funs_term (map_funs_term h t)  range h"
  by (induct t) auto

fun map_funs_subst :: "('f  'g)  ('f, 'v) subst  ('g, 'v) subst" where
  "map_funs_subst fg σ = (λx. map_funs_term fg (σ x))"

lemma map_funs_term_comp:
  "map_funs_term fg (map_funs_term gh t) = map_funs_term (fg  gh) t"
  by (induct t) simp_all

lemma map_funs_subst_distrib [simp]:
  "map_funs_term fg (t  σ) = map_funs_term fg t  map_funs_subst fg σ"
  by (induct t) simp_all

lemma size_map_funs_term [simp]:
  "size (map_funs_term fg t) = size t"
proof (induct t)
  case (Fun f ts)
  then show ?case by (induct ts) auto
qed simp

lemma fold_ident [simp]: "Term_More.fold Var Fun t = t"
  by (induct t) (auto simp: map_ext [of _ "Term_More.fold Var Fun" id])

lemma map_funs_term_ident [simp]:
  "map_funs_term id t = t"
  by (induct t) (simp_all add: map_idI)

lemma ground_map_funs_term [simp]:
  "ground (map_funs_term fg t) = ground t"
  by (induct t) auto

lemma map_funs_term_power:
  fixes f :: "'f  'f"
  shows "((map_funs_term f) ^^ n) = map_funs_term (f ^^ n)"
proof (rule sym, intro ext)
  fix t :: "('f,'v)term"
  show "map_funs_term (f ^^ n) t = (map_funs_term f ^^ n) t"
  proof (induct n)
    case 0
    show ?case by (simp add: term.map_ident)
  next
    case (Suc n)
    show ?case by (simp add: Suc[symmetric] map_funs_term_comp o_def)
  qed
qed

lemma map_funs_term_ctxt_distrib [simp]:
  "map_funs_term fg (Ct) = (map_funs_ctxt fg C)map_funs_term fg t"
  by  (induct C) (auto)

text ‹mapping function symbols (w)ith (a)rities taken into account (wa)›

fun map_funs_term_wa :: "('f × nat  'g)  ('f, 'v) term  ('g, 'v) term"
  where
    "map_funs_term_wa fg (Var x) = Var x" |
    "map_funs_term_wa fg (Fun f ts) = Fun (fg (f, length ts)) (map (map_funs_term_wa fg) ts)"

lemma map_funs_term_map_funs_term_wa:
  "map_funs_term (fg :: ('f  'g)) = map_funs_term_wa (λ (f,n). (fg f))"
proof (intro ext)
  fix t :: "('f,'v)term"
  show "map_funs_term fg t = map_funs_term_wa (λ (f,n). fg f) t"
    by (induct t, auto)
qed

fun map_funs_ctxt_wa :: "('f × nat  'g)  ('f, 'v) ctxt  ('g, 'v) ctxt"
  where
    "map_funs_ctxt_wa fg  = " |
    "map_funs_ctxt_wa fg (More f bef C aft) =
    More (fg (f, Suc (length bef + length aft))) (map (map_funs_term_wa fg) bef) (map_funs_ctxt_wa fg C) (map (map_funs_term_wa fg) aft)"

abbreviation map_funs_subst_wa :: "('f × nat  'g)  ('f, 'v) subst  ('g, 'v) subst" where
  "map_funs_subst_wa fg σ  (λx. map_funs_term_wa fg (σ x))"

lemma map_funs_term_wa_subst [simp]:
  "map_funs_term_wa fg (t  σ) = map_funs_term_wa fg t  map_funs_subst_wa fg σ"
  by (induct t, auto)

lemma map_funs_term_wa_ctxt [simp]:
  "map_funs_term_wa fg (Ct) = (map_funs_ctxt_wa fg C) map_funs_term_wa fg t"
  by (induct C, auto)

lemma map_funs_term_wa_funas_term_id:
  assumes t: "funas_term t  F"
    and id: " f n. (f,n)  F  fg (f,n) = f"
  shows "map_funs_term_wa fg t = t"
  using t
proof (induct t)
  case (Fun f ss)
  then have IH: " s. s  set ss  map_funs_term_wa fg s = s" by auto
  from Fun(2) id have [simp]: "fg (f, length ss) = f" by simp
  show ?case by (simp, insert IH, induct ss, auto)
qed simp

lemma funas_term_map_funs_term_wa:
  "funas_term (map_funs_term_wa fg t) = (λ (f,n). (fg (f,n),n)) ` (funas_term t)"
  by (induct t) auto+

lemma notin_subst_restrict [simp]:
  assumes "x  V" shows "(σ  |s  V) x = Var x"
  using assms by (auto simp: subst_restrict_def)

lemma in_subst_restrict [simp]:
  assumes "x  V" shows "(σ  |s  V) x = σ x"
  using assms by (auto simp: subst_restrict_def)

lemma coincidence_lemma':
  assumes "vars_term t  V"
  shows "t  (σ |s V) = t  σ"
  using assms by (metis in_mono in_subst_restrict term_subst_eq)

lemma vars_term_map_funs_term [simp]:
  "vars_term  map_funs_term (f :: ('f  'g)) = vars_term"
proof
  fix t :: "('f,'v)term"
  show "(vars_term  map_funs_term f) t = vars_term t"
    by (induct t) (auto)
qed

lemma vars_term_map_funs_term2 [simp]:
  "vars_term (map_funs_term f t) = vars_term t"
  using fun_cong [OF vars_term_map_funs_term, of f t]
  by (simp del: vars_term_map_funs_term)

lemma map_funs_term_wa_ctxt_split:
  assumes "map_funs_term_wa fg s = lClt"
  shows " C t. s = Ct  map_funs_term_wa fg t = lt  map_funs_ctxt_wa fg C = lC"
  using assms
proof (induct lC arbitrary: s)
  case Hole
  show ?case
    by (rule exI[of _ Hole], insert Hole, auto)
next
  case (More lf lbef lC laft s)
  from More(2) obtain fs ss where s: "s = Fun fs ss" by (cases s, auto)
  note More = More[unfolded s, simplified]
  let ?lb = "length lbef"
  let ?la = "length laft"
  let ?n = "Suc (?lb + ?la)"
  let ?m = "map_funs_term_wa fg"
  from More(2) have rec: "map ?m ss = lbef @ lClt # laft"
    and lf: "lf = fg (fs,length ss)" by blast+
  from arg_cong[OF rec, of length] have len: "length ss = ?n" by auto
  then have lb: "?lb < length ss" by auto
  note ss = id_take_nth_drop[OF this]
  from rec ss have "map ?m (take ?lb ss @ ss ! ?lb # drop (Suc ?lb) ss) = lbef @ lClt # laft" by auto
  then have id: "take ?lb (map ?m ss) @ ?m (ss ! ?lb) # drop (Suc ?lb) (map ?m ss) = lbef @ lClt # laft"
    (is "?l1 @ ?l2 # ?l3 = ?r1 @ ?r2 # ?r3")
    unfolding take_map drop_map
    by auto
  from len have len2: " P. length ?l1 = length ?r1  P"
    unfolding length_take by auto
  from id[unfolded List.append_eq_append_conv[OF len2]]
  have id: "?l1 = ?r1" "?l2 = ?r2" "?l3 = ?r3" by auto
  from More(1)[OF id(2)] obtain C t where sb: "ss ! ?lb = Ct" and map: "map_funs_term_wa fg t = lt" and ma: "map_funs_ctxt_wa fg C = lC" by auto
  let ?C = "More fs (take ?lb ss) C (drop (Suc ?lb) ss)"
  have s: "s = ?Ct"
    unfolding s using ss[unfolded sb] by simp
  have len3: "Suc (length (take ?lb ss) + length (drop (Suc ?lb) ss)) = length ss"
    unfolding length_take length_drop len by auto
  show ?case
  proof (intro exI conjI, rule s, rule map)
    show "map_funs_ctxt_wa fg ?C = More lf lbef lC laft"
      unfolding map_funs_ctxt_wa.simps
      unfolding len3
      using id ma lf
      unfolding take_map drop_map
      by auto
  qed
qed

lemma subst_extend_flat_ctxt:
  assumes dist: "distinct vs"
    and len1: "length(take i (map Var vs)) = length ss1"
    and len2: "length(drop (Suc i) (map Var vs)) = length ss2"
    and i: "i < length vs"
  shows "More f (take i (map Var vs))  (drop (Suc i) (map Var vs)) c subst_extend σ (zip (take i vs@drop (Suc i) vs) (ss1@ss2)) = More f ss1  ss2"
proof -
  let ?V = "map Var vs"
  let ?vs1 = "take i vs" and ?vs2 = "drop (Suc i) vs"
  let ?ss1 = "take i ?V" and ?ss2 = "drop (Suc i) ?V"
  let  = "subst_extend σ (zip (?vs1@?vs2) (ss1@ss2))"
  from len1 and len2 have len: "length(?vs1@?vs2) = length(ss1@ss2)" using i by simp
  from dist i have "distinct(?vs1@?vs2)" 
    by (simp add: set_take_disj_set_drop_if_distinct)
  from subst_extend_absorb[OF this len,of "σ"]
  have map: "map (λt. t) (?ss1@?ss2) = ss1@ss2" unfolding take_map drop_map map_append .
  from len1 and map have "map (λt. t) ?ss1 = ss1" by auto
  moreover from len2 and map have "map (λt. t) ?ss2 = ss2" by auto
  ultimately show ?thesis by simp
qed

lemma subst_extend_flat_ctxt'':
  assumes dist: "distinct vs"
    and len1: "length(take i (map Var vs)) = length ss1"
    and len2: "length(drop i (map Var vs)) = length ss2"
    and i: "i < length vs"
  shows "More f (take i (map Var vs))  (drop i (map Var vs)) c subst_extend σ (zip (take i vs@drop i vs) (ss1@ss2)) = More f ss1  ss2"
proof -
  let ?V = "map Var vs"
  let ?vs1 = "take i vs" and ?vs2 = "drop i vs"
  let ?ss1 = "take i ?V" and ?ss2 = "drop i ?V"
  let  = "subst_extend σ (zip (?vs1@?vs2) (ss1@ss2))"
  from len1 and len2 have len: "length(?vs1@?vs2) = length(ss1@ss2)" using i by simp
  have "distinct(?vs1@?vs2)" using dist unfolding append_take_drop_id by simp
  from subst_extend_absorb[OF this len,of "σ"]
  have map: "map (λt. t) (?ss1@?ss2) = ss1@ss2" unfolding take_map drop_map map_append .
  from len1 and map have "map (λt. t) ?ss1 = ss1" unfolding map_append by auto
  moreover from len2 and map have "map (λt. t) ?ss2 = ss2" unfolding map_append by auto
  ultimately show ?thesis by simp
qed

lemma distinct_map_Var:
  assumes "distinct xs" shows "distinct (map Var xs)"
  using assms by (induct xs) auto

lemma variants_imp_is_Var:
  assumes "s  σ = t" and "t  τ = s"
  shows "xvars_term s. is_Var (σ x)"
  using assms
proof (induct s arbitrary: t)
  case (Var x)
  then show ?case by (cases "σ x") auto
next
  case (Fun f ts)
  then show ?case
    by (auto simp: o_def) (metis map_eq_conv map_ident)
qed

text ‹The range (in a functional sense) of a substitution.›
definition subst_fun_range :: "('f, 'v, 'w) gsubst  'w set"
  where
    "subst_fun_range σ = (vars_term ` range σ)"

lemma subst_variants_imp_is_Var:
  assumes "σ s σ' = τ" and "τ s τ' = σ"
  shows "xsubst_fun_range σ. is_Var (σ' x)"
  using assms by (auto simp: subst_compose_def subst_fun_range_def) (metis variants_imp_is_Var)

lemma variants_imp_image_vars_term_eq:
  assumes "s  σ = t" and "t  τ = s"
  shows "(the_Var  σ) ` vars_term s = vars_term t"
  using assms
proof (induct s arbitrary: t)
  case (Var x)
  then show ?case by (cases t) auto
next
  case (Fun f ss)
  then have IH: "t. i<length ss. (ss ! i)  σ = t  t  τ = ss ! i 
    (the_Var  σ) ` vars_term (ss ! i) = vars_term t"
    by (auto simp: o_def)
  from Fun.prems have t: "t = Fun f (map (λt. t  σ) ss)"
    and ss: "ss = map (λt. t  σ  τ) ss" by (auto simp: o_def)
  have "i<length ss. (the_Var  σ) ` vars_term (ss ! i) = vars_term (ss ! i  σ)"
  proof (intro allI impI)
    fix i
    assume *: "i < length ss"
    have "(ss ! i)  σ = (ss ! i)  σ" by simp
    moreover have "(ss ! i)  σ  τ = ss ! i"
      using * by (subst (2) ss) simp
    ultimately show "(the_Var  σ) ` vars_term (ss ! i) = vars_term ((ss ! i)  σ)"
      using IH and * by blast
  qed
  then have "sset ss. (the_Var  σ) ` vars_term s = vars_term (s  σ)" by (metis in_set_conv_nth)
  then show ?case by (simp add: o_def t image_UN)
qed

lemma terms_to_vars:
  assumes "tset ts. is_Var t"
  shows "(set (map vars_term ts)) = set (map the_Var ts)"
  using assms by (induct ts) auto

lemma Var_the_Var_id:
  assumes "tset ts. is_Var t"
  shows "map Var (map the_Var ts) = ts"
  using assms by (induct ts) auto

lemma distinct_the_vars:
  assumes "tset ts. is_Var t"
    and "distinct ts"
  shows "distinct (map the_Var ts)"
  using assms by (induct ts) auto

lemma map_funs_term_eq_imp_map_funs_term_map_vars_term_eq:
  "map_funs_term fg s = map_funs_term fg t  map_funs_term fg (map_vars_term vw s) = map_funs_term fg (map_vars_term vw t)"
proof (induct s arbitrary: t)
  case (Var x t)
  then show ?case by (cases t, auto)
next
  case (Fun f ss t)
  then obtain g ts where t: "t = Fun g ts" by (cases t, auto)
  from Fun(2)[unfolded t, simplified]
  have f: "fg f = fg g" and ss: "map (map_funs_term fg) ss = map (map_funs_term fg) ts" by auto
  from arg_cong[OF ss, of length] have "length ss = length ts" by simp
  from this ss Fun(1) have "map (map_funs_term fg  map_vars_term vw) ss = map (map_funs_term fg  map_vars_term vw) ts"
    by (induct ss ts rule: list_induct2, auto)
  then show ?case unfolding t by (simp add: f)
qed

lemma var_type_conversion:
  assumes inf: "infinite (UNIV :: 'v set)"
    and fin: "finite (T :: ('f, 'w) terms)"
  shows " (σ :: ('f, 'w, 'v) gsubst) τ. tT. t = t  σ  τ"
proof -
  obtain V where V: "V = (vars_term ` T)" by auto
  have fin: "finite V" unfolding V
    by (rule, rule, rule fin,
        insert finite_vars_term, auto)
  from finite_imp_inj_to_nat_seg[OF fin] obtain to_nat :: "'w  nat" and n :: nat
    where to_nat: "to_nat ` V = {i. i < n}" "inj_on to_nat V" by blast+
  from infinite_countable_subset[OF inf] obtain of_nat :: "nat  'v" where
    of_nat: "range of_nat  UNIV" "inj of_nat"  by auto
  let ?conv = "λ v. of_nat (to_nat v)"
  have inj: "inj_on ?conv V" using of_nat(2) to_nat(2) unfolding inj_on_def by auto
  let ?rev = "the_inv_into V ?conv"
  note rev = the_inv_into_f_eq[OF inj]
  obtain σ where σ: "σ = (λ v. Var (?conv v) :: ('f,'v)term)" by simp
  obtain τ where τ: "τ = (λ v. Var (?rev v) :: ('f,'w)term)" by simp
  show ?thesis
  proof (rule exI[of _ σ], rule exI[of _ τ], intro ballI)
    fix t
    assume t: "t  T"
    have "t  σ  τ = t  (σ s τ)" by simp
    also have "... = t  Var"
    proof (rule term_subst_eq)
      fix x
      assume "x  vars_term t"
      with t have x: "x  V" unfolding V by auto
      show "(σ s τ) x = Var x" unfolding σ τ subst_compose_def
          eval_term.simps term.simps
        by (rule rev[OF refl x])
    qed
    finally show "t = t  σ  τ" by simp
  qed
qed

text ‹combine two substitutions via sum-type›
fun
  merge_substs :: "('f, 'u, 'v) gsubst  ('f, 'w, 'v) gsubst  ('f, 'u + 'w, 'v) gsubst"
  where
    "merge_substs σ τ = (λx.
    (case x of
      Inl y  σ y
    | Inr y  τ y))"

lemma merge_substs_left:
  "map_vars_term Inl s  (merge_substs σ δ) = s  σ"
  by (induct s) auto

lemma merge_substs_right:
  "map_vars_term Inr s  (merge_substs σ δ) = s  δ"
  by (induct s) auto

fun map_vars_subst_ran :: "('w  'u)  ('f, 'v, 'w) gsubst  ('f, 'v, 'u) gsubst"
  where
    "map_vars_subst_ran m σ = (λv. map_vars_term m (σ v))"

lemma map_vars_subst_ran:
  shows "map_vars_term m (t  σ) = t  map_vars_subst_ran m σ"
  by (induct t) (auto)

lemma size_subst: "size t  size (t  σ)"
proof (induct t)
  case (Var x)
  then show ?case by (cases "σ x") auto
next
  case (Fun f ss)
  then show ?case
    by (simp add: o_def, induct ss, force+)
qed

lemma eq_ctxt_subst_iff [simp]:
  "(t = Ct  σ)  C =   (xvars_term t. σ x = Var x)" (is "?L = ?R")
proof
  assume t: "?L"
  then have "size t = size (Ct  σ)" by simp
  with size_ne_ctxt [of C "t  σ"] and size_subst [of t σ]
  have [simp]: "C = " by auto
  have "xvars_term t. σ x = Var x" using t and term_subst_eq_conv [of t Var] by simp
  then show ?R by auto
next
  assume ?R
  then show ?L using term_subst_eq_conv [of t Var] by simp
qed

lemma Fun_Nil_supt[elim!]: "Fun f []  t  P" by auto

lemma map_vars_term_vars_term:
  assumes " x. x  vars_term t  f x = g x"
  shows "map_vars_term f t = map_vars_term g t"
  using assms
proof (induct t)
  case (Fun h ts)
  {
    fix t
    assume t: "t  set ts"
    with Fun(2) have " x. x  vars_term t  f x = g x"
      by auto
    from Fun(1)[OF t this] have "map_vars_term f t = map_vars_term g t" by simp
  }
  then show ?case by auto
qed simp

lemma map_funs_term_ctxt_decomp:
  assumes "map_funs_term fg t = Cs"
  shows " D u. C = map_funs_ctxt fg D  s = map_funs_term fg u  t = Du"
  using assms
proof (induct C arbitrary: t)
  case Hole
  show ?case
    by (rule exI[of _ Hole], rule exI[of _ t], insert Hole, auto)
next
  case (More g bef C aft)
  from More(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
  from More(2)[unfolded t] have f: "fg f = g" and ts: "map (map_funs_term fg) ts = bef @ Cs # aft" (is "?ts = ?bca") by auto
  from ts have "length ?ts = length ?bca" by auto
  then have len: "length ts = length ?bca" by auto
  let ?i = "length bef"
  from len have i: "?i < length ts" by auto
  from arg_cong[OF ts, of "λ xs. xs ! ?i"] len 
  have "map_funs_term fg (ts ! ?i) = Cs" by auto
  from More(1)[OF this] obtain D u where D: "C = map_funs_ctxt fg D" and
    u: "s = map_funs_term fg u" and id: "ts ! ?i = Du" by auto
  from ts have "take ?i ?ts = take ?i ?bca" by simp
  also have "... = bef" by simp
  finally have bef: "map (map_funs_term fg) (take ?i ts) = bef" by (simp add: take_map)
  from ts have "drop (Suc ?i) ?ts = drop (Suc ?i) ?bca" by simp
  also have "... = aft" by simp
  finally have aft: "map (map_funs_term fg) (drop (Suc ?i) ts) = aft" by (simp add:drop_map)
  let ?bda = "take ?i ts @ Du # drop (Suc ?i) ts"
  show ?case
  proof (rule exI[of _ "More f (take ?i ts) D (drop (Suc ?i) ts)"],
      rule exI[of _ u], simp add: u f D bef aft t)
    have "ts = take ?i ts @ ts ! ?i # drop (Suc ?i) ts"
      by (rule id_take_nth_drop[OF i])
    also have "... = ?bda" by (simp add: id)
    finally show "ts = ?bda" .
  qed
qed

lemma funas_term_map_vars_term [simp]:
  "funas_term (map_vars_term τ t) = funas_term t"
  by (induct t) auto

lemma funs_term_funas_term:
  "funs_term t = fst ` (funas_term t)"
  by (induct t) auto

lemma funas_term_map_funs_term:
  "funas_term (map_funs_term fg t) = (λ (f,n). (fg f,n)) ` (funas_term t)"
  by (induct t) auto+

lemma supt_imp_arg_or_supt_of_arg:
  assumes "Fun f ss  t"
  shows "t  set ss  (s  set ss. s  t)"
  using assms by (rule supt.cases) auto

lemma supt_Fun_imp_arg_supteq:
  assumes "Fun f ss  t" shows "s  set ss. s  t"
  using assms by (cases rule: supt.cases) auto

lemma subt_iff_eq_or_subt_of_arg:
  assumes "s = Fun f ss"
  shows "{t. s  t} = ((u  set ss. {t. u  t}){s})"
  using assms proof (induct s)
  case (Var x) then show ?case by auto
next
  case (Fun g ts)
  then have "g = f" and "ts = ss" by auto
  show ?case
  proof
    show "{a. Fun g ts  a}  (uset ss. {a. u  a})  {Fun g ts}"
    proof
      fix x
      assume "x  {a. Fun g ts  a}"
      then have "Fun g ts  x" by simp
      then have "Fun g ts  x  Fun g ts = x" by auto
      then show "x  (uset ss. {a. u a})  {Fun g ts}"
      proof
        assume "Fun g ts  x"
        then obtain u where "u  set ts" and "u  x" using supt_Fun_imp_arg_supteq by best
        then have "x  {a. u  a}" by simp
        with u  set ts have "x  (uset ts. {a. u  a})" by auto
        then show ?thesis unfolding ts = ss by simp
      next
        assume "Fun g ts = x" then show ?thesis by simp
      qed
    qed
  next
    show "(uset ss. {a. u  a})  {Fun g ts}  {a. Fun g ts  a}"
    proof
      fix x
      assume "x  (uset ss. {a. u  a})  {Fun g ts}"
      then have "x  (uset ss. {a. u  a})  x = Fun g ts" by auto
      then show "x  {a. Fun g ts  a}"
      proof
        assume "x  (uset ss. {a. u  a})"
        then obtain u where "u  set ss" and "u  x" by auto
        then show ?thesis unfolding ts = ss by auto
      next
        assume "x = Fun g ts" then show ?thesis by auto
      qed
    qed
  qed
qed

text ‹The set of subterms of a term is finite.›
lemma finite_subterms: "finite {s. t  s}"
proof (induct t)
  case (Var x)
  then have "s. (Var x  s) = (Var x = s)" using supteq.cases by best
  then show ?case unfolding s. (Var x  s) = (Var x = s) by simp
next
  case (Fun f ss)
  have "Fun f ss = Fun f ss" by simp
  from Fun show ?case
    unfolding subt_iff_eq_or_subt_of_arg[OF Fun f ss = Fun f ss] by auto
qed

lemma Fun_supteq: "Fun f ts  u  Fun f ts = u  (tset ts. t  u)"
  using subt_iff_eq_or_subt_of_arg[of "Fun f ts" f ts] by auto

lemma subst_ctxt_distr: "s = Ctσ  D. s = Dtσ"
  using subst_apply_term_ctxt_apply_distrib by auto

lemma ctxt_of_pos_term_subst:
  assumes "p  poss t"
  shows "ctxt_of_pos_term p (t  σ) = ctxt_of_pos_term p t c σ"
  using assms
proof (induct p arbitrary: t)
  case (Cons i p t)
  then obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p  poss (ts ! i)" by (cases t, auto)
  note id = id_take_nth_drop[OF i, symmetric]
  with t have t: "t = Fun f (take i ts @ ts ! i # drop (Suc i) ts)" by auto
  from i have i': "min (length ts) i = i" by simp
  show ?case unfolding t using Cons(1)[OF p, symmetric] i'
    by (simp add: id, insert i, auto simp: take_map drop_map)
qed simp

lemma subt_at_ctxt_of_pos_term:
  assumes t: "(ctxt_of_pos_term p t)u = t" and p: "p  poss t"
  shows "t |_ p = u"
proof -
  let ?C = "ctxt_of_pos_term p t"
  from t and ctxt_supt_id [OF p] have "?Cu = ?Ct |_ p" by simp
  then show ?thesis by simp
qed

lemma subst_ext:
  assumes "xV. σ x = τ x" shows "σ |s V = τ |s V"
proof
  fix x show "(σ |s V) x = (τ |s V) x" using assms
    unfolding subst_restrict_def by (cases "x  V") auto
qed

abbreviation "map_vars_ctxt f  ctxt.map_ctxt (λx. x) f"

lemma map_vars_term_ctxt_commute:
  "map_vars_term m (ct) = (map_vars_ctxt m c)map_vars_term m t"
  by (induct c) auto

lemma map_vars_term_inj_compose:
  assumes inj: " x. n (m x) = x"
  shows "map_vars_term n (map_vars_term m t) = t"
  unfolding map_vars_term_compose o_def inj by (auto simp: term.map_ident)

lemma inj_map_vars_term_the_inv:
  assumes "inj f"
  shows "map_vars_term (the_inv f) (map_vars_term f t) = t"
  unfolding map_vars_term_compose o_def the_inv_f_f[OF assms]
  by (simp add: term.map_ident)

lemma map_vars_ctxt_subst:
  "map_vars_ctxt m (C c σ) = C c map_vars_subst_ran m σ"
  by (induct C) (auto simp: map_vars_subst_ran)

lemma poss_map_vars_term [simp]:
  "poss (map_vars_term f t) = poss t"
  by (induct t) auto

lemma map_vars_term_subt_at [simp]:
  "p  poss t  map_vars_term f (t |_ p) = (map_vars_term f t) |_ p"
proof (induct p arbitrary: t)
  case Nil show ?case by auto
next
  case (Cons i p t)
  from Cons(2) obtain g ts where t: "t = Fun g ts" by (cases t, auto)
  from Cons show ?case unfolding t by auto
qed

lemma hole_pos_subst[simp]: "hole_pos (C c σ) = hole_pos C"
  by (induct C, auto)

lemma hole_pos_ctxt_compose[simp]: "hole_pos (C c D) = hole_pos C @ hole_pos D"
  by (induct C, auto)

lemma subst_left_right: "t  μ^^n  μ = t  μ  μ^^n"
proof -
  have "t  μ ^^ n  μ = t  (μ ^^ n s μ)" by simp
  also have "... = t  (μ s μ ^^ n)"
    using subst_power_compose_distrib[of n "Suc 0" μ] by auto
  finally show ?thesis by simp
qed

lemma subst_right_left: "t  μ  μ^^n = t  μ^^n  μ" unfolding subst_left_right ..

lemma subt_at_id_imp_eps:
  assumes p: "p  poss t" and id: "t |_ p = t"
  shows "p = []"
proof (cases p)
  case (Cons i q)
  from subt_at_nepos_imp_supt[OF p[unfolded Cons], unfolded Cons[symmetric]
      , unfolded id] have False by simp
  then show ?thesis by auto
qed simp

lemma pos_into_subst:
  assumes t: "t  σ = s" and p: "p  poss s" and nt: "¬ (p  poss t  is_Fun (t |_ p))"
  shows "q q' x. p = q @ q'  q  poss t  t |_ q = Var x"
  using p nt unfolding t[symmetric]
proof (induct t arbitrary: p)
  case (Var x)
  show ?case
    by (rule exI[of _ "[]"], rule exI[of _ p], rule exI[of _ x], insert Var, auto)
next
  case (Fun f ts)
  from Fun(3) obtain i q where p: "p = i # q" by (cases p, auto)
  note Fun = Fun[unfolded p]
  from Fun(2) have i: "i < length ts" and q: "q  poss (ts ! i  σ)" by auto
  then have mem: "ts ! i  set ts" by auto
  from Fun(3) i have "¬ (q  poss (ts ! i)  is_Fun (ts ! i |_ q))" by auto
  from Fun(1)[OF mem q this]
  obtain r r' x where q: "q = r @ r'  r  poss (ts ! i)  ts ! i |_ r = Var x" by blast
  show ?case
    by (rule exI[of _ "i # r"], rule exI[of _ r'], rule exI[of _ x],
        unfold p, insert i q, auto)
qed

abbreviation (input) "replace_at t p s  (ctxt_of_pos_term p t)s"

(*may lead to nontermination as [simp]*)
lemma replace_at_ident:
  assumes "p  poss t" and "t |_ p = s"
  shows "replace_at t p s = t"
  using assms by (metis ctxt_supt_id)

lemma ctxt_of_pos_term_append:
  assumes "p  poss t"
  shows "ctxt_of_pos_term (p @ q) t = ctxt_of_pos_term p t c ctxt_of_pos_term q (t |_ p)"
  using assms
proof (induct p arbitrary: t)
  case Nil show ?case by simp
next
  case (Cons i p t)
  from Cons(2) obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p  poss (ts ! i)" by (cases t, auto)
  from Cons(1)[OF p]
  show ?case unfolding t using i by auto
qed

lemma parallel_replace_at:
  fixes p1 :: pos
  assumes parallel: "p1  p2"
    and p1: "p1  poss t"
    and p2: "p2  poss t"
  shows "replace_at (replace_at t p1 s1) p2 s2 = replace_at (replace_at t p2 s2) p1 s1"
proof -
  from parallel_remove_prefix[OF parallel]
  obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
    and ij: "i  j" by blast
  from p1 p2 show ?thesis unfolding p1_id p2_id
  proof (induct p arbitrary: t)
    case (Cons k p)
    from Cons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
    note Cons = Cons[unfolded t]
    let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
    from Cons(2) Cons(3) have "?p1  poss (ts ! k)" "?p2  poss (ts ! k)" by auto
    from Cons(1)[OF this] have rec: "replace_at (replace_at (ts ! k) ?p1 s1) ?p2 s2 = replace_at (replace_at (ts ! k) ?p2 s2) ?p1 s1" .
    from k have min: "min (length ts) k = k" by simp
    show ?case unfolding t using rec min k
      by (simp add: nth_append)
  next
    case Nil
    from Nil(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
    note Nil = Nil[unfolded t]
    from Nil have i: "i < length ts" by auto
    let ?p1 = "i # q1"
    let ?p2 = "j # q2"
    let ?s1 = "replace_at (ts ! i) q1 s1"
    let ?s2 = "replace_at (ts ! j) q2 s2"
    let ?ts1 = "ts[i := ?s1]"
    let ?ts2 = "ts[j := ?s2]"
    from j have j': "j < length ?ts1" by simp
    from i have i': "i < length ?ts2" by simp
    have "replace_at (replace_at t ?p1 s1) ?p2 s2 = replace_at (Fun f ?ts1) ?p2 s2" 
      unfolding t upd_conv_take_nth_drop[OF i] by simp
    also have "... = Fun f (?ts1[j := ?s2])"
      unfolding upd_conv_take_nth_drop[OF j'] using ij by simp
    also have "... = Fun f (?ts2[i := ?s1])" using list_update_swap[OF ij]
      by simp
    also have "... = replace_at (Fun f ?ts2) ?p1 s1"
      unfolding upd_conv_take_nth_drop[OF i'] using ij by simp
    also have "... = replace_at (replace_at t ?p2 s2) ?p1 s1" unfolding t
        upd_conv_take_nth_drop[OF j] by simp
    finally show ?case by simp
  qed
qed

lemma parallel_replace_at_subt_at:
  fixes p1 :: pos
  assumes parallel: "p1  p2"
    and p1: "p1  poss t"
    and p2: "p2  poss t"
  shows " (replace_at t p1 s1) |_ p2 = t |_ p2"
proof -
  from parallel_remove_prefix[OF parallel]
  obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
    and ij: "i  j" by blast
  from p1 p2 show ?thesis unfolding p1_id p2_id
  proof (induct p arbitrary: t)
    case (Cons k p)
    from Cons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
    note Cons = Cons[unfolded t]
    let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
    from Cons(2) Cons(3) have "?p1  poss (ts ! k)" "?p2  poss (ts ! k)" by auto
    from Cons(1)[OF this] have rec: "(replace_at (ts ! k) ?p1 s1) |_ ?p2 = (ts ! k) |_ ?p2" .
    from k have min: "min (length ts) k = k" by simp
    show ?case unfolding t using rec min k
      by (simp add: nth_append)
  next
    case Nil
    from Nil(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
    note Nil = Nil[unfolded t]
    from Nil have i: "i < length ts" by auto
    let ?p1 = "i # q1"
    let ?p2 = "j # q2"
    let ?s1 = "replace_at (ts ! i) q1 s1"
    let ?ts1 = "ts[i := ?s1]"
    from j have j': "j < length ?ts1" by simp
    have "(replace_at t ?p1 s1) |_ ?p2 = (Fun f ?ts1) |_ ?p2" unfolding t upd_conv_take_nth_drop[OF i] by simp
    also have "... = ts ! j |_ q2" using ij by simp
    finally show ?case unfolding t by simp
  qed
qed

lemma parallel_poss_replace_at:
  fixes p1 :: pos
  assumes parallel: "p1  p2"
    and p1: "p1  poss t"
  shows "(p2  poss (replace_at t p1 s1)) = (p2  poss t)"
proof -
  from parallel_remove_prefix[OF parallel]
  obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
    and ij: "i  j" by blast
  from p1 show ?thesis unfolding p1_id p2_id
  proof (induct p arbitrary: t)
    case (Cons k p)
    from Cons(2) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
    note Cons = Cons[unfolded t]
    let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
    from Cons(2) have "?p1  poss (ts ! k)" by auto
    from Cons(1)[OF this] have rec: "(?p2  poss (replace_at (ts ! k) ?p1 s1)) = (?p2  poss (ts ! k))" .
    from k have min: "min (length ts) k = k" by simp
    show ?case unfolding t using rec min k
      by (auto simp: nth_append)
  next
    case Nil
    then obtain f ts where t: "t = Fun f ts" and i: "i < length ts" by (cases t, auto)
    let ?p1 = "i # q1"
    let ?s1 = "replace_at (ts ! i) q1 s1"
    have "replace_at t ?p1 s1 = Fun f (ts[i := ?s1])" unfolding t upd_conv_take_nth_drop[OF i] by simp
    then show ?case unfolding t using ij by auto
  qed
qed

lemma replace_at_subt_at: "p  poss t  (replace_at t p s) |_ p = s"
  by (metis hole_pos_ctxt_of_pos_term subt_at_hole_pos)

lemma replace_at_below_poss:
  assumes p: "p'  poss t" and le: "p p p'"
  shows "p  poss (replace_at t p' s)"
proof -
  from le obtain p'' where p'': "p' = p @ p''" unfolding less_eq_pos_def by auto
  from p show ?thesis  unfolding p''
    by (metis hole_pos_ctxt_of_pos_term hole_pos_poss poss_append_poss)
qed

lemma ctxt_of_pos_term_replace_at_below:
  assumes p: "p  poss t" and le: "p p p'"
  shows "ctxt_of_pos_term p (replace_at t p' u) = ctxt_of_pos_term p t"
proof -
  from le obtain p'' where p': "p' = p @ p''" unfolding less_eq_pos_def by auto
  from p show ?thesis unfolding p'
  proof (induct p arbitrary: t)
    case (Cons i p)
    from Cons(2) obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p  poss (ts ! i)"
      by (cases t, auto)
    from i have min: "min (length ts) i = i" by simp
    show ?case unfolding t using Cons(1)[OF p] i by (auto simp: nth_append min)
  next
    case Nil show ?case by simp
  qed
qed

lemma ctxt_of_pos_term_hole_pos[simp]:
  "ctxt_of_pos_term (hole_pos C) (Ct) = C"
  by (induct C) simp_all

lemma ctxt_poss_imp_ctxt_subst_poss:
  assumes p:"p'  poss Ct" shows "p'  poss Ct  μ"
proof(rule disjE[OF pos_cases[of p' "hole_pos C"]])
  assume "p' p hole_pos C"
  then show ?thesis using hole_pos_poss by (metis less_eq_pos_def poss_append_poss)
next
  assume or:"hole_pos C <p p'  p'  hole_pos C"
  show ?thesis proof(rule disjE[OF or])
    assume "hole_pos C <p p'"
    then obtain q where dec:"p' = hole_pos C @ q" unfolding less_pos_def less_eq_pos_def by auto
    with p have "q  poss (t  μ)" using hole_pos_poss_conv poss_imp_subst_poss by auto
    then show ?thesis using dec hole_pos_poss_conv by auto
  next
    assume "p'  hole_pos C"
    then have par:"hole_pos C  p'" by (rule parallel_pos_sym)
    have aux:"hole_pos C  poss Ct  μ" using hole_pos_poss by auto
    from p show ?thesis using parallel_poss_replace_at[OF par aux,unfolded ctxt_of_pos_term_hole_pos] by fast
  qed
qed

lemma var_pos_maximal:
  assumes pt:"p  poss t" and x:"t |_ p = Var x" and "q  []"
  shows "p @ q  poss t"
proof-
  from assms have "q  poss (Var x)" by force
  with poss_append_poss[of p q] pt x show ?thesis by simp
qed

text ‹Positions in a context›
definition possc :: "('f, 'v) ctxt  pos set"  where "possc C  {p | p. t. p  poss Ct}"

lemma poss_imp_possc: "p  possc C  p  poss Ct" unfolding possc_def by auto

lemma less_eq_hole_pos_in_possc:
  assumes pleq:"p p hole_pos C" shows "p  possc C"
  unfolding possc_def
  using replace_at_below_poss[OF hole_pos_poss pleq, unfolded hole_pos_id_ctxt[OF refl]] by simp

lemma hole_pos_in_possc:"hole_pos C  possc C"
  using less_eq_hole_pos_in_possc order_refl by blast

lemma par_hole_pos_in_possc:
  assumes par:"hole_pos C  p" and ex:"p  poss Ct" shows "p  possc C"
  using parallel_poss_replace_at[OF par hole_pos_poss, unfolded hole_pos_id_ctxt[OF refl], of t] ex
  unfolding possc_def by simp

lemma possc_not_below_hole_pos:
  assumes "p  possc (C::('a,'b) ctxt)" shows "¬ (hole_pos C <p p)"
proof(rule notI)
  assume "hole_pos C <p p"
  then obtain r where p':"p = hole_pos C @ r" and r:"r  []"
    unfolding less_pos_def less_eq_pos_def by auto
  fix x::'b from r have n:"r  poss (Var x)" using poss.simps(1) by auto
  from assms have "p  (poss CVar x)" unfolding possc_def by auto
  with this[unfolded p'] hole_pos_poss_conv[of C r] have "r  poss (Var x)" by auto
  with n show False by simp
qed

lemma possc_subst_not_possc_not_poss:
  assumes y:"p  possc (C c σ)" and n:"p  possc C" shows "p  poss Ct"
proof-
  from n obtain u where a:"p  poss Cu" unfolding possc_def by auto
  from possc_not_below_hole_pos[OF y] have b:"¬ (hole_pos C <p p)"
    unfolding hole_pos_subst[of C σ] by auto
  from n a have c:"¬ (p p hole_pos C)" unfolding less_pos_def using less_eq_hole_pos_in_possc by blast
  with pos_cases b have "p  hole_pos C" by blast
  with par_hole_pos_in_possc[OF parallel_pos_sym[OF this]] n show "p  poss (Ct)" by fast
qed

text ‹All proper terms in a context›
fun ctxt_to_term_list :: "('f, 'v) ctxt  ('f, 'v) term list"
  where
    "ctxt_to_term_list Hole = []" |
    "ctxt_to_term_list (More f bef C aft) = ctxt_to_term_list C @ bef @ aft"

lemma ctxt_to_term_list_supt: "t  set (ctxt_to_term_list C)  Cs  t"
proof (induct C)
  case (More f bef C aft)
  from More(2) have choice: "t  set (ctxt_to_term_list C)  t  set bef  t  set aft" by simp
  {
    assume "t  set bef  t  set aft"
    then have "t  set (bef @ Cs # aft)" by auto
    then have ?case by auto
  }
  moreover
  {
    assume t: "t  set (ctxt_to_term_list C)"
    have "(More f bef C aft)s  Cs" by auto
    moreover have "Cs  t"
      by (rule More(1)[OF t])
    ultimately have ?case
      by (rule supt_trans)
  }
  ultimately show ?case using choice by auto
qed auto

lemma subteq_Var_imp_in_vars_term:
  "r  Var x  x  vars_term r"
proof (induct r rule: term.induct)
  case (Var y) 
  then have "x = y" by (cases rule: supteq.cases) auto
  then show ?case by simp
next
  case (Fun f ss)
  from Fun f ss  Var x have "(Fun f ss = Var x)  (Fun f ss  Var x)" by auto
  then show ?case
  proof
    assume "Fun f ss = Var x" then show ?thesis by auto
  next
    assume "Fun f ss  Var x"
    then obtain s where "s  set ss" and "s  Var x" using supt_Fun_imp_arg_supteq by best
    with Fun have "s  Var x  x  vars_term s" by best
    with s  Var x have "x  vars_term s" by simp
    with s  set ss show ?thesis by auto
  qed
qed

fun instance_term :: "('f, 'v) term  ('f set, 'v) term  bool"
  where
    "instance_term (Var x) (Var y)  x = y" |
    "instance_term (Fun f ts) (Fun fs ss) 
    f  fs  length ts = length ss  (i<length ts. instance_term (ts ! i) (ss ! i))" |
    "instance_term _ _ = False"

fun subt_at_ctxt :: "('f, 'v) ctxt  pos  ('f, 'v) ctxt" (infixl "|'_c" 67)
  where
    "C |_c [] = C" |
    "More f bef C aft |_c (i#p) = C |_c p"

lemma subt_at_subt_at_ctxt:
  assumes "hole_pos C = p @ q"
  shows "Ct |_ p = (C |_c p)t"
  using assms
proof (induct p arbitrary: C)
  case (Cons i p)
  then obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
  from Cons(2) have "hole_pos D = p @ q" unfolding C by simp
  from Cons(1)[OF this] have id: "(D |_c p) t = Dt |_ p" by simp
  show ?case unfolding C subt_at_ctxt.simps id using Cons(2) C by auto
qed simp

lemma hole_pos_subt_at_ctxt:
  assumes "hole_pos C = p @ q"
  shows "hole_pos (C |_c p) = q"
  using assms
proof (induct p arbitrary: C)
  case (Cons i p)
  then obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
  show ?case unfolding C subt_at_ctxt.simps
    by (rule Cons(1), insert Cons(2) C, auto)
qed simp

lemma subt_at_ctxt_compose[simp]: "(C c D) |_c hole_pos C = D"
  by (induct C, auto)

lemma split_ctxt:
  assumes "hole_pos C = p @ q"
  shows " D E. C = D c E  hole_pos D = p  hole_pos E = q  E = C |_c p"
  using assms
proof (induct p arbitrary: C)
  case Nil
  show ?case
    by (rule exI[of _ ], rule exI[of _ C], insert Nil, auto)
next
  case (Cons i p)
  then obtain f bef C' aft where C: "C = More f bef C' aft" by (cases C, auto)
  from Cons(2) have "hole_pos C' = p @ q" unfolding C by simp
  from Cons(1)[OF this] obtain D E where C': "C' = D c E"
    and p: "hole_pos D = p" and q: "hole_pos E = q" and E: "E = C' |_c p"
    by auto
  show ?case
    by (rule exI[of _ "More f bef D aft"], rule exI[of _ E], unfold C C',
        insert p[symmetric] q E Cons(2) C, simp)
qed

lemma ctxt_subst_id[simp]: "C c Var = C" by (induct C, auto)

text ‹the strict subterm relation between contexts and terms›
inductive_set
  suptc :: "(('f, 'v) ctxt × ('f, 'v) term) set"
  where
    arg: "s  set bef  set aft  s  t  (More f bef C aft, t)  suptc"
  |  ctxt: "(C,s)  suptc  (D c C, s)  suptc"

hide_const suptcp

abbreviation suptc_pred where "suptc_pred C t  (C, t)  suptc"

notation (xsymbols)
  suptc_pred ("(_/ ⊳c _)" [56, 56] 55)

lemma suptc_subst: "C ⊳c s  C c σ ⊳c s  σ"
proof (induct rule: suptc.induct)
  case (arg s bef aft t f C)
  let ?s = "λ t. t  σ"
  let ?m = "map ?s"
  have id: "More f bef C aft c σ = More f (?m bef) (C c σ) (?m aft)" by simp
  show ?case unfolding id
    by (rule suptc.arg[OF _ supteq_subst[OF arg(2)]],
        insert arg(1), auto)
next
  case (ctxt C s D)
  have id: "D c C c σ = (D c σ) c (C c σ)" by simp
  show ?case unfolding id
    by (rule suptc.ctxt[OF ctxt(2)])
qed

lemma suptc_imp_supt: "C ⊳c s  Ct  s"
proof (induct rule: suptc.induct)
  case (arg s bef aft u f C)
  let ?C = "(More f bef C aft)"
  from arg(1) have "s  set (args (?Ct))" by auto
  then have "?Ct  s" by auto
  from supt_supteq_trans[OF this arg(2)]
  show ?case .
next
  case (ctxt C s D)
  have supteq: "(D c C)t  Ct" by auto
  from supteq_supt_trans[OF this ctxt(2)]
  show ?case .
qed

lemma suptc_supteq_trans: "C ⊳c s  s  t  C ⊳c t"
proof (induct rule: suptc.induct)
  case (arg s bef aft u f C)
  show ?case
    by (rule suptc.arg[OF arg(1) supteq_trans[OF arg(2) arg(3)]])
next
  case (ctxt C s D)
  then have supt: "C ⊳c t" by auto
  then show ?case by (rule suptc.ctxt)
qed

lemma supteq_suptc_trans: "C = D c E  E ⊳c s  C ⊳c s"
  by (auto intro: suptc.ctxt)

hide_fact (open)
  suptcp.arg suptcp.cases suptcp.induct suptcp.intros suptc.arg suptc.ctxt

lemma supteq_ctxt_cases': "C  t   u 
  C ⊳c u  t  u  ( D C'. C = D c C'  u = C'  t   C'  )"
proof (induct C)
  case (More f bef C aft)
  let ?C = "More f bef C aft"
  let ?ba = "bef @ C  t  # aft"
  from More(2) have "Fun f ?ba  u" by simp
  then show ?case
  proof (cases rule: supteq.cases)
    case refl
    show ?thesis unfolding refl
      by (intro disjI2, rule exI[of _ Hole], rule exI[of _ ?C], auto)
  next
    case (subt v)
    show ?thesis
    proof (cases "v  set bef  set aft")
      case True
      from suptc.arg[OF this subt(2)]
      show ?thesis by simp
    next
      case False
      with subt have "C t   u" by simp
      from More(1)[OF this]
      show ?thesis
      proof (elim disjE exE conjE)
        assume "C ⊳c u"
        from suptc.ctxt[OF this, of "More f bef  aft"] show ?thesis by simp
      next
        fix D C'
        assume *: "C = D c C'" "u = C't" "C'  "
        show ?thesis
          by (intro disjI2 conjI, rule exI[of _ "More f bef D aft"], rule exI[of _ C'],
              insert *, auto)
      qed simp
    qed
  qed
qed simp

lemma supteq_ctxt_cases[consumes 1, case_names in_ctxt in_term sub_ctxt]: "C  t   u 
  (C ⊳c u  P) 
  (t  u  P) 
  ( D C'. C = D c C'  u = C'  t   C'    P)  P"
  using supteq_ctxt_cases' by blast

definition vars_subst :: "('f, 'v) subst  'v set"
  where
    "vars_subst σ = subst_domain σ  (vars_term ` subst_range σ)"

lemma range_vars_subst_compose_subset:
  "range_vars (σ s τ)  (range_vars σ - subst_domain τ)  range_vars τ" (is "?L  ?R")
proof
  fix x
  assume "x  ?L"
  then obtain y where "y  subst_domain (σ s τ)"
    and "x  vars_term ((σ s τ) y)" by (auto simp: range_vars_def)
  then show "x  ?R"
  proof (cases)
    assume "y  subst_domain σ" and "x  vars_term ((σ s τ) y)"
    moreover then obtain v where "v  vars_term (σ y)"
      and "x  vars_term (τ v)" by (auto simp: subst_compose_def vars_term_subst)
    ultimately show ?thesis
      by (cases "v  subst_domain τ") (auto simp: range_vars_def subst_domain_def)
  qed (auto simp: range_vars_def subst_compose_def subst_domain_def)
qed

text ‹
  A substitution is idempotent iff the variables in its range are disjoint from its domain. See also
  "Term Rewriting and All That" Lemma 4.5.7.
›
lemma subst_idemp_iff:
  "σ s σ = σ  subst_domain σ  range_vars σ = {}"
proof
  assume "σ s σ = σ"
  then have "x. σ x  σ = σ x  Var" by simp (metis subst_compose_def)
  then have *: "x. yvars_term (σ x). σ y = Var y"
    unfolding term_subst_eq_conv by simp
  { fix x y
    assume "σ x  Var x" and "x  vars_term (σ y)"
    with * [of y] have False by simp }
  then show "subst_domain σ  range_vars σ = {}"
    by (auto simp: subst_domain_def range_vars_def)
next
  assume "subst_domain σ  range_vars σ = {}"
  then have *: "x y. σ x = Var x  σ y = Var y  x  vars_term (σ y)"
    by (auto simp: subst_domain_def range_vars_def)
  have "x. yvars_term (σ x). σ y = Var y"
  proof
    fix x y
    assume "y  vars_term (σ x)"
    with * [of y x] show "σ y = Var y" by auto
  qed
  then show "σ s σ = σ"
    by (simp add: subst_compose_def term_subst_eq_conv [symmetric])
qed

definition subst_compose' :: "('f, 'v) subst  ('f, 'v) subst  ('f, 'v) subst" where
  "subst_compose' σ τ = (λ x. if (x  subst_domain σ) then σ x  τ else Var x)"

lemma vars_subst_compose':
  assumes "vars_subst τ  subst_domain σ = {}"
  shows "σ s τ = τ s (subst_compose' σ τ)" (is "?l = ?r")
proof
  fix x
  show "?l x = ?r x"
  proof (cases "x  subst_domain σ")
    case True
    with assms have nmem: "x  vars_subst τ" by auto
    then have nmem: "x  subst_domain τ" unfolding vars_subst_def by auto
    then have id: "τ x = Var x" unfolding subst_domain_def by auto
    have "?l x = σ x  τ" unfolding subst_compose_def by simp
    also have  "... = ?r x" unfolding subst_compose'_def subst_compose_def using True unfolding id by simp
    finally show ?thesis .
  next
    case False
    then have l: "?l x = τ x  Var" unfolding subst_domain_def subst_compose_def by auto
    let ?στ = "(λ x. if x  subst_domain σ then σ x  τ else Var x)"
    have r: "?r x = τ x  ?στ"
      unfolding subst_compose'_def subst_compose_def ..
    show "?l x = ?r x" unfolding l r
    proof (rule term_subst_eq)
      fix y
      assume y: "y  vars_term (τ x)"
      have "y  vars_subst τ  τ x = Var x"
      proof (cases "x  subst_domain τ")
        case True then show ?thesis using y unfolding vars_subst_def by auto
      next
        case False
        then show ?thesis  unfolding subst_domain_def by auto
      qed
      then show "Var y = ?στ y"
      proof
        assume "y  vars_subst τ"
        with assms have "y  subst_domain σ" by auto
        then show ?thesis by simp
      next
        assume "τ x = Var x"
        with y have y: "y = x" by simp
        show ?thesis unfolding y using False by auto
      qed
    qed
  qed
qed

lemma vars_subst_compose'_pow:
  assumes "vars_subst τ  subst_domain σ = {}"
  shows "σ ^^ n s τ = τ s (subst_compose' σ τ) ^^ n"
proof (induct n)
  case 0 then show ?case by auto
next
  case (Suc n)
  let ?στ = "subst_compose' σ τ"
  have "σ ^^ Suc n s τ = σ s (σ ^^ n s τ)" by (simp add: ac_simps)
  also have "... = σ s (τ s ?στ^^n)" unfolding Suc ..
  also have "... = (σ s τ) s ?στ ^^ n" by (auto simp: ac_simps)
  also have "... = (τ s ?στ) s ?στ ^^ n" unfolding vars_subst_compose'[OF assms] ..
  finally show ?case by (simp add: ac_simps)
qed

lemma subst_pow_commute:
  assumes "σ s τ = τ s σ"
  shows "σ s (τ ^^ n) = τ ^^ n s σ"
proof (induct n)
  case (Suc n)
  have "σ s τ ^^ Suc n = (σ s τ) s τ ^^ n" by (simp add: ac_simps)
  also have "... = τ s (σ s τ ^^ n)" unfolding assms by (simp add: ac_simps)
  also have "... = τ ^^ Suc n s σ" unfolding Suc by (simp add: ac_simps)
  finally show ?case .
qed simp

lemma subst_power_commute:
  assumes "σ s τ = τ s σ"
  shows "(σ ^^ n) s (τ ^^ n) = (σ s τ)^^n"
proof (induct n)
  case (Suc n)
  have "(σ ^^ Suc n) s (τ ^^ Suc n) = (σ^^n s (σ s τ ^^ n) s τ)"
    unfolding subst_power_Suc by (simp add: ac_simps)
  also have "... = (σ^^n s τ ^^ n) s (σ s τ)"
    unfolding subst_pow_commute[OF assms] by (simp add: ac_simps)
  also have "... = (σ s τ)^^Suc n" unfolding Suc
    unfolding subst_power_Suc ..
  finally show ?case .
qed simp

lemma vars_term_ctxt_apply:
  "vars_term (Ct) = vars_ctxt C  vars_term t"
  by (induct C) (auto)

lemma vars_ctxt_pos_term:
  assumes "p  poss t"
  shows "vars_term t = vars_ctxt (ctxt_of_pos_term p t)  vars_term (t |_ p)"
proof -
  let ?C = "ctxt_of_pos_term p t"
  have "t = ?Ct |_ p" using ctxt_supt_id [OF assms] by simp
  then have "vars_term t = vars_term (?Ct |_ p)" by simp
  then show ?thesis unfolding vars_term_ctxt_apply .
qed

lemma vars_term_subt_at:
  assumes "p  poss t"
  shows "vars_term (t |_ p)  vars_term t"
  using vars_ctxt_pos_term [OF assms] by simp

lemma Var_pow_Var[simp]: "Var ^^ n = Var"
  by (rule, induct n, auto)

definition is_inverse_renaming :: "('f, 'v) subst  ('f, 'v) subst" where
  "is_inverse_renaming σ y = (
    if Var y  subst_range σ then Var (the_inv_into (subst_domain σ) σ (Var y))
    else Var y)"

lemma is_renaming_inverse_domain:
  assumes ren: "is_renaming σ"
    and x: "x  subst_domain σ"
  shows "Var x  σ  is_inverse_renaming σ = Var x" (is "_   = _")
proof -
  note ren = ren[unfolded is_renaming_def]
  from ren obtain y where σx: "σ x = Var y" by force
  from ren have inj: "inj_on σ (subst_domain σ)" by auto
  note inj = the_inv_into_f_eq[OF inj, OF σx]
  note d = is_inverse_renaming_def
  from x have "Var y  subst_range σ" using σx by force
  then have " y = Var (the_inv_into (subst_domain σ) σ (Var y))" unfolding d by simp
  also have "... = Var x" using inj[OF x] by simp
  finally show ?thesis using σx by simp
qed

lemma is_renaming_inverse_range:
  assumes varren: "is_renaming σ"
    and x: "Var x  subst_range σ"
  shows "Var x  σ  is_inverse_renaming σ = Var x" (is "_   = _")
proof (cases "x  subst_domain σ")
  case True
  from is_renaming_inverse_domain[OF varren True]
  show ?thesis .
next
  case False
  then have σx: "σ x = Var x" unfolding subst_domain_def by auto
  note ren = varren[unfolded is_renaming_def]
  note d = is_inverse_renaming_def
  have "Var x  σ   =  x" using σx by auto
  also have "... = Var x"
    unfolding d using x by simp
  finally show ?thesis .
qed

lemma vars_subst_compose:
  "vars_subst (σ s τ)  vars_subst σ  vars_subst τ"
proof
  fix x
  assume "x  vars_subst (σ s τ)"
  from this[unfolded vars_subst_def subst_range.simps]
  obtain y where "y  subst_domain (σ s τ)  (x = y  x  vars_term ((σ s τ) y))" by blast
  with subst_domain_compose[of σ τ] have y: "y  subst_domain σ  subst_domain τ" and disj:
    "x = y  (x  y  x  vars_term (σ y  τ))" unfolding subst_compose_def by auto
  from disj
  show "x  vars_subst σ  vars_subst τ"
  proof
    assume "x = y"
    with y show ?thesis unfolding vars_subst_def by auto
  next
    assume "x  y  x  vars_term (σ y  τ)"
    then obtain z where neq: "x  y" and x: "x  vars_term (τ z)" and z: "z  vars_term (σ y)" unfolding vars_term_subst by auto
    show ?thesis
    proof (cases "τ z = Var z")
      case False
      with x have "x  vars_subst τ" unfolding vars_subst_def subst_domain_def subst_range.simps by blast
      then show ?thesis by auto
    next
      case True
      with x have x: "z = x" by auto
      with z have y: "x  vars_term (σ y)" by auto
      show ?thesis
      proof (cases "σ y = Var y")
        case False
        with y have "x  vars_subst σ" unfolding vars_subst_def subst_domain_def subst_range.simps by blast
        then show ?thesis by auto
      next
        case True
        with y have "x = y" by auto
        with neq show ?thesis by auto
      qed
    qed
  qed
qed

lemma vars_subst_compose_update:
  assumes x: "x  vars_subst σ"
  shows "σ s τ(x := t) = (σ s τ)(x := t)" (is "?l = ?r")
proof
  fix z
  note x = x[unfolded vars_subst_def subst_domain_def]
  from x have xx: "σ x = Var x" by auto
  show "?l z = ?r z"
  proof (cases "z = x")
    case True
    with xx show ?thesis by (simp add: subst_compose_def)
  next
    case False
    then have "?r z = σ z  τ" unfolding subst_compose_def by auto
    also have "... = ?l z" unfolding subst_compose_def
    proof (rule term_subst_eq)
      fix y
      assume "y  vars_term (σ z)"
      with False x have v: "y  x" unfolding subst_range.simps subst_domain_def by force
      then show "τ y = (τ(x := t)) y" by simp
    qed
    finally show ?thesis by simp
  qed
qed

lemma subst_variants_imp_eq:
  assumes "σ s σ' = τ" and "τ s τ' = σ"
  shows "x. σ x  σ' = τ x" "x. τ x  τ' = σ x"
  using assms by (metis subst_compose_def)+

lemma poss_subst_choice: assumes "p  poss (t  σ)" shows
  "p  poss t  is_Fun (t |_ p) 
  ( x q1 q2. q1  poss t  q2  poss (σ x)  t |_ q1 = Var x  x  vars_term t
     p = q1 @ q2  t  σ |_ p = σ x |_ q2)" (is "_  ( x q1 q2. ?p x q1 q2 t p)")
  using assms
proof (induct p arbitrary: t)
  case (Cons i p t)
  show ?case
  proof (cases t)
    case (Var x)
    have "?p x [] (i # p) t (i # p)" using Cons(2) unfolding Var by simp
    then show ?thesis by blast
  next
    case (Fun f ts)
    with Cons(2) have i: "i < length ts" and p: "p  poss (ts ! i  σ)" by auto
    from Cons(1)[OF p]
    show ?thesis
    proof
      assume " x q1 q2. ?p x q1 q2 (ts ! i) p"
      then obtain x q1 q2 where "?p x q1 q2 (ts ! i) p" by auto
      with Fun i have "?p x (i # q1) q2 (Fun f ts) (i # p)" by auto
      then show ?thesis unfolding Fun by blast
    next
      assume "p  poss (ts ! i)  is_Fun (ts ! i |_ p)"
      then show ?thesis using Fun i by auto
    qed
  qed
next
  case Nil
  show ?case
  proof (cases t)
    case (Var x)
    have "?p x [] [] t []" unfolding Var by auto
    then show ?thesis by auto
  qed simp
qed

fun vars_term_list :: "('f, 'v) term  'v list"
  where
    "vars_term_list (Var x) = [x]" |
    "vars_term_list (Fun _ ts) = concat (map vars_term_list ts)"

lemma set_vars_term_list [simp]:
  "set (vars_term_list t) = vars_term t"
  by (induct t) simp_all

lemma unary_vars_term_list:
  assumes t: "funas_term t  F"
    and unary: " f n. (f, n)  F  n  1"
  shows "vars_term_list t = []  ( x  vars_term t. vars_term_list t = [x])"
proof -
  from t show ?thesis
  proof (induct t)
    case Var then show ?case by auto
  next
    case (Fun f ss)
    show ?case
    proof (cases ss)
      case Nil
      then show ?thesis by auto
    next
      case (Cons t ts)
      let ?n = "length ss"
      from Fun(2) have "(f,?n)  F" by auto
      from unary[OF this] have n: "?n  Suc 0" by auto
      with Cons have "?n = Suc 0" by simp
      with Cons have ss: "ss = [t]" by (cases ts, auto)
      note IH = Fun(1)[unfolded ss, simplified]
      from ss have id1: "vars_term_list (Fun f ss) = vars_term_list t" by simp
      from ss have id2: "vars_term (Fun f ss) = vars_term t" by simp
      from Fun(2) ss have mem: "funas_term t  F" by auto
      show ?thesis unfolding id1 id2 using IH[OF refl mem] by simp
    qed
  qed
qed

declare vars_term_list.simps [simp del]

text ‹The list of function symbols in a term (without removing duplicates).›

fun funs_term_list :: "('f, 'v) term  'f list"
  where
    "funs_term_list (Var _) = []" |
    "funs_term_list (Fun f ts) = f # concat (map funs_term_list ts)"

lemma set_funs_term_list [simp]:
  "set (funs_term_list t) = funs_term t"
  by (induct t) simp_all

declare funs_term_list.simps [simp del]

text ‹The list of function symbol and arity pairs in a term
(without removing duplicates).›

fun funas_term_list :: "('f, 'v) term  ('f × nat) list"
  where
    "funas_term_list (Var _) = []" |
    "funas_term_list (Fun f ts) = (f, length ts) # concat (map funas_term_list ts)"

lemma set_funas_term_list [simp]:
  "set (funas_term_list t) = funas_term t"
  by (induct t) simp_all

declare funas_term_list.simps [simp del]

definition funas_args_term_list :: "('f, 'v) term  ('f × nat) list"
  where
    "funas_args_term_list t = concat (map funas_term_list (args t))"

lemma set_funas_args_term_list [simp]:
  "set (funas_args_term_list t) = funas_args_term t"
  by (simp add: funas_args_term_def funas_args_term_list_def)

lemma vars_term_list_map_funs_term:
  "vars_term_list (map_funs_term fg t) = vars_term_list t"
proof (induct t)
  case (Var x) then show ?case by (simp add: vars_term_list.simps)
next
  case (Fun f ss)
  show ?case by (simp add: vars_term_list.simps o_def, insert Fun, induct ss, auto)
qed

lemma funs_term_list_map_funs_term:
  "funs_term_list (map_funs_term fg t) = map fg (funs_term_list t)"
proof (induct t)
  case (Var x) show ?case by (simp add: funs_term_list.simps)
next
  case (Fun f ts)
  show ?case
    by (simp add: funs_term_list.simps, insert Fun, induct ts, auto)
qed

text ‹
  Next we provide some functions to compute multisets instead of sets of
  function symbols, variables, etc.
  they may be helpful for non-duplicating TRSs.
›

fun funs_term_ms :: "('f,'v)term  'f multiset"
  where
    "funs_term_ms (Var x) = {#}" |
    "funs_term_ms (Fun f ts) = {#f#} + # (mset (map funs_term_ms ts))"

fun funs_ctxt_ms :: "('f,'v)ctxt  'f multiset"
  where
    "funs_ctxt_ms Hole = {#}" |
    "funs_ctxt_ms (More f bef C aft) =
    {#f#} + # (mset (map funs_term_ms bef)) +
    funs_ctxt_ms C + # (mset (map funs_term_ms aft))"

lemma funs_term_ms_ctxt_apply:
  "funs_term_ms Ct = funs_ctxt_ms C + funs_term_ms t"
  by (induct C) (auto simp: multiset_eq_iff)

lemma funs_term_ms_subst_apply:
  "funs_term_ms (t  σ) =
    funs_term_ms t + # (image_mset (λ x. funs_term_ms (σ x)) (vars_term_ms t))"
proof (induct t)
  case (Fun f ts)
  let ?m = "mset"
  let ?f = "funs_term_ms"
  let ?ts = "# (?m (map ?f ts))"
  let   = "# (image_mset (λx. ?f (σ x)) (# (?m (map vars_term_ms ts))))"
  let ?tsσ = "# (?m (map (λ x. ?f (x  σ)) ts))"
  have ind: "?tsσ = ?ts + " using Fun
    by (induct ts, auto simp: multiset_eq_iff)
  then show ?case unfolding multiset_eq_iff by (simp add: o_def)
qed auto

lemma ground_vars_term_ms_empty:
  "ground t = (vars_term_ms t = {#})"
  unfolding ground_vars_term_empty
  unfolding set_mset_vars_term_ms [symmetric]
  by (simp del: set_mset_vars_term_ms)

lemma vars_term_ms_map_funs_term [simp]:
  "vars_term_ms (map_funs_term fg t) = vars_term_ms t"
proof (induct t)
  case (Fun f ts)
  then show ?case by (induct ts) auto
qed simp

lemma funs_term_ms_map_funs_term:
  "funs_term_ms (map_funs_term fg t) = image_mset fg (funs_term_ms t)"
proof (induct t)
  case (Fun f ss)
  then show ?case by (induct ss, auto)
qed auto

lemma supteq_imp_vars_term_ms_subset:
  "s  t  vars_term_ms t ⊆# vars_term_ms s"
proof (induct rule: supteq.induct)
  case (subt u ss t f)
  from subt(1) obtain bef aft where ss: "ss = bef @ u # aft"
    by (metis in_set_conv_decomp)
  have "vars_term_ms t ⊆# vars_term_ms u" by fact
  also have " ⊆# # (mset (map vars_term_ms ss))"
    unfolding ss by (simp add: ac_simps)
  also have " = vars_term_ms (Fun f ss)" by auto
  finally show ?case by auto
qed auto

lemma mset_funs_term_list:
  "mset (funs_term_list t) = funs_term_ms t"
proof (induct t)
  case (Var x) show ?case by (simp add: funs_term_list.simps)
next
  case (Fun f ts)
  show ?case
    by (simp add: funs_term_list.simps, insert Fun, induct ts, auto simp: funs_term_list.simps multiset_eq_iff)
qed

text ‹Creating substitutions from lists›

type_synonym ('f, 'v, 'w) gsubstL = "('v × ('f, 'w) term) list"
type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"

definition mk_subst :: "('v  ('f, 'w) term)  ('f, 'v, 'w) gsubstL  ('f, 'v, 'w) gsubst" where
  "mk_subst d xts 
    (λx. case map_of xts x of
      None  d x
    | Some t  t)"

lemma mk_subst_not_mem:
  assumes x: "x  set xs"
  shows "mk_subst f (zip xs ts) x = f x"
proof -
  have "map_of (zip xs ts) x = None"
    unfolding map_of_eq_None_iff set_zip using x[unfolded set_conv_nth] by auto
  then show ?thesis unfolding mk_subst_def by auto
qed

lemma mk_subst_not_mem':
  assumes x: "x  set (map fst ss)"
  shows "mk_subst f ss x = f x"
proof -
  have "map_of ss x = None"
    unfolding map_of_eq_None_iff using x by auto
  then show ?thesis unfolding mk_subst_def by auto
qed

lemma mk_subst_distinct:
  assumes dist: "distinct xs"
    and i: "i < length xs" "i < length ls"
  shows "mk_subst f (zip xs ls) (xs ! i) = ls ! i"
proof - 
  from i have in_zip:"(xs!i, ls!i)  set (zip xs ls)" 
    using nth_zip[OF i] set_zip by auto 
  from dist have dist':"distinct (map fst (zip xs ls))"
    by (simp add: map_fst_zip_take)
  then show ?thesis 
    unfolding mk_subst_def using map_of_is_SomeI[OF dist' in_zip] by simp
qed

lemma mk_subst_Nil [simp]:
  "mk_subst d [] = d"
  by (simp add: mk_subst_def)

lemma mk_subst_concat:
  assumes "x  set (map fst xs)"
  shows "(mk_subst f (xs@ys)) x = (mk_subst f ys) x"
  using assms unfolding mk_subst_def map_of_append
  by (simp add: dom_map_of_conv_image_fst map_add_dom_app_simps(3)) 

lemma mk_subst_concat_Cons:
  assumes "x  set (map fst ss)"
  shows "mk_subst f (concat (ss#ss')) x = mk_subst f ss x"
proof-
  from assms obtain y where "map_of ss x = Some y"
    by (metis list.set_map map_of_eq_None_iff not_None_eq) 
  then show ?thesis unfolding mk_subst_def concat.simps map_of_append
    by simp
qed

lemma vars_term_var_poss_iff:
  "x  vars_term t  (p. p  var_poss t  Var x = t |_ p)" (is "?L  ?R")
proof
  assume x: "?L"
  obtain p where "p  poss t" and "Var x = t |_ p"
    using supteq_imp_subt_at [OF supteq_Var [OF x]] by force
  then show "?R" using var_poss_iff by auto
next
  assume p: "?R"
  then obtain p where 1: "p  var_poss t" and 2: "Var x = t |_ p" by auto
  from var_poss_imp_poss [OF 1] have "p  poss t" .
  then show "?L" by (simp add: 2 subt_at_imp_supteq subteq_Var_imp_in_vars_term)
qed

lemma vars_term_poss_subt_at:
  assumes "x  vars_term t"
  obtains q where "q  poss t" and "t |_ q = Var x"
  using assms
proof (induct t)
  case (Fun f ts)
  then obtain t where t:"t  set ts" and x:"x  vars_term t" by auto
  moreover then obtain i where "t = ts ! i" and "i < length ts" using in_set_conv_nth by metis
  ultimately show ?case using Fun(1)[OF t _ x] Fun(2)[of "Cons i q" for q] by auto
qed auto

lemma vars_ctxt_subt_at':
  assumes "x  vars_ctxt C"
    and "p  poss Ct"
    and "hole_pos C = p"
  shows "q. q  poss Ct  parallel_pos p q  Ct |_ q = Var x"
  using assms
proof (induct C arbitrary: p)
  case (More f bef C aft)
  then have [simp]: "p = length bef # hole_pos C" by auto
  consider
    (C) "x  vars_ctxt C" |
    (bef) t where "t  set bef" and "x  vars_term t" |
    (aft) t where "t  set aft" and "x  vars_term t"
    using More by auto
  then show ?case
  proof (cases)
    case C
    from More(1)[OF this] obtain q where "q  poss Ct  hole_pos C  q  Ct |_ q = Var x"
      by fastforce
    then show ?thesis by (force intro!: exI[of _ "length bef # q"])
  next
    case bef
    then obtain q where "q  poss t" and "t |_ q = Var x"
      using vars_term_poss_subt_at by force
    moreover from bef obtain i where "i < length bef" and "bef ! i = t"
      using in_set_conv_nth by metis
    ultimately show ?thesis
      by (force simp: nth_append intro!: exI[of _ "i # q"])
  next
    case aft
    then obtain q where "q  poss t" and "t |_ q = Var x"
      using vars_term_poss_subt_at by force
    moreover from aft obtain i where "i < length aft" and "aft ! i = t"
      using in_set_conv_nth by metis
    ultimately show ?thesis
      by (force simp: nth_append intro!: exI[of _ "(Suc (length bef) + i) # q"])
  qed
qed auto

lemma vars_ctxt_subt_at:
  assumes "x  vars_ctxt C"
    and "p  poss Ct"
    and "hole_pos C = p"
  obtains q where "q  poss Ct" and "parallel_pos p q" and "Ct |_ q = Var x"
  using vars_ctxt_subt_at' assms by force

lemma poss_is_Fun_fun_poss:
  assumes "p  poss t"
    and "is_Fun (t |_ p)"
  shows "p  fun_poss t"
  using assms by (metis DiffI is_Var_def poss_simps(3) var_poss_iff)

lemma fun_poss_map_vars_term:
  "fun_poss (map_vars_term f t) = fun_poss t"
  unfolding map_vars_term_eq proof(induct t)
  case (Fun g ts)
  {fix i assume "i < length ts"
    with Fun have "fun_poss (map (λt. t  (Var  f)) ts ! i) = fun_poss (ts!i)"
      by fastforce
    then have "{i # p |p. p  fun_poss (map (λt. t  (Var  f)) ts ! i)} = {i # p |p. p  fun_poss (ts ! i)}"
      by presburger
  }
  then show ?case unfolding fun_poss.simps eval_term.simps length_map
    by auto
qed simp

lemma fun_poss_append_poss:
  assumes "p@q  poss t" "q  []"
  shows "p  fun_poss t"
  by (meson assms is_Var_def poss_append_poss poss_is_Fun_fun_poss var_pos_maximal)

lemma fun_poss_append_poss':
  assumes "p@q  fun_poss t"
  shows "p  fun_poss t"
  by (metis append.right_neutral assms fun_poss_append_poss fun_poss_imp_poss)

lemma fun_poss_in_ctxt:
  assumes "q@p  fun_poss (Ct)"
    and "hole_pos C = q"
  shows "p  fun_poss t"
  by (metis Term.term.simps(4) assms fun_poss_fun_conv fun_poss_imp_poss hole_pos_poss hole_pos_poss_conv is_VarE poss_is_Fun_fun_poss subt_at_append subt_at_hole_pos)

lemma args_poss: 
  assumes "i # p  poss t"
  obtains f ts where "t = Fun f ts" "p  poss (ts!i)" "i < length ts"
  by (metis Cons_poss_Var assms poss.elims poss_Cons_poss term.sel(4))

lemma var_poss_parallel:
  assumes "p  var_poss t" and "q  var_poss t" and "p  q"
  shows "p  q"
  using assms proof(induct t arbitrary:p q)
  case (Fun f ts)
  from Fun(2) obtain i p' where i:"i < length ts" "p'  var_poss (ts!i)" and p:"p = i#p'"
    using var_poss_iff by fastforce 
  with Fun(3) obtain j q' where j:"j < length ts" "q'  var_poss (ts!j)" and q:"q = j#q'"
    using var_poss_iff by fastforce 
  then show ?case proof(cases "i = j")
    case True
    from Fun(4) have "p'  q'" 
      unfolding p q True by simp 
    with Fun(1) i j show ?thesis 
      unfolding True p q parallel_pos.simps using nth_mem by blast 
  next
    case False
    then show ?thesis unfolding p q
      by simp
  qed        
qed simp

lemma ctxt_comp_equals:
  assumes poss:"p  poss s" "p  poss t"
    and "ctxt_of_pos_term p s c C = ctxt_of_pos_term p t c D"
  shows "C = D"
  using assms proof(induct p arbitrary:s t)
  case (Cons i p)
  from Cons(2) obtain f ss where s:"s = Fun f ss" and p:"p  poss (ss!i)"
    using args_poss by blast 
  from Cons(3) obtain g ts where t:"t = Fun g ts" and p':"p  poss (ts!i)"
    using args_poss by blast 
  from Cons(1)[OF p p'] Cons(4) show ?case 
    unfolding s t ctxt_of_pos_term.simps ctxt_compose.simps by simp
qed simp

lemma ctxt_subst_comp_pos:
  assumes "q  poss t" and "p  poss (t  τ)"
    and "(ctxt_of_pos_term q t c σ) c C = ctxt_of_pos_term p (t  τ)"
  shows "q p p"
  using assms by (metis hole_pos_ctxt_compose hole_pos_ctxt_of_pos_term hole_pos_subst less_eq_pos_simps(1)) 

text ‹Predicate whether a context is ground, i.e., whether the context contains no variables.›
fun ground_ctxt :: "('f,'v)ctxt  bool" where
  "ground_ctxt Hole = True"
| "ground_ctxt (More f ss1 C ss2) =
    ((sset ss1. ground s)  (sset ss2. ground s)  ground_ctxt C)"

lemma ground_ctxt_apply[simp]: "ground (Ct) = (ground_ctxt C  ground t)"
  by (induct C, auto)

lemma ground_ctxt_compose[simp]: "ground_ctxt (C c D) = (ground_ctxt C  ground_ctxt D)"
  by (induct C, auto)

text ‹Linearity of a term›

fun linear_term :: "('f, 'v) term  bool"
  where
    "linear_term (Var _) = True" |
    "linear_term (Fun _ ts) = (is_partition (map vars_term ts)  (tset ts. linear_term t))"

lemma subst_merge:
  assumes part: "is_partition (map vars_term ts)"
  shows "σ. i<length ts. xvars_term (ts ! i). σ x = τ i x"
proof -
  let  = "map τ [0 ..< length ts]"
  let  = "fun_merge  (map vars_term ts)"
  show ?thesis
    by (rule exI[of _ ], intro allI impI ballI,
        insert fun_merge_part[OF part, of _ _ ], auto)
qed

text ‹Matching for linear terms›
fun weak_match :: "('f, 'v) term  ('f, 'v) term  bool"
  where
    "weak_match _ (Var _)  True" |
    "weak_match (Var _) (Fun _ _)  False" |
    "weak_match (Fun f ts) (Fun g ss) 
    f = g  length ts = length ss  (i < length ts. weak_match (ts ! i) (ss ! i))"

lemma weak_match_refl: "weak_match t t"
  by (induct t) auto

lemma weak_match_match: "weak_match (t  σ) t"
  by (induct t) auto

lemma weak_match_map_funs_term:
  "weak_match t s  weak_match (map_funs_term g t) (map_funs_term g s)"
proof (induct s arbitrary: t)
  case (Fun f ss t)
  from Fun(2) obtain ts where t: "t = Fun f ts" by (cases t, auto)
  from Fun(1)[unfolded set_conv_nth] Fun(2)[unfolded t]
  show ?case unfolding t by force
qed simp

lemma linear_weak_match:
  assumes "linear_term l" and "weak_match t s" and "s = l  σ"
  shows "τ. t = lτ  (xvars_term l. weak_match (Var x  τ) (Var x  σ))"
  using assms proof (induct l arbitrary: s t)
  case (Var x)
  show ?case
  proof (rule exI[of _ "(λ y. t)"], intro conjI, simp)
    from Var show "xvars_term (Var x). weak_match (Var x  (λy. t)) (Var x  σ)"
      by force
  qed
next
  case (Fun f ls)
  let ?n = "length ls"
  from Fun(4) obtain ss where s: "s = Fun f ss" and lss: "length ss = ?n"  by (cases s, auto)
  with Fun(4) have match: " i. i < ?n  ss ! i = (ls ! i)  σ" by auto
  from Fun(3) s lss obtain ts where t: "t = Fun f ts"
    and lts: "length ts = ?n" by (cases t, auto)
  with Fun(3) s have weak_match: " i. i < ?n  weak_match (ts ! i) (ss ! i)" by auto
  from Fun(2) have linear: " i. i < ?n  linear_term (ls ! i)" by simp
  let ?cond = "λ τ i. ts ! i = ls ! i  τ  (xvars_term (ls ! i). weak_match (Var x  τ) (Var x  σ))"
  {
    fix i
    assume i: "i < ?n"
    then have "ls ! i  set ls" by simp
    from Fun(1)[OF this linear[OF i] weak_match[OF i] match[OF i]]
    have " τ. ?cond τ i" .
  }
  then have "i. τ. (i < ?n  ?cond τ i)" by auto
  from choice[OF this] obtain subs where subs: " i. i < ?n  ?cond (subs i) i" by auto
  from Fun(2) have distinct: "is_partition(map vars_term ls)" by simp
  from subst_merge[OF this, of subs]
  obtain τ where τ: " i x . i < length ls  x  vars_term (ls ! i)  τ x = subs i x" by auto
  show ?case
  proof (rule exI[of _ τ], simp add: t, intro ballI conjI)
    fix li x
    assume li: "li  set ls" and x: "x  vars_term li"
    from li obtain i where i: "i < ?n" and li: "li = ls ! i" unfolding set_conv_nth by auto
    with x have x: "x  vars_term (ls ! i)" by simp
    from subs[OF i, THEN conjunct2, THEN bspec, OF x] show "weak_match (τ x) (σ x)" unfolding τ[OF i x[unfolded li]]
      by simp
  next
    show "ts = map (λ t. t  τ) ls"
    proof (rule nth_equalityI, simp add: lts)
      fix i
      assume "i < length ts"
      with lts have i: "i < ?n" by simp
      have "ts ! i = ls ! i  subs i"
        by (rule subs[THEN conjunct1, OF i])
      also have "... = ls ! i  τ" unfolding term_subst_eq_conv using τ[OF i] by auto
      finally show "ts ! i = map (λ t. t  τ) ls ! i"
        by (simp add: nth_map[OF i])
    qed
  qed
qed

lemma map_funs_subst_split:
  assumes "map_funs_term fg t = s  σ"
    and "linear_term s"
  shows " u τ. t = u  τ  map_funs_term fg u = s  (xvars_term s. map_funs_term fg (τ x) = (σ x))"
  using assms
proof (induct s arbitrary: t)
  case (Var x t)
  show ?case
  proof (intro exI conjI)
    show "t = Var x  (λ _. t)" by simp
  qed (insert Var, auto)
next
  case (Fun g ss t)
  from Fun(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
  note Fun = Fun[unfolded t, simplified]
  let ?n = "length ss"
  from Fun have rec: "map (map_funs_term fg) ts = map (λ t. t  σ) ss"
    and g: "fg f = g"
    and lin: " s. s  set ss  linear_term s"
    and part: "is_partition (map vars_term ss)" by auto
  from arg_cong[OF rec, of length] have len: "length ts = ?n" by simp
  from map_nth_conv[OF rec] have rec: " i. i < ?n   map_funs_term fg (ts ! i) = ss ! i  σ" unfolding len by auto
  let ?p = "λ i u τ. ts ! i = u  τ  map_funs_term fg u = ss ! i  (xvars_term (ss ! i). map_funs_term fg (τ x) = σ x)"
  {
    fix i
    assume i: "i < ?n"
    then have "ss ! i  set ss" by auto
    from Fun(1)[OF this rec[OF i] lin[OF this]]
    have " u τ. ?p i u τ" .
  }
  then have "i. u τ. i < ?n  ?p i u τ" by blast
  from choice[OF this] obtain us where "i. τ. i < ?n  ?p i (us i) τ"  ..
  from choice[OF this] obtain τs where p: " i. i < ?n  ?p i (us i) (τs i)" by blast
  from subst_merge[OF part, of τs] obtain τ where τ: " i x. i < ?n  x  vars_term (ss ! i)  τ x = τs i x" by blast
  {
    fix i
    assume i: "i < ?n"
    from p[OF i] have "map_funs_term fg (us i) = ss ! i" by auto
    from arg_cong[OF this, of vars_term] vars_term_map_funs_term[of fg]
    have "vars_term (us i) = vars_term (ss ! i)" by auto
  } note vars = this
  let ?us = "map us [0 ..< ?n]"
  show ?case
  proof (intro exI conjI ballI)
    have ss: "ts = map (λ t. t  τ) ?us"
      unfolding list_eq_iff_nth_eq
      unfolding len
    proof (intro conjI allI impI)
      fix i
      assume i: "i < ?n"
      have us: "?us ! i = us i" using nth_map_upt[of i ?n 0] i by auto
      have "(map (λ t. t  τ) ?us) ! i = us i  τ"
        unfolding us[symmetric]
        using nth_map[of i ?us "λ t. t  τ"]  i by force
      also have "... = us i  τs i"
        by (rule term_subst_eq, rule τ[OF i], insert vars[OF i], auto )
      also have "... = ts ! i" using p[OF i] by simp
      finally
      show "ts ! i = map (λ t. t  τ) ?us ! i" ..
    qed auto
    show "t = Fun f ?us   τ"
      unfolding t
      unfolding ss by auto
  next
    show "map_funs_term fg (Fun f ?us) = Fun g ss"
      using p g by (auto simp: list_eq_iff_nth_eq[of _ ss])
  next
    fix x
    assume x: "x  vars_term (Fun g ss)"
    then obtain s where s: "s  set ss" and x: "x  vars_term s" by auto
    from s[unfolded set_conv_nth] obtain i where s: "s = ss ! i" and i: "i < ?n" by auto
    note x = x[unfolded s]
    from p[OF i] vars[OF i] x τ[OF i x]
    show "map_funs_term fg (τ x) = σ x" by auto
  qed
qed

lemma linear_map_funs_term [simp]:
  "linear_term (map_funs_term f t) = linear_term t"
  by (induct t) simp_all

lemma linear_term_map_inj_on_linear_term:
  assumes "linear_term l"
    and "inj_on f (vars_term l)"
  shows "linear_term (map_vars_term f l)"
  using assms
proof (induct l)
  case (Fun g ls)
  then have part:"is_partition (map vars_term ls)" by auto
  { fix l
    assume l:"l  set ls"
    then have "vars_term l  vars_term (Fun g ls)" by auto
    then have "inj_on f (vars_term l)" using Fun(3) subset_inj_on by blast
    with Fun(1,2) l have "linear_term (map_vars_term f l)" by auto
  }
  moreover have "is_partition (map (vars_term  map_vars_term f) ls)"
    using is_partition_inj_map[OF part, of f] Fun(3) by (simp add: o_def term.set_map)
  ultimately show ?case by auto
qed auto

lemma linear_term_replace_in_subst:
  assumes "linear_term t"
    and "p  poss t"
    and "t |_ p = Var x"
    and " y. y  vars_term t  y  x  σ y = τ y"
    and "τ x = s"
  shows "replace_at (t  σ) p s = t  τ"
  using assms
proof (induct p arbitrary: t)
  case (Cons i p t)
  then obtain f ts where t [simp]: "t = Fun f ts" and i: "i < length ts" and p: "p  poss (ts ! i)"
    by (cases t) auto
  from Cons have "linear_term (ts ! i)" and "ts ! i |_ p = Var x" by auto
  have id: "replace_at (ts ! i  σ) p (τ x) = ts ! i  τ" using Cons by force
  let ?l = " (take i (map (λt. t  σ) ts) @ (ts ! i  τ) # drop (Suc i) (map (λt. t  σ) ts))"
  from i have len: "length ts = length ?l" by auto
  { fix j
    assume j: "j < length ts"
    have "ts ! j  τ = ?l ! j"
    proof (cases "j = i")
      case True
      with i show ?thesis by (auto simp: nth_append)
    next
      case False
      let ?ts = "map (λt. t  σ) ts"
      from i j have le:"j  length ?ts" "i  length ?ts" by auto
      from nth_append_take_drop_is_nth_conv[OF le] False have "?l ! j = ?ts ! j" by simp
      also have "... = ts ! j  σ" using j by simp
      also have "... = ts ! j  τ"
      proof (rule term_subst_eq)
        fix y
        assume y: "y  vars_term (ts ! j)"
        from p have "ts ! i  ts ! i |_ p" by (rule subt_at_imp_supteq)
        then have x: "x  vars_term (ts ! i)" using ts ! i |_ p = Var x
          by (auto intro: subteq_Var_imp_in_vars_term)
        from Cons(2) have "is_partition (map vars_term ts)" by simp
        from this[unfolded is_partition_alt is_partition_alt_def, rule_format] j i False
        have "vars_term (ts ! i)  vars_term (ts ! j) = {}" by auto
        with y x have "y  x" by auto
        with Cons(5) y j show "σ y = τ y" by force
      qed
      finally show ?thesis by simp
    qed
  }
  then show ?case
    by (auto simp: τ x = s[symmetric] id nth_map[OF i, of "λt. t  σ"])
      (metis len map_nth_eq_conv[OF len])
qed auto


lemma var_in_linear_args:
  assumes "linear_term (Fun f ts)"
    and "i < length ts" and "x  vars_term (ts!i)" and "j < length ts  j  i"
  shows "x  vars_term (ts!j)"
proof-
  from assms(1) have "is_partition (map vars_term ts)"
    by simp
  with assms show ?thesis unfolding is_partition_alt is_partition_alt_def
    by auto 
qed

lemma subt_at_linear:
  assumes "linear_term t" and "p  poss t"
  shows "linear_term (t|_p)"
  using assms proof(induct p arbitrary:t)
  case (Cons i p)
  then obtain f ts where f:"t = Fun f ts" and i:"i < length ts" and p:"p  poss (ts!i)"
    by (meson args_poss)
  with Cons(2) have "linear_term (ts!i)"
    by force
  then show ?case
    unfolding f subt_at.simps using Cons.hyps p by blast
qed simp

lemma linear_subterms_disjoint_vars:
  assumes "linear_term t"
    and "p  poss t" and "q  poss t" and "p  q"
  shows "vars_term (t|_p)  vars_term (t|_q) = {}"
  using assms proof(induct t arbitrary: p q)
  case (Fun f ts)
  from Fun(3,5) obtain i p' where i:"i < length ts" "p'  poss (ts!i)" and p:"p = i#p'"
    by auto 
  with Fun(4,5) obtain j q' where j:"j < length ts" "q'  poss (ts!j)" and q:"q = j#q'"
    by auto 
  then show ?case proof(cases "i=j")
    case True
    from Fun(5) have "p'  q'" 
      unfolding p q True by simp
    with Fun(1,2) i j have "vars_term ((ts!j) |_ p')  vars_term ((ts!j) |_ q') = {}" 
      unfolding True by auto 
    then show ?thesis unfolding p q subt_at.simps True by simp
  next
    case False
    from i have "vars_term ((Fun f ts)|_p)  vars_term (ts!i)" 
      unfolding p subt_at.simps by (simp add: vars_term_subt_at) 
    moreover from j have "vars_term ((Fun f ts)|_q)  vars_term (ts!j)" 
      unfolding q subt_at.simps by (simp add: vars_term_subt_at) 
    ultimately show ?thesis using False Fun(2) i j
      by (meson disjoint_iff subsetD var_in_linear_args)
  qed
qed simp

lemma ground_imp_linear_term [simp]: "ground t  linear_term t"
  by (induct t) (auto simp add: is_partition_def ground_vars_term_empty)

text ‹exhaustively apply several maps on function symbols›
fun map_funs_term_enum :: "('f  'g list)  ('f, 'v) term  ('g, 'v) term list"
where
  "map_funs_term_enum fgs (Var x) = [Var x]" |
  "map_funs_term_enum fgs (Fun f ts) = (
    let
      lts = map (map_funs_term_enum fgs) ts;
      ss = concat_lists lts;
      gs = fgs f
    in concat (map (λg. map (Fun g) ss) gs))"


lemma map_funs_term_enum:
  assumes gf: " f g. g  set (fgs f)  gf g = f"
  shows "set (map_funs_term_enum fgs t) = {u. map_funs_term gf u = t  (g n. (g,n)  funas_term u  g  set (fgs (gf g)))}"
proof (induct t)
  case (Var x)
  show ?case (is "_ = ?R")
  proof -
    {
      fix t
      assume "t  ?R"
      then have "t = Var x" by (cases t, auto)
    }
    then show ?thesis by auto
  qed
next
  case (Fun f ts)
  show ?case (is "?L = ?R")
  proof -
    {
      fix i
      assume "i < length ts"
      then have "ts ! i  set ts" by auto
      note Fun[OF this]
    } note ind = this
    let ?cf = "λ u. (g n. (g,n)  funas_term u  g  set (fgs (gf g)))"
    have id: "?L = {Fun g ss | g ss. g  set (fgs f)  length ss = length ts  (i<length ts. ss ! i  set (map_funs_term_enum fgs (ts ! i)))}" (is "_ = ?M1") by auto
    have "?R = {Fun g ss | g ss. map_funs_term gf (Fun g ss) = Fun f ts  ?cf (Fun g ss)}" (is "_ = ?M2")
    proof -
      {
        fix u
        assume u: "u  ?R"
        then obtain g ss where "u = Fun g ss" by (cases u, auto)
        with u have "u  ?M2" by auto
      }
      then have "?R  ?M2" by auto
      moreover have "?M2  ?R" by blast
      finally show ?thesis by auto
    qed
    also have "... = ?M1"
    proof -
      {
        fix u
        assume "u  ?M1"
        then obtain g ss where u: "u = Fun g ss" and g: "g  set (fgs f)" and
          len: "length ss = length ts" and rec: " i. i < length ts  ss ! i  set (map_funs_term_enum fgs (ts ! i))" by auto
        from gf[OF g] have gf: "gf g = f" by simp
        {
          fix i
          assume i: "i < length ts"
          from ind[OF i] rec[OF i]
          have "map_funs_term gf (ss ! i) = ts ! i" by auto
        } note ssts = this
        have "map (map_funs_term gf) ss = ts"
          by (unfold map_nth_eq_conv[OF len], insert ssts, auto)
        with gf
        have mt: "map_funs_term gf (Fun g ss) = Fun f ts" by auto
        have "u  ?M2"
        proof (rule, rule, rule, rule, rule u, rule, rule mt, intro allI impI)
          fix h n
          assume h: "(h,n)  funas_term (Fun g ss)"
          show "h  set (fgs (gf h))"
          proof (cases "(h,n) = (g,length ss)")
            case True
            then have "h = g" by auto
            with g gf show ?thesis by auto
          next
            case False
            with h obtain s where s: "s  set ss" and h: "(h,n)  funas_term s" by auto
            from s[unfolded set_conv_nth] obtain i where i: "i < length ss" and si: "s = ss ! i" by force
            from i len have i': "i < length ts" by auto
            from ind[OF i'] rec[OF i'] h[unfolded si] show ?thesis by auto
          qed
        qed
      }
      then have m1m2: "?M1  ?M2" by blast
      {
        fix u
        assume u: "u  ?M2"
        then obtain g ss where u: "u = Fun g ss"
          and map: "map_funs_term gf (Fun g ss) = Fun f ts"
          and c: "?cf (Fun g ss)"
          by blast
        from map have len: "length ss = length ts" by auto
        from map have g: "gf g = f" by auto
        from map have map: "map (map_funs_term gf) ss = ts" by auto
        from c have g2: "g  set (fgs f)" using g by auto
        have "u  ?M1"
        proof (intro CollectI exI conjI allI impI, rule u, rule g2, rule len)
          fix i
          assume i: "i < length ts"
          with map[unfolded map_nth_eq_conv[OF len]]
          have id: "map_funs_term gf (ss ! i) = ts ! i" by auto
          from i len have si: "ss ! i  set ss" by auto
          show "ss ! i  set (map_funs_term_enum fgs (ts ! i))"
            unfolding ind[OF i]
          proof (intro CollectI conjI impI allI, rule id)
            fix g n
            assume "(g,n)  funas_term (ss ! i)"
            with c si
            show "g  set (fgs (gf g))" by auto
          qed
        qed
      }
      then have m2m1: "?M2  ?M1" by blast
      show "?M2 = ?M1"
        by (rule, rule m2m1, rule m1m2)
    qed
    finally show ?case unfolding id by simp
  qed
qed

declare map_funs_term_enum.simps[simp del]

end