# Theory Partitions

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

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'"
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
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"
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
qed
ultimately show ?thesis
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
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
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)"
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)
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
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"
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