Theory Basic_Utils

text ‹Trivialities›
theory Basic_Utils
  imports TRS.Trs Deriving.Compare_Order_Instances TRS.Multihole_Context
begin

lemma map_prod_times:
  "f ` A × g ` B = map_prod f g ` (A × B)"
  by auto

definition filter_rev_nth where
  "filter_rev_nth P xs i = length (filter P (take (Suc i) xs)) - 1"

lemma filter_rev_nth_butlast:
  "¬ P (last xs) ⟹ filter_rev_nth P xs i = filter_rev_nth P (butlast xs) i"
  unfolding filter_rev_nth_def
  by (induct xs arbitrary: i rule: rev_induct) (auto simp add: take_Cons')

lemma filter_rev_nth_idx:
  assumes "i < length xs" "P (xs ! i)" "ys = filter P xs"
  shows "xs ! i = ys ! (filter_rev_nth P xs i) ∧ filter_rev_nth P xs i < length ys"
  using assms unfolding filter_rev_nth_def
proof (induct xs arbitrary: ys i)
  case (Cons x xs) show ?case
  proof (cases "P x")
    case True
    then obtain ys' where *:"ys = x # ys'" using Cons(4) by auto
    show ?thesis using True Cons(1)[of "i - 1" ys'] Cons(2-)
      unfolding *
      by (cases i) (auto simp: nth_Cons' take_Suc_conv_app_nth)
  next
    case False
    then show ?thesis using Cons(1)[of "i - 1" ys] Cons(2-)
      by (auto simp: nth_Cons')
  qed
qed auto

(* Recursive definition of subterm equivalence *)
fun subterms where
  "subterms (Var x) = {Var x}"
| "subterms (Fun f ts) = {Fun f ts} ∪ (⋃ (subterms ` set ts))"

lemma finite_subterms_fun: "finite (subterms s)"
  by (induct s) auto

lemma subterms_supteq_conv:
  "t ∈ subterms s ⟷ s ⊵ t"
  by (induct s arbitrary: t) (auto simp add: Fun_supteq)

lemma set_all_subteq_subterms:
  "subterms s = {t | t. s ⊵ t}"
  using subterms_supteq_conv
  by auto

lemma root_substerms_funas_term:
  "the ` (root ` (subterms s) - {None}) = funas_term s" (is "?Ls = ?Rs")
proof -
  thm subterms.induct
  {fix x assume "x ∈ ?Ls" then have "x ∈ ?Rs"
    proof (induct s arbitrary: x)
      case (Fun f ts)
      then show ?case
        by auto (metis DiffI Fun.hyps imageI option.distinct(1) singletonD) 
    qed auto}
  moreover
  {fix x assume "x ∈ ?Rs" then have "x ∈ ?Ls"
    proof (induct s arbitrary: x)
      case (Fun f ts)
      then show ?case
        apply (auto simp: image_iff)
        apply (metis DiffI insertI1 option.sel option.simps(3) singletonD)
        by (smt DiffE DiffI Fun.hyps UN_I image_iff insertCI)
    qed auto}
  ultimately show ?thesis by auto
qed

lemma root_substerms_funas_term_set:
  "the ` (root ` ⋃ (subterms ` R) - {None}) = ⋃ (funas_term ` R)"
  using root_substerms_funas_term
  by auto (smt DiffE DiffI UN_I image_iff)

(* Computing list of all permutations of elements of a given set *)

fun list_of_permutation_n where
  "list_of_permutation_n S 0 = [[]]" |
  "list_of_permutation_n S (Suc n) = (let pre = (list_of_permutation_n S n) in
    concat (map (λ x. (map (λ y. x # y) pre)) S))"

lemma list_fun_sym_eq_set_cons_l:
  assumes "x ∈ {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  shows "x ∈ set (list_of_permutation_n L n)"
  using assms
proof (induct n arbitrary: x)
  case (Suc n)
  then obtain f s where x: "x = f # s" and "f ∈ set L"
    by auto (metis Suc_length_conv nth_Cons_0 zero_less_Suc)
  then have "s ∈ set (list_of_permutation_n L n)" using Suc(1,2) by auto fastforce
  then show ?case using x ‹f ∈ set L› by auto 
qed auto

lemma list_fun_sym_eq_set_cons_r:
  assumes "x ∈ set (list_of_permutation_n L n)"
  shows "x ∈ {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  using assms by (induct n arbitrary: x) (auto simp add: nth_Cons')

lemma list_fun_sym_eq_set:
  shows "set (list_of_permutation_n L n) = {gs. length gs = n ∧ (∀ i < n. gs ! i ∈ set L)}"
  using list_fun_sym_eq_set_cons_l list_fun_sym_eq_set_cons_r by blast

lemma list_fun_length_n [elim]:
  assumes "x ∈ set (list_of_permutation_n L n)"
  shows "length x = n"
  using assms list_fun_sym_eq_set_cons_r by blast

primrec add_elem_list_lists :: "'a ⇒ 'a list ⇒ 'a list list" where
  "add_elem_list_lists x [] = [[x]]"
| "add_elem_list_lists x (y # ys) = (x # y # ys) # (map ((#) y) (add_elem_list_lists x ys))"

lemma length_add_elem_list_lists:
  "ys ∈ set (add_elem_list_lists x xs) ⟹ length ys = Suc (length xs)"
  by (induct xs arbitrary: ys) auto

lemma add_elem_list_listsE:
  assumes "ys ∈ set (add_elem_list_lists x xs)"
  shows "∃ n ≤ length xs. ys = take n xs @ x # drop n xs" using assms
proof(induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by auto fastforce
qed auto

lemma add_elem_list_listsI:
  assumes "n ≤ length xs" "ys = take n xs @ x # drop n xs"
  shows "ys ∈ set (add_elem_list_lists x xs)" using assms
proof  (induct xs arbitrary: ys n)
  case (Cons a xs)
  then show ?case
    by (cases n) (auto simp: image_iff) 
qed auto

lemma add_elem_list_lists_def':
  "set (add_elem_list_lists x xs) = {ys | ys n. n ≤ length xs ∧ ys = take n xs @ x # drop n xs}"
  using add_elem_list_listsI add_elem_list_listsE
  by fastforce

fun list_of_permutation_element_n :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list list" where
  "list_of_permutation_element_n x 0 L = [[]]"
|  "list_of_permutation_element_n x (Suc n) L = concat (map (add_elem_list_lists x) (list_of_permutation_n L n))"

lemma list_of_permutation_element_n_conv:
  assumes "n ≠ 0"
  shows "set (list_of_permutation_element_n x n L) =
    {xs | xs i. i < length xs ∧ (∀ j < length xs. j ≠ i ⟶ xs ! j ∈ set L) ∧ length xs = n ∧ xs ! i = x}" (is "?Ls = ?Rs")
proof (intro equalityI)
  from assms obtain j where [simp]: "n = Suc j" using assms by (cases n) auto
  {fix ys assume "ys ∈ ?Ls"
    then obtain xs i where wit: "xs ∈ set (list_of_permutation_n L j)" "i ≤ length xs"
      "ys = take i xs @ x # drop i xs"
      by (auto dest: add_elem_list_listsE)
    then have "i < length ys" "length ys = Suc (length xs)" "ys ! i = x"
      by (auto simp: nth_append)
    moreover have "∀ j < length ys. j ≠ i ⟶ ys ! j ∈ set L" using wit(1, 2)
      by (auto simp: list_fun_sym_eq_set wit(3) min_def nth_append)
    ultimately have "ys ∈ ?Rs" using wit(1)
      by auto}
  then show "?Ls ⊆ ?Rs" by blast
next
  {fix xs assume "xs ∈ ?Rs"
    then obtain i where wit: "i < length xs" "∀ j < length xs. j ≠ i ⟶ xs ! j ∈ set L"
      "length xs = n" "xs ! i = x"
      by blast
    then have *: "xs ∈ set (add_elem_list_lists (xs ! i) (take i xs @ drop (Suc i) xs))"
      unfolding add_elem_list_lists_def'
      by (auto simp: min_def intro!: nth_equalityI)
         (metis Cons_nth_drop_Suc Suc_pred append_Nil append_take_drop_id assms diff_le_self diff_self_eq_0 drop_take less_Suc_eq_le nat_less_le take0)
    have "xs ∈ ?Ls" using wit
      by (cases "length xs")
         (auto simp: list_fun_sym_eq_set nth_append *
               intro!: exI[of _ "take i xs @ drop (Suc i) xs"])}
  then show "?Rs ⊆ ?Ls" by blast
qed

lemma list_of_permutation_element_n_conv':
  assumes "x ∈ set L" "0 < n"
  shows "set (list_of_permutation_element_n x n L) =
      {xs. set xs ⊆ insert x (set L) ∧ length xs = n ∧ x ∈ set xs}"
proof -
  from assms(2) have *: "n ≠ 0" by simp
  show ?thesis using assms in_set_idx
    unfolding list_of_permutation_element_n_conv[OF *]
    by force
qed

section ‹we require a function which adapts the type of variables of a term,
   so that states of the automaton and variables in the term language can be
   chosen independently›

definition adapt_vars :: "('f,'q)term ⇒ ('f,'v)term" where 
  [code del]: "adapt_vars ≡ map_vars_term (λ_. undefined)"

lemma adapt_vars2:
  "adapt_vars (adapt_vars t) = adapt_vars t"
  by (induct t) (auto simp add: adapt_vars_def)

lemma adapt_vars_simps[code, simp]: "adapt_vars (Fun f ts) = Fun f (map adapt_vars ts)"
  by (induct ts, auto simp: adapt_vars_def)

lemma adapt_vars_reverse: "ground t ⟹ adapt_vars t' = t ⟹ adapt_vars t = t'"
  unfolding adapt_vars_def 
proof (induct t arbitrary: t')
  case (Fun f ts)
  then show ?case by (cases t') (auto simp add: map_vars_term_as_subst map_idI)
qed auto

lemma ground_adapt_vars[simp]: "ground (adapt_vars t) = ground t" by (simp add: adapt_vars_def)
lemma funas_term_adapt_vars[simp]: "funas_term (adapt_vars t) = funas_term t" by (simp add: adapt_vars_def)

lemma adapt_vars_adapt_vars[simp]: fixes t :: "('f,'v)term"
  assumes g: "ground t"
  shows "adapt_vars (adapt_vars t :: ('f,'w)term) = t"
proof -
  let ?t' = "adapt_vars t :: ('f,'w)term"
  have gt': "ground ?t'" using g by auto
  from adapt_vars_reverse[OF gt', of t] show ?thesis by blast
qed

lemma adapt_vars_inj:
  assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
  shows "x = y"
  using adapt_vars_adapt_vars assms by metis

definition adapt_vars_ctxt :: "('f,'q)ctxt ⇒ ('f,'v)ctxt" where
  [code del]: "adapt_vars_ctxt = map_vars_ctxt (λ_. undefined)"

lemma adapt_vars_ctxt_simps[simp, code]: 
  "adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"
  "adapt_vars_ctxt Hole = Hole" unfolding adapt_vars_ctxt_def adapt_vars_def by auto

lemma adapt_vars_ctxt[simp]: "adapt_vars (C ⟨ t ⟩ ) = (adapt_vars_ctxt C) ⟨ adapt_vars t ⟩"
  by (induct C, auto)

lemma adapt_vars_subst[simp]: "adapt_vars (l ⋅ σ) = l ⋅ (λ x. adapt_vars (σ x))"
  unfolding adapt_vars_def by simp


(* Move to  Transitive_Closure *)
(* Id constructs an infinite set if the underlying type is not finite,
hence not suitable for FSet *)
lemma ntrancl_Suc' [simp]: "ntrancl (Suc n) R = ntrancl n R ∪ (ntrancl n R O R)" (is "?Ls = ?Rs")
proof
  have "(a, b) ∈ ?Rs" if "(a, b) ∈ ntrancl (Suc n) R" for a b
  proof -
    from that obtain i where "0 < i" "i ≤ Suc (Suc n)" "(a, b) ∈ R ^^ i"
      unfolding ntrancl_def by auto
    show ?thesis
    proof (cases "i = 1")
      case True
      from this ‹(a, b) ∈ R ^^ i› show ?thesis
        by (auto simp: ntrancl_def)
    next
      case False
      with ‹0 < i› obtain j where j: "i = Suc j" "0 < j"
        by (cases i) auto
      with ‹(a, b) ∈ R ^^ i› obtain c where c1: "(a, c) ∈ R ^^ j" and c2: "(c, b) ∈ R"
        by auto
      from c1 j ‹i ≤ Suc (Suc n)› have "(a, c) ∈ ntrancl n R"
        by (fastforce simp: ntrancl_def)
      with c2 show ?thesis by fastforce
    qed
  qed
  then show "ntrancl (Suc n) R ⊆ ?Rs"
    by auto
  show "?Rs ⊆ ntrancl (Suc n) R"
    by (fastforce simp: ntrancl_def)
qed

(* Misc *)
lemma term_idx_induct:
  assumes "⋀x. P (Var x)"
    and "⋀ f ts. (⋀ i. i < length ts ⟹ P (ts ! i)) ⟹ P (Fun f ts)"
  shows "P t" using assms
  by (induct t) auto

(* Isabelles documentation needs quite a lot of updates

instantiation set :: (linorder) linorder
begin
definition less_eq_set
  where "A < B ⟷ (λx. x ∈ A) ≤ (λx. x ∈ B)"
instance proof
end
*)

lemma nempty_list_ex [simp]:
  "Ds ≠ [] ⟹ ∃D. D ∈ set Ds"
  by (cases Ds) auto

fun nthWhile :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
  "nthWhile P [] = 0"
| "nthWhile P (x # xs) = (if P x then 1 + nthWhile P xs else 0)"

lemma nthWhile_cong [fundef_cong]:
  "l = k ⟹ (⋀ x. x ∈ set l ⟹ P x = Q x) ⟹ nthWhile P l = nthWhile Q k"
  by (induct k arbitrary: l) (simp_all)

lemma nthWhile_takeWhile_conv:
  "take (nthWhile P xs) xs = takeWhile P xs"
  by (induct xs) auto

lemma nthWhile_length [simp]:
  "nthWhile P xs ≤ length xs"
  by (induct xs) auto

lemma nthWhile_p [simp]:
  "nthWhile P xs < length xs ⟹ ¬ P (xs ! nthWhile P xs)"
  by (induct xs) auto

lemma set_take_nth_conv:
  assumes "s ∈ set (take i ps)" "i < length ps"
  obtains n where "s = ps ! n" "n ≠ i" "n < length ps"
  using assms by (auto simp: in_set_conv_nth)

lemma set_drop_nth_conv:
  assumes "s ∈ set (drop (Suc i) ps)" "i < length ps"
  obtains n where "s = ps ! n" "n ≠ i" "n < length ps"
  using assms by (auto simp: in_set_conv_nth)

lemma subseteq_set_conv_nth:
  "(∀ i < length ss. ss ! i ∈ T) ⟷ set ss ⊆ T"
  by (metis in_set_conv_nth subset_code(1))

lemma nth_sum_listI:
  assumes "length xs = length ys"
    and "∀ i < length xs. xs ! i = ys ! i"
  shows "sum_list xs = sum_list ys"
  using assms nth_equalityI by blast

lemma sum_list_1_E [elim]:
  assumes "sum_list xs = Suc 0"
  obtains i where "i < length xs" "xs ! i = Suc 0" "∀ j < length xs. j ≠ i ⟶ xs ! j = 0"
proof -
  have "∃ i < length xs. xs ! i = Suc 0 ∧ (∀ j < length xs. j ≠ i ⟶ xs ! j = 0)" using assms
  proof (induct xs)
    case (Cons a xs) show ?case
    proof (cases a)
      case [simp]: 0
      obtain i where "i < length xs" "xs ! i = Suc 0" "(∀ j < length xs. j ≠ i ⟶ xs ! j = 0)"
        using Cons by auto
      then show ?thesis using less_Suc_eq_0_disj
        by (intro exI[of _ "Suc i"]) auto
    next
      case (Suc nat) then show ?thesis using Cons by auto
    qed
  qed auto
  then show " (⋀i. i < length xs ⟹ xs ! i = Suc 0 ⟹ ∀j<length xs. j ≠ i ⟶ xs ! j = 0 ⟹ thesis) ⟹ thesis"
    by blast
qed

lemma sum_list_replicate_greater_zero [simp]:
  "0 < n ⟹ 0 < sum_list (replicate n (Suc 0))"
  by (metis length_replicate sum_list_replicate_length)

lemma concat_nth_nthI:
  assumes "length ss = length ts" "∀ i < length ts. length (ss ! i) = length (ts ! i)"
    and "∀ i < length ts. ∀ j < length (ts ! i). P (ss ! i ! j) (ts ! i ! j)"
  shows "∀ i < length (concat ts). P (concat ss ! i) (concat ts ! i)"
  using assms by (metis nth_concat_two_lists)

lemma last_nthI:
  assumes "i < length ts" "¬ i < length ts - Suc 0"
  shows "ts ! i = last ts" using assms
  by (induct ts arbitrary: i)
    (auto, metis last_conv_nth length_0_conv less_antisym nth_Cons')

(* induction scheme for transitive closures of lists *)

forℛ">inductive_set trancl_list for ℛ where
  base[intro, Pure.intro] : "length xs = length ys ⟹
      (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ) ⟹ (xs, ys) ∈ trancl_list ℛ"
| list_trancl [Pure.intro]: "(xs, ys) ∈ trancl_list ℛ ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹
    (xs, ys[i := z]) ∈ trancl_list ℛ"

lemma trancl_list_appendI [simp, intro]:
  "(xs, ys) ∈ trancl_list ℛ ⟹ (x, y) ∈ ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ"
proof (induct rule: trancl_list.induct)
  case (base xs ys)
  then show ?case using less_Suc_eq_0_disj
    by (intro trancl_list.base) auto
next
  case (list_trancl xs ys i z)
  from list_trancl(3) have *: "y # ys[i := z] = (y # ys)[Suc i := z]" by auto
  show ?case using list_trancl unfolding *
    by (intro trancl_list.list_trancl) auto
qed

lemma trancl_list_append_tranclI [intro]:
  "(x, y) ∈ ℛ⇧+ ⟹ (xs, ys) ∈ trancl_list ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ"
proof (induct rule: trancl.induct)
  case (trancl_into_trancl a b c)
  then have "(a # xs, b # ys) ∈ trancl_list ℛ" by auto
  from trancl_list.list_trancl[OF this, of 0 c]
  show ?case using trancl_into_trancl(3)
    by auto
qed auto

lemma trancl_list_conv:
  "(xs, ys) ∈ trancl_list ℛ ⟷ length xs = length ys ∧ (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧+)" (is "?Ls ⟷ ?Rs")
proof
  assume "?Ls" then show ?Rs
  proof (induct)
    case (list_trancl xs ys i z)
    then show ?case
      by auto (metis nth_list_update trancl.trancl_into_trancl)
  qed auto
next
  assume ?Rs then show ?Ls
  proof (induct ys arbitrary: xs)
    case Nil
    then show ?case by (cases xs) auto
  next
    case (Cons y ys)
    from Cons(2) obtain x xs' where *: "xs = x # xs'" and
      inv: "(x, y) ∈ ℛ⇧+"
      by (cases xs) auto
    show ?case using Cons(1)[of "tl xs"] Cons(2) unfolding *
      by (intro trancl_list_append_tranclI[OF inv]) force
  qed
qed

lemma trancl_list_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧+"
   and "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys"
   and "⋀xs ys i z. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧+ ⟹ P xs ys
      ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹ P xs (ys[i := z])"
 shows "P ss ts" using assms
  by (intro trancl_list.induct[of ss ts ℛ P]) (auto simp: trancl_list_conv)

lemma trancl_list_all_step_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧+"
   and "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys"
   and "⋀xs ys zs. length xs = length ys ⟹ length ys = length zs ⟹
       ∀ i < length zs. (xs ! i, ys ! i) ∈ ℛ⇧+ ⟹ ∀ i < length zs. (ys ! i, zs ! i) ∈ ℛ ∨ ys ! i = zs ! i ⟹
       P xs ys ⟹ P xs zs"
 shows "P ss ts" using assms
  apply (intro trancl_list.induct[of ss ts ℛ P])
  apply (auto simp: trancl_list_conv)
  by (metis length_list_update nth_list_update_eq nth_list_update_neq)

(** REFACTOR ALL FROM HERE *)
(********************************* TO MOVE SECTION **************************)
lemma insert_id_rtrancl [simp]:
  "(insert (r, r) 𝒜)⇧* = 𝒜⇧*"
  by (simp add: r_into_rtrancl rtrancl_subset subset_eq)

lemma map_mctxt_comp [simp]:
  "map_mctxt f (map_mctxt g C) = map_mctxt (f ∘ g) C"
  by (induct C) auto

lemma funas_mctxt_split_vars_funas_term [simp]:
  "funas_mctxt (fst (split_vars s)) = funas_term s"
  by (induct s) auto

lemma map_funs_ctxt_empty:
  "map_funs_ctxt f C = □ ⟹ C = □"
  by (cases C) auto

lemma map_funs_mctxt_empty:
  "map_mctxt f C = MHole ⟹ C = MHole"
  by (cases C) auto

lemma ground_map_funs_ctxt [simp]:
  "ground_ctxt C ⟹ ground_ctxt (map_funs_ctxt f C)"
  by (induct C) auto

lemma map_funs_term_map_funs_term [simp]:
  "map_funs_term f (map_funs_term g t) = map_funs_term (f ∘ g) t"
  by (induct t) auto

lemma map_funs_ctxt_map_funs_ctxt [simp]:
  "map_funs_ctxt f (map_funs_ctxt g C) = map_funs_ctxt (f ∘ g) C"
  by (induct C) (auto simp: comp_def) 

lemma split_vars_fill_holes:
  assumes "C = fst (split_vars s)" and "ss = map Var (snd (split_vars s))"
  shows "fill_holes C ss = s" using assms
  by (metis eqfE(1) split_vars_eqf_subst subst_apply_term_empty)

lemma split_vars_ground'[simp]:
  "ground_mctxt (fst (split_vars s))"
  using prod.exhaust_sel split_vars_ground by blast


lemma trancl_singelton [simp]:
  "{q}⇧+ = {q}"
proof -
  {fix x y assume "(x, y) ∈ {q}⇧+" then have "(x, y) ∈ {q}"
      by induct auto}
  then show ?thesis by auto
qed


lemma rtrancl_Un2_separatorE:
  "B O A = {} ⟹ (A ∪ B)⇧* = A⇧* ∪ A⇧* O B⇧*"
  by (metis R_O_Id empty_subsetI relcomp_distrib rtrancl_U_push rtrancl_reflcl_absorb sup_commute)

lemma trancl_Un2_separatorE:
  assumes "B O A = {}"
  shows "(A ∪ B)⇧+ = A⇧+ ∪ A⇧+ O B⇧+ ∪ B⇧+" (is "?Ls = ?Rs")
proof -
  {fix x y assume "(x, y) ∈ ?Ls"
    then have "(x, y) ∈ ?Rs" using assms
    proof (induct)
      case (step y z)
      then show ?case
        by (auto simp add: trancl_into_trancl relcomp_unfold dest: tranclD2)
    qed auto}
  then show ?thesis
    by (auto simp add: trancl_mono)
       (meson sup_ge1 sup_ge2 trancl_mono trancl_trans)
qed


lemma rel_comp_empty_trancl_simp: "R O R = {} ⟹ R⇧+ = R"
  by (metis O_assoc relcomp_empty2 sup_bot_right trancl_unfold trancl_unfold_right)

lemma choice_nat:
  assumes "∀i<n. ∃x. P x i"
  shows "∃f. ∀x<n. P (f x) x" using assms 
proof -
  from assms have "∀ i. ∃ x. i < n ⟶ P x i" by simp
  from choice[OF this] show ?thesis by auto
qed


lemma sum_list_drop:
  assumes "sum_list (x # xs) = length ys"
  shows "sum_list xs = length (drop x ys)"
  using assms by (induct xs arbitrary: ys) auto

lemma sum_list_relativ_idx_length:
  assumes "sum_list xs = length ys"
    and "i < length xs" and "sum_list (drop i xs) > 0"
  shows "sum_list (take i xs) < length ys"
  using assms
proof (induction xs arbitrary: ys)
  case (Cons x xs)
  then show ?case
    by (cases i, auto) (metis add_strict_left_mono append_take_drop_id less_add_same_cancel1 sum_list.append)
qed auto

lemma sum_list_drop_greater_nth:
  assumes "i < length (xs :: nat list)"
  shows "xs ! i ≤ sum_list (drop i xs)"
  using assms
proof (induct xs arbitrary: i)
  case (Cons a xs)
  then show ?case by (cases i) auto
qed auto

lemma take1_drop:
  assumes "sum_list (take i ys) < length xs"
  shows "take (Suc 0) (drop (sum_list (take i ys)) xs) = [xs ! (sum_list (take i ys))]"
  using assms by (metis Cons_nth_drop_Suc take0 take_Suc_Cons)

lemma fill_holes_MHole2 [simp]:
  assumes "sum_list (map num_holes cs) = length ss" and "i < length cs" and "cs ! i = MHole"
  shows "fill_holes (cs ! i) (partition_holes ss cs ! i) = ss ! (sum_list (take i (map num_holes cs)))"
  using assms sum_list_drop_greater_nth[of i "map num_holes cs"] partition_by_nth[of i "map num_holes cs" ss]
  using sum_list_relativ_idx_length[OF assms(1), of i]
  by (auto simp: take1_drop)

lemma fill_holes_MHole_length:
  assumes "sum_list (map num_holes cs) = length ss" and "i < length cs" and "cs ! i = MHole"
  shows "sum_list (take i (map num_holes cs)) < length ss"
  using assms sum_list_drop_greater_nth[of i "map num_holes cs"]
  using sum_list_relativ_idx_length[OF assms(1)]
  by auto

lemma gmctxt_no_holes_gterm:
  assumes "num_holes C = 0" and "ground_mctxt C"
  shows "ground (term_of_mctxt C)"
  using assms by (induct C) auto

lemma fill_holes_empty_id [simp]:
  assumes "num_holes C = 0"
  shows "fill_holes C [] = term_of_mctxt C"
  using assms by (metis mctxt_of_term_fill_holes mctxt_of_term_term_of_mctxt_id)

lemma map_append_Cons:
  "(map f xs @ f x # map f ys) = map f (xs @ x # ys)"
  by simp

lemma map_append_Cons_nth:
  assumes "i < Suc (length xs + length ys)"
  shows "(map f xs @ f x # map f ys) ! i = f ((xs @ x # ys) ! i)"
  using assms by (auto simp: nth_append_Cons)

(********************************* Support for sum types ********************************)

primrec is_Inl where
  "is_Inl (Inl q) ⟷ True"
| "is_Inl (Inr q) ⟷ False"

primrec is_Inr where
  "is_Inr (Inr q) ⟷ True"
| "is_Inr (Inl q) ⟷ False"

lemma is_InrE:
  assumes "is_Inr q"
  obtains p where "q = Inr p"
  using assms by (cases q) auto

lemma is_InlE:
  assumes "is_Inl q"
  obtains p where "q = Inl p"
  using assms by (cases q) auto

lemma not_is_Inr_is_Inl [simp]:
  "¬ is_Inl t ⟷ is_Inr t"
  "¬ is_Inr t ⟷ is_Inl t"
  by (cases t, auto)+

fun remove_sum where
  "remove_sum (Inl q) = q"
|"remove_sum (Inr q) = q"

lemma [simp]: "remove_sum ∘ Inl = id" by auto

abbreviation CInl :: "'q ⇒ 'q + 'q" where "CInl ≡ Inl"
abbreviation CInr :: "'q ⇒ 'q + 'q" where "CInr ≡ Inr"

lemma inj_CInl: "inj CInl" "inj CInr" using inj_Inl inj_Inr by blast+

lemma map_prod_simp': "map_prod f g G = (f (fst G), g (snd G))"
  by (auto simp add: map_prod_def split!: prod.splits)


(********************************* FINISHED THE TO MOVE SECTION **************************)

lemmas construct_exI' = Ex_list_of_length_P

lemma construct_exI'_double:
  assumes "∀i < n. ∃x y. P x y i"
  shows "∃xs ys. length xs = n ∧ length ys = n ∧ (∀i < n. P (xs ! i) (ys ! i) i)"
proof -
  from assms obtain f g where "P (f i) (g i) i" if "i < n" for i using assms by metis
  then show ?thesis by (intro exI[of _ "map _ [0..<n]"]) auto
qed

lemma construct_exI'_quadraple:
  assumes "∀i < n. ∃x y z w. P x y z w i"
  shows "∃xs ys zs ws. length xs = n ∧ length ys = n ∧  length zs = n ∧  length ws = n 
  ∧ (∀i < n. P (xs ! i) (ys ! i) (zs!i) (ws!i) i)"
proof -
  from assms obtain f1 f2 f3 f4 where "P (f1 i) (f2 i) (f3 i) (f4 i) i" if "i < n" for i using assms 
    by metis
  then show ?thesis by (intro exI[of _ "map _ [0..<n]"]) auto
qed


(* TODO: check whether this is still needed *)
lemma construct_exI:
  assumes "∀i < n. ∃xs. P (xs ! i) i"
  shows "∃xs. length xs = n ∧ (∀i < n. P (xs ! i) i)"
proof -
  guess xss using construct_exI'[OF assms] by (elim exE)
  then show ?thesis by (intro exI[of _ "map (λi. xss ! i ! i) [0..<n]"]) auto
qed

definition right_ground_trs :: "('f, 'v) trs ⇒ bool" where
  "right_ground_trs R ≡ ∀(l, r) ∈ R. ground r"

definition ground_trs :: "('f, 'v) trs ⇒ bool" where
  "ground_trs R ≡ ∀(l, r) ∈ R. ground l ∧ ground r"

lemma ground_imp_right_ground_trs [simp]:
  "ground_trs R ⟹ right_ground_trs R"
  unfolding ground_trs_def right_ground_trs_def by fast

definition set_to_list :: "'a set ⇒ 'a list"
  where "set_to_list s = (SOME l. set l = s)"

lemma set_set_to_list:
  "finite s ⟹ set (set_to_list s) = s"
  unfolding set_to_list_def by (metis (mono_tags) finite_list some_eq_ex)

lemma trancl_full_on:
  "(X × X)⇧+ = X × X"
  using trancl_unfold_left[of "X × X"] trancl_unfold_right[of "X × X"] by auto

lemma Restr_simps:
  "R ⊆ X × X ⟹ Restr (R⇧+) X = R⇧+"
  "R ⊆ X × X ⟹ Restr Id X O R = R"
  "R ⊆ X × X ⟹ R O Restr Id X = R"
  "R ⊆ X × X ⟹ S ⊆ X × X ⟹ Restr (R O S) X = R O S"
  "R ⊆ X × X ⟹ R⇧+ ⊆ X × X"
  subgoal using trancl_mono_set[of R "X × X"] by (auto simp: trancl_full_on)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal using trancl_subset_Sigma .
  done


lemma Restr_tracl_comp_simps:
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ⇧+ O ℛ ⊆ X × X"
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ O ℛ⇧+ ⊆ X × X"
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ⇧+ O ℛ O ℒ⇧+ ⊆ X × X"
  by (auto dest: subsetD[OF Restr_simps(5)[of ℒ]] subsetD[OF Restr_simps(5)[of ℛ]])

lemma Restr_rtracl_comp_simps:
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ⇧* O ℛ ⊆ X × X"
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ O ℛ⇧* ⊆ X × X"
  "ℛ ⊆ X × X ⟹ ℒ ⊆ X × X ⟹ ℒ⇧* O ℛ O ℒ⇧* ⊆ X × X"
  by (auto simp: rtrancl_eq_or_trancl dest:
    subsetD[OF Restr_simps(5)[of ℒ]] subsetD[OF Restr_simps(5)[of ℛ]])

lemma trancl_absorb [simp]: "(ℛ⇧+)⇧+ = ℛ⇧+"
  using trancl_id trans_trancl by blast

lemma inj_on_by_inj:
  "inj f ⟹ inj_on f X"
  unfolding inj_on_def by auto

lemma kleene_induct:
  "A ⊆ X ⟹ B O X ⊆ X ⟹ X O C ⊆ X ⟹ B⇧* O A O C⇧* ⊆ X"
  using relcomp_mono[OF compat_tr_compat[of B X] subset_refl, of "C⇧*"] compat_tr_compat[of "C¯" "X¯"]
    relcomp_mono[OF relcomp_mono, OF subset_refl _ subset_refl, of A X "B⇧*" "C⇧*"]
  unfolding rtrancl_converse converse_relcomp[symmetric] converse_mono by blast

lemma kleene_trancl_induct:
  "A ⊆ X ⟹ B O X ⊆ X ⟹ X O C ⊆ X ⟹ B⇧+ O A O C⇧+ ⊆ X"
  using kleene_induct[of A X B C]
  by (auto simp: rtrancl_eq_or_trancl)
     (meson relcomp.relcompI subsetD trancl_into_rtrancl)

lemma swap_trancl:
  "(prod.swap ` R)⇧+ = prod.swap ` (R⇧+)"
proof -
  have [simp]: "prod.swap ` X = X¯" for X by auto
  show ?thesis by (simp add: trancl_converse)
qed

lemma swap_rtrancl:
  "(prod.swap ` R)⇧* = prod.swap ` (R⇧*)"
proof -
  have [simp]: "prod.swap ` X = X¯" for X by auto
  show ?thesis by (simp add: rtrancl_converse)
qed

abbreviation map_both where
  "map_both f ≡ map_prod f f"

lemma trancl_map:
  assumes simu: "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
    and steps: "(x, y) ∈ r⇧+"
  shows "(f x, f y) ∈ s⇧+"
  using assms rtrancl_map[of r f s]
  by (meson rtrancl_into_trancl1 tranclD2)

lemma trancl_map_prod_mono:
  "map_both f ` R⇧+ ⊆ (map_both f ` R)⇧+"
proof -
  have "(f x, f y) ∈ (map_both f ` R)⇧+" if "(x, y) ∈ R⇧+" for x y using that
    by (induct) (auto intro: trancl_into_trancl)
  then show ?thesis by auto
qed

lemma trancl_map_both_Restr:
  assumes "inj_on f X"
  shows "(map_both f ` Restr R X)⇧+ = map_both f ` (Restr R X)⇧+"
proof -
  have [simp]:
    "map_prod (inv_into X f ∘ f) (inv_into X f ∘ f) ` Restr R X = Restr R X"
    using inv_into_f_f[OF assms]
    apply (intro equalityI subrelI)
     apply (auto simp: comp_def map_prod_def image_def)
    apply (metis (no_types, lifting) IntI SigmaI case_prod_conv)
    done
  have [simp]:
    "map_prod (f ∘ inv_into X f) (f ∘ inv_into X f) ` (map_both f ` Restr R X)⇧+ = (map_both f ` Restr R X)⇧+"
    using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X × X" "map_both f"]]]
    by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
  show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
      image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f ` Restr R X"], of "map_both f"]
    by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed


lemma inj_on_trancl_map_both:
  assumes "inj_on f (fst ` R ∪ snd ` R)"
  shows "(map_both f ` R)⇧+ = map_both f ` R⇧+"
proof -
  have [simp]: "Restr R (fst ` R ∪ snd ` R) = R"
    by (force simp: image_def)
  then show ?thesis using assms
    using trancl_map_both_Restr[of f "fst ` R ∪ snd ` R" R]
    by simp
qed

lemmas trancl_map_both = trancl_map_both_Restr[of _ UNIV, unfolded UNIV_Times_UNIV Int_UNIV_right]

lemma map_both_relcomp:
  "inj_on f (snd ` A ∪ fst ` B) ⟹ map_both f ` A O map_both f ` B = map_both f ` (A O B)"
  by (force simp: inj_on_def intro: rev_image_eqI)

lemma subterm_set_finite:
  shows "finite {t . s ⊳ t}"
  by (intro finite_subset[OF _ finite_subterms[of s]]) auto

lemma ground_set_map_adapt_vars_dist:
  assumes "A ⊆ Collect ground × Collect ground"
  and "B ⊆ Collect ground × Collect ground"
shows "(map_both adapt_vars ` A) O (map_both adapt_vars ` B) = map_both adapt_vars ` (A O B)" (is "?L = ?R")
proof
  show "?L ⊆ ?R" apply (rule) using assms adapt_vars_inj by blast
next
  show "?R ⊆ ?L" apply (rule) using assms adapt_vars_inj by blast
qed




section ‹Conversions of the Nth function between lists and a spliting of the list into lists of lists›

fun concat_index_split where
  "concat_index_split (o_idx, i_idx) (x # xs) =
     (if i_idx < length x
      then (o_idx, i_idx)
      else concat_index_split (Suc o_idx, i_idx - length x) xs)"

lemma concat_index_split_mono_first_arg:
  "i < length (concat xs) ⟹ o_idx ≤ fst (concat_index_split (o_idx, i) xs)"
  by (induct xs arbitrary: o_idx i) (auto, metis Suc_leD add_diff_inverse_nat nat_add_left_cancel_less)

lemma concat_index_split_sound_fst_arg_aux:
  "i < length (concat xs) ⟹ fst (concat_index_split (o_idx, i) xs) < length xs + o_idx"
  by (induct xs arbitrary: o_idx i) (auto, metis add_Suc_right add_diff_inverse_nat nat_add_left_cancel_less)

lemma concat_index_split_sound_fst_arg:
  "i < length (concat xs) ⟹ fst (concat_index_split (0, i) xs) < length xs"
  using concat_index_split_sound_fst_arg_aux[of i xs 0] by auto

lemma concat_index_split_sound_snd_arg_aux:
  assumes "i < length (concat xs)"
  shows "snd (concat_index_split (n, i) xs) < length (xs ! (fst (concat_index_split (n, i) xs) - n))" using assms
proof (induct xs arbitrary: i n)
  case (Cons x xs)
  show ?case proof (cases "i < length x")
    case False then have size: "i - length x < length (concat xs)"
      using Cons(2) False by auto
    obtain k j where [simp]: "concat_index_split (Suc n, i - length x) xs = (k, j)"
      using old.prod.exhaust by blast
    show ?thesis using False Cons(1)[OF size, of "Suc n"] concat_index_split_mono_first_arg[OF size, of "Suc n"]
      by (auto simp: nth_append)
  qed (auto simp add: nth_append) 
qed auto

lemma concat_index_split_sound_snd_arg:
  assumes "i < length (concat xs)"
  shows "snd (concat_index_split (0, i) xs) < length (xs ! fst (concat_index_split (0, i) xs))"
  using concat_index_split_sound_snd_arg_aux[OF assms, of 0] by auto

lemma reconstr_1d_concat_index_split:
  assumes "i < length (concat xs)"
  shows "i = (λ (m, j). sum_list (map length (take (m - n) xs)) + j) (concat_index_split (n, i) xs)" using assms
proof (induct xs arbitrary: i n)
  case (Cons x xs) show ?case
  proof (cases "i < length x")
    case False
    obtain m k where res: "concat_index_split (Suc n, i - length x) xs = (m, k)"
      using prod_decode_aux.cases by blast
    then have unf_ind: "concat_index_split (n, i) (x # xs) = concat_index_split (Suc n, i - length x) xs" and
      size: "i - length x < length (concat xs)" using Cons(2) False by auto
    have "Suc n ≤ m" using concat_index_split_mono_first_arg[OF size, of "Suc n"] by (auto simp: res)
    then have [simp]: "sum_list (map length (take (m - n) (x # xs))) = sum_list (map length (take (m - Suc n) xs)) + length x"
      by (simp add: take_Cons')
    show ?thesis using Cons(1)[OF size, of "Suc n"] False unfolding unf_ind res by auto
  qed auto
qed auto

lemma concat_index_split_larger_lists [simp]:
  assumes "i < length (concat xs)"
  shows "concat_index_split (n, i) (xs @ ys) = concat_index_split (n, i) xs" using assms
  by (induct xs arbitrary: ys n i) auto

lemma concat_index_split_split_sound_aux:
  assumes "i < length (concat xs)"
  shows "concat xs ! i = (λ (k, j). xs ! (k - n) ! j) (concat_index_split (n, i) xs)" using assms
proof (induct xs arbitrary: i n)
  case (Cons x xs)
  show ?case proof (cases "i < length x")
    case False then have size: "i - length x < length (concat xs)"
      using Cons(2) False by auto
    obtain k j where [simp]: "concat_index_split (Suc n, i - length x) xs = (k, j)"
      using prod_decode_aux.cases by blast
    show ?thesis using False Cons(1)[OF size, of "Suc n"]
      using concat_index_split_mono_first_arg[OF size, of "Suc n"]
      by (auto simp: nth_append)
  qed (auto simp add: nth_append) 
qed auto

lemma concat_index_split_sound:
  assumes "i < length (concat xs)"
  shows "concat xs ! i = (λ (k, j). xs ! k ! j) (concat_index_split (0, i) xs)"
  using concat_index_split_split_sound_aux[OF assms, of 0] by auto

lemma concat_index_split_sound_bounds:
  assumes "i < length (concat xs)" and "concat_index_split (0, i) xs = (m, n)"
  shows "m < length xs" "n < length (xs ! m)"
  using concat_index_split_sound_fst_arg[OF assms(1)] concat_index_split_sound_snd_arg[OF assms(1)]
  by (auto simp: assms(2))

lemma concat_index_split_less_length_concat:
  assumes "i < length (concat xs)" and "concat_index_split (0, i) xs = (m, n)"
  shows "i = sum_list (map length (take m xs)) + n" "m < length xs" "n < length (xs ! m)"
    "concat xs ! i = xs ! m ! n"
  using concat_index_split_sound[OF assms(1)] reconstr_1d_concat_index_split[OF assms(1), of 0]
  using concat_index_split_sound_fst_arg[OF assms(1)] concat_index_split_sound_snd_arg[OF assms(1)] assms(2)
  by auto

lemma concat_index_split_unique:
  assumes "i < length (concat xs)" and "length xs = length ys"
    and "∀ i < length xs. length (xs ! i) = length (ys ! i)"
  shows "concat_index_split (n, i) xs = concat_index_split (n, i) ys" using assms
proof (induct xs arbitrary: ys n i)
  case (Cons x xs) note IH = this show ?case
  proof (cases ys)
    case Nil then show ?thesis using Cons(3) by auto
  next
    case [simp]: (Cons y ys')
    have [simp]: "length y = length x" using IH(4) by force
    have [simp]: "¬ i < length x ⟹ i - length x < length (concat xs)" using IH(2) by auto
    have [simp]: "i < length ys' ⟹ length (xs ! i) = length (ys' ! i)" for i using IH(3, 4)
      by (auto simp: All_less_Suc)
    show ?thesis using IH(2-) IH(1)[of "i - length x" ys' "Suc n"] by auto
  qed
qed auto





subsection ‹Position of terms and multihole contexts as lists in contrast to sets.
  The order of the elements of the resulting list corresponds to the order of the variables (holes)
  from left to right›

"poss_args f ts ≡ map2 (λ i t. map ((#) i) (f t)) ([0 ..< length ts]) ts"">abbreviation "poss_args f ts ≡ map2 (λ i t. map ((#) i) (f t)) ([0 ..< length ts]) ts"

fun varposs_list :: "('f, 'v) term ⇒ pos list" where
  "varposs_list (Var x) = [[]]" |
  "varposs_list (Fun f ts) = concat (poss_args varposs_list ts)"

lemma vaposs_list_fun:
  assumes "p ∈ set (varposs_list (Fun f ts))"
  obtains i ps where "i < length ts" "p = i # ps"
  using assms set_zip_leftD by fastforce

lemma map_cons_presv_distinct:
  "distinct t ⟹ distinct (map ((#) i) t)"
  by (simp add: distinct_conv_nth)

lemma varposs_list_distinct:
  "distinct (varposs_list t)"
proof (induct t)
  case (Fun f ts)
  then show ?case proof (induct ts rule: rev_induct)
    case (snoc x xs)
    then have "distinct (varposs_list (Fun f xs))" "distinct (varposs_list x)" by auto
    then show ?case using snoc by (auto simp add: map_cons_presv_distinct dest: set_zip_leftD)
  qed auto
qed auto

lemma varposs_append:
  "varposs (Fun f (ts @ [t])) = varposs (Fun f ts) ∪ ((#) (length ts)) ` varposs t"
  by (auto simp: nth_append split: if_splits)

lemma varposs_eq_varposs_list:
  "varposs t = set (varposs_list t)"
proof (induct t)
  case (Fun f ts)
  then show ?case proof (induct ts rule: rev_induct)
    case (snoc x xs)
    then have "varposs (Fun f xs) = set (varposs_list (Fun f xs))"
      "varposs x = set (varposs_list x)" by auto
    then show ?case using snoc unfolding varposs_append
      by auto
  qed auto
qed auto

lemma varposs_list_var_terms_length:
  "length (varposs_list t) = length (vars_term_list t)"
  by (induct t) (auto simp: vars_term_list.simps intro: eq_length_concat_nth)

lemma vars_term_list_nth:
  assumes "i < length (vars_term_list (Fun f ts))"
    and "concat_index_split (0, i) (map vars_term_list ts) = (k, j)"
  shows "k < length ts ∧ j < length (vars_term_list (ts ! k)) ∧
    vars_term_list (Fun f ts) ! i = map vars_term_list ts ! k ! j ∧
    i = sum_list (map length (map vars_term_list (take k ts))) + j"
  using assms concat_index_split_less_length_concat[of i "map vars_term_list ts" k j]
  by (auto simp: vars_term_list.simps comp_def take_map) 

lemma varposs_list_nth:
  assumes "i < length (varposs_list (Fun f ts))"
     and "concat_index_split (0, i) (poss_args varposs_list ts) = (k, j)"
  shows "k < length ts ∧ j < length (varposs_list (ts ! k)) ∧
    varposs_list (Fun f ts) ! i = k # (map varposs_list ts) ! k ! j ∧
    i = sum_list (map length (map varposs_list (take k ts))) + j"
  using assms concat_index_split_less_length_concat[of i "poss_args varposs_list ts" k j]
  by (auto simp: comp_def take_map intro: nth_sum_listI)


lemma varposs_list_to_var_term_list:
  assumes "i < length (varposs_list t)"
  shows "the_Var (t |_ (varposs_list t ! i)) = (vars_term_list t) ! i" using assms
proof (induct t arbitrary: i)
  case (Fun f ts)
  have "concat_index_split (0, i) (poss_args varposs_list ts) = concat_index_split (0, i) (map vars_term_list ts)"
    using Fun(2) concat_index_split_unique[of i "poss_args varposs_list ts" "map vars_term_list ts" 0]
    using varposs_list_var_terms_length[of "ts ! i" for i]
    by (auto simp: vars_term_list.simps)
  then obtain k j where "concat_index_split (0, i) (poss_args varposs_list ts) = (k, j)"
    "concat_index_split (0, i) (map vars_term_list ts) = (k, j)" by fastforce
  from varposs_list_nth[OF Fun(2) this(1)] vars_term_list_nth[OF _ this(2)]
  show ?case using Fun(2) Fun(1)[OF nth_mem] varposs_list_var_terms_length[of "Fun f ts"] by auto
qed (auto simp: vars_term_list.simps)

fun hole_poss_list :: "('f, 'v) mctxt ⇒ pos list" where
  "hole_poss_list (MVar x) = []" |
  "hole_poss_list MHole = [[]]" |
  "hole_poss_list (MFun f cs) = concat (poss_args hole_poss_list cs)"

lemma unfill_holles_hole_poss_list_length:
  assumes "C ≤ mctxt_of_term t"
  shows "length (unfill_holes C t) = length (hole_poss_list C)" using assms
proof (induct C arbitrary: t)
  case (MFun f ts) then show ?case
    by (cases t) (auto simp: length_concat comp_def
      elim!: less_eq_mctxt_MFunE1 less_eq_mctxt_MVarE1 intro!: nth_sum_listI)
qed (auto elim: less_eq_mctxt_MVarE1)

lemma unfill_holes_to_subst_at_hole_poss:
  assumes "C ≤ mctxt_of_term t"
  shows "unfill_holes C t = map ((|_) t) (hole_poss_list C)" using assms
proof (induct C arbitrary: t)
  case (MVar x)
  then show ?case by (cases t) (auto elim: less_eq_mctxt_MVarE1)
next
  case (MFun f ts)
  from MFun(2) obtain ss where [simp]: "t = Fun f ss" and l: "length ts = length ss"
    by (cases t) (auto elim: less_eq_mctxt_MFunE1)
  let ?ts = "map (λi. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]"
  let ?ss = "map (λ x. map ((|_) (Fun f ss)) (case x of (x, y) ⇒ map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)"
  have eq_l [simp]: "length (concat ?ts) = length (concat ?ss)" using MFun
    by (auto simp: length_concat comp_def elim!: less_eq_mctxt_MFunE1 split!: prod.splits intro!: nth_sum_listI)
  {fix i assume ass: "i < length (concat ?ts)"
    then have lss: "i < length (concat ?ss)" by auto
    obtain m n where [simp]: "concat_index_split (0, i) ?ts = (m, n)" by fastforce
    then have [simp]: "concat_index_split (0, i) ?ss = (m, n)" using concat_index_split_unique[OF ass, of ?ss 0] MFun(2)
      by (auto simp: unfill_holles_hole_poss_list_length[of "ts ! i" "ss ! i" for i]
       simp del: length_unfill_holes elim!: less_eq_mctxt_MFunE1)
    from concat_index_split_less_length_concat(2-)[OF ass ] concat_index_split_less_length_concat(2-)[OF lss]
    have "concat ?ts ! i = concat ?ss! i" using MFun(1)[OF nth_mem, of m "ss ! m"] MFun(2)
      by (auto elim!: less_eq_mctxt_MFunE1)} note nth = this
  show ?case using MFun
    by (auto simp: comp_def map_concat length_concat
        elim!: less_eq_mctxt_MFunE1 split!: prod.splits
        intro!: nth_equalityI nth_sum_listI nth)
qed auto

lemma hole_poss_split_varposs_list_length [simp]:
  "length (hole_poss_list (fst (split_vars t))) = length (varposs_list t)"
  by (induct t)(auto simp: length_concat comp_def intro!: nth_sum_listI)

lemma hole_poss_split_vars_varposs_list:
  "hole_poss_list (fst (split_vars t)) = varposs_list t"
proof (induct t)
  case (Fun f ts)
  let ?ts = "poss_args hole_poss_list (map (fst ∘ split_vars) ts)"
  let ?ss = "poss_args varposs_list ts"
  have len: "length (concat ?ts) = length (concat ?ss)" "length ?ts = length ?ss"
    "∀ i < length ?ts. length (?ts ! i) = length (?ss ! i)" by (auto intro: eq_length_concat_nth)
  {fix i assume ass: "i < length (concat ?ts)"
    then have lss: "i < length (concat ?ss)" using len by auto
    obtain m n where int: "concat_index_split (0, i) ?ts = (m, n)" by fastforce
    then have [simp]: "concat_index_split (0, i) ?ss = (m, n)" using concat_index_split_unique[OF ass len(2-)] by auto
    from concat_index_split_less_length_concat(2-)[OF ass int] concat_index_split_less_length_concat(2-)[OF lss]
    have "concat ?ts ! i = concat ?ss! i" using Fun[OF nth_mem, of m] by auto}
  then show ?case using len by (auto intro: nth_equalityI)
qed auto

end