1.1 --- a/src/HOL/Rational.thy	Wed Feb 25 11:26:01 2009 -0800
     1.2 +++ b/src/HOL/Rational.thy	Wed Feb 25 11:29:59 2009 -0800
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Rational numbers *}
     1.5  
     1.6  theory Rational
     1.7 -imports GCD
     1.8 +imports GCD Archimedean_Field
     1.9  uses ("Tools/rat_arith.ML")
    1.10  begin
    1.11  
    1.12 @@ -563,6 +563,37 @@
    1.13    by (simp add: One_rat_def mult_le_cancel_right)
    1.14  
    1.15  
    1.16 +subsubsection {* Rationals are an Archimedean field *}
    1.17 +
    1.18 +lemma rat_floor_lemma:
    1.19 +  assumes "0 < b"
    1.20 +  shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
    1.21 +proof -
    1.22 +  have "Fract a b = of_int (a div b) + Fract (a mod b) b"
    1.23 +    using `0 < b` by (simp add: of_int_rat)
    1.24 +  moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
    1.25 +    using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff)
    1.26 +  ultimately show ?thesis by simp
    1.27 +qed
    1.28 +
    1.29 +instance rat :: archimedean_field
    1.30 +proof
    1.31 +  fix r :: rat
    1.32 +  show "\<exists>z. r \<le> of_int z"
    1.33 +  proof (induct r)
    1.34 +    case (Fract a b)
    1.35 +    then have "Fract a b \<le> of_int (a div b + 1)"
    1.36 +      using rat_floor_lemma [of b a] by simp
    1.37 +    then show "\<exists>z. Fract a b \<le> of_int z" ..
    1.38 +  qed
    1.39 +qed
    1.40 +
    1.41 +lemma floor_Fract:
    1.42 +  assumes "0 < b" shows "floor (Fract a b) = a div b"
    1.43 +  using rat_floor_lemma [OF `0 < b`, of a]
    1.44 +  by (simp add: floor_unique)
    1.45 +
    1.46 +
    1.47  subsection {* Arithmetic setup *}
    1.48  
    1.49  use "Tools/rat_arith.ML"