src/HOL/Library/Ramsey.thy

--- a/src/HOL/Library/Ramsey.thy	Sun Oct 01 18:29:26 2006 +0200
+++ b/src/HOL/Library/Ramsey.thy	Sun Oct 01 18:29:28 2006 +0200
@@ -5,7 +5,7 @@
 
 header "Ramsey's Theorem"
 
-theory Ramsey imports Main begin
+theory Ramsey imports Main Infinite_Set begin
 
 
 subsection{*Preliminaries*}
@@ -138,13 +138,12 @@
       then obtain n where "x = ?gt n" ..
       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
     qed
-    have "\<exists>s' \<in> range ?gt. infinite (?gt -` {s'})" 
-     by (rule inf_img_fin_dom [OF _ nat_infinite]) 
-        (simp add: finite_nat_iff_bounded rangeg)
+    have "finite (range ?gt)"
+      by (simp add: finite_nat_iff_bounded rangeg)
     then obtain s' and n'
-            where s':      "s' = ?gt n'"
-              and infeqs': "infinite {n. ?gt n = s'}"
-       by (auto simp add: vimage_def)
+      where s': "s' = ?gt n'"
+        and infeqs': "infinite {n. ?gt n = s'}"
+      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
     have inj_gy: "inj ?gy"
     proof (rule linorder_injI)
@@ -241,13 +240,13 @@
 IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004).
 *}
 
-constdefs
+definition
   disj_wf         :: "('a * 'a)set => bool"
-  "disj_wf(r) == \<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i)"
+  "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
 
   transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
-  "transition_idx s T A ==
-     LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k"
+  "transition_idx s T A =
+    (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
 
 
 lemma transition_idx_less: