author paulson Mon, 09 Dec 2019 16:37:26 +0000 changeset 71260 308baf6b450a parent 71259 09aee7f5b447 child 71261 4765fec43414
corrected some confusing terminology / notation
```--- a/src/HOL/Library/Ramsey.thy	Mon Dec 09 16:13:36 2019 +0000
+++ b/src/HOL/Library/Ramsey.thy	Mon Dec 09 16:37:26 2019 +0000
@@ -602,20 +602,20 @@
qed

-subsubsection \<open>Partitions of a Set\<close>
+subsubsection \<open>Partition functions\<close>

-definition part :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
+definition part_fn :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
\<comment> \<open>the function \<^term>\<open>f\<close> partitions the \<^term>\<open>r\<close>-subsets of the typically
infinite set \<^term>\<open>Y\<close> into \<^term>\<open>s\<close> distinct categories.\<close>
-  where "part r s Y f \<longleftrightarrow> (\<forall>X \<in> nsets Y r. f X < s)"
+  where "part_fn r s Y f \<longleftrightarrow> (f \<in> nsets Y r \<rightarrow> {..<s})"

text \<open>For induction, we decrease the value of \<^term>\<open>r\<close> in partitions.\<close>
-lemma part_Suc_imp_part:
-  "\<lbrakk>infinite Y; part (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part r s (Y - {y}) (\<lambda>u. f (insert y u))"
-  by (simp add: part_def nsets_def subset_Diff_insert)
+lemma part_fn_Suc_imp_part_fn:
+  "\<lbrakk>infinite Y; part_fn (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part_fn r s (Y - {y}) (\<lambda>u. f (insert y u))"
+  by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert)

-lemma part_subset: "part r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part r s Y f"
-  unfolding part_def nsets_def by blast
+lemma part_fn_subset: "part_fn r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part_fn r s Y f"
+  unfolding part_fn_def nsets_def by blast

subsection \<open>Ramsey's Theorem: Infinitary Version\<close>
@@ -624,13 +624,13 @@
fixes s r :: nat
and YY :: "'a set"
and f :: "'a set \<Rightarrow> nat"
-  assumes "infinite YY" "part r s YY f"
+  assumes "infinite YY" "part_fn r s YY f"
shows "\<exists>Y' t'. Y' \<subseteq> YY \<and> infinite Y' \<and> t' < s \<and> (\<forall>X. X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> f X = t')"
using assms
proof (induct r arbitrary: YY f)
case 0
then show ?case
-    by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
+    by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong)
next
case (Suc r)
show ?case
@@ -642,8 +642,8 @@
y \<in> YY \<and> y \<notin> Y \<and> Y \<subseteq> YY \<and> infinite Y \<and> t < s
\<and> (\<forall>X. X\<subseteq>Y \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert y) X = t)"
from Suc.prems have infYY': "infinite (YY - {yy})" by auto
-    from Suc.prems have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
-      by (simp add: o_def part_Suc_imp_part yy)
+    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)
from Suc.hyps [OF infYY' partf']
obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
@@ -656,8 +656,8 @@
with x obtain yx' where yx': "yx' \<in> 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 r s (Yx - {yx'}) (f \<circ> insert yx')"
-        by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
+      with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f \<circ> 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' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
"X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'" for X
@@ -750,7 +750,7 @@
\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = r \<longrightarrow> f X < s\<rbrakk>
\<Longrightarrow> \<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s
\<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
-  by (blast intro: Ramsey_induction [unfolded part_def nsets_def])
+  by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def])

corollary Ramsey2:```