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