src/HOL/Library/Float.thy
 changeset 39161 75849a560c09 parent 36778 739a9379e29b child 41024 ba961a606c67
```     1.1 --- a/src/HOL/Library/Float.thy	Mon Sep 06 12:38:45 2010 +0200
1.2 +++ b/src/HOL/Library/Float.thy	Mon Sep 06 15:01:37 2010 +0200
1.3 @@ -397,6 +397,22 @@
1.4    apply auto
1.5    done
1.6
1.7 +lemma zero_less_float:
1.8 +  "(0 < real (Float a b)) = (0 < a)"
1.9 +  apply auto
1.10 +  apply (auto simp add: zero_less_mult_iff)
1.11 +  apply (insert zero_less_pow2[of b])
1.12 +  apply (simp_all)
1.13 +  done
1.14 +
1.15 +lemma float_less_zero:
1.16 +  "(real (Float a b) < 0) = (a < 0)"
1.17 +  apply auto
1.18 +  apply (auto simp add: mult_less_0_iff)
1.19 +  apply (insert zero_less_pow2[of b])
1.20 +  apply (simp_all)
1.21 +  done
1.22 +
1.23  declare real_of_float_simp[simp del]
1.24
1.25  lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
1.26 @@ -1398,7 +1414,7 @@
1.27    finally show ?thesis unfolding ub_mod_def real_of_float_sub real_of_float_mult by auto
1.28  qed
1.29
1.30 -lemma le_float_def': "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)"
1.31 +lemma le_float_def'[code]: "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)"
1.32  proof -
1.33    have le_transfer: "(f \<le> g) = (real (f - g) \<le> 0)" by (auto simp add: le_float_def)
1.34    from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
1.35 @@ -1406,12 +1422,7 @@
1.36    show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero)
1.37  qed
1.38
1.39 -lemma float_less_zero:
1.40 -  "(real (Float a b) < 0) = (a < 0)"
1.41 -  apply (auto simp add: mult_less_0_iff real_of_float_simp)
1.42 -  done
1.43 -
1.44 -lemma less_float_def': "f < g = (case f - g of Float a b \<Rightarrow> a < 0)"
1.45 +lemma less_float_def'[code]: "f < g = (case f - g of Float a b \<Rightarrow> a < 0)"
1.46  proof -
1.47    have less_transfer: "(f < g) = (real (f - g) < 0)" by (auto simp add: less_float_def)
1.48    from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
```