src/HOL/Rational.thy
 changeset 30097 57df8626c23b parent 30095 c6e184561159 child 30198 922f944f03b2
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.6  theory Rational
1.7 -imports GCD
1.8 +imports GCD Archimedean_Field
1.9  uses ("Tools/rat_arith.ML")
1.10  begin
1.12 @@ -563,6 +563,37 @@
1.13    by (simp add: One_rat_def mult_le_cancel_right)
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.49  use "Tools/rat_arith.ML"