use lifting to introduce floating point numbers
authorhoelzl
Wed Apr 18 14:29:22 2012 +0200 (2012-04-18)
changeset 47600e12289b5796b
parent 47599 400b158f1589
child 47601 050718fe6eee
use lifting to introduce floating point numbers
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 18 14:29:21 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 18 14:29:22 2012 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4    "~~/src/HOL/Library/Efficient_Nat"
     1.5  begin
     1.6  
     1.7 +declare powr_numeral[simp]
     1.8 +declare powr_neg_numeral[simp]
     1.9 +
    1.10  section "Horner Scheme"
    1.11  
    1.12  subsection {* Define auxiliary helper @{text horner} function *}
    1.13 @@ -148,7 +151,7 @@
    1.14    case True
    1.15    show ?thesis
    1.16    proof (cases "0 < l")
    1.17 -    case True hence "odd n \<or> 0 < l" and "0 \<le> real l" unfolding less_float_def by auto
    1.18 +    case True hence "odd n \<or> 0 < l" and "0 \<le> real l" by auto
    1.19      have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms
    1.20        unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
    1.21      have "real l ^ n \<le> x ^ n" and "x ^ n \<le> real u ^ n " using `0 \<le> real l` assms
    1.22 @@ -158,7 +161,7 @@
    1.23      case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
    1.24      show ?thesis
    1.25      proof (cases "u < 0")
    1.26 -      case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms unfolding less_float_def by auto
    1.27 +      case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms  by auto
    1.28        hence "real u ^ n \<le> x ^ n" and "x ^ n \<le> real l ^ n" using power_mono[of  "-x" "-real l" n] power_mono[of "-real u" "-x" n]
    1.29          unfolding power_minus_even[OF `even n`] by auto
    1.30        moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
    1.31 @@ -167,9 +170,9 @@
    1.32        case False
    1.33        have "\<bar>x\<bar> \<le> real (max (-l) u)"
    1.34        proof (cases "-l \<le> u")
    1.35 -        case True thus ?thesis unfolding max_def if_P[OF True] using assms unfolding less_eq_float_def by auto
    1.36 +        case True thus ?thesis unfolding max_def if_P[OF True] using assms by auto
    1.37        next
    1.38 -        case False thus ?thesis unfolding max_def if_not_P[OF False] using assms unfolding less_eq_float_def by auto
    1.39 +        case False thus ?thesis unfolding max_def if_not_P[OF False] using assms by auto
    1.40        qed
    1.41        hence x_abs: "\<bar>x\<bar> \<le> \<bar>real (max (-l) u)\<bar>" by auto
    1.42        have u1: "u1 = (max (-l) u) ^ n" and l1: "l1 = 0" using assms unfolding float_power_bnds_def if_not_P[OF P] if_not_P[OF False] by auto
    1.43 @@ -215,7 +218,7 @@
    1.44                else if x < 0 then - ub_sqrt prec (- x)
    1.45                              else 0)"
    1.46  by pat_completeness auto
    1.47 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
    1.48 +termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
    1.49  
    1.50  declare lb_sqrt.simps[simp del]
    1.51  declare ub_sqrt.simps[simp del]
    1.52 @@ -284,7 +287,7 @@
    1.53      qed
    1.54      finally show ?thesis using `0 < m`
    1.55        unfolding Float
    1.56 -      by (subst compute_sqrt_iteration_base) (simp add: ac_simps real_Float del: Float_def)
    1.57 +      by (subst compute_sqrt_iteration_base) (simp add: ac_simps)
    1.58    qed
    1.59  next
    1.60    case (Suc n)
    1.61 @@ -308,20 +311,20 @@
    1.62  lemma lb_sqrt_lower_bound: assumes "0 \<le> real x"
    1.63    shows "0 \<le> real (lb_sqrt prec x)"
    1.64  proof (cases "0 < x")
    1.65 -  case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` unfolding less_float_def less_eq_float_def by auto
    1.66 -  hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto
    1.67 +  case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` by auto
    1.68 +  hence "0 < sqrt_iteration prec prec x" using sqrt_iteration_lower_bound by auto
    1.69    hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \<le> x`] unfolding less_eq_float_def by auto
    1.70    thus ?thesis unfolding lb_sqrt.simps using True by auto
    1.71  next
    1.72 -  case False with `0 \<le> real x` have "real x = 0" unfolding less_float_def by auto
    1.73 -  thus ?thesis unfolding lb_sqrt.simps less_float_def by auto
    1.74 +  case False with `0 \<le> real x` have "real x = 0" by auto
    1.75 +  thus ?thesis unfolding lb_sqrt.simps by auto
    1.76  qed
    1.77  
    1.78  lemma bnds_sqrt':
    1.79    shows "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x) }"
    1.80  proof -
    1.81    { fix x :: float assume "0 < x"
    1.82 -    hence "0 < real x" and "0 \<le> real x" unfolding less_float_def by auto
    1.83 +    hence "0 < real x" and "0 \<le> real x" by auto
    1.84      hence sqrt_gt0: "0 < sqrt x" by auto
    1.85      hence sqrt_ub: "sqrt x < sqrt_iteration prec prec x" using sqrt_iteration_bound by auto
    1.86  
    1.87 @@ -338,7 +341,7 @@
    1.88    note lb = this
    1.89  
    1.90    { fix x :: float assume "0 < x"
    1.91 -    hence "0 < real x" unfolding less_float_def by auto
    1.92 +    hence "0 < real x" by auto
    1.93      hence "0 < sqrt x" by auto
    1.94      hence "sqrt x < sqrt_iteration prec prec x"
    1.95        using sqrt_iteration_bound by auto
    1.96 @@ -352,10 +355,10 @@
    1.97    next case False show ?thesis
    1.98    proof (cases "real x = 0")
    1.99      case True thus ?thesis
   1.100 -      by (auto simp add: less_float_def lb_sqrt.simps ub_sqrt.simps)
   1.101 +      by (auto simp add: lb_sqrt.simps ub_sqrt.simps)
   1.102    next
   1.103      case False with `\<not> 0 < x` have "x < 0" and "0 < -x"
   1.104 -      by (auto simp add: less_float_def)
   1.105 +      by auto
   1.106  
   1.107      with `\<not> 0 < x`
   1.108      show ?thesis using lb[OF `0 < -x`] ub[OF `0 < -x`]
   1.109 @@ -553,7 +556,7 @@
   1.110                                             else Float 1 1 * ub_horner y
   1.111                            else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
   1.112  by pat_completeness auto
   1.113 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
   1.114 +termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto)
   1.115  
   1.116  declare ub_arctan_horner.simps[simp del]
   1.117  declare lb_arctan_horner.simps[simp del]
   1.118 @@ -561,17 +564,17 @@
   1.119  lemma lb_arctan_bound': assumes "0 \<le> real x"
   1.120    shows "lb_arctan prec x \<le> arctan x"
   1.121  proof -
   1.122 -  have "\<not> x < 0" and "0 \<le> x" unfolding less_float_def less_eq_float_def using `0 \<le> real x` by auto
   1.123 +  have "\<not> x < 0" and "0 \<le> x" using `0 \<le> real x` by auto
   1.124    let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)"
   1.125      and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
   1.126  
   1.127    show ?thesis
   1.128    proof (cases "x \<le> Float 1 -1")
   1.129 -    case True hence "real x \<le> 1" unfolding less_eq_float_def Float_num by auto
   1.130 +    case True hence "real x \<le> 1" by auto
   1.131      show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
   1.132        using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
   1.133    next
   1.134 -    case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto
   1.135 +    case False hence "0 < real x" by auto
   1.136      let ?R = "1 + sqrt (1 + real x * real x)"
   1.137      let ?fR = "1 + ub_sqrt prec (1 + x * x)"
   1.138      let ?DIV = "float_divl prec x ?fR"
   1.139 @@ -583,7 +586,7 @@
   1.140        using bnds_sqrt'[of "1 + x * x"] by auto
   1.141  
   1.142      hence "?R \<le> ?fR" by auto
   1.143 -    hence "0 < ?fR" and "0 < real ?fR" unfolding less_float_def using `0 < ?R` by auto
   1.144 +    hence "0 < ?fR" and "0 < real ?fR" using `0 < ?R` by auto
   1.145  
   1.146      have monotone: "(float_divl prec x ?fR) \<le> x / ?R"
   1.147      proof -
   1.148 @@ -613,7 +616,7 @@
   1.149        finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
   1.150      next
   1.151        case False
   1.152 -      hence "2 < real x" unfolding less_eq_float_def Float_num by auto
   1.153 +      hence "2 < real x" by auto
   1.154        hence "1 \<le> real x" by auto
   1.155  
   1.156        let "?invx" = "float_divr prec 1 x"
   1.157 @@ -626,7 +629,7 @@
   1.158            using `0 \<le> arctan x` by auto
   1.159        next
   1.160          case False
   1.161 -        hence "real ?invx \<le> 1" unfolding less_float_def by auto
   1.162 +        hence "real ?invx \<le> 1" by auto
   1.163          have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
   1.164  
   1.165          have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
   1.166 @@ -650,18 +653,18 @@
   1.167  lemma ub_arctan_bound': assumes "0 \<le> real x"
   1.168    shows "arctan x \<le> ub_arctan prec x"
   1.169  proof -
   1.170 -  have "\<not> x < 0" and "0 \<le> x" unfolding less_float_def less_eq_float_def using `0 \<le> real x` by auto
   1.171 +  have "\<not> x < 0" and "0 \<le> x" using `0 \<le> real x` by auto
   1.172  
   1.173    let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)"
   1.174      and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
   1.175  
   1.176    show ?thesis
   1.177    proof (cases "x \<le> Float 1 -1")
   1.178 -    case True hence "real x \<le> 1" unfolding less_eq_float_def Float_num by auto
   1.179 +    case True hence "real x \<le> 1" by auto
   1.180      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
   1.181        using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
   1.182    next
   1.183 -    case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto
   1.184 +    case False hence "0 < real x" by auto
   1.185      let ?R = "1 + sqrt (1 + real x * real x)"
   1.186      let ?fR = "1 + lb_sqrt prec (1 + x * x)"
   1.187      let ?DIV = "float_divr prec x ?fR"
   1.188 @@ -695,7 +698,7 @@
   1.189          show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
   1.190        next
   1.191          case False
   1.192 -        hence "real ?DIV \<le> 1" unfolding less_float_def by auto
   1.193 +        hence "real ?DIV \<le> 1" by auto
   1.194  
   1.195          have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
   1.196          hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
   1.197 @@ -709,16 +712,16 @@
   1.198        qed
   1.199      next
   1.200        case False
   1.201 -      hence "2 < real x" unfolding less_eq_float_def Float_num by auto
   1.202 +      hence "2 < real x" by auto
   1.203        hence "1 \<le> real x" by auto
   1.204        hence "0 < real x" by auto
   1.205 -      hence "0 < x" unfolding less_float_def by auto
   1.206 +      hence "0 < x" by auto
   1.207  
   1.208        let "?invx" = "float_divl prec 1 x"
   1.209        have "0 \<le> arctan x" using arctan_monotone'[OF `0 \<le> real x`] using arctan_tan[of 0, unfolded tan_zero] by auto
   1.210  
   1.211        have "real ?invx \<le> 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: `1 \<le> real x` divide_le_eq_1_pos[OF `0 < real x`])
   1.212 -      have "0 \<le> real ?invx" by (rule float_divl_lower_bound[unfolded less_eq_float_def], auto simp add: `0 < x`)
   1.213 +      have "0 \<le> real ?invx" using `0 < x` by (intro float_divl_lower_bound) auto
   1.214  
   1.215        have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
   1.216  
   1.217 @@ -739,11 +742,11 @@
   1.218  lemma arctan_boundaries:
   1.219    "arctan x \<in> {(lb_arctan prec x) .. (ub_arctan prec x)}"
   1.220  proof (cases "0 \<le> x")
   1.221 -  case True hence "0 \<le> real x" unfolding less_eq_float_def by auto
   1.222 +  case True hence "0 \<le> real x" by auto
   1.223    show ?thesis using ub_arctan_bound'[OF `0 \<le> real x`] lb_arctan_bound'[OF `0 \<le> real x`] unfolding atLeastAtMost_iff by auto
   1.224  next
   1.225    let ?mx = "-x"
   1.226 -  case False hence "x < 0" and "0 \<le> real ?mx" unfolding less_eq_float_def less_float_def by auto
   1.227 +  case False hence "x < 0" and "0 \<le> real ?mx" by auto
   1.228    hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx"
   1.229      using ub_arctan_bound'[OF `0 \<le> real ?mx`] lb_arctan_bound'[OF `0 \<le> real ?mx`] by auto
   1.230    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.231 @@ -801,8 +804,8 @@
   1.232    shows "cos x \<in> {(lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) .. (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))}"
   1.233  proof (cases "real x = 0")
   1.234    case False hence "real x \<noteq> 0" by auto
   1.235 -  hence "0 < x" and "0 < real x" using `0 \<le> real x` unfolding less_float_def by auto
   1.236 -  have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero
   1.237 +  hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   1.238 +  have "0 < x * x" using `0 < x`
   1.239      using mult_pos_pos[where a="real x" and b="real x"] by auto
   1.240  
   1.241    { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
   1.242 @@ -918,8 +921,8 @@
   1.243    shows "sin x \<in> {(x * lb_sin_cos_aux prec (get_even n) 2 1 (x * x)) .. (x * ub_sin_cos_aux prec (get_odd n) 2 1 (x * x))}"
   1.244  proof (cases "real x = 0")
   1.245    case False hence "real x \<noteq> 0" by auto
   1.246 -  hence "0 < x" and "0 < real x" using `0 \<le> real x` unfolding less_float_def by auto
   1.247 -  have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero
   1.248 +  hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   1.249 +  have "0 < x * x" using `0 < x`
   1.250      using mult_pos_pos[where a="real x" and b="real x"] by auto
   1.251  
   1.252    { fix x n have "(\<Sum> j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
   1.253 @@ -1036,7 +1039,7 @@
   1.254      finally have "cos x = 2 * cos (x / 2) * cos (x / 2) - 1" .
   1.255    } note x_half = this[symmetric]
   1.256  
   1.257 -  have "\<not> x < 0" using `0 \<le> real x` unfolding less_float_def by auto
   1.258 +  have "\<not> x < 0" using `0 \<le> real x` by auto
   1.259    let "?ub_horner x" = "ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x)"
   1.260    let "?lb_horner x" = "lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x)"
   1.261    let "?ub_half x" = "Float 1 1 * x * x - 1"
   1.262 @@ -1044,7 +1047,7 @@
   1.263  
   1.264    show ?thesis
   1.265    proof (cases "x < Float 1 -1")
   1.266 -    case True hence "x \<le> pi / 2" unfolding less_float_def using pi_ge_two by auto
   1.267 +    case True hence "x \<le> pi / 2" using pi_ge_two by auto
   1.268      show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 -1`] Let_def
   1.269        using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
   1.270    next
   1.271 @@ -1059,7 +1062,7 @@
   1.272          case True show ?thesis using cos_ge_minus_one unfolding if_P[OF True] by auto
   1.273        next
   1.274          case False
   1.275 -        hence "0 \<le> real y" unfolding less_float_def by auto
   1.276 +        hence "0 \<le> real y" by auto
   1.277          from mult_mono[OF `y \<le> cos ?x2` `y \<le> cos ?x2` `0 \<le> cos ?x2` this]
   1.278          have "real y * real y \<le> cos ?x2 * cos ?x2" .
   1.279          hence "2 * real y * real y \<le> 2 * cos ?x2 * cos ?x2" by auto
   1.280 @@ -1091,7 +1094,7 @@
   1.281  
   1.282      show ?thesis
   1.283      proof (cases "x < 1")
   1.284 -      case True hence "real x \<le> 1" unfolding less_float_def by auto
   1.285 +      case True hence "real x \<le> 1" by auto
   1.286        have "0 \<le> real ?x2" and "?x2 \<le> pi / 2" using pi_ge_two `0 \<le> real x` using assms by auto
   1.287        from cos_boundaries[OF this]
   1.288        have lb: "(?lb_horner ?x2) \<le> ?cos ?x2" and ub: "?cos ?x2 \<le> (?ub_horner ?x2)" by auto
   1.289 @@ -1113,7 +1116,7 @@
   1.290        from cos_boundaries[OF this]
   1.291        have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
   1.292  
   1.293 -      have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by simp
   1.294 +      have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by transfer simp
   1.295  
   1.296        have "(?lb x) \<le> ?cos x"
   1.297        proof -
   1.298 @@ -1197,7 +1200,7 @@
   1.299      using x unfolding k[symmetric]
   1.300      by (cases "k = 0")
   1.301         (auto intro!: add_mono
   1.302 -                simp add: diff_minus k[symmetric] less_float_def
   1.303 +                simp add: diff_minus k[symmetric]
   1.304                  simp del: float_of_numeral)
   1.305    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
   1.306    hence lx_less_ux: "?lx \<le> real ?ux" by (rule order_trans)
   1.307 @@ -1205,7 +1208,7 @@
   1.308    { assume "- ?lpi \<le> ?lx" and x_le_0: "x - k * (2 * pi) \<le> 0"
   1.309      with lpi[THEN le_imp_neg_le] lx
   1.310      have pi_lx: "- pi \<le> ?lx" and lx_0: "real ?lx \<le> 0"
   1.311 -      by (simp_all add: less_eq_float_def)
   1.312 +      by simp_all
   1.313  
   1.314      have "(lb_cos prec (- ?lx)) \<le> cos (real (- ?lx))"
   1.315        using lb_cos_minus[OF pi_lx lx_0] by simp
   1.316 @@ -1220,7 +1223,7 @@
   1.317    { assume "0 \<le> ?lx" and pi_x: "x - k * (2 * pi) \<le> pi"
   1.318      with lx
   1.319      have pi_lx: "?lx \<le> pi" and lx_0: "0 \<le> real ?lx"
   1.320 -      by (auto simp add: less_eq_float_def)
   1.321 +      by auto
   1.322  
   1.323      have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
   1.324        using cos_monotone_0_pi'[OF lx_0 lx pi_x]
   1.325 @@ -1235,7 +1238,7 @@
   1.326    { assume pi_x: "- pi \<le> x - k * (2 * pi)" and "?ux \<le> 0"
   1.327      with ux
   1.328      have pi_ux: "- pi \<le> ?ux" and ux_0: "real ?ux \<le> 0"
   1.329 -      by (simp_all add: less_eq_float_def)
   1.330 +      by simp_all
   1.331  
   1.332      have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
   1.333        using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
   1.334 @@ -1250,7 +1253,7 @@
   1.335    { assume "?ux \<le> ?lpi" and x_ge_0: "0 \<le> x - k * (2 * pi)"
   1.336      with lpi ux
   1.337      have pi_ux: "?ux \<le> pi" and ux_0: "0 \<le> real ?ux"
   1.338 -      by (simp_all add: less_eq_float_def)
   1.339 +      by simp_all
   1.340  
   1.341      have "(lb_cos prec ?ux) \<le> cos ?ux"
   1.342        using lb_cos[OF ux_0 pi_ux] by simp
   1.343 @@ -1272,7 +1275,7 @@
   1.344      from True lpi[THEN le_imp_neg_le] lx ux
   1.345      have "- pi \<le> x - k * (2 * pi)"
   1.346        and "x - k * (2 * pi) \<le> 0"
   1.347 -      by (auto simp add: less_eq_float_def)
   1.348 +      by auto
   1.349      with True negative_ux negative_lx
   1.350      show ?thesis unfolding l u by simp
   1.351    next case False note 1 = this show ?thesis
   1.352 @@ -1285,7 +1288,7 @@
   1.353      from True lpi lx ux
   1.354      have "0 \<le> x - k * (2 * pi)"
   1.355        and "x - k * (2 * pi) \<le> pi"
   1.356 -      by (auto simp add: less_eq_float_def)
   1.357 +      by auto
   1.358      with True positive_ux positive_lx
   1.359      show ?thesis unfolding l u by simp
   1.360    next case False note 2 = this show ?thesis
   1.361 @@ -1314,16 +1317,16 @@
   1.362        case False hence "pi \<le> x - k * (2 * pi)" by simp
   1.363        hence pi_x: "- pi \<le> x - k * (2 * pi) - 2 * pi" by simp
   1.364  
   1.365 -      have "?ux \<le> 2 * pi" using Cond lpi by (auto simp add: less_eq_float_def)
   1.366 +      have "?ux \<le> 2 * pi" using Cond lpi by auto
   1.367        hence "x - k * (2 * pi) - 2 * pi \<le> 0" using ux by simp
   1.368  
   1.369        have ux_0: "real (?ux - 2 * ?lpi) \<le> 0"
   1.370 -        using Cond by (auto simp add: less_eq_float_def)
   1.371 +        using Cond by auto
   1.372  
   1.373        from 2 and Cond have "\<not> ?ux \<le> ?lpi" by auto
   1.374 -      hence "- ?lpi \<le> ?ux - 2 * ?lpi" by (auto simp add: less_eq_float_def)
   1.375 +      hence "- ?lpi \<le> ?ux - 2 * ?lpi" by auto
   1.376        hence pi_ux: "- pi \<le> (?ux - 2 * ?lpi)"
   1.377 -        using lpi[THEN le_imp_neg_le] by (auto simp add: less_eq_float_def)
   1.378 +        using lpi[THEN le_imp_neg_le] by auto
   1.379  
   1.380        have x_le_ux: "x - k * (2 * pi) - 2 * pi \<le> (?ux - 2 * ?lpi)"
   1.381          using ux lpi by auto
   1.382 @@ -1345,7 +1348,7 @@
   1.383      case True note Cond = this with bnds 1 2 3 4
   1.384      have l: "l = Float -1 0"
   1.385        and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
   1.386 -      by (auto simp add: bnds_cos_def Let_def simp del: neg_numeral_float_Float)
   1.387 +      by (auto simp add: bnds_cos_def Let_def)
   1.388  
   1.389      have "cos x \<le> u"
   1.390      proof (cases "-pi < x - k * (2 * pi)")
   1.391 @@ -1356,17 +1359,17 @@
   1.392        case False hence "x - k * (2 * pi) \<le> -pi" by simp
   1.393        hence pi_x: "x - k * (2 * pi) + 2 * pi \<le> pi" by simp
   1.394  
   1.395 -      have "-2 * pi \<le> ?lx" using Cond lpi by (auto simp add: less_eq_float_def)
   1.396 +      have "-2 * pi \<le> ?lx" using Cond lpi by auto
   1.397  
   1.398        hence "0 \<le> x - k * (2 * pi) + 2 * pi" using lx by simp
   1.399  
   1.400        have lx_0: "0 \<le> real (?lx + 2 * ?lpi)"
   1.401 -        using Cond lpi by (auto simp add: less_eq_float_def)
   1.402 +        using Cond lpi by auto
   1.403  
   1.404        from 1 and Cond have "\<not> -?lpi \<le> ?lx" by auto
   1.405 -      hence "?lx + 2 * ?lpi \<le> ?lpi" by (auto simp add: less_eq_float_def)
   1.406 +      hence "?lx + 2 * ?lpi \<le> ?lpi" by auto
   1.407        hence pi_lx: "(?lx + 2 * ?lpi) \<le> pi"
   1.408 -        using lpi[THEN le_imp_neg_le] by (auto simp add: less_eq_float_def)
   1.409 +        using lpi[THEN le_imp_neg_le] by auto
   1.410  
   1.411        have lx_le_x: "(?lx + 2 * ?lpi) \<le> x - k * (2 * pi) + 2 * pi"
   1.412          using lx lpi by auto
   1.413 @@ -1455,7 +1458,7 @@
   1.414               else if x < - 1  then ub_exp_horner prec (get_odd (prec + 2)) 1 1 (float_divr prec x (- floor_fl x)) ^ (nat (- int_floor_fl x))
   1.415                                else ub_exp_horner prec (get_odd (prec + 2)) 1 1 x)"
   1.416  by pat_completeness auto
   1.417 -termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto simp add: less_float_def)
   1.418 +termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if 0 < x then 1 else 0))", auto)
   1.419  
   1.420  lemma exp_m1_ge_quarter: "(1 / 4 :: real) \<le> exp (- 1)"
   1.421  proof -
   1.422 @@ -1466,22 +1469,22 @@
   1.423      unfolding get_even_def eq4
   1.424      by (auto simp add: compute_lapprox_rat compute_rapprox_rat compute_lapprox_posrat compute_rapprox_posrat rat_precision_def compute_bitlen)
   1.425    also have "\<dots> \<le> exp (- 1 :: float)" using bnds_exp_horner[where x="- 1"] by auto
   1.426 -  finally show ?thesis unfolding real_of_float_minus real_of_float_one by simp
   1.427 +  finally show ?thesis by simp
   1.428  qed
   1.429  
   1.430  lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
   1.431  proof -
   1.432    let "?lb_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
   1.433    let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 -2 else y"
   1.434 -  have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto simp add: less_eq_float_def less_float_def)
   1.435 +  have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
   1.436    moreover { fix x :: float fix num :: nat
   1.437 -    have "0 < real (?horner x) ^ num" using `0 < ?horner x`[unfolded less_float_def real_of_float_zero] by (rule zero_less_power)
   1.438 +    have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
   1.439      also have "\<dots> = (?horner x) ^ num" by auto
   1.440      finally have "0 < real ((?horner x) ^ num)" .
   1.441    }
   1.442    ultimately show ?thesis
   1.443      unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
   1.444 -    by (cases "floor_fl x", cases "x < - 1", auto simp add: less_eq_float_def less_float_def)
   1.445 +    by (cases "floor_fl x", cases "x < - 1", auto)
   1.446  qed
   1.447  
   1.448  lemma exp_boundaries': assumes "x \<le> 0"
   1.449 @@ -1490,13 +1493,13 @@
   1.450    let "?lb_exp_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
   1.451    let "?ub_exp_horner x" = "ub_exp_horner prec (get_odd (prec + 2)) 1 1 x"
   1.452  
   1.453 -  have "real x \<le> 0" and "\<not> x > 0" using `x \<le> 0` unfolding less_eq_float_def less_float_def by auto
   1.454 +  have "real x \<le> 0" and "\<not> x > 0" using `x \<le> 0` by auto
   1.455    show ?thesis
   1.456    proof (cases "x < - 1")
   1.457 -    case False hence "- 1 \<le> real x" unfolding less_float_def by auto
   1.458 +    case False hence "- 1 \<le> real x" by auto
   1.459      show ?thesis
   1.460      proof (cases "?lb_exp_horner x \<le> 0")
   1.461 -      from `\<not> x < - 1` have "- 1 \<le> real x" unfolding less_float_def by auto
   1.462 +      from `\<not> x < - 1` have "- 1 \<le> real x" by auto
   1.463        hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
   1.464        from order_trans[OF exp_m1_ge_quarter this]
   1.465        have "Float 1 -2 \<le> exp x" unfolding Float_num .
   1.466 @@ -1510,8 +1513,8 @@
   1.467  
   1.468      let ?num = "nat (- int_floor_fl x)"
   1.469  
   1.470 -    have "real (int_floor_fl x) < - 1" using int_floor_fl `x < - 1` unfolding less_eq_float_def less_float_def real_of_float_uminus real_of_float_one
   1.471 -      by (rule order_le_less_trans)
   1.472 +    have "real (int_floor_fl x) < - 1" using int_floor_fl[of x] `x < - 1`
   1.473 +      by simp
   1.474      hence "real (int_floor_fl x) < 0" by simp
   1.475      hence "int_floor_fl x < 0" by auto
   1.476      hence "1 \<le> - int_floor_fl x" by auto
   1.477 @@ -1550,7 +1553,7 @@
   1.478  
   1.479        show ?thesis
   1.480        proof (cases "?horner \<le> 0")
   1.481 -        case False hence "0 \<le> real ?horner" unfolding less_eq_float_def by auto
   1.482 +        case False hence "0 \<le> real ?horner" by auto
   1.483  
   1.484          have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
   1.485            using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
   1.486 @@ -1586,10 +1589,10 @@
   1.487  proof -
   1.488    show ?thesis
   1.489    proof (cases "0 < x")
   1.490 -    case False hence "x \<le> 0" unfolding less_float_def less_eq_float_def by auto
   1.491 +    case False hence "x \<le> 0" by auto
   1.492      from exp_boundaries'[OF this] show ?thesis .
   1.493    next
   1.494 -    case True hence "-x \<le> 0" unfolding less_float_def less_eq_float_def by auto
   1.495 +    case True hence "-x \<le> 0" by auto
   1.496  
   1.497      have "lb_exp prec x \<le> exp x"
   1.498      proof -
   1.499 @@ -1605,15 +1608,14 @@
   1.500      moreover
   1.501      have "exp x \<le> ub_exp prec x"
   1.502      proof -
   1.503 -      have "\<not> 0 < -x" using `0 < x` unfolding less_float_def by auto
   1.504 +      have "\<not> 0 < -x" using `0 < x` by auto
   1.505  
   1.506        from exp_boundaries'[OF `-x \<le> 0`]
   1.507        have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
   1.508  
   1.509        have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
   1.510 -        using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_zero],
   1.511 -                                                symmetric]]
   1.512 -        unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide real_of_float_one by auto
   1.513 +        using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
   1.514 +        by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
   1.515        also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))" using float_divr .
   1.516        finally show ?thesis unfolding ub_exp.simps if_P[OF True] .
   1.517      qed
   1.518 @@ -1778,16 +1780,15 @@
   1.519  by pat_completeness auto
   1.520  
   1.521  termination proof (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 1 then 1 else 0))", auto)
   1.522 -  fix prec x assume "\<not> x \<le> 0" and "x < 1" and "float_divl (max prec (Suc 0)) 1 x < 1"
   1.523 -  hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1"
   1.524 -    unfolding less_float_def less_eq_float_def by auto
   1.525 +  fix prec and x :: float assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divl (max prec (Suc 0)) 1 x) < 1"
   1.526 +  hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
   1.527    from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1` `1 \<le> max prec (Suc 0)`]
   1.528 -  show False using `float_divl (max prec (Suc 0)) 1 x < 1` unfolding less_float_def less_eq_float_def by auto
   1.529 +  show False using `real (float_divl (max prec (Suc 0)) 1 x) < 1` by auto
   1.530  next
   1.531 -  fix prec x assume "\<not> x \<le> 0" and "x < 1" and "float_divr prec 1 x < 1"
   1.532 -  hence "0 < x" unfolding less_float_def less_eq_float_def by auto
   1.533 -  from float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`, of prec]
   1.534 -  show False using `float_divr prec 1 x < 1` unfolding less_float_def less_eq_float_def by auto
   1.535 +  fix prec x assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divr prec 1 x) < 1"
   1.536 +  hence "0 < x" by auto
   1.537 +  from float_divr_pos_less1_lower_bound[OF `0 < x`, of prec] `real x < 1`
   1.538 +  show False using `real (float_divr prec 1 x) < 1` by auto
   1.539  qed
   1.540  
   1.541  lemma float_pos_eq_mantissa_pos:  "x > 0 \<longleftrightarrow> mantissa x > 0"
   1.542 @@ -1811,24 +1812,20 @@
   1.543      and "Float (mantissa x) (- (bitlen (mantissa x) - 1)) = Float m ( - (bitlen m - 1))"  (is ?th2)
   1.544  proof -
   1.545    from assms have mantissa_pos: "m > 0" "mantissa x > 0"
   1.546 -    using Float_pos_eq_mantissa_pos float_pos_eq_mantissa_pos by simp_all
   1.547 -  thus ?th1 using bitlen_Float[of m e] assms by (simp add: less_float_def zero_less_mult_iff)
   1.548 -  from assms have "x \<noteq> float_of 0" by (auto simp add: zero_float_def zero_less_mult_iff)
   1.549 +    using Float_pos_eq_mantissa_pos[of m e] float_pos_eq_mantissa_pos[of x] by simp_all
   1.550 +  thus ?th1 using bitlen_Float[of m e] assms by (auto simp add: zero_less_mult_iff intro!: arg_cong2[where f=Float])
   1.551 +  have "x \<noteq> float_of 0"
   1.552 +    unfolding zero_float_def[symmetric] using `0 < x` by auto
   1.553    from denormalize_shift[OF assms(1) this] guess i . note i = this
   1.554 -  from `x \<noteq> float_of 0` have "mantissa x \<noteq> 0" by (simp add: mantissa_noteq_0)
   1.555 -  from assms
   1.556 -  have "real (mantissa x) * 2 powr (1 - real (bitlen (mantissa x))) \<in> float"
   1.557 -    using two_powr_int_float[of "1 - bitlen (mantissa x)"] by simp
   1.558 -  moreover
   1.559 +
   1.560    have "2 powr (1 - (real (bitlen (mantissa x)) + real i)) =
   1.561      2 powr (1 - (real (bitlen (mantissa x)))) * inverse (2 powr (real i))"
   1.562      by (simp add: powr_minus[symmetric] powr_add[symmetric] field_simps)
   1.563    hence "real (mantissa x) * 2 powr (1 - real (bitlen (mantissa x))) =
   1.564      (real (mantissa x) * 2 ^ i) * 2 powr (1 - real (bitlen (mantissa x * 2 ^ i)))"
   1.565      using `mantissa x > 0` by (simp add: powr_realpow)
   1.566 -  ultimately
   1.567 -  show ?th2
   1.568 -    using two_powr_int_float[of "1 - bitlen (mantissa x)"] by (simp add: i)
   1.569 +  then show ?th2
   1.570 +    unfolding i by transfer auto
   1.571  qed
   1.572  
   1.573  lemma compute_ln[code]:
   1.574 @@ -1854,7 +1851,7 @@
   1.575  proof -
   1.576    from assms Float_pos_eq_mantissa_pos have "x > 0 \<Longrightarrow> m > 0" by simp
   1.577    thus ?th1 ?th2 using Float_representation_aux[of m e] unfolding x_def[symmetric]
   1.578 -    by (auto simp add: simp del: Float_def dest: not_leE)
   1.579 +    by (auto dest: not_leE)
   1.580  qed
   1.581  
   1.582  lemma ln_shifted_float: assumes "0 < m" shows "ln (Float m e) = ln 2 * (e + (bitlen m - 1)) + ln (Float m (- (bitlen m - 1)))"
   1.583 @@ -1893,9 +1890,9 @@
   1.584    (is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
   1.585  proof (cases "x < Float 1 1")
   1.586    case True
   1.587 -  hence "real (x - 1) < 1" and "real x < 2" unfolding less_float_def Float_num by auto
   1.588 -  have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` unfolding less_float_def less_eq_float_def by auto
   1.589 -  hence "0 \<le> real (x - 1)" using `1 \<le> x` unfolding less_float_def Float_num by auto
   1.590 +  hence "real (x - 1) < 1" and "real x < 2" by auto
   1.591 +  have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
   1.592 +  hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
   1.593  
   1.594    have [simp]: "(Float 3 -1) = 3 / 2" by simp
   1.595  
   1.596 @@ -1906,7 +1903,7 @@
   1.597        using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
   1.598        by auto
   1.599    next
   1.600 -    case False hence *: "3 / 2 < x" by (auto simp add: less_eq_float_def)
   1.601 +    case False hence *: "3 / 2 < x" by auto
   1.602  
   1.603      with ln_add[of "3 / 2" "x - 3 / 2"]
   1.604      have add: "ln x = ln (3 / 2) + ln (real x * 2 / 3)"
   1.605 @@ -1975,8 +1972,7 @@
   1.606  next
   1.607    case False
   1.608    hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
   1.609 -    using `1 \<le> x` unfolding less_float_def less_eq_float_def
   1.610 -    by auto
   1.611 +    using `1 \<le> x` by auto
   1.612    show ?thesis
   1.613    proof -
   1.614      def m \<equiv> "mantissa x"
   1.615 @@ -1986,7 +1982,7 @@
   1.616      let ?x = "Float m (- (bitlen m - 1))"
   1.617  
   1.618      have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
   1.619 -      by (auto simp: less_float_def less_eq_float_def zero_less_mult_iff)
   1.620 +      by (auto simp: zero_less_mult_iff)
   1.621      def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
   1.622      have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
   1.623      from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
   1.624 @@ -2040,15 +2036,15 @@
   1.625    case False hence "1 \<le> x" unfolding less_float_def less_eq_float_def by auto
   1.626    show ?thesis using ub_ln_lb_ln_bounds'[OF `1 \<le> x`] .
   1.627  next
   1.628 -  case True have "\<not> x \<le> 0" using `0 < x` unfolding less_float_def less_eq_float_def by auto
   1.629 -  from True have "real x < 1" by (simp add: less_float_def)
   1.630 -  have "0 < real x" and "real x \<noteq> 0" using `0 < x` unfolding less_float_def by auto
   1.631 +  case True have "\<not> x \<le> 0" using `0 < x` by auto
   1.632 +  from True have "real x < 1" by simp
   1.633 +  have "0 < real x" and "real x \<noteq> 0" using `0 < x` by auto
   1.634    hence A: "0 < 1 / real x" by auto
   1.635  
   1.636    {
   1.637      let ?divl = "float_divl (max prec 1) 1 x"
   1.638 -    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`] unfolding less_eq_float_def less_float_def by auto
   1.639 -    hence B: "0 < real ?divl" unfolding less_eq_float_def by auto
   1.640 +    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`] by auto
   1.641 +    hence B: "0 < real ?divl" by auto
   1.642  
   1.643      have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
   1.644      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.645 @@ -2058,7 +2054,7 @@
   1.646    {
   1.647      let ?divr = "float_divr prec 1 x"
   1.648      have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`] unfolding less_eq_float_def less_float_def by auto
   1.649 -    hence B: "0 < real ?divr" unfolding less_eq_float_def by auto
   1.650 +    hence B: "0 < real ?divr" by auto
   1.651  
   1.652      have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
   1.653      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.654 @@ -2077,7 +2073,7 @@
   1.655      assume "\<not> 0 < x" hence "x \<le> 0" unfolding less_eq_float_def less_float_def by auto
   1.656      thus False using assms by auto
   1.657    qed
   1.658 -  thus "0 < real x" unfolding less_float_def by auto
   1.659 +  thus "0 < real x" by auto
   1.660    have "the (lb_ln prec x) \<le> ln x" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
   1.661    thus "y \<le> ln x" unfolding assms[symmetric] by auto
   1.662  qed
   1.663 @@ -2087,10 +2083,10 @@
   1.664  proof -
   1.665    have "0 < x"
   1.666    proof (rule ccontr)
   1.667 -    assume "\<not> 0 < x" hence "x \<le> 0" unfolding less_eq_float_def less_float_def by auto
   1.668 +    assume "\<not> 0 < x" hence "x \<le> 0" by auto
   1.669      thus False using assms by auto
   1.670    qed
   1.671 -  thus "0 < real x" unfolding less_float_def by auto
   1.672 +  thus "0 < real x" by auto
   1.673    have "ln x \<le> the (ub_ln prec x)" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
   1.674    thus "ln x \<le> y" unfolding assms[symmetric] by auto
   1.675  qed
   1.676 @@ -2470,13 +2466,13 @@
   1.677      and l1: "l1 \<le> interpret_floatarith a xs" and u1: "interpret_floatarith a xs \<le> u1" by blast
   1.678    have either: "0 < l1 \<or> u1 < 0" proof (rule ccontr) assume P: "\<not> (0 < l1 \<or> u1 < 0)" show False using l' unfolding if_not_P[OF P] by auto qed
   1.679    moreover have l1_le_u1: "real l1 \<le> real u1" using l1 u1 by auto
   1.680 -  ultimately have "real l1 \<noteq> 0" and "real u1 \<noteq> 0" unfolding less_float_def by auto
   1.681 +  ultimately have "real l1 \<noteq> 0" and "real u1 \<noteq> 0" by auto
   1.682  
   1.683    have inv: "inverse u1 \<le> inverse (interpret_floatarith a xs)
   1.684             \<and> inverse (interpret_floatarith a xs) \<le> inverse l1"
   1.685    proof (cases "0 < l1")
   1.686      case True hence "0 < real u1" and "0 < real l1" "0 < interpret_floatarith a xs"
   1.687 -      unfolding less_float_def using l1_le_u1 l1 by auto
   1.688 +      using l1_le_u1 l1 by auto
   1.689      show ?thesis
   1.690        unfolding inverse_le_iff_le[OF `0 < real u1` `0 < interpret_floatarith a xs`]
   1.691          inverse_le_iff_le[OF `0 < interpret_floatarith a xs` `0 < real l1`]
   1.692 @@ -2484,7 +2480,7 @@
   1.693    next
   1.694      case False hence "u1 < 0" using either by blast
   1.695      hence "real u1 < 0" and "real l1 < 0" "interpret_floatarith a xs < 0"
   1.696 -      unfolding less_float_def using l1_le_u1 u1 by auto
   1.697 +      using l1_le_u1 u1 by auto
   1.698      show ?thesis
   1.699        unfolding inverse_le_iff_le_neg[OF `real u1 < 0` `interpret_floatarith a xs < 0`]
   1.700          inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
   1.701 @@ -2505,7 +2501,7 @@
   1.702    from lift_un'[OF Abs.prems[unfolded approx.simps], unfolded fst_conv snd_conv] Abs.hyps
   1.703    obtain l1 u1 where l': "l = (if l1 < 0 \<and> 0 < u1 then 0 else min \<bar>l1\<bar> \<bar>u1\<bar>)" and u': "u = max \<bar>l1\<bar> \<bar>u1\<bar>"
   1.704      and l1: "l1 \<le> interpret_floatarith x xs" and u1: "interpret_floatarith x xs \<le> u1" by blast
   1.705 -  thus ?case unfolding l' u' by (cases "l1 < 0 \<and> 0 < u1", auto simp add: real_of_float_min real_of_float_max less_float_def)
   1.706 +  thus ?case unfolding l' u' by (cases "l1 < 0 \<and> 0 < u1", auto simp add: real_of_float_min real_of_float_max)
   1.707  next
   1.708    case (Min a b)
   1.709    from lift_bin'[OF Min.prems[unfolded approx.simps], unfolded fst_conv snd_conv] Min.hyps
   1.710 @@ -2664,7 +2660,7 @@
   1.711      and inequality: "u < l'"
   1.712      by (cases "approx prec a vs", auto,
   1.713        cases "approx prec b vs", auto)
   1.714 -  from inequality[unfolded less_float_def] approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
   1.715 +  from inequality approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
   1.716    show ?case by auto
   1.717  next
   1.718    case (LessEqual a b)
   1.719 @@ -2674,7 +2670,7 @@
   1.720      and inequality: "u \<le> l'"
   1.721      by (cases "approx prec a vs", auto,
   1.722        cases "approx prec b vs", auto)
   1.723 -  from inequality[unfolded less_eq_float_def] approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
   1.724 +  from inequality approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
   1.725    show ?case by auto
   1.726  next
   1.727    case (AtLeastAtMost x a b)
   1.728 @@ -2686,7 +2682,7 @@
   1.729      by (cases "approx prec x vs", auto,
   1.730        cases "approx prec a vs", auto,
   1.731        cases "approx prec b vs", auto, blast)
   1.732 -  from inequality[unfolded less_eq_float_def] approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
   1.733 +  from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
   1.734    show ?case by auto
   1.735  qed
   1.736  
   1.737 @@ -2750,7 +2746,6 @@
   1.738    apply (auto intro!: DERIV_intros
   1.739             simp del: interpret_floatarith.simps(5)
   1.740             simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
   1.741 -  apply (simp add: cos_sin_eq)
   1.742    done
   1.743  next case (Power a n) thus ?case
   1.744    by (cases n, auto intro!: DERIV_intros
   1.745 @@ -2794,7 +2789,7 @@
   1.746      and *: "0 < l \<or> u < 0"
   1.747      by (cases "approx prec a vs", auto)
   1.748    with approx[OF `bounded_by xs vs` approx_Some]
   1.749 -  have "interpret_floatarith a xs \<noteq> 0" unfolding less_float_def by auto
   1.750 +  have "interpret_floatarith a xs \<noteq> 0" by auto
   1.751    thus ?case using Inverse by auto
   1.752  next
   1.753    case (Ln a)
   1.754 @@ -2802,7 +2797,7 @@
   1.755      and *: "0 < l"
   1.756      by (cases "approx prec a vs", auto)
   1.757    with approx[OF `bounded_by xs vs` approx_Some]
   1.758 -  have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
   1.759 +  have "0 < interpret_floatarith a xs" by auto
   1.760    thus ?case using Ln by auto
   1.761  next
   1.762    case (Sqrt a)
   1.763 @@ -2810,7 +2805,7 @@
   1.764      and *: "0 < l"
   1.765      by (cases "approx prec a vs", auto)
   1.766    with approx[OF `bounded_by xs vs` approx_Some]
   1.767 -  have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
   1.768 +  have "0 < interpret_floatarith a xs" by auto
   1.769    thus ?case using Sqrt by auto
   1.770  next
   1.771    case (Power a n) thus ?case by (cases n, auto)
   1.772 @@ -3160,7 +3155,7 @@
   1.773    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
   1.774    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
   1.775      by (auto simp add: diff_minus)
   1.776 -  from order_less_le_trans[OF `0 < ly`[unfolded less_float_def] this]
   1.777 +  from order_less_le_trans[OF _ this, of 0] `0 < ly`
   1.778    show ?thesis by auto
   1.779  qed
   1.780  
   1.781 @@ -3182,7 +3177,7 @@
   1.782    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
   1.783    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
   1.784      by (auto simp add: diff_minus)
   1.785 -  from order_trans[OF `0 \<le> ly`[unfolded less_eq_float_def] this]
   1.786 +  from order_trans[OF _ this, of 0] `0 \<le> ly`
   1.787    show ?thesis by auto
   1.788  qed
   1.789  
     2.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Apr 18 14:29:21 2012 +0200
     2.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Apr 18 14:29:22 2012 +0200
     2.3 @@ -36,19 +36,19 @@
     2.4  section "Compute some transcendental values"
     2.5  
     2.6  lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
     2.7 -  by (approximation 80)
     2.8 +  by (approximation 60)
     2.9  
    2.10  lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
    2.11 -  by (approximation 80)
    2.12 +  by (approximation 40)
    2.13  
    2.14  lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16"
    2.15 -  by (approximation 80)
    2.16 +  by (approximation 60)
    2.17  
    2.18  lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18"
    2.19 -  by (approximation 80)
    2.20 +  by (approximation 70)
    2.21  
    2.22  lemma "\<bar> sin 100 + 0.50636564110975879 \<bar> < inverse 10 ^ 17"
    2.23 -  by (approximation 80)
    2.24 +  by (approximation 70)
    2.25  
    2.26  section "Use variable ranges"
    2.27  
    2.28 @@ -70,7 +70,7 @@
    2.29  lemma
    2.30    defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
    2.31    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
    2.32 -  using assms by (approximation 80)
    2.33 +  using assms by (approximation 20)
    2.34  
    2.35  lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
    2.36    by (approximation 30 splitting: x=1 taylor: x = 3)
     3.1 --- a/src/HOL/Library/Float.thy	Wed Apr 18 14:29:21 2012 +0200
     3.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 18 14:29:22 2012 +0200
     3.3 @@ -8,17 +8,17 @@
     3.4    morphisms real_of_float float_of
     3.5    by auto
     3.6  
     3.7 -declare [[coercion "real::float\<Rightarrow>real"]]
     3.8 +setup_lifting type_definition_float
     3.9  
    3.10  lemmas float_of_inject[simp]
    3.11 -lemmas float_of_cases2 = float_of_cases[case_product float_of_cases]
    3.12 -lemmas float_of_cases3 = float_of_cases2[case_product float_of_cases]
    3.13  
    3.14  defs (overloaded)
    3.15 -  real_of_float_def[code_unfold]: "real == real_of_float"
    3.16 +  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
    3.17  
    3.18 -lemma real_of_float_eq[simp]:
    3.19 -  fixes f1 f2 :: float shows "real f1 = real f2 \<longleftrightarrow> f1 = f2"
    3.20 +declare [[coercion "real :: float \<Rightarrow> real"]]
    3.21 +
    3.22 +lemma real_of_float_eq:
    3.23 +  fixes f1 f2 :: float shows "f1 = f2 \<longleftrightarrow> real f1 = real f2"
    3.24    unfolding real_of_float_def real_of_float_inject ..
    3.25  
    3.26  lemma float_of_real[simp]: "float_of (real x) = x"
    3.27 @@ -27,6 +27,10 @@
    3.28  lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
    3.29    unfolding real_of_float_def by (rule float_of_inverse)
    3.30  
    3.31 +lemma transfer_real_of_float [transfer_rule]:
    3.32 +  "(fun_rel cr_float op =) (\<lambda>x. x) real"
    3.33 +  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def)
    3.34 +
    3.35  subsection {* Real operations preserving the representation as floating point number *}
    3.36  
    3.37  lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
    3.38 @@ -37,7 +41,7 @@
    3.39  lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp  
    3.40  lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
    3.41  lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
    3.42 -lemma real_of_nat_float[simp]: "real (x ::nat) \<in> float" by (intro floatI[of x 0]) simp
    3.43 +lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
    3.44  lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
    3.45  lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float" by (intro floatI[of 1 i]) simp
    3.46  lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
    3.47 @@ -119,232 +123,117 @@
    3.48    finally show ?thesis .
    3.49  qed
    3.50  
    3.51 +lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
    3.52 +
    3.53  subsection {* Arithmetic operations on floating point numbers *}
    3.54  
    3.55 -instantiation float :: ring_1
    3.56 +instantiation float :: "{ring_1, linorder, linordered_ring, linordered_idom, numeral, equal}"
    3.57  begin
    3.58  
    3.59 -definition [simp]: "(0::float) = float_of 0"
    3.60 -
    3.61 -definition [simp]: "(1::float) = float_of 1"
    3.62 -
    3.63 -definition "(x + y::float) = float_of (real x + real y)"
    3.64 -
    3.65 -lemma float_plus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x + float_of y = float_of (x + y)"
    3.66 -  by (simp add: plus_float_def)
    3.67 -
    3.68 -definition "(-x::float) = float_of (- real x)"
    3.69 +lift_definition zero_float :: float is 0 by simp
    3.70 +lift_definition one_float :: float is 1 by simp
    3.71 +lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
    3.72 +lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
    3.73 +lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
    3.74 +lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
    3.75  
    3.76 -lemma uminus_of_float[simp]: "x \<in> float \<Longrightarrow> - float_of x = float_of (- x)"
    3.77 -  by (simp add: uminus_float_def)
    3.78 -
    3.79 -definition "(x - y::float) = float_of (real x - real y)"
    3.80 +lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
    3.81 +lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
    3.82  
    3.83 -lemma float_minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x - float_of y = float_of (x - y)"
    3.84 -  by (simp add: minus_float_def)
    3.85 +lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
    3.86  
    3.87 -definition "(x * y::float) = float_of (real x * real y)"
    3.88 -
    3.89 -lemma float_times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x * float_of y = float_of (x * y)"
    3.90 -  by (simp add: times_float_def)
    3.91 +lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
    3.92 +lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
    3.93  
    3.94  instance
    3.95 -proof
    3.96 -  fix a b c :: float
    3.97 -  show "0 + a = a"
    3.98 -    by (cases a rule: float_of_cases) simp
    3.99 -  show "1 * a = a"
   3.100 -    by (cases a rule: float_of_cases) simp
   3.101 -  show "a * 1 = a"
   3.102 -    by (cases a rule: float_of_cases) simp
   3.103 -  show "-a + a = 0"
   3.104 -    by (cases a rule: float_of_cases) simp
   3.105 -  show "a + b = b + a"
   3.106 -    by (cases a b rule: float_of_cases2) (simp add: ac_simps)
   3.107 -  show "a - b = a + -b"
   3.108 -    by (cases a b rule: float_of_cases2) (simp add: field_simps)
   3.109 -  show "a + b + c = a + (b + c)"
   3.110 -    by (cases a b c rule: float_of_cases3) (simp add: ac_simps)
   3.111 -  show "a * b * c = a * (b * c)"
   3.112 -    by (cases a b c rule: float_of_cases3) (simp add: ac_simps)
   3.113 -  show "(a + b) * c = a * c + b * c"
   3.114 -    by (cases a b c rule: float_of_cases3) (simp add: field_simps)
   3.115 -  show "a * (b + c) = a * b + a * c"
   3.116 -    by (cases a b c rule: float_of_cases3) (simp add: field_simps)
   3.117 -  show "0 \<noteq> (1::float)" by simp
   3.118 -qed
   3.119 +  proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
   3.120  end
   3.121  
   3.122 -lemma real_of_float_uminus[simp]:
   3.123 -  fixes f g::float shows "real (- g) = - real g"
   3.124 -  by (simp add: uminus_float_def)
   3.125 -
   3.126 -lemma real_of_float_plus[simp]:
   3.127 -  fixes f g::float shows "real (f + g) = real f + real g"
   3.128 -  by (simp add: plus_float_def)
   3.129 -
   3.130 -lemma real_of_float_minus[simp]:
   3.131 -  fixes f g::float shows "real (f - g) = real f - real g"
   3.132 -  by (simp add: minus_float_def)
   3.133 -
   3.134 -lemma real_of_float_times[simp]:
   3.135 -  fixes f g::float shows "real (f * g) = real f * real g"
   3.136 -  by (simp add: times_float_def)
   3.137 -
   3.138 -lemma real_of_float_zero[simp]: "real (0::float) = 0" by simp
   3.139 -lemma real_of_float_one[simp]: "real (1::float) = 1" by simp
   3.140 +lemma
   3.141 +  fixes x y :: float
   3.142 +  shows real_of_float_uminus[simp]: "real (- x) = - real x"
   3.143 +    and real_of_float_plus[simp]: "real (y + x) = real y + real x"
   3.144 +    and real_of_float_minus[simp]: "real (y - x) = real y - real x"
   3.145 +    and real_of_float_times[simp]: "real (y * x) = real y * real x"
   3.146 +    and real_of_float_zero[simp]: "real (0::float) = 0"
   3.147 +    and real_of_float_one[simp]: "real (1::float) = 1"
   3.148 +    and real_of_float_le[simp]: "x \<le> y \<longleftrightarrow> real x \<le> real y"
   3.149 +    and real_of_float_less[simp]: "x < y \<longleftrightarrow> real x < real y"
   3.150 +    and real_of_float_abs[simp]: "real (abs x) = abs (real x)"
   3.151 +    and real_of_float_sgn[simp]: "real (sgn x) = sgn (real x)"
   3.152 +  using uminus_float.rep_eq plus_float.rep_eq minus_float.rep_eq times_float.rep_eq
   3.153 +    zero_float.rep_eq one_float.rep_eq less_eq_float.rep_eq less_float.rep_eq
   3.154 +    abs_float.rep_eq sgn_float.rep_eq
   3.155 +  by (simp_all add: real_of_float_def)
   3.156  
   3.157  lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
   3.158    by (induct n) simp_all
   3.159  
   3.160 -instantiation float :: linorder
   3.161 -begin
   3.162 -
   3.163 -definition "x \<le> (y::float) \<longleftrightarrow> real x \<le> real y"
   3.164 -
   3.165 -lemma float_le_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x \<le> float_of y \<longleftrightarrow> x \<le> y"
   3.166 -  by (simp add: less_eq_float_def)
   3.167 -
   3.168 -definition "x < (y::float) \<longleftrightarrow> real x < real y"
   3.169 -
   3.170 -lemma float_less_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x < float_of y \<longleftrightarrow> x < y"
   3.171 -  by (simp add: less_float_def)
   3.172 -
   3.173 -instance
   3.174 -proof
   3.175 -  fix a b c :: float
   3.176 -  show "a \<le> a"
   3.177 -    by (cases a rule: float_of_cases) simp
   3.178 -  show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
   3.179 -    by (cases a b rule: float_of_cases2) auto
   3.180 -  show "a \<le> b \<or> b \<le> a"
   3.181 -    by (cases a b rule: float_of_cases2) auto
   3.182 -  { assume "a \<le> b" "b \<le> a" then show "a = b"
   3.183 -    by (cases a b rule: float_of_cases2) auto }
   3.184 -  { assume "a \<le> b" "b \<le> c" then show "a \<le> c"
   3.185 -    by (cases a b c rule: float_of_cases3) auto }
   3.186 -qed
   3.187 -end
   3.188 -
   3.189 -lemma real_of_float_min: fixes a b::float shows "real (min a b) = min (real a) (real b)"
   3.190 -  by (simp add: min_def less_eq_float_def)
   3.191 -
   3.192 -lemma real_of_float_max: fixes a b::float shows "real (max a b) = max (real a) (real b)"
   3.193 -  by (simp add: max_def less_eq_float_def)
   3.194 -
   3.195 -instantiation float :: linordered_ring
   3.196 -begin
   3.197 -
   3.198 -definition "(abs x :: float) = float_of (abs (real x))"
   3.199 -
   3.200 -lemma float_abs[simp]: "x \<in> float \<Longrightarrow> abs (float_of x) = float_of (abs x)"
   3.201 -  by (simp add: abs_float_def)
   3.202 -
   3.203 -instance
   3.204 -proof
   3.205 -  fix a b c :: float
   3.206 -  show "\<bar>a\<bar> = (if a < 0 then - a else a)"
   3.207 -    by (cases a rule: float_of_cases) simp
   3.208 -  assume "a \<le> b"
   3.209 -  then show "c + a \<le> c + b"
   3.210 -    by (cases a b c rule: float_of_cases3) simp
   3.211 -  assume "0 \<le> c"
   3.212 -  with `a \<le> b` show "c * a \<le> c * b"
   3.213 -    by (cases a b c rule: float_of_cases3) (auto intro: mult_left_mono)
   3.214 -  from `0 \<le> c` `a \<le> b` show "a * c \<le> b * c"
   3.215 -    by (cases a b c rule: float_of_cases3) (auto intro: mult_right_mono)
   3.216 -qed
   3.217 -end
   3.218 -
   3.219 -lemma real_of_abs_float[simp]: fixes f::float shows "real (abs f) = abs (real f)"
   3.220 -  unfolding abs_float_def by simp
   3.221 +lemma fixes x y::float 
   3.222 +  shows real_of_float_min: "real (min x y) = min (real x) (real y)"
   3.223 +    and real_of_float_max: "real (max x y) = max (real x) (real y)"
   3.224 +  by (simp_all add: min_def max_def)
   3.225  
   3.226  instance float :: dense_linorder
   3.227  proof
   3.228    fix a b :: float
   3.229    show "\<exists>c. a < c"
   3.230      apply (intro exI[of _ "a + 1"])
   3.231 -    apply (cases a rule: float_of_cases)
   3.232 +    apply transfer
   3.233      apply simp
   3.234      done
   3.235    show "\<exists>c. c < a"
   3.236      apply (intro exI[of _ "a - 1"])
   3.237 -    apply (cases a rule: float_of_cases)
   3.238 +    apply transfer
   3.239      apply simp
   3.240      done
   3.241    assume "a < b"
   3.242    then show "\<exists>c. a < c \<and> c < b"
   3.243 -    apply (intro exI[of _ "(b + a) * float_of (1/2)"])
   3.244 -    apply (cases a b rule: float_of_cases2)
   3.245 -    apply simp
   3.246 +    apply (intro exI[of _ "(a + b) * Float 1 -1"])
   3.247 +    apply transfer
   3.248 +    apply (simp add: powr_neg_numeral) 
   3.249      done
   3.250  qed
   3.251  
   3.252 -instantiation float :: linordered_idom
   3.253 +instantiation float :: lattice_ab_group_add
   3.254  begin
   3.255  
   3.256 -definition "sgn x = float_of (sgn (real x))"
   3.257 +definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
   3.258 +where "inf_float a b = min a b"
   3.259  
   3.260 -lemma sgn_float[simp]: "x \<in> float \<Longrightarrow> sgn (float_of x) = float_of (sgn x)"
   3.261 -  by (simp add: sgn_float_def)
   3.262 +definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
   3.263 +where "sup_float a b = max a b"
   3.264  
   3.265  instance
   3.266 -proof
   3.267 -  fix a b c :: float
   3.268 -  show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
   3.269 -    by (cases a rule: float_of_cases) simp
   3.270 -  show "a * b = b * a"
   3.271 -    by (cases a b rule: float_of_cases2) (simp add: field_simps)
   3.272 -  show "1 * a = a" "(a + b) * c = a * c + b * c"
   3.273 -    by (simp_all add: field_simps del: one_float_def)
   3.274 -  assume "a < b" "0 < c" then show "c * a < c * b"
   3.275 -    by (cases a b c rule: float_of_cases3) (simp add: field_simps)
   3.276 -qed
   3.277 +  by default
   3.278 +     (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
   3.279  end
   3.280  
   3.281 -definition Float :: "int \<Rightarrow> int \<Rightarrow> float" where
   3.282 -  [simp, code del]: "Float m e = float_of (m * 2 powr e)"
   3.283 -
   3.284 -lemma real_of_float_Float[code]: "real_of_float (Float m e) =
   3.285 -  (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
   3.286 -by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
   3.287 -
   3.288 -code_datatype Float
   3.289 -
   3.290 -lemma real_Float: "real (Float m e) = m * 2 powr e" by simp
   3.291 -
   3.292 -definition normfloat :: "float \<Rightarrow> float" where
   3.293 -  [simp]: "normfloat x = x"
   3.294 +lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
   3.295 +  apply (induct x)
   3.296 +  apply simp
   3.297 +  apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
   3.298 +                  real_of_float_plus real_of_float_one plus_float numeral_float one_float)
   3.299 +  done
   3.300  
   3.301 -lemma compute_normfloat[code]: "normfloat (Float m e) =
   3.302 -  (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
   3.303 -                           else if m = 0 then 0 else Float m e)"
   3.304 -  by (simp del: real_of_int_add split: prod.split)
   3.305 -     (auto simp add: powr_add zmod_eq_0_iff)
   3.306 -
   3.307 -lemma compute_zero[code_unfold, code]: "0 = Float 0 0"
   3.308 -  by simp
   3.309 +lemma transfer_numeral [transfer_rule]: 
   3.310 +  "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   3.311 +  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
   3.312  
   3.313 -lemma compute_one[code_unfold, code]: "1 = Float 1 0"
   3.314 -  by simp
   3.315 -
   3.316 -instance float :: numeral ..
   3.317 -
   3.318 -lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)"
   3.319 -  by (induct k)
   3.320 -     (simp_all only: numeral.simps one_float_def float_plus_float numeral_float one_float plus_float)
   3.321 -
   3.322 -lemma float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
   3.323 +lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   3.324    by (simp add: minus_numeral[symmetric] del: minus_numeral)
   3.325  
   3.326 +lemma transfer_neg_numeral [transfer_rule]: 
   3.327 +  "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
   3.328 +  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
   3.329 +
   3.330  lemma
   3.331 -  shows float_numeral[simp]: "real (numeral x :: float) = numeral x"
   3.332 -    and float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   3.333 -  by simp_all
   3.334 +  shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
   3.335 +    and float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
   3.336 +  unfolding real_of_float_eq by simp_all
   3.337  
   3.338  subsection {* Represent floats as unique mantissa and exponent *}
   3.339  
   3.340 -
   3.341  lemma int_induct_abs[case_names less]:
   3.342    fixes j :: int
   3.343    assumes H: "\<And>n. (\<And>i. \<bar>i\<bar> < \<bar>n\<bar> \<Longrightarrow> P i) \<Longrightarrow> P n"
   3.344 @@ -415,7 +304,7 @@
   3.345     | (powr) m e :: int where "real f = m * 2 powr e" "\<not> 2 dvd m" "f \<noteq> 0"
   3.346  proof (atomize_elim, induct f)
   3.347    case (float_of y) then show ?case
   3.348 -    by (cases rule: floatE_normed) auto
   3.349 +    by (cases rule: floatE_normed) (auto simp: zero_float_def)
   3.350  qed
   3.351  
   3.352  definition mantissa :: "float \<Rightarrow> int" where
   3.353 @@ -432,7 +321,7 @@
   3.354  proof -
   3.355    have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)" by auto
   3.356    then show ?E ?M
   3.357 -    by (auto simp add: mantissa_def exponent_def)
   3.358 +    by (auto simp add: mantissa_def exponent_def zero_float_def)
   3.359  qed
   3.360  
   3.361  lemma
   3.362 @@ -448,23 +337,14 @@
   3.363        by auto
   3.364      then show ?thesis
   3.365        unfolding exponent_def mantissa_def
   3.366 -      by (rule someI2_ex) simp
   3.367 -  qed simp
   3.368 +      by (rule someI2_ex) (simp add: zero_float_def)
   3.369 +  qed (simp add: zero_float_def)
   3.370    then show ?E ?D by auto
   3.371  qed simp
   3.372  
   3.373  lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
   3.374    using mantissa_not_dvd[of f] by auto
   3.375  
   3.376 -lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   3.377 -  unfolding real_of_float_eq[symmetric] mantissa_exponent[of f] by simp
   3.378 -
   3.379 -lemma Float_cases[case_names Float, cases type: float]:
   3.380 -  fixes f :: float
   3.381 -  obtains (Float) m e :: int where "f = Float m e"
   3.382 -  using Float_mantissa_exponent[symmetric]
   3.383 -  by (atomize_elim) auto
   3.384 -
   3.385  lemma 
   3.386    fixes m e :: int
   3.387    defines "f \<equiv> float_of (m * 2 powr e)"
   3.388 @@ -484,6 +364,24 @@
   3.389      by (auto simp: mult_powr_eq_mult_powr_iff)
   3.390  qed
   3.391  
   3.392 +subsection {* Compute arithmetic operations *}
   3.393 +
   3.394 +lemma real_Float[simp]: "real (Float m e) = m * 2 powr e"
   3.395 +  using Float.rep_eq by (simp add: real_of_float_def)
   3.396 +
   3.397 +lemma real_of_float_Float[code]: "real_of_float (Float m e) =
   3.398 +  (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
   3.399 +by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric] Float_def)
   3.400 +
   3.401 +lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   3.402 +  unfolding real_of_float_eq mantissa_exponent[of f] by simp
   3.403 +
   3.404 +lemma Float_cases[case_names Float, cases type: float]:
   3.405 +  fixes f :: float
   3.406 +  obtains (Float) m e :: int where "f = Float m e"
   3.407 +  using Float_mantissa_exponent[symmetric]
   3.408 +  by (atomize_elim) auto
   3.409 +
   3.410  lemma denormalize_shift:
   3.411    assumes f_def: "f \<equiv> Float m e" and not_0: "f \<noteq> float_of 0"
   3.412    obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
   3.413 @@ -520,64 +418,70 @@
   3.414      unfolding real_of_int_inject by auto
   3.415  qed
   3.416  
   3.417 -subsection {* Compute arithmetic operations *}
   3.418 +lemma compute_zero[code_unfold, code]: "0 = Float 0 0"
   3.419 +  by transfer simp
   3.420 +
   3.421 +lemma compute_one[code_unfold, code]: "1 = Float 1 0"
   3.422 +  by transfer simp
   3.423 +
   3.424 +definition normfloat :: "float \<Rightarrow> float" where
   3.425 +  [simp]: "normfloat x = x"
   3.426 +
   3.427 +lemma compute_normfloat[code]: "normfloat (Float m e) =
   3.428 +  (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
   3.429 +                           else if m = 0 then 0 else Float m e)"
   3.430 +  unfolding normfloat_def
   3.431 +  by transfer (auto simp add: powr_add zmod_eq_0_iff)
   3.432  
   3.433  lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
   3.434 -  by simp
   3.435 +  by transfer simp
   3.436  
   3.437  lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
   3.438 -  by simp
   3.439 +  by transfer simp
   3.440  
   3.441  lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
   3.442 -  by simp
   3.443 +  by transfer simp
   3.444  
   3.445  lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
   3.446 -  by (simp add: field_simps powr_add)
   3.447 +  by transfer (simp add: field_simps powr_add)
   3.448  
   3.449  lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
   3.450    (if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
   3.451                else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
   3.452 -  by (simp add: field_simps)
   3.453 -     (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
   3.454 +  by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
   3.455  
   3.456 -lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)" by simp
   3.457 +lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
   3.458 +  by simp
   3.459  
   3.460  lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
   3.461 -  by (simp add: sgn_times)
   3.462 +  by transfer (simp add: sgn_times)
   3.463  
   3.464 -definition is_float_pos :: "float \<Rightarrow> bool" where
   3.465 -  "is_float_pos f \<longleftrightarrow> 0 < f"
   3.466 +lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
   3.467  
   3.468  lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
   3.469 -  by (auto simp add: is_float_pos_def zero_less_mult_iff) (simp add: not_le[symmetric])
   3.470 +  by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
   3.471  
   3.472  lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
   3.473 -  by (simp add: is_float_pos_def field_simps del: zero_float_def)
   3.474 +  by transfer (simp add: field_simps)
   3.475  
   3.476 -definition is_float_nonneg :: "float \<Rightarrow> bool" where
   3.477 -  "is_float_nonneg f \<longleftrightarrow> 0 \<le> f"
   3.478 +lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
   3.479  
   3.480  lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
   3.481 -  by (auto simp add: is_float_nonneg_def zero_le_mult_iff) (simp add: not_less[symmetric])
   3.482 +  by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
   3.483  
   3.484  lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
   3.485 -  by (simp add: is_float_nonneg_def field_simps del: zero_float_def)
   3.486 +  by transfer (simp add: field_simps)
   3.487  
   3.488 -definition is_float_zero :: "float \<Rightarrow> bool" where
   3.489 -  "is_float_zero f \<longleftrightarrow> 0 = f"
   3.490 +lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" by simp
   3.491  
   3.492  lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
   3.493 -  by (auto simp add: is_float_zero_def)
   3.494 -
   3.495 -lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e" by (simp add: abs_mult)
   3.496 +  by transfer (auto simp add: is_float_zero_def)
   3.497  
   3.498 -instantiation float :: equal
   3.499 -begin
   3.500 +lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
   3.501 +  by transfer (simp add: abs_mult)
   3.502  
   3.503 -definition "equal_float (f1 :: float) f2 \<longleftrightarrow> is_float_zero (f1 - f2)"
   3.504 -
   3.505 -instance proof qed (auto simp: equal_float_def is_float_zero_def simp del: zero_float_def)
   3.506 -end
   3.507 +lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
   3.508 +  by transfer simp
   3.509  
   3.510  subsection {* Rounding Real numbers *}
   3.511  
   3.512 @@ -632,12 +536,10 @@
   3.513  
   3.514  subsection {* Rounding Floats *}
   3.515  
   3.516 -definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" where
   3.517 -  "float_up prec x = float_of (round_up prec (real x))"
   3.518 +lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
   3.519  
   3.520 -lemma float_up_float: 
   3.521 -  "x \<in> float \<Longrightarrow> float_up prec (float_of x) = float_of (round_up prec x)"
   3.522 -  unfolding float_up_def by simp
   3.523 +lemma real_of_float_float_up[simp]: "real (float_up e f) = round_up e (real f)"
   3.524 +  using float_up.rep_eq by (simp add: real_of_float_def)
   3.525  
   3.526  lemma float_up_correct:
   3.527    shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
   3.528 @@ -646,15 +548,13 @@
   3.529    have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
   3.530    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
   3.531    finally show "real (float_up e f) - real f \<le> 2 powr real (- e)"
   3.532 -    by (simp add: float_up_def)
   3.533 -qed (simp add: algebra_simps float_up_def round_up)
   3.534 +    by simp
   3.535 +qed (simp add: algebra_simps round_up)
   3.536  
   3.537 -definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" where
   3.538 -  "float_down prec x = float_of (round_down prec (real x))"
   3.539 +lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
   3.540  
   3.541 -lemma float_down_float: 
   3.542 -  "x \<in> float \<Longrightarrow> float_down prec (float_of x) = float_of (round_down prec x)"
   3.543 -  unfolding float_down_def by simp
   3.544 +lemma real_of_float_float_down[simp]: "real (float_down e f) = round_down e (real f)"
   3.545 +  using float_down.rep_eq by (simp add: real_of_float_def)
   3.546  
   3.547  lemma float_down_correct:
   3.548    shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
   3.549 @@ -663,21 +563,8 @@
   3.550    have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
   3.551    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
   3.552    finally show "real f - real (float_down e f) \<le> 2 powr real (- e)"
   3.553 -    by (simp add: float_down_def)
   3.554 -qed (simp add: algebra_simps float_down_def round_down)
   3.555 -
   3.556 -lemma round_down_Float_id:
   3.557 -  assumes "p + e \<ge> 0"
   3.558 -  shows "round_down p (Float m e) = Float m e"
   3.559 -proof -
   3.560 -  from assms have r: "real e + real p = real (nat (e + p))" by simp
   3.561 -  have r: "\<lfloor>real (Float m e) * 2 powr real p\<rfloor> = real (Float m e) * 2 powr real p"
   3.562 -    by (auto intro: exI[where x="m*2^nat (e+p)"]
   3.563 -      simp add: ac_simps powr_add[symmetric] r powr_realpow)
   3.564 -  show ?thesis using assms
   3.565 -    unfolding round_down_def floor_divide_eq_div r
   3.566 -    by (simp add: ac_simps powr_add[symmetric])
   3.567 -qed
   3.568 +    by simp
   3.569 +qed (simp add: algebra_simps round_down)
   3.570  
   3.571  lemma compute_float_down[code]:
   3.572    "float_down p (Float m e) =
   3.573 @@ -687,12 +574,19 @@
   3.574    hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
   3.575      using powr_realpow[of 2 "nat (-(p + e))"] by simp
   3.576    also have "... = 1 / 2 powr p / 2 powr e"
   3.577 -  unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
   3.578 +    unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
   3.579    finally show ?thesis
   3.580 -    unfolding float_down_def round_down_def floor_divide_eq_div[symmetric]
   3.581 -    using `p + e < 0` by (simp add: ac_simps)
   3.582 +    using `p + e < 0`
   3.583 +    by transfer (simp add: ac_simps round_down_def floor_divide_eq_div[symmetric])
   3.584  next
   3.585 -  assume "\<not> p + e < 0" with round_down_Float_id show ?thesis by (simp add: float_down_def)
   3.586 +  assume "\<not> p + e < 0"
   3.587 +  then have r: "real e + real p = real (nat (e + p))" by simp
   3.588 +  have r: "\<lfloor>(m * 2 powr e) * 2 powr real p\<rfloor> = (m * 2 powr e) * 2 powr real p"
   3.589 +    by (auto intro: exI[where x="m*2^nat (e+p)"]
   3.590 +             simp add: ac_simps powr_add[symmetric] r powr_realpow)
   3.591 +  with `\<not> p + e < 0` show ?thesis
   3.592 +    by transfer
   3.593 +       (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
   3.594  qed
   3.595  
   3.596  lemma ceil_divide_floor_conv:
   3.597 @@ -714,19 +608,6 @@
   3.598  qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
   3.599    floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
   3.600  
   3.601 -lemma round_up_Float_id:
   3.602 -  assumes "p + e \<ge> 0"
   3.603 -  shows "round_up p (Float m e) = Float m e"
   3.604 -proof -
   3.605 -  from assms have r1: "real e + real p = real (nat (e + p))" by simp
   3.606 -  have r: "\<lceil>real (Float m e) * 2 powr real p\<rceil> = real (Float m e) * 2 powr real p"
   3.607 -    by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
   3.608 -      intro: exI[where x="m*2^nat (e+p)"])
   3.609 -  show ?thesis using assms
   3.610 -    unfolding float_up_def round_up_def floor_divide_eq_div Let_def r
   3.611 -    by (simp add: ac_simps powr_add[symmetric])
   3.612 -qed
   3.613 -
   3.614  lemma compute_float_up[code]:
   3.615    "float_up p (Float m e) =
   3.616      (let P = 2^nat (-(p + e)); r = m mod P in
   3.617 @@ -745,8 +626,8 @@
   3.618    show ?thesis
   3.619    proof cases
   3.620      assume "2^nat (-(p + e)) dvd m"
   3.621 -    with `p + e < 0` twopow_rewrite show ?thesis
   3.622 -      by (auto simp: ac_simps float_up_def round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
   3.623 +    with `p + e < 0` twopow_rewrite show ?thesis unfolding Let_def
   3.624 +      by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
   3.625    next
   3.626      assume ndvd: "\<not> 2 ^ nat (- (p + e)) dvd m"
   3.627      have one_div: "real m * (1 / real ((2::int) ^ nat (- (p + e)))) =
   3.628 @@ -757,10 +638,19 @@
   3.629        using ndvd unfolding powr_rewrite one_div
   3.630        by (subst ceil_divide_floor_conv) (auto simp: field_simps)
   3.631      thus ?thesis using `p + e < 0` twopow_rewrite
   3.632 -      by (auto simp: ac_simps Let_def float_up_def round_up_def floor_divide_eq_div[symmetric])
   3.633 +      unfolding Let_def
   3.634 +      by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div[symmetric])
   3.635    qed
   3.636  next
   3.637 -  assume "\<not> p + e < 0" with round_up_Float_id show ?thesis by (simp add: float_up_def)
   3.638 +  assume "\<not> p + e < 0"
   3.639 +  then have r1: "real e + real p = real (nat (e + p))" by simp
   3.640 +  have r: "\<lceil>(m * 2 powr e) * 2 powr real p\<rceil> = (m * 2 powr e) * 2 powr real p"
   3.641 +    by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
   3.642 +      intro: exI[where x="m*2^nat (e+p)"])
   3.643 +  then show ?thesis using `\<not> p + e < 0`
   3.644 +    unfolding Let_def
   3.645 +    by transfer
   3.646 +       (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
   3.647  qed
   3.648  
   3.649  lemmas real_of_ints =
   3.650 @@ -790,8 +680,8 @@
   3.651  
   3.652  subsection {* Compute bitlen of integers *}
   3.653  
   3.654 -definition bitlen::"int => int"
   3.655 -where "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   3.656 +definition bitlen :: "int \<Rightarrow> int" where
   3.657 +  "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   3.658  
   3.659  lemma bitlen_nonneg: "0 \<le> bitlen x"
   3.660  proof -
   3.661 @@ -842,12 +732,15 @@
   3.662  defines "f \<equiv> Float m e"
   3.663  shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
   3.664  proof cases
   3.665 -  assume "m \<noteq> 0" hence "f \<noteq> float_of 0" by (simp add: f_def) hence "mantissa f \<noteq> 0"
   3.666 +  assume "m \<noteq> 0"
   3.667 +  hence "f \<noteq> float_of 0"
   3.668 +    unfolding real_of_float_eq by (simp add: f_def)
   3.669 +  hence "mantissa f \<noteq> 0"
   3.670      by (simp add: mantissa_noteq_0)
   3.671    moreover
   3.672    from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
   3.673    ultimately show ?thesis by (simp add: abs_mult)
   3.674 -qed (simp add: f_def bitlen_def)
   3.675 +qed (simp add: f_def bitlen_def Float_def)
   3.676  
   3.677  lemma compute_bitlen[code]:
   3.678    shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
   3.679 @@ -899,7 +792,7 @@
   3.680  proof -
   3.681    have "0 < Float m e" using assms by auto
   3.682    hence "0 < m" using powr_gt_zero[of 2 e]
   3.683 -    by (auto simp: less_float_def less_eq_float_def zero_less_mult_iff)
   3.684 +    by (auto simp: zero_less_mult_iff)
   3.685    hence "m \<noteq> 0" by auto
   3.686    show ?thesis
   3.687    proof (cases "0 \<le> e")
   3.688 @@ -955,8 +848,8 @@
   3.689  
   3.690  definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
   3.691  
   3.692 -definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where
   3.693 -  "lapprox_posrat prec x y = float_of (round_down (rat_precision prec x y) (x / y))"
   3.694 +lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
   3.695 +  is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
   3.696  
   3.697  lemma compute_lapprox_posrat[code]:
   3.698    fixes prec x y 
   3.699 @@ -965,13 +858,13 @@
   3.700         l = rat_precision prec x y;
   3.701         d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
   3.702      in normfloat (Float d (- l)))"
   3.703 -    unfolding lapprox_posrat_def div_mult_twopow_eq
   3.704 -    by (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide
   3.705 -                  field_simps Let_def
   3.706 +    unfolding div_mult_twopow_eq Let_def normfloat_def
   3.707 +    by transfer
   3.708 +       (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps
   3.709               del: two_powr_minus_int_float)
   3.710  
   3.711 -definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where
   3.712 -  "rapprox_posrat prec x y = float_of (round_up (rat_precision prec x y) (x / y))"
   3.713 +lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
   3.714 +  is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
   3.715  
   3.716  (* TODO: optimize using zmod_zmult2_eq, pdivmod ? *)
   3.717  lemma compute_rapprox_posrat[code]:
   3.718 @@ -984,7 +877,7 @@
   3.719       m = fst X mod snd X
   3.720     in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
   3.721  proof (cases "y = 0")
   3.722 -  assume "y = 0" thus ?thesis by (simp add: rapprox_posrat_def Let_def)
   3.723 +  assume "y = 0" thus ?thesis unfolding Let_def normfloat_def by transfer simp
   3.724  next
   3.725    assume "y \<noteq> 0"
   3.726    show ?thesis
   3.727 @@ -995,10 +888,11 @@
   3.728      moreover have "real x * 2 powr real l = real x'"
   3.729        by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
   3.730      ultimately show ?thesis
   3.731 -      unfolding rapprox_posrat_def round_up_def l_def[symmetric]
   3.732 +      unfolding Let_def normfloat_def
   3.733        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
   3.734 -      by (simp add: Let_def floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals
   3.735 -               del: real_of_ints)
   3.736 +        l_def[symmetric, THEN meta_eq_to_obj_eq]
   3.737 +      by transfer
   3.738 +         (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
   3.739     next
   3.740      assume "\<not> 0 \<le> l"
   3.741      def y' == "y * 2 ^ nat (- l)"
   3.742 @@ -1008,14 +902,14 @@
   3.743        using `\<not> 0 \<le> l`
   3.744        by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
   3.745      ultimately show ?thesis
   3.746 +      unfolding Let_def normfloat_def
   3.747        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
   3.748 -      by (simp add: rapprox_posrat_def l_def round_up_def ceil_divide_floor_conv
   3.749 -                    floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals
   3.750 -               del: real_of_ints)
   3.751 +        l_def[symmetric, THEN meta_eq_to_obj_eq]
   3.752 +      by transfer
   3.753 +         (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
   3.754    qed
   3.755  qed
   3.756  
   3.757 -
   3.758  lemma rat_precision_pos:
   3.759    assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   3.760    shows "rat_precision n (int x) (int y) > 0"
   3.761 @@ -1052,16 +946,20 @@
   3.762    also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
   3.763      unfolding int_of_reals real_of_int_le_iff
   3.764      using rat_precision_pos[OF assms] by (rule power_aux)
   3.765 -  finally show ?thesis unfolding rapprox_posrat_def
   3.766 +  finally show ?thesis
   3.767 +    unfolding rapprox_posrat_def
   3.768      apply (simp add: round_up_def)
   3.769 -    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide)
   3.770 +    apply (simp add: field_simps powr_minus inverse_eq_divide)
   3.771      unfolding powr1
   3.772      unfolding int_of_reals real_of_int_less_iff
   3.773 -    unfolding ceiling_less_eq using rat_precision_pos[of x y n] assms apply simp done
   3.774 +    unfolding ceiling_less_eq
   3.775 +    using rat_precision_pos[of x y n] assms
   3.776 +    apply simp
   3.777 +    done
   3.778  qed
   3.779  
   3.780 -definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where
   3.781 -  "lapprox_rat prec x y = float_of (round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))"
   3.782 +lift_definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   3.783 +  "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
   3.784  
   3.785  lemma compute_lapprox_rat[code]:
   3.786    "lapprox_rat prec x y =
   3.787 @@ -1072,15 +970,15 @@
   3.788        else (if 0 < y
   3.789          then - (rapprox_posrat prec (nat (-x)) (nat y))
   3.790          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   3.791 +  apply transfer
   3.792    apply (cases "y = 0")
   3.793 -  apply (simp add: lapprox_posrat_def rapprox_posrat_def round_down_def lapprox_rat_def)
   3.794 -  apply (auto simp: lapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def
   3.795 -        ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints)
   3.796 +  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   3.797 +                    int_of_reals simp del: real_of_ints)
   3.798    apply (auto simp: ac_simps)
   3.799    done
   3.800  
   3.801 -definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where
   3.802 -  "rapprox_rat prec x y = float_of (round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))"
   3.803 +lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   3.804 +  "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
   3.805  
   3.806  lemma compute_rapprox_rat[code]:
   3.807    "rapprox_rat prec x y =
   3.808 @@ -1091,94 +989,67 @@
   3.809        else (if 0 < y
   3.810          then - (lapprox_posrat prec (nat (-x)) (nat y))
   3.811          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   3.812 -  apply (cases "y = 0", simp add: lapprox_posrat_def rapprox_posrat_def round_up_def rapprox_rat_def)
   3.813 -  apply (auto simp: rapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def
   3.814 -        ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints)
   3.815 +  apply transfer
   3.816 +  apply (cases "y = 0")
   3.817 +  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   3.818 +                    int_of_reals simp del: real_of_ints)
   3.819    apply (auto simp: ac_simps)
   3.820    done
   3.821  
   3.822  subsection {* Division *}
   3.823  
   3.824 -definition div_precision
   3.825 -where "div_precision prec x y =
   3.826 -  rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y"
   3.827 -
   3.828 -definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
   3.829 -where "float_divl prec a b =
   3.830 -  float_of (round_down (div_precision prec a b) (a / b))"
   3.831 +lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
   3.832 +  "\<lambda>(prec::nat) a b. round_down (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
   3.833  
   3.834  lemma compute_float_divl[code]:
   3.835 -  fixes m1 s1 m2 s2
   3.836 -  defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2"
   3.837 -  shows "float_divl prec f1 f2 = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   3.838 +  "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   3.839  proof cases
   3.840 -  assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0"
   3.841 -  then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto
   3.842 -  with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2]
   3.843 -  have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0"
   3.844 -    by (auto simp add: dvd_def)  
   3.845 -  then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>"
   3.846 -    by simp_all
   3.847 -  moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this
   3.848 -  moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this
   3.849 -  moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j))
   3.850 -    = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)"
   3.851 -    by (simp add: powr_divide2[symmetric] powr_realpow)
   3.852 -  moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)"
   3.853 -    unfolding mantissa_exponent by (simp add: powr_divide2[symmetric])
   3.854 -  moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) =
   3.855 -    rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i"
   3.856 -    using pos by (simp add: rat_precision_def)
   3.857 -  ultimately show ?thesis
   3.858 -    unfolding float_divl_def lapprox_rat_def div_precision_def
   3.859 -    by (simp add: abs_mult round_down_shift powr_divide2[symmetric]
   3.860 -                del: int_nat_eq real_of_int_diff times_divide_eq_left )
   3.861 -       (simp add: field_simps powr_divide2[symmetric] powr_add)
   3.862 -next
   3.863 -  assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis
   3.864 -    by (auto simp add: float_divl_def f1_def f2_def lapprox_rat_def)
   3.865 -qed  
   3.866 +  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   3.867 +  then show ?thesis
   3.868 +  proof transfer
   3.869 +    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   3.870 +    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   3.871 +    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   3.872  
   3.873 -definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
   3.874 -where "float_divr prec a b =
   3.875 -  float_of (round_up (div_precision prec a b) (a / b))"
   3.876 +    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   3.877 +      by (simp add: field_simps powr_divide2[symmetric])
   3.878 +    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   3.879 +        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   3.880 +      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   3.881 +    
   3.882 +    show "round_down (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   3.883 +      round_down (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   3.884 +      using not_0 unfolding eq1 eq2 round_down_shift by (simp add: field_simps)
   3.885 +  qed
   3.886 +qed (transfer, auto)
   3.887 +
   3.888 +lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
   3.889 +  "\<lambda>(prec::nat) a b. round_up (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
   3.890  
   3.891  lemma compute_float_divr[code]:
   3.892 -  fixes m1 s1 m2 s2
   3.893 -  defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2"
   3.894 -  shows "float_divr prec f1 f2 = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   3.895 +  "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   3.896  proof cases
   3.897 -  assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0"
   3.898 -  then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto
   3.899 -  with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2]
   3.900 -  have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0"
   3.901 -    by (auto simp add: dvd_def)  
   3.902 -  then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>"
   3.903 -    by simp_all
   3.904 -  moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this
   3.905 -  moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this
   3.906 -  moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j))
   3.907 -    = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)"
   3.908 -    by (simp add: powr_divide2[symmetric] powr_realpow)
   3.909 -  moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)"
   3.910 -    unfolding mantissa_exponent by (simp add: powr_divide2[symmetric])
   3.911 -  moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) =
   3.912 -    rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i"
   3.913 -    using pos by (simp add: rat_precision_def)
   3.914 -  ultimately show ?thesis
   3.915 -    unfolding float_divr_def rapprox_rat_def div_precision_def
   3.916 -    by (simp add: abs_mult round_up_shift powr_divide2[symmetric]
   3.917 -                del: int_nat_eq real_of_int_diff times_divide_eq_left)
   3.918 -       (simp add: field_simps powr_divide2[symmetric] powr_add)
   3.919 -next
   3.920 -  assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis
   3.921 -    by (auto simp add: float_divr_def f1_def f2_def rapprox_rat_def)
   3.922 -qed
   3.923 +  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   3.924 +  then show ?thesis
   3.925 +  proof transfer
   3.926 +    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   3.927 +    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   3.928 +    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   3.929 +
   3.930 +    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   3.931 +      by (simp add: field_simps powr_divide2[symmetric])
   3.932 +    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   3.933 +        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   3.934 +      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   3.935 +    
   3.936 +    show "round_up (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   3.937 +      round_up (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   3.938 +      using not_0 unfolding eq1 eq2 round_up_shift by (simp add: field_simps)
   3.939 +  qed
   3.940 +qed (transfer, auto)
   3.941  
   3.942  subsection {* Lemmas needed by Approximate *}
   3.943  
   3.944 -declare one_float_def[simp del] zero_float_def[simp del]
   3.945 -
   3.946  lemma Float_num[simp]: shows
   3.947     "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
   3.948     "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
   3.949 @@ -1255,14 +1126,11 @@
   3.950    by (auto simp: field_simps mult_le_0_iff)
   3.951  
   3.952  lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
   3.953 -  using round_down by (simp add: float_divl_def)
   3.954 +  by transfer (simp add: round_down)
   3.955  
   3.956  lemma float_divl_lower_bound:
   3.957 -  fixes x y prec
   3.958 -  defines "p == rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y"
   3.959 -  assumes xy: "0 \<le> x" "0 < y" shows "0 \<le> real (float_divl prec x y)"
   3.960 -  using xy unfolding float_divl_def p_def[symmetric] round_down_def
   3.961 -  by (simp add: zero_le_mult_iff zero_le_divide_iff less_eq_float_def less_float_def)
   3.962 +  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
   3.963 +  by transfer (simp add: round_down_def zero_le_mult_iff zero_le_divide_iff)
   3.964  
   3.965  lemma exponent_1: "exponent 1 = 0"
   3.966    using exponent_float[of 1 0] by (simp add: one_float_def)
   3.967 @@ -1292,138 +1160,106 @@
   3.968  qed
   3.969  
   3.970  lemma float_divl_pos_less1_bound:
   3.971 -  assumes "0 < real x" and "real x < 1" and "prec \<ge> 1"
   3.972 -  shows "1 \<le> real (float_divl prec 1 x)"
   3.973 -proof cases
   3.974 -  assume nonneg: "div_precision prec 1 x \<ge> 0"
   3.975 -  hence "2 powr real (div_precision prec 1 x) =
   3.976 -    floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1::real)"
   3.977 -    by (simp add: powr_int del: real_of_int_power) simp
   3.978 -  also have "floor (1::real) \<le> floor (1 / x)" using assms by simp
   3.979 -  also have "floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1 / x) \<le>
   3.980 -    floor (real ((2::int) ^ nat (div_precision prec 1 x)) * (1 / x))"
   3.981 -    by (rule le_mult_floor) (auto simp: assms less_imp_le)
   3.982 -  finally have "2 powr real (div_precision prec 1 x) <=
   3.983 -    floor (2 powr nat (div_precision prec 1 x) / x)" by (simp add: powr_realpow)
   3.984 -  thus ?thesis
   3.985 -    using assms nonneg
   3.986 -    unfolding float_divl_def round_down_def
   3.987 -    by simp (simp add: powr_minus inverse_eq_divide)
   3.988 -next
   3.989 -  assume neg: "\<not> 0 \<le> div_precision prec 1 x"
   3.990 -  have "1 \<le> 1 * 2 powr (prec - 1)" using assms by (simp add: powr_realpow)
   3.991 -  also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1)"
   3.992 -    apply (rule mult_mono) using assms float_upper_bound
   3.993 -    by (auto intro!: divide_nonneg_pos)
   3.994 -  also have "2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1) =
   3.995 -    2 powr real (div_precision prec 1 x) / real x"
   3.996 -    using assms
   3.997 -    apply (simp add: div_precision_def rat_precision_def diff_diff_eq2
   3.998 -    mantissa_1 exponent_1 bitlen_1 powr_add powr_minus real_of_nat_diff)
   3.999 -    apply (simp only: diff_def powr_add)
  3.1000 -    apply simp
  3.1001 -    done
  3.1002 -  finally have "1 \<le> \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>"
  3.1003 -    using floor_mono[of "1::real"] by simp thm mult_mono
  3.1004 -  hence "1 \<le> real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>"
  3.1005 -    by (metis floor_real_of_int one_le_floor)
  3.1006 -  hence "1 * 1 \<le>
  3.1007 -    real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor> * 2 powr - real (div_precision prec 1 x)"
  3.1008 -  apply (rule mult_mono)
  3.1009 -    using assms neg
  3.1010 -    by (auto intro: divide_nonneg_pos mult_nonneg_nonneg simp: real_of_int_minus[symmetric] powr_int simp del: real_of_int_minus) find_theorems "real (- _)"
  3.1011 -  thus ?thesis
  3.1012 -    using assms neg
  3.1013 -    unfolding float_divl_def round_down_def
  3.1014 -    by simp
  3.1015 +  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
  3.1016 +proof transfer
  3.1017 +  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
  3.1018 +  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>" 
  3.1019 +  show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
  3.1020 +  proof cases
  3.1021 +    assume nonneg: "0 \<le> p"
  3.1022 +    hence "2 powr real (p) = floor (real ((2::int) ^ nat p)) * floor (1::real)"
  3.1023 +      by (simp add: powr_int del: real_of_int_power) simp
  3.1024 +    also have "floor (1::real) \<le> floor (1 / x)" using x prec by simp
  3.1025 +    also have "floor (real ((2::int) ^ nat p)) * floor (1 / x) \<le>
  3.1026 +      floor (real ((2::int) ^ nat p) * (1 / x))"
  3.1027 +      by (rule le_mult_floor) (auto simp: x prec less_imp_le)
  3.1028 +    finally have "2 powr real p \<le> floor (2 powr nat p / x)" by (simp add: powr_realpow)
  3.1029 +    thus ?thesis unfolding p_def[symmetric]
  3.1030 +      using x prec nonneg by (simp add: powr_minus inverse_eq_divide round_down_def)
  3.1031 +  next
  3.1032 +    assume neg: "\<not> 0 \<le> p"
  3.1033 +
  3.1034 +    have "x = 2 powr (log 2 x)"
  3.1035 +      using x by simp
  3.1036 +    also have "2 powr (log 2 x) \<le> 2 powr p"
  3.1037 +    proof (rule powr_mono)
  3.1038 +      have "log 2 x \<le> \<lceil>log 2 x\<rceil>"
  3.1039 +        by simp
  3.1040 +      also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + 1"
  3.1041 +        using ceiling_diff_floor_le_1[of "log 2 x"] by simp
  3.1042 +      also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + prec"
  3.1043 +        using prec by simp
  3.1044 +      finally show "log 2 x \<le> real p"
  3.1045 +        using x by (simp add: p_def)
  3.1046 +    qed simp
  3.1047 +    finally have x_le: "x \<le> 2 powr p" .
  3.1048 +
  3.1049 +    from neg have "2 powr real p \<le> 2 powr 0"
  3.1050 +      by (intro powr_mono) auto
  3.1051 +    also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
  3.1052 +    also have "\<dots> \<le> \<lfloor>2 powr real p / x\<rfloor>" unfolding real_of_int_le_iff
  3.1053 +      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq mult_pos_pos)
  3.1054 +    finally show ?thesis
  3.1055 +      using prec x unfolding p_def[symmetric]
  3.1056 +      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq mult_pos_pos)
  3.1057 +  qed
  3.1058  qed
  3.1059  
  3.1060  lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
  3.1061 -  using round_up by (simp add: float_divr_def)
  3.1062 +  using round_up by transfer simp
  3.1063  
  3.1064  lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
  3.1065  proof -
  3.1066 -  have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
  3.1067 +  have "1 \<le> 1 / real x" using `0 < x` and `x < 1` by auto
  3.1068    also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
  3.1069 -  finally show ?thesis unfolding less_eq_float_def by auto
  3.1070 +  finally show ?thesis by auto
  3.1071  qed
  3.1072  
  3.1073  lemma float_divr_nonpos_pos_upper_bound:
  3.1074 -  assumes "real x \<le> 0" and "0 < real y"
  3.1075 -  shows "real (float_divr prec x y) \<le> 0"
  3.1076 -using assms
  3.1077 -unfolding float_divr_def round_up_def
  3.1078 -by (auto simp: field_simps mult_le_0_iff divide_le_0_iff)
  3.1079 +  "real x \<le> 0 \<Longrightarrow> 0 < real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
  3.1080 +  by transfer (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def)
  3.1081  
  3.1082  lemma float_divr_nonneg_neg_upper_bound:
  3.1083 -  assumes "0 \<le> real x" and "real y < 0"
  3.1084 -  shows "real (float_divr prec x y) \<le> 0"
  3.1085 -using assms
  3.1086 -unfolding float_divr_def round_up_def
  3.1087 -by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff)
  3.1088 +  "0 \<le> real x \<Longrightarrow> real y < 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
  3.1089 +  by transfer (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def)
  3.1090 +
  3.1091 +lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is
  3.1092 +  "\<lambda>(prec::nat) x. round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
  3.1093 +
  3.1094 +lemma float_round_up: "real x \<le> real (float_round_up prec x)"
  3.1095 +  using round_up by transfer simp
  3.1096  
  3.1097 -definition "round_prec p f = int p - (bitlen \<bar>mantissa f\<bar> + exponent f)"
  3.1098 +lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is
  3.1099 +  "\<lambda>(prec::nat) x. round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
  3.1100  
  3.1101 -definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
  3.1102 -"float_round_down prec f = float_of (round_down (round_prec prec f) f)"
  3.1103 +lemma float_round_down: "real (float_round_down prec x) \<le> real x"
  3.1104 +  using round_down by transfer simp
  3.1105  
  3.1106 -definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
  3.1107 -"float_round_up prec f = float_of (round_up (round_prec prec f) f)"
  3.1108 +lemma floor_add2[simp]: "\<lfloor> real i + x \<rfloor> = i + \<lfloor> x \<rfloor>"
  3.1109 +  using floor_add[of x i] by (simp del: floor_add add: ac_simps)
  3.1110  
  3.1111  lemma compute_float_round_down[code]:
  3.1112 -fixes prec m e
  3.1113 -defines "d == bitlen (abs m) - int prec"
  3.1114 -defines "P == 2^nat d"
  3.1115 -defines "f == Float m e"
  3.1116 -shows "float_round_down prec f = (let d = d in
  3.1117 -    if 0 < d then let P = P ; n = m div P in Float n (e + d)
  3.1118 -             else f)"
  3.1119 -  unfolding float_round_down_def float_down_def[symmetric]
  3.1120 -    compute_float_down f_def Let_def P_def round_prec_def d_def bitlen_Float
  3.1121 -  by (simp add: field_simps)
  3.1122 -  
  3.1123 -lemma compute_float_round_up[code]:
  3.1124 -fixes prec m e
  3.1125 -defines "d == bitlen (abs m) - int prec"
  3.1126 -defines "P == 2^nat d"
  3.1127 -defines "f == Float m e"
  3.1128 -shows "float_round_up prec f = (let d = d in
  3.1129 -  if 0 < d then let P = P ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d)
  3.1130 -           else f)"
  3.1131 -  unfolding float_round_up_def float_up_def[symmetric]
  3.1132 -    compute_float_up f_def Let_def P_def round_prec_def d_def bitlen_Float
  3.1133 -  by (simp add: field_simps)
  3.1134 -
  3.1135 -lemma float_round_up: "real x \<le> real (float_round_up prec x)"
  3.1136 -  using round_up
  3.1137 -  by (simp add: float_round_up_def)
  3.1138 +  "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
  3.1139 +    if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
  3.1140 +             else Float m e)"
  3.1141 +  unfolding Let_def
  3.1142 +  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
  3.1143 +  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
  3.1144 +  apply (cases "m = 0")
  3.1145 +  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
  3.1146 +  done
  3.1147  
  3.1148 -lemma float_round_down: "real (float_round_down prec x) \<le> real x"
  3.1149 -  using round_down
  3.1150 -  by (simp add: float_round_down_def)
  3.1151 -
  3.1152 -instantiation float :: lattice_ab_group_add
  3.1153 -begin
  3.1154 -
  3.1155 -definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
  3.1156 -where "inf_float a b = min a b"
  3.1157 -
  3.1158 -definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
  3.1159 -where "sup_float a b = max a b"
  3.1160 -
  3.1161 -instance
  3.1162 -proof
  3.1163 -  fix x y :: float show "inf x y \<le> x" unfolding inf_float_def by simp
  3.1164 -  show "inf x y \<le> y" unfolding inf_float_def by simp
  3.1165 -  show "x \<le> sup x y" unfolding sup_float_def by simp
  3.1166 -  show "y \<le> sup x y" unfolding sup_float_def by simp
  3.1167 -  fix z::float
  3.1168 -  assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z" unfolding inf_float_def by simp
  3.1169 -  next fix x y z :: float
  3.1170 -  assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x" unfolding sup_float_def by simp
  3.1171 -qed
  3.1172 -
  3.1173 -end
  3.1174 +lemma compute_float_round_up[code]:
  3.1175 +  "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
  3.1176 +     if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P
  3.1177 +                   in Float (n + (if r = 0 then 0 else 1)) (e + d)
  3.1178 +              else Float m e)"
  3.1179 +  using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
  3.1180 +  unfolding Let_def
  3.1181 +  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
  3.1182 +  apply (cases "m = 0")
  3.1183 +  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
  3.1184 +  done
  3.1185  
  3.1186  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
  3.1187   apply (auto simp: zero_float_def mult_le_0_iff)
  3.1188 @@ -1438,63 +1274,38 @@
  3.1189  unfolding nprt_def inf_float_def min_def Float_le_zero_iff ..
  3.1190  
  3.1191  lemma of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
  3.1192 -  unfolding pprt_def sup_float_def max_def sup_real_def by (auto simp: less_eq_float_def)
  3.1193 +  unfolding pprt_def sup_float_def max_def sup_real_def by auto
  3.1194  
  3.1195  lemma of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
  3.1196 -  unfolding nprt_def inf_float_def min_def inf_real_def by (auto simp: less_eq_float_def)
  3.1197 +  unfolding nprt_def inf_float_def min_def inf_real_def by auto
  3.1198  
  3.1199 -definition int_floor_fl :: "float \<Rightarrow> int" where
  3.1200 -  "int_floor_fl f = floor f"
  3.1201 +lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
  3.1202  
  3.1203  lemma compute_int_floor_fl[code]:
  3.1204    shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e
  3.1205                                    else m div (2 ^ (nat (-e))))"
  3.1206 -  by (simp add: int_floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  3.1207 +  by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  3.1208  
  3.1209 -definition floor_fl :: "float \<Rightarrow> float" where
  3.1210 -  "floor_fl f = float_of (floor f)"
  3.1211 +lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
  3.1212  
  3.1213  lemma compute_floor_fl[code]:
  3.1214    shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e
  3.1215                                    else Float (m div (2 ^ (nat (-e)))) 0)"
  3.1216 -  by (simp add: floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  3.1217 +  by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  3.1218  
  3.1219 -lemma floor_fl: "real (floor_fl x) \<le> real x" by (simp add: floor_fl_def)
  3.1220 -lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by (simp add: int_floor_fl_def)
  3.1221 +lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
  3.1222 +
  3.1223 +lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
  3.1224  
  3.1225  lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
  3.1226  proof cases
  3.1227    assume nzero: "floor_fl x \<noteq> float_of 0"
  3.1228 -  have "floor_fl x \<equiv> Float \<lfloor>real x\<rfloor> 0" by (simp add: floor_fl_def)
  3.1229 -  from denormalize_shift[OF this nzero] guess i . note i = this
  3.1230 +  have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
  3.1231 +  from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
  3.1232    thus ?thesis by simp
  3.1233  qed (simp add: floor_fl_def)
  3.1234  
  3.1235 -(* TODO: not used in approximation
  3.1236 -definition ceiling_fl :: "float_of \<Rightarrow> float" where
  3.1237 -  "ceiling_fl f = float_of (ceiling f)"
  3.1238 -
  3.1239 -lemma compute_ceiling_fl:
  3.1240 -  "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
  3.1241 -                                    else Float (m div (2 ^ (nat (-e))) + 1) 0)"
  3.1242 -
  3.1243 -lemma ceiling_fl: "real x \<le> real (ceiling_fl x)"
  3.1244 -
  3.1245 -definition lb_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float" where
  3.1246 -"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
  3.1247 -
  3.1248 -definition ub_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float" where
  3.1249 -"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
  3.1250 -
  3.1251 -lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
  3.1252 -  assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
  3.1253 -  shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
  3.1254 -
  3.1255 -lemma ub_mod: fixes k :: int and x :: float_of assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
  3.1256 -  assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
  3.1257 -  shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
  3.1258 -
  3.1259 -*)
  3.1260 +code_datatype Float
  3.1261  
  3.1262  end
  3.1263