src/HOL/Rational.thy
 changeset 30095 c6e184561159 parent 29940 83b373f61d41 child 30097 57df8626c23b
```     1.1 --- a/src/HOL/Rational.thy	Wed Feb 25 07:14:33 2009 -0800
1.2 +++ b/src/HOL/Rational.thy	Wed Feb 25 09:09:50 2009 -0800
1.3 @@ -255,7 +255,6 @@
1.4    with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
1.5    with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
1.6  qed
1.7 -
1.8
1.9
1.10  subsubsection {* The field of rational numbers *}
1.11 @@ -532,8 +531,36 @@
1.12  qed
1.13
1.14  lemma zero_less_Fract_iff:
1.15 -  "0 < b ==> (0 < Fract a b) = (0 < a)"
1.16 -by (simp add: Zero_rat_def order_less_imp_not_eq2 zero_less_mult_iff)
1.17 +  "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a"
1.18 +  by (simp add: Zero_rat_def zero_less_mult_iff)
1.19 +
1.20 +lemma Fract_less_zero_iff:
1.21 +  "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
1.22 +  by (simp add: Zero_rat_def mult_less_0_iff)
1.23 +
1.24 +lemma zero_le_Fract_iff:
1.25 +  "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a"
1.26 +  by (simp add: Zero_rat_def zero_le_mult_iff)
1.27 +
1.28 +lemma Fract_le_zero_iff:
1.29 +  "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0"
1.30 +  by (simp add: Zero_rat_def mult_le_0_iff)
1.31 +
1.32 +lemma one_less_Fract_iff:
1.33 +  "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a"
1.34 +  by (simp add: One_rat_def mult_less_cancel_right_disj)
1.35 +
1.36 +lemma Fract_less_one_iff:
1.37 +  "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b"
1.38 +  by (simp add: One_rat_def mult_less_cancel_right_disj)
1.39 +
1.40 +lemma one_le_Fract_iff:
1.41 +  "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a"
1.42 +  by (simp add: One_rat_def mult_le_cancel_right)
1.43 +
1.44 +lemma Fract_le_one_iff:
1.45 +  "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b"
1.46 +  by (simp add: One_rat_def mult_le_cancel_right)
1.47
1.48
1.49  subsection {* Arithmetic setup *}
```