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,4464 +1,4424 @@ 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\ primrec normal:: "nat list \ bool" where normal_0: "normal [] = True" | normal_Suc: "normal (m#ms) = (m > 0)" lemma omega_sum_0_iff [simp]: "normal ns \ omega_sum ns = 0 \ ns = []" by (induction ns) 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 "length ms < length ns" "normal ns" shows "omega_sum ms < omega_sum ns" proof (cases ns) case (Cons n ns') have "\ \ length ms \ \ \ length ns'" using assms local.Cons by (simp add: oexp_mono_le) then have "\ omega_sum (n#ns') \ omega_sum ms" using omega_sum_ge [of n ns'] omega_sum_less [of ms] \normal ns\ local.Cons by auto then show ?thesis by (metis Ord_linear2 Ord_omega_sum local.Cons) qed (use assms in 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 L: ?lhs then have "length ms \ length ns" using omega_sum_length_leD [OF less_imp_le [OF L]] by (simp add: \m > 0\) moreover have "m\n" if "length ms = length ns" using L omega_sum_less_eqlen_iff_cases that by auto ultimately show ?rhs using L by auto next assume ?rhs moreover have "omega_sum (m # ms) < omega_sum (n # ns)" if "length ms < length ns" using that by (metis Suc_mono \n > 0\ length_Cons normal_Suc omega_sum_length_less) ultimately show ?lhs using omega_sum_less_eqlen_iff_cases by force 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)" by (metis (mono_tags, hide_lams) WW_def equalityI image_subset_iff into_from_WW mem_Collect_eq rangeI strict_sorted_into_WW subset_iff) 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)" by blast lemma 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) next show "\  elts (\\\) \ WW" by (auto simp: \_def WW_def strict_sorted_into_WW) qed auto 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 sorted_trans: assumes "xs < ys" "ys < zs" "sorted ys" "ys \ []" shows "xs < zs" using assms unfolding less_list_def by (metis dual_order.strict_trans last_in_set leD neqE sorted_hd_le) lemma strict_sorted_imp_append_less: assumes "strict_sorted (xs @ ys)" shows "xs < ys" using assms by (simp add: less_list_def sorted_wrt_append strict_sorted_sorted_wrt) 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 (auto simp: sorted_wrt_append strict_sorted_sorted_wrt) qed lemma singleton_less_list_iff: "sorted xs \ [n] < xs \ {..n} \ list.set xs = {}" apply (simp add: less_list_def set_eq_iff) by (metis empty_iff less_le_trans list.set(1) list.set_sel(1) not_le sorted_hd_le) lemma less_last_iff: "xs@[x] < ys \ [x] < ys" by (simp add: less_list_def) lemma less_Cons_iff: "NO_MATCH [] ys \ xs < y#ys \ xs < [y]" by (simp add: less_list_def) lemma less_hd_imp_less: "xs < [hd ys] \ xs < ys" by (simp add: less_list_def) lemma last_less_imp_less: "[last xs] < 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" assumes "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 \finite S'\ 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 using sorted_list_of_set_imp_less_sets strict_sorted_imp_sorted by (auto simp: init_segment_def strict_sorted_append_iff) 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 "\j. \j<2; i\j\ \ (h \ list_of) - {j} \ (list.set  AM) \ Pow N = {}" unfolding Ramsey_def by (metis \infinite M\) then have N_disjoint: "(h \ list_of) - {1-i} \ (list.set  AM) \ Pow N = {}" by (metis One_nat_def diff_less_Suc not_less_eq numeral_2_eq_2 zero_less_diff) 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" proof (clarsimp simp add: less_list_def) assume "y \ []" and ne: "interact xs ys \ []" then show "last y < hd (interact xs ys)" using 3 apply simp by (metis dual_order.strict_trans1 hd_interact length_greater_0_conv less_list_def list.sel(1) lists.simps mem_lists_non_Nil nth_Cons' nth_mem) qed 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 (elim Form.cases Form_Body.cases; metis dual_order.order_iff_strict less_not_refl) lemma Form_Body_WW: assumes "Form_Body ka kb xs ys zs" shows "zs \ WW" by (rule Form_Body.cases [OF assms]) (auto simp: WW_def) lemma Form_Body_nonempty: assumes "Form_Body ka kb xs ys zs" shows "length zs > 0" by (rule Form_Body.cases [OF assms]) auto lemma Form_Body_length: assumes "Form_Body ka kb xs ys zs" shows "length xs < length ys" using Form_Body.cases assms by blast 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 form_cases [of l] proof cases case zero then show ?thesis using Form_0_cases_raw assms that(1) by auto next case (nz ka kb) obtain xs ys where xys: "xs \ ys" "U = {xs,ys}" "length xs \ length ys" using Form_elim_upair assms by blast show ?thesis proof (cases "ka = kb") case True show ?thesis using Form.cases [OF \Form l U\] proof cases case (2 k xs' ys' zs') then show ?thesis by (metis le_Suc_eq le_refl mult_2 that) qed (use True nz in \presburger+\) next case False show ?thesis using Form.cases [OF \Form l U\] proof cases case (3 k xs' ys' zs') then show ?thesis by (metis add_Suc_right add_Suc_shift diff_Suc_1 le_Suc_eq mult_2 order_refl that) qed (use False nz in \presburger+\) qed qed 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_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) lemma inter_scheme_strict_sorted: assumes "Form l U" "l>0" shows "strict_sorted (inter_scheme l U)" using inter_scheme_simple [OF assms] by (auto simp: WW_def) 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) show ?case proof (cases x) case Nil show ?thesis proof (cases y) case Nil then show ?thesis using "3" strict_sorted_append_iff by (auto simp: \x = []\) next case (Cons a list) with Nil 3 show ?thesis apply (simp add: strict_sorted_append_iff) by (metis (no_types, lifting) Un_iff set_interact sorted_wrt_append strict_sorted_append_iff strict_sorted_sorted_wrt) qed next case (Cons a list) have \
: "sorted_wrt (<) ((a # list) @ y @ interact xs ys)" by (metis (no_types) "3.prems" interact.simps(3) local.Cons strict_sorted_sorted_wrt) then have "list = [] \ concat xs = [] \ last list < hd (concat xs)" by (metis (full_types) Un_iff hd_in_set last_ConsR last_in_set list.simps(3) set_append set_interact sorted_wrt_append) then have "list < concat xs" using less_list_def by blast have "list < y" by (metis \
append.assoc last.simps less_list_def list.distinct(1) strict_sorted_append_iff strict_sorted_sorted_wrt) note Cons1 = Cons show ?thesis proof (cases y) case Nil then show ?thesis using 3 by (simp add: sorted_wrt_append strict_sorted_sorted_wrt) next case (Cons a' list') have "strict_sorted (list' @ concat ys)" using "3.IH" local.Cons "\
" by (simp add: strict_sorted_sorted_wrt sorted_wrt_append) moreover have "y < concat ys" by (metis "\
" Un_iff hd_in_set last_in_set less_list_def set_interact sorted_wrt_append) ultimately show ?thesis using 3 \list < concat xs\ by (auto simp: Cons1 strict_sorted_append_iff) qed qed 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) 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']" 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) 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 "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) 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') 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') 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')" 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) 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 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 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') 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 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) ultimately obtain j N where "j < 2" "infinite N" "N \ M" and hj: "h  {l \ ?A. List.set l \ 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 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 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 "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) ultimately show ?thesis using that by auto qed moreover have "n < Inf (N - {n})" unfolding n_def 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) 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) qed ultimately 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" + 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" + 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))" + 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 + 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)" + 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)" + have "RF (k-1) q \ 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)" + 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" + 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)" + 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" + 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) 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 lemma 3.8\ - -text \Lemma 3.8 of Jean A. Larson, ibid.\ +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 :: nat \ nat \ nat set, M::nat set). \l::nat. - dl l \ a \ finite a \ dl l \ {} \ a \ {} \ + "\ \ \(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" + 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 Min_in card_eq_0_iff greaterThan_iff le_inf_iff less_nat_zero_code n_not_Suc_n nxt_def subsetD) + 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) + 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 (no_types, hide_lams) IntE Min_in card.empty greaterThan_iff leD not_less_eq_eq nxt_def subsetD zero_less_Suc) + 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" for k k' using that by (induction "k-k'")(auto simp: Inf_M_Suc_ge M_Suc_subset cInf_superset_mono infinite_imp_nonempty lift_Suc_antimono_le) 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 split: prod.split_asm) + 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) + 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 1 - then show ?thesis - by (simp add: Pair bf_rec snd_grab_subset) - next - case 2 - then have "snd (bf M r x) \ snd (bf M r (j', i'))" - by (simp add: Pair less.IH prev_pair_less that(2)) - moreover have "snd (bf M r u) \ snd (bf M r x)" - by (simp add: 2 Pair bf_rec snd_grab_subset) - ultimately show ?thesis - by auto - qed + 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 bf_subset less_sets_fst_grab \infinite M\ by auto + 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) + 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) + 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) + 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)" + 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) \ {}" + 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 :: "nat set" - and x j' i' :: nat + 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::nat)" + 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 - have "b k (j,i) \ {\(M k)..}" - by (rule order_trans [OF _ b_InfM]) auto - also have "\ \ {Inf(M (Suc k'))..}" - using Inf_M_telescoping k by auto - finally show "b k (j,i) \ {Inf(M (Suc k'))..}" . + 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: "K \ \ j0 j \ finite K" for K j0 j - by (simp add: \_def nsets_def) - have \_card: "K \ \ j0 j \ card K = j" for K j0 j - by (simp add: \_def nsets_def) + 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})" - apply (simp add: subset_iff) - by (metis Diff_iff Max.coboundedI Max_in card_0_eq insert_Diff insert_iff le_neq_implies_less nat.distinct(1)) - then show "\L\{j0<..}. finite L \ card L = j \ - (\i\{Max (insert j0 L)<..}. K = insert i L)" + 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_in card_Diff_singleton_if card_gt_0_iff diff_Suc_1 finite_Diff greaterThan_iff insert_subset zero_less_Suc) + 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) - show "enum K j \ K" - by (simp add: cardK finite_enumerate_in_set) - show "k \ enum K j" if "k \ K" for k - using that K - by (metis \finite K\ cardK enum_obtain_index_finite finite_enumerate_mono leI less_Suc_eq less_asym) - qed auto + 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" if "k>0" for k - using that + have b_ge_k: "\ (b k (k, k-1)) \ k-1" for k proof (induction k) case (Suc k) show ?case proof (cases "k=0") case False - have "\ (b k (k, k - Suc 0)) < \ (b (Suc k) (Suc k, k))" - using False Inf_b_less by auto - with False Suc show ?thesis + 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: "k>0" "k \ j" and "j > i" for k j i - using k - proof (induction k) - case (Suc k) - show ?case - proof (cases "j \ k") - case True - have "\ (b k (j,i)) < \ (b (Suc k) (j,i))" - using \j > i\ Suc True by (force intro: Inf_b_less) - then show ?thesis - using Suc.IH True by linarith - next - case False - then have "j = Suc k" - using Suc.prems(2) by linarith - with \i < j\ have "i < Suc k" - by fastforce - moreover have "\ \ (b (Suc k) (j,i)) < \ (b (Suc k) (j,i))" - by fastforce - ultimately have "\ Suc (\ (b (Suc k) (j,i))) < Suc k" - by (metis Inf_b_less \j = Suc k\ b_ge_k diff_Suc_1 leD le_refl lessI zero_less_Suc) - then show ?thesis - by simp - qed - 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 [of _ j i] \j > i\ Sucj - by (metis (no_types, lifting) diff_Suc_1 le_SucI le_trans less_Suc_eq_le nat_le_linear zero_less_Suc) + 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) + proof (induction j) \\a difficult business, 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 subset_iff sorted_list_of_set_Un less_sets_UN2) fix X Y assume X [rule_format]: "\t. t \ X \ j0 < t" and Y [rule_format]: "\t. t \ Y \ j0 < t" and "finite X" and jeq: "j = card X" and "finite Y" 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" by (simp add: Y \card Y = card X\ \finite Y\ finite_enumerate_in_set 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 (rule 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 (metis \_finite atLeast_Suc_greaterThan finite_insert less_sets_Suc_Max less_sets_weaken1 subset_insertI) 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 (metis ih One_nat_def Ord_\ Ord_ord_of_nat oexp_1_right oexp_add one_V_def ord_of_nat.simps(1) ord_of_nat.simps(2) ord_of_nat_add plus_1_eq_Suc) 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(1) that(2)) 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 proof (cases "k < r") case True then show ?thesis by (simp add: ba less_sets_imp_disjnt that) next case False then show ?thesis proof - have "a r \ b k (j,i)" by (metis False a_ne aa ab_same less_linear less_sets_UN2 less_sets_trans rangeI) then show ?thesis using disjnt_sym less_sets_imp_disjnt by blast qed qed 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) have dis: "disjnt (b (enum K j) (j0, j)) (\ii < j\ b_disjoint_less disjnt_def disjnt_sym less_Suc_eq that) qed have j0_less: "j0 < enum K j" by (meson Suc.prems Suc_le_lessD finite_enumerate_in_set greaterThan_iff less_le_trans subsetD K) 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 apply (simp add: card_b split: nat_diff_split) by (metis Suc.prems card_d finite_d finite_enumerate_step le_imp_less_Suc less_asym) 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 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 neg: "\ b (enum L p) (r, p) \ b (enum K i) (j,i)" and "i < j" "p < r" for i p proof (cases "enum K i" "enum L p" rule: linorder_cases) case less then show ?thesis by (simp add: bb enumK less_imp_le_nat \i < j\) next case equal then show ?thesis using \j < r\ enumK \i < j\ by (force simp: IJ_iff pair_less_def intro: bb_same) next case greater then show ?thesis using bb enumL less_imp_le_nat neg \p < r\ by blast qed 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 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 dual_order.refl less_sets_imp_list_less less_sets_weaken1) then have "ps < u1" by (metis K Ksub UnI1 \_card \finite K\ \j \ card K\ \d j \ list.set x\ acc_lengths_subset_d concat.simps(2) empty_iff empty_set hd_append2 less_list_def less_sets_imp_list_less less_sets_weaken1 list.set_sel(1) set_append u_sub 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 dual_order.refl less_sets_imp_list_less less_sets_weaken1) then have "qs < v1" by (metis L Lsub UnI1 \_card \finite L\ \r \ card L\ \d r \ list.set y\ acc_lengths_subset_d concat.simps(2) empty_iff empty_set hd_append2 less_list_def less_sets_imp_list_less less_sets_weaken1 list.set_sel(1) set_append v_sub 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\ apply (simp add: IJ_def pair_less_def less_sets_def) by (metis enumK b_ne card_b_finite last_in_set leD less_imp_le_nat 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 "Min (b (enum K i) (j,i)) \ n" using 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] u1_y apply (simp add: less_list_def disjnt_iff) by (metis card_b_finite hd_list_of leI less_imp_le_nat 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 (metis Min_in card_0_eq card_d d_eq finite_d fst_grab_subset greaterThan_iff in_mono le_inf_iff nxt_def old.nat.distinct(2)) 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 (no_types, hide_lams) One_nat_def Suc_1 WW_seg_subset_WW order.trans less_2_cases m not1 nth_Cons' nth_Cons_Suc) 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 by (metis TC_small UNIV_I UN_I otW' lenlex_transI ordertype_mono subsetI trans_less_than wf_lenlex wf_less_than) 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 with \1 < m\ show ?thesis apply (simp add: h_def len_h_seg \l \ WW\) by (meson \0 < length l\ bij_betw_inv_into_left bij_h_seg l) 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 have "(a, b) \ lenlex less_than" using omega_sum_less_iff by auto then show ?thesis by (simp add: \a \ WW\ \b \ WW\) 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 "f (h  Y) = 0" "finite Y" "card Y = 2" "Y \ M" apply (simp add: nsets_def subset_image_iff) by (metis \M \ WW\ \bij_betw h WW WW'\ bij_betw_def card_image card.infinite inj_on_subset zero_neq_numeral) then 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>\) 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 moreover have "[enum N k] < inter_scheme k u" using inter_scheme [of k u] strict_mono_enum [OF \infinite N\] \
apply (auto simp: less_list_def subset_image_iff subset_eq Bex_def image_iff) by (metis hd_in_set strict_mono_def) 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 False then have "l = 0" by blast 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 True 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 True 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