src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Rat.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -916,6 +916,8 @@
   "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
 
+lemma Rats_infinite: "\<not> finite \<rat>"
+  by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
 
 subsection {* Implementation of rational numbers as pairs of integers *}