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
  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 α. HB. 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  HB  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 α. HC. 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))  (xH'. yH'. (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 α'. HB. 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). Helts ω. 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). Helts . 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 "xelts . yelts . 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 α. Helts β. 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 α. HU. 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 *: "xelts ω. yelts ω. 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: "xH. yH. 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). Helts ω. 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 "xH" "yH" "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 "xH" "yH" "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  bd)"

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). HUU. 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