use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
authorhoelzl
Thu Apr 19 11:55:30 2012 +0200 (2012-04-19)
changeset 47601050718fe6eee
parent 47600 e12289b5796b
child 47603 b716b16ab2ac
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 18 14:29:22 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 19 11:55:30 2012 +0200
     1.3 @@ -634,7 +634,7 @@
     1.4  
     1.5          have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
     1.6  
     1.7 -        have "arctan (1 / x) \<le> arctan ?invx" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divr)
     1.8 +        have "arctan (1 / x) \<le> arctan ?invx" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divr)
     1.9          also have "\<dots> \<le> (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
    1.10          finally have "pi / 2 - (?ub_horner ?invx) \<le> arctan x"
    1.11            using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
    1.12 @@ -726,7 +726,7 @@
    1.13        have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
    1.14  
    1.15        have "(?lb_horner ?invx) \<le> arctan (?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
    1.16 -      also have "\<dots> \<le> arctan (1 / x)" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divl)
    1.17 +      also have "\<dots> \<le> arctan (1 / x)" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divl)
    1.18        finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
    1.19          using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
    1.20          unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
    1.21 @@ -749,8 +749,8 @@
    1.22    case False hence "x < 0" and "0 \<le> real ?mx" by auto
    1.23    hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx"
    1.24      using ub_arctan_bound'[OF `0 \<le> real ?mx`] lb_arctan_bound'[OF `0 \<le> real ?mx`] by auto
    1.25 -  show ?thesis unfolding real_of_float_minus arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
    1.26 -    unfolding atLeastAtMost_iff using bounds[unfolded real_of_float_minus arctan_minus]
    1.27 +  show ?thesis unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
    1.28 +    unfolding atLeastAtMost_iff using bounds[unfolded minus_float.rep_eq arctan_minus]
    1.29      by (simp add: arctan_minus)
    1.30  qed
    1.31  
    1.32 @@ -783,6 +783,7 @@
    1.33  | "lb_sin_cos_aux prec 0 i k x = 0"
    1.34  | "lb_sin_cos_aux prec (Suc n) i k x =
    1.35      (lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
    1.36 +
    1.37  lemma cos_aux:
    1.38    shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
    1.39    and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
    1.40 @@ -880,7 +881,7 @@
    1.41      hence "get_even n = 0" by auto
    1.42      have "- (pi / 2) \<le> x" by (rule order_trans[OF _ `0 < real x`[THEN less_imp_le]], auto)
    1.43      with `x \<le> pi / 2`
    1.44 -    show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps real_of_float_minus real_of_float_zero using cos_ge_zero by auto
    1.45 +    show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps minus_float.rep_eq zero_float.rep_eq using cos_ge_zero by auto
    1.46    qed
    1.47    ultimately show ?thesis by auto
    1.48  next
    1.49 @@ -995,7 +996,7 @@
    1.50      case False
    1.51      hence "get_even n = 0" by auto
    1.52      with `x \<le> pi / 2` `0 \<le> real x`
    1.53 -    show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps real_of_float_minus using sin_ge_zero by auto
    1.54 +    show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps minus_float.rep_eq using sin_ge_zero by auto
    1.55    qed
    1.56    ultimately show ?thesis by auto
    1.57  next
    1.58 @@ -1214,7 +1215,7 @@
    1.59        using lb_cos_minus[OF pi_lx lx_0] by simp
    1.60      also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
    1.61        using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
    1.62 -      by (simp only: real_of_float_uminus real_of_int_minus
    1.63 +      by (simp only: uminus_float.rep_eq real_of_int_minus
    1.64          cos_minus diff_minus mult_minus_left)
    1.65      finally have "(lb_cos prec (- ?lx)) \<le> cos x"
    1.66        unfolding cos_periodic_int . }
    1.67 @@ -1242,7 +1243,7 @@
    1.68  
    1.69      have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
    1.70        using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
    1.71 -      by (simp only: real_of_float_uminus real_of_int_minus
    1.72 +      by (simp only: uminus_float.rep_eq real_of_int_minus
    1.73            cos_minus diff_minus mult_minus_left)
    1.74      also have "\<dots> \<le> (ub_cos prec (- ?ux))"
    1.75        using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
    1.76 @@ -1334,10 +1335,10 @@
    1.77          unfolding cos_periodic_int ..
    1.78        also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
    1.79          using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
    1.80 -        by (simp only: real_of_float_minus real_of_int_minus real_of_one minus_one[symmetric]
    1.81 +        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
    1.82              diff_minus mult_minus_left mult_1_left)
    1.83        also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
    1.84 -        unfolding real_of_float_uminus cos_minus ..
    1.85 +        unfolding uminus_float.rep_eq cos_minus ..
    1.86        also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
    1.87          using lb_cos_minus[OF pi_ux ux_0] by simp
    1.88        finally show ?thesis unfolding u by (simp add: real_of_float_max)
    1.89 @@ -1378,7 +1379,7 @@
    1.90          unfolding cos_periodic_int ..
    1.91        also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
    1.92          using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
    1.93 -        by (simp only: real_of_float_minus real_of_int_minus real_of_one
    1.94 +        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
    1.95            minus_one[symmetric] diff_minus mult_minus_left mult_1_left)
    1.96        also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
    1.97          using lb_cos[OF lx_0 pi_lx] by simp
    1.98 @@ -1534,7 +1535,7 @@
    1.99      proof -
   1.100        have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
   1.101          using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
   1.102 -        unfolding less_eq_float_def real_of_float_zero .
   1.103 +        unfolding less_eq_float_def zero_float.rep_eq .
   1.104  
   1.105        have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
   1.106        also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
   1.107 @@ -1562,7 +1563,7 @@
   1.108            exp (float_divl prec x (- floor_fl x)) ^ ?num"
   1.109            using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
   1.110          also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
   1.111 -          using float_divl by (auto intro!: power_mono simp del: real_of_float_uminus)
   1.112 +          using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
   1.113          also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
   1.114          also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
   1.115          finally show ?thesis
   1.116 @@ -1571,7 +1572,7 @@
   1.117          case True
   1.118          have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
   1.119          from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
   1.120 -        have "- 1 \<le> x / (- floor_fl x)" unfolding real_of_float_minus by auto
   1.121 +        have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
   1.122          from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
   1.123          have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
   1.124          hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
   1.125 @@ -1597,7 +1598,7 @@
   1.126      have "lb_exp prec x \<le> exp x"
   1.127      proof -
   1.128        from exp_boundaries'[OF `-x \<le> 0`]
   1.129 -      have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
   1.130 +      have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
   1.131  
   1.132        have "float_divl prec 1 (ub_exp prec (-x)) \<le> 1 / ub_exp prec (-x)" using float_divl[where x=1] by auto
   1.133        also have "\<dots> \<le> exp x"
   1.134 @@ -1611,7 +1612,7 @@
   1.135        have "\<not> 0 < -x" using `0 < x` by auto
   1.136  
   1.137        from exp_boundaries'[OF `-x \<le> 0`]
   1.138 -      have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
   1.139 +      have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
   1.140  
   1.141        have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
   1.142          using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
   1.143 @@ -1686,7 +1687,7 @@
   1.144  
   1.145    let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
   1.146  
   1.147 -  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
   1.148 +  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
   1.149      using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
   1.150        OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
   1.151      by (rule mult_right_mono)
   1.152 @@ -1694,7 +1695,7 @@
   1.153    finally show "?lb \<le> ?ln" .
   1.154  
   1.155    have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
   1.156 -  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
   1.157 +  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
   1.158      using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
   1.159        OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
   1.160      by (rule mult_right_mono)
   1.161 @@ -1743,14 +1744,14 @@
   1.162    have uthird_gt0: "0 < real ?uthird + 1" using ub3_lb by auto
   1.163    have lthird_gt0: "0 < real ?lthird + 1" using lb3_lb by auto
   1.164  
   1.165 -  show ?ub_ln2 unfolding ub_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
   1.166 +  show ?ub_ln2 unfolding ub_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
   1.167    proof (rule add_mono, fact ln_float_bounds(2)[OF lb2 ub2])
   1.168      have "ln (1 / 3 + 1) \<le> ln (real ?uthird + 1)" unfolding ln_le_cancel_iff[OF third_gt0 uthird_gt0] using ub3 by auto
   1.169      also have "\<dots> \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird"
   1.170        using ln_float_bounds(2)[OF ub3_lb ub3_ub] .
   1.171      finally show "ln (1 / 3 + 1) \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird" .
   1.172    qed
   1.173 -  show ?lb_ln2 unfolding lb_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
   1.174 +  show ?lb_ln2 unfolding lb_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
   1.175    proof (rule add_mono, fact ln_float_bounds(1)[OF lb2 ub2])
   1.176      have "?lthird * lb_ln_horner prec (get_even prec) 1 ?lthird \<le> ln (real ?lthird + 1)"
   1.177        using ln_float_bounds(1)[OF lb3_lb lb3_ub] .
   1.178 @@ -1993,7 +1994,7 @@
   1.179  
   1.180      {
   1.181        have "lb_ln2 prec * ?s \<le> ln 2 * (e + (bitlen m - 1))" (is "?lb2 \<le> _")
   1.182 -        unfolding nat_0 power_0 mult_1_right real_of_float_times
   1.183 +        unfolding nat_0 power_0 mult_1_right times_float.rep_eq
   1.184          using lb_ln2[of prec]
   1.185        proof (rule mult_mono)
   1.186          from float_gt1_scale[OF `1 \<le> Float m e`]
   1.187 @@ -2011,7 +2012,7 @@
   1.188        have "ln ?x \<le> (?x - 1) * ub_ln_horner prec (get_odd prec) 1 (?x - 1)" (is "_ \<le> ?ub_horner") by auto
   1.189        moreover
   1.190        have "ln 2 * (e + (bitlen m - 1)) \<le> ub_ln2 prec * ?s" (is "_ \<le> ?ub2")
   1.191 -        unfolding nat_0 power_0 mult_1_right real_of_float_times
   1.192 +        unfolding nat_0 power_0 mult_1_right times_float.rep_eq
   1.193          using ub_ln2[of prec]
   1.194        proof (rule mult_mono)
   1.195          from float_gt1_scale[OF `1 \<le> Float m e`]
   1.196 @@ -2025,7 +2026,7 @@
   1.197      }
   1.198      ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
   1.199        unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
   1.200 -      unfolding real_of_float_plus e_def[symmetric] m_def[symmetric] by simp
   1.201 +      unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
   1.202    qed
   1.203  qed
   1.204  
   1.205 @@ -2049,7 +2050,7 @@
   1.206      have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
   1.207      hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
   1.208      from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
   1.209 -    have "?ln \<le> - the (lb_ln prec ?divl)" unfolding real_of_float_uminus by (rule order_trans)
   1.210 +    have "?ln \<le> - the (lb_ln prec ?divl)" unfolding uminus_float.rep_eq by (rule order_trans)
   1.211    } moreover
   1.212    {
   1.213      let ?divr = "float_divr prec 1 x"
   1.214 @@ -2059,7 +2060,7 @@
   1.215      have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
   1.216      hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
   1.217      from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
   1.218 -    have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding real_of_float_uminus by (rule order_trans)
   1.219 +    have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding uminus_float.rep_eq by (rule order_trans)
   1.220    }
   1.221    ultimately show ?thesis unfolding lb_ln.simps[where x=x]  ub_ln.simps[where x=x]
   1.222      unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
   1.223 @@ -2447,7 +2448,7 @@
   1.224    from lift_un'[OF Minus.prems[unfolded approx.simps]] Minus.hyps
   1.225    obtain l1 u1 where "l = -u1" and "u = -l1"
   1.226      "l1 \<le> interpret_floatarith a xs" and "interpret_floatarith a xs \<le> u1" unfolding fst_conv snd_conv by blast
   1.227 -  thus ?case unfolding interpret_floatarith.simps using real_of_float_minus by auto
   1.228 +  thus ?case unfolding interpret_floatarith.simps using minus_float.rep_eq by auto
   1.229  next
   1.230    case (Mult a b)
   1.231    from lift_bin'[OF Mult.prems[unfolded approx.simps]] Mult.hyps
     2.1 --- a/src/HOL/Library/Float.thy	Wed Apr 18 14:29:22 2012 +0200
     2.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 19 11:55:30 2012 +0200
     2.3 @@ -8,13 +8,16 @@
     2.4    morphisms real_of_float float_of
     2.5    by auto
     2.6  
     2.7 -setup_lifting type_definition_float
     2.8 +defs (overloaded)
     2.9 +  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
    2.10 +
    2.11 +lemma type_definition_float': "type_definition real float_of float"
    2.12 +  using type_definition_float unfolding real_of_float_def .
    2.13 +
    2.14 +setup_lifting (no_code) type_definition_float'
    2.15  
    2.16  lemmas float_of_inject[simp]
    2.17  
    2.18 -defs (overloaded)
    2.19 -  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
    2.20 -
    2.21  declare [[coercion "real :: float \<Rightarrow> real"]]
    2.22  
    2.23  lemma real_of_float_eq:
    2.24 @@ -27,10 +30,6 @@
    2.25  lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
    2.26    unfolding real_of_float_def by (rule float_of_inverse)
    2.27  
    2.28 -lemma transfer_real_of_float [transfer_rule]:
    2.29 -  "(fun_rel cr_float op =) (\<lambda>x. x) real"
    2.30 -  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def)
    2.31 -
    2.32  subsection {* Real operations preserving the representation as floating point number *}
    2.33  
    2.34  lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
    2.35 @@ -124,6 +123,9 @@
    2.36  qed
    2.37  
    2.38  lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
    2.39 +declare Float.rep_eq[simp]
    2.40 +
    2.41 +code_datatype Float
    2.42  
    2.43  subsection {* Arithmetic operations on floating point numbers *}
    2.44  
    2.45 @@ -131,41 +133,34 @@
    2.46  begin
    2.47  
    2.48  lift_definition zero_float :: float is 0 by simp
    2.49 +declare zero_float.rep_eq[simp]
    2.50  lift_definition one_float :: float is 1 by simp
    2.51 +declare one_float.rep_eq[simp]
    2.52  lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
    2.53 +declare plus_float.rep_eq[simp]
    2.54  lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
    2.55 +declare times_float.rep_eq[simp]
    2.56  lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
    2.57 +declare minus_float.rep_eq[simp]
    2.58  lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
    2.59 +declare uminus_float.rep_eq[simp]
    2.60  
    2.61  lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
    2.62 +declare abs_float.rep_eq[simp]
    2.63  lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
    2.64 +declare sgn_float.rep_eq[simp]
    2.65  
    2.66  lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
    2.67  
    2.68  lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
    2.69 +declare less_eq_float.rep_eq[simp]
    2.70  lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
    2.71 +declare less_float.rep_eq[simp]
    2.72  
    2.73  instance
    2.74    proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
    2.75  end
    2.76  
    2.77 -lemma
    2.78 -  fixes x y :: float
    2.79 -  shows real_of_float_uminus[simp]: "real (- x) = - real x"
    2.80 -    and real_of_float_plus[simp]: "real (y + x) = real y + real x"
    2.81 -    and real_of_float_minus[simp]: "real (y - x) = real y - real x"
    2.82 -    and real_of_float_times[simp]: "real (y * x) = real y * real x"
    2.83 -    and real_of_float_zero[simp]: "real (0::float) = 0"
    2.84 -    and real_of_float_one[simp]: "real (1::float) = 1"
    2.85 -    and real_of_float_le[simp]: "x \<le> y \<longleftrightarrow> real x \<le> real y"
    2.86 -    and real_of_float_less[simp]: "x < y \<longleftrightarrow> real x < real y"
    2.87 -    and real_of_float_abs[simp]: "real (abs x) = abs (real x)"
    2.88 -    and real_of_float_sgn[simp]: "real (sgn x) = sgn (real x)"
    2.89 -  using uminus_float.rep_eq plus_float.rep_eq minus_float.rep_eq times_float.rep_eq
    2.90 -    zero_float.rep_eq one_float.rep_eq less_eq_float.rep_eq less_float.rep_eq
    2.91 -    abs_float.rep_eq sgn_float.rep_eq
    2.92 -  by (simp_all add: real_of_float_def)
    2.93 -
    2.94  lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
    2.95    by (induct n) simp_all
    2.96  
    2.97 @@ -213,7 +208,7 @@
    2.98    apply (induct x)
    2.99    apply simp
   2.100    apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
   2.101 -                  real_of_float_plus real_of_float_one plus_float numeral_float one_float)
   2.102 +                  plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
   2.103    done
   2.104  
   2.105  lemma transfer_numeral [transfer_rule]: 
   2.106 @@ -366,12 +361,9 @@
   2.107  
   2.108  subsection {* Compute arithmetic operations *}
   2.109  
   2.110 -lemma real_Float[simp]: "real (Float m e) = m * 2 powr e"
   2.111 -  using Float.rep_eq by (simp add: real_of_float_def)
   2.112 -
   2.113  lemma real_of_float_Float[code]: "real_of_float (Float m e) =
   2.114    (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
   2.115 -by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric] Float_def)
   2.116 +by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
   2.117  
   2.118  lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   2.119    unfolding real_of_float_eq mantissa_exponent[of f] by simp
   2.120 @@ -537,9 +529,7 @@
   2.121  subsection {* Rounding Floats *}
   2.122  
   2.123  lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
   2.124 -
   2.125 -lemma real_of_float_float_up[simp]: "real (float_up e f) = round_up e (real f)"
   2.126 -  using float_up.rep_eq by (simp add: real_of_float_def)
   2.127 +declare float_up.rep_eq[simp]
   2.128  
   2.129  lemma float_up_correct:
   2.130    shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
   2.131 @@ -552,9 +542,7 @@
   2.132  qed (simp add: algebra_simps round_up)
   2.133  
   2.134  lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
   2.135 -
   2.136 -lemma real_of_float_float_down[simp]: "real (float_down e f) = round_down e (real f)"
   2.137 -  using float_down.rep_eq by (simp add: real_of_float_def)
   2.138 +declare float_down.rep_eq[simp]
   2.139  
   2.140  lemma float_down_correct:
   2.141    shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
   2.142 @@ -929,7 +917,8 @@
   2.143    ultimately show ?thesis using assms by simp
   2.144  qed
   2.145  
   2.146 -lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   2.147 +lemma rapprox_posrat_less1:
   2.148 +  assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   2.149    shows "real (rapprox_posrat n x y) < 1"
   2.150  proof -
   2.151    have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
   2.152 @@ -947,14 +936,10 @@
   2.153      unfolding int_of_reals real_of_int_le_iff
   2.154      using rat_precision_pos[OF assms] by (rule power_aux)
   2.155    finally show ?thesis
   2.156 -    unfolding rapprox_posrat_def
   2.157 -    apply (simp add: round_up_def)
   2.158 -    apply (simp add: field_simps powr_minus inverse_eq_divide)
   2.159 -    unfolding powr1
   2.160 +    apply (transfer fixing: n x y)
   2.161 +    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
   2.162      unfolding int_of_reals real_of_int_less_iff
   2.163 -    unfolding ceiling_less_eq
   2.164 -    using rat_precision_pos[of x y n] assms
   2.165 -    apply simp
   2.166 +    apply (simp add: ceiling_less_eq)
   2.167      done
   2.168  qed
   2.169  
   2.170 @@ -970,12 +955,7 @@
   2.171        else (if 0 < y
   2.172          then - (rapprox_posrat prec (nat (-x)) (nat y))
   2.173          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   2.174 -  apply transfer
   2.175 -  apply (cases "y = 0")
   2.176 -  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   2.177 -                    int_of_reals simp del: real_of_ints)
   2.178 -  apply (auto simp: ac_simps)
   2.179 -  done
   2.180 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   2.181  
   2.182  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   2.183    "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
   2.184 @@ -989,12 +969,7 @@
   2.185        else (if 0 < y
   2.186          then - (lapprox_posrat prec (nat (-x)) (nat y))
   2.187          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   2.188 -  apply transfer
   2.189 -  apply (cases "y = 0")
   2.190 -  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   2.191 -                    int_of_reals simp del: real_of_ints)
   2.192 -  apply (auto simp: ac_simps)
   2.193 -  done
   2.194 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   2.195  
   2.196  subsection {* Division *}
   2.197  
   2.198 @@ -1004,23 +979,17 @@
   2.199  lemma compute_float_divl[code]:
   2.200    "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   2.201  proof cases
   2.202 -  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.203 -  then show ?thesis
   2.204 -  proof transfer
   2.205 -    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.206 -    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   2.207 -    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   2.208 +  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   2.209 +  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   2.210 +  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.211 +  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   2.212 +    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   2.213 +  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   2.214 +    by (simp add: field_simps powr_divide2[symmetric])
   2.215  
   2.216 -    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   2.217 -      by (simp add: field_simps powr_divide2[symmetric])
   2.218 -    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   2.219 -        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   2.220 -      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   2.221 -    
   2.222 -    show "round_down (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   2.223 -      round_down (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   2.224 -      using not_0 unfolding eq1 eq2 round_down_shift by (simp add: field_simps)
   2.225 -  qed
   2.226 +  show ?thesis
   2.227 +    using not_0 
   2.228 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
   2.229  qed (transfer, auto)
   2.230  
   2.231  lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
   2.232 @@ -1029,23 +998,17 @@
   2.233  lemma compute_float_divr[code]:
   2.234    "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   2.235  proof cases
   2.236 -  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.237 -  then show ?thesis
   2.238 -  proof transfer
   2.239 -    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.240 -    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   2.241 -    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   2.242 +  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   2.243 +  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   2.244 +  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   2.245 +  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   2.246 +    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   2.247 +  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   2.248 +    by (simp add: field_simps powr_divide2[symmetric])
   2.249  
   2.250 -    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   2.251 -      by (simp add: field_simps powr_divide2[symmetric])
   2.252 -    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   2.253 -        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   2.254 -      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   2.255 -    
   2.256 -    show "round_up (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   2.257 -      round_up (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   2.258 -      using not_0 unfolding eq1 eq2 round_up_shift by (simp add: field_simps)
   2.259 -  qed
   2.260 +  show ?thesis
   2.261 +    using not_0 
   2.262 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   2.263  qed (transfer, auto)
   2.264  
   2.265  subsection {* Lemmas needed by Approximate *}
   2.266 @@ -1242,12 +1205,9 @@
   2.267    "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
   2.268      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
   2.269               else Float m e)"
   2.270 +  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.271    unfolding Let_def
   2.272 -  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.273 -  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
   2.274 -  apply (cases "m = 0")
   2.275 -  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
   2.276 -  done
   2.277 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   2.278  
   2.279  lemma compute_float_round_up[code]:
   2.280    "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
   2.281 @@ -1256,10 +1216,7 @@
   2.282                else Float m e)"
   2.283    using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.284    unfolding Let_def
   2.285 -  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
   2.286 -  apply (cases "m = 0")
   2.287 -  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
   2.288 -  done
   2.289 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   2.290  
   2.291  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   2.292   apply (auto simp: zero_float_def mult_le_0_iff)
   2.293 @@ -1282,15 +1239,13 @@
   2.294  lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
   2.295  
   2.296  lemma compute_int_floor_fl[code]:
   2.297 -  shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e
   2.298 -                                  else m div (2 ^ (nat (-e))))"
   2.299 +  "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   2.300    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   2.301  
   2.302  lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
   2.303  
   2.304  lemma compute_floor_fl[code]:
   2.305 -  shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e
   2.306 -                                  else Float (m div (2 ^ (nat (-e)))) 0)"
   2.307 +  "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   2.308    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   2.309  
   2.310  lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
   2.311 @@ -1305,7 +1260,5 @@
   2.312    thus ?thesis by simp
   2.313  qed (simp add: floor_fl_def)
   2.314  
   2.315 -code_datatype Float
   2.316 -
   2.317  end
   2.318