diff --git a/thys/Nash_Williams/Nash_Extras.thy b/thys/Nash_Williams/Nash_Extras.thy --- a/thys/Nash_Williams/Nash_Extras.thy +++ b/thys/Nash_Williams/Nash_Extras.thy @@ -1,55 +1,55 @@ section \The Pointwise Less-Than Relation Between Two Sets\ theory Nash_Extras imports "HOL-Library.Ramsey" "HOL-Library.Countable_Set" begin definition less_sets :: "['a::order set, 'a::order set] \ bool" (infixr "\" 50) where "A \ B \ \x\A. \y\B. x < y" lemma less_setsD: "\A \ B; a \ A; b \ B\ \ a < b" by (auto simp: less_sets_def) lemma less_sets_irrefl [simp]: "A \ A \ A = {}" by (auto simp: less_sets_def) lemma less_sets_trans: "\A \ B; B \ C; B \ {}\ \ A \ C" unfolding less_sets_def using less_trans by blast lemma less_sets_weaken1: "\A' \ B; A \ A'\ \ A \ B" by (auto simp: less_sets_def) lemma less_sets_weaken2: "\A \ B'; B \ B'\ \ A \ B" by (auto simp: less_sets_def) lemma less_sets_imp_disjnt: "A \ B \ disjnt A B" by (auto simp: less_sets_def disjnt_def) lemma less_sets_UN1: "less_sets (\\) B \ (\A\\. A \ B)" by (auto simp: less_sets_def) lemma less_sets_UN2: "less_sets A (\ \) \ (\B\\. A \ B)" by (auto simp: less_sets_def) lemma less_sets_Un1: "less_sets (A \ A') B \ A \ B \ A' \ B" by (auto simp: less_sets_def) lemma less_sets_Un2: "less_sets A (B \ B') \ A \ B \ A \ B'" by (auto simp: less_sets_def) lemma strict_sorted_imp_less_sets: "strict_sorted (as @ bs) \ (list.set as) \ (list.set bs)" - by (simp add: less_sets_def sorted_wrt_append strict_sorted_sorted_wrt) + by (simp add: less_sets_def sorted_wrt_append) lemma Sup_nat_less_sets_singleton: fixes n::nat assumes "Sup T < n" "finite T" shows "less_sets T {n}" using assms Max_less_iff by (auto simp: Sup_nat_def less_sets_def split: if_split_asm) end diff --git a/thys/Ordinal_Partitions/Library_Additions.thy b/thys/Ordinal_Partitions/Library_Additions.thy --- a/thys/Ordinal_Partitions/Library_Additions.thy +++ b/thys/Ordinal_Partitions/Library_Additions.thy @@ -1,338 +1,338 @@ section \Library additions\ theory Library_Additions imports "ZFC_in_HOL.Ordinal_Exp" "HOL-Library.Ramsey" "Nash_Williams.Nash_Williams" begin lemma finite_enumerate_Diff_singleton: fixes S :: "'a::wellorder set" assumes "finite S" and i: "i < card S" "enumerate S i < x" shows "enumerate (S - {x}) i = enumerate S i" using i proof (induction i) case 0 have "(LEAST i. i \ S \ i\x) = (LEAST i. i \ S)" proof (rule Least_equality) have "\t. t \ S \ t\x" using 0 \finite S\ finite_enumerate_in_set by blast then show "(LEAST i. i \ S) \ S \ (LEAST i. i \ S) \ x" by (metis "0.prems"(2) LeastI enumerate_0 not_less_Least) qed (simp add: Least_le) then show ?case by (auto simp: enumerate_0) next case (Suc i) then have x: "enumerate S i < x" by (meson enumerate_step finite_enumerate_step less_trans) have cardSx: "Suc i < card (S - {x})" and "i < card S" using Suc \finite S\ card_Diff_singleton_if finite_enumerate_Ex by fastforce+ have "(LEAST s. s \ S \ s\x \ enumerate (S - {x}) i < s) = (LEAST s. s \ S \ enumerate S i < s)" (is "_ = ?r") proof (intro Least_equality conjI) show "?r \ S" by (metis (lifting) LeastI Suc.prems(1) assms(1) finite_enumerate_in_set finite_enumerate_step) show "?r \ x" using Suc.prems not_less_Least [of _ "\t. t \ S \ enumerate S i < t"] \finite S\ finite_enumerate_in_set finite_enumerate_step by blast show "enumerate (S - {x}) i < ?r" by (metis (full_types) Suc.IH Suc.prems(1) \i < card S\ enumerate_Suc'' enumerate_step finite_enumerate_Suc'' finite_enumerate_step x) show "\y. y \ S \ y \ x \ enumerate (S - {x}) i < y \ ?r \ y" by (simp add: Least_le Suc.IH \i < card S\ x) qed then show ?case using Suc assms by (simp add: finite_enumerate_Suc'' cardSx) qed lemma hd_lex: "\hd ms < hd ns; length ms = length ns; ns \ []\ \ (ms, ns) \ lex less_than" by (metis hd_Cons_tl length_0_conv less_than_iff lexord_cons_cons lexord_lex) lemma sorted_hd_le: assumes "sorted xs" "x \ list.set xs" shows "hd xs \ x" using assms by (induction xs) (auto simp: less_imp_le) lemma sorted_le_last: assumes "sorted xs" "x \ list.set xs" shows "x \ last xs" using assms by (induction xs) (auto simp: less_imp_le) lemma hd_list_of: assumes "finite A" "A \ {}" shows "hd (sorted_list_of_set A) = Min A" proof (rule antisym) have "Min A \ A" by (simp add: assms) then show "hd (sorted_list_of_set A) \ Min A" by (simp add: sorted_hd_le \finite A\) next show "Min A \ hd (sorted_list_of_set A)" by (metis Min_le assms hd_in_set set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) qed lemma sorted_hd_le_last: assumes "sorted xs" "xs \ []" shows "hd xs \ last xs" using assms by (simp add: sorted_hd_le) lemma sorted_list_of_set_set_of [simp]: "strict_sorted l \ sorted_list_of_set (list.set l) = l" by (simp add: strict_sorted_equal) lemma range_strict_mono_ext: fixes f::"nat \ 'a::linorder" assumes eq: "range f = range g" and sm: "strict_mono f" "strict_mono g" shows "f = g" proof fix n show "f n = g n" proof (induction n rule: less_induct) case (less n) obtain x y where xy: "f n = g y" "f x = g n" by (metis eq imageE rangeI) then have "n = y" by (metis (no_types) less.IH neq_iff sm strict_mono_less xy) then show ?case using xy by auto qed qed subsection \Other material\ definition strict_mono_sets :: "['a::order set, 'a::order \ 'b::order set] \ bool" where "strict_mono_sets A f \ \x\A. \y\A. x < y \ less_sets (f x) (f y)" lemma strict_mono_setsD: assumes "strict_mono_sets A f" "x < y" "x \ A" "y \ A" shows "less_sets (f x) (f y)" using assms by (auto simp: strict_mono_sets_def) lemma strict_mono_on_o: "\strict_mono_on r A; strict_mono_on s B; s  B \ A\ \ strict_mono_on (r \ s) B" by (auto simp: image_subset_iff strict_mono_on_def) lemma strict_mono_sets_imp_disjoint: fixes A :: "'a::linorder set" assumes "strict_mono_sets A f" shows "pairwise (\x y. disjnt (f x) (f y)) A" using assms unfolding strict_mono_sets_def pairwise_def by (meson antisym_conv3 disjnt_sym less_sets_imp_disjnt) lemma strict_mono_sets_subset: assumes "strict_mono_sets B f" "A \ B" shows "strict_mono_sets A f" using assms by (auto simp: strict_mono_sets_def) lemma strict_mono_less_sets_Min: assumes "strict_mono_sets I f" "finite I" "I \ {}" shows "less_sets (f (Min I)) (\ (f  (I - {Min I})))" using assms by (simp add: strict_mono_sets_def less_sets_UN2 dual_order.strict_iff_order) lemma pair_less_iff1 [simp]: "((x,y), (x,z)) \ pair_less \ y" "\\{}" "\A. A \ \ \ infinite A" and "\A B. \A \ \; B \ \\ \ A \ B \ \" shows "infinite (\\)" by (simp add: assms finite_Inf_in) lemma atLeast_less_sets: "\less_sets A {x}; B \ {x..}\ \ less_sets A B" by (force simp: less_sets_def subset_iff) subsection \The list-of function\ lemma sorted_list_of_set_insert_cons: assumes "finite A" "less_sets {a} A" shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A" proof - have "strict_sorted (a # sorted_list_of_set A)" using assms less_setsD by auto moreover have "list.set (a # sorted_list_of_set A) = insert a A" using assms by force moreover have "length (a # sorted_list_of_set A) = card (insert a A)" using assms card_insert_if less_setsD by fastforce ultimately show ?thesis by (metis \finite A\ finite_insert sorted_list_of_set_unique) qed lemma sorted_list_of_set_Un: assumes AB: "less_sets A B" and fin: "finite A" "finite B" shows "sorted_list_of_set (A \ B) = sorted_list_of_set A @ sorted_list_of_set B" proof - have "strict_sorted (sorted_list_of_set A @ sorted_list_of_set B)" using AB unfolding less_sets_def - by (metis fin set_sorted_list_of_set sorted_wrt_append strict_sorted_list_of_set strict_sorted_sorted_wrt) + by (metis fin set_sorted_list_of_set sorted_wrt_append strict_sorted_list_of_set) moreover have "card A + card B = card (A \ B)" using less_sets_imp_disjnt [OF AB] by (simp add: assms card_Un_disjoint disjnt_def) ultimately show ?thesis by (simp add: assms strict_sorted_equal) qed lemma sorted_list_of_set_UN_lessThan: fixes k::nat assumes sm: "strict_mono_sets {..i. i < k \ finite (A i)" shows "sorted_list_of_set (\i A) (sorted_list_of_set {.. (A  {.. (A  {.. (A  {.. A k)" by (simp add: Un_commute lessThan_Suc) also have "\ = sorted_list_of_set (\ (A  {.. = concat (map (sorted_list_of_set \ A) (sorted_list_of_set {.. = concat (map (sorted_list_of_set \ A) (sorted_list_of_set {..i. i \ k \ finite (A i)" shows "sorted_list_of_set (\i\k. A i) = concat (map (sorted_list_of_set \ A) (sorted_list_of_set {..k}))" by (metis assms lessThan_Suc_atMost less_Suc_eq_le sorted_list_of_set_UN_lessThan) subsection \Monotonic enumeration of a countably infinite set\ abbreviation "enum \ enumerate" text \Could be generalised to infinite countable sets of any type\ lemma nat_infinite_iff: fixes N :: "nat set" shows "infinite N \ (\f::nat\nat. N = range f \ strict_mono f)" proof safe assume "infinite N" then show "\f. N = range (f::nat \ nat) \ strict_mono f" by (metis bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_mono_def) next fix f :: "nat \ nat" assume "strict_mono f" and "N = range f" and "finite (range f)" then show False using range_inj_infinite strict_mono_imp_inj_on by blast qed lemma enum_works: fixes N :: "nat set" assumes "infinite N" shows "N = range (enum N) \ strict_mono (enum N)" by (metis assms bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_monoI) lemma range_enum: "range (enum N) = N" and strict_mono_enum: "strict_mono (enum N)" if "infinite N" for N :: "nat set" using enum_works [OF that] by auto lemma enum_0_eq_Inf: fixes N :: "nat set" assumes "infinite N" shows "enum N 0 = Inf N" proof - have "enum N 0 \ N" using assms range_enum by auto moreover have "\x. x \ N \ enum N 0 \ x" by (metis (mono_tags, hide_lams) assms imageE le0 less_mono_imp_le_mono range_enum strict_monoD strict_mono_enum) ultimately show ?thesis by (metis cInf_eq_minimum) qed lemma enum_works_finite: fixes N :: "nat set" assumes "finite N" shows "N = enum N  {.. strict_mono_on (enum N) {.. N" "finite N" obtains i where "i < card N" "x = enum N i" by (metis \x \ N\ \finite N\ enum_works_finite imageE lessThan_iff) lemma enum_0_eq_Inf_finite: fixes N :: "nat set" assumes "finite N" "N \ {}" shows "enum N 0 = Inf N" proof - have "enum N 0 \ N" by (metis Nat.neq0_conv assms empty_is_image enum_works_finite image_eqI lessThan_empty_iff lessThan_iff) moreover have "enum N 0 \ x" if "x \ N" for x proof - obtain i where "i < card N" "x = enum N i" by (metis \x \ N\ \finite N\ enum_obtain_index_finite) with assms show ?thesis by (metis Nat.neq0_conv finite_enumerate_mono less_or_eq_imp_le) qed ultimately show ?thesis by (metis cInf_eq_minimum) qed lemma greaterThan_less_enum: fixes N :: "nat set" assumes "N \ {x<..}" "infinite N" shows "x < enum N i" using assms range_enum by fastforce lemma atLeast_le_enum: fixes N :: "nat set" assumes "N \ {x..}" "infinite N" shows "x \ enum N i" using assms range_enum by fastforce lemma less_sets_empty1 [simp]: "less_sets {} A" and less_sets_empty2 [simp]: "less_sets A {}" by (simp_all add: less_sets_def) lemma less_sets_singleton1 [simp]: "less_sets {a} A \ (\x\A. a < x)" and less_sets_singleton2 [simp]: "less_sets A {a} \ (\x\A. x < a)" by (simp_all add: less_sets_def) lemma less_sets_atMost [simp]: "less_sets {..a} A \ (\x\A. a < x)" and less_sets_alLeast [simp]: "less_sets A {a..} \ (\x\A. x < a)" by (auto simp: less_sets_def) lemma less_sets_imp_strict_mono_sets: assumes "\i. less_sets (A i) (A (Suc i))" "\i. i>0 \ A i \ {}" shows "strict_mono_sets UNIV A" proof (clarsimp simp: strict_mono_sets_def) fix i j::nat assume "i < j" then show "less_sets (A i) (A j)" proof (induction "j-i" arbitrary: i j) case (Suc x) then show ?case by (metis Suc_diff_Suc Suc_inject Suc_mono assms less_Suc_eq less_sets_trans zero_less_Suc) qed auto qed lemma less_sets_Suc_Max: assumes "finite A" shows "less_sets A {Suc (Max A)..}" proof (cases "A = {}") case False then show ?thesis by (simp add: assms less_Suc_eq_le) qed auto lemma infinite_nat_greaterThan: fixes m::nat assumes "infinite N" shows "infinite (N \ {m<..})" proof - have "N \ -{m<..} \ (N \ {m<..})" by blast moreover have "finite (-{m<..})" by simp ultimately show ?thesis using assms finite_subset by blast qed end diff --git a/thys/Ordinal_Partitions/Omega_Omega.thy b/thys/Ordinal_Partitions/Omega_Omega.thy --- a/thys/Ordinal_Partitions/Omega_Omega.thy +++ b/thys/Ordinal_Partitions/Omega_Omega.thy @@ -1,4288 +1,4278 @@ section \An ordinal partition theorem by Jean A. Larson\ text \Jean A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$. \emph{Annals of Mathematical Logic}, 6:129–145, 1973.\ theory Omega_Omega imports "HOL-Library.Product_Lexorder" Erdos_Milner begin abbreviation "list_of \ sorted_list_of_set" subsection \Cantor normal form for ordinals below @{term "\\\"}\ text \Unlike @{term Cantor_sum}, there is no list of ordinal exponents, which are instead taken as consecutive. We obtain an order-isomorphism between @{term "\\\"} and increasing lists of natural numbers (ordered lexicographically).\ fun omega_sum_aux where Nil: "omega_sum_aux 0 _ = 0" | Suc: "omega_sum_aux (Suc n) [] = 0" | Cons: "omega_sum_aux (Suc n) (m#ms) = (\\n) * (ord_of_nat m) + omega_sum_aux n ms" abbreviation omega_sum where "omega_sum ms \ omega_sum_aux (length ms) ms" text \A normal expansion has no leading zeroes\ inductive normal:: "nat list \ bool" where normal_Nil[iff]: "normal []" | normal_Cons: "m > 0 \ normal (m#ms)" inductive_simps normal_Cons_iff [simp]: "normal (m#ms)" lemma omega_sum_0_iff [simp]: "normal ns \ omega_sum ns = 0 \ ns = []" by (induction ns rule: normal.induct) auto lemma Ord_omega_sum_aux [simp]: "Ord (omega_sum_aux k ms)" by (induction rule: omega_sum_aux.induct) auto lemma Ord_omega_sum: "Ord (omega_sum ms)" by simp lemma omega_sum_less_\\ [intro]: "omega_sum ms < \\\" proof (induction ms) case (Cons m ms) have "\ \ (length ms) * ord_of_nat m \ elts (\ \ Suc (length ms))" using Ord_mem_iff_lt by auto then have "\$$length ms) * ord_of_nat m \ elts (\\$$" using Ord_ord_of_nat oexp_mono_le omega_nonzero ord_of_nat_le_omega by blast with Cons show ?case by (auto simp: mult_succ OrdmemD oexp_less indecomposableD indecomposable_\_power) qed (auto simp: zero_less_Limit) lemma omega_sum_aux_less: "omega_sum_aux k ms < \ \ k" proof (induction rule: omega_sum_aux.induct) case (3 n m ms) have " \\n * ord_of_nat m + \\n < \\n * \" by (metis Ord_ord_of_nat \_power_succ_gtr mult_succ oexp_succ ord_of_nat.simps(2)) with 3 show ?case using dual_order.strict_trans by force qed auto lemma omega_sum_less: "omega_sum ms < \ \ (length ms)" by (rule omega_sum_aux_less) lemma omega_sum_ge: "m \ 0 \ \ \ (length ms) \ omega_sum (m#ms)" apply clarsimp by (metis Ord_ord_of_nat add_le_cancel_left0 le_mult Nat.neq0_conv ord_of_eq_0_iff vsubsetD) lemma omega_sum_length_less: assumes "normal ns" "length ms < length ns" shows "omega_sum ms < omega_sum ns" using assms proof (induction rule: normal.induct) case (normal_Cons n ns') have "\ \ length ms \ \ \ length ns'" using normal_Cons oexp_mono_le by auto then show ?case by (metis gr_implies_not_zero less_le_trans normal_Cons.hyps omega_sum_aux_less omega_sum_ge) qed auto lemma omega_sum_length_leD: assumes "omega_sum ms \ omega_sum ns" "normal ms" shows "length ms \ length ns" by (meson assms leD leI omega_sum_length_less) lemma omega_sum_less_eqlen_iff_cases [simp]: assumes "length ms = length ns" shows "omega_sum (m#ms) < omega_sum (n#ns) \ m m=n \ omega_sum ms < omega_sum ns" (is "?lhs = ?rhs") proof assume L: ?lhs have "\ Suc n < Suc m" using omega_sum_less [of ms] omega_sum_less [of ns] L assms mult_nat_less_add_less by fastforce with L assms show ?rhs by auto qed (auto simp: mult_nat_less_add_less omega_sum_aux_less assms) lemma omega_sum_lex_less_iff_cases: "((length ms, omega_sum (m#ms)), (length ns, omega_sum (n#ns))) \ less_than <*lex*> VWF \ length ms < length ns \ length ms = length ns \ m m=n \ ((length ms, omega_sum ms), (length ns, omega_sum ns)) \ less_than <*lex*> VWF" using omega_sum_less_eqlen_iff_cases by force lemma omega_sum_less_iff_cases: assumes "m > 0" "n > 0" shows "omega_sum (m#ms) < omega_sum (n#ns) \ length ms < length ns \ length ms = length ns \ m length ms = length ns \ m=n \ omega_sum ms < omega_sum ns" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis Suc_less_eq \m>0\ length_Cons less_asym nat_neq_iff normal_Cons omega_sum_length_less omega_sum_less_eqlen_iff_cases) next assume ?rhs then show ?lhs by (metis (full_types) Suc_less_eq \n>0\ length_Cons normal_Cons omega_sum_length_less omega_sum_less_eqlen_iff_cases) qed lemma omega_sum_less_iff: "((length ms, omega_sum ms), (length ns, omega_sum ns)) \ less_than <*lex*> VWF \ (ms,ns) \ lenlex less_than" proof (induction ms arbitrary: ns) case (Cons m ms) then show ?case proof (induction ns) case (Cons n ns') show ?case using Cons.prems Cons_lenlex_iff omega_sum_less_eqlen_iff_cases by fastforce qed auto qed auto lemma eq_omega_sum_less_iff: assumes "length ms = length ns" shows "(omega_sum ms, omega_sum ns) \ VWF \ (ms,ns) \ lenlex less_than" by (metis assms in_lex_prod less_not_refl less_than_iff omega_sum_less_iff) lemma eq_omega_sum_eq_iff: assumes "length ms = length ns" shows "omega_sum ms = omega_sum ns \ ms=ns" proof assume "omega_sum ms = omega_sum ns" then have "(omega_sum ms, omega_sum ns) \ VWF" "(omega_sum ns, omega_sum ms) \ VWF" by auto then obtain "(ms,ns) \ lenlex less_than" "(ns,ms) \ lenlex less_than" using assms eq_omega_sum_less_iff by metis moreover have "total (lenlex less_than)" by (simp add: total_lenlex total_less_than) ultimately show "ms=ns" by (meson UNIV_I total_on_def) qed auto lemma inj_omega_sum: "inj_on omega_sum {l. length l = n}" unfolding inj_on_def using eq_omega_sum_eq_iff by fastforce lemma Ex_omega_sum: "\ \ elts (\\n) \ \ns. \ = omega_sum ns \ length ns = n" proof (induction n arbitrary: \) case 0 then show ?case by (rule_tac x="[]" in exI) auto next case (Suc n) then obtain k::nat where k: "\ \ elts (\ \ n * k)" and kmin: "\k'. k' \ \ elts (\ \ n * k')" by (metis Ord_ord_of_nat elts_mult_\E oexp_succ ord_of_nat.simps(2)) show ?case proof (cases k) case (Suc k') then obtain \ where \: "\ = (\ \ n * k') + \" by (metis lessI mult_succ ord_of_nat.simps(2) k kmin mem_plus_V_E) then have \in: "\ \ elts (\ \ n)" using Suc k mult_succ by auto then obtain ns where ns: "\ = omega_sum ns" and len: "length ns = n" using Suc.IH by auto moreover have "omega_sum ns < \\n" using OrdmemD ns \in by auto ultimately show ?thesis by (rule_tac x="k'#ns" in exI) (simp add: \) qed (use k in auto) qed lemma omega_sum_drop [simp]: "omega_sum (dropWhile (\n. n=0) ns) = omega_sum ns" by (induction ns) auto lemma normal_drop [simp]: "normal (dropWhile (\n. n=0) ns)" by (induction ns) auto lemma omega_sum_\\: assumes "\ \ elts (\\\)" obtains ns where "\ = omega_sum ns" "normal ns" proof - obtain ms where "\ = omega_sum ms" using assms Ex_omega_sum by (auto simp: oexp_Limit elts_\) show thesis proof show "\ = omega_sum (dropWhile (\n. n=0) ms)" by (simp add: \\ = omega_sum ms\) show "normal (dropWhile (\n. n=0) ms)" by auto qed qed definition Cantor_\\ :: "V \ nat list" where "Cantor_\\ \ \x. SOME ns. x = omega_sum ns \ normal ns" lemma assumes "\ \ elts (\\\)" shows Cantor_\\: "omega_sum (Cantor_\\ \) = \" and normal_Cantor_\\: "normal (Cantor_\\ \)" by (metis (mono_tags, lifting) Cantor_\\_def assms omega_sum_\\ someI)+ subsection \Larson's set $W(n)$\ definition WW :: "nat list set" where "WW \ {l. strict_sorted l}" fun into_WW :: "nat \ nat list \ nat list" where "into_WW k [] = []" | "into_WW k (n#ns) = (k+n) # into_WW (Suc (k+n)) ns" fun from_WW :: "nat \ nat list \ nat list" where "from_WW k [] = []" | "from_WW k (n#ns) = (n - k) # from_WW (Suc n) ns" lemma from_into_WW [simp]: "from_WW k (into_WW k ns) = ns" by (induction ns arbitrary: k) auto lemma inj_into_WW: "inj (into_WW k)" by (metis from_into_WW injI) lemma into_from_WW_aux: "\strict_sorted ns; \n\list.set ns. k \ n\ \ into_WW k (from_WW k ns) = ns" by (induction ns arbitrary: k) (auto simp: Suc_leI) lemma into_from_WW [simp]: "strict_sorted ns \ into_WW 0 (from_WW 0 ns) = ns" by (simp add: into_from_WW_aux) lemma into_WW_imp_ge: "y \ List.set (into_WW x ns) \ x \ y" by (induction ns arbitrary: x) fastforce+ lemma strict_sorted_into_WW: "strict_sorted (into_WW x ns)" by (induction ns arbitrary: x) (auto simp: dest: into_WW_imp_ge) lemma length_into_WW: "length (into_WW x ns) = length ns" by (induction ns arbitrary: x) auto lemma WW_eq_range_into: "WW = range (into_WW 0)" proof - have "\ns. strict_sorted ns \ ns \ range (into_WW 0)" by (metis into_from_WW rangeI) then show ?thesis by (auto simp: WW_def strict_sorted_into_WW) qed lemma into_WW_lenlex_iff: "(into_WW k ms, into_WW k ns) \ lenlex less_than \ (ms, ns) \ lenlex less_than" proof (induction ms arbitrary: ns k) case Nil then show ?case by simp (metis length_0_conv length_into_WW) next case (Cons m ms) then show ?case by (induction ns) (auto simp: Cons_lenlex_iff length_into_WW) qed lemma wf_llt [simp]: "wf (lenlex less_than)" and trans_llt [simp]: "trans (lenlex less_than)" by blast+ lemma total_llt [simp]: "total_on A (lenlex less_than)" by (meson UNIV_I total_lenlex total_less_than total_on_def) lemma omega_sum_1_less: assumes "(ms,ns) \ lenlex less_than" shows "omega_sum (1#ms) < omega_sum (1#ns)" proof - have "omega_sum (1#ms) < omega_sum (1#ns)" if "length ms < length ns" using omega_sum_less_iff_cases that zero_less_one by blast then show ?thesis using assms by (auto simp: mult_succ simp flip: omega_sum_less_iff) qed lemma ordertype_WW_1: "ordertype WW (lenlex less_than) \ ordertype UNIV (lenlex less_than)" by (rule ordertype_mono) auto lemma ordertype_WW_2: "ordertype UNIV (lenlex less_than) \ \\\" proof (rule ordertype_inc_le_Ord) show "range (\ms. omega_sum (1#ms)) \ elts (\\\)" by (meson Ord_\ Ord_mem_iff_lt Ord_oexp Ord_omega_sum image_subset_iff omega_sum_less_\\) qed (use omega_sum_1_less in auto) lemma ordertype_WW_3: "\\\ \ ordertype WW (lenlex less_than)" proof - define \ where "\ \ into_WW 0 \ Cantor_\\" have \\: "\\\ = tp (elts (\\\))" by simp also have "\ \ ordertype WW (lenlex less_than)" proof (rule ordertype_inc_le) fix \ \ assume \: "\ \ elts (\\\)" and \: "\ \ elts (\\\)" and "(\, \) \ VWF" then obtain *: "Ord \" "Ord \" "\<\" by (metis Ord_in_Ord Ord_ordertype VWF_iff_Ord_less \\) then have "length (Cantor_\\ \) \ length (Cantor_\\ \)" using \ \ by (simp add: Cantor_\\ normal_Cantor_\\ omega_sum_length_leD) with \ \ * have "(Cantor_\\ \, Cantor_\\ \) \ lenlex less_than" by (auto simp: Cantor_\\ simp flip: omega_sum_less_iff) then show "(\ \, \ \) \ lenlex less_than" by (simp add: \_def into_WW_lenlex_iff) qed (auto simp: \_def WW_def strict_sorted_into_WW) finally show "\\\ \ ordertype WW (lenlex less_than)" . qed lemma ordertype_WW: "ordertype WW (lenlex less_than) = \\\" and ordertype_UNIV_\\: "ordertype UNIV (lenlex less_than) = \\\" using ordertype_WW_1 ordertype_WW_2 ordertype_WW_3 by auto lemma ordertype_\\: fixes F :: "nat \ nat list set" assumes "\j::nat. ordertype (F j) (lenlex less_than) = \\j" shows "ordertype (\j. F j) (lenlex less_than) = \\\" proof (rule antisym) show "ordertype (\ (range F)) (lenlex less_than) \ \ \ \" by (metis ordertype_UNIV_\\ ordertype_mono small top_greatest trans_llt wf_llt) have "\n. \ \ ord_of_nat n \ ordertype (\ (range F)) (lenlex less_than)" by (metis TC_small Union_upper assms ordertype_mono rangeI trans_llt wf_llt) then show "\ \ \ \ ordertype (\ (range F)) (lenlex less_than)" by (auto simp: oexp_\_Limit ZFC_in_HOL.SUP_le_iff elts_\) qed definition WW_seg :: "nat \ nat list set" where "WW_seg n \ {l \ WW. length l = n}" lemma WW_seg_subset_WW: "WW_seg n \ WW" by (auto simp: WW_seg_def) lemma WW_eq_UN_WW_seg: "WW = (\ n. WW_seg n)" by (auto simp: WW_seg_def) lemma ordertype_list_seg: "ordertype {l. length l = n} (lenlex less_than) = \\n" proof - have "bij_betw omega_sum {l. length l = n} (elts (\\n))" unfolding WW_seg_def bij_betw_def by (auto simp: inj_omega_sum Ord_mem_iff_lt omega_sum_less dest: Ex_omega_sum) then show ?thesis by (force simp: ordertype_eq_iff simp flip: eq_omega_sum_less_iff) qed lemma ordertype_WW_seg: "ordertype (WW_seg n) (lenlex less_than) = \\n" (is "ordertype ?W ?R = \\n") proof - have "ordertype {l. length l = n} ?R = ordertype ?W ?R" proof (subst ordertype_eq_ordertype) show "\f. bij_betw f {l. length l = n} ?W \ (\x\{l. length l = n}. \y\{l. length l = n}. ((f x, f y) \ lenlex less_than) = ((x, y) \ lenlex less_than))" proof (intro exI conjI) have "inj_on (into_WW 0) {l. length l = n}" by (metis from_into_WW inj_onI) then show "bij_betw (into_WW 0) {l. length l = n} ?W" by (auto simp: bij_betw_def WW_seg_def WW_eq_range_into length_into_WW) qed (simp add: into_WW_lenlex_iff) qed auto then show ?thesis using ordertype_list_seg by auto qed subsection \Definitions required for the lemmas\ subsubsection \Larson's "$<$"-relation on ordered lists\ instantiation list :: (ord)ord begin definition "xs < ys \ xs \ [] \ ys \ [] \ last xs < hd ys" for xs ys :: "'a list" definition "xs \ ys \ xs < ys \ xs = ys" for xs ys :: "'a list" instance by standard end lemma less_Nil [simp]: "xs < []" "[] < xs" by (auto simp: less_list_def) lemma less_sets_imp_list_less: assumes "list.set xs \ list.set ys" shows "xs < ys" by (metis assms last_in_set less_list_def less_sets_def list.set_sel(1)) lemma less_sets_imp_sorted_list_of_set: assumes "A \ B" "finite A" "finite B" shows "list_of A < list_of B" by (simp add: assms less_sets_imp_list_less) lemma sorted_list_of_set_imp_less_sets: assumes "xs < ys" "sorted xs" "sorted ys" shows "list.set xs \ list.set ys" using assms sorted_hd_le sorted_le_last by (force simp: less_list_def less_sets_def intro: order.trans) lemma less_list_iff_less_sets: assumes "sorted xs" "sorted ys" shows "xs < ys \ list.set xs \ list.set ys" using assms sorted_hd_le sorted_le_last by (force simp: less_list_def less_sets_def intro: order.trans) lemma strict_sorted_append_iff: "strict_sorted (xs @ ys) \ xs < ys \ strict_sorted xs \ strict_sorted ys" (is "?lhs = ?rhs") -proof - assume ?lhs then show ?rhs - by (auto simp: sorted_wrt_append strict_sorted_sorted_wrt less_list_def) -next - assume R: ?rhs - then have "\x y. \x \ list.set xs; y \ list.set ys\ \ x < y" - using less_setsD sorted_list_of_set_imp_less_sets strict_sorted_imp_sorted by blast - with R show ?lhs - by (metis sorted_wrt_append strict_sorted_sorted_wrt) -qed + by (metis less_list_iff_less_sets less_setsD sorted_wrt_append strict_sorted_imp_less_sets strict_sorted_imp_sorted) lemma singleton_less_list_iff: "sorted xs \ [n] < xs \ {..n} \ list.set xs = {}" apply (simp add: less_list_def disjoint_iff) by (metis empty_iff less_le_trans list.set(1) list.set_sel(1) not_le sorted_hd_le) lemma less_hd_imp_less: "xs < [hd ys] \ xs < ys" by (simp add: less_list_def) lemma strict_sorted_concat_I: assumes "\x. x \ list.set xs \ strict_sorted x" "\n. Suc n < length xs \ xs!n < xs!Suc n" "xs \ lists (- {[]})" shows "strict_sorted (concat xs)" using assms proof (induction xs) case (Cons x xs) then have "x < concat xs" apply (simp add: less_list_def) by (metis Compl_iff hd_concat insertI1 length_greater_0_conv length_pos_if_in_set list.sel(1) lists.cases nth_Cons_0) with Cons show ?case by (force simp: strict_sorted_append_iff) qed auto subsection \Nash Williams for lists\ subsubsection \Thin sets of lists\ inductive initial_segment :: "'a list \ 'a list \ bool" where "initial_segment xs (xs@ys)" definition thin :: "'a list set \ bool" where "thin A \ \ (\x y. x \ A \ y \ A \ x \ y \ initial_segment x y)" lemma initial_segment_ne: assumes "initial_segment xs ys" "xs \ []" shows "ys \ [] \ hd ys = hd xs" using assms by (auto elim!: initial_segment.cases) lemma take_initial_segment: assumes "initial_segment xs ys" "k \ length xs" shows "take k xs = take k ys" by (metis append_eq_conv_conj assms initial_segment.cases min_def take_take) lemma initial_segment_length_eq: assumes "initial_segment xs ys" "length xs = length ys" shows "xs = ys" using assms initial_segment.cases by fastforce lemma initial_segment_Nil [simp]: "initial_segment [] ys" by (simp add: initial_segment.simps) lemma initial_segment_Cons [simp]: "initial_segment (x#xs) (y#ys) \ x=y \ initial_segment xs ys" by (metis append_Cons initial_segment.simps list.inject) lemma init_segment_iff_initial_segment: assumes "strict_sorted xs" "strict_sorted ys" shows "init_segment (list.set xs) (list.set ys) \ initial_segment xs ys" (is "?lhs = ?rhs") proof assume ?lhs then obtain S' where S': "list.set ys = list.set xs \ S'" "list.set xs \ S'" by (auto simp: init_segment_def) then have "finite S'" by (metis List.finite_set finite_Un) have "ys = xs @ list_of S'" using S' \strict_sorted xs\ proof (induction xs) case Nil with \strict_sorted ys\ show ?case by auto next case (Cons a xs) with \finite S'\ have "ys = a # xs @ list_of S'" by (metis List.finite_set append_Cons assms(2) sorted_list_of_set_Un sorted_list_of_set_set_of) then show ?case by (auto simp: Cons) qed then show ?rhs using initial_segment.intros by blast next assume ?rhs then show ?lhs proof cases case (1 ys) with assms(2) show ?thesis by (metis init_segment_def set_append sorted_list_of_set_imp_less_sets strict_sorted_append_iff strict_sorted_imp_sorted) qed qed theorem Nash_Williams_WW: fixes h :: "nat list \ nat" assumes "infinite M" and h: "h  {l \ A. List.set l \ M} \ {..<2}" and "thin A" "A \ WW" obtains i N where "i < 2" "infinite N" "N \ M" "h  {l \ A. List.set l \ N} \ {i}" proof - define AM where "AM \ {l \ A. List.set l \ M}" have "thin_set (list.set  A)" using \thin A\ \A \ WW\ unfolding thin_def thin_set_def WW_def by (auto simp: subset_iff init_segment_iff_initial_segment) then have "thin_set (list.set  AM)" by (simp add: AM_def image_subset_iff thin_set_def) then have "Ramsey (list.set  AM) 2" using Nash_Williams_2 by metis moreover have "(h \ list_of) \ list.set  AM \ {..<2}" unfolding AM_def proof clarsimp fix l assume "l \ A" "list.set l \ M" then have "strict_sorted l" using WW_def \A \ WW\ by blast then show "h (list_of (list.set l)) < 2" using h \l \ A\ \list.set l \ M\ by auto qed ultimately obtain N i where N: "N \ M" "infinite N" "i<2" and "list.set  AM \ Pow N \ (h \ list_of) - {i}" unfolding Ramsey_eq by (metis \infinite M\) then have N_disjoint: "(h \ list_of) - {1-i} \ (list.set  AM) \ Pow N = {}" unfolding subset_vimage_iff less_2_cases_iff by force have "h  {l \ A. list.set l \ N} \ {i}" proof clarify fix l assume "l \ A" and "list.set l \ N" then have "h l < 2" using h \N \ M\ by force with \i<2\ have "h l \ Suc 0 - i \ h l = i" by (auto simp: eval_nat_numeral less_Suc_eq) moreover have "strict_sorted l" using \A \ WW\ \l \ A\ unfolding WW_def by blast moreover have "h (list_of (list.set l)) = 1 - i \ \ (list.set l \ N)" using N_disjoint \N \ M\ \l \ A\ by (auto simp: AM_def) ultimately show "h l = i" using N \N \ M\ \l \ A\ \list.set l \ N\ by (auto simp: vimage_def set_eq_iff AM_def WW_def subset_iff) qed then show thesis using that \i<2\ N by auto qed subsection \Specialised functions on lists\ lemma mem_lists_non_Nil: "xss \ lists (- {[]}) \ (\x \ list.set xss. x \ [])" by auto fun acc_lengths :: "nat \ 'a list list \ nat list" where "acc_lengths acc [] = []" | "acc_lengths acc (l#ls) = (acc + length l) # acc_lengths (acc + length l) ls" lemma length_acc_lengths [simp]: "length (acc_lengths acc ls) = length ls" by (induction ls arbitrary: acc) auto lemma acc_lengths_eq_Nil_iff [simp]: "acc_lengths acc ls = [] \ ls = []" by (metis length_0_conv length_acc_lengths) lemma set_acc_lengths: assumes "ls \ lists (- {[]})" shows "list.set (acc_lengths acc ls) \ {acc<..}" using assms by (induction ls rule: acc_lengths.induct) fastforce+ text \Useful because @{text acc_lengths.simps} will sometimes be deleted from the simpset.\ lemma hd_acc_lengths [simp]: "hd (acc_lengths acc (l#ls)) = acc + length l" by simp lemma last_acc_lengths [simp]: "ls \ [] \ last (acc_lengths acc ls) = acc + sum_list (map length ls)" by (induction acc ls rule: acc_lengths.induct) auto lemma nth_acc_lengths [simp]: "\ls \ []; k < length ls\ \ acc_lengths acc ls ! k = acc + sum_list (map length (take (Suc k) ls))" by (induction acc ls arbitrary: k rule: acc_lengths.induct) (fastforce simp: less_Suc_eq nth_Cons')+ lemma acc_lengths_plus: "acc_lengths (m+n) as = map ((+)m) (acc_lengths n as)" by (induction n as arbitrary: m rule: acc_lengths.induct) (auto simp: add.assoc) lemma acc_lengths_shift: "NO_MATCH 0 acc \ acc_lengths acc as = map ((+)acc) (acc_lengths 0 as)" by (metis acc_lengths_plus add.comm_neutral) lemma length_concat_acc_lengths: "ls \ [] \ k + length (concat ls) \ list.set (acc_lengths k ls)" by (metis acc_lengths_eq_Nil_iff last_acc_lengths last_in_set length_concat) lemma strict_sorted_acc_lengths: assumes "ls \ lists (- {[]})" shows "strict_sorted (acc_lengths acc ls)" using assms proof (induction ls rule: acc_lengths.induct) case (2 acc l ls) then have "strict_sorted (acc_lengths (acc + length l) ls)" by auto then show ?case using set_acc_lengths "2.prems" by auto qed auto lemma acc_lengths_append: "acc_lengths acc (xs @ ys) = acc_lengths acc xs @ acc_lengths (acc + sum_list (map length xs)) ys" by (induction acc xs rule: acc_lengths.induct) (auto simp: add.assoc) lemma length_concat_ge: assumes "as \ lists (- {[]})" shows "length (concat as) \ length as" using assms proof (induction as) case (Cons a as) then have "length a \ Suc 0" "\l. l \ list.set as \ length l \ Suc 0" by (auto simp: Suc_leI) then show ?case using Cons.IH by force qed auto fun interact :: "'a list list \ 'a list list \ 'a list" where "interact [] ys = concat ys" | "interact xs [] = concat xs" | "interact (x#xs) (y#ys) = x @ y @ interact xs ys" lemma (in monoid_add) length_interact: "length (interact xs ys) = sum_list (map length xs) + sum_list (map length ys)" by (induction rule: interact.induct) (auto simp: length_concat) lemma length_interact_ge: assumes "xs \ lists (- {[]})" "ys \ lists (- {[]})" shows "length (interact xs ys) \ length xs + length ys" by (metis add_mono assms length_concat length_concat_ge length_interact) lemma set_interact [simp]: shows "list.set (interact xs ys) = list.set (concat xs) \ list.set (concat ys)" by (induction rule: interact.induct) auto lemma interact_eq_Nil_iff [simp]: assumes "xs \ lists (- {[]})" "ys \ lists (- {[]})" shows "interact xs ys = [] \ xs=[] \ ys=[]" using length_interact_ge [OF assms] by fastforce lemma interact_sing [simp]: "interact [x] ys = x @ concat ys" by (metis (no_types) concat.simps(2) interact.simps neq_Nil_conv) lemma hd_interact: "\xs \ []; hd xs \ []\ \ hd (interact xs ys) = hd (hd xs)" by (smt (verit, best) hd_append2 hd_concat interact.elims list.sel(1)) lemma acc_lengths_concat_injective: assumes "concat as' = concat as" "acc_lengths n as' = acc_lengths n as" shows "as' = as" using assms proof (induction as arbitrary: n as') case Nil then show ?case by (metis acc_lengths_eq_Nil_iff) next case (Cons a as) then obtain a' bs where "as' = a'#bs" by (metis Suc_length_conv length_acc_lengths) with Cons show ?case by simp qed lemma acc_lengths_interact_injective: assumes "interact as' bs' = interact as bs" "acc_lengths a as' = acc_lengths a as" "acc_lengths b bs' = acc_lengths b bs" shows "as' = as \ bs' = bs" using assms proof (induction as bs arbitrary: a b as' bs' rule: interact.induct) case (1 cs) then show ?case by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(1)) next case (2 c cs) then show ?case by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(2) list.exhaust) next case (3 x xs y ys) then obtain a' us b' vs where "as' = a'#us" "bs' = b'#vs" by (metis length_Suc_conv length_acc_lengths) with 3 show ?case by auto qed lemma strict_sorted_interact_I: assumes "length ys \ length xs" "length xs \ Suc (length ys)" "\x. x \ list.set xs \ strict_sorted x" "\y. y \ list.set ys \ strict_sorted y" "\n. n < length ys \ xs!n < ys!n" "\n. Suc n < length xs \ ys!n < xs!Suc n" assumes "xs \ lists (- {[]})" "ys \ lists (- {[]})" shows "strict_sorted (interact xs ys)" using assms proof (induction rule: interact.induct) case (3 x xs y ys) then have "x < y" by force moreover have "strict_sorted (interact xs ys)" using 3 by simp (metis Suc_less_eq nth_Cons_Suc) moreover have "y < interact xs ys" using 3 apply (simp add: less_list_def) by (metis hd_interact le_zero_eq length_greater_0_conv list.sel(1) list.set_sel(1) list.size(3) lists.simps mem_lists_non_Nil nth_Cons_0) ultimately show ?case using 3 by (simp add: strict_sorted_append_iff less_list_def) qed auto subsection \Forms and interactions\ subsubsection \Forms\ inductive Form_Body :: "[nat, nat, nat list, nat list, nat list] \ bool" where "Form_Body ka kb xs ys zs" if "length xs < length ys" "xs = concat (a#as)" "ys = concat (b#bs)" "a#as \ lists (- {[]})" "b#bs \ lists (- {[]})" "length (a#as) = ka" "length (b#bs) = kb" "c = acc_lengths 0 (a#as)" "d = acc_lengths 0 (b#bs)" "zs = concat [c, a, d, b] @ interact as bs" "strict_sorted zs" inductive Form :: "[nat, nat list set] \ bool" where "Form 0 {xs,ys}" if "length xs = length ys" "xs \ ys" | "Form (2*k-1) {xs,ys}" if "Form_Body k k xs ys zs" "k > 0" | "Form (2*k) {xs,ys}" if "Form_Body (Suc k) k xs ys zs" "k > 0" inductive_cases Form_0_cases_raw: "Form 0 u" lemma Form_elim_upair: assumes "Form l U" obtains xs ys where "xs \ ys" "U = {xs,ys}" "length xs \ length ys" using assms by (smt (verit, best) Form.simps Form_Body.cases less_or_eq_imp_le nat_neq_iff) lemma assumes "Form_Body ka kb xs ys zs" shows Form_Body_WW: "zs \ WW" and Form_Body_nonempty: "length zs > 0" and Form_Body_length: "length xs < length ys" using Form_Body.cases [OF assms] by (fastforce simp: WW_def)+ lemma form_cases: fixes l::nat obtains (zero) "l = 0" | (nz) ka kb where "l = ka+kb - 1" "0 < kb" "kb \ ka" "ka \ Suc kb" proof - have "l = 0 \ (\ka kb. l = ka+kb - 1 \ 0 < kb \ kb \ ka \ ka \ Suc kb)" by presburger then show thesis using nz zero by blast qed subsubsection \Interactions\ lemma interact: assumes "Form l U" "l>0" obtains ka kb xs ys zs where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys zs" "0 < kb" "kb \ ka" "ka \ Suc kb" using assms unfolding Form.simps by (smt (verit, best) add_Suc diff_Suc_1 lessI mult_2 nat_less_le order_refl) definition inter_scheme :: "nat \ nat list set \ nat list" where "inter_scheme l U \ SOME zs. \k xs ys. U = {xs,ys} \ (l = 2*k-1 \ Form_Body k k xs ys zs \ l = 2*k \ Form_Body (Suc k) k xs ys zs)" lemma inter_scheme: assumes "Form l U" "l>0" obtains ka kb xs ys where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys (inter_scheme l U)" "0 < kb" "kb \ ka" "ka \ Suc kb" using interact [OF \Form l U\] proof cases case (2 ka kb xs ys zs) then have \
: "\ka kb zs. \ Form_Body ka kb ys xs zs" using Form_Body_length less_asym' by blast have "Form_Body ka kb xs ys (inter_scheme l U)" proof (cases "ka = kb") case True with 2 have l: "\k. l \ k * 2" by presburger have [simp]: "\k. kb + kb - Suc 0 = k * 2 - Suc 0 \ k=kb" by auto show ?thesis unfolding inter_scheme_def using 2 l True by (auto simp: \
\l > 0\ Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex) next case False with 2 have l: "\k. l \ k * 2 - Suc 0" and [simp]: "ka = Suc kb" by presburger+ have [simp]: "\k. kb + kb = k * 2 \ k=kb" by auto show ?thesis unfolding inter_scheme_def using 2 l False by (auto simp: \
\l > 0\ Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex) qed then show ?thesis by (simp add: 2 that) qed (use \l > 0\ in auto) lemma inter_scheme_strict_sorted: assumes "Form l U" "l>0" shows "strict_sorted (inter_scheme l U)" using Form_Body.simps assms inter_scheme by fastforce lemma inter_scheme_simple: assumes "Form l U" "l>0" shows "inter_scheme l U \ WW \ length (inter_scheme l U) > 0" using inter_scheme [OF assms] by (meson Form_Body_WW Form_Body_nonempty) subsubsection \Injectivity of interactions\ proposition inter_scheme_injective: assumes "Form l U" "Form l U'" "l > 0" and eq: "inter_scheme l U' = inter_scheme l U" shows "U' = U" proof - obtain ka kb xs ys where l: "l = ka+kb - 1" and U: "U = {xs,ys}" and FB: "Form_Body ka kb xs ys (inter_scheme l U)" and kb: "0 < kb" "kb \ ka" "ka \ Suc kb" using assms inter_scheme by blast then obtain a as b bs c d where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)" and len: "length (a#as) = ka" "length (b#bs) = kb" and c: "c = acc_lengths 0 (a#as)" and d: "d = acc_lengths 0 (b#bs)" and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs" by (auto simp: Form_Body.simps) obtain ka' kb' xs' ys' where l': "l = ka'+kb' - 1" and U': "U' = {xs',ys'}" and FB': "Form_Body ka' kb' xs' ys' (inter_scheme l U')" and kb': "0 < kb'" "kb' \ ka'" "ka' \ Suc kb'" using assms inter_scheme by blast then obtain a' as' b' bs' c' d' where xs': "xs' = concat (a'#as')" and ys': "ys' = concat (b'#bs')" and len': "length (a'#as') = ka'" "length (b'#bs') = kb'" and c': "c' = acc_lengths 0 (a'#as')" and d': "d' = acc_lengths 0 (b'#bs')" and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'" using Form_Body.simps by auto have [simp]: "ka' = ka \ kb' = kb" using \l > 0\ l l' kb kb' le_SucE le_antisym mult_2 by linarith have [simp]: "length c = length c'" "length d = length d'" using c c' d d' len' len by auto have c_off: "c' = c" "a' @ d' @ b' @ interact as' bs' = a @ d @ b @ interact as bs" using eq by (auto simp: Ueq Ueq') then have len_a: "length a' = length a" by (metis acc_lengths.simps(2) add.left_neutral c c' nth_Cons_0) with c_off have \
: "a' = a" "d' = d" "b' @ interact as' bs' = b @ interact as bs" by auto then have "length (interact as' bs') = length (interact as bs)" by (metis acc_lengths.simps(2) add_left_cancel append_eq_append_conv d d' list.inject) with \
have "b' = b" "interact as' bs' = interact as bs" by auto moreover have "acc_lengths 0 as' = acc_lengths 0 as" using \a' = a\ \c' = c\ by (simp add: c' c acc_lengths_shift) moreover have "acc_lengths 0 bs' = acc_lengths 0 bs" using \b' = b\ \d' = d\ by (simp add: d' d acc_lengths_shift) ultimately have "as' = as \ bs' = bs" using acc_lengths_interact_injective by blast then show ?thesis by (simp add: \a' = a\ U U' \b' = b\ xs xs' ys ys') qed lemma strict_sorted_interact_imp_concat: "strict_sorted (interact as bs) \ strict_sorted (concat as) \ strict_sorted (concat bs)" proof (induction as bs rule: interact.induct) case (3 x xs y ys) have "x < concat xs" using "3.prems" - apply (simp add: strict_sorted_append_iff) - by (metis (full_types) Un_iff hd_in_set last_in_set less_list_def set_append set_interact sorted_wrt_append strict_sorted_append_iff strict_sorted_sorted_wrt) + by (smt (verit, del_insts) Un_iff hd_in_set interact.simps(3) last_in_set less_list_def set_append set_interact sorted_wrt_append) moreover have "y < concat ys" - using "3.prems" - by (metis Un_iff hd_in_set interact.simps(3) last_in_set less_list_def set_interact sorted_wrt_append strict_sorted_sorted_wrt) + using 3 sorted_wrt_append strict_sorted_append_iff by fastforce ultimately show ?case using 3 by (auto simp add: strict_sorted_append_iff) qed auto lemma strict_sorted_interact_hd: "\strict_sorted (interact cs ds); cs \ []; ds \ []; hd cs \ []; hd ds \ []\ \ hd (hd cs) < hd (hd ds)" - by (metis Nil_is_append_conv hd_append2 hd_in_set interact.simps(3) list.exhaust_sel sorted_wrt_append strict_sorted_sorted_wrt) + by (metis append_is_Nil_conv hd_append2 hd_in_set interact.simps(3) list.exhaust_sel sorted_wrt_append) text \the lengths of the two lists can differ by one\ proposition interaction_scheme_unique_aux: assumes "concat as = concat as'" and ys': "concat bs = concat bs'" and "as \ lists (- {[]})" "bs \ lists (- {[]})" and "strict_sorted (interact as bs)" and "length bs \ length as" "length as \ Suc (length bs)" and "as' \ lists (- {[]})" "bs' \ lists (- {[]})" and "strict_sorted (interact as' bs')" and "length bs' \ length as'" "length as' \ Suc (length bs')" and "length as = length as'" "length bs = length bs'" shows "as = as' \ bs = bs'" using assms proof (induction "length as" arbitrary: as bs as' bs') case 0 then show ?case by auto next case (Suc k) show ?case proof (cases k) case 0 - then obtain a a' where "as = [a]" "as' = [a']" + then obtain a a' where aa': "as = [a]" "as' = [a']" by (metis Suc.hyps(2) \length as = length as'\ Suc_length_conv length_0_conv) - with 0 show ?thesis - using Suc.prems - apply (simp add: le_Suc_eq) - by (metis concat.simps length_0_conv length_Suc_conv self_append_conv) + show ?thesis + proof + show "as = as'" + using aa' \concat as = concat as'\ by force + with Suc 0 show " bs = bs'" + by (metis Suc_leI append_Nil2 concat.simps impossible_Cons le_antisym length_greater_0_conv list.exhaust) + qed next case (Suc k') then obtain a cs b ds where eq: "as = a#cs" "bs = b#ds" using Suc.prems by (metis Suc.hyps(2) le0 list.exhaust list.size(3) not_less_eq_eq) have "length as' \ 0" using Suc.hyps(2) \length as = length as'\ by force then obtain a' cs' b' ds' where eq': "as' = a'#cs'" "bs' = b'#ds'" by (metis \length bs = length bs'\ eq(2) length_0_conv list.exhaust) obtain k: "k = length cs" "k \ Suc (length ds)" using eq \Suc k = length as\ \length bs \ length as\ \length as \ Suc (length bs)\ by auto case (Suc k') obtain [simp]: "b \ []" "b' \ []" "a \ []" "a' \ []" using Suc.prems by (simp add: eq eq') then have "hd b' = hd b" using Suc.prems(2) by (metis concat.simps(2) eq'(2) eq(2) hd_append2) - have ss_ab: "strict_sorted (concat as)" "strict_sorted (concat bs)" using strict_sorted_interact_imp_concat Suc.prems(5) by blast+ - have "a < b" - by (metis eq Suc.prems(5) append.assoc interact.simps(3) strict_sorted_append_iff) - have sw_ab: "sorted_wrt (<) (a @ b @ interact cs ds)" - by (metis Suc.prems(5) eq interact.simps(3) strict_sorted_sorted_wrt) - then have "hd b \ list.set (concat cs)" - by (metis Un_iff \b \ []\ list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append) - have "b < concat cs" - using eq \strict_sorted (interact as bs)\ - unfolding strict_sorted_append_iff - by (metis Un_iff last_in_set less_list_def list.set_sel(1) set_interact sorted_wrt_append sw_ab) + have sw_ab: "strict_sorted (a @ b @ interact cs ds)" + by (metis Suc.prems(5) eq interact.simps(3)) + then obtain "a < b" "strict_sorted a" "strict_sorted b" + by (metis append_assoc strict_sorted_append_iff) + have b_cs: "strict_sorted (concat (b # cs))" + by (metis append.simps(1) concat.simps(2) interact.simps(3) strict_sorted_interact_imp_concat sw_ab) + then have "b < concat cs" + using strict_sorted_append_iff by auto have "strict_sorted (a @ concat cs)" using eq(1) ss_ab(1) by force - then have b_cs: "strict_sorted (b @ concat cs)" - by (metis \b < concat cs\ strict_sorted_append_iff strict_sorted_sorted_wrt sw_ab) have "list.set a = list.set (concat as) \ {..< hd b}" proof - have "x \ list.set a" if "x < hd b" and "l \ list.set cs" and "x \ list.set l" for x l using b_cs sorted_hd_le strict_sorted_imp_sorted that by fastforce then show ?thesis using \b \ []\ sw_ab by (force simp: strict_sorted_append_iff sorted_wrt_append eq) qed moreover have ss_ab': "strict_sorted (concat as')" "strict_sorted (concat bs')" using strict_sorted_interact_imp_concat Suc.prems(10) by blast+ - have "a' < b'" - by (metis eq' Suc.prems(10) append.assoc interact.simps(3) strict_sorted_append_iff) - have sw_ab': "sorted_wrt (<) (a' @ b' @ interact cs' ds')" - by (metis Suc.prems(10) eq' interact.simps(3) strict_sorted_sorted_wrt) + have sw_ab': "strict_sorted (a' @ b' @ interact cs' ds')" + by (metis Suc.prems(10) eq' interact.simps(3)) + then obtain "a' < b'" "strict_sorted a'" "strict_sorted b'" + by (metis append_assoc strict_sorted_append_iff) + have b_cs': "strict_sorted (concat (b' # cs'))" + by (metis (no_types) Suc.prems(10) append_Nil eq' interact.simps(3) strict_sorted_append_iff strict_sorted_interact_imp_concat) + then have "b' < concat cs'" + by (simp add: strict_sorted_append_iff) then have "hd b' \ list.set (concat cs')" - by (metis Un_iff \b' \ []\ list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append) - have "b' < concat cs'" - using eq' \strict_sorted (interact as' bs')\ - apply (simp add: strict_sorted_append_iff) - by (metis Un_iff last_in_set less_list_def list.set_sel(1) set_interact sorted_wrt_append sw_ab') + by (metis Un_iff \b' \ []\ list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append sw_ab') have "strict_sorted (a' @ concat cs')" using eq'(1) ss_ab'(1) by force then have b_cs': "strict_sorted (b' @ concat cs')" using \b' < concat cs'\ eq'(2) ss_ab'(2) strict_sorted_append_iff by auto have "list.set a' = list.set (concat as') \ {..< hd b'}" proof - have "x \ list.set a'" if "x < hd b'" and "l \ list.set cs'" and "x \ list.set l" for x l using b_cs' sorted_hd_le strict_sorted_imp_sorted that by fastforce then show ?thesis using \b' \ []\ sw_ab' by (force simp: strict_sorted_append_iff sorted_wrt_append eq') qed ultimately have "a=a'" - by (metis Suc.prems(1) \hd b' = hd b\ sorted_wrt_append strict_sorted_equal strict_sorted_sorted_wrt sw_ab sw_ab') + by (simp add: Suc.prems(1) \hd b' = hd b\ \strict_sorted a'\ \strict_sorted a\ strict_sorted_equal) moreover have ccat_cs_cs': "concat cs = concat cs'" using Suc.prems(1) \a = a'\ eq'(1) eq(1) by fastforce have "b=b'" proof (cases "ds = [] \ ds' = []") case True then show ?thesis using \length bs = length bs'\ Suc.prems(2) eq'(2) eq(2) by auto next case False - then have "ds \ []" "ds' \ []" - by auto - have "sorted (concat ds)" "sorted (concat ds')" + then have "ds \ []" "ds' \ []" "sorted (concat ds)" "sorted (concat ds')" using eq(2) ss_ab(2) eq'(2) ss_ab'(2) strict_sorted_append_iff strict_sorted_imp_sorted by auto - have "strict_sorted b" - by (metis Suc.prems(2) concat.simps(2) eq(2) ss_ab'(2) strict_sorted_append_iff) + have "strict_sorted b" "strict_sorted b'" + using b_cs b_cs' sorted_wrt_append by auto moreover have "cs \ []" using k local.Suc by auto then obtain "hd cs \ []" "hd ds \ []" using Suc.prems(3) Suc.prems(4) eq list.set_sel(1) by (simp add: \ds \ []\ mem_lists_non_Nil) then have "concat cs \ []" using \cs \ []\ hd_in_set by auto have "hd (concat cs) < hd (concat ds)" using strict_sorted_interact_hd - by (metis \cs \ []\ \ds \ []\ \hd cs \ []\ \hd ds \ []\ hd_concat strict_sorted_append_iff strict_sorted_sorted_wrt sw_ab) - then have "list.set b = list.set (concat bs) \ {..< hd (concat cs)}" - using ss_ab \b < concat cs\ - apply (auto simp: strict_sorted_append_iff eq) - apply (metis \concat cs \ []\ b_cs hd_in_set sorted_wrt_append strict_sorted_sorted_wrt) - using \sorted (concat ds)\ sorted_hd_le by fastforce + by (metis \cs \ []\ \ds \ []\ \hd cs \ []\ \hd ds \ []\ hd_concat sorted_wrt_append sw_ab) + + have "list.set b = list.set (concat bs) \ {..< hd (concat cs)}" + proof - + have 1: "x \ list.set b" + if "x < hd (concat cs)" and "l \ list.set ds" and "x \ list.set l" for x l + using \hd (concat cs) < hd (concat ds)\ \sorted (concat ds)\ sorted_hd_le that by fastforce + have 2: "l < hd (concat cs)" if "l \ list.set b" for l + by (meson \b < concat cs\ \b \ []\ \concat cs \ []\ \strict_sorted b\ le_less_trans less_list_def sorted_le_last strict_sorted_imp_sorted that) + show ?thesis + using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq) + qed moreover - have "sorted (concat ds')" - using eq'(2) ss_ab'(2) strict_sorted_append_iff strict_sorted_imp_sorted by auto have "cs' \ []" using k local.Suc \concat cs \ []\ ccat_cs_cs' by auto then obtain "hd cs' \ []" "hd ds' \ []" using Suc.prems(8,9) \ds' \ []\ eq'(1) eq'(2) list.set_sel(1) by auto then have "concat cs' \ []" using \cs' \ []\ hd_in_set by auto have "hd (concat cs') < hd (concat ds')" using strict_sorted_interact_hd - by (metis \cs' \ []\ \ds' \ []\ \hd cs' \ []\ \hd ds' \ []\ hd_concat strict_sorted_append_iff strict_sorted_sorted_wrt sw_ab') - then have "list.set b' = list.set (concat bs') \ {..< hd (concat cs')}" - using ss_ab' \b' < concat cs'\ - apply (auto simp: strict_sorted_append_iff eq') - apply (metis \concat cs' \ []\ b_cs' list.set_sel(1) sorted_wrt_append strict_sorted_sorted_wrt) - using \sorted (concat ds')\ sorted_hd_le by fastforce + by (metis \cs' \ []\ \ds' \ []\ \hd cs' \ []\ \hd ds' \ []\ hd_concat sorted_wrt_append sw_ab') + have "list.set b' = list.set (concat bs') \ {..< hd (concat cs')}" + proof - + have 1: "x \ list.set b'" + if "x < hd (concat cs')" and "l \ list.set ds'" and "x \ list.set l" for x l + using \hd (concat cs') < hd (concat ds')\ \sorted (concat ds')\ sorted_hd_le that by fastforce + have 2: "l < hd (concat cs')" if "l \ list.set b'" for l + by (metis \concat cs' \ []\ b_cs' list.set_sel(1) sorted_wrt_append that) + show ?thesis + using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq') + qed ultimately show "b = b'" - by (metis Suc.prems(2) ccat_cs_cs' strict_sorted_append_iff strict_sorted_equal strict_sorted_sorted_wrt sw_ab') + by (simp add: Suc.prems(2) ccat_cs_cs' strict_sorted_equal) qed moreover have "cs = cs' \ ds = ds'" proof (rule Suc.hyps) show "k = length cs" using eq Suc.hyps(2) by auto[1] show "concat ds = concat ds'" using Suc.prems(2) \b = b'\ eq'(2) eq(2) by auto show "strict_sorted (interact cs ds)" using eq Suc.prems(5) strict_sorted_append_iff by auto show "length ds \ length cs" "length cs \ Suc (length ds)" using eq Suc.hyps(2) Suc.prems(6) k by auto show "strict_sorted (interact cs' ds')" using eq' Suc.prems(10) strict_sorted_append_iff by auto show "length cs = length cs'" using Suc.hyps(2) Suc.prems(13) eq'(1) k(1) by force qed (use ccat_cs_cs' eq eq' Suc.prems in auto) ultimately show ?thesis by (simp add: \a = a'\ \b = b'\ eq eq') qed qed proposition Form_Body_unique: assumes "Form_Body ka kb xs ys zs" "Form_Body ka kb xs ys zs'" and "kb \ ka" "ka \ Suc kb" shows "zs' = zs" proof - obtain a as b bs c d where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)" and ne: "a#as \ lists (- {[]})" "b#bs \ lists (- {[]})" and len: "length (a#as) = ka" "length (b#bs) = kb" and c: "c = acc_lengths 0 (a#as)" and d: "d = acc_lengths 0 (b#bs)" and Ueq: "zs = concat [c, a, d, b] @ interact as bs" and ss_zs: "strict_sorted zs" using Form_Body.cases [OF assms(1)] by (metis (no_types)) obtain a' as' b' bs' c' d' where xs': "xs = concat (a'#as')" and ys': "ys = concat (b'#bs')" and ne': "a'#as' \ lists (- {[]})" "b'#bs' \ lists (- {[]})" and len': "length (a'#as') = ka" "length (b'#bs') = kb" and c': "c' = acc_lengths 0 (a'#as')" and d': "d' = acc_lengths 0 (b'#bs')" and Ueq': "zs' = concat [c', a', d', b'] @ interact as' bs'" and ss_zs': "strict_sorted zs'" using Form_Body.cases [OF assms(2)] by (metis (no_types)) have [simp]: "length c = length c'" "length d = length d'" using c c' d d' len' len by auto note acc_lengths.simps [simp del] have "a < b" using ss_zs by (auto simp: Ueq strict_sorted_append_iff less_list_def c d) have "a' < b'" using ss_zs' by (auto simp: Ueq' strict_sorted_append_iff less_list_def c' d') have "a#as = a'#as' \ b#bs = b'#bs'" proof (rule interaction_scheme_unique_aux) show "strict_sorted (interact (a # as) (b # bs))" using ss_zs \a < b\ by (auto simp: Ueq strict_sorted_append_iff less_list_def d) show "strict_sorted (interact (a' # as') (b' # bs'))" using ss_zs' \a' < b'\ by (auto simp: Ueq' strict_sorted_append_iff less_list_def d') show "length (b # bs) \ length (a # as)" "length (b' # bs') \ length (a' # as')" using \kb \ ka\ len len' by auto show "length (a # as) \ Suc (length (b # bs))" using \ka \ Suc kb\ len by linarith then show "length (a' # as') \ Suc (length (b' # bs'))" using len len' by fastforce qed (use len len' xs xs' ys ys' ne ne' in fastforce)+ then show ?thesis using Ueq Ueq' c c' d d' by blast qed lemma Form_Body_imp_inter_scheme: assumes FB: "Form_Body ka kb xs ys zs" and "0 < kb" "kb \ ka" "ka \ Suc kb" shows "zs = inter_scheme ((ka+kb) - Suc 0) {xs,ys}" proof - have "length xs < length ys" by (meson Form_Body_length assms(1)) have [simp]: "a + a = b + b \ a=b" "a + a - Suc 0 = b + b - Suc 0 \ a=b" for a b::nat by auto show ?thesis proof (cases "ka = kb") case True show ?thesis unfolding inter_scheme_def apply (rule some_equality [symmetric], metis One_nat_def True FB mult_2) subgoal for zs' using assms \length xs < length ys\ by (auto simp: True mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger) done next case False then have eq: "ka = Suc kb" using assms by linarith show ?thesis unfolding inter_scheme_def apply (rule some_equality [symmetric], use assms False mult_2 one_is_add eq in fastforce) subgoal for zs' using assms \length xs < length ys\ by (auto simp: eq mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger) done qed qed subsection \For Lemma 3.8 AND PROBABLY 3.7\ definition grab :: "nat set \ nat \ nat set \ nat set" where "grab N n \ (N \ enumerate N  {.. {enumerate N n..})" lemma grab_0 [simp]: "grab N 0 = ({}, N)" by (fastforce simp: grab_def enumerate_0 Least_le) lemma less_sets_grab: "infinite N \ fst (grab N n) \ snd (grab N n)" by (auto simp: grab_def less_sets_def intro: enumerate_mono less_le_trans) lemma finite_grab [iff]: "finite (fst (grab N n))" by (simp add: grab_def) lemma card_grab [simp]: assumes "infinite N" shows "card (fst (grab N n)) = n" proof - have "N \ enumerate N  {.. N" using grab_def range_enum by fastforce lemma snd_grab_subset: "snd (grab N n) \ N" by (auto simp: grab_def) lemma grab_Un_eq: assumes "infinite N" shows "fst (grab N n) \ snd (grab N n) = N" proof show "N \ fst (grab N n) \ snd (grab N n)" unfolding grab_def using assms enumerate_Ex le_less_linear strict_mono_enum strict_mono_less by fastforce qed (simp add: grab_def) lemma finite_grab_iff [simp]: "finite (snd (grab N n)) \ finite N" by (metis finite_grab grab_Un_eq infinite_Un infinite_super snd_grab_subset) lemma grab_eqD: "\grab N n = (A,M); infinite N\ \ A \ M \ finite A \ card A = n \ infinite M \ A \ N \ M \ N" using card_grab grab_def less_sets_grab finite_grab_iff by auto lemma less_sets_fst_grab: "A \ N \ A \ fst (grab N n)" by (simp add: fst_grab_subset less_sets_weaken2) text\Possibly redundant, given @{term grab}\ definition nxt where "nxt \ \N. \n::nat. N \ {n<..}" lemma infinite_nxtN: "infinite N \ infinite (nxt N n)" by (simp add: infinite_nat_greaterThan nxt_def) lemma nxt_subset: "nxt N n \ N" unfolding nxt_def by blast lemma nxt_subset_greaterThan: "m \ n \ nxt N n \ {m<..}" by (auto simp: nxt_def) lemma nxt_subset_atLeast: "m \ n \ nxt N n \ {m..}" by (auto simp: nxt_def) lemma enum_nxt_ge: "infinite N \ a \ enum (nxt N a) n" by (simp add: atLeast_le_enum infinite_nxtN nxt_subset_atLeast) lemma inj_enum_nxt: "infinite N \ inj_on (enum (nxt N a)) A" by (simp add: infinite_nxtN strict_mono_enum strict_mono_imp_inj_on) subsection \Larson's Lemma 3.11\ text \Again from Jean A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$. \emph{Annals of Mathematical Logic}, 6:129–145, 1973.\ lemma lemma_3_11: assumes "l > 0" shows "thin (inter_scheme l  {U. Form l U})" using form_cases [of l] proof cases case zero then show ?thesis using assms by auto next case (nz ka kb) note acc_lengths.simps [simp del] show ?thesis unfolding thin_def proof clarify fix U U' assume ne: "inter_scheme l U \ inter_scheme l U'" and init: "initial_segment (inter_scheme l U) (inter_scheme l U')" assume "Form l U" then obtain kp kq xs ys where "l = kp+kq - 1" "U = {xs,ys}" and U: "Form_Body kp kq xs ys (inter_scheme l U)" and "0 < kq" "kq \ kp" "kp \ Suc kq" using assms inter_scheme by blast then have "kp = ka \ kq = kb" using nz by linarith then obtain a as b bs c d where len: "length (a#as) = ka" "length (b#bs) = kb" and c: "c = acc_lengths 0 (a#as)" and d: "d = acc_lengths 0 (b#bs)" and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs" using U by (auto simp: Form_Body.simps) assume "Form l U'" then obtain kp' kq' xs' ys' where "l = kp'+kq' - 1" "U' = {xs',ys'}" and U': "Form_Body kp' kq' xs' ys' (inter_scheme l U')" and "0 < kq'" "kq' \ kp'" "kp' \ Suc kq'" using assms inter_scheme by blast then have "kp' = ka \ kq' = kb" using nz by linarith then obtain a' as' b' bs' c' d' where len': "length (a'#as') = ka" "length (b'#bs') = kb" and c': "c' = acc_lengths 0 (a'#as')" and d': "d' = acc_lengths 0 (b'#bs')" and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'" using U' by (auto simp: Form_Body.simps) have [simp]: "length bs' = length bs" "length as' = length as" using len len' by auto have "inter_scheme l U \ []" "inter_scheme l U' \ []" using Form_Body_nonempty U U' by auto define u1 where "u1 \ hd (inter_scheme l U)" have u1_eq': "u1 = hd (inter_scheme l U')" using \inter_scheme l U \ []\ init u1_def initial_segment_ne by fastforce have au1: "u1 = length a" by (simp add: u1_def Ueq c) have au1': "u1 = length a'" by (simp add: u1_eq' Ueq' c') have len_eqk: "length c' = ka" "length d' = kb" "length c' = ka" "length d' = kb" using c d len c' d' len' by auto have take: "take (ka + u1 + kb) (c @ a @ d @ l) = c @ a @ d" "take (ka + u1 + kb) (c' @ a' @ d' @ l) = c' @ a' @ d'" for l using c d c' d' len by (simp_all flip: au1 au1') have leU: "ka + u1 + kb \ length (inter_scheme l U)" using c d len by (simp add: au1 Ueq) then have "take (ka + u1 + kb) (inter_scheme l U) = take (ka + u1 + kb) (inter_scheme l U')" using take_initial_segment init by blast then have \
: "c @ a @ d = c' @ a' @ d'" by (metis Ueq Ueq' append.assoc concat.simps(2) take) have "length (inter_scheme l U) = ka + (c @ a @ d)!(ka-1) + kb + last d" by (simp add: Ueq c d length_interact nth_append flip: len) moreover have "length (inter_scheme l U') = ka + (c' @ a' @ d')!(ka-1) + kb + last d'" by (simp add: Ueq' c' d' length_interact nth_append flip: len') moreover have "last d = last d'" using "\
" c d d' len'(1) len_eqk(1) by auto ultimately have "length (inter_scheme l U) = length (inter_scheme l U')" by (simp add: \
) then show False using init initial_segment_length_eq ne by blast qed qed subsection \Larson's Lemma 3.6\ proposition lemma_3_6: fixes g :: "nat list set \ nat" assumes g: "g \ [WW]\<^bsup>2\<^esup> \ {0,1}" obtains N j where "infinite N" and "\k u. \k > 0; u \ [WW]\<^bsup>2\<^esup>; Form k u; [enum N k] < inter_scheme k u; List.set (inter_scheme k u) \ N\ \ g u = j k" proof - define \ where "\ \ \m::nat. \M. infinite M \ m < Inf M" define \ where "\ \ \l m n::nat. \M N j. n > m \ N \ M \ n \ M \ (\U. Form l U \ U \ WW \ [n] < inter_scheme l U \ list.set (inter_scheme l U) \ N \ g U = j)" have *: "\n N j. \ n N \ \ l m n M N j" if "l > 0" "\ m M" for l m::nat and M :: "nat set" proof - - let ?A = "inter_scheme l  {U \ [WW]\<^bsup>2\<^esup>. Form l U}" - define h where "h \ \zs. g (inv_into {U \ [WW]\<^bsup>2\<^esup>. Form l U} (inter_scheme l) zs)" - have "thin ?A" - using \l > 0\ lemma_3_11 by (simp add: thin_def) - moreover - have "?A \ WW" - using inter_scheme_simple \0 < l\ by blast + define FF where "FF \ {U \ [WW]\<^bsup>2\<^esup>. Form l U}" + define h where "h \ \zs. g (inv_into FF (inter_scheme l) zs)" + have "thin (inter_scheme l  FF)" + using \l > 0\ lemma_3_11 by (simp add: thin_def FF_def) moreover - have "h  {l \ ?A. List.set l \ M} \ {..<2}" - using g inv_into_into[of concl: "{U \ [WW]\<^bsup>2\<^esup>. Form l U}" "inter_scheme l"] - by (force simp: h_def Pi_iff) + have "inter_scheme l  FF \ WW" + using inter_scheme_simple \0 < l\ FF_def by blast + moreover + have "h  {xs \ inter_scheme l  FF. List.set xs \ M} \ {..<2}" + using g inv_into_into[of concl: "FF" "inter_scheme l"] + by (force simp: h_def FF_def Pi_iff) ultimately - obtain j N where "j < 2" "infinite N" "N \ M" and hj: "h  {l \ ?A. List.set l \ N} \ {j}" + obtain j N where "j < 2" "infinite N" "N \ M" and hj: "h  {xs \ inter_scheme l  FF. List.set xs \ N} \ {j}" using \\ m M\ unfolding \_def by (blast intro: Nash_Williams_WW [of M]) - define n where "n \ Inf N" - have "n > m" - using \\ m M\ \infinite N\ unfolding n_def \_def Inf_nat_def infinite_nat_iff_unbounded + let ?n = "Inf N" + have "?n > m" + using \\ m M\ \infinite N\ unfolding \_def Inf_nat_def infinite_nat_iff_unbounded by (metis LeastI_ex \N \ M\ le_less_trans not_less not_less_Least subsetD) - have "g U = j" if "Form l U" "U \ WW" "[n] < inter_scheme l U" "list.set (inter_scheme l U) \ N - {n}" for U + have "g U = j" if "Form l U" "U \ WW" "[?n] < inter_scheme l U" "list.set (inter_scheme l U) \ N - {?n}" for U proof - obtain xs ys where xys: "xs \ ys" "U = {xs,ys}" using Form_elim_upair \Form l U\ by blast - moreover have "inj_on (inter_scheme l) {U \ [WW]\<^bsup>2\<^esup>. Form l U}" - using \0 < l\ inj_on_def inter_scheme_injective by blast + moreover have "inj_on (inter_scheme l) FF" + using \0 < l\ inj_on_def inter_scheme_injective FF_def by blast moreover - have "g (inv_into {U \ [WW]\<^bsup>2\<^esup>. Form l U} (inter_scheme l) (inter_scheme l U)) = j" - using hj that xys subset_Diff_insert by (fastforce simp: h_def image_iff) + have "g (inv_into FF (inter_scheme l) (inter_scheme l U)) = j" + using hj that xys subset_Diff_insert by (fastforce simp: h_def FF_def image_iff) ultimately show ?thesis - using that by auto + using that FF_def by auto qed - moreover have "n < Inf (N - {n})" - unfolding n_def + moreover have "?n < Inf (N - {?n})" by (metis Diff_iff Inf_nat_def Inf_nat_def1 \infinite N\ finite.emptyI infinite_remove linorder_neqE_nat not_less_Least singletonI) - moreover have "n \ M" - by (metis Inf_nat_def1 \N \ M\ \infinite N\ finite.emptyI n_def subsetD) - ultimately have "\ n (N - {n}) \ \ l m n M (N - {n}) j" - using \\ m M\ \infinite N\ \N \ M\ \n > m\ by (auto simp: \_def \_def) + moreover have "?n \ M" + by (metis Inf_nat_def1 \N \ M\ \infinite N\ finite.emptyI subsetD) + ultimately have "\ ?n (N - {?n}) \ \ l m ?n M (N - {?n}) j" + using \\ m M\ \infinite N\ \N \ M\ \?n > m\ by (auto simp: \_def \_def) then show ?thesis by blast qed have base: "\ 0 {0<..}" unfolding \_def by (metis infinite_Ioi Inf_nat_def1 greaterThan_iff greaterThan_non_empty) have step: "Ex ($$n,N,j). \ n N \ \ l m n M N j)" if "\ m M" "l > 0" for m M l using * [of l m M] that by (auto simp: \_def) define G where "G \ \l m M. @(n,N,j). \ n N \ \ (Suc l) m n M N j" have G\: "(\(n,N,j). \ n N) (G l m M)" and G\: "(\(n,N,j). \ (Suc l) m n M N j) (G l m M)" if "\ m M" for l m M using step [OF that, of "Suc l"] by (force simp: G_def dest: some_eq_imp)+ have G_increasing: "(\(n,N,j). n > m \ N \ M \ n \ M) (G l m M)" if "\ m M" for l m M using G\ [OF that, of l] that by (simp add: \_def split: prod.split_asm) define H where "H \ rec_nat (0,{0<..},0) (\l (m,M,j). G l m M)" have H_simps: "H 0 = (0,{0<..},0)" "\l. H (Suc l) = (case H l of (m,M,j) \ G l m M)" by (simp_all add: H_def) have H\: "(\(n,N,j). \ n N) (H l)" for l by (induction l) (use base G\ in \auto simp: H_simps split: prod.split_asm$$ define \ where "\ \ (\l. case H l of (n,M,j) \ n)" have H_inc: "\ l \ l" for l proof (induction l) case (Suc l) then show ?case using H\ [of l] G_increasing [of "\ l"] apply (clarsimp simp: H_simps \_def split: prod.split) by (metis (no_types, lifting) case_prodD leD le_less_trans not_less_eq_eq) qed auto let ?N = "range \" define j where "j \ \l. case H l of (n,M,j) \ j" have H_increasing_Suc: "(case H k of (n, N, j') \ N) \ (case H (Suc k) of (n, N, j') \ insert n N)" for k using H\ [of k] by (force simp: H_simps split: prod.split dest: G_increasing [where l=k]) have H_increasing_superset: "(case H k of (n, N, j') \ N) \ (case H (n+k) of (n, N, j') \ N)" for k n proof (induction n) case (Suc n) then show ?case using H_increasing_Suc [of "n+k"] by (auto split: prod.split_asm) qed auto then have H_increasing_less: "(case H k of (n, N, j') \ N) \ (case H l of (n, N, j') \ insert n N)" if "k k < \ (Suc k)" for k using H\ [of k] unfolding \_def by (auto simp: H_simps split: prod.split dest: G_increasing [where l=k]) then have strict_mono_\: "strict_mono \" by (simp add: strict_mono_Suc_iff) then have enum_N: "enum ?N = \" by (metis enum_works nat_infinite_iff range_strict_mono_ext) have **: "?N \ {n<..} \ N'" if H: "H k = (n, N', j)" for n N' k j proof clarify fix l assume "n < \ l" then have False if "l \ k" using that strict_monoD [OF strict_mono_\, of l k ] H by (force simp: \_def) then have "k < l" using not_less by blast then obtain M j where Mj: "H l = (\ l,M,j)" unfolding \_def by (metis (mono_tags, lifting) case_prod_conv old.prod.exhaust) then show "\ l \ N'" using that H_increasing_less [OF \k] Mj by auto qed show thesis proof show "infinite (?N::nat set)" using H_inc infinite_nat_iff_unbounded_le by auto next fix l U assume "0 < l" and U: "U \ [WW]\<^bsup>2\<^esup>" and interU: "[enum ?N l] < inter_scheme l U" "Form l U" and sub: "list.set (inter_scheme l U) \ ?N" obtain k where k: "l = Suc k" using \0 < l\ gr0_conv_Suc by blast - have "U \ WW" - using U by (auto simp: nsets_def) - moreover have "g U = v" if "H k = (m, M, j0)" and "G k m M = (n, N', v)" for m M j0 n N' v proof - have n: "\ (Suc k) = n" using that by (simp add: \_def H_simps) have "{..enum (range \) l} \ list.set (inter_scheme l U) = {}" using inter_scheme_strict_sorted \0 < l\ interU singleton_less_list_iff strict_sorted_iff by blast then have "list.set (inter_scheme (Suc k) U) \ N'" using that sub ** [of "Suc k" n N' v] Suc_le_eq not_less_eq_eq by (fastforce simp: k n enum_N H_simps) then show ?thesis - using that interU \U \ WW\ G\ [of m M k] H\ [of k] - by (auto simp: \_def k enum_N H_simps n) + using that interU U G\ [of m M k] H\ [of k] + by (auto simp: \_def k enum_N H_simps n nsets_def) qed - ultimately show "g U = j l" + with U show "g U = j l" by (auto simp: k j_def H_simps split: prod.split) qed qed subsection \Larson's Lemma 3.7\ subsubsection \Preliminaries\ text \Analogous to @{thm [source] ordered_nsets_2_eq}, but without type classes\ lemma total_order_nsets_2_eq: assumes tot: "total_on A r" and irr: "irrefl r" shows "nsets A 2 = {{x,y} | x y. x \ A \ y \ A \ (x,y) \ r}" (is "_ = ?rhs") proof show "nsets A 2 \ ?rhs" using tot unfolding numeral_nat total_on_def nsets_def by (fastforce simp: card_Suc_eq Set.doubleton_eq_iff not_less) show "?rhs \ nsets A 2" using irr unfolding numeral_nat by (force simp: nsets_def card_Suc_eq irrefl_def) qed lemma lenlex_nsets_2_eq: "nsets A 2 = {{x,y} | x y. x \ A \ y \ A \ (x,y) \ lenlex less_than}" using total_order_nsets_2_eq by (simp add: total_order_nsets_2_eq irrefl_def) lemma sum_sorted_list_of_set_map: "finite I \ sum_list (map f (list_of I)) = sum f I" proof (induction "card I" arbitrary: I) case (Suc n I) then have [simp]: "I \ {}" by auto have "sum_list (map f (list_of (I - {Min I}))) = sum f (I - {Min I})" using Suc by auto then show ?case using Suc.prems sum.remove [of I "Min I" f] by (simp add: sorted_list_of_set_nonempty Suc) qed auto lemma sorted_list_of_set_UN_eq_concat: assumes I: "strict_mono_sets I f" "finite I" and fin: "\i. finite (f i)" shows "list_of (\i \ I. f i) = concat (map (list_of \ f) (list_of I))" using I proof (induction "card I" arbitrary: I) case (Suc n I) then have "I \ {}" and Iexp: "I = insert (Min I) (I - {Min I})" using Min_in Suc.hyps(2) Suc.prems(2) by fastforce+ have IH: "list_of (\ (f  (I - {Min I}))) = concat (map (list_of \ f) (list_of (I - {Min I})))" using Suc unfolding strict_mono_sets_def by (metis DiffE Iexp card_Diff_singleton diff_Suc_1 finite_Diff insertI1) have "list_of (\ (f  I)) = list_of (\ (f  (insert (Min I) (I - {Min I}))))" using Iexp by auto also have "\ = list_of (f (Min I) \ \ (f  (I - {Min I})))" by (metis Union_image_insert) also have "\ = list_of (f (Min I)) @ list_of (\ (f  (I - {Min I})))" proof (rule sorted_list_of_set_Un) show "f (Min I) \ \ (f  (I - {Min I}))" using Suc.prems \I \ {}\ strict_mono_less_sets_Min by blast show "finite (\ (f  (I - {Min I})))" by (simp add: \finite I\ fin) qed (use fin in auto) also have "\ = list_of (f (Min I)) @ concat (map (list_of \ f) (list_of (I - {Min I})))" using IH by metis also have "\ = concat (map (list_of \ f) (list_of I))" by (simp add: Suc.prems(2) \I \ {}\ sorted_list_of_set_nonempty) finally show ?case . qed auto subsubsection \Lemma 3.7 of Jean A. Larson, ibid.\ proposition lemma_3_7: assumes "infinite N" "l > 0" obtains M where "M \ [WW]\<^bsup>m\<^esup>" "\U. U \ [M]\<^bsup>2\<^esup> \ Form l U \ List.set (inter_scheme l U) \ N" proof (cases "m < 2") case True obtain w where w: "w \ WW" using WW_def strict_sorted_into_WW by auto define M where "M \ if m=0 then {} else {w}" have M: "M \ [WW]\<^bsup>m\<^esup>" using True by (auto simp: M_def nsets_def w) have [simp]: "[M]\<^bsup>2\<^esup> = {}" using True by (auto simp: M_def nsets_def w dest: subset_singletonD) show ?thesis using M that by fastforce next case False then have "m \ 2" by auto have nonz: "(enum N \ Suc) i > 0" for i using assms(1) le_enumerate less_le_trans by fastforce note infinite_nxt_N = infinite_nxtN [OF \infinite N\, iff] note \infinite N\ [ iff] have [simp]: "{n<.. \k D. enum (nxt N (enum (nxt N (Max D)) (Inf D - 1)))  {.. \k. rec_nat ((enum N \ Suc)  {..r. DF_Suc k)" have DF_simps: "DF k 0 = (enum N \ Suc)  {.. Suc) {..infinite N\ DF_simps DF_Suc_def card_image infinite_nxtN strict_mono_enum strict_mono_imp_inj_on) qed have DF_ne: "DF k i \ {}" for i k by (metis card_DF card_lessThan lessThan_empty_iff nat.simps(3)) have finite_DF: "finite (DF k i)" for i k by (induction i) (auto simp: DF_simps DF_Suc_def) have DF_Suc: "DF k i \ DF k (Suc i)" for i k unfolding less_sets_def by (force simp: finite_DF DF_simps DF_Suc_def intro!: greaterThan_less_enum nxt_subset_greaterThan atLeast_le_enum nxt_subset_atLeast infinite_nxtN [OF \infinite N\]) have DF_DF: "DF k i \ DF k j" if "i N" for i k proof (induction i) case 0 then show ?case using \infinite N\ range_enum by (auto simp: DF_simps) next case (Suc i) then show ?case unfolding DF_simps DF_Suc_def image_subset_iff by (metis IntE \infinite N\ enumerate_in_set infinite_nxtN nxt_def) qed have sm_enum_DF: "strict_mono_on (enum (DF k i)) {..k}" for k i by (metis card_DF enum_works_finite finite_DF lessThan_Suc_atMost) define AF where "AF \ \k i. enum (nxt N (Max (DF k i)))  {.. {}" for i k by (auto simp: AF_def lessThan_empty_iff DF_gt0) have finite_AF [simp]: "finite (AF k i)" for i k by (simp add: AF_def) have card_AF: "card (AF k i) = \ (DF k i)" for k i by (simp add: AF_def card_image inj_enum_nxt) have DF_AF: "DF k i \ AF k i" for i k unfolding less_sets_def AF_def by (simp add: finite_DF greaterThan_less_enum nxt_subset_greaterThan) have E: "\x \ y; infinite M\ \ enum M x < enum (nxt N (enum M y)) z" for x y z M by (metis infinite_nxt_N dual_order.eq_iff enumerate_mono greaterThan_less_enum nat_less_le nxt_subset_greaterThan) have AF_DF_Suc: "AF k i \ DF k (Suc i)" for i k by (auto simp: DF_simps DF_Suc_def less_sets_def AF_def E) have AF_DF: "AF k p \ DF k q" if "p AF k (Suc i)" for i k using AF_DF_Suc DF_AF DF_ne less_sets_trans by blast then have sm_AF: "strict_mono_sets UNIV (AF k)" for k by (simp add: AF_ne less_sets_imp_strict_mono_sets) define del where "del \ \k i j. enum (DF k i) j - enum (DF k i) (j - 1)" define QF where "QF k \ wfrec pair_less (\f (j,i). if j=0 then AF k i else let r = (if i=0 then f (j-1,m-1) else f (j,i-1)) in enum (nxt N (Suc (Max r)))  {..< del k (if j=k then m - Suc i else i) j})" for k note cut_apply [simp] have finite_QF [simp]: "finite (QF k p)" for p k using wf_pair_less proof (induction p rule: wf_induct_rule) case (less p) then show ?case by (simp add: def_wfrec [OF QF_def, of k p] split: prod.split) qed have del_gt_0: "\j < Suc k; 0 < j\ \ 0 < del k i j" for i j k by (simp add: card_DF del_def finite_DF) have QF_ne [simp]: "QF k (j,i) \ {}" if j: "j < Suc k" for j i k using wf_pair_less j proof (induction "(j,i)" rule: wf_induct_rule) case less then show ?case by (auto simp: def_wfrec [OF QF_def, of k "(j,i)"] AF_ne lessThan_empty_iff del_gt_0) qed have QF_0 [simp]: "QF k (0,i) = AF k i" for i k by (simp add: def_wfrec [OF QF_def]) have QF_Suc: "QF k (Suc j,0) = enum (nxt N (Suc (Max (QF k (j, m - 1)))))  {..< del k (if Suc j = k then m - 1 else 0) (Suc j)}" for j k apply (simp add: def_wfrec [OF QF_def, of k "(Suc j,0)"] One_nat_def) apply (simp add: pair_less_def cut_def) done have QF_Suc_Suc: "QF k (Suc j, Suc i) = enum (nxt N (Suc (Max (QF k (Suc j, i)))))  {..< del k (if Suc j = k then m - Suc(Suc i) else Suc i) (Suc j)}" for i j k by (simp add: def_wfrec [OF QF_def, of k "(Suc j,Suc i)"]) have less_QF1: "QF k (j, m - 1) \ QF k (Suc j,0)" for j k by (auto simp: def_wfrec [OF QF_def, of k "(Suc j,0)"] pair_lessI1 enum_nxt_ge intro!: less_sets_weaken2 [OF less_sets_Suc_Max]) have less_QF2: "QF k (j,i) \ QF k (j, Suc i)" for j i k by (auto simp: def_wfrec [OF QF_def, of k "(j, Suc i)"] pair_lessI2 enum_nxt_ge intro: less_sets_weaken2 [OF less_sets_Suc_Max] strict_mono_setsD [OF sm_AF]) have less_QF_same: "QF k (j,i') \ QF k (j,i)" if "i' < i" "j \ k" for i' i j k proof (rule strict_mono_setsD [OF less_sets_imp_strict_mono_sets]) show "QF k (j, i) \ QF k (j, Suc i)" for i by (simp add: less_QF2) show "QF k (j, i) \ {}" if "0 < i" for i using that by (simp add: \j \ k\ le_imp_less_Suc) qed (use that in auto) have less_QF_step: "QF k (j-1, i') \ QF k (j,i)" if "0 < j" "j \ k" "i' < m" for j i' i k proof - have less_QF1': "QF k (j - 1, m-1) \ QF k (j,0)" if "j > 0" for j by (metis less_QF1 that Suc_pred One_nat_def) have "QF k (j-1, i') \ QF k (j,0)" proof (cases "i' = m - 1") case True then show ?thesis using less_QF1' \0 < j\ by blast next case False show ?thesis using False that less_sets_trans [OF less_QF_same less_QF1' QF_ne] by auto qed then show ?thesis by (metis QF_ne less_QF_same less_Suc_eq_le less_sets_trans \j \ k\ zero_less_iff_neq_zero) qed have less_QF: "QF k (j',i') \ QF k (j,i)" if j: "j' < j" "j \ k" and i: "i' < m" "i < m" for j' j i' i k using j proof (induction "j-j'" arbitrary: j) case (Suc d) show ?case proof (cases "j' < j - 1") case True then have "QF k (j', i') \ QF k (j - 1, i)" using Suc.hyps Suc.prems(2) by force then show ?thesis by (rule less_sets_trans [OF _ less_QF_step QF_ne]) (use Suc i in auto) next case False then have "j' = j - 1" using \j' < j\ by linarith then show ?thesis using Suc.hyps \j \ k\ less_QF_step i by auto qed qed auto have sm_QF: "strict_mono_sets ({..k} \ {.. {..k} \ {.. {..k} \ {..: "p = (j',i')" "q = (j,i)" "i' < m" "i < m" "j' \ k" "j \ k" using surj_pair [of p] surj_pair [of q] by blast with \p < q\ have "j' < j \ j' = j \ i' < i" by auto then show "QF k p \ QF k q" using \
less_QF less_QF_same by presburger qed then have sm_QF1: "strict_mono_sets {..j. QF k (j,i))" if "i ka" "ka \ k" for ka k i proof - have "{.. {..k}" by (metis lessThan_Suc_atMost lessThan_subset_iff \Suc k \ ka\) then show ?thesis by (simp add: less_QF strict_mono_sets_def subset_iff that) qed have disjoint_QF: "i'=i \ j'=j" if "\ disjnt (QF k (j', i')) (QF k (j,i))" "j' \ k" "j \ k" "i' < m" "i < m" for i' i j' j k using that strict_mono_sets_imp_disjoint [OF sm_QF] by (force simp: pairwise_def) have card_QF: "card (QF k (j,i)) = (if j=0 then \ (DF k i) else del k (if j = k then m - Suc i else i) j)" for i k j proof (cases j) case 0 then show ?thesis by (simp add: AF_def card_image inj_enum_nxt) next case (Suc j') show ?thesis by (cases i; simp add: Suc One_nat_def QF_Suc QF_Suc_Suc card_image inj_enum_nxt) qed have AF_non_Nil: "list_of (AF k i) \ []" for k i by (simp add: AF_ne) have QF_non_Nil: "list_of (QF k (j,i)) \ []" if "j < Suc k" for i j k by (simp add: that) have AF_subset_N: "AF k i \ N" for i k unfolding AF_def image_subset_iff using nxt_subset enumerate_in_set infinite_nxtN \infinite N\ by blast have QF_subset_N: "QF k (j,i) \ N" for i j k proof (induction j) case (Suc j) show ?case by (cases i) (use nxt_subset enumerate_in_set in $$force simp: QF_Suc QF_Suc_Suc)+$$ qed (use AF_subset_N in auto) obtain ka k where "k>0" and kka: "k \ ka" "ka \ Suc k" "l = ((ka+k) - 1)" by (metis One_nat_def assms(2) diff_add_inverse form_cases le0 le_refl) then have "ka > 0" using dual_order.strict_trans1 by blast have ka_k_or_Suc: "ka = k \ ka = Suc k" using kka by linarith have lessThan_k: "{..0" for k::nat using that by auto then have sorted_list_of_set_k: "list_of {..0" for k::nat using sorted_list_of_set_insert_cons [of concl: 0 "{0<.. \j i. if j = k then QF k (j, m - Suc i) else QF k (j,i)" have RF_subset_N: "RF j i \ N" if "i0 < k\ by auto have disjoint_RF: "i'=i \ j'=j" if "\ disjnt (RF j' i') (RF j i)" "j' \ k" "j \ k" "i' < m" "i < m" for i' i j' j using disjoint_QF that by (auto simp: RF_def split: if_split_asm dest: disjoint_QF) have sum_card_RF [simp]: "(\j\n. card (RF j i)) = enum (DF k i) n" if "n \ k" "i < m" for i n using that proof (induction n) case 0 then show ?case using DF_ne [of k i] finite_DF [of k i] \k>0\ by (simp add: RF_def AF_def card_image inj_enum_nxt enum_0_eq_Inf_finite) next case (Suc n) then have "enum (DF k i) 0 \ enum (DF k i) n \ enum (DF k i) n \ enum (DF k i) (Suc n)" using sm_enum_DF [of k i] by (metis Suc_leD card_DF dual_order.eq_iff finite_DF finite_enumerate_mono le_imp_less_Suc less_imp_le_nat not_gr_zero) with Suc show ?case by (auto simp: RF_def card_QF del_def) qed have DF_in_N: "enum (DF k i) j \ N" if "j \ k" for i j by (metis DF_N card_DF finite_DF finite_enumerate_in_set le_imp_less_Suc subsetD that) have Inf_DF_N: "$$DF k p) \ N" for k p using DF_N DF_ne Inf_nat_def1 by blast have RF_in_N: "(\j\n. card (RF j i)) \ N" if "n \ k" "i < m" for i n by (auto simp: DF_in_N that) have "ka - 1 \ k" using kka(2) by linarith then have sum_card_RF' [simp]: "(\j0 < ka\ lessThan_Suc_atMost that) have enum_DF_le_iff [simp]: "enum (DF k i) j \ enum (DF k i') j \ i \ i'" (is "?lhs = _") if "j \ k" for i' i j k proof show "i \ i'" if ?lhs proof - have "enum (DF k i) j \ DF k i" by (simp add: card_DF finite_enumerate_in_set finite_DF le_imp_less_Suc \j \ k$$ moreover have "enum (DF k i') j \ DF k i'" by (simp add: \j \ k\ card_DF finite_enumerate_in_set finite_DF le_imp_less_Suc that) ultimately have "enum (DF k i') j < enum (DF k i) j" if "i' < i" using sm_DF [of k] by (meson UNIV_I less_sets_def strict_mono_setsD that) then show ?thesis using not_less that by blast qed show ?lhs if "i \ i'" using sm_DF [of k] that \j \ k\ card_DF finite_enumerate_in_set finite_DF le_eq_less_or_eq by (force simp: strict_mono_sets_def less_sets_def finite_enumerate_in_set) qed then have enum_DF_eq_iff[simp]: "enum (DF k i) j = enum (DF k i') j \ i = i'" if "j \ k" for i' i j k by (metis le_antisym order_refl that) have enum_DF_less_iff [simp]: "enum (DF k i) j < enum (DF k i') j \ i < i'" if "j \ k" for i' i j k by (meson enum_DF_le_iff not_less that) have card_AF_sum: "card (AF k i) + (\j\{0<..k > 0\ \k \ ka\ \ka \ Suc k\ by (simp add: lessThan_k RF_0 flip: sum_card_RF') have sorted_list_of_set_iff [simp]: "list_of {0<.. k = 1" if "k>0" for k::nat proof - have "list_of {0<.. {0<.. \ k = 1" using \k > 0\ atLeastSucLessThan_greaterThanLessThan by fastforce finally show ?thesis . qed show thesis \\proof of main result\ proof have inj: "inj_on (\i. list_of (\jjjjj RF 0 x" using AF_ne QF_0 \0 < k\ Inf_nat_def1 \k \ ka\ by (force simp: RF_def) with eq \ka > 0\ obtain j' where "j' < ka" "n \ RF j' y" by blast then show ?thesis using disjoint_QF [of k 0 x j'] n \x < m\ \y < m\ \ka \ Suc k\ \0 < k\ by (force simp: RF_def disjnt_iff simp del: QF_0 split: if_split_asm) qed qed define M where "M \ (\i. list_of (\jk \ ka\ card_image inj) moreover have "M \ WW" by (force simp: M_def WW_def) ultimately show "M \ [WW]\<^bsup>m\<^esup>" by (simp add: nsets_def) have sm_RF: "strict_mono_sets {..j. RF j i)" if "i []" if "j < Suc k" for i j using that by (simp add: RF_def) have less_RF_same: "RF j i' \ RF j i" if "i' < i" "j < k" for i' i j using that by (simp add: less_QF_same RF_def) have less_RF_same_k: "RF k i' \ RF k i" \\reversed version for @{term k}\ if "i < i'" "i' < m" for i' i using that by (simp add: less_QF_same RF_def) show "Form l U \ list.set (inter_scheme l U) \ N" if "U \ [M]\<^bsup>2\<^esup>" for U proof - from that obtain x y where "U = {x,y}" "x \ M" "y \ M" and xy: "(x,y) \ lenlex less_than" by (auto simp: lenlex_nsets_2_eq) let ?R = "\p. list_of \ (\j. RF j p)" obtain p q where x: "x = list_of (\jjx \ M\ \y \ M\ by (auto simp: M_def) then have pq: "pk \ ka\ \ka \ Suc k\ lexl_not_refl [OF irrefl_less_than] by (auto simp: lenlex_def sm_RF sorted_list_of_set_UN_lessThan length_concat sum_sorted_list_of_set_map) moreover have xc: "x = concat (map (?R p) (list_of {..k \ ka\ \ka \ Suc k\ \p < m\ sm_RF) have yc: "y = concat (map (?R q) (list_of {..k \ ka\ \ka \ Suc k\ \q < m\ sm_RF) have enum_DF_AF: "enum (DF k p) (ka - 1) < hd (list_of (AF k p))" for p proof (rule less_setsD [OF DF_AF]) show "enum (DF k p) (ka - 1) \ DF k p" using \ka \ Suc k\ card_DF finite_DF by (auto simp: finite_enumerate_in_set) show "hd (list_of (AF k p)) \ AF k p" using AF_non_Nil finite_AF hd_in_set set_sorted_list_of_set by blast qed have less_RF_RF: "RF n p \ RF n q" if "n < k" for n using that \p by (simp add: less_RF_same) have less_RF_Suc: "RF n q \ RF (Suc n) q" if "n < k" for n using \q < m\ that by (auto simp: RF_def less_QF) have less_RF_k: "RF k q \ RF k p" using \q < m\ less_RF_same_k \p by blast have less_RF_k_ka: "RF (k-1) p \ RF (ka - 1) q" using ka_k_or_Suc less_RF_RF by (metis One_nat_def RF_def \0 < k\ \ka - 1 \ k\ \p < m\ diff_Suc_1 diff_Suc_less less_QF_step) have Inf_DF_eq_enum: "\ (DF k i) = enum (DF k i) 0" for k i by (simp add: Inf_nat_def enumerate_0) have Inf_DF_less: "\ (DF k i') < \ (DF k i)" if "i'x. x \ AF k i \ \ (DF k i') < x" if "i'\i" for i' i k using less_setsD [OF DF_AF] DF_ne that by (metis Inf_DF_less Inf_nat_def1 dual_order.order_iff_strict dual_order.strict_trans) show ?thesis \\The general case requires @{term\k>1\}, necessitating a painful special case\ proof (cases "k=1") case True with kka consider "ka=1" | "ka=2" by linarith then show ?thesis proof cases case 1 define zs where "zs = card (AF 1 p) # list_of (AF 1 p) @ card (AF 1 q) # list_of (AF 1 q)" have zs: "Form_Body ka k x y zs" proof (intro that exI conjI Form_Body.intros) show "x = concat ([list_of (AF k p)])" "y = concat ([list_of (AF k q)])" by (simp_all add: x y 1 lessThan_Suc RF_0) have "AF k p \ insert (\ (DF k q)) (AF k q)" by (metis AF_DF DF_ne Inf_nat_def1 RF_0 \0 < k\ insert_iff less_RF_RF less_sets_def pq(1)) then have "strict_sorted (list_of (AF k p) @ \ (DF k q) # list_of (AF k q))" by (auto simp: strict_sorted_append_iff intro: less_sets_imp_list_less AF_Inf_DF_less) moreover have "\x. x \ AF k q \ \ (DF k p) < x" by (meson AF_Inf_DF_less less_imp_le_nat \p < q\) moreover have "\x. x \ AF 1 p \ \ (DF 1 p) < x" by (meson DF_AF DF_ne Inf_nat_def1 less_setsD) ultimately show "strict_sorted zs" using \p < q\ True Inf_DF_less DF_AF DF_ne by (auto simp: zs_def less_sets_def card_AF AF_Inf_DF_less) qed (auto simp: \k=1\ \ka=1\ zs_def AF_ne \length x < length y\) have zs_N: "list.set zs \ N" using AF_subset_N by (auto simp: zs_def card_AF Inf_DF_N \k=1\) show ?thesis proof have "l = 1" using kka \k=1\ \ka=1\ by auto have "Form (2*1-1) {x,y}" using "1" Form.intros(2) True zs by fastforce then show "Form l U" by (simp add: \U = {x,y}\ \l = 1\ One_nat_def) show "list.set (inter_scheme l U) \ N" using kka zs zs_N \k=1\ Form_Body_imp_inter_scheme by (fastforce simp: \U = {x,y}\) qed next case 2 note True [simp] note 2 [simp] have [simp]: "{0<..<2} = {1::nat}" by auto have enum_DF1_eq: "enum (DF 1 i) 1 = card (AF 1 i) + card (RF 1 i)" if "i < m" for i using card_AF_sum that by (simp add: One_nat_def) have card_RF: "card (RF 1 i) = enum (DF 1 i) 1 - enum (DF 1 i) 0" if "i < m" for i using that by (auto simp: RF_def card_QF del_def) have list_of_AF_RF: "list_of (AF 1 q \ RF 1 q) = list_of (AF 1 q) @ list_of (RF 1 q)" by (metis One_nat_def RF_0 True \0 < k\ finite_RF less_RF_Suc sorted_list_of_set_Un) define zs where "zs = card (AF 1 p) # (card (AF 1 p) + card (RF 1 p)) # list_of (AF 1 p) @ (card (AF 1 q) + card (RF 1 q)) # list_of (AF 1 q) @ list_of (RF 1 q) @ list_of (RF 1 p)" have zs: "Form_Body ka k x y zs" proof (intro that exI conjI Form_Body.intros) have "x = list_of (RF 0 p \ RF 1 p)" by (simp add: x eval_nat_numeral lessThan_Suc RF_0 Un_commute One_nat_def) also have "\ = list_of (RF 0 p) @ list_of (RF 1 p)" using RF_def True \p < m\ less_QF_step by (metis QF_0 RF_0 diff_self_eq_0 finite_RF le_refl sorted_list_of_set_Un zero_less_one) finally show "x = concat ([list_of (AF 1 p),list_of (RF 1 p)])" by (simp add: RF_0) show "y = concat [list_of (RF 1 q \ AF 1 q)]" by (simp add: y eval_nat_numeral lessThan_Suc RF_0 One_nat_def) show zs: "zs = concat [[card (AF 1 p), card (AF 1 p) + card (RF 1 p)], list_of (AF 1 p), [card (AF 1 q) + card (RF 1 q)], list_of (RF 1 q \ AF 1 q)] @ interact [list_of (RF 1 p)] []" using list_of_AF_RF by (simp add: zs_def Un_commute) show "strict_sorted zs" proof (simp add: \p \q \p zs_def strict_sorted_append_iff, intro conjI strip) show "0 < card (RF 1 p)" using \p by (simp add: card_RF card_DF finite_DF) show "card (AF 1 p) < card (AF 1 q) + card (RF 1 q)" using \p \q by (simp add: Inf_DF_less card_AF trans_less_add1) show "card (AF 1 p) < x" if "x \ AF 1 p \ (AF 1 q \ (RF 1 q \ RF 1 p))" for x using that apply (simp add: card_AF) by (metis AF_ne DF_AF DF_ne less_RF_RF less_RF_Suc less_RF_k Inf_nat_def1 One_nat_def RF_0 RF_non_Nil True finite_RF lessI less_setsD less_sets_trans sorted_list_of_set_eq_Nil_iff) show "card (AF 1 p) + card (RF 1 p) < card (AF 1 q) + card (RF 1 q)" using \p < q\ \p < m\ \q < m\ by (metis enum_DF1_eq enum_DF_less_iff le_refl) show "card (AF 1 p) + card (RF 1 p) < x" if "x \ AF 1 p \ (AF 1 q \ (RF 1 q \ RF 1 p))" for x using that \p < m\ apply (simp flip: enum_DF1_eq) by (metis AF_ne DF_AF less_RF_RF less_RF_Suc less_RF_k One_nat_def RF_0 RF_non_Nil Suc_mono True \0 < k\ card_DF finite_enumerate_in_set finite_DF less_setsD less_sets_trans sorted_list_of_set_empty) have "list_of (AF 1 p) < list_of {enum (DF 1 q) 1}" proof (rule less_sets_imp_sorted_list_of_set) show "AF 1 p \ {enum (DF 1 q) 1}" by (metis AF_DF card_DF empty_subsetI finite_DF finite_enumerate_in_set insert_subset less_Suc_eq less_sets_weaken2 pq(1)) qed auto then show "list_of (AF 1 p) < (card (AF 1 q) + card (RF 1 q)) # list_of (AF 1 q) @ list_of (RF 1 q) @ list_of (RF 1 p)" using \q < m\ by (simp add: less_list_def enum_DF1_eq) show "card (AF 1 q) + card (RF 1 q) < x" if "x \ AF 1 q \ (RF 1 q \ RF 1 p)" for x using that \q < m\ apply (simp flip: enum_DF1_eq) by (metis AF_ne DF_AF less_RF_Suc less_RF_k One_nat_def RF_0 RF_non_Nil True card_DF finite_enumerate_in_set finite_DF finite_RF lessI less_setsD less_sets_trans sorted_list_of_set_eq_Nil_iff) have "list_of (AF 1 q) < list_of (RF 1 q)" proof (rule less_sets_imp_sorted_list_of_set) show "AF 1 q \ RF 1 q" by (metis less_RF_Suc One_nat_def RF_0 True \0 < k\) qed auto then show "list_of (AF 1 q) < list_of (RF 1 q) @ list_of (RF 1 p)" using RF_non_Nil by (auto simp: less_list_def) show "list_of (RF 1 q) < list_of (RF 1 p)" proof (rule less_sets_imp_sorted_list_of_set) show "RF 1 q \ RF 1 p" by (metis less_RF_k True) qed auto qed show "[list_of (AF 1 p), list_of (RF 1 p)] \ lists (- {[]})" using RF_non_Nil \0 < k\ by (auto simp: zs_def AF_ne) show "[card (AF 1 q) + card (RF 1 q)] = acc_lengths 0 [list_of (RF 1 q \ AF 1 q)]" using list_of_AF_RF by (auto simp: zs_def AF_ne sup_commute) qed (auto simp: zs_def AF_ne \length x < length y\) have zs_N: "list.set zs \ N" using \p < m\ \q < m\ DF_in_N enum_DF1_eq [symmetric] by (auto simp: zs_def card_AF AF_subset_N RF_subset_N Inf_DF_N) show ?thesis proof have "Form (2*1) {x,y}" by (metis "2" Form.simps Suc_1 True zero_less_one zs) with kka show "Form l U" by (simp add: \U = {x,y}\) show "list.set (inter_scheme l U) \ N" using kka zs zs_N \k=1\ Form_Body_imp_inter_scheme by (fastforce simp: \U = {x, y}\) qed qed next case False then have "k \ 2" "ka \ 2" using kka \k>0\ by auto then have k_minus_1 [simp]: "Suc (k - Suc (Suc 0)) = k - Suc 0" by auto have [simp]: "Suc (k - 2) = k-1" using \k \ 2\ by linarith define PP where "PP \ map (?R p) (list_of {0<.. map (?R q) (list_of {0<.. RF (ka-1) q)])" let ?INT = "interact PP QQ" \\No separate sets A and B as in the text, but instead we treat both cases as once\ have [simp]: "length PP = ka - 1" by (simp add: PP_def) have [simp]: "length QQ = k-1" using \k \ 2\ by (simp add: QQ_def) have PP_n: "PP ! n = list_of (RF (Suc n) p)" if "n < ka-1" for n using that kka by (auto simp: PP_def nth_sorted_list_of_set_greaterThanLessThan) have QQ_n: "QQ ! n = (if n < k-2 then list_of (RF (Suc n) q) else list_of (RF (k-1) q \ RF (ka - 1) q))" if "n < k-1" for n using that kka by (auto simp: QQ_def nth_append nth_sorted_list_of_set_greaterThanLessThan) have QQ_n_same: "QQ ! n = list_of (RF (Suc n) q)" if "n < k-1" "k=ka" for n using that kka Suc_diff_Suc by (fastforce simp: One_nat_def QQ_def nth_append nth_sorted_list_of_set_greaterThanLessThan) have split_nat_interval: "{0<.. 2" for n::nat using that by auto have split_list_interval: "list_of{0<.. 2" for n::nat proof (intro sorted_list_of_set_unique [THEN iffD1] conjI) have "list_of {0<..n \ 2\ in auto) have list_of_RF_Un: "list_of (RF (k-1) q \ RF k q) = list_of (RF (k-1) q) @ list_of (RF k q)" by (metis Suc_diff_1 \0 < k\ finite_RF lessI less_RF_Suc sorted_list_of_set_Un) have card_AF_sum_QQ: "card (AF k q) + sum_list (map length QQ) = (\j RF k q = {}" using less_RF_Suc [of "k-1"] \k > 0\ by (auto simp: less_sets_def) then have "card (RF (k-1) q \ RF k q) = card (RF (k-1) q) + card (RF k q)" by (simp add: card_Un_disjoint) then show ?thesis using \k\2\ \q < m\ apply (simp add: QQ_def True flip: RF_0) apply (simp add: lessThan_k split_nat_interval sum_sorted_list_of_set_map) done next case False with kka have "ka=k" by linarith with \k\2\ show ?thesis by (simp add: QQ_def lessThan_k split_nat_interval sum_sorted_list_of_set_map flip: RF_0) qed define LENS where "LENS \ \i. acc_lengths 0 (list_of (AF k i) # map (?R i) (list_of {0<.. N" if "i < m" for i proof - have eq: "(list_of (AF k i) # map (?R i) (list_of {0<..0 < ka\ sorted_list_of_set_k by auto let ?f = "rec_nat [card (AF k i)] (\n r. r @ [(\j\Suc n. card (RF j i))])" have f: "acc_lengths 0 (map (?R i) (list_of {..v})) = ?f v" for v by (induction v) (auto simp: RF_0 acc_lengths_append sum_sorted_list_of_set_map) have 3: "list.set (?f v) \ N" if "v \ k" for v using that proof (induction v) case 0 have "card (AF k i) \ N" by (metis DF_N DF_ne Inf_nat_def1 card_AF subsetD) with 0 show ?case by simp next case (Suc v) then have "enum (DF k i) (Suc v) \ N" by (metis DF_N card_DF finite_enumerate_in_set finite_DF in_mono le_imp_less_Suc) with Suc \i < m\ show ?case by (simp del: sum.atMost_Suc) qed show ?thesis unfolding LENS_def by (metis 3 Suc_pred' \0 < ka\ \ka - 1 \ k\ eq f lessThan_Suc_atMost) qed define LENS_QQ where "LENS_QQ \ acc_lengths 0 (list_of (AF k q) # QQ)" have LENS_QQ_subset: "list.set LENS_QQ \ list.set (LENS q)" proof (cases "ka = Suc k") case True with \k \ 2\ show ?thesis unfolding QQ_def LENS_QQ_def LENS_def by (auto simp: list_of_RF_Un split_list_interval acc_lengths_append) next case False then have "ka=k" using kka by linarith with \k \ 2\ show ?thesis by (simp add: QQ_def LENS_QQ_def LENS_def split_list_interval) qed have ss_INT: "strict_sorted ?INT" proof (rule strict_sorted_interact_I) fix n assume "n < length QQ" then have n: "n < k-1" by simp have "n = k - 2" if "\ n < k - 2" using n that by linarith moreover have "list_of (RF (Suc (k - 2)) p) < list_of (RF (k-1) q \ RF (ka - 1) q)" by (auto simp: less_sets_imp_sorted_list_of_set less_sets_Un2 less_RF_RF less_RF_k_ka \0 < k\) ultimately show "PP ! n < QQ ! n" using \k \ ka\ n by (auto simp: PP_n QQ_n less_sets_imp_sorted_list_of_set less_RF_RF) next fix n have V: "\Suc n < ka - 1\ \ list_of (RF (Suc n) q) < list_of (RF (Suc (Suc n)) p)" for n by (smt RF_def Suc_leI \ka - 1 \ k\ \q < m\ diff_Suc_1 finite_RF less_QF_step less_le_trans less_sets_imp_sorted_list_of_set nat_neq_iff zero_less_Suc) have "RF (k - 1) q \ RF k p" by (metis One_nat_def RF_non_Nil Suc_pred \0 < k\ finite_RF lessI less_RF_Suc less_RF_k less_sets_trans sorted_list_of_set_eq_Nil_iff) with kka have "RF (k-1) q \ RF (ka - 1) q \ RF k p" by (metis less_RF_k One_nat_def less_sets_Un1 antisym_conv2 diff_Suc_1 le_less_Suc_eq) then have VI: "list_of (RF (k-1) q \ RF (ka - 1) q) < list_of (RF k p)" by (rule less_sets_imp_sorted_list_of_set) auto assume "Suc n < length PP" with \ka \ Suc k\ VI show "QQ ! n < PP ! Suc n" apply (clarsimp simp: PP_n QQ_n V) by (metis One_nat_def Suc_1 Suc_lessI add.right_neutral add_Suc_right diff_Suc_Suc ka_k_or_Suc less_diff_conv) next show "PP \ lists (- {[]})" using RF_non_Nil kka by (clarsimp simp: PP_def) (metis RF_non_Nil less_le_trans) show "QQ \ lists (- {[]})" using RF_non_Nil kka by (clarsimp simp: QQ_def) (metis RF_non_Nil Suc_pred \0 < k\ less_SucI One_nat_def) qed (use kka PP_def QQ_def in auto) then have ss_QQ: "strict_sorted (concat QQ)" using strict_sorted_interact_imp_concat by blast obtain zs where zs: "Form_Body ka k x y zs" and zs_N: "list.set zs \ N" proof (intro that exI conjI Form_Body.intros [OF \length x < length y\]) show "x = concat (list_of (AF k p) # PP)" using \ka > 0\ by (simp add: PP_def RF_0 xc sorted_list_of_set_k) let ?YR = "(map (list_of \ (\j. RF j q)) (list_of {0<..ka - 1 \ k\ less_le_trans) then show "list_of (RF (list_of {0<.. lists (- {[]})" using RF_non_Nil \ka \ Suc k\ by (auto simp: mem_lists_non_Nil) qed auto show "list.set (concat ?YR) = list.set (concat QQ)" using ka_k_or_Suc proof assume "ka = k" then show "list.set (concat (map (list_of \ (\j. RF j q)) (list_of {0<..k\2\ by simp (simp add: split_nat_interval QQ_def) next assume "ka = Suc k" then show "list.set (concat (map (list_of \ (\j. RF j q)) (list_of {0<..k\2\ by simp (auto simp: QQ_def split_nat_interval) qed qed then show "y = concat (list_of (AF k q) # QQ)" using \ka > 0\ by (simp add: RF_0 yc sorted_list_of_set_k) show "list_of (AF k p) # PP \ lists (- {[]})" "list_of (AF k q) # QQ \ lists (- {[]})" using RF_non_Nil kka by (auto simp: AF_ne PP_def QQ_def eq_commute [of "[]"]) show "list.set ((LENS p @ list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT)) \ N" using AF_subset_N RF_subset_N LENS_subset_N \p < m\ \q < m\ LENS_QQ_subset by (auto simp: subset_iff PP_def QQ_def) show "length (list_of (AF k p) # PP) = ka" "length (list_of (AF k q) # QQ) = k" using \0 < ka\ \0 < k\ by auto show "LENS p = acc_lengths 0 (list_of (AF k p) # PP)" by (auto simp: LENS_def PP_def) show "strict_sorted (LENS p @ list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT)" unfolding strict_sorted_append_iff proof (intro conjI ss_INT) show "LENS p < list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT" using AF_non_Nil [of k p] \k \ ka\ \ka \ Suc k\ \p < m\ card_AF_sum enum_DF_AF by (simp add: enum_DF_AF less_list_def card_AF_sum LENS_def sum_sorted_list_of_set_map del: acc_lengths.simps) show "strict_sorted (LENS p)" unfolding LENS_def by (rule strict_sorted_acc_lengths) (use RF_non_Nil AF_non_Nil kka in \auto simp: in_lists_conv_set\) show "strict_sorted LENS_QQ" unfolding LENS_QQ_def QQ_def by (rule strict_sorted_acc_lengths) (use RF_non_Nil AF_non_Nil kka in \auto simp: in_lists_conv_set\) have last_AF_DF: "last (list_of (AF k p)) < \ (DF k q)" using AF_DF [OF \p < q\, of k] AF_non_Nil [of k p] DF_ne [of k q] by (metis Inf_nat_def1 finite_AF last_in_set less_sets_def set_sorted_list_of_set) then show "list_of (AF k p) < LENS_QQ @ list_of (AF k q) @ ?INT" by (simp add: less_list_def card_AF LENS_QQ_def) show "LENS_QQ < list_of (AF k q) @ ?INT" using AF_non_Nil [of k q] \q < m\ card_AF_sum enum_DF_AF card_AF_sum_QQ by (auto simp: less_list_def AF_ne hd_append card_AF_sum LENS_QQ_def) show "list_of (AF k q) < ?INT" proof - have "AF k q \ RF 1 p" using \0 < k\ \p < m\ \q < m\ by (simp add: RF_def less_QF flip: QF_0) then have "last (list_of (AF k q)) < hd (list_of (RF 1 p))" proof (rule less_setsD) show "last (list_of (AF k q)) \ AF k q" using AF_non_Nil finite_AF last_in_set set_sorted_list_of_set by blast show "hd (list_of (RF 1 p)) \ RF 1 p" by (metis One_nat_def RF_non_Nil \0 < k\ finite_RF hd_in_set not_less_eq set_sorted_list_of_set) qed with \k > 0\ \ka \ 2\ RF_non_Nil show ?thesis by (simp add: One_nat_def hd_interact less_list_def sorted_list_of_set_greaterThanLessThan PP_def QQ_def) qed qed auto qed (auto simp: LENS_QQ_def) show ?thesis proof (cases "ka = k") case True then have "l = 2*k-1" by (simp add: kka(3) mult_2) then show ?thesis by (metis One_nat_def Form.intros(2) Form_Body_imp_inter_scheme True \0 < k\ \U = {x, y}\ kka zs zs_N) next case False then have "l = 2*k" using kka by linarith then show ?thesis by (metis One_nat_def False Form.intros(3) Form_Body_imp_inter_scheme \0 < k\ \U = {x, y}\ antisym kka le_SucE zs zs_N) qed qed qed qed qed subsection \Larson's Lemma 3.8\ subsubsection \Primitives needed for the inductive construction of @{term b}\ definition IJ where "IJ \ \k. Sigma {..k} (\j::nat. {.. IJ k \ (\j i. u = (j,i) \ i j\k)" by (auto simp: IJ_def) lemma finite_IJ: "finite (IJ k)" by (auto simp: IJ_def) fun prev where "prev 0 0 = None" | "prev (Suc 0) 0 = None" | "prev (Suc j) 0 = Some (j, j - Suc 0)" | "prev j (Suc i) = Some (j,i)" lemma prev_eq_None_iff: "prev j i = None \ j \ Suc 0 \ i = 0" by (auto simp: le_Suc_eq elim: prev.elims) lemma prev_pair_less: "prev j i = Some ji' \ (ji', (j,i)) \ pair_less" by (auto simp: pair_lessI1 elim: prev.elims) lemma prev_Some_less: "\prev j i = Some (j',i'); i \ j\ \ i' < j'" by (auto elim: prev.elims) lemma prev_maximal: "\prev j i = Some (j',i'); (ji'', (j,i)) \ pair_less; ji'' \ IJ k\ \ (ji'', (j',i')) \ pair_less \ ji'' = (j',i')" by (force simp: IJ_def pair_less_def elim: prev.elims) lemma pair_less_prev: assumes "(u, (j,i)) \ pair_less" "u \ IJ k" shows "prev j i = Some u \ (\x. (u, x) \ pair_less \ prev j i = Some x)" proof (cases "prev j i") case None then show ?thesis using assms by (force simp: prev_eq_None_iff pair_less_def IJ_def split: prod.split) next case (Some a) then show ?thesis by (metis assms prev_maximal prod.exhaust_sel) qed subsubsection \Special primitives for the ordertype proof\ definition USigma :: "'a set set \ ('a set \ 'a set) \ 'a set set" where "USigma \ B \ \X\\. \y \ B X. {insert y X}" definition usplit where "usplit f A \ f (A - {Max A}) (Max A)" lemma USigma_empty [simp]: "USigma {} B = {}" by (auto simp: USigma_def) lemma USigma_iff: assumes "\I j. I \ \ \ I \ J I \ finite I" shows "x \ USigma \ J \ usplit (\I j. I \ \ \ j \ J I \ x = insert j I) x" proof - have [simp]: "\I j. \I \ \; j \ J I\ \ Max (insert j I) = j" by (meson Max_insert2 assms less_imp_le less_sets_def) show ?thesis proof - have \
: "j \ I" if "I \ \" "j \ J I" for I j using that by (metis assms less_irrefl less_sets_def) have "\I\\. \j\J I. x = insert j I" if "x - {Max x} \ \" and "Max x \ J (x - {Max x})" "x \ {}" using that by (metis Max_in assms infinite_remove insert_Diff) then show ?thesis by (auto simp: USigma_def usplit_def \
) qed qed proposition ordertype_append_image_IJ: assumes lenB [simp]: "\i j. i \ \ \ j \ J i \ length (B j) = c" and AB: "\i j. i \ \ \ j \ J i \ A i < B j" and IJ: "\i. i \ \ \ i \ J i \ finite i" and \: "\i. i \ \ \ ordertype (B  J i) (lenlex less_than) = \" and A: "inj_on A \" shows "ordertype (usplit (\i j. A i @ B j)  USigma \ J) (lenlex less_than) = \ * ordertype (A  \) (lenlex less_than)" (is "ordertype ?AB ?R = _ * ?\") proof (cases "\ = {}") case False have "Ord \" using \ False wf_Ord_ordertype by fastforce show ?thesis proof (subst ordertype_eq_iff) define split where "split \ \l::nat list. (take (length l - c) l, (drop (length l - c) l))" have oB: "ordermap (B  J i) ?R (B j) \ \" if \i \ \\ \j \ J i\ for i j using \ less_TC_iff that by fastforce then show "Ord (\ * ?\)" by (intro \Ord \\ wf_Ord_ordertype Ord_mult; simp) define f where "f \ \u. let (x,y) = split u in let i = inv_into \ A x in \ * ordermap (A\) ?R x + ordermap (BJ i) ?R y" have inv_into_IA [simp]: "inv_into \ A (A i) = i" if "i \ \" for i by (simp add: A that) show "\f. bij_betw f ?AB (elts (\ * ?\)) \ (\x\?AB. \y\?AB. (f x < f y) = ((x, y) \ ?R))" unfolding bij_betw_def proof (intro exI conjI strip) show "inj_on f ?AB" proof (clarsimp simp: f_def inj_on_def split_def USigma_iff IJ usplit_def) fix x y assume \
: "\ * ordermap (A  \) ?R (A (x - {Max x})) + ordermap (B  J (x - {Max x})) ?R (B (Max x)) = \ * ordermap (A  \) ?R (A (y - {Max y})) + ordermap (B  J (y - {Max y})) ?R (B (Max y))" and x: "x - {Max x} \ \" and y: "y - {Max y} \ \" and mx: "Max x \ J (x - {Max x})" and "x = insert (Max x) x" and my: "Max y \ J (y - {Max y})" have "ordermap (A\) ?R (A (x - {Max x})) = ordermap (A\) ?R (A (y - {Max y}))" and B_eq: "ordermap (B  J (x - {Max x})) ?R (B (Max x)) = ordermap (B  J (y - {Max y})) ?R (B (Max y))" using mult_cancellation_lemma [OF \
] oB mx my x y by blast+ then have "A (x - {Max x}) = A (y - {Max y})" using x y by auto then have "x - {Max x} = y - {Max y}" by (metis x y inv_into_IA) then show "A (x - {Max x}) = A (y - {Max y}) \ B (Max x) = B (Max y)" using B_eq mx my by auto qed show "f  ?AB = elts (\ * ?\)" proof show "f  ?AB \ elts (\ * ?\)" using \Ord \\ apply (clarsimp simp add: f_def split_def USigma_iff IJ usplit_def) by (metis TC_small \ add_mult_less image_eqI ordermap_in_ordertype trans_llt wf_Ord_ordertype wf_llt) show "elts (\ * ?\) \ f  ?AB" proof (clarsimp simp: f_def split_def image_iff USigma_iff IJ usplit_def Bex_def elim!: elts_multE split: prod.split) fix \ \ assume \: "\ \ elts \" and \: "\ \ elts ?\" have "\ \ ordermap (A  \) (lenlex less_than)  A  \" by (meson \ ordermap_surj subset_iff) then obtain i where "i \ \" and yv: "\ = ordermap (A\) ?R (A i)" by blast have "\ \ ordermap (B  J i) (lenlex less_than)  B  J i" by (metis (no_types) \ \ \i \ \\ in_mono ordermap_surj) then obtain j where "j \ J i" and xu: "\ = ordermap (BJ i) ?R (B j)" by blast then have mji: "Max (insert j i) = j" by (meson IJ Max_insert2 \i \ \\ less_imp_le less_sets_def) have [simp]: "i - {j} = i" using IJ \i \ \\ \j \ J i\ less_setsD by fastforce show "\l. (\K. K - {Max K} \ \ \ Max K \ J (K - {Max K}) \ K = insert (Max K) K \ l = A (K - {Max K}) @ B (Max K)) \ \ * \ + \ = \ * ordermap (A  \) ?R (take (length l - c) l) + ordermap (B  J (inv_into \ A (take (length l - c) l))) ?R (drop (length l - c) l)" proof (intro conjI exI) let ?ji = "insert j i" show "A i @ B j = A (?ji - {Max ?ji}) @ B (Max ?ji)" by (auto simp: mji) qed (use \i \ \\ \j \ J i\ mji xu yv in auto) qed qed next fix p q assume "p \ ?AB" and "q \ ?AB" then obtain x y where peq: "p = A (x - {Max x}) @ B (Max x)" and qeq: "q = A (y - {Max y}) @ B (Max y)" and x: "x - {Max x} \ \" and y: "y - {Max y} \ \" and mx: "Max x \ J (x - {Max x})" and my: "Max y \ J (y - {Max y})" by (auto simp: USigma_iff IJ usplit_def) let ?mx = "x - {Max x}" let ?my = "y - {Max y}" show "(f p < f q) \ ((p, q) \ ?R)" proof assume "f p < f q" then consider "ordermap (A\) ?R (A (x - {Max x})) < ordermap (A\) ?R (A (y - {Max y}))" | "ordermap (A\) ?R (A (x - {Max x})) = ordermap (A\) ?R (A (y - {Max y}))" "ordermap (BJ (x - {Max x})) ?R (B (Max x)) < ordermap (BJ (y - {Max y})) ?R (B (Max y))" using x y mx my by (auto dest: mult_cancellation_less simp: f_def split_def peq qeq oB) then have "(A ?mx @ B (Max x), A ?my @ B (Max y)) \ ?R" proof cases case 1 then have "(A ?mx, A ?my) \ ?R" using x y by (force simp: Ord_mem_iff_lt intro: converse_ordermap_mono) then show ?thesis using x y mx my lenB lenlex_append1 by blast next case 2 then have "A ?mx = A ?my" using \?my \ \\ \?mx \ \\ by auto then have eq: "?mx = ?my" by (metis \?my \ \\ \?mx \ \\ inv_into_IA) then have "(B (Max x), B (Max y)) \ ?R" using mx my 2 by (force simp: Ord_mem_iff_lt intro: converse_ordermap_mono) with 2 show ?thesis by (simp add: eq irrefl_less_than) qed then show "(p,q) \ ?R" by (simp add: peq qeq f_def split_def sorted_list_of_set_Un AB) next assume pqR: "(p,q) \ ?R" then have \
: "(A ?mx @ B (Max x), A ?my @ B (Max y)) \ ?R" using peq qeq by blast then consider "(A ?mx, A ?my) \ ?R" | "A ?mx = A ?my \ (B (Max x), B (Max y)) \ ?R" proof (cases "(A ?mx, A ?my) \ ?R") case False have False if "(A ?my, A ?mx) \ ?R" by (metis \?my \ \\ \?mx \ \\ "\
" $$Max y) \ J ?my\ \(Max x) \ J ?mx\ lenB lenlex_append1 omega_sum_1_less order.asym that) then have "A ?mx = A ?my" by (meson False UNIV_I total_llt total_on_def) then show ?thesis using "\ " irrefl_less_than that(2) by auto qed (use that in blast) then have "\ * ordermap (A$$ ?R (A ?mx) + ordermap (BJ ?mx) ?R (B (Max x)) < \ * ordermap (A\) ?R (A ?my) + ordermap (BJ ?my) ?R (B (Max y))" proof cases case 1 show ?thesis proof (rule add_mult_less_add_mult) show "ordermap (A\) (lenlex less_than) (A ?mx) < ordermap (A\) (lenlex less_than) (A ?my)" by (simp add: "1" \?my \ \\ \?mx \ \\ ordermap_mono_less) show "Ord (ordertype (A\) ?R)" using wf_Ord_ordertype by blast show "ordermap (B  J ?mx) ?R (B (Max x)) \ elts \" using Ord_less_TC_mem \Ord \\ \?mx \ \\ $$Max x) \ J ?mx\ oB by blast show "ordermap (B  J ?my) ?R (B (Max y)) \ elts \" using Ord_less_TC_mem \Ord \\ \?my \ \\ \(Max y) \ J ?my\ oB by blast qed (use \?my \ \\ \?mx \ \\ \Ord \\ in auto) next case 2 with \?mx \ \\ show ?thesis using \(Max y) \ J ?my\ \(Max x) \ J ?mx\ ordermap_mono_less by (metis (no_types, hide_lams) Kirby.add_less_cancel_left TC_small image_iff inv_into_IA trans_llt wf_llt y) qed then show "f p < f q" using \?my \ \\ \?mx \ \\ \(Max y) \ J ?my\ \(Max x) \ J ?mx\ by (auto simp: peq qeq f_def split_def AB) qed qed qed auto qed auto subsubsection \The final part of 3.8, where two sequences are merged\ inductive merge :: "[nat list list,nat list list,nat list list,nat list list] \ bool" where NullNull: "merge [] [] [] []" | Null: "as \ [] \ merge as [] [concat as] []" | App: "\as1 \ []; bs1 \ []; concat as1 < concat bs1; concat bs1 < concat as2; merge as2 bs2 as bs\ \ merge (as1@as2) (bs1@bs2) (concat as1 # as) (concat bs1 # bs)" inductive_simps Null1 [simp]: "merge [] bs us vs" inductive_simps Null2 [simp]: "merge as [] us vs" lemma merge_single: "\concat as < concat bs; concat as \ []; concat bs \ []\ \ merge as bs [concat as] [concat bs]" using merge.App [of as bs "[]" "[]"] by (fastforce simp: less_list_def) lemma merge_length1_nonempty: assumes "merge as bs us vs" "as \ lists (- {[]})" shows "us \ lists (- {[]})" using assms by induction (auto simp: mem_lists_non_Nil) lemma merge_length2_nonempty: assumes "merge as bs us vs" "bs \ lists (- {[]})" shows "vs \ lists (- {[]})" using assms by induction (auto simp: mem_lists_non_Nil) lemma merge_length1_gt_0: assumes "merge as bs us vs" "as \ []" shows "length us > 0" using assms by induction auto lemma merge_length_le: assumes "merge as bs us vs" shows "length vs \ length us" using assms by induction auto lemma merge_length_le_Suc: assumes "merge as bs us vs" shows "length us \ Suc (length vs)" using assms by induction auto lemma merge_length_less2: assumes "merge as bs us vs" shows "length vs \ length as" using assms proof induction case (App as1 bs1 as2 bs2 as bs) then show ?case using length_greater_0_conv [of as1] by (simp, presburger) qed auto lemma merge_preserves: assumes "merge as bs us vs" shows "concat as = concat us \ concat bs = concat vs" using assms by induction auto lemma merge_interact: assumes "merge as bs us vs" "strict_sorted (concat as)" "strict_sorted (concat bs)" "bs \ lists (- {[]})" shows "strict_sorted (interact us vs)" using assms proof induction case (App as1 bs1 as2 bs2 as bs) then have bs: "concat bs1 < concat bs" "concat bs1 < concat as" and xx: "concat bs1 \ []" using merge_preserves strict_sorted_append_iff by fastforce+ then have "concat bs1 < interact as bs" unfolding less_list_def using App bs - by (metis (no_types, lifting) Un_iff concat_append hd_in_set last_in_set merge_preserves set_interact sorted_wrt_append strict_sorted_append_iff strict_sorted_sorted_wrt) + by (metis (no_types, lifting) Un_iff concat_append hd_in_set last_in_set merge_preserves set_interact sorted_wrt_append strict_sorted_append_iff) with App show ?case apply (simp add: strict_sorted_append_iff del: concat_eq_Nil_conv) by (metis hd_append2 less_list_def xx) qed auto lemma acc_lengths_merge1: assumes "merge as bs us vs" shows "list.set (acc_lengths k us) \ list.set (acc_lengths k as)" using assms proof (induction arbitrary: k) case (App as1 bs1 as2 bs2 as bs) then show ?case apply (simp add: acc_lengths_append strict_sorted_append_iff length_concat_acc_lengths) by (simp add: le_supI2 length_concat) qed (auto simp: length_concat_acc_lengths) lemma acc_lengths_merge2: assumes "merge as bs us vs" shows "list.set (acc_lengths k vs) \ list.set (acc_lengths k bs)" using assms proof (induction arbitrary: k) case (App as1 bs1 as2 bs2 as bs) then show ?case apply (simp add: acc_lengths_append strict_sorted_append_iff length_concat_acc_lengths) by (simp add: le_supI2 length_concat) qed (auto simp: length_concat_acc_lengths) lemma length_hd_le_concat: assumes "as \ []" shows "length (hd as) \ length (concat as)" by (metis (no_types) add.commute assms concat.simps(2) le_add2 length_append list.exhaust_sel) lemma length_hd_merge2: assumes "merge as bs us vs" shows "length (hd bs) \ length (hd vs)" using assms by induction (auto simp: length_hd_le_concat) lemma merge_less_sets_hd: assumes "merge as bs us vs" "strict_sorted (concat as)" "strict_sorted (concat bs)" "bs \ lists (- {[]})" shows "list.set (hd us) \ list.set (concat vs)" using assms proof induction case (App as1 bs1 as2 bs2 as bs) then have \ : "list.set (concat bs1) \ list.set (concat bs2)" by (force simp: dest: strict_sorted_imp_less_sets) have *: "list.set (concat as1) \ list.set (concat bs1)" using App by (metis concat_append strict_sorted_append_iff strict_sorted_imp_less_sets) then have "list.set (concat as1) \ list.set (concat bs)" using App \ less_sets_trans merge_preserves by (metis List.set_empty append_in_lists_conv le_zero_eq length_0_conv length_concat_ge) with * App.hyps show ?case by (fastforce simp: less_sets_UN1 less_sets_UN2 less_sets_Un2) qed auto lemma set_takeWhile: assumes "strict_sorted (concat as)" "as \ lists (- {[]})" shows "list.set (takeWhile (\x. x < y) as) = {x \ list.set as. x < y}" using assms proof (induction as) case (Cons a as) have "a < y" if a: "a < concat as" "strict_sorted a" "strict_sorted (concat as)" "x < y" "x \ []" "x \ list.set as" for x proof - have "last x \ list.set (concat as)" using set_concat that(5) that(6) by fastforce then have "last a < hd (concat as)" using Cons.prems that by (auto simp: less_list_def) also have "\ \ hd y" if "y \ []" using that a by (meson \last x \ list.set (concat as)\ dual_order.strict_trans less_list_def not_le sorted_hd_le strict_sorted_imp_sorted) finally show ?thesis by (simp add: less_list_def) qed then show ?case using Cons by (auto simp: strict_sorted_append_iff) qed auto proposition merge_exists: assumes "strict_sorted (concat as)" "strict_sorted (concat bs)" "as \ lists (- {[]})" "bs \ lists (- {[]})" "hd as < hd bs" "as \ []" "bs \ []" and disj: "\a b. \a \ list.set as; b \ list.set bs\ \ a bus vs. merge as bs us vs" using assms proof (induction "length as + length bs" arbitrary: as bs rule: less_induct) case (less as bs) obtain as1 as2 bs1 bs2 where A: "as1 \ []" "bs1 \ []" "concat as1 < concat bs1" "concat bs1 < concat as2" and B: "as = as1@as2" "bs = bs1@bs2" and C: "bs2 = [] \ (as2 \ [] \ hd as2 < hd bs2)" proof define as1 where "as1 \ takeWhile (\x. x < hd bs) as" define as2 where "as2 \ dropWhile (\x. x < hd bs) as" define bs1 where "bs1 \ if as2=[] then bs else takeWhile (\x. x < hd as2) bs" define bs2 where "bs2 \ if as2=[] then [] else dropWhile (\x. x < hd as2) bs" have as1: "as1 = takeWhile (\x. last x < hd (hd bs)) as" using less.prems by (auto simp: as1_def less_list_def cong: takeWhile_cong) have as2: "as2 = dropWhile (\x. last x < hd (hd bs)) as" using less.prems by (auto simp: as2_def less_list_def cong: dropWhile_cong) have hd_as2: "as2 \ [] \ \ hd as2 < hd bs" using as2_def hd_dropWhile by metis have hd_bs2: "bs2 \ [] \ \ hd bs2 < hd as2" using bs2_def hd_dropWhile by metis show "as1 \ []" by (simp add: as1_def less.prems takeWhile_eq_Nil_iff) show "bs1 \ []" by (metis as2 bs1_def hd_as2 hd_in_set less.prems(7) less.prems(8) set_dropWhileD takeWhile_eq_Nil_iff) show "bs2 = [] \ (as2 \ [] \ hd as2 < hd bs2)" by (metis as2_def bs2_def hd_bs2 less.prems(8) list.set_sel(1) set_dropWhileD) have AB: "list.set A \ list.set B" if "A \ list.set as1" "B \ list.set bs" for A B proof - have "A \ list.set as" using that by (metis as1 set_takeWhileD) then have "sorted A" by (metis concat.simps(2) concat_append less.prems(1) sorted_append split_list_last strict_sorted_imp_sorted) moreover have "sorted (hd bs)" by (metis concat.simps(2) hd_Cons_tl less.prems(2) less.prems(7) strict_sorted_append_iff strict_sorted_imp_sorted) ultimately show ?thesis using that less.prems apply (clarsimp simp add: as1_def set_takeWhile less_list_iff_less_sets less_sets_def) by (metis (full_types) UN_I hd_concat less_le_trans list.set_sel(1) set_concat sorted_hd_le strict_sorted_imp_sorted) qed show "as = as1@as2" by (simp add: as1_def as2_def) show "bs = bs1@bs2" by (simp add: bs1_def bs2_def) have "list.set (concat as1) \ list.set (concat bs1)" using AB set_takeWhileD by (fastforce simp: as1_def bs1_def less_sets_UN1 less_sets_UN2) then show "concat as1 < concat bs1" by (rule less_sets_imp_list_less) have "list.set (concat bs1) \ list.set (concat as2)" if "as2 \ []" proof (clarsimp simp add: bs1_def less_sets_UN1 less_sets_UN2 set_takeWhile less.prems) fix A B assume "A \ list.set as2" "B \ list.set bs" "B < hd as2" with that show "list.set B \ list.set A" using hd_as2 less.prems(1,2) apply (clarsimp simp add: less_sets_def less_list_def) apply (auto simp: as2_def) apply (simp flip: as2_def) by (smt (verit, ccfv_SIG) UN_I \as = as1 @ as2\ concat.simps(2) concat_append hd_concat in_set_conv_decomp_first le_less_trans less_le_trans set_concat sorted_append sorted_hd_le sorted_le_last strict_sorted_imp_sorted that) qed then show "concat bs1 < concat as2" by (simp add: bs1_def less_sets_imp_list_less) qed obtain cs ds where "merge as2 bs2 cs ds" proof (cases "as2 = [] \ bs2 = []") case True then show thesis using that C NullNull Null by metis next have \: "length as2 + length bs2 < length as + length bs" by (simp add: A B) case False moreover have "strict_sorted (concat as2)" "strict_sorted (concat bs2)" "as2 \ lists (- {[]})" "bs2 \ lists (- {[]})" "\a b. \a \ list.set as2; b \ list.set bs2\ \ a < b \ b < a" using B less.prems strict_sorted_append_iff by auto ultimately show ?thesis using C less.hyps [OF \] False that by force qed then obtain cs where "merge (as1 @ as2) (bs1 @ bs2) (concat as1 # cs) (concat bs1 # ds)" using A merge.App by blast then show ?case using B by blast qed subsubsection \Actual proof of Larson's Lemma 3.8\ proposition lemma_3_8: assumes "infinite N" obtains X where "X \ WW" "ordertype X (lenlex less_than) = \\\" "\u. u \ [X]\<^bsup>2\<^esup> \ \l. Form l u \ (l > 0 \ [enum N l] < inter_scheme l u \ List.set (inter_scheme l u) \ N)" proof - let ?LL = "lenlex less_than" define bf where "bf \ \M q. wfrec pair_less (\f (j,i). let R = (case prev j i of None \ M | Some u \ snd (f u)) in grab R (q j i))" have bf_rec: "bf M q (j,i) = (let R = (case prev j i of None \ M | Some u \ snd (bf M q u)) in grab R (q j i))" for M q j i by (subst (1) bf_def) (simp add: Let_def wfrec bf_def cut_apply prev_pair_less cong: conj_cong split: option.split) have "infinite (snd (bf M q u)) = infinite M \ fst (bf M q u) \ M \ snd (bf M q u) \ M" for M q u using wf_pair_less proof (induction u rule: wf_induct_rule) case (less u) then show ?case proof (cases u) case (Pair j i) with less.IH prev_pair_less show ?thesis apply (simp add: bf_rec [of M q j i] split: option.split) using fst_grab_subset snd_grab_subset by blast qed qed then have infinite_bf [simp]: "infinite (snd (bf M q u)) = infinite M" and bf_subset: "fst (bf M q u) \ M \ snd (bf M q u) \ M" for M q u by auto have bf_less_sets: "fst (bf M q ij) \ snd (bf M q ij)" if "infinite M" for M q ij using wf_pair_less proof (induction ij rule: wf_induct_rule) case (less u) then show ?case proof (cases u) case (Pair j i) with less_sets_grab show ?thesis by (simp add: bf_rec [of M q j i] less.IH prev_pair_less that split: option.split) qed qed have card_fst_bf: "finite (fst (bf M q (j,i))) \ card (fst (bf M q (j,i))) = q j i" if "infinite M" for M q j i by (simp add: that bf_rec [of M q j i] split: option.split) have bf_cong: "bf M q u = bf M q' u" if "snd u \ fst u" and eq: "\y x. \x\y; y\fst u\ \ q' y x = q y x" for M q q' u using wf_pair_less that proof (induction u rule: wf_induct_rule) case (less u) show ?case proof (cases u) case (Pair j i) with less.prems show ?thesis proof (clarsimp simp add: bf_rec [of M _ j i] split: option.split) fix j' i' assume *: "prev j i = Some (j',i')" then have **: "((j', i'), u) \ pair_less" by (simp add: Pair prev_pair_less) moreover have "i' < j'" using Pair less.prems by (simp add: prev_Some_less [OF *]) moreover have "\x y. \x \ y; y \ j'\ \ q' y x = q y x" using ** less.prems by (auto simp: pair_less_def Pair) ultimately show "grab (snd (bf M q (j',i'))) (q j i) = grab (snd (bf M q' (j',i'))) (q j i)" using less.IH by auto qed qed qed define ediff where "ediff \ \D:: nat \ nat set. \j i. enum (D j) (Suc i) - enum (D j) i" define F where "F \ \l (dl,a0::nat set,b0::nat \ nat \ nat set,M). let (d,Md) = grab (nxt M (enum N (Suc (2 * Suc l)))) (Suc l) in let (a,Ma) = grab Md (Min d) in let Gb = bf Ma (ediff (dl(l := d))) in let dl' = dl(l := d) in (dl', a, fst \ Gb, snd (Gb(l, l-1)))" define DF where "DF \ rec_nat (\i\{..<0}. {}, {}, \p. {}, N) F" have DF_simps: "DF 0 = (\i\{..<0}. {}, {}, \p. {}, N)" "DF (Suc l) = F l (DF l)" for l by (auto simp: DF_def) note cut_apply [simp] have inf [rule_format]: "\dl al bl L. DF l = (dl,al,bl,L) \ infinite L" for l by (induction l) (auto simp: DF_simps F_def Let_def grab_eqD infinite_nxtN assms split: prod.split) define \ where "\ \ \(dl, a, b, M). \l::nat. dl l \ a \ card a > 0 \ (\j\l. card (dl j) = Suc j) \ a \ \(range b) \ range b \ Collect finite \ a \ N \ \(range b) \ N \ infinite M \ b(l,l-1) \ M \ M \ N" have \_DF: "\ (DF (Suc l)) l" for l proof (induction l) case 0 show ?case using assms apply (clarsimp simp add: bf_rec F_def DF_simps \_def split: prod.split) apply (drule grab_eqD, blast dest: grab_eqD infinite_nxtN)+ apply (auto simp: less_sets_UN2 less_sets_grab card_fst_bf elim!: less_sets_weaken2) apply (metis card_1_singleton_iff Min_singleton greaterThan_iff insertI1 le0 nxt_subset_greaterThan subsetD) using nxt_subset snd_grab_subset bf_subset by blast+ next case (Suc l) then show ?case using assms unfolding Let_def DF_simps(2)[of "Suc l"] F_def \_def apply (clarsimp simp add: bf_rec DF_simps split: prod.split) apply (drule grab_eqD, metis grab_eqD infinite_nxtN)+ apply (safe, simp_all add: less_sets_UN2 less_sets_grab card_fst_bf card_Suc_eq_finite) apply (meson less_sets_weaken2) apply (metis Min_in gr0I greaterThan_iff insert_not_empty le_inf_iff less_asym nxt_def subsetD) apply (meson bf_subset less_sets_weaken2) apply (meson nxt_subset subset_eq) apply (meson bf_subset nxt_subset subset_eq) using bf_rec infinite_bf apply force using bf_less_sets bf_rec apply force by (metis bf_rec bf_subset nxt_subset subsetD) qed define d where "d \ \k. let (dk,ak,bk,M) = DF(Suc k) in dk k" define a where "a \ \k. let (dk,ak,bk,M) = DF(Suc k) in ak" define b where "b \ \k. let (dk,ak,bk,M) = DF(Suc k) in bk" define M where "M \ \k. let (dk,ak,bk,M) = DF k in M" have infinite_M [simp]: "infinite (M k)" for k by (auto simp: M_def inf split: prod.split) have M_Suc_subset: "M (Suc k) \ M k" for k apply (clarsimp simp add: Let_def M_def F_def DF_simps split: prod.split) apply (drule grab_eqD, blast dest: infinite_nxtN local.inf)+ using bf_subset nxt_subset by blast have Inf_M_Suc_ge: "Inf (M k) \ Inf (M (Suc k))" for k by (simp add: M_Suc_subset cInf_superset_mono infinite_imp_nonempty) have Inf_M_telescoping: "{Inf (M k)..} \ {Inf (M k')..}" if k': "k'\k" for k k' using that Inf_nat_def1 infinite_M unfolding Inf_nat_def atLeast_subset_iff by (metis M_Suc_subset finite.emptyI le_less_linear lift_Suc_antimono_le not_less_Least subsetD) have d_eq: "d k = fst (grab (nxt (M k) (enum N (Suc (2 * Suc k)))) (Suc k))" for k by (simp add: d_def M_def Let_def DF_simps F_def split: prod.split) then have finite_d [simp]: "finite (d k)" for k by simp then have d_ne [simp]: "d k \ {}" for k by (metis card.empty card_grab d_eq infinite_M infinite_nxtN nat.distinct(1)) have a_eq: "\M. a k = fst (grab M (Min (d k))) \ infinite M" for k apply (simp add: a_def d_def M_def Let_def DF_simps F_def split: prod.split) by (metis fst_conv grab_eqD infinite_nxtN local.inf) then have card_a: "card (a k) = Inf (d k)" for k by (metis cInf_eq_Min card_grab d_ne finite_d) have d_eq_dl: "d k = dl k" if "(dl,a,b,P) = DF l" "k < l" for k l dl a b P using that by (induction l arbitrary: dl a b P) (simp_all add: d_def DF_simps F_def Let_def split: prod.split_asm prod.split) have card_d [simp]: "card (d k) = Suc k" for k by (auto simp: d_eq infinite_nxtN) have d_ne [simp]: "d j \ {}" and a_ne [simp]: "a j \ {}" and finite_d [simp]: "finite (d j)" and finite_a [simp]: "finite (a j)" for j using \_DF [of "j"] by (auto simp: \_def a_def d_def card_gt_0_iff split: prod.split_asm) have da: "d k \ a k" for k using \_DF [of "k"] by (simp add: \_def a_def d_def split: prod.split_asm) have ab_same: "a k \ \(range(b k))" for k using \_DF [of "k"] by (simp add: \_def a_def b_def M_def split: prod.split_asm) have snd_bf_subset: "snd (bf M r (j,i)) \ snd (bf M r (j',i'))" if ji: "((j',i'), (j,i)) \ pair_less" "(j',i') \ IJ k" for M r k j i j' i' using wf_pair_less ji proof (induction rule: wf_induct_rule [where a= "(j,i)"]) case (less u) show ?case proof (cases u) case (Pair j i) then consider "prev j i = Some (j', i')" | x where "((j', i'), x) \ pair_less" "prev j i = Some x" using less.prems pair_less_prev by blast then show ?thesis proof cases case 2 with less.IH show ?thesis unfolding bf_rec Pair by (metis in_mono option.simps(5) prev_pair_less snd_grab_subset subsetI that(2)) qed (simp add: Pair bf_rec snd_grab_subset) qed qed have less_bf: "fst (bf M r (j',i')) \ fst (bf M r (j,i))" if ji: "((j',i'), (j,i)) \ pair_less" "(j',i') \ IJ k" and "infinite M" for M r k j i j' i' proof - consider "prev j i = Some (j', i')" | j'' i'' where "((j', i'), (j'',i'')) \ pair_less" "prev j i = Some (j'',i'')" by (metis pair_less_prev ji prod.exhaust_sel) then show ?thesis proof cases case 1 then show ?thesis using bf_less_sets bf_rec less_sets_fst_grab \infinite M\ by force next case 2 then have "fst (bf M r (j',i')) \ snd (bf M r (j'',i''))" by (meson bf_less_sets snd_bf_subset less_sets_weaken2 that) with 2 show ?thesis using bf_rec bf_subset less_sets_fst_grab \infinite M\ by auto qed qed have aM: "a k \ M (Suc k)" for k apply (clarsimp simp add: a_def M_def DF_simps F_def Let_def split: prod.split) by (meson bf_subset grab_eqD infinite_nxtN less_sets_weaken2 local.inf) then have "a k \ a (Suc k)" for k by (metis IntE card_d card.empty d_eq da fst_grab_subset less_sets_trans less_sets_weaken2 nat.distinct(1) nxt_def subsetI) then have aa: "a j \ a k" if "j b k (j,i)" if "k'\k" for k k' j i by (metis a_ne ab_same le_less less_sets_UN2 less_sets_trans rangeI that) have db: "d j \ b k (j,i)" if "j\k" for k j i by (meson a_ne ab da less_sets_trans that) have bMkk: "b k (k,k-1) \ M (Suc k)" for k using \_DF [of k] by (simp add: \_def b_def d_def M_def split: prod.split_asm) have b: "\P \ M k. infinite P \ (\j i. i\j \ j\k \ b k (j,i) = fst (bf P (ediff d) (j,i)))" for k proof (clarsimp simp: b_def DF_simps F_def Let_def split: prod.split) fix a a' d' dl bb P M' M'' assume gr: "grab M'' (Min d') = (a', M')" "grab (nxt P (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d', M'')" and DF: "DF k = (dl, a, bb, P)" have deq: "d j = (if j = k then d' else dl j)" if "j\k" for j proof (cases "j < k") case True then show ?thesis by (metis DF d_eq_dl less_not_refl) next case False then show ?thesis using that DF gr by (auto simp: d_def DF_simps F_def Let_def split: prod.split) qed have "M' \ P" by (metis gr in_mono nxt_subset snd_conv snd_grab_subset subsetI) also have "P \ M k" using DF by (simp add: M_def) finally have "M' \ M k" . moreover have "infinite M'" using DF by (metis (mono_tags) finite_grab_iff gr infinite_nxtN local.inf snd_conv) moreover have "ediff (dl(k := d')) j i = ediff d j i" if "j\k" for j i by (simp add: deq that ediff_def) then have "bf M' (ediff (dl(k := d'))) (j,i) = bf M' (ediff d) (j,i)" if "i \ j" "j\k" for j i using bf_cong that by fastforce ultimately show "\P\M k. infinite P \ (\j i. i \ j \ j \ k \ fst (bf M' (ediff (dl(k := d'))) (j,i)) = fst (bf P (ediff d) (j,i)))" by auto qed have card_b: "card (b k (j,i)) = enum (d j) (Suc i) - enum (d j) i" if "j\k" for k j i \\there's a short proof of this from the previous result but it would need @{term"i\j"}\ proof (clarsimp simp: b_def DF_simps F_def Let_def split: prod.split) fix dl and a a' d':: "nat set" and bb M M' M'' assume gr: "grab M'' (Min d') = (a', M')" "grab (nxt M (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d',M'')" and DF: "DF k = (dl, a, bb, M)" have "d j = (if j = k then d' else dl j)" proof (cases "j < k") case True then show ?thesis by (metis DF d_eq_dl less_not_refl) next case False then show ?thesis using that DF gr by (auto simp: d_def DF_simps F_def Let_def split: prod.split) qed then show "card (fst (bf M' (ediff (dl(k := d'))) (j,i))) = enum (d j) (Suc i) - enum (d j) i" using DF gr card_fst_bf grab_eqD infinite_nxtN local.inf ediff_def by auto qed have card_b_pos: "card (b k (j,i)) > 0" if "i < j" "j\k" for k j i by (simp add: card_b that finite_enumerate_step) have b_ne [simp]: "b k (j,i) \ {}" if "i < j" "j\k" for k j i using card_b_pos [OF that] less_imp_neq by fastforce+ have card_b_finite [simp]: "finite (b k u)" for k u using \_DF [of k] by (fastforce simp: \_def b_def) have bM: "b k (j,i) \ M (Suc k)" if "ik" for i j k proof - obtain M' where "M' \ M k" "infinite M'" and bk: "\j i. i\j \ j\k \ b k (j,i) = fst (bf M' (ediff d) (j,i))" using b by (metis (no_types, lifting)) show ?thesis proof (cases "j=k \ i = k-1") case False show ?thesis proof (rule less_sets_trans [OF _ bMkk]) show "b k (j,i) \ b k (k, k-1)" using that \infinite M'\ False by (force simp: bk pair_less_def IJ_def intro: less_bf) show "b k (k, k-1) \ {}" using b_ne that by auto qed qed (use bMkk in auto) qed have b_InfM: "\ (range (b k)) \ {\(M k)..}" for k proof (clarsimp simp add: \_def b_def M_def DF_simps F_def Let_def split: prod.split) fix r dl :: "nat \ nat set" and a b and d' a' M'' M' P and x j' i' :: nat assume gr: "grab M'' (Min d') = (a', M')" "grab (nxt P (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d', M'')" and DF: "DF k = (dl, a, b, P)" and x: "x \ fst (bf M' (ediff (dl(k := d'))) (j', i'))" have "infinite P" using DF local.inf by blast then have "M' \ P" by (meson gr grab_eqD infinite_nxtN nxt_subset order.trans) with bf_subset show "\ P \ x" using Inf_nat_def x le_less_linear not_less_Least by fastforce qed have b_Inf_M_Suc: "b k (j,i) \ {Inf(M (Suc k))}" if "ik" for k j i using bMkk [of k] that by (metis Inf_nat_def1 bM finite.emptyI infinite_M less_setsD less_sets_singleton2) have bb_same: "b k (j',i') \ b k (j,i)" if "((j',i'), (j,i)) \ pair_less" "(j',i') \ IJ k" for k j i j' i' using that unfolding b_def DF_simps F_def Let_def by (auto simp: less_bf grab_eqD infinite_nxtN local.inf split: prod.split) have bb: "b k' (j',i') \ b k (j,i)" if j: "i' < j'" "j'\k'" and k: "k' {Inf(M (Suc k'))}" using Suc_lessD b_Inf_M_Suc nat_less_le j by blast show "b k (j,i) \ {Inf(M (Suc k'))..}" by (meson Inf_M_telescoping Suc_leI UnionI b_InfM rangeI subset_eq k) qed have M_subset_N: "M k \ N" for k proof (cases k) case (Suc k') with \_DF [of k'] show ?thesis by (auto simp: M_def Let_def \_def split: prod.split) qed (auto simp: M_def DF_simps) have a_subset_N: "a k \ N" for k using \_DF [of k] by (simp add: a_def \_def split: prod.split prod.split_asm) have d_subset_N: "d k \ N" for k using M_subset_N [of k] d_eq fst_grab_subset nxt_subset by blast have b_subset_N: "b k (j,i) \ N" for k j i using \_DF [of k] by (force simp: b_def \_def) define \:: "[nat,nat] \ nat set set" where "\ \ \j0 j. nsets {j0<..} j" have \_finite: "finite K" and \_card: "card K = j" if "K \ \ j0 j" for K j0 j using that by (auto simp add: \_def nsets_def) have \_enum: "j0 < enum K i" if "K \ \ j0 j" "i < card K" for K j0 j i using that by (auto simp: \_def nsets_def finite_enumerate_in_set subset_eq) have \_0 [simp]: "\ k 0 = {{}}" for k by (auto simp: \_def) have \_Suc: "\ j0 (Suc j) = USigma (\ j0 j) (\K. {Max (insert j0 K)<..})" (is "?lhs = ?rhs") for j j0 proof show "\ j0 (Suc j) \ USigma (\ j0 j) (\K. {Max (insert j0 K)<..})" unfolding \_def nsets_def USigma_def proof clarsimp fix K assume K: "K \ {j0<..}" "finite K" "card K = Suc j" then have "Max K \ K" by (metis Max_in card_0_eq nat.distinct(1)) then obtain i where "Max (insert j0 (K - {Max K})) < i" "K = insert i (K - {Max K})" using K by (simp add: subset_iff) (metis DiffE Max.coboundedI insertCI insert_Diff le_neq_implies_less) then show "\L\{j0<..}. finite L \ card L = j \ (\i\{Max (insert j0 L)<..}. K = insert i L)" using K by (metis \Max K \ K\ card_Diff_singleton_if diff_Suc_1 finite_Diff greaterThan_iff insert_subset) qed show "?rhs \ \ j0 (Suc j)" by (force simp: \_def nsets_def USigma_def) qed define BB where "BB \ \j0 j K. list_of (a j0 \ (\i \j. BB j j  \ j j" have less_list_of: "BB j i K < list_of (b l (j,i))" if K: "K \ \ j i" "\j\K. j < l" and "i \ j" "j \ l" for j i K l unfolding BB_def proof (rule less_sets_imp_sorted_list_of_set) have "\i. i < card K \ b (enum K i) (j,i) \ b l (j, card K)" using that by (metis \_card \_enum \_finite bb finite_enumerate_in_set nat_less_le less_le_trans) then show "a j \ (\i b l (j,i)" using that unfolding \_def nsets_def by (auto simp: less_sets_Un1 less_sets_UN1 ab finite_enumerate_in_set subset_eq) qed auto have BB_Suc: "BB j0 (Suc j) K = usplit (\L k. BB j0 j L @ list_of (b k (j0, j))) K" if j: "j \ j0" and K: "K \ \ j0 (Suc j)" for j0 j K \\towards the ordertype proof\ proof - have Kj: "K \ {j0<..}" and [simp]: "finite K" and cardK: "card K = Suc j" using K by (auto simp: \_def nsets_def) have KMK: "K - {Max K} \ \ j0 j" using that by (simp add: \_Suc USigma_iff \_finite less_sets_def usplit_def) have "j0 < Max K" by (metis Kj Max_in cardK card_gt_0_iff greaterThan_iff subsetD zero_less_Suc) have MaxK: "Max K = enum K j" proof (rule Max_eqI) fix k assume "k \ K" with K cardK show "k \ enum K j" by (metis \finite K\ finite_enumerate_Ex finite_enumerate_mono_iff leI lessI not_less_eq) qed (auto simp: cardK finite_enumerate_in_set) have ene: "i enum (K - {enum K j}) i = enum K i" for i using finite_enumerate_Diff_singleton [OF \finite K\] by (simp add: cardK) have "BB j0 (Suc j) K = list_of ((a j0 \ (\x b (enum K j) (j0, j))" by (simp add: BB_def lessThan_Suc Un_ac) also have "\ = list_of ((a j0 \ (\i b (enum K j) (j0, j)" if "i enum K i" using that K by (metis \_enum cardK less_SucI less_imp_le_nat) show "enum K i < enum K j" by (simp add: cardK finite_enumerate_mono that) qed moreover have "a j0 \ b (enum K j) (j0, j)" using MaxK \j0 < Max K\ ab by auto ultimately show "a j0 \ (\x b (enum K j) (j0, j)" by (simp add: less_sets_Un1 less_sets_UN1) qed (auto simp: finite_UnI) also have "\ = BB j0 j (K - {Max K}) @ list_of (b (Max K) (j0, j))" by (simp add: BB_def MaxK ene) also have "\ = usplit (\L k. BB j0 j L @ list_of (b k (j0, j))) K" by (simp add: usplit_def) finally show ?thesis . qed have enum_d_0: "enum (d j) 0 = Inf (d j)" for j using enum_0_eq_Inf_finite by auto have Inf_b_less: "\(b k' (j',i')) < \(b k (j,i))" if j: "i' < j'" "i < j" "j'\k'" "j\k" and k: "k' (b k (k, k-1)) \ k-1" for k proof (induction k) case (Suc k) show ?case proof (cases "k=0") case False then have "\ (b k (k, k - 1)) < \ (b (Suc k) (Suc k, k))" using Inf_b_less by auto with Suc show ?thesis by simp qed auto qed auto have b_ge: "\ (b k (j,i)) \ k-1" if "k \ j" "j > i" for k j i proof - have "\ Suc (\ (b k (j, i))) < k" by (metis (no_types) Inf_b_less Suc_leI b_ge_k diff_Suc_1 lessI not_less that) then show ?thesis by simp qed have hd_b: "hd (list_of (b k (j,i))) = \ (b k (j,i))" if "i < j" "j \ k" for k j i using that by (simp add: hd_list_of cInf_eq_Min) have b_disjoint_less: "b (enum K i) (j0, i) \ b (enum K i') (j0, i') = {}" if K: "K \ {j0<..}" "finite K" "card K \ j0" "i' < j" "i < i'" "j \ j0" for i i' j j0 K proof (intro bb less_sets_imp_disjnt [unfolded disjnt_def]) show "i < j0" using that by linarith then show "j0 \ enum K i" by (meson K finite_enumerate_in_set greaterThan_iff less_imp_le_nat less_le_trans subsetD) show "enum K i < enum K i'" using K \j \ j0\ that by auto qed have b_disjoint: "b (enum K i) (j0, i) \ b (enum K i') (j0, i') = {}" if K: "K \ {j0<..}" "finite K" "card K \ j0" "i < j" "i' < j" "i \ i'" "j \ j0" for i i' j j0 K using that b_disjoint_less inf_commute neq_iff by metis have ot\: "ordertype ((\k. list_of (b k (j,i)))  {Max (insert j K)<..}) ?LL = \" (is "?lhs = _") if K: "K \ \ j i" "j > i" for j i K proof - have Sucj: "Suc (Max (insert j K)) \ j" using \_finite that(1) le_Suc_eq by auto let ?N = "{Inf(b k (j,i))| k. Max (insert j K) < k}" have infN: "infinite ?N" proof (clarsimp simp add: infinite_nat_iff_unbounded_le) fix m show "\n\m. \k. n = \ (b k (j,i)) \ Max (insert j K) < k" using b_ge \j > i\ Sucj by (metis (no_types, lifting) diff_Suc_1 le_SucI le_trans less_Suc_eq_le nat_le_linear) qed have [simp]: "Max (insert j K) < k \ j < k \ (\a\K. a < k)" for k using that by (auto simp: \_finite) have "?lhs = ordertype ?N less_than" proof (intro ordertype_eqI strip) have "list_of (b k (j,i)) = list_of (b k' (j,i))" if "j \ k" "j \ k'" "hd (list_of (b k (j,i))) = hd (list_of (b k' (j,i)))" for k k' by (metis Inf_b_less \i < j\ hd_b nat_less_le not_le that) moreover have "\k' j' i'. hd (list_of (b k (j,i))) = \ (b k' (j', i')) \ i' < j' \ j' \ k'" if "j \ k" for k using that \i < j\ hd_b less_imp_le_nat by blast moreover have "\k'. hd (list_of (b k (j,i))) = \ (b k' (j,i)) \ j < k' \ (\a\K. a < k')" if "j < k" "\a\K. a < k" for k using that K hd_b less_imp_le_nat by blast moreover have "\ (b k (j,i)) \ hd  (\k. list_of (b k (j,i)))  {Max (insert j K)<..}" if "j < k" "\a\K. a < k" for k using that K by (auto simp: hd_b image_iff) ultimately show "bij_betw hd ((\k. list_of (b k (j,i)))  {Max (insert j K)<..}) {\ (b k (j,i)) |k. Max (insert j K) < k}" by (auto simp: bij_betw_def inj_on_def) next fix ms ns assume "ms \ (\k. list_of (b k (j,i)))  {Max (insert j K)<..}" and "ns \ (\k. list_of (b k (j,i)))  {Max (insert j K)<..}" with that obtain k k' where ms: "ms = list_of (b k (j,i))" and ns: "ns = list_of (b k' (j,i))" and "j < k" "j < k'" and lt_k: "\a\K. a < k" and lt_k': "\a\K. a < k'" by (auto simp: \_finite) then have len_eq [simp]: "length ns = length ms" by (simp add: card_b) have nz: "length ns \ 0" using b_ne \i < j\ \j < k'\ ns by auto show "(hd ms, hd ns) \ less_than \ (ms, ns) \ ?LL" proof assume "(hd ms, hd ns) \ less_than" then show "(ms, ns) \ ?LL" using that nz by (fastforce simp: lenlex_def \_finite card_b intro: hd_lex) next assume \ : "(ms, ns) \ ?LL" then have "(list_of (b k' (j,i)), list_of (b k (j,i))) \ ?LL" using less_asym ms ns omega_sum_1_less by blast then show "(hd ms, hd ns) \ less_than" using \j < k\ \j < k'\ Inf_b_less [of i j i j] ms ns by (metis Cons_lenlex_iff \ len_eq b_ne card_b_finite diff_Suc_1 hd_Cons_tl hd_b length_Cons less_or_eq_imp_le less_than_iff linorder_neqE_nat sorted_list_of_set_eq_Nil_iff that(2)) qed qed auto also have "\ = \" using infN ordertype_nat_\ by blast finally show ?thesis . qed have ot\j: "ordertype (BB j0 j  \ j0 j) ?LL = \\j" if "j \ j0" for j j0 using that proof (induction j) \\a difficult proof, but no hints in Larson's text\ case 0 then show ?case by (auto simp: XX_def) next case (Suc j) then have ih: "ordertype (BB j0 j  \ j0 j) ?LL = \ \ j" by simp have "j \ j0" by (simp add: Suc.prems Suc_leD) have inj_BB: "inj_on (BB j0 j) ([{j0<..}]\<^bsup>j\<^esup>)" proof (clarsimp simp: inj_on_def BB_def nsets_def sorted_list_of_set_Un less_sets_UN2) fix X Y assume X: "X \ {j0<..}" and Y: "Y \ {j0<..}" and "finite X" "finite Y" and jeq: "j = card X" and "card Y = card X" and eq: "list_of (a j0 \ (\i (\in. \n < card X\ \ j0 \ enum X n" using X \finite X\ finite_enumerate_in_set less_imp_le_nat by blast have enumY: "\n. \n < card X\ \ j0 \ enum Y n" using subsetD [OF Y] by (metis \card Y = card X\ \finite Y\ finite_enumerate_in_set greaterThan_iff less_imp_le_nat) have smX: "strict_mono_sets {..i. b (enum X i) (j0, i))" and smY: "strict_mono_sets {..i. b (enum Y i) (j0, i))" using Suc.prems \card Y = card X\ \finite X\ \finite Y\ bb enumX enumY jeq by (auto simp: strict_mono_sets_def) have len_eq: "length ms = length ns" if "(ms, ns) \ list.set (zip (map (list_of \ (\i. b (enum X i) (j0,i))) (list_of {.. (\i. b (enum Y i) (j0,i))) (list_of {.. card X" for ms ns n using that by (induction n rule: nat.induct) (auto simp: card_b enumX enumY) have "concat (map (list_of \ (\i. b (enum X i) (j0, i))) (list_of {.. (\i. b (enum Y i) (j0, i))) (list_of {.. (\i. b (enum X i) (j0, i))) (list_of {.. (\i. b (enum Y i) (j0, i))) (list_of {.. (b (enum X i) (j0,i))" "Inf (b (enum Y i) (j0,i)) \ (b (enum Y i) (j0,i))" "i < j0" using Inf_nat_def1 Suc.prems b_ne enumX enumY jeq that by auto ultimately show ?thesis by (metis Inf_b_less enumX enumY leI nat_less_le that) qed then show "X = Y" by (simp add: \card Y = card X\ \finite X\ \finite Y\ finite_enum_ext) qed have BB_Suc': "BB j0 (Suc j) X = usplit (\L k. BB j0 j L @ list_of (b k (j0, j))) X" if "X \ USigma (\ j0 j) (\K. {Max (insert j0 K)<..})" for X using that by (simp add: USigma_iff \_finite less_sets_def usplit_def \_Suc BB_Suc \j \ j0$$ have "ordertype (BB j0 (Suc j)  \ j0 (Suc j)) ?LL = ordertype (usplit (\L k. BB j0 j L @ list_of (b k (j0, j)))  USigma (\ j0 j) (\K. {Max (insert j0 K)<..})) ?LL" by (simp add: BB_Suc' \_Suc) also have "\ = \ * ordertype (BB j0 j  \ j0 j) ?LL" proof (intro ordertype_append_image_IJ) fix L k assume "L \ \ j0 j" and "k \ {Max (insert j0 L)<..}" then have "j0 < k" and L: "\a. a \ L \ a < k" by (simp_all add: \_finite) then show "BB j0 j L < list_of (b k (j0, j))" by (simp add: \L \ \ j0 j\ \j \ j0\ \_finite less_list_of) next show "inj_on (BB j0 j) (\ j0 j)" by (simp add: \_def inj_BB) next fix L assume L: "L \ \ j0 j" then show "L \ {Max (insert j0 L)<..} \ finite L" by (simp add: \_finite less_sets_def) show "ordertype ((\i. list_of (b i (j0, j)))  {Max (insert j0 L)<..}) ?LL = \" using L Suc.prems Suc_le_lessD ot\ by blast qed (auto simp: \_finite card_b) also have "\ = \ \ ord_of_nat (Suc j)" by (simp add: oexp_mult_commute ih) finally show ?case . qed define seqs where "seqs \ \j0 j K. list_of (a j0) # (map (list_of \ (\i. b (enum K i) (j0,i))) (list_of {.. lists (- {[]})" if K: "K \ \ j0 j" and "j \ j0" for K j j0 proof - have j0: "\i. i < card K \ j0 \ enum K i" and le_j0: "card K \ j0" using finite_enumerate_in_set that unfolding \_def nsets_def by fastforce+ show "BB j0 j K = concat (seqs j0 j K)" using that unfolding BB_def \_def nsets_def seqs_def by (fastforce simp: j0 ab bb less_sets_UN2 sorted_list_of_set_Un strict_mono_sets_def sorted_list_of_set_UN_lessThan) have "b (enum K i) (j0, i) \ {}" if "i < card K" for i using j0 le_j0 less_le_trans that by simp moreover have "card K = j" using K \_card by blast ultimately show "seqs j0 j K \ lists (- {[]})" by (clarsimp simp: seqs_def) (metis card_b_finite sorted_list_of_set_eq_Nil_iff) qed have BB_decomp: "\cs. BB j0 j K = concat cs \ cs \ lists (- {[]})" if K: "K \ \ j0 j" and "j \ j0" for K j j0 using BB_eq_concat_seqs seqs_ne K that(2) by blast have a_subset_M: "a k \ M k" for k apply (clarsimp simp: a_def M_def DF_simps F_def Let_def split: prod.split_asm) by (metis (no_types) fst_conv fst_grab_subset nxt_subset snd_conv snd_grab_subset subsetD) have ba_Suc: "b k (j,i) \ a (Suc k)" if "i < j" "j \ k" for i j k by (meson a_subset_M bM less_sets_weaken2 nat_less_le that) have ba: "b k (j,i) \ a r" if "i < j" "j \ k" "k < r" for i j k r by (metis Suc_lessI a_ne aa ba_Suc less_sets_trans that) have disjnt_ba: "disjnt (b k (j,i)) (a r)" if "i < j" "j \ k" for i j k r by (meson ab ba disjnt_sym less_sets_imp_disjnt not_le that) have bb_disjnt: "disjnt (b k (j,i)) (b l (r,q))" if "q < r" "i < j" "j \ k" "r \ l" "j < r" for i j q r k l proof (cases "k=l") case True with that show ?thesis by (force simp: pair_less_def IJ_def intro: bb_same less_sets_imp_disjnt) next case False with that show ?thesis by (metis bb less_sets_imp_disjnt disjnt_sym nat_neq_iff) qed have sum_card_b: "(\i {j0<..}" "finite K" "card K \ j0" and "j \ j0" for j0 j K using \j \ j0\ proof (induction j) case 0 then show ?case by auto next case (Suc j) then have "j < card K" using that(3) by linarith have dis: "disjnt (b (enum K j) (j0, j)) (\ij < card K\ by (force simp: finite_enumerate_in_set) have "(\ii = card (b (enum K j) (j0, j)) + enum (d j0) j - enum (d j0) 0" using \Suc j \ j0\ by (simp add: Suc.IH split: nat_diff_split) also have "\ = enum (d j0) (Suc j) - enum (d j0) 0" using j0_less Suc.prems card_b less_or_eq_imp_le by force finally show ?case . qed have card_UN_b: "card (\i {j0<..}" "finite K" "card K \ j0" and "j \ j0" for j0 j K using that by (simp add: card_UN_disjoint sum_card_b b_disjoint) have len_BB: "length (BB j j K) = enum (d j) j" if K: "K \ \ j j" and "j \ j" for j K proof - have dis_ab: "\i. i < j \ disjnt (a j) (b (enum K i) (j,i))" using K \_card \_enum ab less_sets_imp_disjnt nat_less_le by blast show ?thesis using K unfolding BB_def \_def nsets_def by (simp add: card_UN_b card_Un_disjnt dis_ab card_a cInf_le_finite finite_enumerate_in_set enum_0_eq_Inf_finite) qed have "d k \ d (Suc k)" for k by (metis aM a_ne d_eq da less_sets_fst_grab less_sets_trans less_sets_weaken2 nxt_subset) then have dd: "d k' \ d k" if "k' < k" for k' k by (meson UNIV_I d_ne less_sets_imp_strict_mono_sets strict_mono_sets_def that) show thesis proof show "(\ (range XX)) \ WW" by (auto simp: XX_def BB_def WW_def) show "ordertype (\ (range XX)) (?LL) = \ \ \" using ot\j by (simp add: XX_def ordertype_\\) next fix U assume U: "U \ [\ (range XX)]\<^bsup>2\<^esup>" then obtain x y where Ueq: "U = {x,y}" and len_xy: "length x \ length y" by (auto simp: lenlex_nsets_2_eq lenlex_length) show "\l. Form l U \ (0 < l \ [enum N l] < inter_scheme l U \ list.set (inter_scheme l U) \ N)" proof (cases "length x = length y") case True then show ?thesis using Form.intros(1) U Ueq by fastforce next case False then have xy: "length x < length y" using len_xy by auto obtain j r K L where K: "K \ \ j j" and xeq: "x = BB j j K" and ne: "BB j j K \ BB r r L" and L: "L \ \ r r" and yeq: "y = BB r r L" using U by (auto simp: Ueq XX_def) then have "length x = enum (d j) j" "length y = enum (d r) r" by (auto simp: len_BB) then have "j < r" using xy dd by (metis card_d finite_enumerate_in_set finite_d lessI less_asym less_setsD linorder_neqE_nat) then have aj_ar: "a j \ a r" using aa by auto have Ksub: "K \ {j<..}" and "finite K" "card K \ j" using K by (auto simp: \_def nsets_def) have Lsub: "L \ {r<..}" and "finite L" "card L \ r" using L by (auto simp: \_def nsets_def) have enumK: "enum K i > j" if "i < j" for i using K \_card \_enum that by blast have enumL: "enum L i > r" if "i < r" for i using L \_card \_enum that by blast have "list.set (acc_lengths w (seqs j0 j K)) \ (+) w  d j0" if K: "K \ {j0<..}" "finite K" "card K \ j0" and "j \ j0" for j0 j K w using \j \ j0\ proof (induction j arbitrary: w) case 0 then show ?case by (simp add: seqs_def Inf_nat_def1 card_a) next case (Suc j) let ?db = "\ (d j0) + ((\i \ (d j0)" using Suc.prems card_d by (simp add: cInf_le_finite finite_enumerate_in_set) then have "?db = enum (d j0) (Suc j)" using Suc.prems that by (simp add: cInf_le_finite finite_enumerate_in_set sum_card_b card_b enum_d_0 \j0 < enum K j\ less_or_eq_imp_le) then have "?db \ d j0" using Suc.prems finite_enumerate_in_set by (auto simp: finite_enumerate_in_set) moreover have "list.set (acc_lengths w (seqs j0 j K)) \ (+) w  d j0" by (simp add: Suc Suc_leD) then have "list.set (acc_lengths (w + \ (d j0)) (map (list_of \ (\i. b (enum K i) (j0,i))) (list_of {.. (+) w  d j0" by (simp add: seqs_def card_a subset_insertI) ultimately show ?case by (simp add: seqs_def acc_lengths_append image_iff Inf_nat_def1 sum_sorted_list_of_set_map card_a) qed then have acc_lengths_subset_d: "list.set (acc_lengths 0 (seqs j0 j K)) \ d j0" if K: "K \ {j0<..}" "finite K" "card K \ j0" and "j \ j0" for j0 j K by (metis image_add_0 that) have "strict_sorted x" "strict_sorted y" by (auto simp: xeq yeq BB_def) have disjnt_xy: "disjnt (list.set x) (list.set y)" proof - have "disjnt (a j) (a r)" using \j < r\ aa less_sets_imp_disjnt by blast moreover have "disjnt (b (enum K i) (j,i)) (a r)" if "i < j" for i by (simp add: disjnt_ba enumK less_imp_le_nat that) moreover have "disjnt (a j) (b (enum L q) (r,q))" if "q < r" for q by (meson disjnt_ba disjnt_sym enumL less_imp_le_nat that) moreover have "disjnt (b (enum K i) (j,i)) (b (enum L q) (r,q))" if "i < j" "q < r" for i q by (meson \j < r\ bb_disjnt enumK enumL less_imp_le that) ultimately show ?thesis by (simp add: xeq yeq BB_def) qed have "\us vs. merge (seqs j j K) (seqs r r L) us vs" proof (rule merge_exists) show "strict_sorted (concat (seqs j j K))" using BB_eq_concat_seqs K \strict_sorted x\ xeq by auto show "strict_sorted (concat (seqs r r L))" using BB_eq_concat_seqs L \strict_sorted y\ yeq by auto show "seqs j j K \ lists (- {[]})" "seqs r r L \ lists (- {[]})" by (auto simp: K L seqs_ne) show "hd (seqs j j K) < hd (seqs r r L)" by (simp add: aj_ar less_sets_imp_list_less seqs_def) show "seqs j j K \ []" "seqs r r L \ []" using seqs_def by blast+ have less_bb: "b (enum K i) (j,i) \ b (enum L p) (r, p)" if "\ b (enum L p) (r, p) \ b (enum K i) (j,i)" and "i < j" "p < r" for i p by (metis IJ_iff \j < r\ bb bb_same enumK enumL less_imp_le_nat linorder_neqE_nat pair_lessI1 that) show "u < v \ v < u" if "u \ list.set (seqs j j K)" and "v \ list.set (seqs r r L)" for u v using that enumK enumL unfolding seqs_def apply (auto simp: seqs_def aj_ar intro!: less_bb less_sets_imp_list_less) apply (meson ab ba less_imp_le_nat not_le)+ done qed then obtain uus vvs where merge: "merge (seqs j j K) (seqs r r L) uus vvs" by metis then have "uus \ []" using merge_length1_gt_0 by (auto simp: seqs_def) then obtain u1 us where us: "u1#us = uus" by (metis neq_Nil_conv) define ku where "ku \ length (u1#us)" define ps where "ps \ acc_lengths 0 (u1#us)" have us_ne: "u1#us \ lists (- {[]})" using merge_length1_nonempty seqs_ne us merge us K by auto have xu_eq: "x = concat (u1#us)" using BB_eq_concat_seqs K merge merge_preserves us xeq by auto then have "strict_sorted u1" using \strict_sorted x\ strict_sorted_append_iff by auto have u_sub: "list.set ps \ list.set (acc_lengths 0 (seqs j j K))" using acc_lengths_merge1 merge ps_def us by blast have "vvs \ []" using merge BB_eq_concat_seqs L merge_preserves xy yeq by auto then obtain v1 vs where vs: "v1#vs = vvs" by (metis neq_Nil_conv) define kv where "kv \ length (v1#vs)" define qs where "qs \ acc_lengths 0 (v1#vs)" have vs_ne: "v1#vs \ lists (- {[]})" using L merge merge_length2_nonempty seqs_ne vs by auto have yv_eq: "y = concat (v1#vs)" using BB_eq_concat_seqs L merge merge_preserves vs yeq by auto then have "strict_sorted v1" using \strict_sorted y\ strict_sorted_append_iff by auto have v_sub: "list.set qs \ list.set (acc_lengths 0 (seqs r r L))" using acc_lengths_merge2 merge qs_def vs by blast have ss_concat_jj: "strict_sorted (concat (seqs j j K))" using BB_eq_concat_seqs K \strict_sorted x\ xeq by auto then obtain k: "0 < kv" "kv \ ku" "ku \ Suc kv" "kv \ Suc j" using us vs merge_length_le merge_length_le_Suc merge_length_less2 merge unfolding ku_def kv_def by fastforce define zs where "zs \ concat [ps,u1,qs,v1] @ interact us vs" have ss: "strict_sorted zs" proof - have ssp: "strict_sorted ps" unfolding ps_def by (meson strict_sorted_acc_lengths us_ne) have ssq: "strict_sorted qs" unfolding qs_def by (meson strict_sorted_acc_lengths vs_ne) have "d j \ list.set x" using da [of j] db [of j] K \_card \_enum nat_less_le by (auto simp: xeq BB_def less_sets_Un2 less_sets_UN2) then have ac_x: "acc_lengths 0 (seqs j j K) < x" by (meson Ksub \finite K\ \j \ card K\ acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1) then have "ps < x" by (meson Ksub \d j \ list.set x\ \finite K\ \j \ card K\ acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1 u_sub) then have "ps < u1" by (metis Nil_is_append_conv concat.simps(2) hd_append2 less_list_def xu_eq) have "d r \ list.set y" using da [of r] db [of r] L \_card \_enum nat_less_le by (auto simp: yeq BB_def less_sets_Un2 less_sets_UN2) then have "acc_lengths 0 (seqs r r L) < y" by (meson Lsub \finite L\ \r \ card L\ acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1) then have "qs < y" by (metis L Lsub \_card \d r \ list.set y\ \finite L\ acc_lengths_subset_d less_sets_imp_list_less less_sets_weaken1 order_refl v_sub) then have "qs < v1" by (metis concat.simps(2) gr_implies_not0 hd_append2 less_list_def list.size(3) xy yv_eq) have carda_v1: "card (a r) \ length v1" using length_hd_merge2 [OF merge] unfolding vs [symmetric] by (simp add: seqs_def) have ab_enumK: "\i. i < j \ a j \ b (enum K i) (j,i)" by (meson ab enumK le_trans less_imp_le_nat) have ab_enumL: "\q. q < r \ a j \ b (enum L q) (r,q)" by (meson \j < r\ ab enumL le_trans less_imp_le_nat) then have ay: "a j \ list.set y" by (auto simp: yeq BB_def less_sets_Un2 less_sets_UN2 aj_ar) have disjnt_hd_last_K_y: "disjnt {hd l..last l} (list.set y)" if l: "l \ list.set (seqs j j K)" for l proof (clarsimp simp add: yeq BB_def disjnt_iff Ball_def, intro conjI strip) fix u assume u: "u \ last l" and "hd l \ u" with l consider "u \ last (list_of (a j))" "hd (list_of (a j)) \ u" | i where "i last (list_of (b (enum K i) (j,i)))" "hd (list_of (b (enum K i) (j,i))) \ u" by (force simp: seqs_def) note l_cases = this then show "u \ a r" proof cases case 1 then show ?thesis by (metis a_ne aj_ar finite_a last_in_set leD less_setsD set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) next case 2 then show ?thesis by (metis enumK ab ba Inf_nat_def1 b_ne card_b_finite hd_b last_in_set less_asym less_setsD not_le set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) qed fix q assume "q < r" show "u \ b (enum L q) (r,q)" using l_cases proof cases case 1 then show ?thesis by (metis \q < r\ a_ne ab_enumL finite_a last_in_set leD less_setsD set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) next case 2 show ?thesis proof (cases "enum K i = enum L q") case True then show ?thesis using 2 bb_same [of concl: "enum L q" j i r q] \j < r\ u by (metis IJ_iff b_ne card_b_finite enumK last_in_set leD less_imp_le_nat less_setsD pair_lessI1 set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) next case False with 2 bb enumK enumL show ?thesis unfolding less_sets_def by (metis \q < r\ b_ne card_b_finite last_in_set leD less_imp_le_nat list.set_sel(1) nat_neq_iff set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff) qed qed qed have u1_y: "list.set u1 \ list.set y" using vs yv_eq L \strict_sorted y\ merge merge_less_sets_hd merge_preserves seqs_ne ss_concat_jj us by fastforce have u1_subset_seqs: "list.set u1 \ list.set (concat (seqs j j K))" using merge_preserves [OF merge] us by auto have "b k (j,i) \ d (Suc k)" if "j\k" "i d k'" if "j\k" "i d (Suc k)" for k by (metis aM d_eq less_sets_fst_grab less_sets_weaken2 nxt_subset) then have ad: "a k \ d k'" if "k list.set u1" for n proof - obtain l where l: "l \ list.set (seqs j j K)" and n: "n \ list.set l" using n u1_subset_seqs by auto then consider "l = list_of (a j)" | i where "l = list_of (b (enum K i) (j,i))" "i < j" by (force simp: seqs_def) then show ?thesis proof cases case 1 then show ?thesis by (metis Inf_nat_def1 \j < r\ ad d_ne finite_a less_setsD n set_sorted_list_of_set) next case 2 then have "hd (list_of (b (enum K i) (j,i))) = Min (b (enum K i) (j,i))" by (meson b_ne card_b_finite enumK hd_list_of less_imp_le_nat) also have "\ \ n" using 2 n by (simp add: less_list_def disjnt_iff less_sets_def) also have f8: "n < hd y" using less_setsD that u1_y by (metis gr_implies_not0 list.set_sel(1) list.size(3) xy) finally have "l < y" using 2 disjnt_hd_last_K_y [OF l] by (simp add: disjnt_iff) (metis leI less_imp_le_nat less_list_def list.set_sel(1)) moreover have "last (list_of (b (enum K i) (j,i))) < hd (list_of (a r))" using \l < y\ L n by (auto simp: 2yeq BB_eq_concat_seqs seqs_def less_list_def) then have "enum K i < r" by (metis "2"(1) a_ne ab card_b_finite empty_iff finite.emptyI finite_a last_in_set leI less_asym less_setsD list.set_sel(1) n set_sorted_list_of_set) moreover have "j \ enum K i" by (simp add: "2"(2) enumK less_imp_le_nat) ultimately show ?thesis using 2 n bd [of j "enum K i" i r] Inf_nat_def1 less_setsD by force qed qed then have "last u1 < Inf (d r)" using \uus \ []\ us_ne by auto also have "\ \ length v1" using card_a carda_v1 by auto finally have "last u1 < length v1" . then have "u1 < qs" by (simp add: qs_def less_list_def) have "strict_sorted (interact (u1#us) (v1#vs))" using L \strict_sorted x\ \strict_sorted y\ merge merge_interact merge_preserves seqs_ne us vs xu_eq yv_eq by auto then have "strict_sorted (interact us vs)" "v1 < interact us vs" by (auto simp: strict_sorted_append_iff) moreover have "ps < u1 @ qs @ v1 @ interact us vs" using \ps < u1\ us_ne unfolding less_list_def by auto moreover have "u1 < qs @ v1 @ interact us vs" by (metis \u1 < qs\ \vvs \ []\ acc_lengths_eq_Nil_iff hd_append less_list_def qs_def vs) moreover have "qs < v1 @ interact us vs" using \qs < v1\ us_ne \last u1 < length v1\ vs_ne by (auto simp: less_list_def) ultimately show ?thesis by (simp add: zs_def strict_sorted_append_iff ssp ssq \strict_sorted u1\ \strict_sorted v1\) qed have ps_subset_d: "list.set ps \ d j" using K Ksub \_card \finite K\ acc_lengths_subset_d u_sub by blast have ps_less_u1: "ps < u1" proof - have "hd u1 = hd x" using us_ne by (auto simp: xu_eq) then have "hd u1 \ a j" by (simp add: xeq BB_eq_concat_seqs K seqs_def hd_append hd_list_of) then have "list.set ps \ {hd u1}" by (metis da ps_subset_d less_sets_def singletonD subset_iff) then show ?thesis by (metis less_hd_imp_less list.set(2) empty_set less_sets_imp_list_less) qed have qs_subset_d: "list.set qs \ d r" using L Lsub \_card \finite L\ acc_lengths_subset_d v_sub by blast have qs_less_v1: "qs < v1" proof - have "hd v1 = hd y" using vs_ne by (auto simp: yv_eq) then have "hd v1 \ a r" by (simp add: yeq BB_eq_concat_seqs L seqs_def hd_append hd_list_of) then have "list.set qs \ {hd v1}" by (metis da qs_subset_d less_sets_def singletonD subset_iff) then show ?thesis by (metis less_hd_imp_less list.set(2) empty_set less_sets_imp_list_less) qed have FB: "Form_Body ku kv x y zs" unfolding Form_Body.simps using ku_def kv_def ps_def qs_def ss us_ne vs_ne xu_eq xy yv_eq zs_def by blast then have "zs = (inter_scheme ((ku+kv) - Suc 0) {x,y})" by (simp add: Form_Body_imp_inter_scheme k) obtain l where "l \ 2 * (Suc j)" and l: "Form l U" and zs_eq_interact: "zs = inter_scheme l {x,y}" proof show "ku+kv-1 \ 2 * (Suc j)" using k by auto show "Form (ku+kv-1) U" proof (cases "ku=kv") case True then show ?thesis using FB Form.simps Ueq \0 < kv\ by (auto simp: mult_2) next case False then have "ku = Suc kv" using k by auto then show ?thesis using FB Form.simps Ueq \0 < kv\ by auto qed show "zs = inter_scheme (ku + kv - 1) {x, y}" using Form_Body_imp_inter_scheme by (simp add: FB k) qed then have "enum N l \ enum N (Suc (2 * Suc j))" by (simp add: assms less_imp_le_nat) also have "\ < Min (d j)" by (smt (verit, best) Min_gr_iff d_eq d_ne finite_d fst_grab_subset greaterThan_iff in_mono le_inf_iff nxt_def) finally have ls: "{enum N l} \ d j" by simp have "l > 0" by (metis l False Form_0_cases_raw Set.doubleton_eq_iff Ueq gr0I) show ?thesis unfolding Ueq proof (intro exI conjI impI) have zs_subset: "list.set zs \ list.set (acc_lengths 0 (seqs j j K)) \ list.set (acc_lengths 0 (seqs r r L)) \ list.set x \ list.set y" using u_sub v_sub by (auto simp: zs_def xu_eq yv_eq) also have "\ \ N" proof (simp, intro conjI) show "list.set (acc_lengths 0 (seqs j j K)) \ N" using d_subset_N Ksub \finite K\ \j \ card K\ acc_lengths_subset_d by blast show "list.set (acc_lengths 0 (seqs r r L)) \ N" using d_subset_N Lsub \finite L\ \r \ card L\ acc_lengths_subset_d by blast show "list.set x \ N" "list.set y \ N" by (simp_all add: xeq yeq BB_def a_subset_N UN_least b_subset_N) qed finally show "list.set (inter_scheme l {x, y}) \ N" using zs_eq_interact by blast have "[enum N l] < ps" using ps_subset_d ls by (metis empty_set less_sets_imp_list_less less_sets_weaken2 list.simps(15)) then show "[enum N l] < inter_scheme l {x, y}" by (simp add: zs_def less_list_def ps_def flip: zs_eq_interact) qed (use Ueq l in blast) qed qed qed subsection \The main partition theorem for @{term "\\\"}\ definition iso_ll where "iso_ll A B \ iso (lenlex less_than \ (A\A)) (lenlex less_than \ (B\B))" corollary ordertype_eq_ordertype_iso_ll: assumes "Field (Restr (lenlex less_than) A) = A" "Field (Restr (lenlex less_than) B) = B" shows "(ordertype A (lenlex less_than) = ordertype B (lenlex less_than)) \ (\f. iso_ll A B f)" proof - have "total_on A (lenlex less_than) \ total_on B (lenlex less_than)" by (meson UNIV_I total_lenlex total_on_def total_on_less_than) then show ?thesis by (simp add: assms wf_lenlex lenlex_transI iso_ll_def ordertype_eq_ordertype_iso_Restr) qed theorem partition_\\_aux: assumes "\ \ elts \" shows "partn_lst (lenlex less_than) WW [\\\,\] 2" (is "partn_lst ?R WW [\\\,\] 2") proof (cases "\ \ 1") case True then show ?thesis using strict_sorted_into_WW unfolding WW_def by (auto intro!: partn_lst_triv1[where i=1]) next case False obtain m where m: "\ = ord_of_nat m" using assms elts_\ by auto then have "m>1" using False by auto show ?thesis unfolding partn_lst_def proof clarsimp fix f assume f: "f \ [WW]\<^bsup>2\<^esup> \ {..: "?P0 \ ?P1" proof (rule disjCI) assume not1: "\ ?P1" have "\W'. ordertype W' ?R = \\n \ f  [W']\<^bsup>2\<^esup> \ {0} \ W' \ WW_seg (n*m)" for n::nat proof - have fnm: "f \ [WW_seg (n*m)]\<^bsup>2\<^esup> \ {..\n, ord_of_nat m] 2" using ordertype_WW_seg [of "n*m"] by (simp add: partn_lst_VWF_imp_partn_lst [OF Theorem_3_2]) show ?thesis using partn_lst_E [OF * fnm, simplified] by (metis One_nat_def WW_seg_subset_WW less_2_cases m not1 nth_Cons_0 nth_Cons_Suc numeral_2_eq_2 subset_trans) qed then obtain W':: "nat \ nat list set" where otW': "\n. ordertype (W' n) ?R = \\n" and f_W': "\n. f  [W' n]\<^bsup>2\<^esup> \ {0}" and seg_W': "\n. W' n \ WW_seg (n*m)" by metis define WW' where "WW' \ (\n. W' n)" have "WW' \ WW" using seg_W' WW_seg_subset_WW by (force simp: WW'_def) with f have f': "f \ [WW']\<^bsup>2\<^esup> \ {..\\" proof (rule antisym) have "ordertype WW' ?R \ ordertype WW ?R" by (simp add: \WW' \ WW\ lenlex_transI ordertype_mono wf_lenlex) with ordertype_WW show "ordertype WW' ?R \ \ \ \" by simp have "\ \ n \ ordertype (\ (range W')) ?R" for n::nat using oexp_Limit ordertype_\\ otW' by auto then show "\ \ \ \ ordertype WW' ?R" by (auto simp: elts_\ oexp_Limit ZFC_in_HOL.SUP_le_iff WW'_def) qed have FR_WW: "Field (Restr (lenlex less_than) WW) = WW" by (simp add: Limit_omega_oexp Limit_ordertype_imp_Field_Restr ordertype_WW) have FR_WW': "Field (Restr (lenlex less_than) WW') = WW'" by (simp add: Limit_omega_oexp Limit_ordertype_imp_Field_Restr ot') have FR_W: "Field (Restr (lenlex less_than) (WW_seg n)) = WW_seg n" if "n>0" for n by (simp add: Limit_omega_oexp ordertype_WW_seg that Limit_ordertype_imp_Field_Restr) have FR_W': "Field (Restr (lenlex less_than) (W' n)) = W' n" if "n>0" for n by (simp add: Limit_omega_oexp otW' that Limit_ordertype_imp_Field_Restr) have "\h. iso_ll (WW_seg n) (W' n) h" if "n>0" for n proof (subst ordertype_eq_ordertype_iso_ll [symmetric]) show "ordertype (WW_seg n) (lenlex less_than) = ordertype (W' n) (lenlex less_than)" by (simp add: ordertype_WW_seg otW') qed (auto simp: FR_W FR_W' that) then obtain h_seg where h_seg: "\n. n > 0 \ iso_ll (WW_seg n) (W' n) (h_seg n)" by metis define h where "h \ \l. if l=[] then [] else h_seg (length l) l" have bij_h_seg: "\n. n > 0 \ bij_betw (h_seg n) (WW_seg n) (W' n)" using h_seg by (simp add: iso_ll_def iso_iff2 FR_W FR_W') have len_h_seg: "length (h_seg (length l) l) = length l * m" if "length l > 0" "l \ WW" for l using bij_betwE [OF bij_h_seg] seg_W' that by (simp add: WW_seg_def subset_iff) have hlen: "length (h x) = length (h y) \ length x = length y" if "x \ WW" "y \ WW" for x y using that \1 < m\ h_def len_h_seg by force have h: "iso_ll WW WW' h" unfolding iso_ll_def iso_iff2 FR_WW FR_WW' proof (intro conjI strip) have W'_ne: "W' n \ {}" for n using otW' [of n] by auto then have "[] \ WW'" using seg_W' [of 0] by (auto simp: WW'_def WW_seg_def) let ?g = "\l. if l=[] then l else inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l" have h_seg_iff: "\n a b. \a \ WW_seg n; b \ WW_seg n; n>0\ \ (a, b) \ lenlex less_than \ (h_seg n a, h_seg n b) \ lenlex less_than \ h_seg n a \ W' n \ h_seg n b \ W' n" using h_seg by (auto simp: iso_ll_def iso_iff2 FR_W FR_W') show "bij_betw h WW WW'" unfolding bij_betw_iff_bijections proof (intro exI conjI ballI) fix l assume "l \ WW" then have l: "l \ WW_seg (length l)" by (simp add: WW_seg_def) have "h l \ W' (length l)" proof (cases "l=[]") case True with seg_W' [of 0] W'_ne show ?thesis by (auto simp: WW_seg_def h_def) next case False then show ?thesis using bij_betwE bij_h_seg h_def l by fastforce qed show "h l \ WW'" using WW'_def \h l \ W' (length l)\ by blast show "?g (h l) = l" proof (cases "l=[]") case False then have "length l > 0" by auto then have "h_seg (length l) l \ []" using \1 < m\ \l \ WW\ len_h_seg by fastforce moreover have "bij_betw (h_seg (length l)) (WW_seg (length l)) (W' (length l))" using \0 < length l\ bij_h_seg by presburger ultimately show ?thesis using \l \ WW\ bij_betw_inv_into_left h_def l len_h_seg by fastforce qed (auto simp: h_def) next fix l assume "l \ WW'" then have l: "l \ W' (length l div m)" using WW_seg_def \1 < m\ seg_W' by (fastforce simp: WW'_def) show "?g l \ WW" proof (cases "l=[]") case False then have "l \ W' 0" using WW_seg_def seg_W' by fastforce with l have "inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l \ WW_seg (length l div m)" by (metis Nat.neq0_conv bij_betwE bij_betw_inv_into bij_h_seg) then show ?thesis using False WW_seg_subset_WW by auto qed (auto simp: WW_def) show "h (?g l) = l" proof (cases "l=[]") case False then have "0 < length l div m" using WW_seg_def l seg_W' by fastforce then have "inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l \ WW_seg (length l div m)" by (metis bij_betw_imp_surj_on bij_h_seg inv_into_into l) then show ?thesis using bij_h_seg [of "length l div m"] WW_seg_def \0 < length l div m\ bij_betw_inv_into_right l by (fastforce simp: h_def) qed (auto simp: h_def) qed fix a b assume "a \ WW" "b \ WW" show "(a, b) \ Restr (lenlex less_than) WW \ (h a, h b) \ Restr (lenlex less_than) WW'" (is "?lhs = ?rhs") proof assume L: ?lhs then consider "length a < length b" | "length a = length b" "(a, b) \ lex less_than" by (auto simp: lenlex_conv) then show ?rhs proof cases case 1 then have "length (h a) < length (h b)" using \1 < m\ \a \ WW\ \b \ WW\ h_def len_h_seg by auto then have "(h a, h b) \ lenlex less_than" by (auto simp: lenlex_conv) then show ?thesis using \a \ WW\ \b \ WW\ \bij_betw h WW WW'\ bij_betwE by fastforce next case 2 then have ab: "a \ WW_seg (length a)" "b \ WW_seg (length a)" using \a \ WW\ \b \ WW\ by (auto simp: WW_seg_def) have "length (h a) = length (h b)" using 2 \a \ WW\ \b \ WW\ h_def len_h_seg by force moreover have "(a, b) \ lenlex less_than" using L by blast then have "(h_seg (length a) a, h_seg (length a) b) \ lenlex less_than" using 2 ab h_seg_iff by blast ultimately show ?thesis using 2 \a \ WW\ \b \ WW\ \bij_betw h WW WW'\ bij_betwE h_def by fastforce qed next assume R: ?rhs then have R': "(h a, h b) \ lenlex less_than" by blast then consider "length a < length b" | "length a = length b" "(h a, h b) \ lex less_than" using \a \ WW\ \b \ WW\ \m > 1\ by (auto simp: lenlex_conv h_def len_h_seg split: if_split_asm) then show ?lhs proof cases case 1 then show ?thesis using omega_sum_less_iff \a \ WW\ \b \ WW\ by auto next case 2 then have ab: "a \ WW_seg (length a)" "b \ WW_seg (length a)" using \a \ WW\ \b \ WW\ by (auto simp: WW_seg_def) then have "(a, b) \ lenlex less_than" using bij_betwE [OF bij_h_seg] \a \ WW\ \b \ WW\ R' 2 by (simp add: h_def h_seg_iff split: if_split_asm) then show ?thesis using \a \ WW\ \b \ WW\ by blast qed qed qed let ?fh = "f \ image h" have "bij_betw h WW WW'" using h unfolding iso_ll_def iso_iff2 by (fastforce simp: FR_WW FR_WW') moreover have "{.. [WW]\<^bsup>2\<^esup> \ {0,1}" unfolding Pi_iff using bij_betwE f' bij_betw_nsets by (metis PiE comp_apply) have "f{x,y} = 0" if "x \ WW'" "y \ WW'" "length x = length y" "x \ y" for x y proof - obtain p q where "x \ W' p" and "y \ W' q" using WW'_def \x \ WW'\ \y \ WW'\ by blast then obtain n where "{x,y} \ [W' n]\<^bsup>2\<^esup>" using seg_W' \1 < m\ \length x = length y\ \x \ y\ by (auto simp: WW'_def WW_seg_def subset_iff) then show "f{x,y} = 0" using f_W' by blast qed then have fh_eq_0_eqlen: "?fh{x,y} = 0" if "x \ WW" "y \ WW" "length x = length y" "x\y" for x y using \bij_betw h WW WW'\ that hlen by (simp add: bij_betw_iff_bijections) metis have m_f_0: "\x$M]\<^bsup>2\<^esup>. f x = 0" if "M \ WW" "card M = m" for M proof - have "finite M" using False m that by auto with not1 [simplified, rule_format, of M] f show ?thesis using that \1 < m\ apply (simp add: Pi_iff image_subset_iff finite_ordertype_eq_card m) by (metis less_2_cases nsets_mono numeral_2_eq_2 subset_iff) qed have m_fh_0: "\x\[M]\<^bsup>2\<^esup>. ?fh x = 0" if "M \ WW" "card M = m" for M proof - have "h  M \ WW" using \WW' \ WW\ \bij_betw h WW WW'\ bij_betwE that(1) by fastforce moreover have "card (h  M) = m" by (metis \bij_betw h WW WW'\ bij_betw_def bij_betw_subset card_image that) ultimately have "\x \ [h  M]\<^bsup>2\<^esup>. f x = 0" by (metis m_f_0) then obtain Y where Y: "f (h  Y) = 0" "Y \ M" and "finite (h  Y)" "card (h  Y) = 2" by (auto simp: nsets_def subset_image_iff) then have "card Y = 2" using \bij_betw h WW WW'\ \M \ WW\ by (metis bij_betw_def card_image inj_on_subset) with Y card.infinite[of Y] show ?thesis by (auto simp: nsets_def) qed obtain N j where "infinite N" and N: "\k u. \k > 0; u \ [WW]\<^bsup>2\<^esup>; Form k u; [enum N k] < inter_scheme k u; List.set (inter_scheme k u) \ N\ \ ?fh u = j k" using lemma_3_6 [OF fh] by blast have infN': "infinite (enum N  {k<..})" for k by (simp add: \infinite N\ enum_works finite_image_iff infinite_Ioi strict_mono_imp_inj_on) have j_0: "j k = 0" if "k>0" for k proof - obtain M where M: "M \ [WW]\<^bsup>m\<^esup>" and MF: "\u. u \ [M]\<^bsup>2\<^esup> \ Form k u" and Mi: "\u. u \ [M]\<^bsup>2\<^esup> \ List.set (inter_scheme k u) \ enum N  {k<..}" using lemma_3_7 [OF infN' \k > 0$ by metis obtain u where u: "u \ [M]\<^bsup>2\<^esup>" "?fh u = 0" using m_fh_0 [of M] M [unfolded nsets_def] by force moreover have \
: "Form k u" "List.set (inter_scheme k u) \ enum N  {k<..}" by (simp_all add: MF Mi \u \ [M]\<^bsup>2\<^esup>\) then have "hd (inter_scheme k u) \ enum N  {k<..}" using hd_in_set inter_scheme_simple that by blast then have "[enum N k] < inter_scheme k u" using strict_mono_enum [OF \infinite N\] by (auto simp: less_list_def strict_mono_def) moreover have "u \ [WW]\<^bsup>2\<^esup>" using M u by (auto simp: nsets_def) moreover have "enum N  {k<..} \ N" using \infinite N\ range_enum by auto ultimately show ?thesis using N \
that by auto qed obtain X where "X \ WW" and otX: "ordertype X (lenlex less_than) = \\\" and X: "\u. u \ [X]\<^bsup>2\<^esup> \ \l. Form l u \ (l > 0 \ [enum N l] < inter_scheme l u \ List.set (inter_scheme l u) \ N)" using lemma_3_8 [OF \infinite N\] ot' by blast have 0: "?fh  [X]\<^bsup>2\<^esup> \ {0}" proof clarsimp fix u assume u: "u \ [X]\<^bsup>2\<^esup>" obtain l where "Form l u" and l: "l > 0 \ [enum N l] < inter_scheme l u \ List.set (inter_scheme l u) \ N" using u X by blast have "?fh u = 0" proof (cases "l = 0") case True then show ?thesis by (metis Form_0_cases_raw \Form l u\ \X \ WW\ doubleton_in_nsets_2 fh_eq_0_eqlen subset_iff u) next case False then obtain "[enum N l] < inter_scheme l u" "List.set (inter_scheme l u) \ N" "j l = 0" using Nat.neq0_conv j_0 l by blast with False show ?thesis using \X \ WW\ N inter_scheme \Form l u\ doubleton_in_nsets_2 u by (auto simp: nsets_def) qed then show "f (h  u) = 0" by auto qed show ?P0 proof (intro exI conjI) show "h  X \ WW" using \WW' \ WW\ \X \ WW\ \bij_betw h WW WW'\ bij_betw_imp_surj_on by fastforce show "ordertype (h  X) (lenlex less_than) = \ \ \" proof (subst ordertype_inc_eq) show "(h x, h y) \ lenlex less_than" if "x \ X" "y \ X" "(x, y) \ lenlex less_than" for x y using that h \X \ WW\ by (auto simp: FR_WW FR_WW' iso_iff2 iso_ll_def) qed (use otX in auto) show "f  [h  X]\<^bsup>2\<^esup> \ {0}" proof (clarsimp simp: image_subset_iff nsets_def) fix Y assume "Y \ h  X" and "finite Y" and "card Y = 2" have "inv_into WW h  Y \ X" using \X \ WW\ \Y \ h  X\ \bij_betw h WW WW'\ bij_betw_inv_into_LEFT by blast moreover have "finite (inv_into WW h  Y)" using \finite Y\ by blast moreover have "card (inv_into WW h  Y) = 2" by (metis \X \ WW\ \Y \ h  X\ \card Y = 2\ card_image inj_on_inv_into subset_image_iff subset_trans) ultimately have "f (h  inv_into WW h  Y) = 0" using 0 by (auto simp: image_subset_iff nsets_def) then show "f Y = 0" by (metis \X \ WW\ \Y \ h  X\ image_inv_into_cancel image_mono order_trans) qed qed qed then show "\iH\WW. ordertype H ?R = [\\\, \] ! i \ f  [H]\<^bsup>2\<^esup> \ {i}" by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc) qed qed text \Theorem 3.1 of Jean A. Larson, ibid.\ theorem partition_\\: "\ \ elts \ \ partn_lst_VWF (\\\) [\\\,\] 2" using partn_lst_imp_partn_lst_VWF_eq [OF partition_\\_aux] ordertype_WW by auto end diff --git a/thys/ZFC_in_HOL/Cantor_NF.thy b/thys/ZFC_in_HOL/Cantor_NF.thy --- a/thys/ZFC_in_HOL/Cantor_NF.thy +++ b/thys/ZFC_in_HOL/Cantor_NF.thy @@ -1,1429 +1,1429 @@ section \Cantor Normal Form\ theory Cantor_NF imports Ordinal_Exp begin subsection \Cantor normal form\ text \Lemma 5.1\ lemma cnf_1: assumes \: "\ \ elts \" "Ord \" and "m > 0" shows "\\\ * ord_of_nat n < \\\ * ord_of_nat m" proof - have \: "\\succ \ \ \\\" using Ord_mem_iff_less_TC assms oexp_mono succ_le_TC_iff by auto have "\\\ * ord_of_nat n < \\\ * \" using Ord_in_Ord OrdmemD assms by auto also have "\ = \\succ \" using Ord_in_Ord \ by auto also have "\ \ \\\" using "\" by blast also have "\ \ \\\ * ord_of_nat m" using \m > 0\ le_mult by auto finally show ?thesis . qed fun Cantor_sum where Cantor_sum_Nil: "Cantor_sum [] ms = 0" | Cantor_sum_Nil2: "Cantor_sum (\#\s) [] = 0" | Cantor_sum_Cons: "Cantor_sum (\#\s) (m#ms) = (\\\) * ord_of_nat m + Cantor_sum \s ms" abbreviation Cantor_dec :: "V list \ bool" where "Cantor_dec \ sorted_wrt (>)" lemma Ord_Cantor_sum: assumes "List.set \s \ ON" shows "Ord (Cantor_sum \s ms)" using assms proof (induction \s arbitrary: ms) case (Cons a \s ms) then show ?case by (cases ms) auto qed auto lemma Cantor_dec_Cons_iff [simp]: "Cantor_dec (\#\#\s) \ \ < \ \ Cantor_dec (\#\s)" by auto text \Lemma 5.2. The second and third premises aren't really necessary, but their removal requires quite a lot of work.\ lemma cnf_2: assumes "List.set (\#\s) \ ON" "list.set ms \ {0<..}" "length \s = length ms" and "Cantor_dec (\#\s)" shows "\\\ > Cantor_sum \s ms" using assms proof (induction ms arbitrary: \ \s) case Nil then obtain \0 where \0: "(\#\s) = [\0]" by (metis length_0_conv) then have "Ord \0" using Nil.prems(1) by auto then show ?case using \0 zero_less_Limit by auto next case (Cons m1 ms) then obtain \0 \1 \s' where \01: "(\#\s) = \0#\1#\s'" by (metis (no_types, lifting) Cons.prems(3) Suc_length_conv) then have "Ord \0" "Ord \1" using Cons.prems(1) \01 by auto have *: "\\\0 * ord_of_nat 1 > \\\1 * ord_of_nat m1" proof (rule cnf_1) show "\1 \ elts \0" using Cons.prems \01 by (simp add: Ord_mem_iff_lt \Ord \0\ \Ord \1\) qed (use \Ord \0\ in auto) show ?case proof (cases ms) case Nil then show ?thesis using * one_V_def Cons.prems(3) \01 by auto next case (Cons m2 ms') then obtain \2 \s'' where \02: "(\#\s) = \0#\1#\2#\s''" by (metis Cons.prems(3) Suc_length_conv \01 length_tl list.sel(3)) then have "Ord \2" using Cons.prems(1) by auto have "m1 > 0" "m2 > 0" using Cons.prems Cons by auto have "\\\1 * ord_of_nat m1 + \\\1 * ord_of_nat m1 = (\\\1 * ord_of_nat m1) * ord_of_nat 2" by (simp add: mult_succ eval_nat_numeral) also have "\ < \\\0" using cnf_1 [of concl: "\1" "m1 * 2" "\0" 1] Cons.prems \01 one_V_def by (simp add: mult.assoc ord_of_nat_mult Ord_mem_iff_lt) finally have II: "\\\1 * ord_of_nat m1 + \\\1 * ord_of_nat m1 < \\\0" by simp have "Cantor_sum (tl \s) ms < \\hd \s" proof (rule Cons.IH) show "Cantor_dec (hd \s # tl \s)" using \Cantor_dec (\#\s)\ \01 by auto qed (use Cons.prems \01 in auto) then have "Cantor_sum (\2 # \s'') ms < \\\1" using \02 by auto also have "\ \ \\\1 * ord_of_nat m1" by (simp add: \0 < m1\ le_mult) finally show ?thesis using II \02 dual_order.strict_trans by fastforce qed qed proposition Cantor_nf_exists: assumes "Ord \" obtains \s ms where "List.set \s \ ON" "list.set ms \ {0<..}" "length \s = length ms" and "Cantor_dec \s" and "\ = Cantor_sum \s ms" using assms proof (induction \ arbitrary: thesis rule: Ord_induct) case (step \) show ?case proof (cases "\ = 0") case True have "Cantor_sum [] [] = 0" by simp with True show ?thesis using length_pos_if_in_set step.prems subset_eq by (metis length_0_conv not_gr_zero sorted_wrt.simps(1)) next case False define \hat where "\hat \ Sup {\ \ ON. \\\ \ \}" then have "Ord \hat" using Ord_Sup assms by fastforce have "\\. \Ord \; \\\ \ \\ \ \ \ \\\" by (metis Ord_\ OrdmemD le_oexp' order_trans step.hyps one_V_def succ_in_omega zero_in_omega) then have "{\ \ ON. \\\ \ \} \ elts (succ (\\\))" using Ord_mem_iff_lt step.hyps by force then have sma: "small {\ \ ON. \\\ \ \}" by (meson down) have le: "\\\hat \ \" proof (rule ccontr) assume "\ \\\hat \ \" then have \: "\ \ elts (\\\hat)" by (meson Ord_\ Ord_linear2 Ord_mem_iff_lt Ord_oexp \Ord \hat\ step.hyps) obtain \ where "Ord \" "\\\ \ \" "\ < \" using \Ord \hat\ proof (cases \hat rule: Ord_cases) case 0 with \ show thesis by (auto simp: False) next case (succ \) have "succ \ \ {\ \ ON. \\\ \ \}" by (rule succ_in_Sup_Ord) (use succ \hat_def sma in auto) then have "\\succ \ \ \" by blast with \ show thesis using \\ \\\hat \ \\ succ by blast next case limit with \ show thesis apply (clarsimp simp: oexp_Limit \hat_def) by (meson Ord_\ Ord_in_Ord Ord_linear_le mem_not_refl oexp_mono_le omega_nonzero vsubsetD) qed then show False by (metis Ord_\ OrdmemD leD le_less_trans le_oexp' one_V_def succ_in_omega zero_in_omega) qed have False if "\M. \ < \\\hat * ord_of_nat M" proof - have \: "\\\hat * ord_of_nat M \ \" for M by (meson that Ord_\ Ord_linear2 Ord_mult Ord_oexp Ord_ord_of_nat \Ord \hat\ step.hyps) have "\ \\succ \hat \ \" using Ord_mem_iff_lt \hat_def \Ord \hat\ sma elts_succ by blast then have "\ < \\succ \hat" by (meson Ord_\ Ord_linear2 Ord_oexp Ord_succ \Ord \hat\ step.hyps) also have "\ = \\\hat * \" using \Ord \hat\ oexp_succ by blast also have "\ = Sup (range (\m. \\\hat * ord_of_nat m))" by (simp add: mult_Limit) (auto simp: \_def image_image) also have "\ \ \" using \ by blast finally show False by simp qed then obtain M where M: "\\\hat * ord_of_nat M > \" by blast have bound: "i \ M" if "\\\hat * ord_of_nat i \ \" for i proof - have "\\\hat * ord_of_nat i < \\\hat * ord_of_nat M" using M dual_order.strict_trans2 that by blast then show ?thesis using \Ord \hat\ less_V_def by auto qed define mhat where "mhat \ Greatest (\m. \\\hat * ord_of_nat m \ \)" have mhat_ge: "m \ mhat" if "\\\hat * ord_of_nat m \ \" for m unfolding mhat_def by (metis (mono_tags, lifting) Greatest_le_nat bound that) have mhat: "\\\hat * ord_of_nat mhat \ \" unfolding mhat_def by (rule GreatestI_nat [where k=0 and b=M]) (use bound in auto) then obtain \ where "Ord \" "\ \ \" and \: "\ = \\\hat * ord_of_nat mhat + \" by (metis Ord_\ Ord_mult Ord_oexp Ord_ord_of_nat \Ord \hat\ step.hyps le_Ord_diff) have False if "\ = \" proof - have "\ \ \\\hat" by (simp add: le that) then obtain \ where "Ord \" "\ \ \" and \: "\ = \\\hat + \" by (metis Ord_\ Ord_oexp \Ord \hat\ \Ord \\ le_Ord_diff) then have "\ = \\\hat * ord_of_nat mhat + \\\hat + \" by (simp add: \ add.assoc) then have "\\\hat * ord_of_nat (Suc mhat) \ \" by (metis add_le_cancel_left add.right_neutral le_0 mult_succ ord_of_nat.simps(2)) then show False using Suc_n_not_le_n mhat_ge by blast qed then have \in\: "\ \ elts \" using Ord_mem_iff_lt \Ord \\ \\ \ \\ less_V_def step.hyps by auto show thesis proof (cases "\ = 0") case True show thesis proof (rule step.prems) show "\ = Cantor_sum [\hat] [mhat]" by (simp add: True \) qed (use \ True \\ \ 0\ \Ord \hat\ in auto) next case False obtain \s ns where sub: "List.set \s \ ON" "list.set ns \ {0<..}" and len_eq: "length \s = length ns" and dec: "Cantor_dec \s" and \eq: "\ = Cantor_sum \s ns" using step.IH [OF \in\] by blast then have "length \s > 0" "length ns > 0" using False Cantor_sum.simps(1) \\ = Cantor_sum \s ns\ by auto then obtain \0 n0 \s' ns' where \0: "\s = \0 # \s'" and "Ord \0" and n0: "ns = n0 # ns'" and "n0 > 0" using sub by (auto simp: neq_Nil_conv) moreover have False if "\0 > \hat" proof - have "\\\0 \ \\\0 * ord_of_nat n0 + u" for u using \n0 > 0\ by (metis add_le_cancel_left Ord_ord_of_nat add.right_neutral dual_order.trans gr_implies_not_zero le_0 le_mult ord_of_eq_0_iff) moreover have "\\\0 > \" using that \Ord \0\ by (metis (no_types, lifting) Ord_\ Ord_linear2 Ord_oexp Sup_upper \hat_def leD mem_Collect_eq sma step.hyps) ultimately have "\ \ \\\0" by (simp add: \eq \0 n0) then show ?thesis using \\ < \\\0\ \\ \ \\ by auto qed ultimately have "\0 \ \hat" using Ord_linear2 \Ord \hat\ by auto then consider "\0 < \hat" | "\0 = \hat" using dual_order.order_iff_strict by auto then show ?thesis proof cases case 1 show ?thesis proof (rule step.prems) show "list.set (\hat#\s) \ ON" using sub by (auto simp: \Ord \hat\) show "list.set (mhat#ns) \ {0::nat<..}" using sub using \\ = \ \ False\ \ by fastforce show "Cantor_dec (\hat#\s)" using that \\0 < \hat\ \Ord \hat\ \Ord \0\ Ord_mem_iff_lt \0 dec less_Suc_eq_0_disj by (force simp: \0 n0) show "length (\hat#\s) = length (mhat#ns)" by (auto simp: len_eq) show "\ = Cantor_sum (\hat#\s) (mhat#ns)" by (simp add: \ \eq \0 n0) qed next case 2 show ?thesis proof (rule step.prems) show "list.set \s \ ON" by (simp add: sub(1)) show "list.set ((n0+mhat)#ns') \ {0::nat<..}" using n0 sub(2) by auto show "length (\s::V list) = length ((n0+mhat)#ns')" by (simp add: len_eq n0) show "Cantor_dec \s" using that \0 dec by auto show "\ = Cantor_sum \s ((n0+mhat)#ns')" using 2 by (simp add: add_mult_distrib \0 \ \eq add.assoc add.commute n0 ord_of_nat_add) qed qed qed qed qed lemma Cantor_sum_0E: assumes "Cantor_sum \s ms = 0" "List.set \s \ ON" "list.set ms \ {0<..}" "length \s = length ms" shows "\s = []" using assms proof (induction \s arbitrary: ms) case Nil then show ?case by auto next case (Cons a list) then obtain m ms' where "ms = m#ms'" "m \ 0" "list.set ms' \ {0<..}" by simp (metis Suc_length_conv greaterThan_iff insert_subset list.set(2)) with Cons show ?case by auto qed lemma Cantor_nf_unique_aux: assumes "Ord \" and \sON: "List.set \s \ ON" and \sON: "List.set \s \ ON" and ms: "list.set ms \ {0<..}" and ns: "list.set ns \ {0<..}" and mseq: "length \s = length ms" and nseq: "length \s = length ns" and \sdec: "Cantor_dec \s" and \sdec: "Cantor_dec \s" and \seq: "\ = Cantor_sum \s ms" and \seq: "\ = Cantor_sum \s ns" shows "\s = \s \ ms = ns" using assms proof (induction \ arbitrary: \s ms \s ns rule: Ord_induct) case (step \) show ?case proof (cases "\ = 0") case True then show ?thesis using step.prems by (metis Cantor_sum_0E length_0_conv) next case False then obtain \0 \s' \0 \s' where \s: "\s = \0 # \s'" and \s: "\s = \0 # \s'" by (metis Cantor_sum.simps(1) min_list.cases step.prems(9,10)) then have ON: "Ord \0" "list.set \s' \ ON" "Ord \0" "list.set \s' \ ON" using \s \s step.prems(1,2) by auto then obtain m0 ms' n0 ns' where ms: "ms = m0 # ms'" and ns: "ns = n0 # ns'" by (metis \s \s length_0_conv list.distinct(1) list.exhaust step.prems(5,6)) then have nz: "m0 \ 0" "list.set ms' \ {0<..}" "n0 \ 0" "list.set ns' \ {0<..}" using ms ns step.prems(3,4) by auto have False if "\0 < \0" proof - have Ordc: "Ord (Cantor_sum \s ns)" "Ord (\\\0)" using Ord_oexp \Ord \0\ step.hyps step.prems(10) by blast+ have *: "Cantor_sum \s ns < \\\0" using step.prems(2-6) \Ord \0\ \Cantor_dec \s\ that \s cnf_2 by (metis Cantor_dec_Cons_iff insert_subset list.set(2) mem_Collect_eq) then show False by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc \s \m0 \ 0\ * le_mult ms not_add_mem_right ord_of_eq_0 step.prems(9,10) vsubsetD) qed moreover have False if "\0 < \0" proof - have Ordc: "Ord (Cantor_sum \s ms)" "Ord (\\\0)" using Ord_oexp \Ord \0\ step.hyps step.prems(9) by blast+ have *: "Cantor_sum \s ms < \\\0" using step.prems(1-5) \Ord \0\ \Cantor_dec \s\ that \s cnf_2 by (metis Cantor_dec_Cons_iff \s insert_subset list.set(2)) then show False by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc \s \n0 \ 0\ * le_mult not_add_mem_right ns ord_of_eq_0 step.prems(9,10) vsubsetD) qed ultimately have 1: "\0 = \0" using Ord_linear_lt \Ord \0\ \Ord \0\ by blast have False if "m0 < n0" proof - have "\\\0 > Cantor_sum \s' ms'" using \s \list.set ms' \ {0<..}\ cnf_2 ms step.prems(1,5,7) by auto then have "\ < \\\0 * ord_of_nat m0 + \\\0" by (simp add: \s ms step.prems(9)) also have "\ = \\\0 * ord_of_nat (Suc m0)" by (simp add: mult_succ) also have "\ \ \\\0 * ord_of_nat n0" by (meson Ord_\ Ord_oexp Ord_ord_of_nat Suc_leI \Ord \0\ mult_cancel_le_iff ord_of_nat_mono_iff that) also have "\ \ \" by (metis Cantor_sum_Cons add_le_cancel_left \s \\0 = \0\ add.right_neutral le_0 ns step.prems(10)) finally show False by blast qed moreover have False if "n0 < m0" proof - have "\\\0 > Cantor_sum \s' ns'" using \s \list.set ns' \ {0<..}\ cnf_2 ns step.prems(2,6,8) by auto then have "\ < \\\0 * ord_of_nat n0 + \\\0" by (simp add: \s ns step.prems(10)) also have "\ = \\\0 * ord_of_nat (Suc n0)" by (simp add: mult_succ) also have "\ \ \\\0 * ord_of_nat m0" by (meson Ord_\ Ord_oexp Ord_ord_of_nat Suc_leI \Ord \0\ mult_cancel_le_iff ord_of_nat_mono_iff that) also have "\ \ \" by (metis Cantor_sum_Cons add_le_cancel_left \s \\0 = \0\ add.right_neutral le_0 ms step.prems(9)) finally show False by blast qed ultimately have 2: "m0 = n0" using nat_neq_iff by blast have "\s' = \s' \ ms' = ns'" proof (rule step.IH) have "Cantor_sum \s' ms' < \\\0" using \s cnf_2 ms nz(2) step.prems(1) step.prems(5) step.prems(7) by auto also have "\ \ Cantor_sum \s ms" apply (simp add: \s \s ms ns) by (metis Cantor_sum_Cons add_less_cancel_left ON(1) Ord_\ Ord_linear2 Ord_oexp Ord_ord_of_nat \s add.right_neutral dual_order.strict_trans1 le_mult ms not_less_0 nz(1) ord_of_eq_0 step.hyps step.prems(9)) finally show "Cantor_sum \s' ms' \ elts \" using ON(2) Ord_Cantor_sum Ord_mem_iff_lt step.hyps step.prems(9) by blast show "length \s' = length ms'" "length \s' = length ns'" using \s ms \s ns step.prems by auto show "Cantor_dec \s'" "Cantor_dec \s'" using \s \s step.prems(7,8) by auto have "Cantor_sum \s ms = Cantor_sum \s ns" using step.prems(9,10) by auto then show "Cantor_sum \s' ms' = Cantor_sum \s' ns'" using 1 2 by (simp add: \s \s ms ns) qed (use ON nz in auto) then show ?thesis using 1 2 by (simp add: \s \s ms ns) qed qed proposition Cantor_nf_unique: assumes "Cantor_sum \s ms = Cantor_sum \s ns" and \sON: "List.set \s \ ON" and \sON: "List.set \s \ ON" and ms: "list.set ms \ {0<..}" and ns: "list.set ns \ {0<..}" and mseq: "length \s = length ms" and nseq: "length \s = length ns" and \sdec: "Cantor_dec \s" and \sdec: "Cantor_dec \s" shows "\s = \s \ ms = ns" using Cantor_nf_unique_aux Ord_Cantor_sum assms by auto lemma less_\_power: assumes "Ord \1" "Ord \" and \2: "\2 \ elts \1" and \: "\ < \\\2" and "m1 > 0" "m2 > 0" shows "\\\2 * ord_of_nat m2 + \ < \\\1 * ord_of_nat m1 + (\\\2 * ord_of_nat m2 + \)" (is "?lhs < ?rhs") proof - obtain oo: "Ord (\\\1)" "Ord (\\\2)" using Ord_in_Ord Ord_oexp assms by blast moreover obtain "ord_of_nat m2 \ 0" using assms ord_of_eq_0 by blast ultimately have "\ < \\\2 * ord_of_nat m2" by (meson Ord_ord_of_nat \ dual_order.strict_trans1 le_mult) with oo assms have "?lhs \ ?rhs" by (metis Ord_mult Ord_ord_of_nat add_strict_mono add.assoc cnf_1 not_add_less_right oo) then show ?thesis by (simp add: add_le_left \Ord \\ less_V_def oo) qed lemma Cantor_sum_ge: assumes "List.set (\#\s) \ ON" "list.set ms \ {0<..}" "length ms > 0" shows "\ \ \ \ Cantor_sum (\#\s) ms" proof - obtain m ns where ms: "ms = Cons m ns" - using assms(3) strict_sorted.cases by auto + by (meson assms(3) list.set_cases nth_mem) then have "\ \ \ \ \ \ \ * ord_of_nat m" using assms(2) le_mult by auto then show ?thesis using dual_order.trans ms by auto qed subsection \Simplified Cantor normal form\ text \No coefficients, and the exponents decreasing non-strictly\ fun \_sum where \_sum_Nil: "\_sum [] = 0" | \_sum_Cons: "\_sum (\#\s) = (\\\) + \_sum \s" abbreviation \_dec :: "V list \ bool" where "\_dec \ sorted_wrt (\)" lemma Ord_\_sum [simp]: "List.set \s \ ON \ Ord (\_sum \s)" by (induction \s) auto lemma \_dec_Cons_iff [simp]: "\_dec (\#\#\s) \ \ \ \ \ \_dec (\#\s)" by auto lemma \_sum_0E: assumes "\_sum \s = 0" "List.set \s \ ON" shows "\s = []" using assms by (induction \s) auto fun \_of_Cantor where \_of_Cantor_Nil: "\_of_Cantor [] ms = []" | \_of_Cantor_Nil2: "\_of_Cantor (\#\s) [] = []" | \_of_Cantor_Cons: "\_of_Cantor (\#\s) (m#ms) = replicate m \ @ \_of_Cantor \s ms" lemma \_sum_append [simp]: "\_sum (xs @ ys) = \_sum xs + \_sum ys" by (induction xs) (auto simp: add.assoc) lemma \_sum_replicate [simp]: "\_sum (replicate m a) = \ \ a * ord_of_nat m" by (induction m) (auto simp: mult_succ simp flip: replicate_append_same) lemma \_sum_of_Cantor [simp]: "\_sum (\_of_Cantor \s ms) = Cantor_sum \s ms" proof (induction \s arbitrary: ms) case (Cons a \s ms) then show ?case by (cases ms) auto qed auto lemma \_of_Cantor_subset: "List.set (\_of_Cantor \s ms) \ List.set \s" proof (induction \s arbitrary: ms) case (Cons a \s ms) then show ?case by (cases ms) auto qed auto lemma \_dec_replicate: "\_dec (replicate m \ @ \s) = (if m=0 then \_dec \s else \_dec (\#\s))" by (induction m arbitrary: \s) (simp_all flip: replicate_append_same) lemma \_dec_of_Cantor_aux: assumes "Cantor_dec (\#\s)" "length \s = length ms" shows "\_dec (\_of_Cantor (\#\s) (m#ms))" using assms proof (induction \s arbitrary: ms) case Nil then show ?case using sorted_wrt_iff_nth_less by fastforce next case (Cons a \s ms) then obtain n ns where ns: "ms = n#ns" by (metis length_Suc_conv) then have "a \ \" using Cons.prems(1) order.strict_implies_order by auto moreover have "\x\list.set (\_of_Cantor \s ns). x \ a" using Cons ns \a \ \\ apply (simp add: \_dec_replicate) by (meson \_of_Cantor_subset order.strict_implies_order subsetD) ultimately show ?case using Cons ns by (force simp: \_dec_replicate) qed lemma \_dec_of_Cantor: assumes "Cantor_dec \s" "length \s = length ms" shows "\_dec (\_of_Cantor \s ms)" proof (cases \s) case Nil then have "ms = []" using assms by auto with Nil show ?thesis by simp next case (Cons a list) then show ?thesis by (metis \_dec_of_Cantor_aux assms length_Suc_conv) qed proposition \_nf_exists: assumes "Ord \" obtains \s where "List.set \s \ ON" and "\_dec \s" and "\ = \_sum \s" proof - obtain \s ms where "List.set \s \ ON" "list.set ms \ {0<..}" and length: "length \s = length ms" and "Cantor_dec \s" and \: "\ = Cantor_sum \s ms" using Cantor_nf_exists assms by blast then show thesis by (metis \_dec_of_Cantor \_of_Cantor_subset \_sum_of_Cantor order_trans that) qed lemma \_sum_take_drop: "\_sum \s = \_sum (take k \s) + \_sum (drop k \s)" proof (induction k arbitrary: \s) case 0 then show ?case by simp next case (Suc k) then show ?case proof (cases "\s") case Nil then show ?thesis by simp next case (Cons a list) with Suc.prems show ?thesis by (simp add: add.assoc flip: Suc.IH) qed qed lemma in_elts_\_sum: assumes "\ \ elts (\_sum \s)" shows "\ks. \\\elts (\ \ (\s!k)). \ = \_sum (take k \s) + \" using assms proof (induction \s arbitrary: \) case (Cons \ \s) then have "\ \ elts (\ \ \ + \_sum \s)" by simp then show ?case proof (rule mem_plus_V_E) fix \ assume \: "\ \ elts (\_sum \s)" and \: "\ = \ \ \ + \" then obtain k \ where "ks" "\ \ elts (\ \ (\s!k))" "\ = \_sum (take k \s) + \" using Cons.IH by blast then show ?case by (rule_tac x="Suc k" in exI) (simp add: \ add.assoc) qed auto qed auto lemma \_le_\_sum: "\k < length \s; List.set \s \ ON\ \ \ \ (\s!k) \ \_sum \s" proof (induction \s arbitrary: k) case (Cons a \s) then obtain "Ord a" "list.set \s \ ON" by simp with Cons.IH have "\k x. k < length \s \ \ \ \s ! k \ \ \ a + \_sum \s" by (meson Ord_\ Ord_\_sum Ord_oexp add_le_left order_trans) then show ?case using Cons by (simp add: nth_Cons split: nat.split) qed auto lemma \_sum_less_self: assumes "List.set (\#\s) \ ON" and "\_dec (\#\s)" shows "\_sum \s < \\\ + \_sum \s" using assms proof (induction \s arbitrary: \) case Nil then show ?case using ZFC_in_HOL.neq0_conv by fastforce next case (Cons \1 \s) then show ?case by (simp add: add_right_strict_mono oexp_mono_le) qed text \Something like Lemma 5.2 for @{term \_sum}\ lemma \_sum_less_\_power: assumes "\_dec (\#\s)" "List.set (\#\s) \ ON" shows "\_sum \s < \\\ * \" using assms proof (induction \s) case Nil then show ?case by (simp add: \_gt0) next case (Cons \ \s) then have "Ord \" by auto have "\_sum \s < \\\ * \" using Cons by force then have "\\\ + \_sum \s < \\\ + \\\ * \" using Cons.prems add_right_strict_mono oexp_mono_le by auto also have "\ = \\\ * \" by (metis Kirby.add_mult_distrib mult.right_neutral one_plus_\_equals_\) finally show ?case by simp qed lemma \_sum_nf_unique_aux: assumes "Ord \" and \sON: "List.set \s \ ON" and \sON: "List.set \s \ ON" and \sdec: "\_dec \s" and \sdec: "\_dec \s" and \seq: "\ = \_sum \s" and \seq: "\ = \_sum \s" shows "\s = \s" using assms proof (induction \ arbitrary: \s \s rule: Ord_induct) case (step \) show ?case proof (cases "\ = 0") case True then show ?thesis using step.prems by (metis \_sum_0E) next case False then obtain \0 \s' \0 \s' where \s: "\s = \0 # \s'" and \s: "\s = \0 # \s'" by (metis \_sum.elims step.prems(5,6)) then have ON: "Ord \0" "list.set \s' \ ON" "Ord \0" "list.set \s' \ ON" using \s \s step.prems(1,2) by auto have False if "\0 < \0" proof - have Ordc: "Ord (\_sum \s)" "Ord (\\\0)" using Ord_oexp \Ord \0\ step.hyps step.prems(6) by blast+ have "\_sum \s < \\\0 * \" by (rule \_sum_less_\_power) (use \s step.prems ON in auto) also have "\ \ \\\0" using ON by (metis Ord_\ Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that) finally show False using \s leD step.prems(5,6) by auto qed moreover have False if "\0 < \0" proof - have Ordc: "Ord (\_sum \s)" "Ord (\\\0)" using Ord_oexp \Ord \0\ step.hyps step.prems(5) by blast+ have "\_sum \s < \\\0 * \" by (rule \_sum_less_\_power) (use \s step.prems ON in auto) also have "\ \ \\\0" using ON by (metis Ord_\ Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that) finally show False using \s leD step.prems(5,6) by (simp add: \\ = \_sum \s\ leD) qed ultimately have \: "\0 = \0" using Ord_linear_lt \Ord \0\ \Ord \0\ by blast moreover have "\s' = \s'" proof (rule step.IH) show "\_sum \s' \ elts \" using step.prems \s by (simp add: Ord_mem_iff_lt \_sum_less_self) show "\_dec \s'" "\_dec \s'" using \s \s step.prems(3,4) by auto have "\_sum \s = \_sum \s" using step.prems(5,6) by auto then show "\_sum \s' = \_sum \s'" by (simp add: \ \s \s) qed (use ON in auto) ultimately show ?thesis by (simp add: \s \s) qed qed subsection \Indecomposable ordinals\ text \Cf exercise 5 on page 43 of Kunen\ definition indecomposable where "indecomposable \ \ Ord \ \ (\\ \ elts \. \\ \ elts \. \+\ \ elts \)" lemma indecomposableD: "\indecomposable \; \ < \; \ < \; Ord \; Ord \\ \ \+\ < \" by (meson Ord_mem_iff_lt OrdmemD indecomposable_def) lemma indecomposable_imp_Ord: "indecomposable \ \ Ord \" using indecomposable_def by blast lemma indecomposable_1: "indecomposable 1" by (auto simp: indecomposable_def) lemma indecomposable_0: "indecomposable 0" by (auto simp: indecomposable_def) lemma indecomposable_succ [simp]: "indecomposable (succ \) \ \ = 0" using not_add_mem_right apply (auto simp: indecomposable_def) apply (metis add_right_cancel add.right_neutral) done lemma indecomposable_alt: assumes ord: "Ord \" "Ord \" and \: "\ < \" and minor: "\\ \. \\ < \; \ < \; Ord \\ \ \+\ < \" shows "\+\ = \" proof - have "\ \+\ < \" by (simp add: add_le_left ord leD) moreover have "\ \ < \+\" by (metis assms le_Ord_diff less_V_def) ultimately show ?thesis by (simp add: add_le_left less_V_def ord) qed lemma indecomposable_imp_eq: assumes "indecomposable \" "Ord \" "\ < \" shows "\+\ = \" by (metis assms indecomposableD indecomposable_def le_Ord_diff less_V_def less_irrefl) lemma indecomposable2: assumes y: "y < x" and z: "z < x" and minor: "\y::V. y < x \ y+x = x" shows "y+z < x" by (metis add_less_cancel_left y z minor) lemma indecomposable_imp_Limit: assumes indec: "indecomposable \" and "\ > 1" shows "Limit \" using indecomposable_imp_Ord [OF indec] proof (cases rule: Ord_cases) case (succ \) then show ?thesis using assms one_V_def by auto qed (use assms in auto) lemma eq_imp_indecomposable: assumes "Ord \" "\\::V. \ \ elts \ \ \+\ = \" shows "indecomposable \" by (metis add_mem_right_cancel assms indecomposable_def) lemma indecomposable_\_power: assumes "Ord \" shows "indecomposable (\\\)" unfolding indecomposable_def proof (intro conjI ballI) show "Ord (\\\)" by (simp add: \Ord \\) next fix \ \ assume asm: "\ \ elts (\\\)" "\ \ elts (\\\)" then obtain ord: "Ord \" "Ord \" and \: "\ < \\\" and \: "\ < \\\" by (meson Ord_\ Ord_in_Ord Ord_oexp OrdmemD \Ord \\) show "\ + \ \ elts (\\\)" using \Ord \\ proof (cases \ rule: Ord_cases) case 0 then show ?thesis using \Ord \\ asm by auto next case (succ l) have "\x\elts \. \ + \ \ elts (\\l * x)" if x: "x \ elts \" "\ \ elts (\\l * x)" and y: "y \ elts \" "\ \ elts (\\l * y)" for x y proof - obtain "Ord x" "Ord y" "Ord (\\l * x)" "Ord (\\l * y)" using Ord_\ Ord_mult Ord_oexp x y nat_into_Ord succ(1) by presburger then have "\ + \ \ elts (\\l * (x+y))" using add_mult_distrib Ord_add Ord_mem_iff_lt add_strict_mono ord x y by presburger then show ?thesis using x y by blast qed then show ?thesis using \Ord \\ succ ord \ \ by (auto simp: mult_Limit simp flip: Ord_mem_iff_lt) next case limit have "Ord (\\\)" by (simp add: \Ord \\) then obtain x y where x: "x \ elts \" "Ord x" "\ \ elts (\\x)" and y: "y \ elts \" "Ord y" "\ \ elts (\\y)" using \Ord \\ limit ord \ \ oexp_Limit by (auto simp flip: Ord_mem_iff_lt intro: Ord_in_Ord) then have "succ (x \ y) \ elts \" by (metis Limit_def Ord_linear_le limit sup.absorb2 sup.orderE) moreover have "\ + \ \ elts (\\succ (x \ y))" proof - have oxy: "Ord (x \ y)" using Ord_sup x y by blast then obtain "\\x \ \$$x \ y)" "\\y \ \\(x \ y)" by (metis Ord_\ Ord_linear_le Ord_mem_iff_less_TC Ord_mem_iff_lt le_TC_def less_le_not_le oexp_mono omega_nonzero sup.absorb2 sup.orderE x(2) y(2)) then have "\ \ elts (\\(x \ y))" "\ \ elts (\\(x \ y))" using x y by blast+ then have "\ + \ \ elts (\\(x \ y) * succ (succ 0))" by (metis Ord_\ Ord_add Ord_mem_iff_lt Ord_oexp Ord_sup add_strict_mono mult.right_neutral mult_succ ord one_V_def x(2) y(2)) then show ?thesis apply (simp add: oxy) using Ord_\ Ord_mult Ord_oexp Ord_trans mem_0_Ord mult_add_mem_0 oexp_eq_0_iff omega_nonzero oxy succ_in_omega by presburger qed ultimately show ?thesis using ord \Ord (\\$$\ limit oexp_Limit by auto qed qed lemma \_power_imp_eq: assumes "\ < \\\" "Ord \" "Ord \" "\ \ 0" shows "\ + \\\ = \\\" by (simp add: assms indecomposable_\_power indecomposable_imp_eq) lemma mult_oexp_indec: "\Ord \; Limit \; indecomposable \\ \ \ * (\ \ \) = (\ \ \)" by (metis Limit_def Ord_1 OrdmemD indecomposable_imp_eq oexp_1_right oexp_add one_V_def) lemma mult_oexp_\: "Ord \ \ \ * (\ \ \) = (\ \ \)" by (metis Ord_1 Ord_\ oexp_1_right oexp_add one_plus_\_equals_\) lemma type_imp_indecomposable: assumes \: "Ord \" and minor: "\X. X \ elts \ \ ordertype X VWF = \ \ ordertype (elts \ - X) VWF = \" shows "indecomposable \" unfolding indecomposable_def proof (intro conjI ballI) fix \ \ assume \: "\ \ elts \" and \: "\ \ elts \" then obtain \\: "elts \ \ elts \" "elts \ \ elts \" "Ord \" "Ord \" using \ Ord_in_Ord Ord_trans by blast then have oeq: "ordertype (elts \) VWF = \" by auto show "\ + \ \ elts \" proof (rule ccontr) assume "\ + \ \ elts \" then obtain \ where \: "Ord \" "\ + \ = \" by (metis Ord_ordertype \$$1) le_Ord_diff less_eq_V_def minor oeq) then have "\ \ elts \" using Ord_linear \\ \ \\ + \ \ elts \\ by blast then have "ordertype (elts \ - elts$$ VWF = \" using \ ordertype_diff Limit_def \ \Ord \\ by blast then show False by (metis \ \\ \ elts \\ \elts \ \ elts \\ oeq mem_not_refl minor) qed qed (use assms in auto) text \This proof uses Cantor normal form, yet still is rather long\ proposition indecomposable_is_\_power: assumes inc: "indecomposable \" obtains "\ = 0" | \ where "Ord \" "\ = \\\" proof (cases "\ = 0") case True then show thesis by (simp add: that) next case False obtain "Ord \" using Limit_def assms indecomposable_def by blast then obtain \s ms where Cantor: "List.set \s \ ON" "list.set ms \ {0<..}" "length \s = length ms" "Cantor_dec \s" and \: "\ = Cantor_sum \s ms" using Cantor_nf_exists by blast consider (0) "length \s = 0" | (1) "length \s = 1" | (2) "length \s \ 2" by linarith then show thesis proof cases case 0 then show ?thesis using \ assms False indecomposable_def by auto next case 1 then obtain \ m where \m: "\s = [\]" "ms = [m]" by (metis One_nat_def \length \s = length ms\ length_0_conv length_Suc_conv) then obtain "Ord \" "m \ 0" "Ord (\\\)" using \list.set \s \ ON\ \list.set ms \ {0<..}\ by auto have \: "\ = \\\ * ord_of_nat m" using \m by (simp add: \) moreover have "m = 1" proof (rule ccontr) assume "m \ 1" then have 2: "m \ 2" using \m \ 0\ by linarith then have "m = Suc 0 + Suc 0 + (m-2)" by simp then have "ord_of_nat m = 1 + 1 + ord_of_nat (m-2)" by (metis add.left_neutral mult.left_neutral mult_succ ord_of_nat.simps ord_of_nat_add) then have \eq: "\ = \\\ + \\\ + \\\ * ord_of_nat (m-2)" using \ by (simp add: add_mult_distrib) moreover have less: "\\\ < \" by (metis Ord_\ OrdmemD \eq \Ord \\ add_le_cancel_left0 add_less_cancel_left0 le_less_trans less_V_def oexp_gt_0_iff zero_in_omega) moreover have "\\\ + \\\ * ord_of_nat (m-2) < \" using "2" "\" \Ord \\ assms less indecomposableD less_V_def by auto ultimately show False using indecomposableD [OF inc, of "\\\" "\\\ + \\\ * ord_of_nat (m-2)"] by (simp add: \Ord (\\\)\ add.assoc) qed moreover have "Ord \" using \List.set \s \ ON\ by (simp add: \\s = [\]\) ultimately show ?thesis by (metis One_nat_def mult.right_neutral ord_of_nat.simps one_V_def that(2)) next case 2 then obtain \1 \2 \s' m1 m2 ms' where \m: "\s = \1#\2#\s'" "ms = m1#m2#ms'" by (metis Cantor(3) One_nat_def Suc_1 impossible_Cons length_Cons list.size(3) not_numeral_le_zero remdups_adj.cases) then obtain "Ord \1" "Ord \2" "m1 \ 0" "m2 \ 0" "Ord (\\\1)" "Ord (\\\2)" "list.set \s' \ ON" "list.set ms' \ {0<..}" using \list.set \s \ ON\ \list.set ms \ {0<..}\ by auto have oCs: "Ord (Cantor_sum \s' ms')" by (simp add: Ord_Cantor_sum \list.set \s' \ ON\) have \21: "\2 \ elts \1" using Cantor_dec_Cons_iff \m(1) \Cantor_dec \s\ by (simp add: Ord_mem_iff_lt \Ord \1\ \Ord \2\) have "\\\2 \ 0" by (simp add: \Ord \2\) then have *: "(\\\2 * ord_of_nat m2 + Cantor_sum \s' ms') > 0" by (simp add: OrdmemD \Ord (\\\2)\ \m2 \ 0\ mem_0_Ord oCs) have \: "\ = \\\1 * ord_of_nat m1 + (\\\2 * ord_of_nat m2 + Cantor_sum \s' ms')" (is "\ = ?\ + ?\") using \m by (simp add: \) moreover have "\\\2 * ord_of_nat m2 + Cantor_sum \s' ms' < \\\1 * ord_of_nat m1 + (\\\2 * ord_of_nat m2 + Cantor_sum \s' ms')" if "\2 \ elts \1" proof (rule less_\_power) show "Cantor_sum \s' ms' < \\\2" using \m Cantor cnf_2 by auto qed (use oCs \Ord \1\ \m1 \ 0\ \m2 \ 0\ that in auto) then have "?\ < \" using \21 by (simp add: \ \m) moreover have less: "?\ < \" using oCs by (metis \ "*" add_less_cancel_left add.right_neutral) ultimately have False using indecomposableD [OF inc, of "?\" "?\"] by (simp add: \Ord (\\\1)\ \Ord (\\\2)\ oCs) then show ?thesis .. qed qed corollary indecomposable_iff_\_power: "indecomposable \ \ \ = 0 \ (\\. \ = \\\ \ Ord \)" by (meson indecomposable_0 indecomposable_\_power indecomposable_is_\_power) theorem indecomposable_imp_type: fixes X :: "bool \ V set" assumes \: "indecomposable \" and "\b. ordertype (X b) VWF \ \" "\b. small (X b)" "\b. X b \ ON" and "elts \ \ (UN b. X b)" shows "\b. ordertype (X b) VWF = \" using \ [THEN indecomposable_imp_Ord] assms proof (induction arbitrary: X) case (succ \) show ?case proof (cases "\ = 0") case True then have "\b. 0 \ X b" using succ.prems(5) by blast then have "\b. ordertype (X b) VWF \ 0" using succ.prems(3) by auto then have "\b. ordertype (X b) VWF \ succ 0" by (meson Ord_0 Ord_linear2 Ord_ordertype less_eq_V_0_iff succ_le_iff) then show ?thesis using True succ.prems(2) by blast next case False then show ?thesis using succ.prems by auto qed next case (Limit \) then obtain \ where \: "\ = \\\" and "\ \ 0" "Ord \" by (metis Limit_eq_Sup_self image_ident indecomposable_is_\_power not_succ_Limit oexp_0_right one_V_def zero_not_Limit) show ?case proof (cases "Limit \") case True have ot: "\b. ordertype (X b \ elts (\\\)) VWF = \\\" if "\ \ elts \" for \ proof (rule Limit.IH) have "Ord \" using Ord_in_Ord \Ord \\ that by blast then show "\\\ \ elts \" by (simp add: Ord_mem_iff_lt \ \_gt1 \Ord \\ oexp_less that) show "indecomposable (\\\)" using \Ord \\ indecomposable_1 indecomposable_\_power by fastforce show "small (X b \ elts (\\\))" for b by (meson down inf_le2) show "ordertype (X b \ elts (\ \ \)) VWF \ \ \ \" for b by (simp add: \Ord \\ ordertype_le_Ord) show "X b \ elts (\ \ \) \ ON" for b by (simp add: Limit.prems inf.coboundedI1) show "elts (\ \ \) \ (\b. X b \ elts (\ \ \))" using Limit.prems Limit.hyps \\ \ \ \ elts \\ by clarsimp (metis Ord_trans UN_E indecomposable_imp_Ord subset_eq) qed define A where "A \ \b. {\ \ elts \. ordertype (X b \ elts (\\\)) VWF \ \\\}" have Asmall: "small (A b)" for b by (simp add: A_def) have AON: "A b \ ON" for b using A_def \Ord \\ elts_subset_ON by blast have eq: "elts \ = (\ b. A b)" by (auto simp: A_def) (metis ot eq_refl) then obtain b where b: "Sup (A b) = \" using \Limit \\ apply (auto simp: UN_bool_eq) by (metis AON ON_imp_Ord Ord_Sup Ord_linear_le Limit_eq_Sup_self Sup_Un_distrib Asmall sup.absorb2 sup.orderE) have "\\\ \ ordertype (X b) VWF" if "\ \ A b" for \ proof - have "(\\\) = ordertype ((X b) \ elts (\\\)) VWF" using \Ord \\ that by (simp add: A_def Ord_in_Ord dual_order.antisym ordertype_le_Ord) also have "\ \ ordertype (X b) VWF" by (simp add: Limit.prems ordertype_VWF_mono) finally show ?thesis . qed then have "ordertype (X b) VWF \ Sup ((\\. \\\)  A b)" by blast moreover have "Sup ((\\. \\\)  A b) = \ \ Sup (A b)" by (metis b Ord_\ ZFC_in_HOL.Sup_empty AON \\ \ 0\ Asmall oexp_Sup omega_nonzero) ultimately show ?thesis using Limit.hyps Limit.prems \ b by auto next case False then obtain \ where \: "\ = succ \" "Ord \" using Ord_cases \\ \ 0\ \Ord \\ by auto then have Ord\\: "Ord (\\\)" using Ord_oexp by blast have subX12: "elts (\\\ * \) \ (\b. X b)" using Limit \ \ by auto define E where "E \ \n. {\\\ * ord_of_nat n ..< \\\ * ord_of_nat (Suc n)} \ ON" have EON: "E n \ ON" for n using E_def by blast have E_imp_less: "x < y" if "i < j" "x \ E i" "y \ E j" for x y i j proof - have "succ (i) \ ord_of_nat j" using that(1) by force then have "\ y \ x" using that apply (auto simp: E_def) by (metis Ord\\ Ord_ord_of_nat leD mult_cancel_le_iff ord_of_nat.simps(2) order_trans) with that show ?thesis by (meson EON ON_imp_Ord Ord_linear2) qed then have djE: "disjnt (E i) (E j)" if "i \ j" for i j using that nat_neq_iff unfolding disjnt_def by auto have less_imp_E: "i \ j" if "x < y" "x \ E i" "y \ E j" for x y i j using that E_imp_less [OF _ \y \ E j\ \x \ E i\] leI less_asym by blast have inc: "indecomposable (\\\)" using \ indecomposable_1 indecomposable_\_power by fastforce have in_En: "\\\ * ord_of_nat n + x \ E n" if "x \ elts (\\\)" for x n using that Ord\\ Ord_in_Ord [OF Ord\\] by (auto simp: E_def Ord\\ OrdmemD mult_succ) have *: "elts \ = $$range E)" proof have "\m. \\\ * m \ x \ x < \\\ * succ (ord_of_nat m)" if "x \ elts (\\\ * ord_of_nat n)" for x n using that apply (clarsimp simp add: mult [of _ "ord_of_nat n"] lift_def) by (metis add_less_cancel_left OrdmemD inc indecomposable_imp_Ord mult_succ plus sup_ge1) moreover have "Ord x" if "x \ elts (\\\ * ord_of_nat n)" for x n by (meson Ord\\ Ord_in_Ord Ord_mult Ord_ord_of_nat that) ultimately show "elts \ \ \(range E)" by (auto simp: \ \ E_def mult_Limit elts_$$ have "x \ elts (\\\ * succ(ord_of_nat n))" if "Ord x" "x < \\\ * succ (n)" for x n by (metis that Ord_mem_iff_lt Ord_mult Ord_ord_of_nat inc indecomposable_imp_Ord ord_of_nat.simps(2)) then show "$$range E) \ elts \" by (force simp: \ \ E_def Limit.prems mult_Limit) qed have smE: "small (E n)" for n by (metis "*" complete_lattice_class.Sup_upper down rangeI) have otE: "ordertype (E n) VWF = \\\" for n by (simp add: E_def inc indecomposable_imp_Ord mult_succ ordertype_interval_eq) define cut where "cut \ \n x. odiff x (\\\ * ord_of_nat n)" have cutON: "cut n  X \ ON" if "X \ ON" for n X using that by (simp add: image_subset_iff cut_def ON_imp_Ord Ord\\ Ord_odiff) have cut [simp]: "cut n (\ \ \ * ord_of_nat n + x) = x" for x n by (auto simp: cut_def) have cuteq: "x \ cut n  (X \ E n) \ \\\ * ord_of_nat n + x \ X" if x: "x \ elts (\\$$" for x X n proof show "\\\ * ord_of_nat n + x \ X" if "x \ cut n  (X \ E n)" using E_def Ord\\ Ord_odiff_eq image_iff local.cut_def that by auto show "x \ cut n  (X \ E n)" if "\\\ * ord_of_nat n + x \ X" by (metis (full_types) IntI cut image_iff in_En that x) qed have ot_cuteq: "ordertype (cut n  (X \ E n)) VWF = ordertype (X \ E n) VWF" for n X proof (rule ordertype_VWF_inc_eq) show "X \ E n \ ON" using E_def by blast then show "cut n  (X \ E n) \ ON" by (simp add: cutON) show "small (X \ E n)" by (meson Int_lower2 smE smaller_than_small) show "cut n x < cut n y" if "x \ X \ E n" "y \ X \ E n" "x < y" for x y using that \X \ E n \ ON\ by(simp add: E_def Ord\\ Ord_odiff_less_odiff local.cut_def) qed define N where "N \ \b. {n. ordertype (X b \ E n) VWF = \\\}" have "\b. infinite (N b)" proof (rule ccontr) assume "\b. infinite (N b)" then obtain n where "\b. n \ N b" apply (simp add: ex_bool_eq) by (metis (full_types) finite_nat_set_iff_bounded not_less_iff_gr_or_eq) moreover have "\b. ordertype (cut n  (X b \ E n)) VWF = \\\" proof (rule Limit.IH) show "\\\ \ elts \" by (metis Limit.hyps Limit_def Limit_omega Ord_mem_iff_less_TC \ \ mult_le2 not_succ_Limit oexp_succ omega_nonzero one_V_def) show "indecomposable (\\\)" by (simp add: inc) show "ordertype (cut n  (X b \ E n)) VWF \ \\\" for b by (metis "otE" inf_le2 ordertype_VWF_mono ot_cuteq smE) show "small (cut n  (X b \ E n))" for b using smE subset_iff_less_eq_V by (meson inf_le2 replacement) show "cut n  (X b \ E n) \ ON" for b using E_def cutON by auto have "elts (\\\ * succ n) \ $$range X)" by (metis Ord\\ Ord_\ Ord_ord_of_nat less_eq_V_def mult_cancel_le_iff ord_of_nat.simps(2) ord_of_nat_le_omega order_trans subX12) then show "elts (\\$$ \ (\b. cut n  (X b \ E n))" by (auto simp: mult_succ mult_Limit UN_subset_iff cuteq UN_bool_eq) qed then have "\b. ordertype (X b \ E n) VWF = \\\" by (simp add: ot_cuteq) ultimately show False by (simp add: N_def) qed then obtain b where b: "infinite (N b)" by blast then obtain \ :: "nat \ nat" where \: "bij_betw \ UNIV (N b)" and mono: "strict_mono \" by (meson bij_enumerate enumerate_mono strict_mono_def) then have "ordertype (X b \ E (\ n)) VWF = \\\" for n using N_def bij_betw_imp_surj_on by blast moreover have "small (X b \ E (\ n))" for n by (meson inf_le2 smE subset_iff_less_eq_V) ultimately have "\f. bij_betw f (X b \ E (\ n)) (elts (\\\)) \ (\x \ X b \ E (\ n). \y \ X b \ E (\ n). f x < f y \ (x,y) \ VWF)" for n by (metis Ord_ordertype ordertype_VWF_eq_iff) then obtain F where bijF: "\n. bij_betw (F n) (X b \ E (\ n)) (elts (\\\))" and F: "\n. \x \ X b \ E (\ n). \y \ X b \ E (\ n). F n x < F n y \ (x,y) \ VWF" by metis then have F_bound: "\n. \x \ X b \ E (\ n). F n x < \\\" by (metis Ord_\ Ord_oexp OrdmemD $$2) bij_betw_imp_surj_on image_eqI) have F_Ord: "\n. \x \ X b \ E (\ n). Ord (F n x)" by (metis otE ON_imp_Ord Ord_ordertype bijF bij_betw_def elts_subset_ON imageI) have inc: "\ n \ n" for n by (simp add: mono strict_mono_imp_increasing) have dj\: "disjnt (E (\ i)) (E (\ j))" if "i \ j" for i j by (rule djE) (use \ that in \auto simp: bij_betw_def inj_def$$ define Y where "Y \ (\n. E (\ n))" have "\n. y \ E (\ n)" if "y \ Y" for y using Y_def that by blast then obtain \ where \: "\y. y \ Y \ y \ E (\ (\ y))" by metis have "Y \ ON" by (auto simp: Y_def E_def) have \le: "\ x \ \ y" if "x < y" "x \ Y" "y \ Y" for x y using less_imp_E strict_mono_less_eq that \ [OF \x \ Y\] \ [OF \y \ Y\] mono unfolding Y_def by blast have eq\: "x \ E (\ k) \ \ x = k" for x k using \ unfolding Y_def by (meson UN_I disjnt_iff dj\ iso_tuple_UNIV_I) have upper: "\\\ * ord_of_nat (\ x) \ x" if "x \ Y" for x using that proof (clarsimp simp add: Y_def eq\) fix u v assume u: "u \ elts (\\\ * ord_of_nat v)" and v: "x \ E (\ v)" then have "u < \\\ * ord_of_nat v" by (simp add: OrdmemD $$2)) also have "\ \ \\\ * ord_of_nat (\ v)" by (simp add: \(2) inc) also have "\ \ x" using v by (simp add: E_def) finally show "u \ elts x" using \Y \ ON\ by (meson ON_imp_Ord Ord_\ Ord_in_Ord Ord_mem_iff_lt Ord_mult Ord_oexp Ord_ord_of_nat \(2) that u) qed define G where "G \ \x. \\\ * ord_of_nat (\ x) + F (\ x) x" have G_strict_mono: "G x < G y" if "x < y" "x \ X b \ Y" "y \ X b \ Y" for x y proof (cases "\ x = \ y") case True then show ?thesis using that unfolding G_def by (metis F Int_iff add_less_cancel_left Limit.prems(4) ON_imp_Ord VWF_iff_Ord_less$$ next case False then have "\ x < \ y" by (meson IntE \le le_less that) then show ?thesis using that by (simp add: G_def F_Ord F_bound Ord\\ \ mult_nat_less_add_less) qed have "ordertype (X b \ Y) VWF = (\\\) * \" proof (rule ordertype_VWF_eq_iff [THEN iffD2]) show "Ord (\\\ * \)" by (simp add: \) show "small (X b \ Y)" by (meson Limit.prems(3) inf_le1 subset_iff_less_eq_V) have "bij_betw G (X b \ Y) (elts (\\\ * \))" proof (rule bij_betw_imageI) show "inj_on G (X b \ Y)" proof (rule linorder_inj_onI) fix x y assume xy: "x < y" "x \ (X b \ Y)" "y \ (X b \ Y)" show "G x \ G y" using G_strict_mono xy by force next show "x \ y \ y \ x" if "x \ (X b \ Y)" "y \ (X b \ Y)" for x y using that \X b \ ON\ by (clarsimp simp: Y_def) (metis ON_imp_Ord Ord_linear Ord_trans) qed show "G  (X b \ Y) = elts (\\\ * \)" proof show "G  (X b \ Y) \ elts (\\\ * \)" using \X b \ ON\ apply (clarsimp simp: G_def mult_Limit Y_def eq\) by (metis IntI add_mem_right_cancel bijF bij_betw_imp_surj_on image_eqI mult_succ ord_of_nat_\ succ_in_omega) show "elts (\\\ * \) \ G  (X b \ Y)" proof fix x assume x: "x \ elts (\\\ * \)" then obtain k where n: "x \ elts (\\\ * ord_of_nat (Suc k))" and minim: "\m. m < Suc k \ x \ elts (\\\ * ord_of_nat m)" using elts_mult_\E by (metis old.nat.exhaust) then obtain y where y: "y \ elts (\\\)" and xeq: "x = \\\ * ord_of_nat k + y" using x by (auto simp: mult_succ elim: mem_plus_V_E) then have 1: "inv_into (X b \ E (\ k)) (F k) y \ (X b \ E (\ k))" by (metis bijF bij_betw_def inv_into_into) then have "(inv_into (X b \ E (\ k)) (F k) y) \ X b \ Y" by (force simp: Y_def) moreover have "G (inv_into (X b \ E (\ k)) (F k) y) = x" by (metis "1" G_def Int_iff bijF bij_betw_inv_into_right eq\ xeq y) ultimately show "x \ G  (X b \ Y)" by blast qed qed qed moreover have "(x,y) \ VWF" if "x \ X b" "x \ Y" "y \ X b" "y \ Y" "G x < G y" for x y proof - have "x < y" using that by (metis G_strict_mono Int_iff Limit.prems(4) ON_imp_Ord Ord_linear_lt less_asym) then show ?thesis using ON_imp_Ord \Y \ ON\ that by auto qed moreover have "G x < G y" if "x \ X b" "x \ Y" "y \ X b" "y \ Y" "(x, y) \ VWF" for x y proof - have "x < y" using that ON_imp_Ord \Y \ ON\ by auto then show ?thesis by (simp add: G_strict_mono that) qed ultimately show "\f. bij_betw f (X b \ Y) (elts (\\\ * \)) \ (\x$$X b \ Y). \y\(X b \ Y). f x < f y \ ((x, y) \ VWF))" by blast qed moreover have "ordertype (\n. X b \ E (\ n)) VWF \ ordertype (X b) VWF" using Limit.prems(3) ordertype_VWF_mono by auto ultimately have "ordertype (X b) VWF = (\\$$ * \" using Limit.hyps Limit.prems(2) \ \ using Y_def by auto then show ?thesis using Limit.hyps \ \ by auto qed qed auto corollary indecomposable_imp_type2: assumes \: "indecomposable \" "X \ elts \" shows "ordertype X VWF = \ \ ordertype (elts \ - X) VWF = \" proof - have "Ord \" using assms indecomposable_imp_Ord by blast have "\b. ordertype (if b then X else elts \ - X) VWF = \" proof (rule indecomposable_imp_type) show "ordertype (if b then X else elts \ - X) VWF \ \" for b by (simp add: \Ord \\ assms ordertype_le_Ord) show "(if b then X else elts \ - X) \ ON" for b using \Ord \\ assms elts_subset_ON by auto qed (use assms down in auto) then show ?thesis by (metis (full_types)) qed subsection \From ordinals to order types\ lemma indecomposable_ordertype_eq: assumes indec: "indecomposable \" and \: "ordertype A VWF = \" and A: "B \ A" "small A" shows "ordertype B VWF = \ \ ordertype (A-B) VWF = \" proof (rule ccontr) assume "\ (ordertype B VWF = \ \ ordertype (A - B) VWF = \)" moreover have "ordertype (ordermap A VWF  B) VWF = ordertype B VWF" using \B \ A\ by (auto intro: ordertype_image_ordermap [OF \small A\]) moreover have "ordertype (elts \ - ordermap A VWF  B) VWF = ordertype (A - B) VWF" by (metis ordertype_map_image \ A elts_of_set ordertype_def replacement) moreover have "ordermap A VWF ` B \ elts \" using \ A by blast ultimately show False using indecomposable_imp_type2 [OF \indecomposable \\] \small A\ by metis qed lemma indecomposable_ordertype_ge: assumes indec: "indecomposable \" and \: "ordertype A VWF \ \" and small: "small A" "small B" shows "ordertype B VWF \ \ \ ordertype (A-B) VWF \ \" proof - obtain A' where "A' \ A" "ordertype A' VWF = \" by (meson \ \small A\ indec indecomposable_def le_ordertype_obtains_subset) then have "ordertype (B \ A') VWF = \ \ ordertype (A'-B) VWF = \" by (metis Diff_Diff_Int Diff_subset Int_commute \small A\ indecomposable_ordertype_eq indec smaller_than_small) moreover have "ordertype (B \ A') VWF \ ordertype B VWF" by (meson Int_lower1 small ordertype_VWF_mono smaller_than_small) moreover have "ordertype (A'-B) VWF \ ordertype (A-B) VWF" by (meson Diff_mono Diff_subset \A' \ A\ \small A\ order_refl ordertype_VWF_mono smaller_than_small) ultimately show ?thesis by blast qed text \now for finite partitions\ lemma indecomposable_ordertype_finite_eq: assumes "indecomposable \" and \: "finite \" "pairwise disjnt \" "\\ = A" "\ \ {}" "ordertype A VWF = \" "small A" shows "\X \ \. ordertype X VWF = \" using \ proof (induction arbitrary: A) case (insert X \) show ?case proof (cases "\ = {}") case True then show ?thesis using insert.prems by blast next case False have smA: "small (\\)" using insert.prems by auto show ?thesis proof (cases "\X \ \. ordertype X VWF = \") case True then show ?thesis using insert.prems by blast next case False have "X = A - \\" using insert.hyps insert.prems by (auto simp: pairwise_insert disjnt_iff) then have "ordertype X VWF = \" using indecomposable_ordertype_eq assms insert False by (metis Union_mono cSup_singleton pairwise_insert smA subset_insertI) then show ?thesis using insert.prems by blast qed qed qed auto lemma indecomposable_ordertype_finite_ge: assumes indec: "indecomposable \" and \: "finite \" "A \ \\" "\ \ {}" "ordertype A VWF \ \" "small (\\)" shows "\X \ \. ordertype X VWF \ \" using \ proof (induction arbitrary: A) case (insert X \) show ?case proof (cases "\ = {}") case True then have "\ \ ordertype X VWF" using insert.prems by (simp add: order.trans ordertype_VWF_mono) then show ?thesis using insert.prems by blast next case False show ?thesis proof (cases "\X \ \. ordertype X VWF \ \") case True then show ?thesis using insert.prems by blast next case False moreover have "small (X \ \\)" using insert.prems by auto moreover have "ordertype ($$insert X$$) VWF \ \" using insert.prems ordertype_VWF_mono by blast ultimately have "ordertype X VWF \ \" using indecomposable_ordertype_ge [OF indec] by (metis Diff_subset_conv Sup_insert cSup_singleton insert.IH small_sup_iff subset_refl) then show ?thesis using insert.prems by blast qed qed qed auto end