# Theory Miscellaneous

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

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

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

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

lemma 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"
by (smt assms length_prefix_ex' nth_append append.assoc append.simps(2) add_diff_cancel_left'
diff_Suc_1 length_Cons length_append)

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

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

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
```