src/HOL/Rational.thy
changeset 29940 83b373f61d41
parent 29925 17d1e32ef867
child 30095 c6e184561159
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Rational.thy	Mon Feb 16 19:11:35 2009 +0100
     1.2 +++ b/src/HOL/Rational.thy	Mon Feb 16 19:11:55 2009 +0100
     1.3 @@ -886,14 +886,13 @@
     1.4    finally show ?thesis using assms by simp
     1.5  qed
     1.6  
     1.7 -lemma rat_less_eq_code [code]:
     1.8 -  "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
     1.9 -       then sgn c * sgn d \<ge> 0
    1.10 -     else if d = 0
    1.11 -       then sgn a * sgn b \<le> 0
    1.12 -     else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
    1.13 -by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
    1.14 -  (auto simp add: sgn_times sgn_0_0 le_less sgn_1_pos [symmetric] sgn_1_neg [symmetric])
    1.15 +lemma (in ordered_idom) sgn_greater [simp]:
    1.16 +  "0 < sgn a \<longleftrightarrow> 0 < a"
    1.17 +  unfolding sgn_if by auto
    1.18 +
    1.19 +lemma (in ordered_idom) sgn_less [simp]:
    1.20 +  "sgn a < 0 \<longleftrightarrow> a < 0"
    1.21 +  unfolding sgn_if by auto
    1.22  
    1.23  lemma rat_le_eq_code [code]:
    1.24    "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
    1.25 @@ -901,9 +900,17 @@
    1.26       else if d = 0
    1.27         then sgn a * sgn b < 0
    1.28       else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)"
    1.29 -by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
    1.30 -   (auto simp add: sgn_times sgn_0_0 sgn_1_pos [symmetric] sgn_1_neg [symmetric],
    1.31 -     auto simp add: sgn_1_pos)
    1.32 +  by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
    1.33 +
    1.34 +lemma rat_less_eq_code [code]:
    1.35 +  "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
    1.36 +       then sgn c * sgn d \<ge> 0
    1.37 +     else if d = 0
    1.38 +       then sgn a * sgn b \<le> 0
    1.39 +     else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
    1.40 +  by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
    1.41 +    (auto simp add: le_less not_less sgn_0_0)
    1.42 +
    1.43  
    1.44  lemma rat_plus_code [code]:
    1.45    "Fract a b + Fract c d = (if b = 0