theory Utils
  imports Regular_Tree_Relations.Term_Context
    Regular_Tree_Relations.FSet_Utils
begin

subsection ‹Misc›

definition "funas_trs ℛ = ⋃ ((λ (s, t). funas_term s ∪ funas_term t) ` ℛ)"

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

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

fun varposs :: "('f, 'v) term ⇒ pos set" where
  "varposs (Var x) = {[]}" |
  "varposs (Fun f ts) = (⋃i<length ts. {i # p | p. p ∈ varposs (ts ! i)})"

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

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

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 sorted_append_bigger:
  "sorted xs ⟹  ∀x ∈ set xs. x ≤ y ⟹ sorted (xs @ [y])"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  then have s: "sorted xs" by (cases xs) simp_all
  from Cons have a: "∀x∈set xs. x ≤ y" by simp
  from Cons(1)[OF s a] Cons(2-) show ?case by (cases xs) simp_all
qed

lemma find_SomeD:
  "List.find P xs = Some x ⟹ P x"
  "List.find P xs = Some x ⟹ x∈set xs"
  by (auto simp add: find_Some_iff)

lemma sum_list_replicate_length' [simp]:
  "sum_list (replicate n (Suc 0)) = n"
  by (induct n) simp_all

lemma arg_subteq [simp]:
  assumes "t ∈ set ts" shows "Fun f ts ⊵ t"
  using assms by auto

lemma finite_funas_term: "finite (funas_term s)"
  by (induct s) auto

lemma finite_funas_trs:
  "finite ℛ ⟹ finite (funas_trs ℛ)"
  by (induct rule: finite.induct) (auto simp: finite_funas_term funas_trs_def)

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) (auto elim: supteq.cases)

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

lemma finite_subterms: "finite {t. s ⊵ t}"
  unfolding set_all_subteq_subterms[symmetric]
  by (simp add: finite_subterms_fun)

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

lemma finite_UN_I2:
  "finite A ⟹ (∀ B ∈ A. finite B) ⟹ finite (⋃ A)"
  by blast

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 g assume "g ∈ ?Rs" then have "g ∈ ?Ls"
    proof (induct s arbitrary: g)
      case (Fun f ts)
      from Fun(2) consider "g = (f, length ts)" | "∃ t ∈ set ts. g ∈ funas_term t"
        by (force simp: in_set_conv_nth)
      then show ?case
      proof cases
        case 1 then show ?thesis
          by (auto simp: image_iff intro: bexI[of _ "Some (f, length ts)"])
      next
        case 2
        then obtain t where wit: "t ∈ set ts" "g ∈ funas_term t" by blast
        have "g ∈ the ` (root ` subterms t - {None})" using Fun(1)[OF wit] .
        then show ?thesis using wit(1)
          by (auto simp: image_iff)
      qed
    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)


lemma subst_merge:
  assumes part: "is_partition (map vars_term ts)"
  shows "∃σ. ∀i<length ts. ∀x∈vars_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


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 subseteq_set_conv_nth:
  "(∀ i < length ss. ss ! i ∈ T) ⟷ set ss ⊆ T"
  by (metis in_set_conv_nth subset_code(1))

lemma singelton_trancl [simp]: "{a}⇧+ = {a}"
  using tranclD tranclD2 by fastforce 

context
includes fset.lifting
begin
lemmas frelcomp_empty_ftrancl_simp = rel_comp_empty_trancl_simp [Transfer.transferred]
lemmas in_fset_idx = in_set_idx [Transfer.transferred]
lemmas fsubseteq_fset_conv_nth = subseteq_set_conv_nth [Transfer.transferred]
lemmas singelton_ftrancl [simp] = singelton_trancl [Transfer.transferred]
end

lemma set_take_nth:
  assumes "x ∈ set (take i xs)"
  shows "∃ j < length xs. j < i ∧ xs ! j = x" using assms
  by (metis in_set_conv_nth length_take min_less_iff_conj nth_take)

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 concat_nth_length:
  "i < length uss ⟹ j < length (uss ! i) ⟹
    sum_list (map length (take i uss)) + j < length (concat uss)"
by (induct uss arbitrary: i j) (simp, case_tac i, auto)

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 nth_equalityE:
  "xs = ys ⟹ (length xs = length ys ⟹ (⋀i. i < length xs ⟹ xs ! i = ys ! i) ⟹ P) ⟹ P"
  by simp

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

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

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 ℛ]])


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

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 nth_concat_split':
  assumes "i < length (concat xs)"
  obtains j k where "j < length xs" "k < length (xs ! j)" "concat xs ! i = xs ! j ! k" "i = sum_list (map length (take j xs)) + k"
  using concat_index_split_less_length_concat[OF assms]
  by (meson old.prod.exhaust)

lemma sum_list_split [dest!, consumes 1]:
  assumes "sum_list (map length (take i xs)) + j = sum_list (map length (take k xs)) + l"
   and "i < length xs" "k < length xs"
   and "j < length (xs ! i)" "l < length (xs ! k)"
 shows "i = k ∧ j = l" using assms
proof (induct xs rule: rev_induct)
  case (snoc x xs)
  then show ?case
    by (auto simp: nth_append split: if_splits)
       (metis concat_nth_length length_concat not_add_less1)+
qed 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) (metis IH(4) Suc_less_eq length_Cons Cons nth_Cons_Suc)
    show ?thesis using IH(2-) IH(1)[of "i - length x" ys' "Suc n"] by auto
  qed
qed auto

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

lemma vars_term_list_empty_ground [simp]:
  "vars_term_list t = [] ⟷ ground t"
  by (induct t) auto

lemma varposs_imp_poss:
  assumes "p ∈ varposs t"
  shows "p ∈ poss t"
  using assms by (induct t arbitrary: p) auto

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 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:
  "set (varposs_list t) = varposs 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)

end