add lemmas about comparisons of Fract a b with 0 and 1
authorhuffman
Wed Feb 25 09:09:50 2009 -0800 (2009-02-25)
changeset 30095c6e184561159
parent 30094 83e864eb239f
child 30096 c5497842ee35
add lemmas about comparisons of Fract a b with 0 and 1
src/HOL/Rational.thy
     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 *}