src/HOL/Rational.thy

--- a/src/HOL/Rational.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Rational.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -5,7 +5,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports GCD
+imports GCD Archimedean_Field
 uses ("Tools/rat_arith.ML")
 begin
 
@@ -21,8 +21,8 @@
   "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
   by (simp add: ratrel_def)
 
-lemma refl_ratrel: "refl {x. snd x \<noteq> 0} ratrel"
-  by (auto simp add: refl_def ratrel_def)
+lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
+  by (auto simp add: refl_on_def ratrel_def)
 
 lemma sym_ratrel: "sym ratrel"
   by (simp add: ratrel_def sym_def)
@@ -44,7 +44,7 @@
 qed
   
 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
-  by (rule equiv.intro [OF refl_ratrel sym_ratrel trans_ratrel])
+  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
 
 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
@@ -255,7 +255,6 @@
   with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
   with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
 qed
-  
 
 
 subsubsection {* The field of rational numbers *}
@@ -532,8 +531,67 @@
 qed
 
 lemma zero_less_Fract_iff:
-  "0 < b ==> (0 < Fract a b) = (0 < a)"
-by (simp add: Zero_rat_def order_less_imp_not_eq2 zero_less_mult_iff)
+  "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a"
+  by (simp add: Zero_rat_def zero_less_mult_iff)
+
+lemma Fract_less_zero_iff:
+  "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
+  by (simp add: Zero_rat_def mult_less_0_iff)
+
+lemma zero_le_Fract_iff:
+  "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a"
+  by (simp add: Zero_rat_def zero_le_mult_iff)
+
+lemma Fract_le_zero_iff:
+  "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0"
+  by (simp add: Zero_rat_def mult_le_0_iff)
+
+lemma one_less_Fract_iff:
+  "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a"
+  by (simp add: One_rat_def mult_less_cancel_right_disj)
+
+lemma Fract_less_one_iff:
+  "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b"
+  by (simp add: One_rat_def mult_less_cancel_right_disj)
+
+lemma one_le_Fract_iff:
+  "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a"
+  by (simp add: One_rat_def mult_le_cancel_right)
+
+lemma Fract_le_one_iff:
+  "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b"
+  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 *}