Theory Ramsey

(*  Title:      HOL/Library/Ramsey.thy
    Author:     Tom Ridge. Full finite version by L C Paulson.
*)

section ‹Ramsey's Theorem›

theory Ramsey
  imports Infinite_Set Equipollence FuncSet 
begin

subsection ‹Preliminary definitions›

abbreviation strict_sorted :: "'a::linorder list ⇒ bool" where
  "strict_sorted ≡ sorted_wrt (<)" 

subsubsection ‹The $n$-element subsets of a set $A$›

definition nsets :: "['a set, nat] ⇒ 'a set set" ("([_]⇗_⇖)" [0,999] 999)
  where "nsets A n ≡ {N. N ⊆ A ∧ finite N ∧ card N = n}"

lemma finite_imp_finite_nsets: "finite A ⟹ finite ([A]⇗k⇖)"
  by (simp add: nsets_def)

lemma nsets_mono: "A ⊆ B ⟹ nsets A n ⊆ nsets B n"
  by (auto simp: nsets_def)

lemma nsets_Pi_contra: "A' ⊆ A ⟹ Pi ([A]⇗n⇖) B ⊆ Pi ([A']⇗n⇖) B"
  by (auto simp: nsets_def)

lemma nsets_2_eq: "nsets A 2 = (⋃x∈A. ⋃y∈A - {x}. {{x, y}})"
  by (auto simp: nsets_def card_2_iff)

lemma nsets2_E:
  assumes "e ∈ [A]⇗2⇖"
  obtains x y where "e = {x,y}" "x ∈ A" "y ∈ A" "x≠y"
  using assms by (auto simp: nsets_def card_2_iff)

lemma nsets_doubleton_2_eq [simp]: "[{x, y}]⇗2⇖ = (if x=y then {} else {{x, y}})"
  by (auto simp: nsets_2_eq)

lemma doubleton_in_nsets_2 [simp]: "{x,y} ∈ [A]⇗2⇖ ⟷ x ∈ A ∧ y ∈ A ∧ x ≠ y"
  by (auto simp: nsets_2_eq Set.doubleton_eq_iff)

lemma nsets_3_eq: "nsets A 3 = (⋃x∈A. ⋃y∈A - {x}. ⋃z∈A - {x,y}. {{x,y,z}})"
  by (simp add: eval_nat_numeral nsets_def card_Suc_eq) blast

lemma nsets_4_eq: "[A]⇗4⇖ = (⋃u∈A. ⋃x∈A - {u}. ⋃y∈A - {u,x}. ⋃z∈A - {u,x,y}. {{u,x,y,z}})"
     (is "_ = ?rhs")
proof
  show "[A]⇗4⇖ ⊆ ?rhs"
    by (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) blast
  show "?rhs ⊆ [A]⇗4⇖"
    apply (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq)
    by (metis insert_iff singletonD)
qed

lemma nsets_disjoint_2:
  "X ∩ Y = {} ⟹ [X ∪ Y]⇗2⇖ = [X]⇗2⇖ ∪ [Y]⇗2⇖ ∪ (⋃x∈X. ⋃y∈Y. {{x,y}})"
  by (fastforce simp: nsets_2_eq Set.doubleton_eq_iff)

lemma ordered_nsets_2_eq:
  fixes A :: "'a::linorder set"
  shows "nsets A 2 = {{x,y} | x y. x ∈ A ∧ y ∈ A ∧ x<y}"
     (is "_ = ?rhs")
proof
  show "nsets A 2 ⊆ ?rhs"
    unfolding numeral_nat
    apply (clarsimp simp add: nsets_def card_Suc_eq Set.doubleton_eq_iff not_less)
    by (metis antisym)
  show "?rhs ⊆ nsets A 2"
    unfolding numeral_nat by (auto simp: nsets_def card_Suc_eq)
qed

lemma ordered_nsets_3_eq:
  fixes A :: "'a::linorder set"
  shows "nsets A 3 = {{x,y,z} | x y z. x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x<y ∧ y<z}"
     (is "_ = ?rhs")
proof
  show "nsets A 3 ⊆ ?rhs"
    apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
    by (metis insert_commute linorder_cases)
  show "?rhs ⊆ nsets A 3"
    apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
  by (metis empty_iff insert_iff not_less_iff_gr_or_eq)
qed

lemma ordered_nsets_4_eq:
  fixes A :: "'a::linorder set"
  shows "[A]⇗4⇖ = {U. ∃u x y z. U = {u,x,y,z} ∧ u ∈ A ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ u < x ∧ x < y ∧ y < z}"
    (is "_ = Collect ?RHS")
proof -
  { fix U
    assume "U ∈ [A]⇗4⇖"
    then obtain l where "strict_sorted l" "List.set l = U" "length l = 4" "U ⊆ A"
      by (simp add: nsets_def) (metis finite_set_strict_sorted)
    then have "?RHS U"
      unfolding numeral_nat length_Suc_conv by auto blast }
  moreover
  have "Collect ?RHS ⊆ [A]⇗4⇖"
    apply (clarsimp simp add: nsets_def eval_nat_numeral)
    apply (subst card_insert_disjoint, auto)+
    done
  ultimately show ?thesis
    by auto
qed

lemma ordered_nsets_5_eq:
  fixes A :: "'a::linorder set"
  shows "[A]⇗5⇖ = {U. ∃u v x y z. U = {u,v,x,y,z} ∧ u ∈ A ∧ v ∈ A ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ u < v ∧ v < x ∧ x < y ∧ y < z}"
    (is "_ = Collect ?RHS")
proof -
  { fix U
  assume "U ∈ [A]⇗5⇖"
  then obtain l where "strict_sorted l" "List.set l = U" "length l = 5" "U ⊆ A"
    apply (simp add: nsets_def)
    by (metis finite_set_strict_sorted)
  then have "?RHS U"
    unfolding numeral_nat length_Suc_conv by auto blast }
  moreover
  have "Collect ?RHS ⊆ [A]⇗5⇖"
    apply (clarsimp simp add: nsets_def eval_nat_numeral)
    apply (subst card_insert_disjoint, auto)+
    done
  ultimately show ?thesis
    by auto
qed

lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
  apply (simp add: binomial_def nsets_def)
  by (meson subset_eq_atLeast0_lessThan_finite)

lemma nsets_eq_empty_iff: "nsets A r = {} ⟷ finite A ∧ card A < r"
  unfolding nsets_def
proof (intro iffI conjI)
  assume that: "{N. N ⊆ A ∧ finite N ∧ card N = r} = {}"
  show "finite A"
    using infinite_arbitrarily_large that by auto
  then have "¬ r ≤ card A"
    using that by (simp add: set_eq_iff) (metis obtain_subset_with_card_n)
  then show "card A < r"
    using not_less by blast
next
  show "{N. N ⊆ A ∧ finite N ∧ card N = r} = {}"
    if "finite A ∧ card A < r"
    using that card_mono leD by auto
qed

lemma nsets_eq_empty: "⟦finite A; card A < r⟧ ⟹ nsets A r = {}"
  by (simp add: nsets_eq_empty_iff)

lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})"
  by (auto simp: nsets_def)

lemma nsets_singleton_iff: "nsets {a} r = (if r=0 then {{}} else if r=1 then {{a}} else {})"
  by (auto simp: nsets_def card_gt_0_iff subset_singleton_iff)

lemma nsets_self [simp]: "nsets {..<m} m = {{..<m}}"
  unfolding nsets_def
  apply auto
  by (metis add.left_neutral lessThan_atLeast0 lessThan_iff subset_card_intvl_is_intvl)

lemma nsets_zero [simp]: "nsets A 0 = {{}}"
  by (auto simp: nsets_def)

lemma nsets_one: "nsets A (Suc 0) = (λx. {x}) ` A"
  using card_eq_SucD by (force simp: nsets_def)

lemma inj_on_nsets:
  assumes "inj_on f A"
  shows "inj_on (λX. f ` X) ([A]⇗n⇖)"
  using assms unfolding nsets_def
  by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq)

lemma bij_betw_nsets:
  assumes "bij_betw f A B"
  shows "bij_betw (λX. f ` X) ([A]⇗n⇖) ([B]⇗n⇖)"
proof -
  have "(`) f ` [A]⇗n⇖ = [f ` A]⇗n⇖"
    using assms
    apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset)
    by (metis card_image inj_on_finite order_refl subset_image_inj)
  with assms show ?thesis
    by (auto simp: bij_betw_def inj_on_nsets)
qed

lemma nset_image_obtains:
  assumes "X ∈ [f`A]⇗k⇖" "inj_on f A"
  obtains Y where "Y ∈ [A]⇗k⇖" "X = f ` Y"
  using assms
  apply (clarsimp simp add: nsets_def subset_image_iff)
  by (metis card_image finite_imageD inj_on_subset)

lemma nsets_image_funcset:
  assumes "g ∈ S → T" and "inj_on g S"
  shows "(λX. g ` X) ∈ [S]⇗k⇖ → [T]⇗k⇖"
    using assms
    by (fastforce simp: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset)

lemma nsets_compose_image_funcset:
  assumes f: "f ∈ [T]⇗k⇖ → D" and "g ∈ S → T" and "inj_on g S"
  shows "f ∘ (λX. g ` X) ∈ [S]⇗k⇖ → D"
proof -
  have "(λX. g ` X) ∈ [S]⇗k⇖ → [T]⇗k⇖"
    using assms by (simp add: nsets_image_funcset)
  then show ?thesis
    using f by fastforce
qed

subsubsection ‹Further properties, involving equipollence›

lemma nsets_lepoll_cong:
  assumes "A ≲ B"
  shows "[A]⇗k⇖ ≲ [B]⇗k⇖"
proof -
  obtain f where f: "inj_on f A" "f ` A ⊆ B"
    by (meson assms lepoll_def)
  define F where "F ≡ λN. f ` N"
  have "inj_on F ([A]⇗k⇖)"
    using F_def f inj_on_nsets by blast
  moreover
  have "F ` ([A]⇗k⇖) ⊆ [B]⇗k⇖"
    by (metis F_def bij_betw_def bij_betw_nsets f nsets_mono)
  ultimately show ?thesis
    by (meson lepoll_def)
qed

lemma nsets_eqpoll_cong:
  assumes "A≈B"
  shows "[A]⇗k⇖ ≈ [B]⇗k⇖"
  by (meson assms eqpoll_imp_lepoll eqpoll_sym lepoll_antisym nsets_lepoll_cong)

lemma infinite_imp_infinite_nsets:
  assumes inf: "infinite A" and "k>0"
  shows "infinite ([A]⇗k⇖)"
proof -
  obtain B where "B ⊂ A" "A≈B"
    by (meson inf infinite_iff_psubset)
  then obtain a where a: "a ∈ A" "a ∉ B"
    by blast
  then obtain N where "N ⊆ B" "finite N" "card N = k-1" "a ∉ N"
    by (metis ‹A ≈ B› inf eqpoll_finite_iff infinite_arbitrarily_large subset_eq)
  with a ‹k>0› ‹B ⊂ A› have "insert a N ∈ [A]⇗k⇖"
    by (simp add: nsets_def)
  with a have "nsets B k ≠ nsets A k"
    by (metis (no_types, lifting) in_mono insertI1 mem_Collect_eq nsets_def)
  moreover have "nsets B k ⊆ nsets A k"
    using ‹B ⊂ A› nsets_mono by auto
  ultimately show ?thesis
    unfolding infinite_iff_psubset_le
    by (meson ‹A ≈ B› eqpoll_imp_lepoll nsets_eqpoll_cong psubsetI)
qed

lemma finite_nsets_iff:
  assumes "k>0"
  shows "finite ([A]⇗k⇖) ⟷ finite A"
  using assms finite_imp_finite_nsets infinite_imp_infinite_nsets by blast

lemma card_nsets [simp]: "card (nsets A k) = card A choose k"
proof (cases "finite A")
  case True
  then show ?thesis
    by (metis bij_betw_nsets bij_betw_same_card binomial_eq_nsets ex_bij_betw_nat_finite)
next
  case False
  then show ?thesis
    by (cases "k=0"; simp add: finite_nsets_iff)
qed

subsubsection ‹Partition predicates›

definition "monochromatic ≡ λβ α γ f i. ∃H ∈ nsets β α. f ` (nsets H γ) ⊆ {i}"

text ‹uniform partition sizes›
definition partn :: "'a set ⇒ nat ⇒ nat ⇒ 'b set ⇒ bool"
  where "partn β α γ δ ≡ ∀f ∈ nsets β γ  →  δ. ∃ξ∈δ. monochromatic β α γ f ξ"

text ‹partition sizes enumerated in a list›
definition partn_lst :: "'a set ⇒ nat list ⇒ nat ⇒ bool"
  where "partn_lst β α γ ≡ ∀f ∈ nsets β γ  →  {..<length α}. ∃i < length α. monochromatic β (α!i) γ f i"

text ‹There's always a 0-clique›
lemma partn_lst_0: "γ > 0 ⟹ partn_lst β (0#α) γ"
  by (force simp: partn_lst_def monochromatic_def nsets_empty_iff)

lemma partn_lst_0': "γ > 0 ⟹ partn_lst β (a#0#α) γ"
  by (force simp: partn_lst_def monochromatic_def nsets_empty_iff)

lemma partn_lst_greater_resource:
  fixes M::nat
  assumes M: "partn_lst {..<M} α γ" and "M ≤ N"
  shows "partn_lst {..<N} α γ"
proof (clarsimp simp: partn_lst_def)
  fix f
  assume "f ∈ nsets {..<N} γ → {..<length α}"
  then have "f ∈ nsets {..<M} γ → {..<length α}"
    by (meson Pi_anti_mono ‹M ≤ N› lessThan_subset_iff nsets_mono subsetD)
  then obtain i H where i: "i < length α" and H: "H ∈ nsets {..<M} (α ! i)" and subi: "f ` nsets H γ ⊆ {i}"
    using M unfolding partn_lst_def monochromatic_def by blast
  have "H ∈ nsets {..<N} (α ! i)"
    using ‹M ≤ N› H by (auto simp: nsets_def subset_iff)
  then show "∃i<length α. monochromatic {..<N} (α!i) γ f i"
    using i subi unfolding monochromatic_def by blast
qed

lemma partn_lst_fewer_colours:
  assumes major: "partn_lst β (n#α) γ" and "n ≥ γ"
  shows "partn_lst β α γ"
proof (clarsimp simp: partn_lst_def)
  fix f :: "'a set ⇒ nat"
  assume f: "f ∈ [β]⇗γ⇖ → {..<length α}"
  then obtain i H where i: "i < Suc (length α)"
      and H: "H ∈ [β]⇗((n # α) ! i)⇖"
      and hom: "∀x∈[H]⇗γ⇖. Suc (f x) = i"
    using ‹n ≥ γ› major [unfolded partn_lst_def, rule_format, of "Suc o f"]
    by (fastforce simp: image_subset_iff nsets_eq_empty_iff monochromatic_def)
  show "∃i<length α. monochromatic β (α!i) γ f i"
  proof (cases i)
    case 0
    then have "[H]⇗γ⇖ = {}"
      using hom by blast
    then show ?thesis
      using 0 H ‹n ≥ γ›
      by (simp add: nsets_eq_empty_iff) (simp add: nsets_def)
  next
    case (Suc i')
    then show ?thesis
      unfolding monochromatic_def using i H hom by auto
  qed
qed

lemma partn_lst_eq_partn: "partn_lst {..<n} [m,m] 2 = partn {..<n} m 2 {..<2::nat}"
  apply (simp add: partn_lst_def partn_def numeral_2_eq_2)
  by (metis less_2_cases numeral_2_eq_2 lessThan_iff nth_Cons_0 nth_Cons_Suc)

lemma partn_lstE:
  assumes "partn_lst β α γ" "f ∈ nsets β γ  →  {..<l}" "length α = l"
  obtains i H where "i < length α" "H ∈ nsets β (α!i)" "f ` (nsets H γ) ⊆ {i}"
  using partn_lst_def monochromatic_def assms by metis

lemma partn_lst_less:
  assumes M: "partn_lst β α n" and eq: "length α' = length α" 
    and le: "⋀i. i < length α ⟹ α'!i ≤ α!i "
  shows "partn_lst β α' n"
proof (clarsimp simp: partn_lst_def)
  fix f
  assume "f ∈ [β]⇗n⇖ → {..<length α'}"
  then obtain i H where i: "i < length α"
                   and "H ⊆ β"  and H: "card H = (α!i)" and "finite H"
                   and fi: "f ` nsets H n ⊆ {i}"
    using assms by (auto simp: partn_lst_def monochromatic_def nsets_def)
  then obtain bij where bij: "bij_betw bij H {0..<α!i}"
    by (metis ex_bij_betw_finite_nat)
  then have inj: "inj_on (inv_into H bij) {0..<α' ! i}"
    by (metis bij_betw_def dual_order.refl i inj_on_inv_into ivl_subset le)
  define H' where "H' = inv_into H bij ` {0..<α'!i}"
  show "∃i<length α'. monochromatic β (α'!i) n f i"
    unfolding monochromatic_def
  proof (intro exI bexI conjI)
    show "i < length α'"
      by (simp add: assms(2) 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)
    then have "finite H'"
      by (simp add: ‹finite H› finite_subset)
    with ‹H' ⊆ H› have cardH': "card H' = (α'!i)"
      unfolding H'_def by (simp add: inj card_image)
    show "f ` [H']⇗n⇖ ⊆ {i}"
      by (meson ‹H' ⊆ H› dual_order.trans fi image_mono nsets_mono)
    show "H' ∈ [β]⇗(α'! i)⇖"
      using ‹H ⊆ β› ‹H' ⊆ H› ‹finite H'› cardH' nsets_def by fastforce
  qed
qed


subsection ‹Finite versions of Ramsey's theorem›

text ‹
  To distinguish the finite and infinite ones, lower and upper case
  names are used (ramsey vs Ramsey).
›

subsubsection ‹The Erdős--Szekeres theorem exhibits an upper bound for Ramsey numbers›

text ‹The Erdős--Szekeres bound, essentially extracted from the proof›
fun ES :: "[nat,nat,nat] ⇒ nat"
  where "ES 0 k l = max k l"
  |     "ES (Suc r) k l = 
            (if r=0 then k+l-1
             else if k=0 ∨ l=0 then 1 else Suc (ES r (ES (Suc r) (k-1) l) (ES (Suc r) k (l-1))))"

declare ES.simps [simp del]

lemma ES_0 [simp]: "ES 0 k l = max k l"
  using ES.simps(1) by blast

lemma ES_1 [simp]: "ES 1 k l = k+l-1"
  using ES.simps(2) [of 0 k l] by simp

lemma ES_2: "ES 2 k l = (if k=0 ∨ l=0 then 1 else ES 2 (k-1) l + ES 2 k (l-1))"
  unfolding numeral_2_eq_2
  by (smt (verit) ES.elims One_nat_def Suc_pred add_gr_0 neq0_conv nat.inject zero_less_Suc)

text ‹The Erdős--Szekeres upper bound›
lemma ES2_choose: "ES 2 k l = (k+l) choose k"
proof (induct n ≡ "k+l" arbitrary: k l)
  case 0
  then show ?case
    by (auto simp: ES_2)
next
  case (Suc n)
  then have "k>0 ⟹ l>0 ⟹ ES 2 (k - 1) l + ES 2 k (l - 1) = k + l choose k"
    using choose_reduce_nat by force
  then show ?case
    by (metis ES_2 Nat.add_0_right binomial_n_0 binomial_n_n gr0I)
qed

subsubsection ‹Trivial cases›

text ‹Vacuous, since we are dealing with 0-sets!›
lemma ramsey0: "∃N::nat. partn_lst {..<N} [q1,q2] 0"
  by (force simp: partn_lst_def monochromatic_def ex_in_conv less_Suc_eq nsets_eq_empty_iff)

text ‹Just the pigeon hole principle, since we are dealing with 1-sets›
lemma ramsey1_explicit: "partn_lst {..<q0 + q1 - Suc 0} [q0,q1] 1"
proof -
  have "∃i<Suc (Suc 0). ∃H∈nsets {..<q0 + q1 - 1} ([q0, q1] ! i). f ` nsets H 1 ⊆ {i}"
    if "f ∈ nsets {..<q0 + q1 - 1} (Suc 0) → {..<Suc (Suc 0)}" for f
  proof -
    define A where "A ≡ λi. {q. q < q0+q1-1 ∧ f {q} = i}"
    have "A 0 ∪ A 1 = {..<q0 + q1-1}"
      using that by (auto simp: A_def PiE_iff nsets_one lessThan_Suc_atMost le_Suc_eq)
    moreover have "A 0 ∩ A 1 = {}"
      by (auto simp: A_def)
    ultimately have "q0 + q1 ≤ card (A 0) + card (A 1) + 1"
      by (metis card_Un_le card_lessThan le_diff_conv)
    then consider "card (A 0) ≥ q0" | "card (A 1) ≥ q1"
      by linarith
    then obtain i where "i < Suc (Suc 0)" "card (A i) ≥ [q0, q1] ! i"
      by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc)
    then obtain B where "B ⊆ A i" "card B = [q0, q1] ! i" "finite B"
      by (meson obtain_subset_with_card_n)
    then have "B ∈ nsets {..<q0 + q1 - 1} ([q0, q1] ! i) ∧ f ` nsets B (Suc 0) ⊆ {i}"
      by (auto simp: A_def nsets_def card_1_singleton_iff)
    then show ?thesis
      using ‹i < Suc (Suc 0)› by auto
  qed
  then show ?thesis
    by (simp add: partn_lst_def monochromatic_def)
qed

lemma ramsey1: "∃N::nat. partn_lst {..<N} [q0,q1] 1"
  using ramsey1_explicit by blast


subsubsection ‹Ramsey's theorem with TWO colours and arbitrary exponents (hypergraph version)›

lemma ramsey_induction_step:
  fixes p::nat
  assumes p1: "partn_lst {..<p1} [q1-1,q2] (Suc r)" and p2: "partn_lst {..<p2} [q1,q2-1] (Suc r)"
    and p: "partn_lst {..<p} [p1,p2] r"
    and "q1>0" "q2>0"
  shows "partn_lst {..<Suc p} [q1, q2] (Suc r)"
proof -
  have "∃i<Suc (Suc 0). ∃H∈nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) ⊆ {i}"
    if f: "f ∈ nsets {..p} (Suc r) → {..<Suc (Suc 0)}" for f
  proof -
    define g where "g ≡ λR. f (insert p R)"
    have "f (insert p i) ∈ {..<Suc (Suc 0)}" if "i ∈ nsets {..<p} r" for i
      using that card_insert_if by (fastforce simp: nsets_def intro!: Pi_mem [OF f])
    then have g: "g ∈ nsets {..<p} r → {..<Suc (Suc 0)}"
      by (force simp: g_def PiE_iff)
    then obtain i U where i: "i < Suc (Suc 0)" and gi: "g ` nsets U r ⊆ {i}"
      and U: "U ∈ nsets {..<p} ([p1, p2] ! i)"
      using p by (auto simp: partn_lst_def monochromatic_def)
    then have Usub: "U ⊆ {..<p}"
      by (auto simp: nsets_def)
    consider (izero) "i = 0" | (ione) "i = Suc 0"
      using i by linarith
    then show ?thesis
    proof cases
      case izero
      then have "U ∈ nsets {..<p} p1"
        using U by simp
      then obtain u where u: "bij_betw u {..<p1} U"
        using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp: nsets_def)
      have u_nsets: "u ` X ∈ nsets {..p} n" if "X ∈ nsets {..<p1} n" for X n
      proof -
        have "inj_on u X"
          using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def)
        then show ?thesis
          using Usub u that bij_betwE
          by (fastforce simp: nsets_def card_image)
      qed
      define h where "h ≡ λR. f (u ` R)"
      have "h ∈ nsets {..<p1} (Suc r) → {..<Suc (Suc 0)}"
        unfolding h_def using f u_nsets by auto
      then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) ⊆ {j}"
        and V: "V ∈ nsets {..<p1} ([q1 - Suc 0, q2] ! j)"
        using p1 by (auto simp: partn_lst_def monochromatic_def)
      then have Vsub: "V ⊆ {..<p1}"
        by (auto simp: nsets_def)
      have invinv_eq: "u ` inv_into {..<p1} u ` X = X" if "X ⊆ u ` {..<p1}" for X
        by (simp add: image_inv_into_cancel that)
      let ?W = "insert p (u ` V)"
      consider (jzero) "j = 0" | (jone) "j = Suc 0"
        using j by linarith
      then show ?thesis
      proof cases
        case jzero
        then have "V ∈ nsets {..<p1} (q1 - Suc 0)"
          using V by simp
        then have "u ` V ∈ nsets {..<p} (q1 - Suc 0)"
          using u_nsets [of _ "q1 - Suc 0"] nsets_mono [OF Vsub] Usub u
          unfolding bij_betw_def nsets_def
          by (fastforce elim!: subsetD)
        then have inq1: "?W ∈ nsets {..p} q1"
          unfolding nsets_def using ‹q1 > 0› card_insert_if by fastforce
        have invu_nsets: "inv_into {..<p1} u ` X ∈ nsets V r"
          if "X ∈ nsets (u ` V) r" for X r
        proof -
          have "X ⊆ u ` V ∧ finite X ∧ card X = r"
            using nsets_def that by auto
          then have [simp]: "card (inv_into {..<p1} u ` X) = card X"
            by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u)
          show ?thesis
            using that u Vsub by (fastforce simp: nsets_def bij_betw_def)
        qed
        have "f X = i" if X: "X ∈ nsets ?W (Suc r)" for X
        proof (cases "p ∈ X")
          case True
          then have Xp: "X - {p} ∈ nsets (u ` V) r"
            using X by (auto simp: nsets_def)
          moreover have "u ` V ⊆ U"
            using Vsub bij_betwE u by blast
          ultimately have "X - {p} ∈ nsets U r"
            by (meson in_mono nsets_mono)
          then have "g (X - {p}) = i"
            using gi by blast
          have "f X = i"
            using gi True ‹X - {p} ∈ nsets U r› insert_Diff
            by (fastforce simp: g_def image_subset_iff)
          then show ?thesis
            by (simp add: ‹f X = i› ‹g (X - {p}) = i›)
        next
          case False
          then have Xim: "X ∈ nsets (u ` V) (Suc r)"
            using X by (auto simp: nsets_def subset_insert)
          then have "u ` inv_into {..<p1} u ` X = X"
            using Vsub bij_betw_imp_inj_on u
            by (fastforce simp: nsets_def image_mono invinv_eq subset_trans)
          then show ?thesis
            using izero jzero hj Xim invu_nsets unfolding h_def
            by (fastforce simp: image_subset_iff)
        qed
        moreover have "insert p (u ` V) ∈ nsets {..p} q1"
          by (simp add: izero inq1)
        ultimately show ?thesis
          by (metis izero image_subsetI insertI1 nth_Cons_0 zero_less_Suc)
      next
        case jone
        then have "u ` V ∈ nsets {..p} q2"
          using V u_nsets by auto
        moreover have "f ` nsets (u ` V) (Suc r) ⊆ {j}"
          using hj
          by (force simp: h_def image_subset_iff nsets_def subset_image_inj card_image dest: finite_imageD)
        ultimately show ?thesis
          using jone not_less_eq by fastforce
      qed
    next
      case ione
      then have "U ∈ nsets {..<p} p2"
        using U by simp
      then obtain u where u: "bij_betw u {..<p2} U"
        using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp: nsets_def)
      have u_nsets: "u ` X ∈ nsets {..p} n" if "X ∈ nsets {..<p2} n" for X n
      proof -
        have "inj_on u X"
          using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def)
        then show ?thesis
          using Usub u that bij_betwE
          by (fastforce simp: nsets_def card_image)
      qed
      define h where "h ≡ λR. f (u ` R)"
      have "h ∈ nsets {..<p2} (Suc r) → {..<Suc (Suc 0)}"
        unfolding h_def using f u_nsets by auto
      then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) ⊆ {j}"
        and V: "V ∈ nsets {..<p2} ([q1, q2 - Suc 0] ! j)"
        using p2 by (auto simp: partn_lst_def monochromatic_def)
      then have Vsub: "V ⊆ {..<p2}"
        by (auto simp: nsets_def)
      have invinv_eq: "u ` inv_into {..<p2} u ` X = X" if "X ⊆ u ` {..<p2}" for X
        by (simp add: image_inv_into_cancel that)
      let ?W = "insert p (u ` V)"
      consider (jzero) "j = 0" | (jone) "j = Suc 0"
        using j by linarith
      then show ?thesis
      proof cases
        case jone
        then have "V ∈ nsets {..<p2} (q2 - Suc 0)"
          using V by simp
        then have "u ` V ∈ nsets {..<p} (q2 - Suc 0)"
          using u_nsets [of _ "q2 - Suc 0"] nsets_mono [OF Vsub] Usub u
          unfolding bij_betw_def nsets_def
          by (fastforce elim!: subsetD)
        then have inq1: "?W ∈ nsets {..p} q2"
          unfolding nsets_def using ‹q2 > 0› card_insert_if by fastforce
        have invu_nsets: "inv_into {..<p2} u ` X ∈ nsets V r"
          if "X ∈ nsets (u ` V) r" for X r
        proof -
          have "X ⊆ u ` V ∧ finite X ∧ card X = r"
            using nsets_def that by auto
          then have [simp]: "card (inv_into {..<p2} u ` X) = card X"
            by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u)
          show ?thesis
            using that u Vsub by (fastforce simp: nsets_def bij_betw_def)
        qed
        have "f X = i" if X: "X ∈ nsets ?W (Suc r)" for X
        proof (cases "p ∈ X")
          case True
          then have Xp: "X - {p} ∈ nsets (u ` V) r"
            using X by (auto simp: nsets_def)
          moreover have "u ` V ⊆ U"
            using Vsub bij_betwE u by blast
          ultimately have "X - {p} ∈ nsets U r"
            by (meson in_mono nsets_mono)
          then have "g (X - {p}) = i"
            using gi by blast
          have "f X = i"
            using gi True ‹X - {p} ∈ nsets U r› insert_Diff
            by (fastforce simp: g_def image_subset_iff)
          then show ?thesis
            by (simp add: ‹f X = i› ‹g (X - {p}) = i›)
        next
          case False
          then have Xim: "X ∈ nsets (u ` V) (Suc r)"
            using X by (auto simp: nsets_def subset_insert)
          then have "u ` inv_into {..<p2} u ` X = X"
            using Vsub bij_betw_imp_inj_on u
            by (fastforce simp: nsets_def image_mono invinv_eq subset_trans)
          then show ?thesis
            using ione jone hj Xim invu_nsets unfolding h_def
            by (fastforce simp: image_subset_iff)
        qed
        moreover have "insert p (u ` V) ∈ nsets {..p} q2"
          by (simp add: ione inq1)
        ultimately show ?thesis
          by (metis ione image_subsetI insertI1 lessI nth_Cons_0 nth_Cons_Suc)
      next
        case jzero
        then have "u ` V ∈ nsets {..p} q1"
          using V u_nsets by auto
        moreover have "f ` nsets (u ` V) (Suc r) ⊆ {j}"
          using hj
          apply (clarsimp simp add: h_def image_subset_iff nsets_def)
          by (metis Zero_not_Suc card_eq_0_iff card_image subset_image_inj)
        ultimately show ?thesis
          using jzero not_less_eq by fastforce
      qed
    qed
  qed
  then show "?thesis"
    using lessThan_Suc lessThan_Suc_atMost
    by (auto simp: partn_lst_def monochromatic_def insert_commute)
qed

proposition ramsey2_full: "partn_lst {..<ES r q1 q2} [q1,q2] r"
proof (induction r arbitrary: q1 q2)
  case 0
  then show ?case
    by (auto simp: partn_lst_def monochromatic_def less_Suc_eq ex_in_conv nsets_eq_empty_iff)
next
  case (Suc r)
  note outer = this
  show ?case
  proof (cases "r = 0")
    case True
    then show ?thesis
      using ramsey1_explicit by (force simp: ES.simps)
  next
    case False
    then have "r > 0"
      by simp
    show ?thesis
      using Suc.prems
    proof (induct k ≡ "q1 + q2" arbitrary: q1 q2)
      case 0
      with partn_lst_0 show ?case by auto 
    next
      case (Suc k)
      consider "q1 = 0 ∨ q2 = 0" | "q1 ≠ 0" "q2 ≠ 0" by auto
      then show ?case
      proof cases
        case 1
        with False partn_lst_0 partn_lst_0' show ?thesis
          by blast
      next
        define p1 where "p1 ≡ ES (Suc r) (q1-1) q2"
        define p2 where "p2 ≡ ES (Suc r) q1 (q2-1)"
        define p where "p ≡ ES r p1 p2"
        case 2
        with Suc have "k = (q1-1) + q2" "k = q1 + (q2 - 1)" by auto
        then have p1: "partn_lst {..<p1} [q1-1,q2] (Suc r)"
              and p2: "partn_lst {..<p2} [q1,q2-1] (Suc r)"
          using Suc.hyps unfolding p1_def p2_def by blast+
        then have p: "partn_lst {..<p} [p1,p2] r"
          using outer Suc.prems unfolding p_def by auto
        show ?thesis
          using ramsey_induction_step [OF p1 p2 p] "2" ES.simps(2) False p1_def p2_def p_def by auto
      qed
    qed
  qed
qed

subsubsection ‹Full Ramsey's theorem with multiple colours and arbitrary exponents›

theorem ramsey_full: "∃N::nat. partn_lst {..<N} qs r"
proof (induction k ≡ "length qs" arbitrary: qs)
  case 0
  then show ?case
    by (rule_tac x=" r" in exI) (simp add: partn_lst_def)
next
  case (Suc k)
  note IH = this
  show ?case
  proof (cases k)
    case 0
    with Suc obtain q where "qs = [q]"
      by (metis length_0_conv length_Suc_conv)
    then show ?thesis
      by (rule_tac x=q in exI) (auto simp: partn_lst_def monochromatic_def funcset_to_empty_iff)
  next
    case (Suc k')
    then obtain q1 q2 l where qs: "qs = q1#q2#l"
      by (metis Suc.hyps(2) length_Suc_conv)
    then obtain q::nat where q: "partn_lst {..<q} [q1,q2] r"
      using ramsey2_full by blast
    then obtain p::nat where p: "partn_lst {..<p} (q#l) r"
      using IH ‹qs = q1 # q2 # l› by fastforce
    have keq: "Suc (length l) = k"
      using IH qs by auto
    show ?thesis
    proof (intro exI conjI)
      show "partn_lst {..<p} qs r"
      proof (auto simp: partn_lst_def)
        fix f
        assume f: "f ∈ nsets {..<p} r → {..<length qs}"
        define g where "g ≡ λX. if f X < Suc (Suc 0) then 0 else f X - Suc 0"
        have "g ∈ nsets {..<p} r → {..<k}"
          unfolding g_def using f Suc IH
          by (auto simp: Pi_def not_less)
        then obtain i U where i: "i < k" and gi: "g ` nsets U r ⊆ {i}"
                and U: "U ∈ nsets {..<p} ((q#l) ! i)"
          using p keq by (auto simp: partn_lst_def monochromatic_def)
        show "∃i<length qs. monochromatic {..<p} (qs!i) r f i"
        proof (cases "i = 0")
          case True
          then have "U ∈ nsets {..<p} q" and f01: "f ` nsets U r ⊆ {0, Suc 0}"
            using U gi unfolding g_def by (auto simp: image_subset_iff)
          then obtain u where u: "bij_betw u {..<q} U"
            using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp: nsets_def)
          then have Usub: "U ⊆ {..<p}"
            by (smt (verit) U mem_Collect_eq nsets_def)
          have u_nsets: "u ` X ∈ nsets {..<p} n" if "X ∈ nsets {..<q} n" for X n
          proof -
            have "inj_on u X"
              using u that bij_betw_imp_inj_on inj_on_subset
              by (force simp: nsets_def)
            then show ?thesis
              using Usub u that bij_betwE
              by (fastforce simp: nsets_def card_image)
          qed
          define h where "h ≡ λX. f (u ` X)"
          have "f (u ` X) < Suc (Suc 0)" if "X ∈ nsets {..<q} r" for X
          proof -
            have "u ` X ∈ nsets U r"
              using u u_nsets that by (auto simp: nsets_def bij_betwE subset_eq)
            then show ?thesis
              using f01 by auto
          qed
          then have "h ∈ nsets {..<q} r → {..<Suc (Suc 0)}"
            unfolding h_def by blast
          then obtain j V where j: "j < Suc (Suc 0)" and hj: "h ` nsets V r ⊆ {j}"
            and V: "V ∈ nsets {..<q} ([q1,q2] ! j)"
            using q by (auto simp: partn_lst_def monochromatic_def)
          show ?thesis
            unfolding monochromatic_def
          proof (intro exI conjI bexI)
            show "j < length qs"
              using Suc Suc.hyps(2) j by linarith
            have "nsets (u ` V) r ⊆ (λx. (u ` x)) ` nsets V r"
              apply (clarsimp simp add: nsets_def image_iff)
              by (metis card_eq_0_iff card_image image_is_empty subset_image_inj)
            then have "f ` nsets (u ` V) r ⊆ h ` nsets V r"
              by (auto simp: h_def)
            then show "f ` nsets (u ` V) r ⊆ {j}"
              using hj by auto
            show "(u ` V) ∈ nsets {..<p} (qs ! j)"
              using V j less_2_cases numeral_2_eq_2 qs u_nsets by fastforce
          qed
        next
          case False
          then have eq: "⋀A. ⟦A ∈ [U]⇗r⇖⟧ ⟹ f A = Suc i"
            by (metis Suc_pred diff_0_eq_0 g_def gi image_subset_iff not_gr0 singletonD)
          show ?thesis
            unfolding monochromatic_def
          proof (intro exI conjI bexI)
            show "Suc i < length qs"
              using Suc.hyps(2) i by auto
            show "f ` nsets U r ⊆ {Suc i}"
              using False by (auto simp: eq)
            show "U ∈ nsets {..<p} (qs ! (Suc i))"
              using False U qs by auto
          qed
        qed
      qed
    qed
  qed
qed

subsubsection ‹Simple graph version›

text ‹This is the most basic version in terms of cliques and independent
  sets, i.e. the version for graphs and 2 colours.
›

definition "clique V E ⟷ (∀v∈V. ∀w∈V. v ≠ w ⟶ {v, w} ∈ E)"
definition "indep V E ⟷ (∀v∈V. ∀w∈V. v ≠ w ⟶ {v, w} ∉ E)"

lemma clique_Un: "⟦clique K F; clique L F; ∀v∈K. ∀w∈L. v≠w ⟶ {v,w} ∈ F⟧ ⟹ clique (K ∪ L) F"
  by (metis UnE clique_def doubleton_eq_iff)

lemma null_clique[simp]: "clique {} E" and null_indep[simp]: "indep {} E"
  by (auto simp: clique_def indep_def)

lemma smaller_clique: "⟦clique R E; R' ⊆ R⟧ ⟹ clique R' E"
  by (auto simp: clique_def)

lemma smaller_indep: "⟦indep R E; R' ⊆ R⟧ ⟹ indep R' E"
  by (auto simp: indep_def)

lemma ramsey2:
  "∃r≥1. ∀(V::'a set) (E::'a set set). finite V ∧ card V ≥ r ⟶
    (∃R ⊆ V. card R = m ∧ clique R E ∨ card R = n ∧ indep R E)"
proof -
  obtain N where "N ≥ Suc 0" and N: "partn_lst {..<N} [m,n] 2"
    using ramsey2_full nat_le_linear partn_lst_greater_resource by blast
  have "∃R⊆V. card R = m ∧ clique R E ∨ card R = n ∧ indep R E"
    if "finite V" "N ≤ card V" for V :: "'a set" and E :: "'a set set"
  proof -
    from that
    obtain v where u: "inj_on v {..<N}" "v ` {..<N} ⊆ V"
      by (metis card_le_inj card_lessThan finite_lessThan)
    define f where "f ≡ λe. if v ` e ∈ E then 0 else Suc 0"
    have f: "f ∈ nsets {..<N} 2 → {..<Suc (Suc 0)}"
      by (simp add: f_def)
    then obtain i U where i: "i < 2" and gi: "f ` nsets U 2 ⊆ {i}"
      and U: "U ∈ nsets {..<N} ([m,n] ! i)"
      using N numeral_2_eq_2 by (auto simp: partn_lst_def monochromatic_def)
    show ?thesis
    proof (intro exI conjI)
      show "v ` U ⊆ V"
        using U u by (auto simp: image_subset_iff nsets_def)
      show "card (v ` U) = m ∧ clique (v ` U) E ∨ card (v ` U) = n ∧ indep (v ` U) E"
        using i unfolding numeral_2_eq_2
          using gi U u
          apply (simp add: image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq)
          apply (auto simp: f_def nsets_def card_image inj_on_subset split: if_split_asm)
          done
    qed
  qed
  then show ?thesis
    using ‹Suc 0 ≤ N› by auto
qed


subsection ‹Preliminaries for the infinitary version›

subsubsection ‹``Axiom'' of Dependent Choice›

primrec choice :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ nat ⇒ 'a"
  where ― ‹An integer-indexed chain of choices›
    choice_0: "choice P r 0 = (SOME x. P x)"
  | choice_Suc: "choice P r (Suc n) = (SOME y. P y ∧ (choice P r n, y) ∈ r)"

lemma choice_n:
  assumes P0: "P x0"
    and Pstep: "⋀x. P x ⟹ ∃y. P y ∧ (x, y) ∈ r"
  shows "P (choice P r n)"
proof (induct n)
  case 0
  show ?case by (force intro: someI P0)
next
  case Suc
  then show ?case by (auto intro: someI2_ex [OF Pstep])
qed

lemma dependent_choice:
  assumes trans: "trans r"
    and P0: "P x0"
    and Pstep: "⋀x. P x ⟹ ∃y. P y ∧ (x, y) ∈ r"
  obtains f :: "nat ⇒ 'a" where "⋀n. P (f n)" and "⋀n m. n < m ⟹ (f n, f m) ∈ r"
proof
  fix n
  show "P (choice P r n)"
    by (blast intro: choice_n [OF P0 Pstep])
next
  fix n m :: nat
  assume "n < m"
  from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) ∈ r" for k
    by (auto intro: someI2_ex)
  then show "(choice P r n, choice P r m) ∈ r"
    by (auto intro: less_Suc_induct [OF ‹n < m›] transD [OF trans])
qed


subsubsection ‹Partition functions›

definition part_fn :: "nat ⇒ nat ⇒ 'a set ⇒ ('a set ⇒ nat) ⇒ bool"
  ― ‹the function \<^term>‹f› partitions the \<^term>‹r›-subsets of the typically
      infinite set \<^term>‹Y› into \<^term>‹s› distinct categories.›
  where "part_fn r s Y f ⟷ (f ∈ nsets Y r → {..<s})"

text ‹For induction, we decrease the value of \<^term>‹r› in partitions.›
lemma part_fn_Suc_imp_part_fn:
  "⟦infinite Y; part_fn (Suc r) s Y f; y ∈ Y⟧ ⟹ part_fn r s (Y - {y}) (λu. f (insert y u))"
  by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert)

lemma part_fn_subset: "part_fn r s YY f ⟹ Y ⊆ YY ⟹ part_fn r s Y f"
  unfolding part_fn_def nsets_def by blast


subsection ‹Ramsey's Theorem: Infinitary Version›

lemma Ramsey_induction:
  fixes s r :: nat
    and YY :: "'a set"
    and f :: "'a set ⇒ nat"
  assumes "infinite YY" "part_fn r s YY f"
  shows "∃Y' t'. Y' ⊆ YY ∧ infinite Y' ∧ t' < s ∧ (∀X. X ⊆ Y' ∧ finite X ∧ card X = r ⟶ f X = t')"
  using assms
proof (induct r arbitrary: YY f)
  case 0
  then show ?case
    by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong)
next
  case (Suc r)
  show ?case
  proof -
    from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy ∈ YY"
      by blast
    let ?ramr = "{((y, Y, t), (y', Y', t')). y' ∈ Y ∧ Y' ⊆ Y}"
    let ?propr = "λ(y, Y, t).
                 y ∈ YY ∧ y ∉ Y ∧ Y ⊆ YY ∧ infinite Y ∧ t < s
                 ∧ (∀X. X⊆Y ∧ finite X ∧ card X = r ⟶ (f ∘ insert y) X = t)"
    from Suc.prems have infYY': "infinite (YY - {yy})" by auto
    from Suc.prems have partf': "part_fn r s (YY - {yy}) (f ∘ insert yy)"
      by (simp add: o_def part_fn_Suc_imp_part_fn yy)
    have transr: "trans ?ramr" by (force simp: trans_def)
    from Suc.hyps [OF infYY' partf']
    obtain Y0 and t0 where "Y0 ⊆ YY - {yy}" "infinite Y0" "t0 < s"
      "X ⊆ Y0 ∧ finite X ∧ card X = r ⟶ (f ∘ insert yy) X = t0" for X
      by blast
    with yy have propr0: "?propr(yy, Y0, t0)" by blast
    have proprstep: "∃y. ?propr y ∧ (x, y) ∈ ?ramr" if x: "?propr x" for x
    proof (cases x)
      case (fields yx Yx tx)
      with x obtain yx' where yx': "yx' ∈ Yx"
        by (blast dest: infinite_imp_nonempty)
      from fields x have infYx': "infinite (Yx - {yx'})" by auto
      with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f ∘ insert yx')"
        by (simp add: o_def part_fn_Suc_imp_part_fn part_fn_subset [where YY=YY and Y=Yx])
      from Suc.hyps [OF infYx' partfx'] obtain Y' and t'
        where Y': "Y' ⊆ Yx - {yx'}" "infinite Y'" "t' < s"
          "X ⊆ Y' ∧ finite X ∧ card X = r ⟶ (f ∘ insert yx') X = t'" for X
        by blast
      from fields x Y' yx' have "?propr (yx', Y', t') ∧ (x, (yx', Y', t')) ∈ ?ramr"
        by blast
      then show ?thesis ..
    qed
    from dependent_choice [OF transr propr0 proprstep]
    obtain g where pg: "?propr (g n)" and rg: "n < m ⟹ (g n, g m) ∈ ?ramr" for n m :: nat
      by blast
    let ?gy = "fst ∘ g"
    let ?gt = "snd ∘ snd ∘ g"
    have rangeg: "∃k. range ?gt ⊆ {..<k}"
    proof (intro exI subsetI)
      fix x
      assume "x ∈ range ?gt"
      then obtain n where "x = ?gt n" ..
      with pg [of n] show "x ∈ {..<s}" by (cases "g n") auto
    qed
    from rangeg have "finite (range ?gt)"
      by (simp add: finite_nat_iff_bounded)
    then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}"
      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
    with pg [of n'] have less': "s'<s" by (cases "g n'") auto
    have inj_gy: "inj ?gy"
    proof (rule linorder_injI)
      fix m m' :: nat
      assume "m < m'"
      from rg [OF this] pg [of m] show "?gy m ≠ ?gy m'"
        by (cases "g m", cases "g m'") auto
    qed
    show ?thesis
    proof (intro exI conjI)
      from pg show "?gy ` {n. ?gt n = s'} ⊆ YY"
        by (auto simp add: Let_def split_beta)
      from infeqs' show "infinite (?gy ` {n. ?gt n = s'})"
        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
      show "s' < s" by (rule less')
      show "∀X. X ⊆ ?gy ` {n. ?gt n = s'} ∧ finite X ∧ card X = Suc r ⟶ f X = s'"
      proof -
        have "f X = s'"
          if X: "X ⊆ ?gy ` {n. ?gt n = s'}"
          and cardX: "finite X" "card X = Suc r"
          for X
        proof -
          from X obtain AA where AA: "AA ⊆ {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
            by (auto simp add: subset_image_iff)
          with cardX have "AA ≠ {}" by auto
          then have AAleast: "(LEAST x. x ∈ AA) ∈ AA" by (auto intro: LeastI_ex)
          show ?thesis
          proof (cases "g (LEAST x. x ∈ AA)")
            case (fields ya Ya ta)
            with AAleast Xeq have ya: "ya ∈ X" by (force intro!: rev_image_eqI)
            then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
            also have "… = ta"
            proof -
              have *: "X - {ya} ⊆ Ya"
              proof
                fix x assume x: "x ∈ X - {ya}"
                then obtain a' where xeq: "x = ?gy a'" and a': "a' ∈ AA"
                  by (auto simp add: Xeq)
                with fields x have "a' ≠ (LEAST x. x ∈ AA)" by auto
                with Least_le [of "λx. x ∈ AA", OF a'] have "(LEAST x. x ∈ AA) < a'"
                  by arith
                from xeq fields rg [OF this] show "x ∈ Ya" by auto
              qed
              have "card (X - {ya}) = r"
                by (simp add: cardX ya)
              with pg [of "LEAST x. x ∈ AA"] fields cardX * show ?thesis
                by (auto simp del: insert_Diff_single)
            qed
            also from AA AAleast fields have "… = s'" by auto
            finally show ?thesis .
          qed
        qed
        then show ?thesis by blast
      qed
    qed
  qed
qed


theorem Ramsey:
  fixes s r :: nat
    and Z :: "'a set"
    and f :: "'a set ⇒ nat"
  shows
   "⟦infinite Z;
      ∀X. X ⊆ Z ∧ finite X ∧ card X = r ⟶ f X < s⟧
    ⟹ ∃Y t. Y ⊆ Z ∧ infinite Y ∧ t < s
            ∧ (∀X. X ⊆ Y ∧ finite X ∧ card X = r ⟶ f X = t)"
  by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def])

corollary Ramsey2:
  fixes s :: nat
    and Z :: "'a set"
    and f :: "'a set ⇒ nat"
  assumes infZ: "infinite Z"
    and part: "∀x∈Z. ∀y∈Z. x ≠ y ⟶ f {x, y} < s"
  shows "∃Y t. Y ⊆ Z ∧ infinite Y ∧ t < s ∧ (∀x∈Y. ∀y∈Y. x≠y ⟶ f {x, y} = t)"
proof -
  from part have part2: "∀X. X ⊆ Z ∧ finite X ∧ card X = 2 ⟶ f X < s"
    by (fastforce simp: eval_nat_numeral card_Suc_eq)
  obtain Y t where *:
    "Y ⊆ Z" "infinite Y" "t < s" "(∀X. X ⊆ Y ∧ finite X ∧ card X = 2 ⟶ f X = t)"
    by (insert Ramsey [OF infZ part2]) auto
  then have "∀x∈Y. ∀y∈Y. x ≠ y ⟶ f {x, y} = t" by auto
  with * show ?thesis by iprover
qed

corollary Ramsey_nsets:
  fixes f :: "'a set ⇒ nat"
  assumes "infinite Z" "f ` nsets Z r ⊆ {..<s}"
  obtains Y t where "Y ⊆ Z" "infinite Y" "t < s" "f ` nsets Y r ⊆ {t}"
  using Ramsey [of Z r f s] assms by (auto simp: nsets_def image_subset_iff)


subsection ‹Disjunctive Well-Foundedness›

text ‹
  An application of Ramsey's theorem to program termination. See
  \<^cite>‹"Podelski-Rybalchenko"›.
›

definition disj_wf :: "('a × 'a) set ⇒ bool"
  where "disj_wf r ⟷ (∃T. ∃n::nat. (∀i<n. wf (T i)) ∧ r = (⋃i<n. T i))"

definition transition_idx :: "(nat ⇒ 'a) ⇒ (nat ⇒ ('a × 'a) set) ⇒ nat set ⇒ nat"
  where "transition_idx s T A = (LEAST k. ∃i j. A = {i, j} ∧ i < j ∧ (s j, s i) ∈ T k)"


lemma transition_idx_less:
  assumes "i < j" "(s j, s i) ∈ T k" "k < n"
  shows "transition_idx s T {i, j} < n"
proof -
  from assms(1,2) have "transition_idx s T {i, j} ≤ k"
    by (simp add: transition_idx_def, blast intro: Least_le)
  with assms(3) show ?thesis by simp
qed

lemma transition_idx_in:
  assumes "i < j" "(s j, s i) ∈ T k"
  shows "(s j, s i) ∈ T (transition_idx s T {i, j})"
  using assms
  by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI)

text ‹To be equal to the union of some well-founded relations is equivalent
  to being the subset of such a union.›
lemma disj_wf: "disj_wf r ⟷ (∃T. ∃n::nat. (∀i<n. wf(T i)) ∧ r ⊆ (⋃i<n. T i))"
proof -
  have *: "⋀T n. ⟦∀i<n. wf (T i); r ⊆ ⋃ (T ` {..<n})⟧
           ⟹ (∀i<n. wf (T i ∩ r)) ∧ r = (⋃i<n. T i ∩ r)"
    by (force simp: wf_Int1)
  show ?thesis
    unfolding disj_wf_def by auto (metis "*")
qed

theorem trans_disj_wf_implies_wf:
  assumes "trans r"
    and "disj_wf r"
  shows "wf r"
proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
  assume "∃s. ∀i. (s (Suc i), s i) ∈ r"
  then obtain s where sSuc: "∀i. (s (Suc i), s i) ∈ r" ..
  from ‹disj_wf r› obtain T and n :: nat where wfT: "∀k<n. wf(T k)" and r: "r = (⋃k<n. T k)"
    by (auto simp add: disj_wf_def)
  have s_in_T: "∃k. (s j, s i) ∈ T k ∧ k<n" if "i < j" for i j
  proof -
    from ‹i < j› have "(s j, s i) ∈ r"
    proof (induct rule: less_Suc_induct)
      case 1
      then show ?case by (simp add: sSuc)
    next
      case 2
      with ‹trans r› show ?case
        unfolding trans_def by blast
    qed
    then show ?thesis by (auto simp add: r)
  qed
  have "i < j ⟹ transition_idx s T {i, j} < n" for i j
    using s_in_T transition_idx_less by blast
  then have trless: "i ≠ j ⟹ transition_idx s T {i, j} < n" for i j
    by (metis doubleton_eq_iff less_linear)
  have "∃K k. K ⊆ UNIV ∧ infinite K ∧ k < n ∧
      (∀i∈K. ∀j∈K. i ≠ j ⟶ transition_idx s T {i, j} = k)"
    by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
  then obtain K and k where infK: "infinite K" and "k < n"
    and allk: "∀i∈K. ∀j∈K. i ≠ j ⟶ transition_idx s T {i, j} = k"
    by auto
  have "(s (enumerate K (Suc m)), s (enumerate K m)) ∈ T k" for m :: nat
  proof -
    let ?j = "enumerate K (Suc m)"
    let ?i = "enumerate K m"
    have ij: "?i < ?j" by (simp add: enumerate_step infK)
    have "?j ∈ K" "?i ∈ K" by (simp_all add: enumerate_in_set infK)
    with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk)
    from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) ∈ T k'" "k'<n" by blast
    then show "(s ?j, s ?i) ∈ T k" by (simp add: k transition_idx_in ij)
  qed
  then have "¬ wf (T k)"
    unfolding wf_iff_no_infinite_down_chain by iprover
  with wfT ‹k < n› show False by blast
qed

end