src/HOL/Rational.thy
changeset 30097 57df8626c23b
parent 30095 c6e184561159
child 30198 922f944f03b2
--- a/src/HOL/Rational.thy	Wed Feb 25 11:26:01 2009 -0800
+++ b/src/HOL/Rational.thy	Wed Feb 25 11:29:59 2009 -0800
@@ -5,7 +5,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports GCD
+imports GCD Archimedean_Field
 uses ("Tools/rat_arith.ML")
 begin
 
@@ -563,6 +563,37 @@
   by (simp add: One_rat_def mult_le_cancel_right)
 
 
+subsubsection {* Rationals are an Archimedean field *}
+
+lemma rat_floor_lemma:
+  assumes "0 < b"
+  shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
+proof -
+  have "Fract a b = of_int (a div b) + Fract (a mod b) b"
+    using `0 < b` by (simp add: of_int_rat)
+  moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
+    using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff)
+  ultimately show ?thesis by simp
+qed
+
+instance rat :: archimedean_field
+proof
+  fix r :: rat
+  show "\<exists>z. r \<le> of_int z"
+  proof (induct r)
+    case (Fract a b)
+    then have "Fract a b \<le> of_int (a div b + 1)"
+      using rat_floor_lemma [of b a] by simp
+    then show "\<exists>z. Fract a b \<le> of_int z" ..
+  qed
+qed
+
+lemma floor_Fract:
+  assumes "0 < b" shows "floor (Fract a b) = a div b"
+  using rat_floor_lemma [OF `0 < b`, of a]
+  by (simp add: floor_unique)
+
+
 subsection {* Arithmetic setup *}
 
 use "Tools/rat_arith.ML"