transfer now handles Let
authorhoelzl
Thu Apr 19 22:13:46 2012 +0200 (2012-04-19)
changeset 47615341fd902ef1c
parent 47614 540a5af9a01c
child 47616 632a1e5710e6
transfer now handles Let
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Thu Apr 19 20:19:24 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 19 22:13:46 2012 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Library/Float.thy
     1.5 +    Author:     Johannes Hölzl, Fabian Immler
     1.6 +    Copyright   2012  TU München
     1.7 +*)
     1.8 +
     1.9  header {* Floating-Point Numbers *}
    1.10  
    1.11  theory Float
    1.12 @@ -614,7 +619,7 @@
    1.13    show ?thesis
    1.14    proof cases
    1.15      assume "2^nat (-(p + e)) dvd m"
    1.16 -    with `p + e < 0` twopow_rewrite show ?thesis unfolding Let_def
    1.17 +    with `p + e < 0` twopow_rewrite show ?thesis
    1.18        by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
    1.19    next
    1.20      assume ndvd: "\<not> 2 ^ nat (- (p + e)) dvd m"
    1.21 @@ -626,7 +631,6 @@
    1.22        using ndvd unfolding powr_rewrite one_div
    1.23        by (subst ceil_divide_floor_conv) (auto simp: field_simps)
    1.24      thus ?thesis using `p + e < 0` twopow_rewrite
    1.25 -      unfolding Let_def
    1.26        by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div[symmetric])
    1.27    qed
    1.28  next
    1.29 @@ -636,7 +640,6 @@
    1.30      by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
    1.31        intro: exI[where x="m*2^nat (e+p)"])
    1.32    then show ?thesis using `\<not> p + e < 0`
    1.33 -    unfolding Let_def
    1.34      by transfer
    1.35         (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
    1.36  qed
    1.37 @@ -846,9 +849,9 @@
    1.38         l = rat_precision prec x y;
    1.39         d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
    1.40      in normfloat (Float d (- l)))"
    1.41 -    unfolding div_mult_twopow_eq Let_def normfloat_def
    1.42 +    unfolding div_mult_twopow_eq normfloat_def
    1.43      by transfer
    1.44 -       (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps
    1.45 +       (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
    1.46               del: two_powr_minus_int_float)
    1.47  
    1.48  lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
    1.49 @@ -865,7 +868,7 @@
    1.50       m = fst X mod snd X
    1.51     in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
    1.52  proof (cases "y = 0")
    1.53 -  assume "y = 0" thus ?thesis unfolding Let_def normfloat_def by transfer simp
    1.54 +  assume "y = 0" thus ?thesis unfolding normfloat_def by transfer simp
    1.55  next
    1.56    assume "y \<noteq> 0"
    1.57    show ?thesis
    1.58 @@ -876,7 +879,7 @@
    1.59      moreover have "real x * 2 powr real l = real x'"
    1.60        by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
    1.61      ultimately show ?thesis
    1.62 -      unfolding Let_def normfloat_def
    1.63 +      unfolding normfloat_def
    1.64        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
    1.65          l_def[symmetric, THEN meta_eq_to_obj_eq]
    1.66        by transfer
    1.67 @@ -890,7 +893,7 @@
    1.68        using `\<not> 0 \<le> l`
    1.69        by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
    1.70      ultimately show ?thesis
    1.71 -      unfolding Let_def normfloat_def
    1.72 +      unfolding normfloat_def
    1.73        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
    1.74          l_def[symmetric, THEN meta_eq_to_obj_eq]
    1.75        by transfer
    1.76 @@ -1206,7 +1209,6 @@
    1.77      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
    1.78               else Float m e)"
    1.79    using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
    1.80 -  unfolding Let_def
    1.81    by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
    1.82  
    1.83  lemma compute_float_round_up[code]: