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 α. ∃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