diff -r 1ba5331b4623 -r 6b2bdc57155b src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/HOL/Rat.thy	Sat Jul 09 13:41:58 2011 +0200
@@ -739,6 +739,20 @@
   qed
 qed
 
+instantiation rat :: floor_ceiling
+begin
+
+definition [code del]:
+  "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+  fix x :: rat
+  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+    unfolding floor_rat_def using floor_exists1 by (rule theI')
+qed
+
+end
+
 lemma floor_Fract: "floor (Fract a b) = a div b"
   using rat_floor_lemma [of a b]
   by (simp add: floor_unique)