src/HOL/Decision_Procs/Approximation.thy
 changeset 56479 91958d4b30f7 parent 56410 a14831ac3023 child 56483 5b82c58b665c
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 08 23:16:00 2014 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 09 09:37:47 2014 +0200
1.3 @@ -1466,8 +1466,7 @@
1.4          using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
1.5          unfolding less_eq_float_def zero_float.rep_eq .
1.6
1.7 -      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0`
1.8 -        by (auto simp: divide_minus_left divide_minus_right)
1.9 +      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
1.10        also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
1.11        also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num" unfolding num_eq fl_eq
1.12          by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
1.13 @@ -1487,16 +1486,15 @@
1.14          case False hence "0 \<le> real ?horner" by auto
1.15
1.16          have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
1.17 -          using `real (floor_fl x) < 0` `real x \<le> 0`
1.18 -            by (auto simp: field_simps intro!: order_trans[OF float_divl])
1.19 +          using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
1.20 +
1.21          have "(?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num \<le>
1.22            exp (float_divl prec x (- floor_fl x)) ^ ?num"
1.23            using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
1.24          also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
1.25            using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
1.26          also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
1.27 -        also have "\<dots> = exp x" using `real ?num \<noteq> 0`
1.28 -          by (auto simp: field_simps)
1.29 +        also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
1.30          finally show ?thesis
1.31            unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_not_P[OF False] by auto
1.32        next
1.33 @@ -1508,8 +1506,7 @@
1.34          have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
1.35          hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
1.36            by (auto intro!: power_mono)
1.37 -        also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
1.38 -          using `real (floor_fl x) \<noteq> 0` by (auto simp: field_simps)
1.39 +        also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
1.40          finally show ?thesis
1.41            unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power .
1.42        qed
```