src/HOL/Decision_Procs/Approximation.thy
 changeset 60017 b785d6d06430 parent 59850 f339ff48a6ee child 60533 1e7ccd864b62
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 09 20:42:38 2015 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 11 11:56:40 2015 +0100
1.3 @@ -241,7 +241,9 @@
1.4    show ?case
1.5    proof (cases x)
1.6      case (Float m e)
1.7 -    hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps)
1.8 +    hence "0 < m" using assms
1.9 +      apply (auto simp: sign_simps)
1.10 +      by (meson not_less powr_ge_pzero)
1.11      hence "0 < sqrt m" by auto
1.12
1.13      have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_nonneg by auto
1.14 @@ -1858,7 +1860,8 @@
1.15    finally show "?ln \<le> ?ub" .
1.16  qed
1.17
1.18 -lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
1.20 +  fixes x::real assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
1.21  proof -
1.22    have "x \<noteq> 0" using assms by auto
1.23    have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
1.24 @@ -1885,7 +1888,7 @@
1.25    let ?uthird = "rapprox_rat (max prec 1) 1 3"
1.26    let ?lthird = "lapprox_rat prec 1 3"
1.27
1.28 -  have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1)"
1.29 +  have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1::real)"
1.30      using ln_add[of "3 / 2" "1 / 2"] by auto
1.31    have lb3: "?lthird \<le> 1 / 3" using lapprox_rat[of prec 1 3] by auto
1.32    hence lb3_ub: "real ?lthird < 1" by auto
1.33 @@ -1955,10 +1958,8 @@
1.34
1.35  lemma float_pos_eq_mantissa_pos:  "x > 0 \<longleftrightarrow> mantissa x > 0"
1.36    apply (subst Float_mantissa_exponent[of x, symmetric])
1.37 -  apply (auto simp add: zero_less_mult_iff zero_float_def powr_gt_zero[of 2 "exponent x"] dest: less_zeroE)
1.38 -  using powr_gt_zero[of 2 "exponent x"]
1.39 -  apply simp
1.40 -  done
1.41 +  apply (auto simp add: zero_less_mult_iff zero_float_def  dest: less_zeroE)
1.42 +  by (metis not_le powr_ge_pzero)
1.43
1.44  lemma Float_pos_eq_mantissa_pos:  "Float m e > 0 \<longleftrightarrow> m > 0"
1.45    using powr_gt_zero[of 2 "e"]
1.46 @@ -2140,8 +2141,9 @@
1.47      let ?s = "Float (e + (bitlen m - 1)) 0"
1.48      let ?x = "Float m (- (bitlen m - 1))"
1.49
1.50 -    have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
1.51 -      by (auto simp: zero_less_mult_iff)
1.52 +    have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
1.53 +      apply (auto simp add: zero_less_mult_iff)
1.54 +      using not_le powr_ge_pzero by blast
1.55      def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
1.56      have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
1.57      from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
1.58 @@ -2180,7 +2182,7 @@
1.59          from float_gt1_scale[OF `1 \<le> Float m e`]
1.60          show "0 \<le> real (e + (bitlen m - 1))" by auto
1.61        next
1.62 -        have "0 \<le> ln 2" by simp
1.63 +        have "0 \<le> ln (2 :: real)" by simp
1.64          thus "0 \<le> real (ub_ln2 prec)" using ub_ln2[of prec] by arith
1.65        qed auto
1.66        ultimately have "ln x \<le> float_plus_up prec ?ub2 ?ub_horner"
1.67 @@ -2333,10 +2335,9 @@
1.68    unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
1.69    by auto
1.70
1.71 -lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
1.72 -  unfolding powr_def interpret_floatarith.simps ..
1.73 -
1.74 -lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
1.75 +lemma interpret_floatarith_log:
1.76 +    "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs =
1.77 +     log (interpret_floatarith b vs) (interpret_floatarith x vs)"
1.78    unfolding log_def interpret_floatarith.simps divide_inverse ..
1.79
1.80  lemma interpret_floatarith_num:
1.81 @@ -3481,7 +3482,7 @@
1.82  subsection {* Implement proof method \texttt{approximation} *}
1.83
1.84  lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
1.85 -  interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
1.86 +  interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
1.87    interpret_floatarith_sin
1.88
1.89  oracle approximation_oracle = {* fn (thy, t) =>
```