author wenzelm Sat, 24 Jun 2006 22:54:37 +0200 changeset 19949 0505dce27b0b parent 19948 1be283f3f1ba child 19950 fd74bf4e603e
fix/fixes: tuned type constraints;
```--- a/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:25:31 2006 +0200
+++ b/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:54:37 2006 +0200
@@ -41,7 +41,7 @@
by (auto intro: someI2_ex)
show "\<forall>n m. n<m --> (choice P r n, choice P r m) \<in> r"
proof (intro strip)
-    fix n and m::nat
+    fix n m :: nat
assume less: "n<m"
show "(choice P r n, choice P r m) \<in> r" using PSuc
by (auto intro: less_Suc_induct [OF less] transD [OF trans])
@@ -73,7 +73,7 @@
subsection {*Ramsey's Theorem: Infinitary Version*}

lemma ramsey_induction:
-  fixes s::nat and r::nat
+  fixes s r :: nat
shows
"!!(YY::'a set) (f::'a set => nat).
[|infinite YY; part r s YY f|]
@@ -147,7 +147,7 @@
with pg [of n'] have less': "s'<s" by (cases "g n'") auto
have inj_gy: "inj ?gy"
proof (rule linorder_injI)
-      fix m and m'::nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
+      fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
qed
show ?thesis
@@ -205,7 +205,7 @@

text{*Repackaging of Tom Ridge's final result*}
theorem Ramsey:
-  fixes s::nat and r::nat and Z::"'a set" and f::"'a set => nat"
+  fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
shows
"[|infinite Z;
\<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]```