# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1709045856 0
# Node ID d11cee9c3a7c24959ddaf4c14989ca250e3ad7b3
# Parent  6dbe7910dcfc72cd8b63b90b391335f33bd88024
Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers

diff -r 6dbe7910dcfc -r d11cee9c3a7c src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Feb 27 10:49:48 2024 +0100
+++ b/src/HOL/Library/Ramsey.thy	Tue Feb 27 14:57:36 2024 +0000
@@ -5,7 +5,7 @@
 section \<open>Ramsey's Theorem\<close>
 
 theory Ramsey
-  imports Infinite_Set FuncSet
+  imports Infinite_Set Equipollence FuncSet 
 begin
 
 subsection \<open>Preliminary definitions\<close>
@@ -194,7 +194,7 @@
   assumes "g \<in> S \<rightarrow> T" and "inj_on g S"
   shows "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>"
     using assms
-    by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset)
+    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 \<in> [T]\<^bsup>k\<^esup> \<rightarrow> D" and "g \<in> S \<rightarrow> T" and "inj_on g S"
@@ -206,14 +206,84 @@
     using f by fastforce
 qed
 
+subsubsection \<open>Further properties, involving equipollence\<close>
+
+lemma nsets_lepoll_cong:
+  assumes "A \<lesssim> B"
+  shows "[A]\<^bsup>k\<^esup> \<lesssim> [B]\<^bsup>k\<^esup>"
+proof -
+  obtain f where f: "inj_on f A" "f ` A \<subseteq> B"
+    by (meson assms lepoll_def)
+  define F where "F \<equiv> \<lambda>N. f ` N"
+  have "inj_on F ([A]\<^bsup>k\<^esup>)"
+    using F_def f inj_on_nsets by blast
+  moreover
+  have "F ` ([A]\<^bsup>k\<^esup>) \<subseteq> [B]\<^bsup>k\<^esup>"
+    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\<approx>B"
+  shows "[A]\<^bsup>k\<^esup> \<approx> [B]\<^bsup>k\<^esup>"
+  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]\<^bsup>k\<^esup>)"
+proof -
+  obtain B where "B \<subset> A" "A\<approx>B"
+    by (meson inf infinite_iff_psubset)
+  then obtain a where a: "a \<in> A" "a \<notin> B"
+    by blast
+  then obtain N where "N \<subseteq> B" "finite N" "card N = k-1" "a \<notin> N"
+    by (metis \<open>A \<approx> B\<close> inf eqpoll_finite_iff infinite_arbitrarily_large subset_eq)
+  with a \<open>k>0\<close> \<open>B \<subset> A\<close> have "insert a N \<in> [A]\<^bsup>k\<^esup>"
+    by (simp add: nsets_def)
+  with a have "nsets B k \<noteq> nsets A k"
+    by (metis (no_types, lifting) in_mono insertI1 mem_Collect_eq nsets_def)
+  moreover have "nsets B k \<subseteq> nsets A k"
+    using \<open>B \<subset> A\<close> nsets_mono by auto
+  ultimately show ?thesis
+    unfolding infinite_iff_psubset_le
+    by (meson \<open>A \<approx> B\<close> eqpoll_imp_lepoll nsets_eqpoll_cong psubsetI)
+qed
+
+lemma finite_nsets_iff:
+  assumes "k>0"
+  shows "finite ([A]\<^bsup>k\<^esup>) \<longleftrightarrow> 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 \<open>Partition predicates\<close>
 
+definition "monochromatic \<equiv> \<lambda>\<beta> \<alpha> \<gamma> f i. \<exists>H \<in> nsets \<beta> \<alpha>. f ` (nsets H \<gamma>) \<subseteq> {i}"
+
+text \<open>uniform partition sizes\<close>
 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "partn \<beta> \<alpha> \<gamma> \<delta> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma>  \<rightarrow>  \<delta>. \<exists>H \<in> nsets \<beta> \<alpha>. \<exists>\<xi>\<in>\<delta>. f ` (nsets H \<gamma>) \<subseteq> {\<xi>}"
+  where "partn \<beta> \<alpha> \<gamma> \<delta> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma>  \<rightarrow>  \<delta>. \<exists>\<xi>\<in>\<delta>. monochromatic \<beta> \<alpha> \<gamma> f \<xi>"
 
+text \<open>partition sizes enumerated in a list\<close>
 definition partn_lst :: "'a set \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
-  where "partn_lst \<beta> \<alpha> \<gamma> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma>  \<rightarrow>  {..<length \<alpha>}.
-              \<exists>i < length \<alpha>. \<exists>H \<in> nsets \<beta> (\<alpha>!i). f ` (nsets H \<gamma>) \<subseteq> {i}"
+  where "partn_lst \<beta> \<alpha> \<gamma> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma>  \<rightarrow>  {..<length \<alpha>}. \<exists>i < length \<alpha>. monochromatic \<beta> (\<alpha>!i) \<gamma> f i"
+
+text \<open>There's always a 0-clique\<close>
+lemma partn_lst_0: "\<gamma> > 0 \<Longrightarrow> partn_lst \<beta> (0#\<alpha>) \<gamma>"
+  by (force simp: partn_lst_def monochromatic_def nsets_empty_iff)
+
+lemma partn_lst_0': "\<gamma> > 0 \<Longrightarrow> partn_lst \<beta> (a#0#\<alpha>) \<gamma>"
+  by (force simp: partn_lst_def monochromatic_def nsets_empty_iff)
 
 lemma partn_lst_greater_resource:
   fixes M::nat
@@ -225,11 +295,11 @@
   then have "f \<in> nsets {..<M} \<gamma> \<rightarrow> {..<length \<alpha>}"
     by (meson Pi_anti_mono \<open>M \<le> N\<close> lessThan_subset_iff nsets_mono subsetD)
   then obtain i H where i: "i < length \<alpha>" and H: "H \<in> nsets {..<M} (\<alpha> ! i)" and subi: "f ` nsets H \<gamma> \<subseteq> {i}"
-    using M partn_lst_def by blast
+    using M unfolding partn_lst_def monochromatic_def by blast
   have "H \<in> nsets {..<N} (\<alpha> ! i)"
     using \<open>M \<le> N\<close> H by (auto simp: nsets_def subset_iff)
-  then show "\<exists>i<length \<alpha>. \<exists>H\<in>nsets {..<N} (\<alpha> ! i). f ` nsets H \<gamma> \<subseteq> {i}"
-    using i subi by blast
+  then show "\<exists>i<length \<alpha>. monochromatic {..<N} (\<alpha>!i) \<gamma> f i"
+    using i subi unfolding monochromatic_def by blast
 qed
 
 lemma partn_lst_fewer_colours:
@@ -242,8 +312,8 @@
       and H: "H \<in> [\<beta>]\<^bsup>((n # \<alpha>) ! i)\<^esup>"
       and hom: "\<forall>x\<in>[H]\<^bsup>\<gamma>\<^esup>. Suc (f x) = i"
     using \<open>n \<ge> \<gamma>\<close> major [unfolded partn_lst_def, rule_format, of "Suc o f"]
-    by (fastforce simp: image_subset_iff nsets_eq_empty_iff)
-  show "\<exists>i<length \<alpha>. \<exists>H\<in>nsets \<beta> (\<alpha> ! i). f ` [H]\<^bsup>\<gamma>\<^esup> \<subseteq> {i}"
+    by (fastforce simp: image_subset_iff nsets_eq_empty_iff monochromatic_def)
+  show "\<exists>i<length \<alpha>. monochromatic \<beta> (\<alpha>!i) \<gamma> f i"
   proof (cases i)
     case 0
     then have "[H]\<^bsup>\<gamma>\<^esup> = {}"
@@ -254,7 +324,7 @@
   next
     case (Suc i')
     then show ?thesis
-      using i H hom by auto
+      unfolding monochromatic_def using i H hom by auto
   qed
 qed
 
@@ -265,7 +335,7 @@
 lemma partn_lstE:
   assumes "partn_lst \<beta> \<alpha> \<gamma>" "f \<in> nsets \<beta> \<gamma>  \<rightarrow>  {..<l}" "length \<alpha> = l"
   obtains i H where "i < length \<alpha>" "H \<in> nsets \<beta> (\<alpha>!i)" "f ` (nsets H \<gamma>) \<subseteq> {i}"
-  using partn_lst_def assms by blast
+  using partn_lst_def monochromatic_def assms by metis
 
 lemma partn_lst_less:
   assumes M: "partn_lst \<beta> \<alpha> n" and eq: "length \<alpha>' = length \<alpha>" 
@@ -277,13 +347,14 @@
   then obtain i H where i: "i < length \<alpha>"
                    and "H \<subseteq> \<beta>"  and H: "card H = (\<alpha>!i)" and "finite H"
                    and fi: "f ` nsets H n \<subseteq> {i}"
-    using assms by (auto simp: partn_lst_def nsets_def)
+    using assms by (auto simp: partn_lst_def monochromatic_def nsets_def)
   then obtain bij where bij: "bij_betw bij H {0..<\<alpha>!i}"
     by (metis ex_bij_betw_finite_nat)
   then have inj: "inj_on (inv_into H bij) {0..<\<alpha>' ! 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..<\<alpha>'!i}"
-  show "\<exists>i<length \<alpha>'. \<exists>H\<in>[\<beta>]\<^bsup>(\<alpha>' ! i)\<^esup>. f ` [H]\<^bsup>n\<^esup> \<subseteq> {i}"
+  show "\<exists>i<length \<alpha>'. monochromatic \<beta> (\<alpha>'!i) n f i"
+    unfolding monochromatic_def
   proof (intro exI bexI conjI)
     show "i < length \<alpha>'"
       by (simp add: assms(2) i)
@@ -306,51 +377,298 @@
 
 text \<open>
   To distinguish the finite and infinite ones, lower and upper case
-  names are used.
+  names are used (ramsey vs Ramsey).
 \<close>
 
+subsubsection \<open>The Erdős--Szekeres theorem exhibits an upper bound for Ramsey numbers\<close>
+
+text \<open>The Erdős--Szekeres bound, essentially extracted from the proof\<close>
+fun ES :: "[nat,nat,nat] \<Rightarrow> 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 \<or> 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 \<or> 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 \<open>The Erdős--Szekeres upper bound\<close>
+lemma ES2_choose: "ES 2 k l = (k+l) choose k"
+proof (induct n \<equiv> "k+l" arbitrary: k l)
+  case 0
+  then show ?case
+    by (auto simp: ES_2)
+next
+  case (Suc n)
+  then have "k>0 \<Longrightarrow> l>0 \<Longrightarrow> 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 \<open>Trivial cases\<close>
 
 text \<open>Vacuous, since we are dealing with 0-sets!\<close>
 lemma ramsey0: "\<exists>N::nat. partn_lst {..<N} [q1,q2] 0"
-  by (force simp: partn_lst_def ex_in_conv less_Suc_eq nsets_eq_empty_iff)
+  by (force simp: partn_lst_def monochromatic_def ex_in_conv less_Suc_eq nsets_eq_empty_iff)
 
 text \<open>Just the pigeon hole principle, since we are dealing with 1-sets\<close>
-lemma ramsey1: "\<exists>N::nat. partn_lst {..<N} [q0,q1] 1"
+lemma ramsey1_explicit: "partn_lst {..<q0 + q1 - Suc 0} [q0,q1] 1"
 proof -
-  have "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..<Suc (q0 + q1)} ([q0, q1] ! i). f ` nsets H (Suc 0) \<subseteq> {i}"
-    if "f \<in> nsets {..<Suc (q0 + q1)} (Suc 0) \<rightarrow> {..<Suc (Suc 0)}" for f
+  have "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..<q0 + q1 - 1} ([q0, q1] ! i). f ` nsets H 1 \<subseteq> {i}"
+    if "f \<in> nsets {..<q0 + q1 - 1} (Suc 0) \<rightarrow> {..<Suc (Suc 0)}" for f
   proof -
-    define A where "A \<equiv> \<lambda>i. {q. q \<le> q0+q1 \<and> f {q} = i}"
-    have "A 0 \<union> A 1 = {..q0 + q1}"
+    define A where "A \<equiv> \<lambda>i. {q. q < q0+q1-1 \<and> f {q} = i}"
+    have "A 0 \<union> 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 \<inter> A 1 = {}"
       by (auto simp: A_def)
-    ultimately have "q0 + q1 \<le> card (A 0) + card (A 1)"
-      by (metis card_Un_le card_atMost eq_imp_le le_SucI le_trans)
+    ultimately have "q0 + q1 \<le> card (A 0) + card (A 1) + 1"
+      by (metis card_Un_le card_lessThan le_diff_conv)
     then consider "card (A 0) \<ge> q0" | "card (A 1) \<ge> q1"
       by linarith
     then obtain i where "i < Suc (Suc 0)" "card (A i) \<ge> [q0, q1] ! i"
       by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc)
     then obtain B where "B \<subseteq> A i" "card B = [q0, q1] ! i" "finite B"
       by (meson obtain_subset_with_card_n)
-    then have "B \<in> nsets {..<Suc (q0 + q1)} ([q0, q1] ! i) \<and> f ` nsets B (Suc 0) \<subseteq> {i}"
+    then have "B \<in> nsets {..<q0 + q1 - 1} ([q0, q1] ! i) \<and> f ` nsets B (Suc 0) \<subseteq> {i}"
       by (auto simp: A_def nsets_def card_1_singleton_iff)
     then show ?thesis
       using \<open>i < Suc (Suc 0)\<close> by auto
   qed
   then show ?thesis
-    by (clarsimp simp: partn_lst_def) blast
+    by (simp add: partn_lst_def monochromatic_def)
 qed
 
+lemma ramsey1: "\<exists>N::nat. partn_lst {..<N} [q0,q1] 1"
+  using ramsey1_explicit by blast
+
 
-subsubsection \<open>Ramsey's theorem with two colours and arbitrary exponents (hypergraph version)\<close>
+subsubsection \<open>Ramsey's theorem with TWO colours and arbitrary exponents (hypergraph version)\<close>
 
-proposition ramsey2_full: "\<exists>N::nat. partn_lst {..<N} [q1,q2] r"
+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 "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) \<subseteq> {i}"
+    if f: "f \<in> nsets {..p} (Suc r) \<rightarrow> {..<Suc (Suc 0)}" for f
+  proof -
+    define g where "g \<equiv> \<lambda>R. f (insert p R)"
+    have "f (insert p i) \<in> {..<Suc (Suc 0)}" if "i \<in> nsets {..<p} r" for i
+      using that card_insert_if by (fastforce simp: nsets_def intro!: Pi_mem [OF f])
+    then have g: "g \<in> nsets {..<p} r \<rightarrow> {..<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 \<subseteq> {i}"
+      and U: "U \<in> nsets {..<p} ([p1, p2] ! i)"
+      using p by (auto simp: partn_lst_def monochromatic_def)
+    then have Usub: "U \<subseteq> {..<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 \<in> 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 \<in> nsets {..p} n" if "X \<in> 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 \<equiv> \<lambda>R. f (u ` R)"
+      have "h \<in> nsets {..<p1} (Suc r) \<rightarrow> {..<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) \<subseteq> {j}"
+        and V: "V \<in> nsets {..<p1} ([q1 - Suc 0, q2] ! j)"
+        using p1 by (auto simp: partn_lst_def monochromatic_def)
+      then have Vsub: "V \<subseteq> {..<p1}"
+        by (auto simp: nsets_def)
+      have invinv_eq: "u ` inv_into {..<p1} u ` X = X" if "X \<subseteq> 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 \<in> nsets {..<p1} (q1 - Suc 0)"
+          using V by simp
+        then have "u ` V \<in> 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 \<in> nsets {..p} q1"
+          unfolding nsets_def using \<open>q1 > 0\<close> card_insert_if by fastforce
+        have invu_nsets: "inv_into {..<p1} u ` X \<in> nsets V r"
+          if "X \<in> nsets (u ` V) r" for X r
+        proof -
+          have "X \<subseteq> u ` V \<and> finite X \<and> 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 \<in> nsets ?W (Suc r)" for X
+        proof (cases "p \<in> X")
+          case True
+          then have Xp: "X - {p} \<in> nsets (u ` V) r"
+            using X by (auto simp: nsets_def)
+          moreover have "u ` V \<subseteq> U"
+            using Vsub bij_betwE u by blast
+          ultimately have "X - {p} \<in> 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 \<open>X - {p} \<in> nsets U r\<close> insert_Diff
+            by (fastforce simp: g_def image_subset_iff)
+          then show ?thesis
+            by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>)
+        next
+          case False
+          then have Xim: "X \<in> 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) \<in> 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 \<in> nsets {..p} q2"
+          using V u_nsets by auto
+        moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {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 \<in> 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 \<in> nsets {..p} n" if "X \<in> 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 \<equiv> \<lambda>R. f (u ` R)"
+      have "h \<in> nsets {..<p2} (Suc r) \<rightarrow> {..<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) \<subseteq> {j}"
+        and V: "V \<in> nsets {..<p2} ([q1, q2 - Suc 0] ! j)"
+        using p2 by (auto simp: partn_lst_def monochromatic_def)
+      then have Vsub: "V \<subseteq> {..<p2}"
+        by (auto simp: nsets_def)
+      have invinv_eq: "u ` inv_into {..<p2} u ` X = X" if "X \<subseteq> 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 \<in> nsets {..<p2} (q2 - Suc 0)"
+          using V by simp
+        then have "u ` V \<in> 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 \<in> nsets {..p} q2"
+          unfolding nsets_def using \<open>q2 > 0\<close> card_insert_if by fastforce
+        have invu_nsets: "inv_into {..<p2} u ` X \<in> nsets V r"
+          if "X \<in> nsets (u ` V) r" for X r
+        proof -
+          have "X \<subseteq> u ` V \<and> finite X \<and> 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 \<in> nsets ?W (Suc r)" for X
+        proof (cases "p \<in> X")
+          case True
+          then have Xp: "X - {p} \<in> nsets (u ` V) r"
+            using X by (auto simp: nsets_def)
+          moreover have "u ` V \<subseteq> U"
+            using Vsub bij_betwE u by blast
+          ultimately have "X - {p} \<in> 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 \<open>X - {p} \<in> nsets U r\<close> insert_Diff
+            by (fastforce simp: g_def image_subset_iff)
+          then show ?thesis
+            by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>)
+        next
+          case False
+          then have Xim: "X \<in> 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) \<in> 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 \<in> nsets {..p} q1"
+          using V u_nsets by auto
+        moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {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 (simp add: ramsey0)
+    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
@@ -358,7 +676,7 @@
   proof (cases "r = 0")
     case True
     then show ?thesis
-      using ramsey1 by auto
+      using ramsey1_explicit by (force simp: ES.simps)
   next
     case False
     then have "r > 0"
@@ -367,231 +685,28 @@
       using Suc.prems
     proof (induct k \<equiv> "q1 + q2" arbitrary: q1 q2)
       case 0
-      show ?case
-      proof
-        show "partn_lst {..<1::nat} [q1, q2] (Suc r)"
-          using nsets_empty_iff subset_insert 0
-          by (fastforce simp: partn_lst_def funcset_to_empty_iff nsets_eq_empty image_subset_iff)
-      qed
+      with partn_lst_0 show ?case by auto 
     next
       case (Suc k)
       consider "q1 = 0 \<or> q2 = 0" | "q1 \<noteq> 0" "q2 \<noteq> 0" by auto
       then show ?case
       proof cases
         case 1
-        then have "partn_lst {..< Suc 0} [q1, q2] (Suc r)"
-          unfolding partn_lst_def using \<open>r > 0\<close>
-          by (fastforce simp add: nsets_empty_iff nsets_singleton_iff lessThan_Suc)
-        then show ?thesis by blast
+        with False partn_lst_0 partn_lst_0' show ?thesis
+          by blast
       next
+        define p1 where "p1 \<equiv> ES (Suc r) (q1-1) q2"
+        define p2 where "p2 \<equiv> ES (Suc r) q1 (q2-1)"
+        define p where "p \<equiv> ES r p1 p2"
         case 2
-        with Suc have "k = (q1 - 1) + q2" "k = q1 + (q2 - 1)" by auto
-        then obtain p1 p2::nat where  p1: "partn_lst {..<p1} [q1-1,q2] (Suc r)" and p2: "partn_lst {..<p2} [q1,q2-1] (Suc r)"
-          using Suc.hyps by blast
-        then obtain p::nat where p: "partn_lst {..<p} [p1,p2] r"
-          using outer Suc.prems by auto
+        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
-        proof (intro exI conjI)
-          have "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) \<subseteq> {i}"
-            if f: "f \<in> nsets {..p} (Suc r) \<rightarrow> {..<Suc (Suc 0)}" for f
-          proof -
-            define g where "g \<equiv> \<lambda>R. f (insert p R)"
-            have "f (insert p i) \<in> {..<Suc (Suc 0)}" if "i \<in> nsets {..<p} r" for i
-              using that card_insert_if by (fastforce simp: nsets_def intro!: Pi_mem [OF f])
-            then have g: "g \<in> nsets {..<p} r \<rightarrow> {..<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 \<subseteq> {i}"
-              and U: "U \<in> nsets {..<p} ([p1, p2] ! i)"
-              using p by (auto simp: partn_lst_def)
-            then have Usub: "U \<subseteq> {..<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 \<in> 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 add: nsets_def)
-              have u_nsets: "u ` X \<in> nsets {..p} n" if "X \<in> 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 add: nsets_def card_image)
-              qed
-              define h where "h \<equiv> \<lambda>R. f (u ` R)"
-              have "h \<in> nsets {..<p1} (Suc r) \<rightarrow> {..<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) \<subseteq> {j}"
-                and V: "V \<in> nsets {..<p1} ([q1 - Suc 0, q2] ! j)"
-                using p1 by (auto simp: partn_lst_def)
-              then have Vsub: "V \<subseteq> {..<p1}"
-                by (auto simp: nsets_def)
-              have invinv_eq: "u ` inv_into {..<p1} u ` X = X" if "X \<subseteq> 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 \<in> nsets {..<p1} (q1 - Suc 0)"
-                  using V by simp
-                then have "u ` V \<in> 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 \<in> nsets {..p} q1"
-                  unfolding nsets_def using \<open>q1 \<noteq> 0\<close> card_insert_if by fastforce
-                have invu_nsets: "inv_into {..<p1} u ` X \<in> nsets V r"
-                  if "X \<in> nsets (u ` V) r" for X r
-                proof -
-                  have "X \<subseteq> u ` V \<and> finite X \<and> 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 \<in> nsets ?W (Suc r)" for X
-                proof (cases "p \<in> X")
-                  case True
-                  then have Xp: "X - {p} \<in> nsets (u ` V) r"
-                    using X by (auto simp: nsets_def)
-                  moreover have "u ` V \<subseteq> U"
-                    using Vsub bij_betwE u by blast
-                  ultimately have "X - {p} \<in> 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 \<open>X - {p} \<in> nsets U r\<close> insert_Diff
-                    by (fastforce simp add: g_def image_subset_iff)
-                  then show ?thesis
-                    by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>)
-                next
-                  case False
-                  then have Xim: "X \<in> 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 add: image_subset_iff)
-                qed
-                moreover have "insert p (u ` V) \<in> 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 \<in> nsets {..p} q2"
-                  using V u_nsets by auto
-                moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {j}"
-                  using hj
-                  by (force simp add: 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 \<in> 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 add: nsets_def)
-              have u_nsets: "u ` X \<in> nsets {..p} n" if "X \<in> 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 add: nsets_def card_image)
-              qed
-              define h where "h \<equiv> \<lambda>R. f (u ` R)"
-              have "h \<in> nsets {..<p2} (Suc r) \<rightarrow> {..<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) \<subseteq> {j}"
-                and V: "V \<in> nsets {..<p2} ([q1, q2 - Suc 0] ! j)"
-                using p2 by (auto simp: partn_lst_def)
-              then have Vsub: "V \<subseteq> {..<p2}"
-                by (auto simp: nsets_def)
-              have invinv_eq: "u ` inv_into {..<p2} u ` X = X" if "X \<subseteq> 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 \<in> nsets {..<p2} (q2 - Suc 0)"
-                  using V by simp
-                then have "u ` V \<in> 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 \<in> nsets {..p} q2"
-                  unfolding nsets_def using \<open>q2 \<noteq> 0\<close> card_insert_if by fastforce
-                have invu_nsets: "inv_into {..<p2} u ` X \<in> nsets V r"
-                  if "X \<in> nsets (u ` V) r" for X r
-                proof -
-                  have "X \<subseteq> u ` V \<and> finite X \<and> 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 \<in> nsets ?W (Suc r)" for X
-                proof (cases "p \<in> X")
-                  case True
-                  then have Xp: "X - {p} \<in> nsets (u ` V) r"
-                    using X by (auto simp: nsets_def)
-                  moreover have "u ` V \<subseteq> U"
-                    using Vsub bij_betwE u by blast
-                  ultimately have "X - {p} \<in> 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 \<open>X - {p} \<in> nsets U r\<close> insert_Diff
-                    by (fastforce simp add: g_def image_subset_iff)
-                  then show ?thesis
-                    by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>)
-                next
-                  case False
-                  then have Xim: "X \<in> 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 add: image_subset_iff)
-                qed
-                moreover have "insert p (u ` V) \<in> 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 \<in> nsets {..p} q1"
-                  using V u_nsets by auto
-                moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {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 "partn_lst {..<Suc p} [q1,q2] (Suc r)"
-            using lessThan_Suc lessThan_Suc_atMost by (auto simp: partn_lst_def insert_commute)
-        qed
+          using ramsey_induction_step [OF p1 p2 p] "2" ES.simps(2) False p1_def p2_def p_def by auto
       qed
     qed
   qed
@@ -613,7 +728,7 @@
     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 funcset_to_empty_iff)
+      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"
@@ -636,14 +751,14 @@
           by (auto simp: Pi_def not_less)
         then obtain i U where i: "i < k" and gi: "g ` nsets U r \<subseteq> {i}"
                 and U: "U \<in> nsets {..<p} ((q#l) ! i)"
-          using p keq by (auto simp: partn_lst_def)
-        show "\<exists>i<length qs. \<exists>H\<in>nsets {..<p} (qs ! i). f ` nsets H r \<subseteq> {i}"
+          using p keq by (auto simp: partn_lst_def monochromatic_def)
+        show "\<exists>i<length qs. monochromatic {..<p} (qs!i) r f i"
         proof (cases "i = 0")
           case True
           then have "U \<in> nsets {..<p} q" and f01: "f ` nsets U r \<subseteq> {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 add: nsets_def)
+            using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp: nsets_def)
           then have Usub: "U \<subseteq> {..<p}"
             by (smt (verit) U mem_Collect_eq nsets_def)
           have u_nsets: "u ` X \<in> nsets {..<p} n" if "X \<in> nsets {..<q} n" for X n
@@ -653,7 +768,7 @@
               by (force simp: nsets_def)
             then show ?thesis
               using Usub u that bij_betwE
-              by (fastforce simp add: nsets_def card_image)
+              by (fastforce simp: nsets_def card_image)
           qed
           define h where "h \<equiv> \<lambda>X. f (u ` X)"
           have "f (u ` X) < Suc (Suc 0)" if "X \<in> nsets {..<q} r" for X
@@ -667,8 +782,9 @@
             unfolding h_def by blast
           then obtain j V where j: "j < Suc (Suc 0)" and hj: "h ` nsets V r \<subseteq> {j}"
             and V: "V \<in> nsets {..<q} ([q1,q2] ! j)"
-            using q by (auto simp: partn_lst_def)
+            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
@@ -684,14 +800,15 @@
           qed
         next
           case False
+          then have eq: "\<And>A. \<lbrakk>A \<in> [U]\<^bsup>r\<^esup>\<rbrakk> \<Longrightarrow> 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 \<subseteq> {Suc i}"
-              using i gi False
-              apply (auto simp: g_def image_subset_iff)
-              by (metis Suc_lessD Suc_pred g_def gi image_subset_iff not_less_eq singleton_iff)
+              using False by (auto simp: eq)
             show "U \<in> nsets {..<p} (qs ! (Suc i))"
               using False U qs by auto
           qed
@@ -710,6 +827,18 @@
 definition "clique V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<in> E)"
 definition "indep V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<notin> E)"
 
+lemma clique_Un: "\<lbrakk>clique K F; clique L F; \<forall>v\<in>K. \<forall>w\<in>L. v\<noteq>w \<longrightarrow> {v,w} \<in> F\<rbrakk> \<Longrightarrow> clique (K \<union> 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: "\<lbrakk>clique R E; R' \<subseteq> R\<rbrakk> \<Longrightarrow> clique R' E"
+  by (auto simp: clique_def)
+
+lemma smaller_indep: "\<lbrakk>indep R E; R' \<subseteq> R\<rbrakk> \<Longrightarrow> indep R' E"
+  by (auto simp: indep_def)
+
 lemma ramsey2:
   "\<exists>r\<ge>1. \<forall>(V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
     (\<exists>R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
@@ -727,7 +856,7 @@
       by (simp add: f_def)
     then obtain i U where i: "i < 2" and gi: "f ` nsets U 2 \<subseteq> {i}"
       and U: "U \<in> nsets {..<N} ([m,n] ! i)"
-      using N numeral_2_eq_2 by (auto simp: partn_lst_def)
+      using N numeral_2_eq_2 by (auto simp: partn_lst_def monochromatic_def)
     show ?thesis
     proof (intro exI conjI)
       show "v ` U \<subseteq> V"
@@ -745,7 +874,7 @@
 qed
 
 
-subsection \<open>Preliminaries\<close>
+subsection \<open>Preliminaries for the infinitary version\<close>
 
 subsubsection \<open>``Axiom'' of Dependent Choice\<close>
 
@@ -827,7 +956,7 @@
     from Suc.prems have infYY': "infinite (YY - {yy})" by auto
     from Suc.prems have partf': "part_fn r s (YY - {yy}) (f \<circ> insert yy)"
       by (simp add: o_def part_fn_Suc_imp_part_fn yy)
-    have transr: "trans ?ramr" by (force simp add: trans_def)
+    have transr: "trans ?ramr" by (force simp: trans_def)
     from Suc.hyps [OF infYY' partf']
     obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
       "X \<subseteq> Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0" for X
@@ -944,7 +1073,7 @@
   shows "\<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s \<and> (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y \<longrightarrow> f {x, y} = t)"
 proof -
   from part have part2: "\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = 2 \<longrightarrow> f X < s"
-    by (fastforce simp add: eval_nat_numeral card_Suc_eq)
+    by (fastforce simp: eval_nat_numeral card_Suc_eq)
   obtain Y t where *:
     "Y \<subseteq> Z" "infinite Y" "t < s" "(\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = 2 \<longrightarrow> f X = t)"
     by (insert Ramsey [OF infZ part2]) auto
@@ -994,7 +1123,7 @@
 proof -
   have *: "\<And>T n. \<lbrakk>\<forall>i<n. wf (T i); r \<subseteq> \<Union> (T ` {..<n})\<rbrakk>
            \<Longrightarrow> (\<forall>i<n. wf (T i \<inter> r)) \<and> r = (\<Union>i<n. T i \<inter> r)"
-    by (force simp add: wf_Int1)
+    by (force simp: wf_Int1)
   show ?thesis
     unfolding disj_wf_def by auto (metis "*")
 qed