section ‹An ordinal partition theorem by Jean A. Larson› text ‹Jean A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$. \emph{Annals of Mathematical Logic}, 6:129--145, 1973.› theory Omega_Omega imports "HOL-Library.Product_Lexorder" Erdos_Milner begin abbreviation "list_of ≡ sorted_list_of_set" subsection ‹Cantor normal form for ordinals below @{term "ω↑ω"}› text ‹Unlike @{term Cantor_sum}, there is no list of ordinal exponents, which are instead taken as consecutive. We obtain an order-isomorphism between @{term "ω↑ω"} and increasing lists of natural numbers (ordered lexicographically).› fun omega_sum_aux where Nil: "omega_sum_aux 0 _ = 0" | Suc: "omega_sum_aux (Suc n) [] = 0" | Cons: "omega_sum_aux (Suc n) (m#ms) = (ω↑n) * (ord_of_nat m) + omega_sum_aux n ms" abbreviation omega_sum where "omega_sum ms ≡ omega_sum_aux (length ms) ms" text ‹A normal expansion has no leading zeroes› inductive normal:: "nat list ⇒ bool" where normal_Nil[iff]: "normal []" | normal_Cons: "m > 0 ⟹ normal (m#ms)" inductive_simps normal_Cons_iff [simp]: "normal (m#ms)" lemma omega_sum_0_iff [simp]: "normal ns ⟹ omega_sum ns = 0 ⟷ ns = []" by (induction ns rule: normal.induct) auto lemma Ord_omega_sum_aux [simp]: "Ord (omega_sum_aux k ms)" by (induction rule: omega_sum_aux.induct) auto lemma Ord_omega_sum: "Ord (omega_sum ms)" by simp lemma omega_sum_less_ωω [intro]: "omega_sum ms < ω↑ω" proof (induction ms) case (Cons m ms) have "ω ↑ (length ms) * ord_of_nat m ∈ elts (ω ↑ Suc (length ms))" using Ord_mem_iff_lt by auto then have "ω↑(length ms) * ord_of_nat m ∈ elts (ω↑ω)" using Ord_ord_of_nat oexp_mono_le omega_nonzero ord_of_nat_le_omega by blast with Cons show ?case by (auto simp: mult_succ OrdmemD oexp_less indecomposableD indecomposable_ω_power) qed (auto simp: zero_less_Limit) lemma omega_sum_aux_less: "omega_sum_aux k ms < ω ↑ k" proof (induction rule: omega_sum_aux.induct) case (3 n m ms) have " ω↑n * ord_of_nat m + ω↑n < ω↑n * ω" by (metis Ord_ord_of_nat ω_power_succ_gtr mult_succ oexp_succ ord_of_nat.simps(2)) with 3 show ?case using dual_order.strict_trans by force qed auto lemma omega_sum_less: "omega_sum ms < ω ↑ (length ms)" by (rule omega_sum_aux_less) lemma omega_sum_ge: "m ≠ 0 ⟹ ω ↑ (length ms) ≤ omega_sum (m#ms)" apply clarsimp by (metis Ord_ord_of_nat add_le_cancel_left0 le_mult Nat.neq0_conv ord_of_eq_0_iff vsubsetD) lemma omega_sum_length_less: assumes "normal ns" "length ms < length ns" shows "omega_sum ms < omega_sum ns" using assms proof (induction rule: normal.induct) case (normal_Cons n ns') have "ω ↑ length ms ≤ ω ↑ length ns'" using normal_Cons oexp_mono_le by auto then show ?case by (metis gr_implies_not_zero less_le_trans normal_Cons.hyps omega_sum_aux_less omega_sum_ge) qed auto lemma omega_sum_length_leD: assumes "omega_sum ms ≤ omega_sum ns" "normal ms" shows "length ms ≤ length ns" by (meson assms leD leI omega_sum_length_less) lemma omega_sum_less_eqlen_iff_cases [simp]: assumes "length ms = length ns" shows "omega_sum (m#ms) < omega_sum (n#ns) ⟷ m<n ∨ m=n ∧ omega_sum ms < omega_sum ns" using omega_sum_less [of ms] omega_sum_less [of ns] by (metis Kirby.add_less_cancel_left Omega_Omega.Cons Ord_ω Ord_oexp Ord_omega_sum Ord_ord_of_nat assms length_Cons linorder_neqE_nat mult_nat_less_add_less order_less_asym) 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<n ∨ length ms = length ns ∧ m=n ∧ omega_sum ms < omega_sum ns" by (smt (verit) assms length_Cons less_eq_Suc_le less_le_not_le nat_less_le normal_Cons not_le omega_sum_length_less omega_sum_less_eqlen_iff_cases) 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'<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_ω) then show thesis by (metis normal_drop omega_sum_drop that) qed definition Cantor_ωω :: "V ⇒ nat list" where "Cantor_ωω ≡ λx. SOME ns. x = omega_sum ns ∧ normal ns" lemma assumes "γ ∈ elts (ω↑ω)" shows Cantor_ωω: "omega_sum (Cantor_ωω γ) = γ" and normal_Cantor_ωω: "normal (Cantor_ωω γ)" by (metis (mono_tags, lifting) Cantor_ωω_def assms omega_sum_ωω someI)+ subsection ‹Larson's set $W(n)$› definition WW :: "nat list set" where "WW ≡ {l. strict_sorted l}" fun into_WW :: "nat ⇒ nat list ⇒ nat list" where "into_WW k [] = []" | "into_WW k (n#ns) = (k+n) # into_WW (Suc (k+n)) ns" fun from_WW :: "nat ⇒ nat list ⇒ nat list" where "from_WW k [] = []" | "from_WW k (n#ns) = (n - k) # from_WW (Suc n) ns" lemma from_into_WW [simp]: "from_WW k (into_WW k ns) = ns" by (induction ns arbitrary: k) auto lemma inj_into_WW: "inj (into_WW k)" by (metis from_into_WW injI) lemma into_from_WW_aux: "⟦strict_sorted ns; ∀n∈list.set ns. k ≤ n⟧ ⟹ into_WW k (from_WW k ns) = ns" by (induction ns arbitrary: k) (auto simp: Suc_leI) lemma into_from_WW [simp]: "strict_sorted ns ⟹ into_WW 0 (from_WW 0 ns) = ns" by (simp add: into_from_WW_aux) lemma into_WW_imp_ge: "y ∈ List.set (into_WW x ns) ⟹ x ≤ y" by (induction ns arbitrary: x) fastforce+ lemma strict_sorted_into_WW: "strict_sorted (into_WW x ns)" by (induction ns arbitrary: x) (auto simp: dest: into_WW_imp_ge) lemma length_into_WW: "length (into_WW x ns) = length ns" by (induction ns arbitrary: x) auto lemma WW_eq_range_into: "WW = range (into_WW 0)" proof - have "⋀ns. strict_sorted ns ⟹ ns ∈ range (into_WW 0)" by (metis into_from_WW rangeI) then show ?thesis by (auto simp: WW_def strict_sorted_into_WW) qed lemma into_WW_lenlex_iff: "(into_WW k ms, into_WW k ns) ∈ lenlex less_than ⟷ (ms, ns) ∈ lenlex less_than" proof (induction ms arbitrary: ns k) case Nil then show ?case by simp (metis length_0_conv length_into_WW) next case (Cons m ms) then show ?case by (induction ns) (auto simp: Cons_lenlex_iff length_into_WW) qed lemma wf_llt [simp]: "wf (lenlex less_than)" and trans_llt [simp]: "trans (lenlex less_than)" by blast+ lemma total_llt [simp]: "total_on A (lenlex less_than)" by (meson UNIV_I total_lenlex total_less_than total_on_def) lemma omega_sum_1_less: assumes "(ms,ns) ∈ lenlex less_than" shows "omega_sum (1#ms) < omega_sum (1#ns)" proof - have "omega_sum (1#ms) < omega_sum (1#ns)" if "length ms < length ns" using omega_sum_less_iff_cases that zero_less_one by blast then show ?thesis using assms by (auto simp: mult_succ simp flip: omega_sum_less_iff) qed lemma ordertype_WW_1: "ordertype WW (lenlex less_than) ≤ ordertype UNIV (lenlex less_than)" by (rule ordertype_mono) auto lemma ordertype_WW_2: "ordertype UNIV (lenlex less_than) ≤ ω↑ω" proof (rule ordertype_inc_le_Ord) show "range (λms. omega_sum (1#ms)) ⊆ elts (ω↑ω)" by (meson Ord_ω Ord_mem_iff_lt Ord_oexp Ord_omega_sum image_subset_iff omega_sum_less_ωω) qed (use omega_sum_1_less in auto) lemma ordertype_WW_3: "ω↑ω ≤ ordertype WW (lenlex less_than)" proof - define π where "π ≡ into_WW 0 ∘ Cantor_ωω" have ωω: "ω↑ω = tp (elts (ω↑ω))" by simp also have "… ≤ ordertype WW (lenlex less_than)" proof (rule ordertype_inc_le) fix α β assume α: "α ∈ elts (ω↑ω)" and β: "β ∈ elts (ω↑ω)" and "(α, β) ∈ VWF" then obtain *: "Ord α" "Ord β" "α<β" by (metis Ord_in_Ord Ord_ordertype VWF_iff_Ord_less ωω) then have "length (Cantor_ωω α) ≤ length (Cantor_ωω β)" using α β by (simp add: Cantor_ωω normal_Cantor_ωω omega_sum_length_leD) with α β * have "(Cantor_ωω α, Cantor_ωω β) ∈ lenlex less_than" by (auto simp: Cantor_ωω simp flip: omega_sum_less_iff) then show "(π α, π β) ∈ lenlex less_than" by (simp add: π_def into_WW_lenlex_iff) qed (auto simp: π_def WW_def strict_sorted_into_WW) finally show "ω↑ω ≤ ordertype WW (lenlex less_than)" . qed lemma ordertype_WW: "ordertype WW (lenlex less_than) = ω↑ω" and ordertype_UNIV_ωω: "ordertype UNIV (lenlex less_than) = ω↑ω" using ordertype_WW_1 ordertype_WW_2 ordertype_WW_3 by auto lemma ordertype_ωω: fixes F :: "nat ⇒ nat list set" assumes "⋀j::nat. ordertype (F j) (lenlex less_than) = ω↑j" shows "ordertype (⋃j. F j) (lenlex less_than) = ω↑ω" proof (rule antisym) show "ordertype (⋃ (range F)) (lenlex less_than) ≤ ω ↑ ω" by (metis ordertype_UNIV_ωω ordertype_mono small top_greatest trans_llt wf_llt) have "⋀n. ω ↑ ord_of_nat n ≤ ordertype (⋃ (range F)) (lenlex less_than)" by (metis TC_small Union_upper assms ordertype_mono rangeI trans_llt wf_llt) then show "ω ↑ ω ≤ ordertype (⋃ (range F)) (lenlex less_than)" by (auto simp: oexp_ω_Limit ZFC_in_HOL.SUP_le_iff elts_ω) qed definition WW_seg :: "nat ⇒ nat list set" where "WW_seg n ≡ {l ∈ WW. length l = n}" lemma WW_seg_subset_WW: "WW_seg n ⊆ WW" by (auto simp: WW_seg_def) lemma WW_eq_UN_WW_seg: "WW = (⋃ n. WW_seg n)" by (auto simp: WW_seg_def) lemma ordertype_list_seg: "ordertype {l. length l = n} (lenlex less_than) = ω↑n" proof - have "bij_betw omega_sum {l. length l = n} (elts (ω↑n))" unfolding WW_seg_def bij_betw_def by (auto simp: inj_omega_sum Ord_mem_iff_lt omega_sum_less dest: Ex_omega_sum) then show ?thesis by (force simp: ordertype_eq_iff simp flip: eq_omega_sum_less_iff) qed lemma ordertype_WW_seg: "ordertype (WW_seg n) (lenlex less_than) = ω↑n" (is "ordertype ?W ?R = ω↑n") proof - have "ordertype {l. length l = n} ?R = ordertype ?W ?R" proof (subst ordertype_eq_ordertype) show "∃f. bij_betw f {l. length l = n} ?W ∧ (∀x∈{l. length l = n}. ∀y∈{l. length l = n}. ((f x, f y) ∈ lenlex less_than) = ((x, y) ∈ lenlex less_than))" proof (intro exI conjI) have "inj_on (into_WW 0) {l. length l = n}" by (metis from_into_WW inj_onI) then show "bij_betw (into_WW 0) {l. length l = n} ?W" by (auto simp: bij_betw_def WW_seg_def WW_eq_range_into length_into_WW) qed (simp add: into_WW_lenlex_iff) qed auto then show ?thesis using ordertype_list_seg by auto qed subsection ‹Definitions required for the lemmas› subsubsection ‹Larson's "$<$"-relation on ordered lists› instantiation list :: (ord)ord begin definition "xs < ys ≡ xs ≠ [] ∧ ys ≠ [] ⟶ last xs < hd ys" for xs ys :: "'a list" definition "xs ≤ ys ≡ xs < ys ∨ xs = ys" for xs ys :: "'a list" instance by standard end lemma less_Nil [simp]: "xs < []" "[] < xs" by (auto simp: less_list_def) lemma less_sets_imp_list_less: assumes "list.set xs ≪ list.set ys" shows "xs < ys" by (metis assms last_in_set less_list_def less_sets_def list.set_sel(1)) lemma less_sets_imp_sorted_list_of_set: assumes "A ≪ B" "finite A" "finite B" shows "list_of A < list_of B" by (simp add: assms less_sets_imp_list_less) lemma sorted_list_of_set_imp_less_sets: assumes "xs < ys" "sorted xs" "sorted ys" shows "list.set xs ≪ list.set ys" using assms sorted_hd_le sorted_le_last by (force simp: less_list_def less_sets_def intro: order.trans) lemma less_list_iff_less_sets: assumes "sorted xs" "sorted ys" shows "xs < ys ⟷ list.set xs ≪ list.set ys" using assms sorted_hd_le sorted_le_last by (force simp: less_list_def less_sets_def intro: order.trans) lemma strict_sorted_append_iff: "strict_sorted (xs @ ys) ⟷ xs < ys ∧ strict_sorted xs ∧ strict_sorted ys" by (metis less_list_iff_less_sets less_setsD sorted_wrt_append strict_sorted_imp_less_sets strict_sorted_imp_sorted) lemma singleton_less_list_iff: "sorted xs ⟹ [n] < xs ⟷ {..n} ∩ list.set xs = {}" apply (simp add: less_list_def disjoint_iff) by (metis empty_iff less_le_trans list.set(1) list.set_sel(1) not_le sorted_hd_le) lemma less_hd_imp_less: "xs < [hd ys] ⟹ xs < ys" by (simp add: less_list_def) lemma strict_sorted_concat_I: assumes "⋀x. x ∈ list.set xs ⟹ strict_sorted x" "⋀n. Suc n < length xs ⟹ xs!n < xs!Suc n" "xs ∈ lists (- {[]})" shows "strict_sorted (concat xs)" using assms proof (induction xs) case (Cons x xs) then have "x < concat xs" apply (simp add: less_list_def) by (metis Compl_iff hd_concat insertI1 length_greater_0_conv length_pos_if_in_set list.sel(1) lists.cases nth_Cons_0) with Cons show ?case by (force simp: strict_sorted_append_iff) qed auto subsection ‹Nash Williams for lists› subsubsection ‹Thin sets of lists› inductive initial_segment :: "'a list ⇒ 'a list ⇒ bool" where "initial_segment xs (xs@ys)" definition thin :: "'a list set ⇒ bool" where "thin A ≡ ¬ (∃x y. x ∈ A ∧ y ∈ A ∧ x ≠ y ∧ initial_segment x y)" lemma initial_segment_ne: assumes "initial_segment xs ys" "xs ≠ []" shows "ys ≠ [] ∧ hd ys = hd xs" using assms by (auto elim!: initial_segment.cases) lemma take_initial_segment: assumes "initial_segment xs ys" "k ≤ length xs" shows "take k xs = take k ys" by (metis append_eq_conv_conj assms initial_segment.cases min_def take_take) lemma initial_segment_length_eq: assumes "initial_segment xs ys" "length xs = length ys" shows "xs = ys" using assms initial_segment.cases by fastforce lemma initial_segment_Nil [simp]: "initial_segment [] ys" by (simp add: initial_segment.simps) lemma initial_segment_Cons [simp]: "initial_segment (x#xs) (y#ys) ⟷ x=y ∧ initial_segment xs ys" by (metis append_Cons initial_segment.simps list.inject) lemma init_segment_iff_initial_segment: assumes "strict_sorted xs" "strict_sorted ys" shows "init_segment (list.set xs) (list.set ys) ⟷ initial_segment xs ys" (is "?lhs = ?rhs") proof assume ?lhs then obtain S' where S': "list.set ys = list.set xs ∪ S'" "list.set xs ≪ S'" by (auto simp: init_segment_def) then have "finite S'" by (metis List.finite_set finite_Un) have "ys = xs @ list_of S'" using S' ‹strict_sorted xs› proof (induction xs) case Nil with ‹strict_sorted ys› show ?case by auto next case (Cons a xs) with ‹finite S'› have "ys = a # xs @ list_of S'" by (metis List.finite_set append_Cons assms(2) sorted_list_of_set_Un sorted_list_of_set_set_of) then show ?case by (auto simp: Cons) qed then show ?rhs using initial_segment.intros by blast next assume ?rhs then show ?lhs proof cases case (1 ys) with assms show ?thesis by (simp add: init_segment_Un strict_sorted_imp_less_sets) qed qed theorem Nash_Williams_WW: fixes h :: "nat list ⇒ nat" assumes "infinite M" and h: "h ` {l ∈ A. List.set l ⊆ M} ⊆ {..<2}" and "thin A" "A ⊆ WW" obtains i N where "i < 2" "infinite N" "N ⊆ M" "h ` {l ∈ A. List.set l ⊆ N} ⊆ {i}" proof - define AM where "AM ≡ {l ∈ A. List.set l ⊆ M}" have "thin_set (list.set ` A)" using ‹thin A› ‹A ⊆ WW› unfolding thin_def thin_set_def WW_def by (auto simp: subset_iff init_segment_iff_initial_segment) then have "thin_set (list.set ` AM)" by (simp add: AM_def image_subset_iff thin_set_def) then have "Ramsey (list.set ` AM) 2" using Nash_Williams_2 by metis moreover have "(h ∘ list_of) ∈ list.set ` AM → {..<2}" unfolding AM_def proof clarsimp fix l assume "l ∈ A" "list.set l ⊆ M" then have "strict_sorted l" using WW_def ‹A ⊆ WW› by blast then show "h (list_of (list.set l)) < 2" using h ‹l ∈ A› ‹list.set l ⊆ M› by auto qed ultimately obtain N i where N: "N ⊆ M" "infinite N" "i<2" and "list.set ` AM ∩ Pow N ⊆ (h ∘ list_of) -` {i}" unfolding Ramsey_eq by (metis ‹infinite M›) then have N_disjoint: "(h ∘ list_of) -` {1-i} ∩ (list.set ` AM) ∩ Pow N = {}" unfolding subset_vimage_iff less_2_cases_iff by force have "h ` {l ∈ A. list.set l ⊆ N} ⊆ {i}" proof clarify fix l assume "l ∈ A" and "list.set l ⊆ N" then have "h l < 2" using h ‹N ⊆ M› by force with ‹i<2› have "h l ≠ Suc 0 - i ⟹ h l = i" by (auto simp: eval_nat_numeral less_Suc_eq) moreover have "strict_sorted l" using ‹A ⊆ WW› ‹l ∈ A› unfolding WW_def by blast moreover have "h (list_of (list.set l)) = 1 - i ⟶ ¬ (list.set l ⊆ N)" using N_disjoint ‹N ⊆ M› ‹l ∈ A› by (auto simp: AM_def) ultimately show "h l = i" using N ‹N ⊆ M› ‹l ∈ A› ‹list.set l ⊆ N› by (auto simp: vimage_def set_eq_iff AM_def WW_def subset_iff) qed then show thesis using that ‹i<2› N by auto qed subsection ‹Specialised functions on lists› lemma mem_lists_non_Nil: "xss ∈ lists (- {[]}) ⟷ (∀x ∈ list.set xss. x ≠ [])" by auto fun acc_lengths :: "nat ⇒ 'a list list ⇒ nat list" where "acc_lengths acc [] = []" | "acc_lengths acc (l#ls) = (acc + length l) # acc_lengths (acc + length l) ls" lemma length_acc_lengths [simp]: "length (acc_lengths acc ls) = length ls" by (induction ls arbitrary: acc) auto lemma acc_lengths_eq_Nil_iff [simp]: "acc_lengths acc ls = [] ⟷ ls = []" by (metis length_0_conv length_acc_lengths) lemma set_acc_lengths: assumes "ls ∈ lists (- {[]})" shows "list.set (acc_lengths acc ls) ⊆ {acc<..}" using assms by (induction ls rule: acc_lengths.induct) fastforce+ text ‹Useful because @{text acc_lengths.simps} will sometimes be deleted from the simpset.› lemma hd_acc_lengths [simp]: "hd (acc_lengths acc (l#ls)) = acc + length l" by simp lemma last_acc_lengths [simp]: "ls ≠ [] ⟹ last (acc_lengths acc ls) = acc + sum_list (map length ls)" by (induction acc ls rule: acc_lengths.induct) auto lemma nth_acc_lengths [simp]: "⟦ls ≠ []; k < length ls⟧ ⟹ acc_lengths acc ls ! k = acc + sum_list (map length (take (Suc k) ls))" by (induction acc ls arbitrary: k rule: acc_lengths.induct) (fastforce simp: less_Suc_eq nth_Cons')+ lemma acc_lengths_plus: "acc_lengths (m+n) as = map ((+)m) (acc_lengths n as)" by (induction n as arbitrary: m rule: acc_lengths.induct) (auto simp: add.assoc) lemma acc_lengths_shift: "NO_MATCH 0 acc ⟹ acc_lengths acc as = map ((+)acc) (acc_lengths 0 as)" by (metis acc_lengths_plus add.comm_neutral) lemma length_concat_acc_lengths: "ls ≠ [] ⟹ k + length (concat ls) ∈ list.set (acc_lengths k ls)" by (metis acc_lengths_eq_Nil_iff last_acc_lengths last_in_set length_concat) lemma strict_sorted_acc_lengths: assumes "ls ∈ lists (- {[]})" shows "strict_sorted (acc_lengths acc ls)" using assms proof (induction ls rule: acc_lengths.induct) case (2 acc l ls) then have "strict_sorted (acc_lengths (acc + length l) ls)" by auto then show ?case using set_acc_lengths "2.prems" by auto qed auto lemma acc_lengths_append: "acc_lengths acc (xs @ ys) = acc_lengths acc xs @ acc_lengths (acc + sum_list (map length xs)) ys" by (induction acc xs rule: acc_lengths.induct) (auto simp: add.assoc) lemma length_concat_ge: assumes "as ∈ lists (- {[]})" shows "length (concat as) ≥ length as" using assms proof (induction as) case (Cons a as) then have "length a ≥ Suc 0" "⋀l. l ∈ list.set as ⟹ length l ≥ Suc 0" by (auto simp: Suc_leI) then show ?case using Cons.IH by force qed auto fun interact :: "'a list list ⇒ 'a list list ⇒ 'a list" where "interact [] ys = concat ys" | "interact xs [] = concat xs" | "interact (x#xs) (y#ys) = x @ y @ interact xs ys" lemma (in monoid_add) length_interact: "length (interact xs ys) = sum_list (map length xs) + sum_list (map length ys)" by (induction rule: interact.induct) (auto simp: length_concat) lemma length_interact_ge: assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})" shows "length (interact xs ys) ≥ length xs + length ys" by (metis add_mono assms length_concat length_concat_ge length_interact) lemma set_interact [simp]: shows "list.set (interact xs ys) = list.set (concat xs) ∪ list.set (concat ys)" by (induction rule: interact.induct) auto lemma interact_eq_Nil_iff [simp]: assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})" shows "interact xs ys = [] ⟷ xs=[] ∧ ys=[]" using length_interact_ge [OF assms] by fastforce lemma interact_sing [simp]: "interact [x] ys = x @ concat ys" by (metis (no_types) concat.simps(2) interact.simps neq_Nil_conv) lemma hd_interact: "⟦xs ≠ []; hd xs ≠ []⟧ ⟹ hd (interact xs ys) = hd (hd xs)" by (smt (verit, best) hd_append2 hd_concat interact.elims list.sel(1)) lemma acc_lengths_concat_injective: assumes "concat as' = concat as" "acc_lengths n as' = acc_lengths n as" shows "as' = as" using assms proof (induction as arbitrary: n as') case Nil then show ?case by (metis acc_lengths_eq_Nil_iff) next case (Cons a as) then obtain a' bs where "as' = a'#bs" by (metis Suc_length_conv length_acc_lengths) with Cons show ?case by simp qed lemma acc_lengths_interact_injective: assumes "interact as' bs' = interact as bs" "acc_lengths a as' = acc_lengths a as" "acc_lengths b bs' = acc_lengths b bs" shows "as' = as ∧ bs' = bs" using assms proof (induction as bs arbitrary: a b as' bs' rule: interact.induct) case (1 cs) then show ?case by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(1)) next case (2 c cs) then show ?case by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(2) list.exhaust) next case (3 x xs y ys) then obtain a' us b' vs where "as' = a'#us" "bs' = b'#vs" by (metis length_Suc_conv length_acc_lengths) with 3 show ?case by auto qed lemma strict_sorted_interact_I: assumes "length ys ≤ length xs" "length xs ≤ Suc (length ys)" "⋀x. x ∈ list.set xs ⟹ strict_sorted x" "⋀y. y ∈ list.set ys ⟹ strict_sorted y" "⋀n. n < length ys ⟹ xs!n < ys!n" "⋀n. Suc n < length xs ⟹ ys!n < xs!Suc n" assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})" shows "strict_sorted (interact xs ys)" using assms proof (induction rule: interact.induct) case (3 x xs y ys) then have "x < y" by force moreover have "strict_sorted (interact xs ys)" using 3 by simp (metis Suc_less_eq nth_Cons_Suc) moreover have "y < interact xs ys" using 3 apply (simp add: less_list_def) by (metis hd_interact le_zero_eq length_greater_0_conv list.sel(1) list.set_sel(1) list.size(3) lists.simps mem_lists_non_Nil nth_Cons_0) ultimately show ?case using 3 by (simp add: strict_sorted_append_iff less_list_def) qed auto subsection ‹Forms and interactions› subsubsection ‹Forms› inductive Form_Body :: "[nat, nat, nat list, nat list, nat list] ⇒ bool" where "Form_Body ka kb xs ys zs" if "length xs < length ys" "xs = concat (a#as)" "ys = concat (b#bs)" "a#as ∈ lists (- {[]})" "b#bs ∈ lists (- {[]})" "length (a#as) = ka" "length (b#bs) = kb" "c = acc_lengths 0 (a#as)" "d = acc_lengths 0 (b#bs)" "zs = concat [c, a, d, b] @ interact as bs" "strict_sorted zs" inductive Form :: "[nat, nat list set] ⇒ bool" where "Form 0 {xs,ys}" if "length xs = length ys" "xs ≠ ys" | "Form (2*k-1) {xs,ys}" if "Form_Body k k xs ys zs" "k > 0" | "Form (2*k) {xs,ys}" if "Form_Body (Suc k) k xs ys zs" "k > 0" inductive_cases Form_0_cases_raw: "Form 0 u" lemma Form_elim_upair: assumes "Form l U" obtains xs ys where "xs ≠ ys" "U = {xs,ys}" "length xs ≤ length ys" using assms by (smt (verit, best) Form.simps Form_Body.cases less_or_eq_imp_le nat_neq_iff) lemma assumes "Form_Body ka kb xs ys zs" shows Form_Body_WW: "zs ∈ WW" and Form_Body_nonempty: "length zs > 0" and Form_Body_length: "length xs < length ys" using Form_Body.cases [OF assms] by (fastforce simp: WW_def)+ lemma form_cases: fixes l::nat obtains (zero) "l = 0" | (nz) ka kb where "l = ka+kb - 1" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb" proof - have "l = 0 ∨ (∃ka kb. l = ka+kb - 1 ∧ 0 < kb ∧ kb ≤ ka ∧ ka ≤ Suc kb)" by presburger then show thesis using nz zero by blast qed subsubsection ‹Interactions› lemma interact: assumes "Form l U" "l>0" obtains ka kb xs ys zs where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys zs" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb" using assms unfolding Form.simps by (smt (verit, best) add_Suc diff_Suc_1 lessI mult_2 nat_less_le order_refl) definition inter_scheme :: "nat ⇒ nat list set ⇒ nat list" where "inter_scheme l U ≡ SOME zs. ∃k xs ys. U = {xs,ys} ∧ (l = 2*k-1 ∧ Form_Body k k xs ys zs ∨ l = 2*k ∧ Form_Body (Suc k) k xs ys zs)" lemma inter_scheme: assumes "Form l U" "l>0" obtains ka kb xs ys where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys (inter_scheme l U)" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb" using interact [OF ‹Form l U›] proof cases case (2 ka kb xs ys zs) then have §: "⋀ka kb zs. ¬ Form_Body ka kb ys xs zs" using Form_Body_length less_asym' by blast have "Form_Body ka kb xs ys (inter_scheme l U)" proof (cases "ka = kb") case True with 2 have l: "∀k. l ≠ k * 2" by presburger have [simp]: "⋀k. kb + kb - Suc 0 = k * 2 - Suc 0 ⟷ k=kb" by auto show ?thesis unfolding inter_scheme_def using 2 l True by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex) next case False with 2 have l: "∀k. l ≠ k * 2 - Suc 0" and [simp]: "ka = Suc kb" by presburger+ have [simp]: "⋀k. kb + kb = k * 2 ⟷ k=kb" by auto show ?thesis unfolding inter_scheme_def using 2 l False by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex) qed then show ?thesis by (simp add: 2 that) qed (use ‹l > 0› in auto) lemma inter_scheme_strict_sorted: assumes "Form l U" "l>0" shows "strict_sorted (inter_scheme l U)" using Form_Body.simps assms inter_scheme by fastforce lemma inter_scheme_simple: assumes "Form l U" "l>0" shows "inter_scheme l U ∈ WW ∧ length (inter_scheme l U) > 0" using inter_scheme [OF assms] by (meson Form_Body_WW Form_Body_nonempty) subsubsection ‹Injectivity of interactions› proposition inter_scheme_injective: assumes "Form l U" "Form l U'" "l > 0" and eq: "inter_scheme l U' = inter_scheme l U" shows "U' = U" proof - obtain ka kb xs ys where l: "l = ka+kb - 1" and U: "U = {xs,ys}" and FB: "Form_Body ka kb xs ys (inter_scheme l U)" and kb: "0 < kb" "kb ≤ ka" "ka ≤ Suc kb" using assms inter_scheme by blast then obtain a as b bs c d where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)" and len: "length (a#as) = ka" "length (b#bs) = kb" and c: "c = acc_lengths 0 (a#as)" and d: "d = acc_lengths 0 (b#bs)" and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs" by (auto simp: Form_Body.simps) obtain ka' kb' xs' ys' where l': "l = ka'+kb' - 1" and U': "U' = {xs',ys'}" and FB': "Form_Body ka' kb' xs' ys' (inter_scheme l U')" and kb': "0 < kb'" "kb' ≤ ka'" "ka' ≤ Suc kb'" using assms inter_scheme by blast then obtain a' as' b' bs' c' d' where xs': "xs' = concat (a'#as')" and ys': "ys' = concat (b'#bs')" and len': "length (a'#as') = ka'" "length (b'#bs') = kb'" and c': "c' = acc_lengths 0 (a'#as')" and d': "d' = acc_lengths 0 (b'#bs')" and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'" using Form_Body.simps by auto have [simp]: "ka' = ka ∧ kb' = kb" using ‹l > 0› l l' kb kb' le_SucE le_antisym mult_2 by linarith have [simp]: "length c = length c'" "length d = length d'" using c c' d d' len' len by auto have c_off: "c' = c" "a' @ d' @ b' @ interact as' bs' = a @ d @ b @ interact as bs" using eq by (auto simp: Ueq Ueq') then have len_a: "length a' = length a" by (metis acc_lengths.simps(2) add.left_neutral c c' nth_Cons_0) with c_off have §: "a' = a" "d' = d" "b' @ interact as' bs' = b @ interact as bs" by auto then have "length (interact as' bs') = length (interact as bs)" by (metis acc_lengths.simps(2) add_left_cancel append_eq_append_conv d d' list.inject) with § have "b' = b" "interact as' bs' = interact as bs" by auto moreover have "acc_lengths 0 as' = acc_lengths 0 as" using ‹a' = a› ‹c' = c› by (simp add: c' c acc_lengths_shift) moreover have "acc_lengths 0 bs' = acc_lengths 0 bs" using ‹b' = b› ‹d' = d› by (simp add: d' d acc_lengths_shift) ultimately have "as' = as ∧ bs' = bs" using acc_lengths_interact_injective by blast then show ?thesis by (simp add: ‹a' = a› U U' ‹b' = b› xs xs' ys ys') qed lemma strict_sorted_interact_imp_concat: "strict_sorted (interact as bs) ⟹ strict_sorted (concat as) ∧ strict_sorted (concat bs)" proof (induction as bs rule: interact.induct) case (3 x xs y ys) have "x < concat xs" using "3.prems" by (smt (verit, del_insts) Un_iff hd_in_set interact.simps(3) last_in_set less_list_def set_append set_interact sorted_wrt_append) moreover have "y < concat ys" using 3 sorted_wrt_append strict_sorted_append_iff by fastforce ultimately show ?case using 3 by (auto simp add: strict_sorted_append_iff) qed auto lemma strict_sorted_interact_hd: "⟦strict_sorted (interact cs ds); cs ≠ []; ds ≠ []; hd cs ≠ []; hd ds ≠ []⟧ ⟹ hd (hd cs) < hd (hd ds)" by (metis append_is_Nil_conv hd_append2 hd_in_set interact.simps(3) list.exhaust_sel sorted_wrt_append) text ‹the lengths of the two lists can differ by one› proposition interaction_scheme_unique_aux: assumes "concat as = concat as'" and ys': "concat bs = concat bs'" and "as ∈ lists (- {[]})" "bs ∈ lists (- {[]})" and "strict_sorted (interact as bs)" and "length bs ≤ length as" "length as ≤ Suc (length bs)" and "as' ∈ lists (- {[]})" "bs' ∈ lists (- {[]})" and "strict_sorted (interact as' bs')" and "length bs' ≤ length as'" "length as' ≤ Suc (length bs')" and "length as = length as'" "length bs = length bs'" shows "as = as' ∧ bs = bs'" using assms proof (induction "length as" arbitrary: as bs as' bs') case 0 then show ?case by auto next case SUC: (Suc k) show ?case proof (cases k) case 0 with SUC obtain a a' where aa': "as = [a]" "as' = [a']" by (metis Suc_length_conv length_0_conv) show ?thesis proof show "as = as'" using aa' ‹concat as = concat as'› by force with SUC 0 show "bs = bs'" by (metis Suc_leI append_Nil2 concat.simps impossible_Cons le_antisym length_greater_0_conv list.exhaust) qed next case (Suc k') then obtain a cs b ds where eq: "as = a#cs" "bs = b#ds" using SUC by (metis le0 list.exhaust list.size(3) not_less_eq_eq) have "length as' ≠ 0" using SUC 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 by auto case (Suc k') obtain [simp]: "b ≠ []" "b' ≠ []" "a ≠ []" "a' ≠ []" using SUC by (simp add: eq eq') then have "hd b' = hd b" using SUC 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 sw_ab: "strict_sorted (a @ b @ interact cs ds)" by (metis SUC.prems(5) eq interact.simps(3)) then obtain "a < b" "strict_sorted a" "strict_sorted b" by (metis append_assoc strict_sorted_append_iff) have b_cs: "strict_sorted (concat (b # cs))" by (metis append.simps(1) concat.simps(2) interact.simps(3) strict_sorted_interact_imp_concat sw_ab) then have "b < concat cs" using strict_sorted_append_iff by auto have "strict_sorted (a @ concat cs)" using eq(1) ss_ab(1) by force 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 sw_ab': "strict_sorted (a' @ b' @ interact cs' ds')" by (metis SUC.prems(10) eq' interact.simps(3)) then obtain "a' < b'" "strict_sorted a'" "strict_sorted b'" by (metis append_assoc strict_sorted_append_iff) have b_cs': "strict_sorted (concat (b' # cs'))" by (metis (no_types) SUC.prems(10) append_Nil eq' interact.simps(3) strict_sorted_append_iff strict_sorted_interact_imp_concat) then have "b' < concat cs'" by (simp add: strict_sorted_append_iff) then have "hd b' ∉ list.set (concat cs')" by (metis Un_iff ‹b' ≠ []› list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append 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 (simp add: SUC.prems(1) ‹hd b' = hd b› ‹strict_sorted a'› ‹strict_sorted a› strict_sorted_equal) moreover have ccat_cs_cs': "concat cs = concat cs'" using SUC.prems(1) ‹a = a'› eq'(1) eq(1) by fastforce have "b=b'" proof (cases "ds = [] ∨ ds' = []") case True then show ?thesis using SUC eq'(2) eq(2) by fastforce next case False then have "ds ≠ []" "ds' ≠ []" "sorted (concat ds)" "sorted (concat ds')" using eq(2) ss_ab(2) eq'(2) ss_ab'(2) strict_sorted_append_iff strict_sorted_imp_sorted by auto have "strict_sorted b" "strict_sorted b'" using b_cs b_cs' sorted_wrt_append by auto moreover have "cs ≠ []" using k local.Suc by auto then obtain "hd cs ≠ []" "hd ds ≠ []" using SUC.prems(3) SUC.prems(4) eq list.set_sel(1) by (simp add: ‹ds ≠ []› mem_lists_non_Nil) then have "concat cs ≠ []" using ‹cs ≠ []› hd_in_set by auto have "hd (concat cs) < hd (concat ds)" using strict_sorted_interact_hd by (metis ‹cs ≠ []› ‹ds ≠ []› ‹hd cs ≠ []› ‹hd ds ≠ []› hd_concat sorted_wrt_append sw_ab) have "list.set b = list.set (concat bs) ∩ {..< hd (concat cs)}" proof - have 1: "x ∈ list.set b" if "x < hd (concat cs)" and "l ∈ list.set ds" and "x ∈ list.set l" for x l using ‹hd (concat cs) < hd (concat ds)› ‹sorted (concat ds)› sorted_hd_le that by fastforce have 2: "l < hd (concat cs)" if "l ∈ list.set b" for l by (metis ‹concat cs ≠ []› b_cs concat.simps(2) list.set_sel(1) sorted_wrt_append that) show ?thesis using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq) qed moreover have "cs' ≠ []" using k 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 sorted_wrt_append sw_ab') have "list.set b' = list.set (concat bs') ∩ {..< hd (concat cs')}" proof - have 1: "x ∈ list.set b'" if "x < hd (concat cs')" and "l ∈ list.set ds'" and "x ∈ list.set l" for x l using ‹hd (concat cs') < hd (concat ds')› ‹sorted (concat ds')› sorted_hd_le that by fastforce have 2: "l < hd (concat cs')" if "l ∈ list.set b'" for l by (metis ‹concat cs' ≠ []› b_cs' list.set_sel(1) sorted_wrt_append that) show ?thesis using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq') qed ultimately show "b = b'" by (simp add: SUC.prems(2) ccat_cs_cs' strict_sorted_equal) qed moreover have "cs = cs' ∧ ds = ds'" proof (rule SUC.hyps) show "k = length cs" using eq SUC.hyps(2) by auto[1] show "concat ds = concat ds'" using SUC.prems(2) ‹b = b'› eq'(2) eq(2) by auto show "strict_sorted (interact cs ds)" using eq SUC.prems(5) strict_sorted_append_iff by auto show "length ds ≤ length cs" "length cs ≤ Suc (length ds)" using eq SUC 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 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) using assms ‹length xs < length ys› by (auto simp: True mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger) 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) using assms ‹length xs < length ys› by (auto simp: eq mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger) 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 ` {..<n}, 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} = enumerate N ` {..<n}" using assms by (auto simp: enumerate_in_set) with assms show ?thesis by (simp add: card_image grab_def strict_mono_enum strict_mono_imp_inj_on) qed lemma fst_grab_subset: "fst (grab N 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]⇗2⇖ → {0,1}" obtains N j where "infinite N" and "⋀k u. ⟦k > 0; u ∈ [WW]⇗2⇖; 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 - define FF where "FF ≡ {U ∈ [WW]⇗2⇖. Form l U}" define h where "h ≡ λzs. g (inv_into FF (inter_scheme l) zs)" have "thin (inter_scheme l ` FF)" using ‹l > 0› lemma_3_11 by (simp add: thin_def FF_def) moreover have "inter_scheme l ` FF ⊆ WW" using inter_scheme_simple ‹0 < l› FF_def by blast moreover have "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ M} ⊆ {..<2}" using g inv_into_into[of concl: "FF" "inter_scheme l"] by (force simp: h_def FF_def Pi_iff) ultimately obtain j N where "j < 2" "infinite N" "N ⊆ M" and hj: "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ N} ⊆ {j}" using ‹Φ m M› unfolding Φ_def by (blast intro: Nash_Williams_WW [of M]) let ?n = "Inf N" have "?n > m" using ‹Φ m M› ‹infinite N› unfolding Φ_def Inf_nat_def infinite_nat_iff_unbounded by (metis LeastI_ex ‹N ⊆ M› le_less_trans not_less not_less_Least subsetD) have "g U = j" if "Form l U" "U ⊆ WW" "[?n] < inter_scheme l U" "list.set (inter_scheme l U) ⊆ N - {?n}" for U 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) FF" using ‹0 < l› inj_on_def inter_scheme_injective FF_def by blast moreover have "g (inv_into FF (inter_scheme l) (inter_scheme l U)) = j" using hj that xys subset_Diff_insert by (fastforce simp: h_def FF_def image_iff) ultimately show ?thesis using that FF_def by auto qed moreover have "?n < Inf (N - {?n})" by (metis Diff_iff Inf_nat_def Inf_nat_def1 ‹infinite N› finite.emptyI infinite_remove linorder_neqE_nat not_less_Least singletonI) moreover have "?n ∈ M" by (metis Inf_nat_def1 ‹N ⊆ M› ‹infinite N› finite.emptyI 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