section ‹Ordinal Partitions› text ‹Material 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. Also from ``Partition Relations'' by A. Hajnal and J. A. Larson, in \emph{Handbook of Set Theory}, edited by Matthew Foreman and Akihiro Kanamori (Springer, 2010).› theory Partitions imports Library_Additions "ZFC_in_HOL.ZFC_Typeclasses" "ZFC_in_HOL.Cantor_NF" begin abbreviation tp :: "V set ⇒ V" where "tp A ≡ ordertype A VWF" subsection ‹Ordinal Partitions: Definitions› definition partn_lst :: "[('a × 'a) set, 'a set, V list, nat] ⇒ bool" where "partn_lst r B α n ≡ ∀f ∈ [B]⇗n⇖ → {..<length α}. ∃i < length α. ∃H. H ⊆ B ∧ ordertype H r = (α!i) ∧ f ` (nsets H n) ⊆ {i}" abbreviation partn_lst_VWF :: "V ⇒ V list ⇒ nat ⇒ bool" where "partn_lst_VWF β ≡ partn_lst VWF (elts β)" lemma partn_lst_E: assumes "partn_lst r B α n" "f ∈ nsets B n → {..<l}" "l = length α" obtains i H where "i < l" "H ⊆ B" "ordertype H r = α!i" "f ` (nsets H n) ⊆ {i}" using assms by (auto simp: partn_lst_def) lemma partn_lst_VWF_nontriv: assumes "partn_lst_VWF β α n" "l = length α" "Ord β" "l > 0" obtains i where "i < l" "α!i ≤ β" proof - have "{..<l} ≠ {}" by (simp add: ‹l > 0› lessThan_empty_iff) then obtain f where "f ∈ nsets (elts β) n → {..<l}" by (meson Pi_eq_empty equals0I) then obtain i H where "i < l" "H ⊆ elts β" and eq: "tp H = α!i" using assms by (metis partn_lst_E) then have "α!i ≤ β" by (metis ‹H ⊆ elts β› ‹Ord β› eq ordertype_le_Ord) then show thesis using ‹i < l› that by auto qed lemma partn_lst_triv0: assumes "α!i = 0" "i < length α" "n ≠ 0" shows "partn_lst r B α n" by (metis partn_lst_def assms bot_least image_empty nsets_empty_iff ordertype_empty) lemma partn_lst_triv1: assumes "α!i ≤ 1" "i < length α" "n > 1" "B ≠ {}" "wf r" shows "partn_lst r B α n" unfolding partn_lst_def proof clarsimp obtain γ where "γ ∈ B" "α ≠ []" using assms mem_0_Ord by fastforce have 01: "α!i = 0 ∨ α!i = 1" using assms by (fastforce simp: one_V_def) fix f assume f: "f ∈ [B]⇗n⇖ → {..<length α}" with assms have "ordertype {γ} r = 1 ∧ f ` [{γ}]⇗n⇖ ⊆ {i}" "ordertype {} r = 0 ∧ f ` [{}]⇗n⇖ ⊆ {i}" by (auto simp: one_V_def ordertype_insert nsets_eq_empty) with assms 01 show "∃i<length α. ∃H⊆B. ordertype H r = α ! i ∧ f ` [H]⇗n⇖ ⊆ {i}" using ‹γ ∈ B› by auto qed lemma partn_lst_two_swap: assumes "partn_lst r B [x,y] n" shows "partn_lst r B [y,x] n" proof - { fix f :: "'a set ⇒ nat" assume f: "f ∈ [B]⇗n⇖ → {..<2}" then have f': "(λi. 1 - i) ∘ f ∈ [B]⇗n⇖ → {..<2}" by (auto simp: Pi_def) obtain i H where "i<2" "H ⊆ B" "ordertype H r = ([x,y]!i)" "((λi. 1 - i) ∘ f) ` (nsets H n) ⊆ {i}" by (auto intro: partn_lst_E [OF assms f']) moreover have "f x = Suc 0" if "Suc 0 ≤ f x" "x∈[H]⇗n⇖" for x using f that ‹H ⊆ B› nsets_mono by (fastforce simp: Pi_iff) ultimately have "ordertype H r = [y,x] ! (1-i) ∧ f ` [H]⇗n⇖ ⊆ {1-i}" by (force simp: eval_nat_numeral less_Suc_eq) then have "∃i H. i<2 ∧ H⊆B ∧ ordertype H r = [y,x] ! i ∧ f ` [H]⇗n⇖ ⊆ {i}" by (metis Suc_1 ‹H ⊆ B› diff_less_Suc) } then show ?thesis by (auto simp: partn_lst_def eval_nat_numeral) qed lemma partn_lst_greater_resource: assumes M: "partn_lst r B α n" and "B ⊆ C" shows "partn_lst r C α n" proof (clarsimp simp: partn_lst_def) fix f assume "f ∈ [C]⇗n⇖ → {..<length α}" then have "f ∈ [B]⇗n⇖ → {..<length α}" by (metis ‹B ⊆ C› part_fn_def part_fn_subset) then obtain i H where "i < length α" and "H ⊆ B" "ordertype H r = (α!i)" and "f ` nsets H n ⊆ {i}" using M partn_lst_def by metis then show "∃i<length α. ∃H⊆C. ordertype H r = α ! i ∧ f ` [H]⇗n⇖ ⊆ {i}" using ‹B ⊆ C› by blast qed lemma partn_lst_less: assumes M: "partn_lst r B α n" and eq: "length α' = length α" and "List.set α' ⊆ ON" and le: "⋀i. i < length α ⟹ α'!i ≤ α!i " and r: "wf r" "trans r" "total_on B r" and "small B" shows "partn_lst r B α' n" proof (clarsimp simp: partn_lst_def) fix f assume "f ∈ [B]⇗n⇖ → {..<length α'}" then obtain i H where "i < length α" and "H ⊆ B" "small H" and H: "ordertype H r = (α!i)" and fi: "f ` nsets H n ⊆ {i}" using assms by (auto simp: partn_lst_def smaller_than_small) then have bij: "bij_betw (ordermap H r) H (elts (α!i))" using ordermap_bij [of r H] r by (smt ‹small B› in_mono smaller_than_small total_on_def) define H' where "H' = inv_into H (ordermap H r) ` (elts (α'!i))" have "H' ⊆ H" using bij ‹i < length α› bij_betw_imp_surj_on le by (force simp: H'_def image_subset_iff intro: inv_into_into) moreover have ot: "ordertype H' r = (α'!i)" proof (subst ordertype_eq_iff) show "Ord (α' ! i)" using assms by (simp add: ‹i < length α› subset_eq) show "small H'" by (simp add: H'_def) show "∃f. bij_betw f H' (elts (α' ! i)) ∧ (∀x∈H'. ∀y∈H'. (f x < f y) = ((x, y) ∈ r))" proof (intro exI conjI ballI) show "bij_betw (ordermap H r) H' (elts (α' ! i))" using ‹H' ⊆ H› by (metis H'_def ‹i < length α› bij bij_betw_inv_into_RIGHT bij_betw_subset le less_eq_V_def) show "(ordermap H r x < ordermap H r y) = ((x, y) ∈ r)" if "x ∈ H'" "y ∈ H'" for x y proof (intro iffI ordermap_mono_less) assume "ordermap H r x < ordermap H r y" then show "(x, y) ∈ r" by (metis ‹H ⊆ B› ‹small H› ‹H' ⊆ H› leD ordermap_mono_le r subsetD that total_on_def) qed (use assms that ‹H' ⊆ H› ‹small H› in auto) qed show "total_on H' r" using r by (meson ‹H ⊆ B› ‹H' ⊆ H› subsetD total_on_def) qed (use r in auto) ultimately show "∃i<length α'. ∃H⊆B. ordertype H r = α' ! i ∧ f ` [H]⇗n⇖ ⊆ {i}" using ‹H ⊆ B› ‹i < length α› fi assms by (metis image_mono nsets_mono subset_trans) qed text ‹Holds because no $n$-sets exist!› lemma partn_lst_VWF_degenerate: assumes "k < n" shows "partn_lst_VWF ω (ord_of_nat k # αs) n" proof (clarsimp simp: partn_lst_def) fix f :: "V set ⇒ nat" have "[elts (ord_of_nat k)]⇗n⇖ = {}" by (simp add: nsets_eq_empty assms finite_Ord_omega) then have "f ` [elts (ord_of_nat k)]⇗n⇖ ⊆ {0}" by auto then show "∃i < Suc (length αs). ∃H⊆elts ω. tp H = (ord_of_nat k # αs) ! i ∧ f ` [H]⇗n⇖ ⊆ {i}" using assms ordertype_eq_Ord [of "ord_of_nat k"] elts_ord_of_nat less_Suc_eq_0_disj by fastforce qed lemma partn_lst_VWF_ω_2: assumes "Ord α" shows "partn_lst_VWF (ω ↑ (1+α)) [2, ω ↑ (1+α)] 2" (is "partn_lst_VWF ?β _ _") proof (clarsimp simp: partn_lst_def) fix f assume f: "f ∈ [elts ?β]⇗2⇖ → {..<Suc (Suc 0)}" show "∃i<Suc (Suc 0). ∃H⊆elts ?β. tp H = [2, ?β] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}" proof (cases "∃x ∈ elts ?β. ∃y ∈ elts ?β. x ≠ y ∧ f{x,y} = 0") case True then obtain x y where "x ∈ elts ?β" "y ∈ elts ?β" "x ≠ y" "f {x, y} = 0" by auto then have "{x,y} ⊆ elts ?β" "tp {x,y} = 2" "f ` [{x, y}]⇗2⇖ ⊆ {0}" by auto (simp add: eval_nat_numeral ordertype_VWF_finite_nat) with ‹x ≠ y› show ?thesis by (metis nth_Cons_0 zero_less_Suc) next case False with f have "∀x∈elts ?β. ∀y∈elts ?β. x ≠ y ⟶ f {x, y} = 1" unfolding Pi_iff using lessThan_Suc by force then have "tp (elts ?β) = ?β" "f ` [elts ?β]⇗2⇖ ⊆ {Suc 0}" by (auto simp: assms nsets_2_eq) then show ?thesis by (metis lessI nth_Cons_0 nth_Cons_Suc subsetI) qed qed subsection ‹Relating partition properties on @{term VWF} to the general case› text ‹Two very similar proofs here!› lemma partn_lst_imp_partn_lst_VWF_eq: assumes part: "partn_lst r U α n" and β: "ordertype U r = β" and "small U" and r: "wf r" "trans r" "total_on U r" shows "partn_lst_VWF β α n" unfolding partn_lst_def proof clarsimp fix f assume f: "f ∈ [elts β]⇗n⇖ → {..<length α}" define cv where "cv ≡ λX. ordermap U r ` X" have bij: "bij_betw (ordermap U r) U (elts β)" using ordermap_bij [of "r" U] assms by blast then have bij_cv: "bij_betw cv ([U]⇗n⇖) ([elts β]⇗n⇖)" using bij_betw_nsets cv_def by blast then have func: "f ∘ cv ∈ [U]⇗n⇖ → {..<length α}" and "inj_on (ordermap U r) U" using bij bij_betw_def bij_betw_apply f by fastforce+ then have cv_part: "⟦∀x∈[X]⇗n⇖. f (cv x) = i; X ⊆ U; a ∈ [cv X]⇗n⇖⟧ ⟹ f a = i" for a X i n by (force simp: cv_def nsets_def subset_image_iff inj_on_subset finite_image_iff card_image) have ot_eq [simp]: "tp (cv X) = ordertype X r" if "X ⊆ U" for X unfolding cv_def by (meson ‹small U› ordertype_image_ordermap r that total_on_subset) obtain X i where "X ⊆ U" and X: "ordertype X r = α!i" "(f ∘ cv) ` [X]⇗n⇖ ⊆ {i}" and "i < length α" using part func by (auto simp: partn_lst_def) show "∃i < length α. ∃H⊆elts β. tp H = α!i ∧ f ` [H]⇗n⇖ ⊆ {i}" proof (intro exI conjI) show "i < length α" by (simp add: ‹i < length α›) show "cv X ⊆ elts β" using ‹X ⊆ U› bij bij_betw_imp_surj_on cv_def by blast show "tp (cv X) = α ! i" by (simp add: X(1) ‹X ⊆ U›) show "f ` [cv X]⇗n⇖ ⊆ {i}" using X ‹X ⊆ U› cv_part unfolding image_subset_iff cv_def by (metis comp_apply insertCI singletonD) qed qed lemma partn_lst_imp_partn_lst_VWF: assumes part: "partn_lst r U α n" and β: "ordertype U r ≤ β" "small U" and r: "wf r" "trans r" "total_on U r" shows "partn_lst_VWF β α n" by (metis assms less_eq_V_def partn_lst_imp_partn_lst_VWF_eq partn_lst_greater_resource) lemma partn_lst_VWF_imp_partn_lst_eq: assumes part: "partn_lst_VWF β α n" and β: "ordertype U r = β" "small U" and r: "wf r" "trans r" "total_on U r" shows "partn_lst r U α n" unfolding partn_lst_def proof clarsimp fix f assume f: "f ∈ [U]⇗n⇖ → {..<length α}" define cv where "cv ≡ λX. inv_into U (ordermap U r) ` X" have bij: "bij_betw (ordermap U r) U (elts β)" using ordermap_bij [of "r" U] assms by blast then have bij_cv: "bij_betw cv ([elts β]⇗n⇖) ([U]⇗n⇖)" using bij_betw_nsets bij_betw_inv_into unfolding cv_def by blast then have func: "f ∘ cv ∈ [elts β]⇗n⇖ → {..<length α}" using bij_betw_apply f by fastforce have "inj_on (ordermap U r) U" using bij bij_betw_def by blast then have cv_part: "⟦∀x∈[X]⇗n⇖. f (cv x) = i; X ⊆ elts β; a ∈ [cv X]⇗n⇖⟧ ⟹ f a = i" for a X i n by (metis bij bij_betw_imp_surj_on cv_def inj_on_inv_into nset_image_obtains) have ot_eq [simp]: "ordertype (cv X) r = tp X" if "X ⊆ elts β" for X unfolding cv_def proof (rule ordertype_inc_eq) show "small X" using down that by auto show "(inv_into U (ordermap U r) x, inv_into U (ordermap U r) y) ∈ r" if "x ∈ X" "y ∈ X" and "(x,y) ∈ VWF" for x y proof - have xy: "x ∈ ordermap U r ` U" "y ∈ ordermap U r ` U" using ‹X ⊆ elts β› ‹x ∈ X› ‹y ∈ X› bij bij_betw_imp_surj_on by blast+ then have eq: "ordermap U r (inv_into U (ordermap U r) x) = x" "ordermap U r (inv_into U (ordermap U r) y) = y" by (meson f_inv_into_f)+ then have "y ∉ elts x" by (metis (no_types) VWF_non_refl mem_imp_VWF that(3) trans_VWF trans_def) with r show ?thesis by (metis (no_types) VWF_non_refl xy eq assms(3) inv_into_into ordermap_mono that(3) total_on_def) qed qed (use r in auto) obtain X i where "X ⊆ elts β" and X: "tp X = α!i" "(f ∘ cv) ` [X]⇗n⇖ ⊆ {i}" and "i < length α" using part func by (auto simp: partn_lst_def) show "∃i < length α. ∃H⊆U. ordertype H r = α!i ∧ f ` [H]⇗n⇖ ⊆ {i}" proof (intro exI conjI) show "i < length α" by (simp add: ‹i < length α›) show "cv X ⊆ U" using ‹X ⊆ elts β› bij bij_betw_imp_surj_on bij_betw_inv_into cv_def by blast show "ordertype (cv X) r = α ! i" by (simp add: X(1) ‹X ⊆ elts β›) show "f ` [cv X]⇗n⇖ ⊆ {i}" using X ‹X ⊆ elts β› cv_part unfolding image_subset_iff cv_def by (metis comp_apply insertCI singletonD) qed qed corollary partn_lst_VWF_imp_partn_lst: assumes "partn_lst_VWF β α n" and β: "ordertype U r ≥ β" "small U" "wf r" "trans r" "total_on U r" shows "partn_lst r U α n" by (metis assms less_eq_V_def partn_lst_VWF_imp_partn_lst_eq partn_lst_greater_resource) subsection ‹Simple consequences of the definitions› text ‹A restatement of the infinite Ramsey theorem using partition notation› lemma Ramsey_partn: "partn_lst_VWF ω [ω,ω] 2" proof (clarsimp simp: partn_lst_def) fix f assume "f ∈ [elts ω]⇗2⇖ → {..<Suc (Suc 0)}" then have *: "∀x∈elts ω. ∀y∈elts ω. x ≠ y ⟶ f {x, y} < 2" by (auto simp: nsets_def eval_nat_numeral) obtain H i where H: "H ⊆ elts ω" and "infinite H" and t: "i < Suc (Suc 0)" and teq: "∀x∈H. ∀y∈H. x ≠ y ⟶ f {x, y} = i" using Ramsey2 [OF infinite_ω *] by (auto simp: eval_nat_numeral) then have "tp H = [ω, ω] ! i" using less_2_cases eval_nat_numeral ordertype_infinite_ω by force moreover have "f ` {N. N ⊆ H ∧ finite N ∧ card N = 2} ⊆ {i}" by (force simp: teq card_2_iff) ultimately have "f ` [H]⇗2⇖ ⊆ {i}" by (metis (no_types) nsets_def numeral_2_eq_2) then show "∃i<Suc (Suc 0). ∃H⊆elts ω. tp H = [ω,ω] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}" using H ‹tp H = [ω, ω] ! i› t by blast qed text ‹This is the counterexample sketched in Hajnal and Larson, section 9.1.› proposition omega_basic_counterexample: assumes "Ord α" shows "¬ partn_lst_VWF α [succ (vcard α), ω] 2" proof - obtain π where funπ: "π ∈ elts α → elts (vcard α)" and injπ: "inj_on π (elts α)" using inj_into_vcard by auto have Ordπ: "Ord (π x)" if "x ∈ elts α" for x using Ord_in_Ord funπ that by fastforce define f where "f A ≡ @i::nat. ∃x y. A = {x,y} ∧ x < y ∧ (π x < π y ∧ i=0 ∨ π y < π x ∧ i=1)" for A have f_Pi: "f ∈ [elts α]⇗2⇖ → {..<Suc (Suc 0)}" proof fix A assume "A ∈ [elts α]⇗2⇖" then obtain x y where xy: "x ∈ elts α" "y ∈ elts α" "x < y" and A: "A = {x,y}" apply (clarsimp simp: nsets_2_eq) by (metis Ord_in_Ord Ord_linear_lt assms insert_commute) consider "π x < π y" | "π y < π x" by (metis Ordπ Ord_linear_lt injπ inj_onD less_imp_not_eq2 xy) then show "f A ∈ {..<Suc (Suc 0)}" by (metis A One_nat_def lessI lessThan_iff zero_less_Suc ‹x < y› A exE_some [OF _ f_def]) qed have fiff: "π x < π y ∧ i=0 ∨ π y < π x ∧ i=1" if f: "f {x,y} = i" and xy: "x ∈ elts α" "y ∈ elts α" "x<y" for x y i proof - consider "π x < π y" | "π y < π x" using xy by (metis Ordπ Ord_linear_lt injπ inj_onD less_V_def) then show ?thesis proof cases case 1 then have "f{x,y} = 0" using ‹x<y› by (force simp: f_def Set.doubleton_eq_iff) then show ?thesis using "1" f by auto next case 2 then have "f{x,y} = 1" using ‹x<y› by (force simp: f_def Set.doubleton_eq_iff) then show ?thesis using "2" f by auto qed qed have False if eq: "tp H = succ (vcard α)" and H: "H ⊆ elts α" and 0: "⋀A. A ∈ [H]⇗2⇖ ⟹ f A = 0" for H proof - have [simp]: "small H" using H down by auto have OH: "Ord x" if "x ∈ H" for x using H Ord_in_Ord ‹Ord α› that by blast have π: "π x < π y" if "x∈H" "y∈H" "x<y" for x y using 0 [of "{x,y}"] that H fiff by (fastforce simp: nsets_2_eq) have sub_vcard: "π ` H ⊆ elts (vcard α)" using H funπ by auto have "tp H = tp (π ` H)" proof (rule ordertype_VWF_inc_eq [symmetric]) show "π ` H ⊆ ON" using H Ordπ by blast qed (auto simp: π OH subsetI) also have "… ≤ vcard α" by (simp add: H sub_vcard assms ordertype_le_Ord) finally show False by (simp add: eq succ_le_iff) qed moreover have False if eq: "tp H = ω" and H: "H ⊆ elts α" and 1: "⋀A. A ∈ [H]⇗2⇖ ⟹ f A = Suc 0" for H proof - have [simp]: "small H" using H down by auto define η where "η ≡ inv_into H (ordermap H VWF) ∘ ord_of_nat" have bij: "bij_betw (ordermap H VWF) H (elts ω)" by (metis ordermap_bij ‹small H› eq total_on_VWF wf_VWF) then have "bij_betw (inv_into H (ordermap H VWF)) (elts ω) H" by (simp add: bij_betw_inv_into) then have η: "bij_betw η UNIV H" unfolding η_def by (metis ω_def bij_betw_comp_iff2 bij_betw_def elts_of_set inf inj_ord_of_nat order_refl) moreover have Ordη: "Ord (η k)" for k by (meson H Ord_in_Ord UNIV_I η assms bij_betw_apply subsetD) moreover obtain k where k: "(π (η(Suc k)), π (η k)) ∉ VWF" by (meson wf_VWF wf_iff_no_infinite_down_chain) moreover have π: "π y < π x" if "x∈H" "y∈H" "x<y" for x y using 1 [of "{x,y}"] that H fiff by (fastforce simp: nsets_2_eq) ultimately have "η (Suc k) ≤ η k" by (metis H Ordπ Ord_linear2 VWF_iff_Ord_less bij_betw_def rangeI subset_iff) then have "(η (Suc k), η k) ∈ VWF ∨ η (Suc k) = η k" using Ordη Ord_mem_iff_lt by auto then have "ordermap H VWF (η (Suc k)) ≤ ordermap H VWF (η k)" by (metis η ‹small H› bij_betw_imp_surj_on ordermap_mono_le rangeI trans_VWF wf_VWF) moreover have "ordermap H VWF (η (Suc k)) = succ (ord_of_nat k)" unfolding η_def using bij bij_betw_inv_into_right by force moreover have "ordermap H VWF (η k) = ord_of_nat k" using η_def bij bij_betw_inv_into_right by force ultimately show False by (simp add: less_eq_V_def) qed ultimately show ?thesis apply (simp add: partn_lst_def image_subset_iff) by (metis f_Pi less_2_cases nth_Cons_0 nth_Cons_Suc numeral_2_eq_2) qed subsection ‹Specker's theorem› definition form_split :: "[nat,nat,nat,nat,nat] ⇒ bool" where "form_split a b c d i ≡ a ≤ c ∧ (i=0 ∧ a<b ∧ b<c ∧ c<d ∨ i=1 ∧ a<c ∧ c<b ∧ b<d ∨ i=2 ∧ a<c ∧ c<d ∧ d<b ∨ i=3 ∧ a=c ∧ b≠d)" definition form :: "[(nat*nat)set, nat] ⇒ bool" where "form u i ≡ ∃a b c d. u = {(a,b),(c,d)} ∧ form_split a b c d i" definition scheme :: "[(nat*nat)set] ⇒ nat set" where "scheme u ≡ fst ` u ∪ snd ` u" definition UU :: "(nat*nat) set" where "UU ≡ {(a,b). a < b}" lemma ordertype_UNIV_ω2: "ordertype UNIV pair_less = ω↑2" using ordertype_Times [of concl: UNIV UNIV less_than less_than] by (simp add: total_less_than pair_less_def ordertype_nat_ω numeral_2_eq_2) lemma ordertype_UU_ge_ω2: "ordertype UNIV pair_less ≤ ordertype UU pair_less" proof (rule ordertype_inc_le) define π where "π ≡ λ(m,n). (m, Suc (m+n))" show "(π (x::nat × nat), π y) ∈ pair_less" if "(x, y) ∈ pair_less" for x y using that by (auto simp: π_def pair_less_def split: prod.split) show "range π ⊆ UU" by (auto simp: π_def UU_def) qed auto lemma ordertype_UU_ω2: "ordertype UU pair_less = ω↑2" by (metis eq_iff ordertype_UNIV_ω2 ordertype_UU_ge_ω2 ordertype_mono small top_greatest trans_pair_less wf_pair_less) text ‹Lemma 2.3 of 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_2_3: fixes f :: "(nat × nat) set ⇒ nat" assumes "f ∈ [UU]⇗2⇖ → {..<Suc (Suc 0)}" obtains N js where "infinite N" and "⋀k u. ⟦k < 4; u ∈ [UU]⇗2⇖; form u k; scheme u ⊆ N⟧ ⟹ f u = js!k" proof - have f_less2: "f {p,q} < Suc (Suc 0)" if "p ≠ q" "p ∈ UU" "q ∈ UU" for p q proof - have "{p,q} ∈ [UU]⇗2⇖" using that by (simp add: nsets_def) then show ?thesis using assms by (simp add: Pi_iff) qed define f0 where "f0 ≡ (λA::nat set. THE x. ∃a b c d. A = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d ∧ x = f {(a,b),(c,d)})" have f0: "f0 {a,b,c,d} = f {(a,b),(c,d)}" if "a<b" "b<c" "c<d" for a b c d unfolding f0_def apply (rule theI2 [where a = "f {(a,b), (c,d)}"]) using that by (force simp: insert_eq_iff split: if_split_asm)+ have "f0 X < Suc (Suc 0)" if "finite X" and "card X = 4" for X proof - have "X ∈ [X]⇗4⇖" using that by (auto simp: nsets_def) then obtain a b c d where "X = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d" by (auto simp: ordered_nsets_4_eq) then show ?thesis using f0 f_less2 by (auto simp: UU_def) qed then have "∃N t. infinite N ∧ t < Suc (Suc 0) ∧ (∀X. X ⊆ N ∧ finite X ∧ card X = 4 ⟶ f0 X = t)" using Ramsey [of UNIV 4 f0 2] by (simp add: eval_nat_numeral) then obtain N0 j0 where "infinite N0" and j0: "j0 < Suc (Suc 0)" and N0: "⋀A. A ∈ [N0]⇗4⇖ ⟹ f0 A = j0" by (auto simp: nsets_def) define f1 where "f1 ≡ (λA::nat set. THE x. ∃a b c d. A = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d ∧ x = f {(a,c),(b,d)})" have f1: "f1 {a,b,c,d} = f {(a,c),(b,d)}" if "a<b" "b<c" "c<d" for a b c d unfolding f1_def apply (rule theI2 [where a = "f {(a,c), (b,d)}"]) using that by (force simp: insert_eq_iff split: if_split_asm)+ have "f1 X < Suc (Suc 0)" if "finite X" and "card X = 4" for X proof - have "X ∈ [X]⇗4⇖" using that by (auto simp: nsets_def) then obtain a b c d where "X = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d" by (auto simp: ordered_nsets_4_eq) then show ?thesis using f1 f_less2 by (auto simp: UU_def) qed then have "∃N t. N ⊆ N0 ∧ infinite N ∧ t < Suc (Suc 0) ∧ (∀X. X ⊆ N ∧ finite X ∧ card X = 4 ⟶ f1 X = t)" using ‹infinite N0› Ramsey [of N0 4 f1 2] by (simp add: eval_nat_numeral) then obtain N1 j1 where "N1 ⊆ N0" "infinite N1" and j1: "j1 < Suc (Suc 0)" and N1: "⋀A. A ∈ [N1]⇗4⇖ ⟹ f1 A = j1" by (auto simp: nsets_def) define f2 where "f2 ≡ (λA::nat set. THE x. ∃a b c d. A = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d ∧ x = f {(a,d),(b,c)})" have f2: "f2 {a,b,c,d} = f {(a,d),(b,c)}" if "a<b" "b<c" "c<d" for a b c d unfolding f2_def apply (rule theI2 [where a = "f {(a,d), (b,c)}"]) using that by (force simp: insert_eq_iff split: if_split_asm)+ have "f2 X < Suc (Suc 0)" if "finite X" and "card X = 4" for X proof - have "X ∈ [X]⇗4⇖" using that by (auto simp: nsets_def) then obtain a b c d where "X = {a,b,c,d} ∧ a<b ∧ b<c ∧ c<d" by (auto simp: ordered_nsets_4_eq) then show ?thesis using f2 f_less2 by (auto simp: UU_def) qed then have "∃N t. N ⊆ N1 ∧ infinite N ∧ t < Suc (Suc 0) ∧ (∀X. X ⊆ N ∧ finite X ∧ card X = 4 ⟶ f2 X = t)" using ‹infinite N1› Ramsey [of N1 4 f2 2] by (simp add: eval_nat_numeral) then obtain N2 j2 where "N2 ⊆ N1" "infinite N2" and j2: "j2 < Suc (Suc 0)" and N2: "⋀A. A ∈ [N2]⇗4⇖ ⟹ f2 A = j2" by (auto simp: nsets_def) define f3 where "f3 ≡ (λA::nat set. THE x. ∃a b c. A = {a,b,c} ∧ a<b ∧ b<c ∧ x = f {(a,b),(a,c)})" have f3: "f3 {a,b,c} = f {(a,b),(a,c)}" if "a<b" "b<c" for a b c unfolding f3_def apply (rule theI2 [where a = "f {(a,b), (a,c)}"]) using that by (force simp: insert_eq_iff split: if_split_asm)+ have f3': "f3 {a,b,c} = f {(a,b),(a,c)}" if "a<c" "c<b" for a b c using f3 [of a c b] that by (simp add: insert_commute) have "f3 X < Suc (Suc 0)" if "finite X" and "card X = 3" for X proof - have "X ∈ [X]⇗3⇖" using that by (auto simp: nsets_def) then obtain a b c where "X = {a,b,c} ∧ a<b ∧ b<c" by (auto simp: ordered_nsets_3_eq) then show ?thesis using f3 f_less2 by (auto simp: UU_def) qed then have "∃N t. N ⊆ N2 ∧ infinite N ∧ t < Suc (Suc 0) ∧ (∀X. X ⊆ N ∧ finite X ∧ card X = 3 ⟶ f3 X = t)" using ‹infinite N2› Ramsey [of N2 3 f3 2] by (simp add: eval_nat_numeral) then obtain N3 j3 where "N3 ⊆ N2" "infinite N3" and j3: "j3 < Suc (Suc 0)" and N3: "⋀A. A ∈ [N3]⇗3⇖ ⟹ f3 A = j3" by (auto simp: nsets_def) show thesis proof fix k u assume "k < 4" and u: "form u k" "scheme u ⊆ N3" and UU: "u ∈ [UU]⇗2⇖" then consider (0) "k=0" | (1) "k=1" | (2) "k=2" | (3) "k=3" by linarith then show "f u = [j0,j1,j2,j3] ! k" proof cases case 0 have "N3 ⊆ N0" using ‹N1 ⊆ N0› ‹N2 ⊆ N1› ‹N3 ⊆ N2› by auto then show ?thesis using u 0 apply (auto simp: form_def form_split_def scheme_def simp flip: f0) apply (force simp: nsets_def intro: N0) done next case 1 have "N3 ⊆ N1" using ‹N2 ⊆ N1› ‹N3 ⊆ N2› by auto then show ?thesis using u 1 apply (auto simp: form_def form_split_def scheme_def simp flip: f1) apply (force simp: nsets_def intro: N1) done next case 2 then show ?thesis using u ‹N3 ⊆ N2› apply (auto simp: form_def form_split_def scheme_def nsets_def simp flip: f2) apply (force simp: nsets_def intro: N2) done next case 3 { fix a b d assume "{(a, b), (a, d)} ∈ [UU]⇗2⇖" and *: "a ∈ N3" "b ∈ N3" "d ∈ N3" "b ≠ d" then have "a<b" "a<d" by (auto simp: UU_def nsets_def) then have "f {(a, b), (a, d)} = j3" using * apply (auto simp: neq_iff simp flip: f3 f3') apply (force simp: nsets_def intro: N3)+ done } then show ?thesis using u UU 3 by (auto simp: form_def form_split_def scheme_def) qed qed (rule ‹infinite N3›) qed text ‹Lemma 2.4 of Jean A. Larson, ibid.› lemma lemma_2_4: assumes "infinite N" "k < 4" obtains M where "M ∈ [UU]⇗m⇖" "⋀u. u ∈ [M]⇗2⇖ ⟹ form u k" "⋀u. u ∈ [M]⇗2⇖ ⟹ scheme u ⊆ N" proof - obtain f:: "nat ⇒ nat" where "bij_betw f UNIV N" "strict_mono f" using assms by (meson bij_enumerate enumerate_mono strict_monoI) then have iff[simp]: "f x = f y ⟷ x=y" "f x < f y ⟷ x<y" for x y by (simp_all add: strict_mono_eq strict_mono_less) have [simp]: "f x ∈ N" for x using bij_betw_apply [OF ‹bij_betw f UNIV N›] by blast define M0 where "M0 = (λi. (f(2*i), f(Suc(2*i)))) ` {..<m}" define M1 where "M1 = (λi. (f i, f(m+i))) ` {..<m}" define M2 where "M2 = (λi. (f i, f(2*m-i))) ` {..<m}" define M3 where "M3 = (λi. (f 0, f (Suc i))) ` {..<m}" consider (0) "k=0" | (1) "k=1" | (2) "k=2" | (3) "k=3" using assms by linarith then show thesis proof cases case 0 show ?thesis proof have "inj_on (λi. (f (2 * i), f (Suc (2 * i)))) {..<m}" by (auto simp: inj_on_def) then show "M0 ∈ [UU]⇗m⇖" by (simp add: M0_def nsets_def card_image UU_def image_subset_iff) next fix u assume u: "(u::(nat × nat) set) ∈ [M0]⇗2⇖" then obtain x y where "u = {x,y}" "x ≠ y" "x ∈ M0" "y ∈ M0" by (auto simp: nsets_2_eq) then obtain i j where "i<j" "j<m" and ueq: "u = {(f(2*i), f(Suc(2*i))), (f(2*j), f(Suc(2*j)))}" apply (clarsimp simp: M0_def) apply (metis (full_types) insert_commute less_linear)+ done moreover have "f (2 * i) ≤ f (2 * j)" by (simp add: ‹i<j› less_imp_le_nat) ultimately show "form u k" apply (simp add: 0 form_def form_split_def nsets_def) apply (rule_tac x="f (2 * i)" in exI) apply (rule_tac x="f (Suc (2 * i))" in exI) apply (rule_tac x="f (2 * j)" in exI) apply (rule_tac x="f (Suc (2 * j))" in exI) apply auto done show "scheme u ⊆ N" using ueq by (auto simp: scheme_def) qed next case 1 show ?thesis proof have "inj_on (λi. (f i, f(m+i))) {..<m}" by (auto simp: inj_on_def) then show "M1 ∈ [UU]⇗m⇖" by (simp add: M1_def nsets_def card_image UU_def image_subset_iff) next fix u assume u: "(u::(nat × nat) set) ∈ [M1]⇗2⇖" then obtain x y where "u = {x,y}" "x ≠ y" "x ∈ M1" "y ∈ M1" by (auto simp: nsets_2_eq) then obtain i j where "i<j" "j<m" and ueq: "u = {(f i, f(m+i)), (f j, f(m+j))}" apply (auto simp: M1_def) apply (metis (full_types) insert_commute less_linear)+ done then show "form u k" apply (simp add: 1 form_def form_split_def nsets_def) by (metis iff(2) nat_add_left_cancel_less nat_less_le trans_less_add1) show "scheme u ⊆ N" using ueq by (auto simp: scheme_def) qed next case 2 show ?thesis proof have "inj_on (λi. (f i, f(2*m-i))) {..<m}" by (auto simp: inj_on_def) then show "M2 ∈ [UU]⇗m⇖" by (auto simp: M2_def nsets_def card_image UU_def image_subset_iff) next fix u assume u: "(u::(nat × nat) set) ∈ [M2]⇗2⇖" then obtain x y where "u = {x,y}" "x ≠ y" "x ∈ M2" "y ∈ M2" by (auto simp: nsets_2_eq) then obtain i j where "i<j" "j<m" and ueq: "u = {(f i, f(2*m-i)), (f j, f(2*m-j))}" apply (auto simp: M2_def) apply (metis (full_types) insert_commute less_linear)+ done then show "form u k" apply (simp add: 2 form_def form_split_def nsets_def) apply (rule_tac x="f i" in exI) apply (rule_tac x="f (2 * m - i)" in exI) apply (rule_tac x="f j" in exI) apply (rule_tac x="f (2 * m - j)" in exI) apply (auto simp: less_imp_le_nat) done show "scheme u ⊆ N" using ueq by (auto simp: scheme_def) qed next case 3 show ?thesis proof have "inj_on (λi. (f 0, f (Suc i))) {..<m}" by (auto simp: inj_on_def) then show "M3 ∈ [UU]⇗m⇖" by (auto simp: M3_def nsets_def card_image UU_def image_subset_iff) next fix u assume u: "(u::(nat × nat) set) ∈ [M3]⇗2⇖" then obtain x y where "u = {x,y}" "x ≠ y" "x ∈ M3" "y ∈ M3" by (auto simp: nsets_2_eq) then obtain i j where "i<j" "j<m" and ueq: "u = {(f 0, f(Suc i)), (f 0, f(Suc j))}" apply (auto simp: M3_def) apply (metis (full_types) insert_commute less_linear)+ done then show "form u k" by (fastforce simp: 3 form_def form_split_def nsets_def) show "scheme u ⊆ N" using ueq by (auto simp: scheme_def) qed qed qed text ‹Lemma 2.5 of Jean A. Larson, ibid.› lemma lemma_2_5: assumes "infinite N" obtains X where "X ⊆ UU" "ordertype X pair_less = ω↑2" "⋀u. u ∈ [X]⇗2⇖ ⟹ (∃k<4. form u k) ∧ scheme u ⊆ N" proof - obtain C where dis: "pairwise (λi j. disjnt (C i) (C j)) UNIV" and N: "(⋃i. C i) ⊆ N" and infC: "⋀i::nat. infinite (C i)" using assms infinite_infinite_partition by blast then have "∃φ::nat ⇒ nat. inj φ ∧ range φ = C i ∧ strict_mono φ" for i by (metis nat_infinite_iff strict_mono_on_imp_inj_on) then obtain φ:: "[nat,nat] ⇒ nat" where φ: "⋀i. inj (φ i) ∧ range (φ i) = C i ∧ strict_mono (φ i)" by metis then have π_in_C [simp]: "φ i j ∈ C i' ⟷ i'=i" for i i' j using dis by (fastforce simp: pairwise_def disjnt_def) have less_iff [simp]: "φ i j' < φ i j ⟷ j' < j" for i j' j by (simp add: φ strict_mono_less) let ?a = "φ 0" define X where "X ≡ {(?a i, b) | i b. ?a i < b ∧ b ∈ C (Suc i)}" show thesis proof show "X ⊆ UU" by (auto simp: X_def UU_def) show "ordertype X pair_less = ω↑2" proof (rule antisym) have "ordertype X pair_less ≤ ordertype UU pair_less" by (simp add: ‹X ⊆ UU› ordertype_mono) then show "ordertype X pair_less ≤ ω↑2" using ordertype_UU_ω2 by auto define π where "π ≡ λ(i,j::nat). (?a i, φ (Suc i) (?a j))" have "⋀i j. i < j ⟹ φ 0 i < φ (Suc i) (φ 0 j)" by (meson φ le_less_trans less_iff strict_mono_imp_increasing) then have subX: "π ` UU ⊆ X" by (auto simp: UU_def π_def X_def) then have "ordertype (π ` UU) pair_less ≤ ordertype X pair_less" by (simp add: ordertype_mono) moreover have "ordertype (π ` UU) pair_less = ordertype UU pair_less" proof (rule ordertype_inc_eq) show "(π x, π y) ∈ pair_less" if "x ∈ UU" "y ∈ UU" and "(x, y) ∈ pair_less" for x y using that by (auto simp: UU_def π_def pair_less_def) qed auto ultimately show "ω↑2 ≤ ordertype X pair_less" using ordertype_UU_ω2 by simp qed next fix U assume "U ∈ [X]⇗2⇖" then obtain a b c d where Ueq: "U = {(a,b),(c,d)}" and ne: "(a,b) ≠ (c,d)" and inX: "(a,b) ∈ X" "(c,d) ∈ X" and "a ≤ c" apply (auto simp: nsets_def subset_iff eval_nat_numeral card_Suc_eq Set.doubleton_eq_iff) apply (metis nat_le_linear)+ done show "(∃k<4. form U k) ∧ scheme U ⊆ N" proof show "scheme U ⊆ N" using inX N φ by (fastforce simp: scheme_def Ueq X_def) next consider "a < c" | "a = c ∧ b ≠ d" using ‹a ≤ c› ne nat_less_le by blast then show "∃k<4. form U k" proof cases case 1 have *: "a < b" "b ≠ c" "c < d" using inX by (auto simp: X_def) moreover have "⟦a < c; c < b; ¬ d < b⟧ ⟹ b < d" using inX apply (clarsimp simp: X_def not_less) by (metis φ π_in_C imageE nat.inject nat_less_le) ultimately consider (k0) "a<b ∧ b<c ∧ c<d" | (k1) "a<c ∧ c<b ∧ b<d" | (k2) "a<c ∧ c<d ∧ d<b" using 1 less_linear by blast then show ?thesis proof cases case k0 then have "form U 0" unfolding form_def form_split_def using Ueq ‹a ≤ c› by blast then show ?thesis by force next case k1 then have "form U 1" unfolding form_def form_split_def using Ueq ‹a ≤ c› by blast then show ?thesis by force next case k2 then have "form U 2" unfolding form_def form_split_def using Ueq ‹a ≤ c› by blast then show ?thesis by force qed next case 2 then have "form_split a b c d 3" by (auto simp: form_split_def) then show ?thesis using Ueq form_def leI by force qed qed qed qed text ‹Theorem 2.1 of Jean A. Larson, ibid.› lemma Specker_aux: assumes "α ∈ elts ω" shows "partn_lst pair_less UU [ω↑2,α] 2" unfolding partn_lst_def proof clarsimp fix f assume f: "f ∈ [UU]⇗2⇖ → {..<Suc (Suc 0)}" let ?P0 = "∃X ⊆ UU. ordertype X pair_less = ω↑2 ∧ f ` [X]⇗2⇖ ⊆ {0}" let ?P1 = "∃M ⊆ UU. ordertype M pair_less = α ∧ f ` [M]⇗2⇖ ⊆ {1}" have †: "?P0 ∨ ?P1" proof (rule disjCI) assume "¬ ?P1" then have not1: "⋀M. ⟦M ⊆ UU; ordertype M pair_less = α⟧ ⟹ ∃x∈[M]⇗2⇖. f x ≠ Suc 0" by auto obtain m where m: "α = ord_of_nat m" using assms elts_ω by auto then have f_eq_0: "M ∈ [UU]⇗m⇖ ⟹ ∃x∈[M]⇗2⇖. f x = 0" for M using not1 [of M] finite_ordertype_eq_card [of M pair_less m] f apply (clarsimp simp: nsets_def eval_nat_numeral Pi_def) by (meson less_Suc0 not_less_less_Suc_eq subset_trans) obtain N js where "infinite N" and N: "⋀k u. ⟦k < 4; u ∈ [UU]⇗2⇖; form u k; scheme u ⊆ N⟧ ⟹ f u = js!k" using f lemma_2_3 by blast obtain M0 where M0: "M0 ∈ [UU]⇗m⇖" "⋀u. u ∈ [M0]⇗2⇖ ⟹ form u 0" "⋀u. u ∈ [M0]⇗2⇖ ⟹ scheme u ⊆ N" by (rule lemma_2_4 [OF ‹infinite N›]) auto obtain M1 where M1: "M1 ∈ [UU]⇗m⇖" "⋀u. u ∈ [M1]⇗2⇖ ⟹ form u 1" "⋀u. u ∈ [M1]⇗2⇖ ⟹ scheme u ⊆ N" by (rule lemma_2_4 [OF ‹infinite N›]) auto obtain M2 where M2: "M2 ∈ [UU]⇗m⇖" "⋀u. u ∈ [M2]⇗2⇖ ⟹ form u 2" "⋀u. u ∈ [M2]⇗2⇖ ⟹ scheme u ⊆ N" by (rule lemma_2_4 [OF ‹infinite N›]) auto obtain M3 where M3: "M3 ∈ [UU]⇗m⇖" "⋀u. u ∈ [M3]⇗2⇖ ⟹ form u 3" "⋀u. u ∈ [M3]⇗2⇖ ⟹ scheme u ⊆ N" by (rule lemma_2_4 [OF ‹infinite N›]) auto have "js!0 = 0" using N [of 0 ] M0 f_eq_0 [of M0] by (force simp: nsets_def eval_nat_numeral) moreover have "js!1 = 0" using N [of 1] M1 f_eq_0 [of M1] by (force simp: nsets_def eval_nat_numeral) moreover have "js!2 = 0" using N [of 2 ] M2 f_eq_0 [of M2] by (force simp: nsets_def eval_nat_numeral) moreover have "js!3 = 0" using N [of 3 ] M3 f_eq_0 [of M3] by (force simp: nsets_def eval_nat_numeral) ultimately have js0: "js!k = 0" if "k < 4" for k using that by (auto simp: eval_nat_numeral less_Suc_eq) obtain X where "X ⊆ UU" and otX: "ordertype X pair_less = ω↑2" and X: "⋀u. u ∈ [X]⇗2⇖ ⟹ (∃k<4. form u k) ∧ scheme u ⊆ N" using ‹infinite N› lemma_2_5 by auto moreover have "f ` [X]⇗2⇖ ⊆ {0}" proof (clarsimp simp: image_subset_iff) fix u assume u: "u ∈ [X]⇗2⇖" then have u_UU2: "u ∈ [UU]⇗2⇖" using ‹X ⊆ UU› nsets_mono by blast show "f u = 0" using X u N [OF _ u_UU2] js0 by auto qed ultimately show "∃X ⊆ UU. ordertype X pair_less = ω↑2 ∧ f ` [X]⇗2⇖ ⊆ {0}" by blast qed then show "∃i<Suc (Suc 0). ∃H⊆UU. ordertype H pair_less = [ω↑2, α] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}" by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc) qed theorem Specker: "α ∈ elts ω ⟹ partn_lst_VWF (ω↑2) [ω↑2,α] 2" using partn_lst_imp_partn_lst_VWF_eq [OF Specker_aux] ordertype_UU_ω2 wf_pair_less by blast end