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.19 +lemma ln_add: 
    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) =>