When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
authorhoelzl
Mon Sep 06 15:01:37 2010 +0200 (2010-09-06)
changeset 3916175849a560c09
parent 39154 14b16b380ca1
child 39162 e6ec5283cd22
child 39183 512c10416590
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
src/HOL/Library/Float.thy
     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