new lemmas involving Ramsey numbers, infinite sets

--- a/src/HOL/Library/Equipollence.thy	Fri Feb 09 16:43:43 2024 +0000
+++ b/src/HOL/Library/Equipollence.thy	Sun Feb 11 12:52:14 2024 +0000
@@ -747,6 +747,8 @@
   "finite(I \<rightarrow>\<^sub>E S) \<longleftrightarrow> (\<exists>a. S \<subseteq> {a}) \<or> I = {} \<or> finite I \<and> finite S"
   by (fastforce simp: finite_PiE_iff PiE_eq_empty_iff dest: subset_singletonD)
 
+subsection \<open>Misc other resultd\<close>
+
 lemma lists_lepoll_mono:
   assumes "A \<lesssim> B" shows "lists A \<lesssim> lists B"
 proof -
@@ -762,4 +764,37 @@
 lemma lepoll_lists: "A \<lesssim> lists A"
   unfolding lepoll_def inj_on_def by(rule_tac x="\<lambda>x. [x]" in exI) auto
 
+text \<open>Dedekind's definition of infinite set\<close>
+
+lemma infinite_iff_psubset: "infinite A \<longleftrightarrow> (\<exists>B. B \<subset> A \<and> A\<approx>B)"
+proof
+  assume "infinite A"
+  then obtain f :: "nat \<Rightarrow> 'a" where "inj f" and f: "range f \<subseteq> A"
+    by (meson infinite_countable_subset)
+  define C where "C \<equiv> A - range f"
+  have C: "A = range f \<union> C" "range f \<inter> C = {}"
+    using f by (auto simp: C_def)
+  have *: "range (f \<circ> Suc) \<subset> range f"
+    using inj_eq [OF \<open>inj f\<close>] by (fastforce simp: set_eq_iff)
+  have "range f \<union> C \<approx> range (f \<circ> Suc) \<union> C"
+  proof (intro Un_eqpoll_cong)
+    show "range f \<approx> range (f \<circ> Suc)"
+      by (meson \<open>inj f\<close> eqpoll_refl inj_Suc inj_compose inj_on_image_eqpoll_2)
+    show "disjnt (range f) C"
+      by (simp add: C disjnt_def)
+    then show "disjnt (range (f \<circ> Suc)) C"
+      using "*" disjnt_subset1 by blast
+  qed auto
+  moreover have "range (f \<circ> Suc) \<union> C \<subset> A"
+    using "*" f C_def by blast
+  ultimately show "\<exists>B\<subset>A. A \<approx> B"
+    by (metis C(1))
+next
+  assume "\<exists>B\<subset>A. A \<approx> B" then show "infinite A"
+    by (metis card_subset_eq eqpoll_finite_iff eqpoll_iff_card psubsetE)
+qed
+
+lemma infinite_iff_psubset_le: "infinite A \<longleftrightarrow> (\<exists>B. B \<subset> A \<and> A \<lesssim> B)"
+  by (meson eqpoll_imp_lepoll infinite_iff_psubset lepoll_antisym psubsetE subset_imp_lepoll)
+
 end

--- a/src/HOL/Library/Ramsey.thy	Fri Feb 09 16:43:43 2024 +0000
+++ b/src/HOL/Library/Ramsey.thy	Sun Feb 11 12:52:14 2024 +0000
@@ -18,6 +18,9 @@
 definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999)
   where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}"
 
+lemma finite_imp_finite_nsets: "finite A \<Longrightarrow> finite ([A]\<^bsup>k\<^esup>)"
+  by (simp add: nsets_def)
+
 lemma nsets_mono: "A \<subseteq> B \<Longrightarrow> nsets A n \<subseteq> nsets B n"
   by (auto simp: nsets_def)
 
@@ -27,6 +30,11 @@
 lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
   by (auto simp: nsets_def card_2_iff)
 
+lemma nsets2_E:
+  assumes "e \<in> [A]\<^bsup>2\<^esup>"
+  obtains x y where "e = {x,y}" "x \<in> A" "y \<in> A" "x\<noteq>y"
+  using assms by (auto simp: nsets_def card_2_iff)
+
 lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})"
   by (auto simp: nsets_2_eq)
 
@@ -254,6 +262,45 @@
   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 \<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
+
+lemma partn_lst_less:
+  assumes M: "partn_lst \<beta> \<alpha> n" and eq: "length \<alpha>' = length \<alpha>" 
+    and le: "\<And>i. i < length \<alpha> \<Longrightarrow> \<alpha>'!i \<le> \<alpha>!i "
+  shows "partn_lst \<beta> \<alpha>' n"
+proof (clarsimp simp: partn_lst_def)
+  fix f
+  assume "f \<in> [\<beta>]\<^bsup>n\<^esup> \<rightarrow> {..<length \<alpha>'}"
+  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)
+  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}"
+  proof (intro exI bexI conjI)
+    show "i < length \<alpha>'"
+      by (simp add: assms(2) i)
+    have "H' \<subseteq> H"
+      using bij \<open>i < length \<alpha>\<close> 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: \<open>finite H\<close> finite_subset)
+    with \<open>H' \<subseteq> H\<close> have cardH': "card H' = (\<alpha>'!i)"
+      unfolding H'_def by (simp add: inj card_image)
+    show "f ` [H']\<^bsup>n\<^esup> \<subseteq> {i}"
+      by (meson \<open>H' \<subseteq> H\<close> dual_order.trans fi image_mono nsets_mono)
+    show "H' \<in> [\<beta>]\<^bsup>(\<alpha>'! i)\<^esup>"
+      using \<open>H \<subseteq> \<beta>\<close> \<open>H' \<subseteq> H\<close> \<open>finite H'\<close> cardH' nsets_def by fastforce
+  qed
+qed
+
 
 subsection \<open>Finite versions of Ramsey's theorem\<close>