Theory Miscellaneous

(*  Title:      Miscellaneous.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

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

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

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

lemma in_set_zip_swap: "(x,y)  set (zip xs ys)  (y,x)  set (zip ys xs)"
unfolding in_set_zip by auto

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

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

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

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

lemma list_all2_in_set_ex:
  assumes P: "list_all2 P xs ys"
    and x: "x  set xs"
  shows "y  set ys. P x y"
proof -
  obtain i where i: "i < length xs" "xs ! i = x" by (meson x in_set_conv_nth)
  have "i < length ys" "P (xs ! i) (ys ! i)"
    using P i(1) by (simp_all add: list_all2_iff list_all2_nthD)
  thus ?thesis using i(2) by auto
qed

lemma list_all2_in_set_ex':
  assumes P: "list_all2 P xs ys"
    and y: "y  set ys"
  shows "x  set xs. P x y"
proof -
  obtain i where i: "i < length ys" "ys ! i = y" by (meson y in_set_conv_nth)
  have "i < length xs" "P (xs ! i) (ys ! i)"
    using P i(1) by (simp_all add: list_all2_iff list_all2_nthD)
  thus ?thesis using i(2) by auto
qed

lemma list_all2_sym:
  assumes "x y. P x y  P y x"
    and "list_all2 P xs ys"
  shows "list_all2 P ys xs"
using assms(2) by (induct rule: list_all2_induct) (simp_all add: assms(1))

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

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

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

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

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

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

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

lemma map2_those_Some_case:
  assumes "those (map2 f xs ys) = Some zs"
    and "(x,y)  set (zip xs ys)"
  shows "z. f x y = Some z"
  using assms 
proof (induction xs arbitrary: ys zs)
  case (Cons x' xs')
  obtain y' ys' where ys: "ys = y'#ys'" using Cons.prems(2) by (cases ys) simp_all
  obtain z where z: "f x' y' = Some z" using Cons.prems(1) ys by fastforce
  obtain zs' where zs: "those (map2 f xs' ys') = Some zs'" using z Cons.prems(1) ys by auto

  show ?case
  proof (cases "(x,y) = (x',y')")
    case False
    hence "(x,y)  set (zip xs' ys')" using Cons.prems(2) unfolding ys by force
    thus ?thesis using Cons.IH[OF zs] by blast
  qed (use ys z in fast)
qed simp

lemma those_Some_Cons_ex:
  assumes "those (x#xs) = Some ys"
  shows "y ys'. ys = y#ys'  those xs = Some ys'  x = Some y"
using assms by (cases x) auto

lemma those_Some_iff:
  "those xs = Some ys  ((x'  set xs. x. x' = Some x)  ys = map the xs)"
  (is "?A xs ys  ?B xs ys")
proof
  show "?A xs ys  ?B xs ys"
  proof (induction xs arbitrary: ys)
    case (Cons x' xs')
    obtain y' ys' where ys: "ys = y'#ys'" "those xs' = Some ys'" and x: "x' = Some y'"
      using Cons.prems those_Some_Cons_ex by blast
    show ?case using Cons.IH[OF ys(2)] unfolding x ys by simp
  qed simp

  show "?B xs ys  ?A xs ys"
    by (induct xs arbitrary: ys) (simp, fastforce)
qed

lemma those_map2_SomeD:
  assumes "those (map2 f ts ss) = Some θ"
    and "σ  set θ"
  shows "(t,s)  set (zip ts ss). f t s = Some σ"
using those_Some_iff[of "map2 f ts ss" θ] assms by fastforce

lemma those_map2_SomeI:
  assumes "i. i < length xs  f (xs ! i) (ys ! i) = Some (g i)"
    and "length xs = length ys"
  shows "those (map2 f xs ys) = Some (map g [0..<length xs])"
proof -
  have "z  set (map2 f xs ys). z'. z = Some z'"
  proof
    fix z assume z: "z  set (map2 f xs ys)"
    then obtain i where i: "i < length xs" "i < length ys" "z = f (xs ! i) (ys ! i)"
      using in_set_conv_nth[of z "map2 f xs ys"] by auto
    thus "z'. z = Some z'"
      using assms(1) by blast
  qed
  moreover have "map Some (map g [0..<length xs]) = map (λi. f (xs ! i) (ys ! i)) [0..<length xs]"
    using assms by auto
  hence "map Some (map g [0..<length xs]) = map2 f xs ys"
    using assms by (smt map2_map_map map_eq_conv map_nth)
  hence "map (the  Some) (map g [0..<length xs]) = map the (map2 f xs ys)"
    by (metis map_map)
  hence "map g [0..<length xs] = map the (map2 f xs ys)"
    by simp
  ultimately show ?thesis using those_Some_iff by blast
qed


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

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

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

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

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


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

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

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

lemma concat_mono_prefix: "prefix xs ys  prefix (concat xs) (concat ys)"
unfolding prefix_def by fastforce

lemma concat_map_mono_prefix: "prefix xs ys  prefix (concat (map f xs)) (concat (map f ys))"
by (rule map_mono_prefix[THEN concat_mono_prefix])

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

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

lemma length_prefix_ex2:
  assumes "i < length xs" "j < length xs" "i < j"
  shows "ys zs vs. xs = ys@xs ! i#zs@xs ! j#vs  length ys = i  length zs = j - i - 1"
proof -
  obtain xs0 vs where xs0: "xs = xs0@xs ! j#vs" "length xs0 = j"
    using length_prefix_ex'[OF assms(2)] by blast
  then obtain ys zs where "xs0 = ys@xs ! i#zs" "length ys = i"
    by (metis assms(3) length_prefix_ex' nth_append[of _ _ i])
  thus ?thesis using xs0 by force
qed

lemma prefix_prefix_inv:
  assumes xs: "prefix xs (ys@zs)"
    and x: "suffix [x] xs"
  shows "prefix xs ys  x  set zs"
proof -
  have "prefix xs ys" when "x  set zs" using that xs
  proof (induction zs rule: rev_induct)
    case (snoc z zs) show ?case
    proof (rule snoc.IH)
      have "x  z" using snoc.prems(1) by simp
      thus "prefix xs (ys@zs)"
        using snoc.prems(2) x by (metis append1_eq_conv append_assoc prefix_snoc suffixE) 
    qed (use snoc.prems(1) in simp)
  qed simp
  thus ?thesis by blast
qed

lemma prefix_snoc_obtain:
  assumes xs: "prefix (xs@[x]) (ys@zs)"
    and ys: "¬prefix (xs@[x]) ys"
  obtains vs where "xs@[x] = ys@vs@[x]" "prefix (vs@[x]) zs"
proof -
  have "vs. xs@[x] = ys@vs@[x]  prefix (vs@[x]) zs" using xs
  proof (induction zs rule: List.rev_induct)
    case (snoc z zs)
    show ?case
    proof (cases "xs@[x] = ys@zs@[z]")
      case False
      hence "prefix (xs@[x]) (ys@zs)" using snoc.prems by (metis append_assoc prefix_snoc)
      thus ?thesis using snoc.IH by auto
    qed simp
  qed (simp add: ys)
  thus ?thesis using that by blast
qed

lemma prefix_snoc_in_iff: "x  set xs  (B. prefix (B@[x]) xs)"
by (induct xs rule: List.rev_induct) auto


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

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

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


subsection ‹Other Lemmata›
lemma finite_ballI:
  "l  {}. P l" "P x  l  xs. P l  l  insert x xs. P l"
by (blast, blast)

lemma list_set_ballI:
  "l  set []. P l" "P x  l  set xs. P l  l  set (x#xs). P l"
by (simp, simp)

lemma inv_set_fset: "finite M  set (inv set M) = M"
unfolding inv_def by (metis (mono_tags) finite_list someI_ex)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  show ?thesis using 1 2 by blast
qed

lemma ex_list_obtain:
  assumes ts: "t. t  set ts  s. P t s"
  obtains ss where "length ss = length ts" "i < length ss. P (ts ! i) (ss ! i)"
proof -
  have "ss. length ss = length ts  (i < length ss. P (ts ! i) (ss ! i))" using ts
  proof (induction ts rule: List.rev_induct)
    case (snoc t ts)
    obtain s ss where s: "length ss = length ts" "i < length ss. P (ts ! i) (ss ! i)" "P t s"
      using snoc.IH snoc.prems by force
    have *: "length (ss@[s]) = length (ts@[t])" using s(1) by simp
    hence "P ((ts@[t]) ! i) ((ss@[s]) ! i)" when i: "i < length (ss@[s])" for i
      using s(2,3) i nth_append[of ts "[t]"] nth_append[of ss "[s]"] by force
    thus ?case using * by blast
  qed simp
  thus thesis using that by blast
qed

lemma length_1_conv[iff]:
  "(length ts = 1) = (a. ts = [a])"
by (cases ts) simp_all

lemma length_2_conv[iff]:
  "(length ts = 2) = (a b. ts = [a,b])"
proof (cases ts)
  case (Cons a ts') thus ?thesis by (cases ts') simp_all
qed simp

lemma length_3_conv[iff]:
  "(length ts = 3)  (a b c. ts = [a,b,c])"
proof (cases ts)
  case (Cons a ts')
  note * = this
  thus ?thesis
  proof (cases ts')
    case (Cons b ts'') thus ?thesis using * by (cases ts'') simp_all
  qed simp
qed simp

lemma Max_nat_finite_le:
  assumes "finite M"
    and "m. m  M  f m  (n::nat)"
  shows "Max (insert 0 (f ` M))  n"
proof -
  have 0: "finite (insert 0 (f ` M))" using assms(1) by blast
  have 1: "insert 0 (f ` M)  {}" by force
  have 2: "m  n" when "m  insert 0 (f ` M)" for m using assms(2) that by fastforce
  show ?thesis using Max.boundedI[OF 0 1 2] by blast
qed

lemma Max_nat_finite_lt:
  assumes "finite M"
    and "M  {}"
    and "m. m  M  f m < (n::nat)"
  shows "Max (f ` M) < n"
proof -
  define g where "g  λm. Suc (f m)"
  have 0: "finite (f ` M)" "finite (g ` M)" using assms(1) by (blast, blast)
  have 1: "f ` M  {}" "g ` M  {}" using assms(2) by (force, force)
  have 2: "m  n" when "m  g ` M" for m using assms(3) that unfolding g_def by fastforce
  have 3: "Max (g ` M)  n" using Max.boundedI[OF 0(2) 1(2) 2] by blast
  have 4: "Max (f ` M) < Max (g ` M)"
    using Max_in[OF 0(1) 1(1)] Max_gr_iff[OF 0(2) 1(2), of "Max (f ` M)"]
    unfolding g_def by blast
  show ?thesis using 3 4 by linarith
qed

lemma ex_finite_disj_nat_inj:
  fixes N N'::"nat set"
  assumes N: "finite N"
    and N': "finite N'"
  shows "M::nat set. δ::nat  nat. inj δ  δ ` N = M  M  N' = {}"
using N 
proof (induction N rule: finite_induct)
  case empty thus ?case using injI[of "λx::nat. x"] by blast
next
  case (insert n N)
  then obtain M δ where M: "inj δ" "δ ` N = M" "M  N' = {}" by blast

  obtain m where m: "m  M" "m  insert n N" "m  N'"
    using M(2) finite_imageI[OF insert.hyps(1), of δ] insert.hyps(1) N'
    by (metis finite_UnI finite_insert UnCI infinite_nat_iff_unbounded_le
              finite_nat_set_iff_bounded_le)

  define σ where "σ  λk. if k  insert n N then (δ(n := m)) k else Suc (Max (insert m M)) + k"

  have "insert m M  N' = {}" using m M(3) unfolding σ_def by auto
  moreover have "σ ` insert n N = insert m M" using insert.hyps(2) M(2) unfolding σ_def by auto
  moreover have "inj σ"
  proof (intro injI)
    fix i j assume ij: "σ i = σ j"

    have 0: "finite (insert m (δ ` N))"
      using insert.hyps(1) by simp

    have 1: "Suc (Max (insert m (δ ` N))) > k" when k: "k  insert m (δ ` N)" for k
      using Max_ge[OF 0 k] by linarith
    
    have 2: "(δ(n := m)) k  insert m (δ ` N)" when k: "k  insert n N" for k
      using k by auto
    
    have 3: "(δ(n := m)) k  Suc (Max (insert m (δ ` N))) + k'" when k: "k  insert n N" for k k'
      using 1[OF 2[OF k]] by linarith

    have 4: "i  insert n N  j  insert n N"
      using ij 3 M(2) unfolding σ_def by metis

    show "i = j"
    proof (cases "i  insert n N")
      case True
      hence *: "σ i = (δ(n := m)) i" "σ j = (δ(n := m)) j"
               "i  insert n N" "j  insert n N"
        using ij iffD1[OF 4] unfolding σ_def by (argo, argo, argo, argo)

      show ?thesis
      proof (cases "i = n  j = n")
        case True
        moreover have ?thesis when "i = n" "j = n" using that by simp
        moreover have False when "(i = n  j  n)  (i  n  j = n)"
          by (metis M(2) that ij * m(1) fun_upd_other fun_upd_same image_eqI insertE)
        ultimately show ?thesis by argo
      next
        case False thus ?thesis using ij injD[OF M(1), of i j] unfolding *(1,2) by simp
      qed
    next
      case False thus ?thesis using ij 4 unfolding σ_def by force
    qed
  qed
  ultimately show ?case by blast
qed


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

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

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

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

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

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

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

end

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

  have "?s  {}" using base by auto

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

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

end