--- a/src/HOL/Library/Ramsey.thy Tue Feb 27 14:08:28 2024 +0100
+++ b/src/HOL/Library/Ramsey.thy Tue Feb 27 14:57:48 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