author hoelzl Thu Apr 19 11:55:30 2012 +0200 (2012-04-19) changeset 47601 050718fe6eee parent 47600 e12289b5796b child 47603 b716b16ab2ac
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
```     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.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.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.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