(* 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 blast 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 (verit) 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 atomize_elim auto 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 atomize_elim auto 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 atomize_elim auto 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