tuned proofs in Approximation
authorhoelzl
Tue Nov 05 15:10:59 2013 +0100 (2013-11-05)
changeset 54269dcdfec41a325
parent 54268 807532d15d16
child 54270 7405328f4c3c
tuned proofs in Approximation
src/HOL/Decision_Procs/Approximation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 05 13:23:27 2013 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Nov 05 15:10:59 2013 +0100
     1.3 @@ -132,14 +132,7 @@
     1.4  lemma get_odd[simp]: "odd (get_odd n)" unfolding get_odd_def by (cases "odd n", auto)
     1.5  lemma get_even[simp]: "even (get_even n)" unfolding get_even_def by (cases "even n", auto)
     1.6  lemma get_odd_ex: "\<exists> k. Suc k = get_odd n \<and> odd (Suc k)"
     1.7 -proof (cases "odd n")
     1.8 -  case True hence "0 < n" by (rule odd_pos)
     1.9 -  from gr0_implies_Suc[OF this] obtain k where "Suc k = n" by auto
    1.10 -  thus ?thesis unfolding get_odd_def if_P[OF True] using True[unfolded `Suc k = n`[symmetric]] by blast
    1.11 -next
    1.12 -  case False hence "odd (Suc n)" by auto
    1.13 -  thus ?thesis unfolding get_odd_def if_not_P[OF False] by blast
    1.14 -qed
    1.15 +  by (auto simp: get_odd_def odd_pos intro!: exI[of _ "n - 1"])
    1.16  
    1.17  lemma get_even_double: "\<exists>i. get_even n = 2 * i" using get_even[unfolded even_mult_two_ex] .
    1.18  lemma get_odd_double: "\<exists>i. get_odd n = 2 * i + 1" using get_odd[unfolded odd_Suc_mult_two_ex] by auto
    1.19 @@ -151,47 +144,9 @@
    1.20                        else if u < 0         then (u ^ n, l ^ n)
    1.21                                              else (0, (max (-l) u) ^ n))"
    1.22  
    1.23 -lemma float_power_bnds: fixes x :: real
    1.24 -  assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {l .. u}"
    1.25 -  shows "x ^ n \<in> {l1..u1}"
    1.26 -proof (cases "even n")
    1.27 -  case True
    1.28 -  show ?thesis
    1.29 -  proof (cases "0 < l")
    1.30 -    case True hence "odd n \<or> 0 < l" and "0 \<le> real l" by auto
    1.31 -    have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms
    1.32 -      unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
    1.33 -    have "real l ^ n \<le> x ^ n" and "x ^ n \<le> real u ^ n " using `0 \<le> real l` assms
    1.34 -      by (auto simp: power_mono)
    1.35 -    thus ?thesis using assms `0 < l` unfolding l1 u1 by auto
    1.36 -  next
    1.37 -    case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
    1.38 -    show ?thesis
    1.39 -    proof (cases "u < 0")
    1.40 -      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.41 -      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.42 -        unfolding power_minus_even[OF `even n`] by auto
    1.43 -      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.44 -      ultimately show ?thesis by auto
    1.45 -    next
    1.46 -      case False
    1.47 -      have "\<bar>x\<bar> \<le> real (max (-l) u)"
    1.48 -      proof (cases "-l \<le> u")
    1.49 -        case True thus ?thesis unfolding max_def if_P[OF True] using assms by auto
    1.50 -      next
    1.51 -        case False thus ?thesis unfolding max_def if_not_P[OF False] using assms by auto
    1.52 -      qed
    1.53 -      hence x_abs: "\<bar>x\<bar> \<le> \<bar>real (max (-l) u)\<bar>" by auto
    1.54 -      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.55 -      show ?thesis unfolding atLeastAtMost_iff l1 u1 using zero_le_even_power[OF `even n`] power_mono_even[OF `even n` x_abs] by auto
    1.56 -    qed
    1.57 -  qed
    1.58 -next
    1.59 -  case False hence "odd n \<or> 0 < l" by auto
    1.60 -  have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
    1.61 -  have "real l ^ n \<le> x ^ n" and "x ^ n \<le> real u ^ n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
    1.62 -  thus ?thesis unfolding atLeastAtMost_iff l1 u1 less_float_def by auto
    1.63 -qed
    1.64 +lemma float_power_bnds: "(l1, u1) = float_power_bnds n l u \<Longrightarrow> x \<in> {l .. u} \<Longrightarrow> (x::real) ^ n \<in> {l1..u1}"
    1.65 +  by (auto simp: float_power_bnds_def max_def split: split_if_asm
    1.66 +           intro: power_mono_odd power_mono power_mono_even zero_le_even_power)
    1.67  
    1.68  lemma bnds_power: "\<forall> (x::real) l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {l .. u} \<longrightarrow> l1 \<le> x ^ n \<and> x ^ n \<le> u1"
    1.69    using float_power_bnds by auto
    1.70 @@ -244,7 +199,7 @@
    1.71  qed
    1.72  
    1.73  lemma sqrt_iteration_bound: assumes "0 < real x"
    1.74 -  shows "sqrt x < (sqrt_iteration prec n x)"
    1.75 +  shows "sqrt x < sqrt_iteration prec n x"
    1.76  proof (induct n)
    1.77    case 0
    1.78    show ?case
    1.79 @@ -356,20 +311,8 @@
    1.80    note ub = this
    1.81  
    1.82    show ?thesis
    1.83 -  proof (cases "0 < x")
    1.84 -    case True with lb ub show ?thesis by auto
    1.85 -  next case False show ?thesis
    1.86 -  proof (cases "real x = 0")
    1.87 -    case True thus ?thesis
    1.88 -      by (auto simp add: lb_sqrt.simps ub_sqrt.simps)
    1.89 -  next
    1.90 -    case False with `\<not> 0 < x` have "x < 0" and "0 < -x"
    1.91 -      by auto
    1.92 -
    1.93 -    with `\<not> 0 < x`
    1.94 -    show ?thesis using lb[OF `0 < -x`] ub[OF `0 < -x`]
    1.95 -      by (auto simp add: real_sqrt_minus lb_sqrt.simps ub_sqrt.simps)
    1.96 -  qed qed
    1.97 +    using lb[of "-x"] ub[of "-x"] lb[of x] ub[of x]
    1.98 +    by (auto simp add: lb_sqrt.simps ub_sqrt.simps real_sqrt_minus)
    1.99  qed
   1.100  
   1.101  lemma bnds_sqrt: "\<forall> (x::real) lx ux. (l, u) = (lb_sqrt prec lx, ub_sqrt prec ux) \<and> x \<in> {lx .. ux} \<longrightarrow> l \<le> sqrt x \<and> sqrt x \<le> u"
   1.102 @@ -412,8 +355,8 @@
   1.103    assumes "0 \<le> real x" "real x \<le> 1" and "even n"
   1.104    shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
   1.105  proof -
   1.106 -  let "?c i" = "-1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
   1.107 -  let "?S n" = "\<Sum> i=0..<n. ?c i"
   1.108 +  let ?c = "\<lambda>i. -1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
   1.109 +  let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
   1.110  
   1.111    have "0 \<le> real (x * x)" by auto
   1.112    from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
   1.113 @@ -457,30 +400,11 @@
   1.114  
   1.115  lemma arctan_0_1_bounds: assumes "0 \<le> real x" "real x \<le> 1"
   1.116    shows "arctan x \<in> {(x * lb_arctan_horner prec (get_even n) 1 (x * x)) .. (x * ub_arctan_horner prec (get_odd n) 1 (x * x))}"
   1.117 -proof (cases "even n")
   1.118 -  case True
   1.119 -  obtain n' where "Suc n' = get_odd n" and "odd (Suc n')" using get_odd_ex by auto
   1.120 -  hence "even n'" unfolding even_Suc by auto
   1.121 -  have "arctan x \<le> x * ub_arctan_horner prec (get_odd n) 1 (x * x)"
   1.122 -    unfolding `Suc n' = get_odd n`[symmetric] using arctan_0_1_bounds'[OF `0 \<le> real x` `real x \<le> 1` `even n'`] by auto
   1.123 -  moreover
   1.124 -  have "x * lb_arctan_horner prec (get_even n) 1 (x * x) \<le> arctan x"
   1.125 -    unfolding get_even_def if_P[OF True] using arctan_0_1_bounds'[OF `0 \<le> real x` `real x \<le> 1` `even n`] by auto
   1.126 -  ultimately show ?thesis by auto
   1.127 -next
   1.128 -  case False hence "0 < n" by (rule odd_pos)
   1.129 -  from gr0_implies_Suc[OF this] obtain n' where "n = Suc n'" ..
   1.130 -  from False[unfolded this even_Suc]
   1.131 -  have "even n'" and "even (Suc (Suc n'))" by auto
   1.132 -  have "get_odd n = Suc n'" unfolding get_odd_def if_P[OF False] using `n = Suc n'` .
   1.133 -
   1.134 -  have "arctan x \<le> x * ub_arctan_horner prec (get_odd n) 1 (x * x)"
   1.135 -    unfolding `get_odd n = Suc n'` using arctan_0_1_bounds'[OF `0 \<le> real x` `real x \<le> 1` `even n'`] by auto
   1.136 -  moreover
   1.137 -  have "(x * lb_arctan_horner prec (get_even n) 1 (x * x)) \<le> arctan x"
   1.138 -    unfolding get_even_def if_not_P[OF False] unfolding `n = Suc n'` using arctan_0_1_bounds'[OF `0 \<le> real x` `real x \<le> 1` `even (Suc (Suc n'))`] by auto
   1.139 -  ultimately show ?thesis by auto
   1.140 -qed
   1.141 +  using
   1.142 +    arctan_0_1_bounds'[OF assms, of n prec]
   1.143 +    arctan_0_1_bounds'[OF assms, of "n + 1" prec]
   1.144 +    arctan_0_1_bounds'[OF assms, of "n - 1" prec]
   1.145 +  by (auto simp: get_even_def get_odd_def odd_pos simp del: ub_arctan_horner.simps lb_arctan_horner.simps)
   1.146  
   1.147  subsection "Compute \<pi>"
   1.148  
   1.149 @@ -530,16 +454,11 @@
   1.150      finally have "?k * lb_arctan_horner prec (get_even n) 1 (?k * ?k) \<le> arctan (1 / k)" .
   1.151    } note lb_arctan = this
   1.152  
   1.153 -  have "pi \<le> ub_pi n"
   1.154 -    unfolding ub_pi_def machin_pi Let_def unfolding Float_num
   1.155 -    using lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2]
   1.156 +  have "pi \<le> ub_pi n \<and> lb_pi n \<le> pi"
   1.157 +    unfolding lb_pi_def ub_pi_def machin_pi Let_def unfolding Float_num
   1.158 +    using lb_arctan[of 5] ub_arctan[of 239] lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2]
   1.159      by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
   1.160 -  moreover
   1.161 -  have "lb_pi n \<le> pi"
   1.162 -    unfolding lb_pi_def machin_pi Let_def Float_num
   1.163 -    using lb_arctan[of 5] ub_arctan[of 239] powr_realpow[of 2 2]
   1.164 -    by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
   1.165 -  ultimately show ?thesis by auto
   1.166 +  then show ?thesis by auto
   1.167  qed
   1.168  
   1.169  subsection "Compute arcus tangens in the entire domain"
   1.170 @@ -1808,10 +1727,8 @@
   1.171    done
   1.172  
   1.173  lemma Float_pos_eq_mantissa_pos:  "Float m e > 0 \<longleftrightarrow> m > 0"
   1.174 -  apply (auto simp add: zero_less_mult_iff zero_float_def powr_gt_zero[of 2 "exponent x"] dest: less_zeroE)
   1.175    using powr_gt_zero[of 2 "e"]
   1.176 -  apply simp
   1.177 -  done
   1.178 +  by (auto simp add: zero_less_mult_iff zero_float_def simp del: powr_gt_zero dest: less_zeroE)
   1.179  
   1.180  lemma Float_representation_aux:
   1.181    fixes m e