author wenzelm Sun Aug 18 22:44:39 2013 +0200 (2013-08-18) changeset 53079 ade63ccd6f4e parent 53078 cc06f17d8057 child 53080 d815e25ead03
tuned proofs;
```     1.1 --- a/src/HOL/Transcendental.thy	Sun Aug 18 20:41:47 2013 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Sun Aug 18 22:44:39 2013 +0200
1.3 @@ -2,7 +2,6 @@
1.4      Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
1.5      Author:     Lawrence C Paulson
1.7 -
1.8  *)
1.9
1.10  header{*Power Series, Transcendental Functions etc.*}
1.11 @@ -23,42 +22,44 @@
1.12  qed
1.13
1.14  lemma lemma_realpow_diff_sumr:
1.15 -  fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
1.16 -     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
1.17 +  fixes y :: "'a::{comm_semiring_0,monoid_mult}"
1.18 +  shows
1.19 +    "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
1.20        y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.21 -by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
1.22 -         del: setsum_op_ivl_Suc)
1.23 +  by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac del: setsum_op_ivl_Suc)
1.24
1.25  lemma lemma_realpow_diff_sumr2:
1.26 -  fixes y :: "'a::{comm_ring,monoid_mult}" shows
1.27 -     "x ^ (Suc n) - y ^ (Suc n) =
1.28 +  fixes y :: "'a::{comm_ring,monoid_mult}"
1.29 +  shows
1.30 +    "x ^ (Suc n) - y ^ (Suc n) =
1.31        (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.32 -apply (induct n, simp)
1.33 -apply (simp del: setsum_op_ivl_Suc)
1.34 -apply (subst setsum_op_ivl_Suc)
1.35 -apply (subst lemma_realpow_diff_sumr)
1.36 -apply (simp add: distrib_left del: setsum_op_ivl_Suc)
1.37 -apply (subst mult_left_commute [of "x - y"])
1.38 -apply (erule subst)
1.40 -done
1.41 +  apply (induct n)
1.42 +  apply simp
1.43 +  apply (simp del: setsum_op_ivl_Suc)
1.44 +  apply (subst setsum_op_ivl_Suc)
1.45 +  apply (subst lemma_realpow_diff_sumr)
1.46 +  apply (simp add: distrib_left del: setsum_op_ivl_Suc)
1.47 +  apply (subst mult_left_commute [of "x - y"])
1.48 +  apply (erule subst)
1.49 +  apply (simp add: algebra_simps)
1.50 +  done
1.51
1.52  lemma lemma_realpow_rev_sumr:
1.53 -     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
1.54 -      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
1.55 -apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
1.56 -apply (rule inj_onI, simp)
1.57 -apply auto
1.58 -apply (rule_tac x="n - x" in image_eqI, simp, simp)
1.59 -done
1.60 +  "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
1.61 +    (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
1.62 +  apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
1.63 +  apply (rule inj_onI, simp)
1.64 +  apply auto
1.65 +  apply (rule_tac x="n - x" in image_eqI, simp, simp)
1.66 +  done
1.67
1.68  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
1.69 -x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
1.70 +  x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
1.71
1.72  lemma powser_insidea:
1.73    fixes x z :: "'a::real_normed_field"
1.74    assumes 1: "summable (\<lambda>n. f n * x ^ n)"
1.75 -  assumes 2: "norm z < norm x"
1.76 +    and 2: "norm z < norm x"
1.77    shows "summable (\<lambda>n. norm (f n * z ^ n))"
1.78  proof -
1.79    from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
1.80 @@ -75,7 +76,8 @@
1.81    have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
1.82                     K * norm (z ^ n) * inverse (norm (x ^ n))"
1.83    proof (intro exI allI impI)
1.84 -    fix n::nat assume "0 \<le> n"
1.85 +    fix n::nat
1.86 +    assume "0 \<le> n"
1.87      have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
1.88            norm (f n * x ^ n) * norm (z ^ n)"
1.89        by (simp add: norm_mult abs_mult)
1.90 @@ -108,43 +110,61 @@
1.91  qed
1.92
1.93  lemma powser_inside:
1.94 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
1.95 -     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
1.96 -      ==> summable (%n. f(n) * (z ^ n))"
1.97 -by (rule powser_insidea [THEN summable_norm_cancel])
1.98 -
1.99 -lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows
1.100 -  "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) =
1.101 -   (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))"
1.102 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
1.103 +  shows
1.104 +    "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
1.105 +      summable (\<lambda>n. f n * (z ^ n))"
1.106 +  by (rule powser_insidea [THEN summable_norm_cancel])
1.107 +
1.108 +lemma sum_split_even_odd:
1.109 +  fixes f :: "nat \<Rightarrow> real"
1.110 +  shows
1.111 +    "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) =
1.112 +     (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))"
1.113  proof (induct n)
1.114 +  case 0
1.115 +  then show ?case by simp
1.116 +next
1.117    case (Suc n)
1.118    have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
1.119 -        (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
1.120 +    (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
1.121      using Suc.hyps unfolding One_nat_def by auto
1.122 -  also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
1.123 +  also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))"
1.124 +    by auto
1.125    finally show ?case .
1.126 -qed auto
1.127 -
1.128 -lemma sums_if': fixes g :: "nat \<Rightarrow> real" assumes "g sums x"
1.129 +qed
1.130 +
1.131 +lemma sums_if':
1.132 +  fixes g :: "nat \<Rightarrow> real"
1.133 +  assumes "g sums x"
1.134    shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
1.135    unfolding sums_def
1.136  proof (rule LIMSEQ_I)
1.137 -  fix r :: real assume "0 < r"
1.138 +  fix r :: real
1.139 +  assume "0 < r"
1.140    from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
1.141    obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g { 0..<n } - x) < r)" by blast
1.142
1.143    let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i - 1) div 2)"
1.144 -  { fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto
1.145 +  {
1.146 +    fix m
1.147 +    assume "m \<ge> 2 * no"
1.148 +    hence "m div 2 \<ge> no" by auto
1.149      have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }"
1.150        using sum_split_even_odd by auto
1.151 -    hence "(norm (?SUM (2 * (m div 2)) - x) < r)" using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
1.152 +    hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
1.153 +      using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
1.154      moreover
1.155      have "?SUM (2 * (m div 2)) = ?SUM m"
1.156      proof (cases "even m")
1.157 -      case True show ?thesis unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
1.158 +      case True
1.159 +      show ?thesis
1.160 +        unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
1.161      next
1.162 -      case False hence "even (Suc m)" by auto
1.163 -      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]] odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
1.164 +      case False
1.165 +      hence "even (Suc m)" by auto
1.166 +      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
1.167 +        odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
1.168        have eq: "Suc (2 * (m div 2)) = m" by auto
1.169        hence "even (2 * (m div 2))" using `odd m` by auto
1.170        have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
1.171 @@ -156,13 +176,19 @@
1.172    thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
1.173  qed
1.174
1.175 -lemma sums_if: fixes g :: "nat \<Rightarrow> real" assumes "g sums x" and "f sums y"
1.176 +lemma sums_if:
1.177 +  fixes g :: "nat \<Rightarrow> real"
1.178 +  assumes "g sums x" and "f sums y"
1.179    shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
1.180  proof -
1.181    let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
1.182 -  { fix B T E have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
1.183 -      by (cases B) auto } note if_sum = this
1.184 -  have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x" using sums_if'[OF `g sums x`] .
1.185 +  {
1.186 +    fix B T E
1.187 +    have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
1.188 +      by (cases B) auto
1.189 +  } note if_sum = this
1.190 +  have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
1.191 +    using sums_if'[OF `g sums x`] .
1.192    {
1.193      have "?s 0 = 0" by auto
1.194      have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
1.195 @@ -174,8 +200,8 @@
1.196        unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric]
1.197                  image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def]
1.198                  even_Suc Suc_m1 if_eq .
1.199 -  } from sums_add[OF g_sums this]
1.200 -  show ?thesis unfolding if_sum .
1.201 +  }
1.202 +  from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
1.203  qed
1.204
1.205  subsection {* Alternating series test / Leibniz formula *}
1.206 @@ -186,106 +212,140 @@
1.207    shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and>
1.208               ((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
1.209    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
1.210 -proof -
1.211 +proof (rule nested_sequence_unique)
1.212    have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
1.213
1.214 -  have "\<forall> n. ?f n \<le> ?f (Suc n)"
1.215 -  proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
1.216 -  moreover
1.217 -  have "\<forall> n. ?g (Suc n) \<le> ?g n"
1.218 -  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
1.219 -    unfolding One_nat_def by auto qed
1.220 -  moreover
1.221 -  have "\<forall> n. ?f n \<le> ?g n"
1.222 -  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
1.223 -    unfolding One_nat_def by auto qed
1.224 -  moreover
1.225 -  have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
1.226 -  proof (rule LIMSEQ_I)
1.227 -    fix r :: real assume "0 < r"
1.228 -    with `a ----> 0`[THEN LIMSEQ_D]
1.229 -    obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r" by auto
1.230 -    hence "\<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.231 -    thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.232 +  show "\<forall>n. ?f n \<le> ?f (Suc n)"
1.233 +  proof
1.234 +    fix n
1.235 +    show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto
1.236 +  qed
1.237 +  show "\<forall>n. ?g (Suc n) \<le> ?g n"
1.238 +  proof
1.239 +    fix n
1.240 +    show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
1.241 +      unfolding One_nat_def by auto
1.242 +  qed
1.243 +  show "\<forall>n. ?f n \<le> ?g n"
1.244 +  proof
1.245 +    fix n
1.246 +    show "?f n \<le> ?g n" using fg_diff a_pos
1.247 +      unfolding One_nat_def by auto
1.248    qed
1.249 -  ultimately
1.250 -  show ?thesis by (rule nested_sequence_unique)
1.251 +  show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
1.252 +  proof (rule LIMSEQ_I)
1.253 +    fix r :: real
1.254 +    assume "0 < r"
1.255 +    with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
1.256 +      by auto
1.257 +    hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.258 +    thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.259 +  qed
1.260  qed
1.261
1.262 -lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"
1.263 -  assumes a_zero: "a ----> 0" and a_pos: "\<And> n. 0 \<le> a n"
1.264 -  and a_monotone: "\<And> n. a (Suc n) \<le> a n"
1.265 +lemma summable_Leibniz':
1.266 +  fixes a :: "nat \<Rightarrow> real"
1.267 +  assumes a_zero: "a ----> 0"
1.268 +    and a_pos: "\<And> n. 0 \<le> a n"
1.269 +    and a_monotone: "\<And> n. a (Suc n) \<le> a n"
1.270    shows summable: "summable (\<lambda> n. (-1)^n * a n)"
1.271 -  and "\<And>n. (\<Sum>i=0..<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
1.272 -  and "(\<lambda>n. \<Sum>i=0..<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
1.273 -  and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i=0..<2*n+1. (-1)^i*a i)"
1.274 -  and "(\<lambda>n. \<Sum>i=0..<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
1.275 +    and "\<And>n. (\<Sum>i=0..<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
1.276 +    and "(\<lambda>n. \<Sum>i=0..<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
1.277 +    and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i=0..<2*n+1. (-1)^i*a i)"
1.278 +    and "(\<lambda>n. \<Sum>i=0..<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
1.279  proof -
1.280 -  let "?S n" = "(-1)^n * a n"
1.281 -  let "?P n" = "\<Sum>i=0..<n. ?S i"
1.282 -  let "?f n" = "?P (2 * n)"
1.283 -  let "?g n" = "?P (2 * n + 1)"
1.284 -  obtain l :: real where below_l: "\<forall> n. ?f n \<le> l" and "?f ----> l" and above_l: "\<forall> n. l \<le> ?g n" and "?g ----> l"
1.285 +  let ?S = "\<lambda>n. (-1)^n * a n"
1.286 +  let ?P = "\<lambda>n. \<Sum>i=0..<n. ?S i"
1.287 +  let ?f = "\<lambda>n. ?P (2 * n)"
1.288 +  let ?g = "\<lambda>n. ?P (2 * n + 1)"
1.289 +  obtain l :: real
1.290 +    where below_l: "\<forall> n. ?f n \<le> l"
1.291 +      and "?f ----> l"
1.292 +      and above_l: "\<forall> n. l \<le> ?g n"
1.293 +      and "?g ----> l"
1.294      using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
1.295
1.296 -  let ?Sa = "\<lambda> m. \<Sum> n = 0..<m. ?S n"
1.297 +  let ?Sa = "\<lambda>m. \<Sum> n = 0..<m. ?S n"
1.298    have "?Sa ----> l"
1.299    proof (rule LIMSEQ_I)
1.300 -    fix r :: real assume "0 < r"
1.301 -
1.302 +    fix r :: real
1.303 +    assume "0 < r"
1.304      with `?f ----> l`[THEN LIMSEQ_D]
1.305      obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
1.306
1.307      from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
1.308      obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
1.309
1.310 -    { fix n :: nat
1.311 -      assume "n \<ge> (max (2 * f_no) (2 * g_no))" hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
1.312 +    {
1.313 +      fix n :: nat
1.314 +      assume "n \<ge> (max (2 * f_no) (2 * g_no))"
1.315 +      hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
1.316        have "norm (?Sa n - l) < r"
1.317        proof (cases "even n")
1.318 -        case True from even_nat_div_two_times_two[OF this]
1.319 -        have n_eq: "2 * (n div 2) = n" unfolding numeral_2_eq_2[symmetric] by auto
1.320 -        with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" by auto
1.321 -        from f[OF this]
1.322 -        show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
1.323 +        case True
1.324 +        from even_nat_div_two_times_two[OF this]
1.325 +        have n_eq: "2 * (n div 2) = n"
1.326 +          unfolding numeral_2_eq_2[symmetric] by auto
1.327 +        with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
1.328 +          by auto
1.329 +        from f[OF this] show ?thesis
1.330 +          unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
1.331        next
1.332 -        case False hence "even (n - 1)" by simp
1.333 +        case False
1.334 +        hence "even (n - 1)" by simp
1.335          from even_nat_div_two_times_two[OF this]
1.336 -        have n_eq: "2 * ((n - 1) div 2) = n - 1" unfolding numeral_2_eq_2[symmetric] by auto
1.337 -        hence range_eq: "n - 1 + 1 = n" using odd_pos[OF False] by auto
1.338 -
1.339 -        from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no" by auto
1.340 -        from g[OF this]
1.341 -        show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost range_eq .
1.342 +        have n_eq: "2 * ((n - 1) div 2) = n - 1"
1.343 +          unfolding numeral_2_eq_2[symmetric] by auto
1.344 +        hence range_eq: "n - 1 + 1 = n"
1.345 +          using odd_pos[OF False] by auto
1.346 +
1.347 +        from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
1.348 +          by auto
1.349 +        from g[OF this] show ?thesis
1.350 +          unfolding n_eq atLeastLessThanSuc_atLeastAtMost range_eq .
1.351        qed
1.352      }
1.353 -    thus "\<exists> no. \<forall> n \<ge> no. norm (?Sa n - l) < r" by blast
1.354 +    thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
1.355    qed
1.356 -  hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l" unfolding sums_def atLeastLessThanSuc_atLeastAtMost[symmetric] .
1.357 +  hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
1.358 +    unfolding sums_def atLeastLessThanSuc_atLeastAtMost[symmetric] .
1.359    thus "summable ?S" using summable_def by auto
1.360
1.361    have "l = suminf ?S" using sums_unique[OF sums_l] .
1.362
1.363 -  { fix n show "suminf ?S \<le> ?g n" unfolding sums_unique[OF sums_l, symmetric] using above_l by auto }
1.364 -  { fix n show "?f n \<le> suminf ?S" unfolding sums_unique[OF sums_l, symmetric] using below_l by auto }
1.365 -  show "?g ----> suminf ?S" using `?g ----> l` `l = suminf ?S` by auto
1.366 -  show "?f ----> suminf ?S" using `?f ----> l` `l = suminf ?S` by auto
1.367 +  fix n
1.368 +  show "suminf ?S \<le> ?g n"
1.369 +    unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
1.370 +  show "?f n \<le> suminf ?S"
1.371 +    unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
1.372 +  show "?g ----> suminf ?S"
1.373 +    using `?g ----> l` `l = suminf ?S` by auto
1.374 +  show "?f ----> suminf ?S"
1.375 +    using `?f ----> l` `l = suminf ?S` by auto
1.376  qed
1.377
1.378 -theorem summable_Leibniz: fixes a :: "nat \<Rightarrow> real"
1.379 +theorem summable_Leibniz:
1.380 +  fixes a :: "nat \<Rightarrow> real"
1.381    assumes a_zero: "a ----> 0" and "monoseq a"
1.382    shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
1.383 -  and "0 < a 0 \<longrightarrow> (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n. -1^i * a i .. \<Sum>i=0..<2*n+1. -1^i * a i})" (is "?pos")
1.384 -  and "a 0 < 0 \<longrightarrow> (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n+1. -1^i * a i .. \<Sum>i=0..<2*n. -1^i * a i})" (is "?neg")
1.385 -  and "(\<lambda>n. \<Sum>i=0..<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
1.386 -  and "(\<lambda>n. \<Sum>i=0..<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
1.387 +    and "0 < a 0 \<longrightarrow>
1.388 +      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n. -1^i * a i .. \<Sum>i=0..<2*n+1. -1^i * a i})" (is "?pos")
1.389 +    and "a 0 < 0 \<longrightarrow>
1.390 +      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n+1. -1^i * a i .. \<Sum>i=0..<2*n. -1^i * a i})" (is "?neg")
1.391 +    and "(\<lambda>n. \<Sum>i=0..<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
1.392 +    and "(\<lambda>n. \<Sum>i=0..<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
1.393  proof -
1.394    have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
1.395    proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
1.396      case True
1.397 -    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" by auto
1.398 -    { fix n have "a (Suc n) \<le> a n" using ord[where n="Suc n" and m=n] by auto }
1.399 -    note leibniz = summable_Leibniz'[OF `a ----> 0` ge0] and mono = this
1.400 +    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n"
1.401 +      by auto
1.402 +    {
1.403 +      fix n
1.404 +      have "a (Suc n) \<le> a n"
1.405 +        using ord[where n="Suc n" and m=n] by auto
1.406 +    } note mono = this
1.407 +    note leibniz = summable_Leibniz'[OF `a ----> 0` ge0]
1.408      from leibniz[OF mono]
1.409      show ?thesis using `0 \<le> a 0` by auto
1.410    next
1.411 @@ -293,111 +353,129 @@
1.412      case False
1.413      with monoseq_le[OF `monoseq a` `a ----> 0`]
1.414      have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
1.415 -    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto
1.416 -    { fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto }
1.417 -    note monotone = this
1.418 -    note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
1.419 -    have "summable (\<lambda> n. (-1)^n * ?a n)" using leibniz(1) by auto
1.420 -    then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l" unfolding summable_def by auto
1.421 -    from this[THEN sums_minus]
1.422 -    have "(\<lambda> n. (-1)^n * a n) sums -l" by auto
1.423 +    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
1.424 +      by auto
1.425 +    {
1.426 +      fix n
1.427 +      have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n]
1.428 +        by auto
1.429 +    } note monotone = this
1.430 +    note leibniz =
1.431 +      summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
1.432 +        OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
1.433 +    have "summable (\<lambda> n. (-1)^n * ?a n)"
1.434 +      using leibniz(1) by auto
1.435 +    then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
1.436 +      unfolding summable_def by auto
1.437 +    from this[THEN sums_minus] have "(\<lambda> n. (-1)^n * a n) sums -l"
1.438 +      by auto
1.439      hence ?summable unfolding summable_def by auto
1.440      moreover
1.441 -    have "\<And> a b :: real. \<bar> - a - - b \<bar> = \<bar>a - b\<bar>" unfolding minus_diff_minus by auto
1.442 +    have "\<And>a b :: real. \<bar>- a - - b\<bar> = \<bar>a - b\<bar>"
1.443 +      unfolding minus_diff_minus by auto
1.444
1.445      from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
1.446 -    have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)" by auto
1.447 +    have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
1.448 +      by auto
1.449
1.450      have ?pos using `0 \<le> ?a 0` by auto
1.451 -    moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto
1.452 -    moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] by auto
1.453 +    moreover have ?neg
1.454 +      using leibniz(2,4)
1.455 +      unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le
1.456 +      by auto
1.457 +    moreover have ?f and ?g
1.458 +      using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel]
1.459 +      by auto
1.460      ultimately show ?thesis by auto
1.461    qed
1.462 -  from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
1.463 -       this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2]
1.464 +  from this[THEN conjunct1]
1.465 +    this[THEN conjunct2, THEN conjunct1]
1.466 +    this[THEN conjunct2, THEN conjunct2, THEN conjunct1]
1.467 +    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
1.468 +    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2]
1.469    show ?summable and ?pos and ?neg and ?f and ?g .
1.470  qed
1.471
1.472  subsection {* Term-by-Term Differentiability of Power Series *}
1.473
1.474 -definition
1.475 -  diffs :: "(nat => 'a::ring_1) => nat => 'a" where
1.476 -  "diffs c = (%n. of_nat (Suc n) * c(Suc n))"
1.477 +definition diffs :: "(nat => 'a::ring_1) => nat => 'a"
1.478 +  where "diffs c = (\<lambda>n. of_nat (Suc n) * c(Suc n))"
1.479
1.480  text{*Lemma about distributing negation over it*}
1.481 -lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
1.483 +lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
1.484 +  by (simp add: diffs_def)
1.485
1.486  lemma sums_Suc_imp:
1.487    assumes f: "f 0 = 0"
1.488    shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
1.489 -unfolding sums_def
1.490 -apply (rule LIMSEQ_imp_Suc)
1.491 -apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
1.492 -apply (simp only: setsum_shift_bounds_Suc_ivl)
1.493 -done
1.494 +  unfolding sums_def
1.495 +  apply (rule LIMSEQ_imp_Suc)
1.496 +  apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
1.497 +  apply (simp only: setsum_shift_bounds_Suc_ivl)
1.498 +  done
1.499
1.500  lemma diffs_equiv:
1.501    fixes x :: "'a::{real_normed_vector, ring_1}"
1.502 -  shows "summable (%n. (diffs c)(n) * (x ^ n)) ==>
1.503 -      (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
1.504 +  shows "summable (\<lambda>n. (diffs c)(n) * (x ^ n)) \<Longrightarrow>
1.505 +      (\<lambda>n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
1.506           (\<Sum>n. (diffs c)(n) * (x ^ n))"
1.507 -unfolding diffs_def
1.508 -apply (drule summable_sums)
1.509 -apply (rule sums_Suc_imp, simp_all)
1.510 -done
1.511 +  unfolding diffs_def
1.512 +  apply (drule summable_sums)
1.513 +  apply (rule sums_Suc_imp, simp_all)
1.514 +  done
1.515
1.516  lemma lemma_termdiff1:
1.517    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
1.518    "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
1.519     (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
1.522
1.523  lemma sumr_diff_mult_const2:
1.524    "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
1.526 +  by (simp add: setsum_subtractf)
1.527
1.528  lemma lemma_termdiff2:
1.529    fixes h :: "'a :: {field}"
1.530 -  assumes h: "h \<noteq> 0" shows
1.531 -  "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
1.532 -   h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
1.533 -        (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
1.534 -apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
1.535 -apply (simp add: right_diff_distrib diff_divide_distrib h)
1.536 -apply (simp add: mult_assoc [symmetric])
1.537 -apply (cases "n", simp)
1.538 -apply (simp add: lemma_realpow_diff_sumr2 h
1.539 -                 right_diff_distrib [symmetric] mult_assoc
1.540 -            del: power_Suc setsum_op_ivl_Suc of_nat_Suc)
1.541 -apply (subst lemma_realpow_rev_sumr)
1.542 -apply (subst sumr_diff_mult_const2)
1.543 -apply simp
1.544 -apply (simp only: lemma_termdiff1 setsum_right_distrib)
1.545 -apply (rule setsum_cong [OF refl])
1.547 -apply (clarify)
1.548 -apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
1.549 -            del: setsum_op_ivl_Suc power_Suc)
1.550 -apply (subst mult_assoc [symmetric], subst power_add [symmetric])
1.552 -done
1.553 +  assumes h: "h \<noteq> 0"
1.554 +  shows
1.555 +    "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
1.556 +     h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
1.557 +          (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
1.558 +  apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
1.559 +  apply (simp add: right_diff_distrib diff_divide_distrib h)
1.560 +  apply (simp add: mult_assoc [symmetric])
1.561 +  apply (cases "n", simp)
1.562 +  apply (simp add: lemma_realpow_diff_sumr2 h
1.563 +                   right_diff_distrib [symmetric] mult_assoc
1.564 +              del: power_Suc setsum_op_ivl_Suc of_nat_Suc)
1.565 +  apply (subst lemma_realpow_rev_sumr)
1.566 +  apply (subst sumr_diff_mult_const2)
1.567 +  apply simp
1.568 +  apply (simp only: lemma_termdiff1 setsum_right_distrib)
1.569 +  apply (rule setsum_cong [OF refl])
1.571 +  apply (clarify)
1.572 +  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
1.573 +              del: setsum_op_ivl_Suc power_Suc)
1.574 +  apply (subst mult_assoc [symmetric], subst power_add [symmetric])
1.575 +  apply (simp add: mult_ac)
1.576 +  done
1.577
1.578  lemma real_setsum_nat_ivl_bounded2:
1.579    fixes K :: "'a::linordered_semidom"
1.580    assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
1.581 -  assumes K: "0 \<le> K"
1.582 +    and K: "0 \<le> K"
1.583    shows "setsum f {0..<n-k} \<le> of_nat n * K"
1.584 -apply (rule order_trans [OF setsum_mono])
1.585 -apply (rule f, simp)
1.586 -apply (simp add: mult_right_mono K)
1.587 -done
1.588 +  apply (rule order_trans [OF setsum_mono])
1.589 +  apply (rule f, simp)
1.590 +  apply (simp add: mult_right_mono K)
1.591 +  done
1.592
1.593  lemma lemma_termdiff3:
1.594    fixes h z :: "'a::{real_normed_field}"
1.595    assumes 1: "h \<noteq> 0"
1.596 -  assumes 2: "norm z \<le> K"
1.597 -  assumes 3: "norm (z + h) \<le> K"
1.598 +    and 2: "norm z \<le> K"
1.599 +    and 3: "norm (z + h) \<le> K"
1.600    shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
1.601            \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
1.602  proof -
1.603 @@ -410,14 +488,14 @@
1.604      done
1.605    also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
1.606    proof (rule mult_right_mono [OF _ norm_ge_zero])
1.607 -    from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
1.608 +    from norm_ge_zero 2 have K: "0 \<le> K"
1.609 +      by (rule order_trans)
1.610      have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
1.611        apply (erule subst)
1.612        apply (simp only: norm_mult norm_power power_add)
1.613        apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
1.614        done
1.615 -    show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
1.616 -              (z + h) ^ q * z ^ (n - 2 - q))
1.617 +    show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
1.618            \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
1.619        apply (intro
1.620           order_trans [OF norm_setsum]
1.621 @@ -437,19 +515,20 @@
1.622    fixes f :: "'a::{real_normed_field} \<Rightarrow>
1.623                'b::real_normed_vector"
1.624    assumes k: "0 < (k::real)"
1.625 -  assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
1.626 +    and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
1.627    shows "f -- 0 --> 0"
1.628 -unfolding LIM_eq diff_0_right
1.629 -proof (safe)
1.630 +  unfolding LIM_eq diff_0_right
1.631 +proof safe
1.632    let ?h = "of_real (k / 2)::'a"
1.633    have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
1.634    hence "norm (f ?h) \<le> K * norm ?h" by (rule le)
1.635    hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero])
1.636    hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff)
1.637
1.638 -  fix r::real assume r: "0 < r"
1.639 +  fix r::real
1.640 +  assume r: "0 < r"
1.641    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
1.642 -  proof (cases)
1.643 +  proof cases
1.644      assume "K = 0"
1.645      with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)"
1.646        by simp
1.647 @@ -459,7 +538,8 @@
1.648      with zero_le_K have K: "0 < K" by simp
1.649      show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
1.650      proof (rule exI, safe)
1.651 -      from k r K show "0 < min k (r * inverse K / 2)"
1.652 +      from k r K
1.653 +      show "0 < min k (r * inverse K / 2)"
1.654          by (simp add: mult_pos_pos positive_imp_inverse_positive)
1.655      next
1.656        fix x::'a
1.657 @@ -479,14 +559,14 @@
1.658  qed
1.659
1.660  lemma lemma_termdiff5:
1.661 -  fixes g :: "'a::{real_normed_field} \<Rightarrow>
1.662 -              nat \<Rightarrow> 'b::banach"
1.663 +  fixes g :: "'a::real_normed_field \<Rightarrow> nat \<Rightarrow> 'b::banach"
1.664    assumes k: "0 < (k::real)"
1.665    assumes f: "summable f"
1.666    assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
1.667    shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
1.668  proof (rule lemma_termdiff4 [OF k])
1.669 -  fix h::'a assume "h \<noteq> 0" and "norm h < k"
1.670 +  fix h::'a
1.671 +  assume "h \<noteq> 0" and "norm h < k"
1.672    hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
1.674    hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
1.675 @@ -510,7 +590,7 @@
1.676  lemma termdiffs_aux:
1.677    fixes x :: "'a::{real_normed_field,banach}"
1.678    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
1.679 -  assumes 2: "norm x < norm K"
1.680 +    and 2: "norm x < norm K"
1.681    shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
1.682               - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.683  proof -
1.684 @@ -522,7 +602,6 @@
1.685    show ?thesis
1.686    proof (rule lemma_termdiff5)
1.687      show "0 < r - norm x" using r1 by simp
1.688 -  next
1.689      from r r2 have "norm (of_real r::'a) < norm K"
1.690        by simp
1.691      with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
1.692 @@ -532,8 +611,8 @@
1.693        by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
1.694      hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
1.695        by (rule diffs_equiv [THEN sums_summable])
1.696 -    also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))
1.697 -      = (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
1.698 +    also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
1.699 +      (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
1.700        apply (rule ext)
1.702        apply (case_tac n, simp_all add: r_neq_0)
1.703 @@ -550,8 +629,8 @@
1.704        apply (case_tac "nat", simp)
1.706        done
1.707 -    finally show
1.708 -      "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
1.709 +    finally
1.710 +    show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
1.711    next
1.712      fix h::'a and n::nat
1.713      assume h: "h \<noteq> 0"
1.714 @@ -575,11 +654,11 @@
1.715  lemma termdiffs:
1.716    fixes K x :: "'a::{real_normed_field,banach}"
1.717    assumes 1: "summable (\<lambda>n. c n * K ^ n)"
1.718 -  assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1.719 -  assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1.720 -  assumes 4: "norm x < norm K"
1.721 +    and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1.722 +    and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1.723 +    and 4: "norm x < norm K"
1.724    shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
1.725 -unfolding deriv_def
1.726 +  unfolding deriv_def
1.727  proof (rule LIM_zero_cancel)
1.728    show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
1.729              - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
1.730 @@ -613,24 +692,26 @@
1.732        done
1.733    next
1.734 -    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
1.735 -               of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.736 -        by (rule termdiffs_aux [OF 3 4])
1.737 +    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.738 +      by (rule termdiffs_aux [OF 3 4])
1.739    qed
1.740  qed
1.741
1.742
1.743  subsection {* Derivability of power series *}
1.744
1.745 -lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
1.746 +lemma DERIV_series':
1.747 +  fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
1.748    assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)"
1.749 -  and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
1.750 -  and "summable (f' x0)"
1.751 -  and "summable L" and L_def: "\<And> n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar> f x n - f y n \<bar> \<le> L n * \<bar> x - y \<bar>"
1.752 +    and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
1.753 +    and "summable (f' x0)"
1.754 +    and "summable L"
1.755 +    and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
1.756    shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
1.757    unfolding deriv_def
1.758  proof (rule LIM_I)
1.759 -  fix r :: real assume "0 < r" hence "0 < r/3" by auto
1.760 +  fix r :: real
1.761 +  assume "0 < r" hence "0 < r/3" by auto
1.762
1.763    obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
1.764      using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
1.765 @@ -642,7 +723,7 @@
1.766    have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and
1.767      L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto
1.768
1.769 -  let "?diff i x" = "(f (x0 + x) i - f x0 i) / x"
1.770 +  let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
1.771
1.772    let ?r = "r / (3 * real ?N)"
1.773    have "0 < 3 * real ?N" by auto
1.774 @@ -654,23 +735,30 @@
1.775
1.776    have "0 < S'" unfolding S'_def
1.777    proof (rule iffD2[OF Min_gr_iff])
1.778 -    show "\<forall> x \<in> (?s ` { 0 ..< ?N }). 0 < x"
1.779 -    proof (rule ballI)
1.780 -      fix x assume "x \<in> ?s ` {0..<?N}"
1.781 -      then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast
1.782 +    show "\<forall>x \<in> (?s ` { 0 ..< ?N }). 0 < x"
1.783 +    proof
1.784 +      fix x
1.785 +      assume "x \<in> ?s ` {0..<?N}"
1.786 +      then obtain n where "x = ?s n" and "n \<in> {0..<?N}"
1.787 +        using image_iff[THEN iffD1] by blast
1.788        from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
1.789 -      obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)" by auto
1.790 -      have "0 < ?s n" by (rule someI2[where a=s], auto simp add: s_bound)
1.791 +      obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
1.792 +        by auto
1.793 +      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
1.794        thus "0 < x" unfolding `x = ?s n` .
1.795      qed
1.796    qed auto
1.797
1.798    def S \<equiv> "min (min (x0 - a) (b - x0)) S'"
1.799 -  hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0" and "S \<le> S'" using x0_in_I and `0 < S'`
1.800 +  hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0"
1.801 +    and "S \<le> S'" using x0_in_I and `0 < S'`
1.802      by auto
1.803
1.804 -  { fix x assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
1.805 -    hence x_in_I: "x0 + x \<in> { a <..< b }" using S_a S_b by auto
1.806 +  {
1.807 +    fix x
1.808 +    assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
1.809 +    hence x_in_I: "x0 + x \<in> { a <..< b }"
1.810 +      using S_a S_b by auto
1.811
1.812      note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
1.813      note div_smbl = summable_divide[OF diff_smbl]
1.814 @@ -680,109 +768,164 @@
1.815      note div_shft_smbl = summable_divide[OF diff_shft_smbl]
1.816      note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
1.817
1.818 -    { fix n
1.819 +    {
1.820 +      fix n
1.821        have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
1.822 -        using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] unfolding abs_divide .
1.823 -      hence "\<bar> ( \<bar> ?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)" using `x \<noteq> 0` by auto
1.824 +        using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
1.825 +        unfolding abs_divide .
1.826 +      hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)"
1.827 +        using `x \<noteq> 0` by auto
1.828      } note L_ge = summable_le2[OF allI[OF this] ign[OF `summable L`]]
1.829      from order_trans[OF summable_rabs[OF conjunct1[OF L_ge]] L_ge[THEN conjunct2]]
1.830      have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" .
1.831 -    hence "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3") using L_estimate by auto
1.832 -
1.833 -    have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n \<in> { 0 ..< ?N}. \<bar>?diff n x - f' x0 n \<bar>)" ..
1.834 +    hence "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
1.835 +      using L_estimate by auto
1.836 +
1.837 +    have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> \<le>
1.838 +      (\<Sum>n \<in> { 0 ..< ?N}. \<bar>?diff n x - f' x0 n \<bar>)" ..
1.839      also have "\<dots> < (\<Sum>n \<in> { 0 ..< ?N}. ?r)"
1.840      proof (rule setsum_strict_mono)
1.841 -      fix n assume "n \<in> { 0 ..< ?N}"
1.842 -      have "\<bar> x \<bar> < S" using `\<bar> x \<bar> < S` .
1.843 +      fix n
1.844 +      assume "n \<in> { 0 ..< ?N}"
1.845 +      have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` .
1.846        also have "S \<le> S'" using `S \<le> S'` .
1.847        also have "S' \<le> ?s n" unfolding S'_def
1.848        proof (rule Min_le_iff[THEN iffD2])
1.849 -        have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n" using `n \<in> { 0 ..< ?N}` by auto
1.850 +        have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n"
1.851 +          using `n \<in> { 0 ..< ?N}` by auto
1.852          thus "\<exists> a \<in> (?s ` {0..<?N}). a \<le> ?s n" by blast
1.853        qed auto
1.854 -      finally have "\<bar> x \<bar> < ?s n" .
1.855 +      finally have "\<bar>x\<bar> < ?s n" .
1.856
1.857        from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2]
1.858        have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r" .
1.859 -      with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n`
1.860 -      show "\<bar>?diff n x - f' x0 n\<bar> < ?r" by blast
1.861 +      with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
1.862 +        by blast
1.863      qed auto
1.864 -    also have "\<dots> = of_nat (card {0 ..< ?N}) * ?r" by (rule setsum_constant)
1.865 -    also have "\<dots> = real ?N * ?r" unfolding real_eq_of_nat by auto
1.866 +    also have "\<dots> = of_nat (card {0 ..< ?N}) * ?r"
1.867 +      by (rule setsum_constant)
1.868 +    also have "\<dots> = real ?N * ?r"
1.869 +      unfolding real_eq_of_nat by auto
1.870      also have "\<dots> = r/3" by auto
1.871      finally have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
1.872
1.873      from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
1.874 -    have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> =
1.875 -                    \<bar> \<Sum>n. ?diff n x - f' x0 n \<bar>" unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] using suminf_divide[OF diff_smbl, symmetric] by auto
1.876 -    also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq)
1.877 -    also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto
1.878 +    have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
1.879 +        \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"
1.880 +      unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric]
1.881 +      using suminf_divide[OF diff_smbl, symmetric] by auto
1.882 +    also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>"
1.883 +      unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
1.884 +      unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]]
1.885 +      by (rule abs_triangle_ineq)
1.886 +    also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
1.887 +      using abs_triangle_ineq4 by auto
1.888      also have "\<dots> < r /3 + r/3 + r/3"
1.889        using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
1.891 -    finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r"
1.892 +    finally have "\<bar>(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\<bar> < r"
1.893        by auto
1.894 -  } thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
1.895 -      norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r" using `0 < S`
1.896 -    unfolding real_norm_def diff_0_right by blast
1.897 +  }
1.898 +  thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
1.899 +      norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r"
1.900 +    using `0 < S` unfolding real_norm_def diff_0_right by blast
1.901  qed
1.902
1.903 -lemma DERIV_power_series': fixes f :: "nat \<Rightarrow> real"
1.904 +lemma DERIV_power_series':
1.905 +  fixes f :: "nat \<Rightarrow> real"
1.906    assumes converges: "\<And> x. x \<in> {-R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)"
1.907 -  and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R"
1.908 +    and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R"
1.909    shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)"
1.910    (is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))")
1.911  proof -
1.912 -  { fix R' assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'"
1.913 -    hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}" by auto
1.914 +  {
1.915 +    fix R'
1.916 +    assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'"
1.917 +    hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}"
1.918 +      by auto
1.919      have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))"
1.920      proof (rule DERIV_series')
1.921        show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)"
1.922        proof -
1.923 -        have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" using `0 < R'` `0 < R` `R' < R` by auto
1.924 -        hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}" using `R' < R` by auto
1.925 -        have "norm R' < norm ((R' + R) / 2)" using `0 < R'` `0 < R` `R' < R` by auto
1.926 -        from powser_insidea[OF converges[OF in_Rball] this] show ?thesis by auto
1.927 +        have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
1.928 +          using `0 < R'` `0 < R` `R' < R` by auto
1.929 +        hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}"
1.930 +          using `R' < R` by auto
1.931 +        have "norm R' < norm ((R' + R) / 2)"
1.932 +          using `0 < R'` `0 < R` `R' < R` by auto
1.933 +        from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
1.934 +          by auto
1.935        qed
1.936 -      { fix n x y assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
1.937 +      {
1.938 +        fix n x y
1.939 +        assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
1.940          show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
1.941          proof -
1.942 -          have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> = (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>"
1.943 -            unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto
1.944 +          have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
1.945 +            (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>"
1.946 +            unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
1.947 +            by auto
1.948            also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
1.949            proof (rule mult_left_mono)
1.950 -            have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)" by (rule setsum_abs)
1.951 +            have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
1.952 +              by (rule setsum_abs)
1.953              also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)"
1.954              proof (rule setsum_mono)
1.955 -              fix p assume "p \<in> {0..<Suc n}" hence "p \<le> n" by auto
1.956 -              { fix n fix x :: real assume "x \<in> {-R'<..<R'}"
1.957 +              fix p
1.958 +              assume "p \<in> {0..<Suc n}"
1.959 +              hence "p \<le> n" by auto
1.960 +              {
1.961 +                fix n
1.962 +                fix x :: real
1.963 +                assume "x \<in> {-R'<..<R'}"
1.964                  hence "\<bar>x\<bar> \<le> R'"  by auto
1.965 -                hence "\<bar>x^n\<bar> \<le> R'^n" unfolding power_abs by (rule power_mono, auto)
1.966 -              } from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'`
1.967 -              have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)" unfolding abs_mult by auto
1.968 -              thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n" unfolding power_add[symmetric] using `p \<le> n` by auto
1.969 +                hence "\<bar>x^n\<bar> \<le> R'^n"
1.970 +                  unfolding power_abs by (rule power_mono, auto)
1.971 +              }
1.972 +              from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'`
1.973 +              have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)"
1.974 +                unfolding abs_mult by auto
1.975 +              thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n"
1.976 +                unfolding power_add[symmetric] using `p \<le> n` by auto
1.977              qed
1.978 -            also have "\<dots> = real (Suc n) * R' ^ n" unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
1.979 -            finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
1.980 -            show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult[symmetric] by auto
1.981 +            also have "\<dots> = real (Suc n) * R' ^ n"
1.982 +              unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
1.983 +            finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
1.984 +              unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
1.985 +            show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
1.986 +              unfolding abs_mult[symmetric] by auto
1.987            qed
1.988 -          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra
1.989 +          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>"
1.990 +            unfolding abs_mult mult_assoc[symmetric] by algebra
1.991            finally show ?thesis .
1.992 -        qed }
1.993 -      { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
1.994 -          by (auto intro!: DERIV_intros simp del: power_Suc) }
1.995 -      { fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
1.996 +        qed
1.997 +      }
1.998 +      {
1.999 +        fix n
1.1000 +        show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
1.1001 +          by (auto intro!: DERIV_intros simp del: power_Suc)
1.1002 +      }
1.1003 +      {
1.1004 +        fix x
1.1005 +        assume "x \<in> {-R' <..< R'}"
1.1006 +        hence "R' \<in> {-R <..< R}" and "norm x < norm R'"
1.1007 +          using assms `R' < R` by auto
1.1008          have "summable (\<lambda> n. f n * x^n)"
1.1009          proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
1.1010            fix n
1.1011 -          have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" by (rule mult_left_mono, auto)
1.1012 -          show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult
1.1013 -            by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right])
1.1014 +          have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
1.1015 +            by (rule mult_left_mono) auto
1.1016 +          show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)"
1.1017 +            unfolding real_norm_def abs_mult
1.1018 +            by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
1.1019          qed
1.1020          from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute]
1.1021 -        show "summable (?f x)" by auto }
1.1022 -      show "summable (?f' x0)" using converges[OF `x0 \<in> {-R <..< R}`] .
1.1023 -      show "x0 \<in> {-R' <..< R'}" using `x0 \<in> {-R' <..< R'}` .
1.1024 +        show "summable (?f x)" by auto
1.1025 +      }
1.1026 +      show "summable (?f' x0)"
1.1027 +        using converges[OF `x0 \<in> {-R <..< R}`] .
1.1028 +      show "x0 \<in> {-R' <..< R'}"
1.1029 +        using `x0 \<in> {-R' <..< R'}` .
1.1030      qed
1.1031    } note for_subinterval = this
1.1032    let ?R = "(R + \<bar>x0\<bar>) / 2"
1.1033 @@ -798,15 +941,17 @@
1.1034      also have "\<dots> \<le> x0" using False by auto
1.1035      finally show ?thesis .
1.1036    qed
1.1037 -  hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R" using assms by auto
1.1038 +  hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
1.1039 +    using assms by auto
1.1040    from for_subinterval[OF this]
1.1041    show ?thesis .
1.1042  qed
1.1043
1.1044 +
1.1045  subsection {* Exponential Function *}
1.1046
1.1047 -definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
1.1048 -  "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.1049 +definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
1.1050 +  where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.1051
1.1052  lemma summable_exp_generic:
1.1053    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.1054 @@ -844,34 +989,34 @@
1.1055  proof (rule summable_norm_comparison_test [OF exI, rule_format])
1.1056    show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
1.1057      by (rule summable_exp_generic)
1.1058 -next
1.1059 -  fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
1.1060 +  fix n
1.1061 +  show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
1.1063  qed
1.1064
1.1065 -lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
1.1066 -by (insert summable_exp_generic [where x=x], simp)
1.1067 +lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
1.1068 +  using summable_exp_generic [where x=x] by simp
1.1069
1.1070  lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
1.1071 -unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
1.1072 +  unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
1.1073
1.1074
1.1075  lemma exp_fdiffs:
1.1076 -      "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
1.1077 -by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
1.1078 -         del: mult_Suc of_nat_Suc)
1.1079 +      "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
1.1080 +  by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
1.1081 +        del: mult_Suc of_nat_Suc)
1.1082
1.1083  lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
1.1085 +  by (simp add: diffs_def)
1.1086
1.1087  lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
1.1088 -unfolding exp_def scaleR_conv_of_real
1.1089 -apply (rule DERIV_cong)
1.1090 -apply (rule termdiffs [where K="of_real (1 + norm x)"])
1.1091 -apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
1.1092 -apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
1.1094 -done
1.1095 +  unfolding exp_def scaleR_conv_of_real
1.1096 +  apply (rule DERIV_cong)
1.1097 +  apply (rule termdiffs [where K="of_real (1 + norm x)"])
1.1098 +  apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
1.1099 +  apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
1.1100 +  apply (simp del: of_real_add)
1.1101 +  done
1.1102
1.1103  declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.1104
1.1105 @@ -885,12 +1030,15 @@
1.1106    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
1.1107    by (rule isCont_tendsto_compose [OF isCont_exp])
1.1108
1.1109 -lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
1.1110 +lemma continuous_exp [continuous_intros]:
1.1111 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
1.1112    unfolding continuous_def by (rule tendsto_exp)
1.1113
1.1114 -lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
1.1115 +lemma continuous_on_exp [continuous_on_intros]:
1.1116 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
1.1117    unfolding continuous_on_def by (auto intro: tendsto_exp)
1.1118
1.1119 +
1.1120  subsubsection {* Properties of the Exponential Function *}
1.1121
1.1122  lemma powser_zero:
1.1123 @@ -903,12 +1051,12 @@
1.1124  qed
1.1125
1.1126  lemma exp_zero [simp]: "exp 0 = 1"
1.1127 -unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
1.1128 +  unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
1.1129
1.1130  lemma setsum_cl_ivl_Suc2:
1.1131    "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
1.1133 -         del: setsum_cl_ivl_Suc)
1.1135 +           del: setsum_cl_ivl_Suc)
1.1136
1.1138    fixes x y :: "'a::{real_field}"
1.1139 @@ -957,18 +1105,18 @@
1.1140  qed
1.1141
1.1142  lemma exp_add: "exp (x + y) = exp x * exp y"
1.1143 -unfolding exp_def
1.1144 -by (simp only: Cauchy_product summable_norm_exp exp_series_add)
1.1145 +  unfolding exp_def
1.1146 +  by (simp only: Cauchy_product summable_norm_exp exp_series_add)
1.1147
1.1148  lemma mult_exp_exp: "exp x * exp y = exp (x + y)"
1.1150 +  by (rule exp_add [symmetric])
1.1151
1.1152  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
1.1153 -unfolding exp_def
1.1154 -apply (subst suminf_of_real)
1.1155 -apply (rule summable_exp_generic)
1.1157 -done
1.1158 +  unfolding exp_def
1.1159 +  apply (subst suminf_of_real)
1.1160 +  apply (rule summable_exp_generic)
1.1161 +  apply (simp add: scaleR_conv_of_real)
1.1162 +  done
1.1163
1.1164  lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
1.1165  proof
1.1166 @@ -978,7 +1126,7 @@
1.1167  qed
1.1168
1.1169  lemma exp_minus: "exp (- x) = inverse (exp x)"
1.1170 -by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
1.1171 +  by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
1.1172
1.1173  lemma exp_diff: "exp (x - y) = exp x / exp y"
1.1174    unfolding diff_minus divide_inverse
1.1175 @@ -997,31 +1145,29 @@
1.1176  qed
1.1177
1.1178  lemma exp_gt_zero [simp]: "0 < exp (x::real)"
1.1180 +  by (simp add: order_less_le)
1.1181
1.1182  lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
1.1184 +  by (simp add: not_less)
1.1185
1.1186  lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
1.1188 +  by (simp add: not_le)
1.1189
1.1190  lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
1.1191 -by simp
1.1192 +  by simp
1.1193
1.1194  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
1.1195 -apply (induct "n")
1.1197 -done
1.1198 +  by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute)
1.1199
1.1200  text {* Strict monotonicity of exponential. *}
1.1201
1.1202 -lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
1.1203 -apply (drule order_le_imp_less_or_eq, auto)
1.1205 -apply (rule order_trans)
1.1206 -apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
1.1207 -apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
1.1208 -done
1.1209 +lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) \<Longrightarrow> (1 + x) \<le> exp(x)"
1.1210 +  apply (drule order_le_imp_less_or_eq, auto)
1.1211 +  apply (simp add: exp_def)
1.1212 +  apply (rule order_trans)
1.1213 +  apply (rule_tac [2] n = 2 and f = "(\<lambda>n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
1.1214 +  apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
1.1215 +  done
1.1216
1.1217  lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
1.1218  proof -
1.1219 @@ -1034,7 +1180,8 @@
1.1220
1.1221  lemma exp_less_mono:
1.1222    fixes x y :: real
1.1223 -  assumes "x < y" shows "exp x < exp y"
1.1224 +  assumes "x < y"
1.1225 +  shows "exp x < exp y"
1.1226  proof -
1.1227    from `x < y` have "0 < y - x" by simp
1.1228    hence "1 < exp (y - x)" by (rule exp_gt_one)
1.1229 @@ -1042,19 +1189,19 @@
1.1230    thus "exp x < exp y" by simp
1.1231  qed
1.1232
1.1233 -lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y"
1.1234 -apply (simp add: linorder_not_le [symmetric])
1.1235 -apply (auto simp add: order_le_less exp_less_mono)
1.1236 -done
1.1237 +lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
1.1238 +  apply (simp add: linorder_not_le [symmetric])
1.1239 +  apply (auto simp add: order_le_less exp_less_mono)
1.1240 +  done
1.1241
1.1242  lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
1.1243 -by (auto intro: exp_less_mono exp_less_cancel)
1.1244 +  by (auto intro: exp_less_mono exp_less_cancel)
1.1245
1.1246  lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
1.1247 -by (auto simp add: linorder_not_less [symmetric])
1.1248 +  by (auto simp add: linorder_not_less [symmetric])
1.1249
1.1250  lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
1.1252 +  by (simp add: order_eq_iff)
1.1253
1.1254  text {* Comparisons of @{term "exp x"} with one. *}
1.1255
1.1256 @@ -1073,7 +1220,7 @@
1.1257  lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
1.1258    using exp_inj_iff [where x=x and y=0] by simp
1.1259
1.1260 -lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
1.1261 +lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
1.1262  proof (rule IVT)
1.1263    assume "1 \<le> y"
1.1264    hence "0 \<le> y - 1" by simp
1.1265 @@ -1081,10 +1228,10 @@
1.1266    thus "y \<le> exp (y - 1)" by simp
1.1268
1.1269 -lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y"
1.1270 +lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
1.1271  proof (rule linorder_le_cases [of 1 y])
1.1272 -  assume "1 \<le> y" thus "\<exists>x. exp x = y"
1.1273 -    by (fast dest: lemma_exp_total)
1.1274 +  assume "1 \<le> y"
1.1275 +  thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
1.1276  next
1.1277    assume "0 < y" and "y \<le> 1"
1.1278    hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
1.1279 @@ -1096,8 +1243,8 @@
1.1280
1.1281  subsection {* Natural Logarithm *}
1.1282
1.1283 -definition ln :: "real \<Rightarrow> real" where
1.1284 -  "ln x = (THE u. exp u = x)"
1.1285 +definition ln :: "real \<Rightarrow> real"
1.1286 +  where "ln x = (THE u. exp u = x)"
1.1287
1.1288  lemma ln_exp [simp]: "ln (exp x) = x"
1.1290 @@ -1112,27 +1259,27 @@
1.1291    by (erule subst, rule ln_exp)
1.1292
1.1293  lemma ln_one [simp]: "ln 1 = 0"
1.1294 -  by (rule ln_unique, simp)
1.1295 -
1.1296 -lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
1.1298 +  by (rule ln_unique) simp
1.1299 +
1.1300 +lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.1302
1.1303  lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.1304 -  by (rule ln_unique, simp add: exp_minus)
1.1305 -
1.1306 -lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
1.1307 -  by (rule ln_unique, simp add: exp_diff)
1.1308 +  by (rule ln_unique) (simp add: exp_minus)
1.1309 +
1.1310 +lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
1.1311 +  by (rule ln_unique) (simp add: exp_diff)
1.1312
1.1313  lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
1.1314 -  by (rule ln_unique, simp add: exp_real_of_nat_mult)
1.1315 -
1.1316 -lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.1317 -  by (subst exp_less_cancel_iff [symmetric], simp)
1.1318 -
1.1319 -lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
1.1320 +  by (rule ln_unique) (simp add: exp_real_of_nat_mult)
1.1321 +
1.1322 +lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.1323 +  by (subst exp_less_cancel_iff [symmetric]) simp
1.1324 +
1.1325 +lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
1.1326    by (simp add: linorder_not_less [symmetric])
1.1327
1.1328 -lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
1.1329 +lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
1.1331
1.1332  lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
1.1333 @@ -1146,28 +1293,28 @@
1.1334  lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
1.1335    using ln_le_cancel_iff [of 1 x] by simp
1.1336
1.1337 -lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
1.1338 +lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
1.1339    using ln_le_cancel_iff [of 1 x] by simp
1.1340
1.1341 -lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
1.1342 +lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
1.1343    using ln_le_cancel_iff [of 1 x] by simp
1.1344
1.1345 -lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
1.1346 +lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
1.1347    using ln_less_cancel_iff [of x 1] by simp
1.1348
1.1349  lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
1.1350    using ln_less_cancel_iff [of 1 x] by simp
1.1351
1.1352 -lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
1.1353 +lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
1.1354    using ln_less_cancel_iff [of 1 x] by simp
1.1355
1.1356 -lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
1.1357 +lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
1.1358    using ln_less_cancel_iff [of 1 x] by simp
1.1359
1.1360 -lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
1.1361 +lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
1.1362    using ln_inj_iff [of x 1] by simp
1.1363
1.1364 -lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
1.1365 +lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
1.1366    by simp
1.1367
1.1368  lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
1.1369 @@ -1176,7 +1323,7 @@
1.1370    done
1.1371
1.1372  lemma tendsto_ln [tendsto_intros]:
1.1373 -  "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
1.1374 +  "(f ---> a) F \<Longrightarrow> 0 < a \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
1.1375    by (rule isCont_tendsto_compose [OF isCont_ln])
1.1376
1.1377  lemma continuous_ln:
1.1378 @@ -1201,37 +1348,51 @@
1.1379    apply (simp_all add: abs_if isCont_ln)
1.1380    done
1.1381
1.1382 -lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
1.1383 +lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
1.1384    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1.1385
1.1386  declare DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.1387
1.1388 -lemma ln_series: assumes "0 < x" and "x < 2"
1.1389 -  shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))" (is "ln x = suminf (?f (x - 1))")
1.1390 +lemma ln_series:
1.1391 +  assumes "0 < x" and "x < 2"
1.1392 +  shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
1.1393 +  (is "ln x = suminf (?f (x - 1))")
1.1394  proof -
1.1395 -  let "?f' x n" = "(-1)^n * (x - 1)^n"
1.1396 +  let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
1.1397
1.1398    have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
1.1399    proof (rule DERIV_isconst3[where x=x])
1.1400 -    fix x :: real assume "x \<in> {0 <..< 2}" hence "0 < x" and "x < 2" by auto
1.1401 -    have "norm (1 - x) < 1" using `0 < x` and `x < 2` by auto
1.1402 +    fix x :: real
1.1403 +    assume "x \<in> {0 <..< 2}"
1.1404 +    hence "0 < x" and "x < 2" by auto
1.1405 +    have "norm (1 - x) < 1"
1.1406 +      using `0 < x` and `x < 2` by auto
1.1407      have "1 / x = 1 / (1 - (1 - x))" by auto
1.1408 -    also have "\<dots> = (\<Sum> n. (1 - x)^n)" using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
1.1409 -    also have "\<dots> = suminf (?f' x)" unfolding power_mult_distrib[symmetric] by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
1.1410 -    finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
1.1411 +    also have "\<dots> = (\<Sum> n. (1 - x)^n)"
1.1412 +      using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
1.1413 +    also have "\<dots> = suminf (?f' x)"
1.1414 +      unfolding power_mult_distrib[symmetric]
1.1415 +      by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
1.1416 +    finally have "DERIV ln x :> suminf (?f' x)"
1.1417 +      using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
1.1418      moreover
1.1419      have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
1.1420 -    have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
1.1421 +    have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
1.1422 +      (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
1.1423      proof (rule DERIV_power_series')
1.1424 -      show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto
1.1425 -      { fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
1.1426 -        show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
1.1427 -          unfolding One_nat_def
1.1428 -          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
1.1429 -      }
1.1430 +      show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
1.1431 +        using `0 < x` `x < 2` by auto
1.1432 +      fix x :: real
1.1433 +      assume "x \<in> {- 1<..<1}"
1.1434 +      hence "norm (-x) < 1" by auto
1.1435 +      show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
1.1436 +        unfolding One_nat_def
1.1437 +        by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
1.1438      qed
1.1439 -    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
1.1440 -    hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos .
1.1441 +    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
1.1442 +      unfolding One_nat_def by auto
1.1443 +    hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
1.1444 +      unfolding DERIV_iff repos .
1.1445      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
1.1446        by (rule DERIV_diff)
1.1447      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
1.1448 @@ -1241,7 +1402,7 @@
1.1449
1.1450  lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
1.1451  proof -
1.1452 -  have "exp x = suminf (%n. inverse(fact n) * (x ^ n))"
1.1453 +  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
1.1455    also from summable_exp have "... = (\<Sum> n::nat = 0 ..< 2. inverse(fact n) * (x ^ n)) +
1.1456        (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
1.1457 @@ -1251,13 +1412,14 @@
1.1458    finally show ?thesis .
1.1459  qed
1.1460
1.1461 -lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x\<^sup>2"
1.1462 +lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
1.1463  proof -
1.1464    assume a: "0 <= x"
1.1465    assume b: "x <= 1"
1.1466 -  { fix n :: nat
1.1467 +  {
1.1468 +    fix n :: nat
1.1469      have "2 * 2 ^ n \<le> fact (n + 2)"
1.1470 -      by (induct n, simp, simp)
1.1471 +      by (induct n) simp_all
1.1472      hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
1.1473        by (simp only: real_of_nat_le_iff)
1.1474      hence "2 * 2 ^ n \<le> real (fact (n + 2))"
1.1475 @@ -1265,7 +1427,7 @@
1.1476      hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
1.1477        by (rule le_imp_inverse_le) simp
1.1478      hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
1.1479 -      by (simp add: inverse_mult_distrib power_inverse)
1.1480 +      by (simp add: power_inverse)
1.1481      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
1.1482        by (rule mult_mono)
1.1483          (rule mult_mono, simp_all add: power_le_one a b mult_nonneg_nonneg)
1.1484 @@ -1276,10 +1438,10 @@
1.1485      by (intro sums_mult geometric_sums, simp)
1.1486    hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
1.1487      by simp
1.1488 -  have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
1.1489 +  have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
1.1490    proof -
1.1491 -    have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
1.1492 -        suminf (%n. (x\<^sup>2/2) * ((1/2)^n))"
1.1493 +    have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
1.1494 +        suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
1.1495        apply (rule summable_le)
1.1496        apply (rule allI, rule aux1)
1.1497        apply (rule summable_exp [THEN summable_ignore_initial_segment])
1.1498 @@ -1291,7 +1453,7 @@
1.1499    thus ?thesis unfolding exp_first_two_terms by auto
1.1500  qed
1.1501
1.1502 -lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x"
1.1503 +lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
1.1504  proof -
1.1505    assume a: "0 <= (x::real)" and b: "x < 1"
1.1506    have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
1.1507 @@ -1343,13 +1505,13 @@
1.1508    apply auto
1.1509  done
1.1510
1.1511 -lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x\<^sup>2 <= ln (1 + x)"
1.1512 +lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
1.1513  proof -
1.1514    assume a: "0 <= x" and b: "x <= 1"
1.1515    have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
1.1516      by (rule exp_diff)
1.1517    also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
1.1518 -    apply (rule divide_right_mono)
1.1519 +    apply (rule divide_right_mono)
1.1520      apply (rule exp_bound)
1.1521      apply (rule a, rule b)
1.1522      apply simp
1.1523 @@ -1373,7 +1535,7 @@
1.1524    thus ?thesis by (auto simp only: exp_le_cancel_iff)
1.1525  qed
1.1526
1.1527 -lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))"
1.1528 +lemma aux5: "x < 1 \<Longrightarrow> ln(1 - x) = - ln(1 + x / (1 - x))"
1.1529  proof -
1.1530    assume a: "x < 1"
1.1531    have "ln(1 - x) = - ln(1 / (1 - x))"
1.1532 @@ -1384,27 +1546,28 @@
1.1533        by simp
1.1534      also have "... = ln(1 / (1 - x))"
1.1535        apply (rule ln_div [THEN sym])
1.1536 -      by (insert a, auto)
1.1537 +      using a apply auto
1.1538 +      done
1.1539      finally show ?thesis .
1.1540    qed
1.1541    also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
1.1542    finally show ?thesis .
1.1543  qed
1.1544
1.1545 -lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==>
1.1546 -    - x - 2 * x\<^sup>2 <= ln (1 - x)"
1.1547 +lemma ln_one_minus_pos_lower_bound:
1.1548 +  "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
1.1549  proof -
1.1550    assume a: "0 <= x" and b: "x <= (1 / 2)"
1.1551 -  from b have c: "x < 1"
1.1552 -    by auto
1.1553 +  from b have c: "x < 1" by auto
1.1554    then have "ln (1 - x) = - ln (1 + x / (1 - x))"
1.1555      by (rule aux5)
1.1556    also have "- (x / (1 - x)) <= ..."
1.1557 -  proof -
1.1558 +  proof -
1.1559      have "ln (1 + x / (1 - x)) <= x / (1 - x)"
1.1561        apply (rule divide_nonneg_pos)
1.1562 -      by (insert a c, auto)
1.1563 +      using a c apply auto
1.1564 +      done
1.1565      thus ?thesis
1.1566        by auto
1.1567    qed
1.1568 @@ -1414,29 +1577,29 @@
1.1569    have "0 < 1 - x" using a b by simp
1.1570    hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
1.1571      using mult_right_le_one_le[of "x*x" "2*x"] a b
1.1572 -    by (simp add:field_simps power2_eq_square)
1.1573 +    by (simp add: field_simps power2_eq_square)
1.1574    from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
1.1575      by (rule order_trans)
1.1576  qed
1.1577
1.1578 -lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x"
1.1579 +lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
1.1580    apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
1.1581    apply (subst ln_le_cancel_iff)
1.1582    apply auto
1.1583 -done
1.1584 +  done
1.1585
1.1586  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
1.1587 -    "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x\<^sup>2"
1.1588 +  "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
1.1589  proof -
1.1590    assume x: "0 <= x"
1.1591    assume x1: "x <= 1"
1.1592    from x have "ln (1 + x) <= x"
1.1594 -  then have "ln (1 + x) - x <= 0"
1.1595 +  then have "ln (1 + x) - x <= 0"
1.1596      by simp
1.1597    then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
1.1598      by (rule abs_of_nonpos)
1.1599 -  also have "... = x - ln (1 + x)"
1.1600 +  also have "... = x - ln (1 + x)"
1.1601      by simp
1.1602    also have "... <= x\<^sup>2"
1.1603    proof -
1.1604 @@ -1449,11 +1612,11 @@
1.1605  qed
1.1606
1.1607  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
1.1608 -    "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.1609 +  "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.1610  proof -
1.1611    assume a: "-(1 / 2) <= x"
1.1612    assume b: "x <= 0"
1.1613 -  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
1.1614 +  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
1.1615      apply (subst abs_of_nonpos)
1.1616      apply simp
1.1618 @@ -1469,16 +1632,16 @@
1.1619  qed
1.1620
1.1621  lemma abs_ln_one_plus_x_minus_x_bound:
1.1622 -    "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.1623 +    "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.1624    apply (case_tac "0 <= x")
1.1625    apply (rule order_trans)
1.1626    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
1.1627    apply auto
1.1628    apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
1.1629    apply auto
1.1630 -done
1.1631 -
1.1632 -lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
1.1633 +  done
1.1634 +
1.1635 +lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
1.1636  proof -
1.1637    assume x: "exp 1 <= x" "x <= y"
1.1638    moreover have "0 < exp (1::real)" by simp
1.1639 @@ -1517,14 +1680,14 @@
1.1640    finally show ?thesis using b by (simp add: field_simps)
1.1641  qed
1.1642
1.1643 -lemma ln_le_minus_one:
1.1644 -  "0 < x \<Longrightarrow> ln x \<le> x - 1"
1.1645 +lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
1.1646    using exp_ge_add_one_self[of "ln x"] by simp
1.1647
1.1648  lemma ln_eq_minus_one:
1.1649 -  assumes "0 < x" "ln x = x - 1" shows "x = 1"
1.1650 +  assumes "0 < x" "ln x = x - 1"
1.1651 +  shows "x = 1"
1.1652  proof -
1.1653 -  let "?l y" = "ln y - y + 1"
1.1654 +  let ?l = "\<lambda>y. ln y - y + 1"
1.1655    have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
1.1656      by (auto intro!: DERIV_intros)
1.1657
1.1658 @@ -1534,7 +1697,8 @@
1.1659      from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
1.1660      from `x < a` have "?l x < ?l a"
1.1661      proof (rule DERIV_pos_imp_increasing, safe)
1.1662 -      fix y assume "x \<le> y" "y \<le> a"
1.1663 +      fix y
1.1664 +      assume "x \<le> y" "y \<le> a"
1.1665        with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
1.1666          by (auto simp: field_simps)
1.1667        with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
1.1668 @@ -1545,10 +1709,11 @@
1.1669      finally show "x = 1" using assms by auto
1.1670    next
1.1671      assume "1 < x"
1.1672 -    from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast
1.1673 +    from dense[OF this] obtain a where "1 < a" "a < x" by blast
1.1674      from `a < x` have "?l x < ?l a"
1.1675      proof (rule DERIV_neg_imp_decreasing, safe)
1.1676 -      fix y assume "a \<le> y" "y \<le> x"
1.1677 +      fix y
1.1678 +      assume "a \<le> y" "y \<le> x"
1.1679        with `1 < a` have "1 / y - 1 < 0" "0 < y"
1.1680          by (auto simp: field_simps)
1.1681        with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
1.1682 @@ -1557,18 +1722,24 @@
1.1683      also have "\<dots> \<le> 0"
1.1684        using ln_le_minus_one `1 < a` by (auto simp: field_simps)
1.1685      finally show "x = 1" using assms by auto
1.1686 -  qed simp
1.1687 +  next
1.1688 +    assume "x = 1"
1.1689 +    then show ?thesis by simp
1.1690 +  qed
1.1691  qed
1.1692
1.1693  lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
1.1694    unfolding tendsto_Zfun_iff
1.1695  proof (rule ZfunI, simp add: eventually_at_bot_dense)
1.1696    fix r :: real assume "0 < r"
1.1697 -  { fix x assume "x < ln r"
1.1698 +  {
1.1699 +    fix x
1.1700 +    assume "x < ln r"
1.1701      then have "exp x < exp (ln r)"
1.1702        by simp
1.1703      with `0 < r` have "exp x < r"
1.1704 -      by simp }
1.1705 +      by simp
1.1706 +  }
1.1707    then show "\<exists>k. \<forall>n<k. exp n < r" by auto
1.1708  qed
1.1709
1.1710 @@ -1586,6 +1757,7 @@
1.1711
1.1712  lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
1.1713  proof (induct k)
1.1714 +  case 0
1.1715    show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
1.1717         (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
1.1718 @@ -1607,15 +1779,13 @@
1.1719  qed
1.1720
1.1721
1.1722 -definition
1.1723 -  powr  :: "[real,real] => real"     (infixr "powr" 80) where
1.1724 -    --{*exponentation with real exponent*}
1.1725 -  "x powr a = exp(a * ln x)"
1.1726 -
1.1727 -definition
1.1728 -  log :: "[real,real] => real" where
1.1729 -    --{*logarithm of @{term x} to base @{term a}*}
1.1730 -  "log a x = ln x / ln a"
1.1731 +definition powr :: "[real,real] => real"  (infixr "powr" 80)
1.1732 +  -- {*exponentation with real exponent*}
1.1733 +  where "x powr a = exp(a * ln x)"
1.1734 +
1.1735 +definition log :: "[real,real] => real"
1.1736 +  -- {*logarithm of @{term x} to base @{term a}*}
1.1737 +  where "log a x = ln x / ln a"
1.1738
1.1739
1.1740  lemma tendsto_log [tendsto_intros]:
1.1741 @@ -1623,12 +1793,20 @@
1.1742    unfolding log_def by (intro tendsto_intros) auto
1.1743
1.1744  lemma continuous_log:
1.1745 -  assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\<lambda>x. x))" and "f (Lim F (\<lambda>x. x)) \<noteq> 1" and "0 < g (Lim F (\<lambda>x. x))"
1.1746 +  assumes "continuous F f"
1.1747 +    and "continuous F g"
1.1748 +    and "0 < f (Lim F (\<lambda>x. x))"
1.1749 +    and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
1.1750 +    and "0 < g (Lim F (\<lambda>x. x))"
1.1751    shows "continuous F (\<lambda>x. log (f x) (g x))"
1.1752    using assms unfolding continuous_def by (rule tendsto_log)
1.1753
1.1754  lemma continuous_at_within_log[continuous_intros]:
1.1755 -  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a" and "f a \<noteq> 1" and "0 < g a"
1.1756 +  assumes "continuous (at a within s) f"
1.1757 +    and "continuous (at a within s) g"
1.1758 +    and "0 < f a"
1.1759 +    and "f a \<noteq> 1"
1.1760 +    and "0 < g a"
1.1761    shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
1.1762    using assms unfolding continuous_within by (rule tendsto_log)
1.1763
1.1764 @@ -1638,80 +1816,80 @@
1.1765    using assms unfolding continuous_at by (rule tendsto_log)
1.1766
1.1767  lemma continuous_on_log[continuous_on_intros]:
1.1768 -  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
1.1769 +  assumes "continuous_on s f" "continuous_on s g"
1.1770 +    and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
1.1771    shows "continuous_on s (\<lambda>x. log (f x) (g x))"
1.1772    using assms unfolding continuous_on_def by (fast intro: tendsto_log)
1.1773
1.1774  lemma powr_one_eq_one [simp]: "1 powr a = 1"
1.1776 +  by (simp add: powr_def)
1.1777
1.1778  lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
1.1780 +  by (simp add: powr_def)
1.1781
1.1782  lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
1.1784 +  by (simp add: powr_def)
1.1785  declare powr_one_gt_zero_iff [THEN iffD2, simp]
1.1786
1.1787 -lemma powr_mult:
1.1788 -      "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
1.1790 +lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
1.1792
1.1793  lemma powr_gt_zero [simp]: "0 < x powr a"
1.1795 +  by (simp add: powr_def)
1.1796
1.1797  lemma powr_ge_pzero [simp]: "0 <= x powr y"
1.1798 -by (rule order_less_imp_le, rule powr_gt_zero)
1.1799 +  by (rule order_less_imp_le, rule powr_gt_zero)
1.1800
1.1801  lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
1.1803 -
1.1804 -lemma powr_divide:
1.1805 -     "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"
1.1806 -apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
1.1808 -done
1.1809 +  by (simp add: powr_def)
1.1810 +
1.1811 +lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
1.1812 +  apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
1.1814 +  done
1.1815
1.1816  lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
1.1818    apply (subst exp_diff [THEN sym])
1.1820 -done
1.1821 +  done
1.1822
1.1823  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
1.1825 -
1.1826 -lemma powr_mult_base:
1.1827 -  "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
1.1828 -using assms by (auto simp: powr_add)
1.1830 +
1.1831 +lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
1.1832 +  using assms by (auto simp: powr_add)
1.1833
1.1834  lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
1.1836 +  by (simp add: powr_def)
1.1837
1.1838  lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
1.1839 -by (simp add: powr_powr mult_commute)
1.1840 +  by (simp add: powr_powr mult_commute)
1.1841
1.1842  lemma powr_minus: "x powr (-a) = inverse (x powr a)"
1.1843 -by (simp add: powr_def exp_minus [symmetric])
1.1844 +  by (simp add: powr_def exp_minus [symmetric])
1.1845
1.1846  lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
1.1847 -by (simp add: divide_inverse powr_minus)
1.1848 -
1.1849 -lemma powr_less_mono: "[| a < b; 1 < x |] ==> x powr a < x powr b"
1.1851 -
1.1852 -lemma powr_less_cancel: "[| x powr a < x powr b; 1 < x |] ==> a < b"
1.1854 -
1.1855 -lemma powr_less_cancel_iff [simp]: "1 < x ==> (x powr a < x powr b) = (a < b)"
1.1856 -by (blast intro: powr_less_cancel powr_less_mono)
1.1857 -
1.1858 -lemma powr_le_cancel_iff [simp]: "1 < x ==> (x powr a \<le> x powr b) = (a \<le> b)"
1.1859 -by (simp add: linorder_not_less [symmetric])
1.1860 +  by (simp add: divide_inverse powr_minus)
1.1861 +
1.1862 +lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
1.1863 +  by (simp add: powr_def)
1.1864 +
1.1865 +lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
1.1866 +  by (simp add: powr_def)
1.1867 +
1.1868 +lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
1.1869 +  by (blast intro: powr_less_cancel powr_less_mono)
1.1870 +
1.1871 +lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
1.1872 +  by (simp add: linorder_not_less [symmetric])
1.1873
1.1874  lemma log_ln: "ln x = log (exp(1)) x"
1.1876 -
1.1877 -lemma DERIV_log: assumes "x > 0" shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
1.1878 +  by (simp add: log_def)
1.1879 +
1.1880 +lemma DERIV_log:
1.1881 +  assumes "x > 0"
1.1882 +  shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
1.1883  proof -
1.1884    def lb \<equiv> "1 / ln b"
1.1885    moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
1.1886 @@ -1722,71 +1900,74 @@
1.1887
1.1888  lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.1889
1.1890 -lemma powr_log_cancel [simp]:
1.1891 -     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"
1.1892 -by (simp add: powr_def log_def)
1.1893 -
1.1894 -lemma log_powr_cancel [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a (a powr y) = y"
1.1895 -by (simp add: log_def powr_def)
1.1896 -
1.1897 -lemma log_mult:
1.1898 -     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
1.1899 -      ==> log a (x * y) = log a x + log a y"
1.1900 -by (simp add: log_def ln_mult divide_inverse distrib_right)
1.1901 -
1.1902 -lemma log_eq_div_ln_mult_log:
1.1903 -     "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
1.1904 -      ==> log a x = (ln b/ln a) * log b x"
1.1905 -by (simp add: log_def divide_inverse)
1.1906 +lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
1.1907 +  by (simp add: powr_def log_def)
1.1908 +
1.1909 +lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
1.1910 +  by (simp add: log_def powr_def)
1.1911 +
1.1912 +lemma log_mult:
1.1913 +  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
1.1914 +    log a (x * y) = log a x + log a y"
1.1915 +  by (simp add: log_def ln_mult divide_inverse distrib_right)
1.1916 +
1.1917 +lemma log_eq_div_ln_mult_log:
1.1918 +  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
1.1919 +    log a x = (ln b/ln a) * log b x"
1.1920 +  by (simp add: log_def divide_inverse)
1.1921
1.1922  text{*Base 10 logarithms*}
1.1923 -lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x"
1.1925 -
1.1926 -lemma log_base_10_eq2: "0 < x ==> log 10 x = (log 10 (exp 1)) * ln x"
1.1928 +lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
1.1929 +  by (simp add: log_def)
1.1930 +
1.1931 +lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
1.1932 +  by (simp add: log_def)
1.1933
1.1934  lemma log_one [simp]: "log a 1 = 0"
1.1936 +  by (simp add: log_def)
1.1937
1.1938  lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
1.1940 -
1.1941 -lemma log_inverse:
1.1942 -     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> log a (inverse x) = - log a x"
1.1943 -apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
1.1944 -apply (simp add: log_mult [symmetric])
1.1945 -done
1.1946 -
1.1947 -lemma log_divide:
1.1948 -     "[|0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> log a (x/y) = log a x - log a y"
1.1949 -by (simp add: log_mult divide_inverse log_inverse)
1.1950 +  by (simp add: log_def)
1.1951 +
1.1952 +lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
1.1953 +  apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
1.1954 +  apply (simp add: log_mult [symmetric])
1.1955 +  done
1.1956 +
1.1957 +lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
1.1958 +  by (simp add: log_mult divide_inverse log_inverse)
1.1959
1.1960  lemma log_less_cancel_iff [simp]:
1.1961 -     "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)"
1.1962 -apply safe
1.1963 -apply (rule_tac [2] powr_less_cancel)
1.1964 -apply (drule_tac a = "log a x" in powr_less_mono, auto)
1.1965 -done
1.1966 -
1.1967 -lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
1.1968 +  "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
1.1969 +  apply safe
1.1970 +  apply (rule_tac [2] powr_less_cancel)
1.1971 +  apply (drule_tac a = "log a x" in powr_less_mono, auto)
1.1972 +  done
1.1973 +
1.1974 +lemma log_inj:
1.1975 +  assumes "1 < b"
1.1976 +  shows "inj_on (log b) {0 <..}"
1.1977  proof (rule inj_onI, simp)
1.1978 -  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
1.1979 +  fix x y
1.1980 +  assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
1.1981    show "x = y"
1.1982    proof (cases rule: linorder_cases)
1.1983 +    assume "x = y"
1.1984 +    then show ?thesis by simp
1.1985 +  next
1.1986      assume "x < y" hence "log b x < log b y"
1.1987        using log_less_cancel_iff[OF `1 < b`] pos by simp
1.1988 -    thus ?thesis using * by simp
1.1989 +    then show ?thesis using * by simp
1.1990    next
1.1991      assume "y < x" hence "log b y < log b x"
1.1992        using log_less_cancel_iff[OF `1 < b`] pos by simp
1.1993 -    thus ?thesis using * by simp
1.1994 -  qed simp
1.1995 +    then show ?thesis using * by simp
1.1996 +  qed
1.1997  qed
1.1998
1.1999  lemma log_le_cancel_iff [simp]:
1.2000 -     "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
1.2001 -by (simp add: linorder_not_less [symmetric])
1.2002 +  "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
1.2003 +  by (simp add: linorder_not_less [symmetric])
1.2004
1.2005  lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
1.2006    using log_less_cancel_iff[of a 1 x] by simp
1.2007 @@ -1813,11 +1994,12 @@
1.2008    using log_le_cancel_iff[of a x a] by simp
1.2009
1.2010  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
1.2011 -  apply (induct n, simp)
1.2012 +  apply (induct n)
1.2013 +  apply simp
1.2014    apply (subgoal_tac "real(Suc n) = real n + 1")
1.2015    apply (erule ssubst)
1.2016    apply (subst powr_add, simp, simp)
1.2017 -done
1.2018 +  done
1.2019
1.2020  lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
1.2021    unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
1.2022 @@ -1825,16 +2007,19 @@
1.2023  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
1.2024    apply (case_tac "x = 0", simp, simp)
1.2025    apply (rule powr_realpow [THEN sym], simp)
1.2026 -done
1.2027 +  done
1.2028
1.2029  lemma powr_int:
1.2030    assumes "x > 0"
1.2031    shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
1.2032 -proof cases
1.2033 -  assume "i < 0"
1.2034 +proof (cases "i < 0")
1.2035 +  case True
1.2036    have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
1.2037    show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
1.2038 -qed (simp add: assms powr_realpow[symmetric])
1.2039 +next
1.2040 +  case False
1.2041 +  then show ?thesis by (simp add: assms powr_realpow[symmetric])
1.2042 +qed
1.2043
1.2044  lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
1.2045    using powr_realpow[of x "numeral n"] by simp
1.2046 @@ -1842,44 +2027,42 @@
1.2047  lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
1.2048    using powr_int[of x "neg_numeral n"] by simp
1.2049
1.2050 -lemma root_powr_inverse:
1.2051 -  "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
1.2052 +lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
1.2053    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
1.2054
1.2055  lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
1.2056 -by (unfold powr_def, simp)
1.2057 +  unfolding powr_def by simp
1.2058
1.2059  lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
1.2060 -  apply (case_tac "y = 0")
1.2061 +  apply (cases "y = 0")
1.2062    apply force
1.2063    apply (auto simp add: log_def ln_powr field_simps)
1.2064 -done
1.2065 +  done
1.2066
1.2067  lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
1.2068    apply (subst powr_realpow [symmetric])
1.2069    apply (auto simp add: log_powr)
1.2070 -done
1.2071 +  done
1.2072
1.2073  lemma ln_bound: "1 <= x ==> ln x <= x"
1.2074    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
1.2075    apply simp
1.2077 -done
1.2078 +  done
1.2079
1.2080  lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
1.2081 -  apply (case_tac "x = 1", simp)
1.2082 -  apply (case_tac "a = b", simp)
1.2083 +  apply (cases "x = 1", simp)
1.2084 +  apply (cases "a = b", simp)
1.2085    apply (rule order_less_imp_le)
1.2086    apply (rule powr_less_mono, auto)
1.2087 -done
1.2088 +  done
1.2089
1.2090  lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
1.2091    apply (subst powr_zero_eq_one [THEN sym])
1.2092    apply (rule powr_mono, assumption+)
1.2093 -done
1.2094 -
1.2095 -lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a <
1.2096 -    y powr a"
1.2097 +  done
1.2098 +
1.2099 +lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
1.2100    apply (unfold powr_def)
1.2101    apply (rule exp_less_mono)
1.2102    apply (rule mult_strict_left_mono)
1.2103 @@ -1887,10 +2070,9 @@
1.2104    apply (rule order_less_trans)
1.2105    prefer 2
1.2106    apply assumption+
1.2107 -done
1.2108 -
1.2109 -lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a <
1.2110 -    x powr a"
1.2111 +  done
1.2112 +
1.2113 +lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
1.2114    apply (unfold powr_def)
1.2115    apply (rule exp_less_mono)
1.2116    apply (rule mult_strict_left_mono_neg)
1.2117 @@ -1899,17 +2081,16 @@
1.2118    apply (rule order_less_trans)
1.2119    prefer 2
1.2120    apply assumption+
1.2121 -done
1.2122 +  done
1.2123
1.2124  lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
1.2125    apply (case_tac "a = 0", simp)
1.2126    apply (case_tac "x = y", simp)
1.2127    apply (rule order_less_imp_le)
1.2128    apply (rule powr_less_mono2, auto)
1.2129 -done
1.2130 -
1.2131 -lemma powr_inj:
1.2132 -  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
1.2133 +  done
1.2134 +
1.2135 +lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
1.2136    unfolding powr_def exp_inj_iff by simp
1.2137
1.2138  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
1.2139 @@ -1921,7 +2102,7 @@
1.2140    apply (rule ln_bound)
1.2141    apply (erule ge_one_powr_ge_zero)
1.2142    apply (erule order_less_imp_le)
1.2143 -done
1.2144 +  done
1.2145
1.2146  lemma ln_powr_bound2:
1.2147    assumes "1 < x" and "0 < a"
1.2148 @@ -1962,12 +2143,16 @@
1.2149    unfolding powr_def by (intro tendsto_intros)
1.2150
1.2151  lemma continuous_powr:
1.2152 -  assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\<lambda>x. x))"
1.2153 +  assumes "continuous F f"
1.2154 +    and "continuous F g"
1.2155 +    and "0 < f (Lim F (\<lambda>x. x))"
1.2156    shows "continuous F (\<lambda>x. (f x) powr (g x))"
1.2157    using assms unfolding continuous_def by (rule tendsto_powr)
1.2158
1.2159  lemma continuous_at_within_powr[continuous_intros]:
1.2160 -  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a"
1.2161 +  assumes "continuous (at a within s) f"
1.2162 +    and "continuous (at a within s) g"
1.2163 +    and "0 < f a"
1.2164    shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
1.2165    using assms unfolding continuous_within by (rule tendsto_powr)
1.2166
1.2167 @@ -1984,7 +2169,7 @@
1.2168  (* FIXME: generalize by replacing d by with g x and g ---> d? *)
1.2169  lemma tendsto_zero_powrI:
1.2170    assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
1.2171 -  assumes "0 < d"
1.2172 +    and "0 < d"
1.2173    shows "((\<lambda>x. f x powr d) ---> 0) F"
1.2174  proof (rule tendstoI)
1.2175    fix e :: real assume "0 < e"
1.2176 @@ -2002,7 +2187,8 @@
1.2177  qed
1.2178
1.2179  lemma tendsto_neg_powr:
1.2180 -  assumes "s < 0" and "LIM x F. f x :> at_top"
1.2181 +  assumes "s < 0"
1.2182 +    and "LIM x F. f x :> at_top"
1.2183    shows "((\<lambda>x. f x powr s) ---> 0) F"
1.2184  proof (rule tendstoI)
1.2185    fix e :: real assume "0 < e"
1.2186 @@ -2026,11 +2212,11 @@
1.2187  definition cos_coeff :: "nat \<Rightarrow> real" where
1.2188    "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
1.2189
1.2190 -definition sin :: "real \<Rightarrow> real" where
1.2191 -  "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
1.2192 -
1.2193 -definition cos :: "real \<Rightarrow> real" where
1.2194 -  "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
1.2195 +definition sin :: "real \<Rightarrow> real"
1.2196 +  where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
1.2197 +
1.2198 +definition cos :: "real \<Rightarrow> real"
1.2199 +  where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
1.2200
1.2201  lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
1.2202    unfolding sin_coeff_def by simp
1.2203 @@ -2047,22 +2233,22 @@
1.2204    by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
1.2205
1.2206  lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
1.2207 -unfolding sin_coeff_def
1.2208 -apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.2209 -apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.2210 -done
1.2211 +  unfolding sin_coeff_def
1.2212 +  apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.2213 +  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.2214 +  done
1.2215
1.2216  lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
1.2217 -unfolding cos_coeff_def
1.2218 -apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.2219 -apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.2220 -done
1.2221 +  unfolding cos_coeff_def
1.2222 +  apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.2223 +  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.2224 +  done
1.2225
1.2226  lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
1.2227 -unfolding sin_def by (rule summable_sin [THEN summable_sums])
1.2228 +  unfolding sin_def by (rule summable_sin [THEN summable_sums])
1.2229
1.2230  lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
1.2231 -unfolding cos_def by (rule summable_cos [THEN summable_sums])
1.2232 +  unfolding cos_def by (rule summable_cos [THEN summable_sums])
1.2233
1.2234  lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
1.2235    by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
1.2236 @@ -2174,24 +2360,24 @@
1.2237    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
1.2238
1.2239  lemma DERIV_fun_pow: "DERIV g x :> m ==>
1.2240 -      DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
1.2241 +      DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
1.2242    by (auto intro!: DERIV_intros)
1.2243
1.2244  lemma DERIV_fun_exp:
1.2245 -     "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
1.2246 +     "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
1.2247    by (auto intro!: DERIV_intros)
1.2248
1.2249  lemma DERIV_fun_sin:
1.2250 -     "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
1.2251 +     "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
1.2252    by (auto intro!: DERIV_intros)
1.2253
1.2254  lemma DERIV_fun_cos:
1.2255 -     "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
1.2256 +     "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
1.2257    by (auto intro!: DERIV_intros)
1.2258
1.2260 -     "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
1.2261 -      (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
1.2262 +  "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
1.2263 +    (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
1.2264    (is "?f x = 0")
1.2265  proof -
1.2266    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
1.2267 @@ -2245,15 +2431,14 @@
1.2268
1.2269  subsection {* The Constant Pi *}
1.2270
1.2271 -definition pi :: "real" where
1.2272 -  "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
1.2273 +definition pi :: real
1.2274 +  where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
1.2275
1.2276  text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
1.2277     hence define pi.*}
1.2278
1.2279  lemma sin_paired:
1.2280 -     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1))
1.2281 -      sums  sin x"
1.2282 +  "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
1.2283  proof -
1.2284    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
1.2285      by (rule sin_converges [THEN sums_group], simp)
1.2286 @@ -2261,7 +2446,8 @@
1.2287  qed
1.2288
1.2289  lemma sin_gt_zero:
1.2290 -  assumes "0 < x" and "x < 2" shows "0 < sin x"
1.2291 +  assumes "0 < x" and "x < 2"
1.2292 +  shows "0 < sin x"
1.2293  proof -
1.2294    let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
1.2295    have pos: "\<forall>n. 0 < ?f n"
1.2296 @@ -2285,13 +2471,10 @@
1.2297      by (rule suminf_gt_zero)
1.2298  qed
1.2299
1.2300 -lemma cos_double_less_one: "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"
1.2301 -apply (cut_tac x = x in sin_gt_zero)
1.2302 -apply (auto simp add: cos_squared_eq cos_double)
1.2303 -done
1.2304 -
1.2305 -lemma cos_paired:
1.2306 -     "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.2307 +lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
1.2308 +  using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
1.2309 +
1.2310 +lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.2311  proof -
1.2312    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
1.2313      by (rule cos_converges [THEN sums_group], simp)
1.2314 @@ -2301,52 +2484,51 @@
1.2315  lemma real_mult_inverse_cancel:
1.2316       "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
1.2317        ==> inverse x * y < inverse x1 * u"
1.2318 -apply (rule_tac c=x in mult_less_imp_less_left)
1.2319 -apply (auto simp add: mult_assoc [symmetric])
1.2320 -apply (simp (no_asm) add: mult_ac)
1.2321 -apply (rule_tac c=x1 in mult_less_imp_less_right)
1.2322 -apply (auto simp add: mult_ac)
1.2323 -done
1.2324 +  apply (rule_tac c=x in mult_less_imp_less_left)
1.2325 +  apply (auto simp add: mult_assoc [symmetric])
1.2326 +  apply (simp (no_asm) add: mult_ac)
1.2327 +  apply (rule_tac c=x1 in mult_less_imp_less_right)
1.2328 +  apply (auto simp add: mult_ac)
1.2329 +  done
1.2330
1.2331  lemma real_mult_inverse_cancel2:
1.2332       "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
1.2333 -apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
1.2334 -done
1.2335 +  by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
1.2336
1.2337  lemma realpow_num_eq_if:
1.2338    fixes m :: "'a::power"
1.2339    shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
1.2340 -by (cases n, auto)
1.2341 +  by (cases n) auto
1.2342
1.2343  lemma cos_two_less_zero [simp]: "cos (2) < 0"
1.2344 -apply (cut_tac x = 2 in cos_paired)
1.2345 -apply (drule sums_minus)
1.2346 -apply (rule neg_less_iff_less [THEN iffD1])
1.2347 -apply (frule sums_unique, auto)
1.2348 -apply (rule_tac y =
1.2349 - "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
1.2350 -       in order_less_trans)
1.2351 -apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
1.2352 -apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
1.2353 -apply (rule sumr_pos_lt_pair)
1.2354 -apply (erule sums_summable, safe)
1.2355 -unfolding One_nat_def
1.2357 -            del: fact_Suc)
1.2358 -apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
1.2359 -apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
1.2360 -apply (simp only: real_of_nat_mult)
1.2361 -apply (rule mult_strict_mono, force)
1.2362 -  apply (rule_tac [3] real_of_nat_ge_zero)
1.2363 - prefer 2 apply force
1.2364 -apply (rule real_of_nat_less_iff [THEN iffD2])
1.2365 -apply (rule fact_less_mono_nat, auto)
1.2366 -done
1.2367 +  apply (cut_tac x = 2 in cos_paired)
1.2368 +  apply (drule sums_minus)
1.2369 +  apply (rule neg_less_iff_less [THEN iffD1])
1.2370 +  apply (frule sums_unique, auto)
1.2371 +  apply (rule_tac y =
1.2372 +   "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
1.2373 +         in order_less_trans)
1.2374 +  apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
1.2375 +  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
1.2376 +  apply (rule sumr_pos_lt_pair)
1.2377 +  apply (erule sums_summable, safe)
1.2378 +  unfolding One_nat_def
1.2380 +              del: fact_Suc)
1.2381 +  apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
1.2382 +  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
1.2383 +  apply (simp only: real_of_nat_mult)
1.2384 +  apply (rule mult_strict_mono, force)
1.2385 +    apply (rule_tac [3] real_of_nat_ge_zero)
1.2386 +   prefer 2 apply force
1.2387 +  apply (rule real_of_nat_less_iff [THEN iffD2])
1.2388 +  apply (rule fact_less_mono_nat, auto)
1.2389 +  done
1.2390
1.2391  lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
1.2392  lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
1.2393
1.2394 -lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
1.2395 +lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
1.2396  proof (rule ex_ex1I)
1.2397    show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
1.2398      by (rule IVT2, simp_all)
1.2399 @@ -2367,87 +2549,84 @@
1.2400  qed
1.2401
1.2402  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
1.2404 +  by (simp add: pi_def)
1.2405
1.2406  lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
1.2407 -by (simp add: pi_half cos_is_zero [THEN theI'])
1.2408 +  by (simp add: pi_half cos_is_zero [THEN theI'])
1.2409
1.2410  lemma pi_half_gt_zero [simp]: "0 < pi / 2"
1.2411 -apply (rule order_le_neq_trans)
1.2412 -apply (simp add: pi_half cos_is_zero [THEN theI'])
1.2413 -apply (rule notI, drule arg_cong [where f=cos], simp)
1.2414 -done
1.2415 +  apply (rule order_le_neq_trans)
1.2416 +  apply (simp add: pi_half cos_is_zero [THEN theI'])
1.2417 +  apply (rule notI, drule arg_cong [where f=cos], simp)
1.2418 +  done
1.2419
1.2420  lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
1.2421  lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
1.2422
1.2423  lemma pi_half_less_two [simp]: "pi / 2 < 2"
1.2424 -apply (rule order_le_neq_trans)
1.2425 -apply (simp add: pi_half cos_is_zero [THEN theI'])
1.2426 -apply (rule notI, drule arg_cong [where f=cos], simp)
1.2427 -done
1.2428 +  apply (rule order_le_neq_trans)
1.2429 +  apply (simp add: pi_half cos_is_zero [THEN theI'])
1.2430 +  apply (rule notI, drule arg_cong [where f=cos], simp)
1.2431 +  done
1.2432
1.2433  lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
1.2434  lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
1.2435
1.2436  lemma pi_gt_zero [simp]: "0 < pi"
1.2437 -by (insert pi_half_gt_zero, simp)
1.2438 +  using pi_half_gt_zero by simp
1.2439
1.2440  lemma pi_ge_zero [simp]: "0 \<le> pi"
1.2441 -by (rule pi_gt_zero [THEN order_less_imp_le])
1.2442 +  by (rule pi_gt_zero [THEN order_less_imp_le])
1.2443
1.2444  lemma pi_neq_zero [simp]: "pi \<noteq> 0"
1.2445 -by (rule pi_gt_zero [THEN less_imp_neq, THEN not_sym])
1.2446 +  by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
1.2447
1.2448  lemma pi_not_less_zero [simp]: "\<not> pi < 0"
1.2450 +  by (simp add: linorder_not_less)
1.2451
1.2452  lemma minus_pi_half_less_zero: "-(pi/2) < 0"
1.2453 -by simp
1.2454 +  by simp
1.2455
1.2456  lemma m2pi_less_pi: "- (2 * pi) < pi"
1.2457 -by simp
1.2458 +  by simp
1.2459
1.2460  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
1.2461 -apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
1.2462 -apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
1.2464 -done
1.2465 +  using sin_cos_squared_add2 [where x = "pi/2"]
1.2466 +  using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
1.2467 +  by (simp add: power2_eq_1_iff)
1.2468
1.2469  lemma cos_pi [simp]: "cos pi = -1"
1.2470 -by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
1.2471 +  using cos_add [where x = "pi/2" and y = "pi/2"] by simp
1.2472
1.2473  lemma sin_pi [simp]: "sin pi = 0"
1.2474 -by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
1.2475 +  using sin_add [where x = "pi/2" and y = "pi/2"] by simp
1.2476
1.2477  lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
1.2479 +  by (simp add: cos_diff)
1.2480
1.2481  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
1.2484
1.2485  lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
1.2487 +  by (simp add: sin_diff)
1.2488
1.2489  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
1.2492
1.2493  lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
1.2496
1.2497  lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
1.2500
1.2501  lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
1.2504
1.2505  lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
1.2508
1.2509  lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
1.2510 -apply (induct "n")
1.2511 -apply (auto simp add: real_of_nat_Suc distrib_right)
1.2512 -done
1.2513 +  by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
1.2514
1.2515  lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
1.2516  proof -
1.2517 @@ -2457,58 +2636,57 @@
1.2518  qed
1.2519
1.2520  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
1.2521 -apply (induct "n")
1.2522 -apply (auto simp add: real_of_nat_Suc distrib_right)
1.2523 -done
1.2524 +  by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
1.2525
1.2526  lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
1.2527 -by (simp add: mult_commute [of pi])
1.2528 +  by (simp add: mult_commute [of pi])
1.2529
1.2530  lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
1.2532 +  by (simp add: cos_double)
1.2533
1.2534  lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
1.2535 -by simp
1.2536 +  by simp
1.2537
1.2538  lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
1.2539 -apply (rule sin_gt_zero, assumption)
1.2540 -apply (rule order_less_trans, assumption)
1.2541 -apply (rule pi_half_less_two)
1.2542 -done
1.2543 +  apply (rule sin_gt_zero, assumption)
1.2544 +  apply (rule order_less_trans, assumption)
1.2545 +  apply (rule pi_half_less_two)
1.2546 +  done
1.2547
1.2548  lemma sin_less_zero:
1.2549 -  assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
1.2550 +  assumes "- pi/2 < x" and "x < 0"
1.2551 +  shows "sin x < 0"
1.2552  proof -
1.2553    have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
1.2554    thus ?thesis by simp
1.2555  qed
1.2556
1.2557  lemma pi_less_4: "pi < 4"
1.2558 -by (cut_tac pi_half_less_two, auto)
1.2559 +  using pi_half_less_two by auto
1.2560
1.2561  lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
1.2562 -apply (cut_tac pi_less_4)
1.2563 -apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
1.2564 -apply (cut_tac cos_is_zero, safe)
1.2565 -apply (rename_tac y z)
1.2566 -apply (drule_tac x = y in spec)
1.2567 -apply (drule_tac x = "pi/2" in spec, simp)
1.2568 -done
1.2569 +  apply (cut_tac pi_less_4)
1.2570 +  apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
1.2571 +  apply (cut_tac cos_is_zero, safe)
1.2572 +  apply (rename_tac y z)
1.2573 +  apply (drule_tac x = y in spec)
1.2574 +  apply (drule_tac x = "pi/2" in spec, simp)
1.2575 +  done
1.2576
1.2577  lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
1.2578 -apply (rule_tac x = x and y = 0 in linorder_cases)
1.2579 -apply (rule cos_minus [THEN subst])
1.2580 -apply (rule cos_gt_zero)
1.2581 -apply (auto intro: cos_gt_zero)
1.2582 -done
1.2583 +  apply (rule_tac x = x and y = 0 in linorder_cases)
1.2584 +  apply (rule cos_minus [THEN subst])
1.2585 +  apply (rule cos_gt_zero)
1.2586 +  apply (auto intro: cos_gt_zero)
1.2587 +  done
1.2588
1.2589  lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
1.2590 -apply (auto simp add: order_le_less cos_gt_zero_pi)
1.2591 -apply (subgoal_tac "x = pi/2", auto)
1.2592 -done
1.2593 +  apply (auto simp add: order_le_less cos_gt_zero_pi)
1.2594 +  apply (subgoal_tac "x = pi/2", auto)
1.2595 +  done
1.2596
1.2597  lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
1.2598 -by (simp add: sin_cos_eq cos_gt_zero_pi)
1.2599 +  by (simp add: sin_cos_eq cos_gt_zero_pi)
1.2600
1.2601  lemma pi_ge_two: "2 \<le> pi"
1.2602  proof (rule ccontr)
1.2603 @@ -2528,7 +2706,7 @@
1.2604  qed
1.2605
1.2606  lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
1.2607 -by (auto simp add: order_le_less sin_gt_zero_pi)
1.2608 +  by (auto simp add: order_le_less sin_gt_zero_pi)
1.2609
1.2610  text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
1.2611    It should be possible to factor out some of the common parts. *}
1.2612 @@ -2636,54 +2814,74 @@
1.2613  apply (auto simp add: even_mult_two_ex)
1.2614  done
1.2615
1.2616 -lemma cos_monotone_0_pi: assumes "0 \<le> y" and "y < x" and "x \<le> pi"
1.2617 +lemma cos_monotone_0_pi:
1.2618 +  assumes "0 \<le> y" and "y < x" and "x \<le> pi"
1.2619    shows "cos x < cos y"
1.2620  proof -
1.2621    have "- (x - y) < 0" using assms by auto
1.2622
1.2623    from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
1.2624 -  obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z" by auto
1.2625 +  obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
1.2626 +    by auto
1.2627    hence "0 < z" and "z < pi" using assms by auto
1.2628    hence "0 < sin z" using sin_gt_zero_pi by auto
1.2629 -  hence "cos x - cos y < 0" unfolding cos_diff minus_mult_commute[symmetric] using `- (x - y) < 0` by (rule mult_pos_neg2)
1.2630 +  hence "cos x - cos y < 0"
1.2631 +    unfolding cos_diff minus_mult_commute[symmetric]
1.2632 +    using `- (x - y) < 0` by (rule mult_pos_neg2)
1.2633    thus ?thesis by auto
1.2634  qed
1.2635
1.2636 -lemma cos_monotone_0_pi': assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi" shows "cos x \<le> cos y"
1.2637 +lemma cos_monotone_0_pi':
1.2638 +  assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
1.2639 +  shows "cos x \<le> cos y"
1.2640  proof (cases "y < x")
1.2641 -  case True show ?thesis using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
1.2642 +  case True
1.2643 +  show ?thesis
1.2644 +    using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
1.2645  next
1.2646 -  case False hence "y = x" using `y \<le> x` by auto
1.2647 +  case False
1.2648 +  hence "y = x" using `y \<le> x` by auto
1.2649    thus ?thesis by auto
1.2650  qed
1.2651
1.2652 -lemma cos_monotone_minus_pi_0: assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
1.2653 +lemma cos_monotone_minus_pi_0:
1.2654 +  assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
1.2655    shows "cos y < cos x"
1.2656  proof -
1.2657 -  have "0 \<le> -x" and "-x < -y" and "-y \<le> pi" using assms by auto
1.2658 -  from cos_monotone_0_pi[OF this]
1.2659 -  show ?thesis unfolding cos_minus .
1.2660 +  have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
1.2661 +    using assms by auto
1.2662 +  from cos_monotone_0_pi[OF this] show ?thesis
1.2663 +    unfolding cos_minus .
1.2664  qed
1.2665
1.2666 -lemma cos_monotone_minus_pi_0': assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0" shows "cos y \<le> cos x"
1.2667 +lemma cos_monotone_minus_pi_0':
1.2668 +  assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
1.2669 +  shows "cos y \<le> cos x"
1.2670  proof (cases "y < x")
1.2671 -  case True show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`] by auto
1.2672 +  case True
1.2673 +  show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
1.2674 +    by auto
1.2675  next
1.2676 -  case False hence "y = x" using `y \<le> x` by auto
1.2677 +  case False
1.2678 +  hence "y = x" using `y \<le> x` by auto
1.2679    thus ?thesis by auto
1.2680  qed
1.2681
1.2682 -lemma sin_monotone_2pi': assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2" shows "sin y \<le> sin x"
1.2683 +lemma sin_monotone_2pi':
1.2684 +  assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
1.2685 +  shows "sin y \<le> sin x"
1.2686  proof -
1.2687    have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
1.2688      using pi_ge_two and assms by auto
1.2689 -  from cos_monotone_0_pi'[OF this] show ?thesis unfolding minus_sin_cos_eq[symmetric] by auto
1.2690 +  from cos_monotone_0_pi'[OF this] show ?thesis
1.2691 +    unfolding minus_sin_cos_eq[symmetric] by auto
1.2692  qed
1.2693
1.2694 +
1.2695  subsection {* Tangent *}
1.2696
1.2697 -definition tan :: "real \<Rightarrow> real" where
1.2698 -  "tan = (\<lambda>x. sin x / cos x)"
1.2699 +definition tan :: "real \<Rightarrow> real"
1.2700 +  where "tan = (\<lambda>x. sin x / cos x)"
1.2701
1.2702  lemma tan_zero [simp]: "tan 0 = 0"
1.2704 @@ -2719,10 +2917,11 @@
1.2706
1.2707  lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
1.2708 -by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
1.2709 +  by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
1.2710
1.2711  lemma tan_less_zero:
1.2712 -  assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
1.2713 +  assumes lb: "- pi/2 < x" and "x < 0"
1.2714 +  shows "tan x < 0"
1.2715  proof -
1.2716    have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
1.2717    thus ?thesis by simp
1.2718 @@ -2763,71 +2962,74 @@
1.2719    "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
1.2720    unfolding continuous_on_def by (auto intro: tendsto_tan)
1.2721
1.2722 -lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
1.2723 +lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
1.2724    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
1.2725
1.2726  lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
1.2727 -apply (cut_tac LIM_cos_div_sin)
1.2728 -apply (simp only: LIM_eq)
1.2729 -apply (drule_tac x = "inverse y" in spec, safe, force)
1.2730 -apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
1.2731 -apply (rule_tac x = "(pi/2) - e" in exI)
1.2732 -apply (simp (no_asm_simp))
1.2733 -apply (drule_tac x = "(pi/2) - e" in spec)
1.2734 -apply (auto simp add: tan_def sin_diff cos_diff)
1.2735 -apply (rule inverse_less_iff_less [THEN iffD1])
1.2736 -apply (auto simp add: divide_inverse)
1.2737 -apply (rule mult_pos_pos)
1.2738 -apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
1.2739 -apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
1.2740 -done
1.2741 +  apply (cut_tac LIM_cos_div_sin)
1.2742 +  apply (simp only: LIM_eq)
1.2743 +  apply (drule_tac x = "inverse y" in spec, safe, force)
1.2744 +  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
1.2745 +  apply (rule_tac x = "(pi/2) - e" in exI)
1.2746 +  apply (simp (no_asm_simp))
1.2747 +  apply (drule_tac x = "(pi/2) - e" in spec)
1.2748 +  apply (auto simp add: tan_def sin_diff cos_diff)
1.2749 +  apply (rule inverse_less_iff_less [THEN iffD1])
1.2750 +  apply (auto simp add: divide_inverse)
1.2751 +  apply (rule mult_pos_pos)
1.2752 +  apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
1.2753 +  apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
1.2754 +  done
1.2755
1.2756  lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
1.2757 -apply (frule order_le_imp_less_or_eq, safe)
1.2758 - prefer 2 apply force
1.2759 -apply (drule lemma_tan_total, safe)
1.2760 -apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
1.2761 -apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
1.2762 -apply (drule_tac y = xa in order_le_imp_less_or_eq)
1.2763 -apply (auto dest: cos_gt_zero)
1.2764 -done
1.2765 +  apply (frule order_le_imp_less_or_eq, safe)
1.2766 +   prefer 2 apply force
1.2767 +  apply (drule lemma_tan_total, safe)
1.2768 +  apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
1.2769 +  apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
1.2770 +  apply (drule_tac y = xa in order_le_imp_less_or_eq)
1.2771 +  apply (auto dest: cos_gt_zero)
1.2772 +  done
1.2773
1.2774  lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
1.2775 -apply (cut_tac linorder_linear [of 0 y], safe)
1.2776 -apply (drule tan_total_pos)
1.2777 -apply (cut_tac [2] y="-y" in tan_total_pos, safe)
1.2778 -apply (rule_tac [3] x = "-x" in exI)
1.2779 -apply (auto del: exI intro!: exI)
1.2780 -done
1.2781 +  apply (cut_tac linorder_linear [of 0 y], safe)
1.2782 +  apply (drule tan_total_pos)
1.2783 +  apply (cut_tac [2] y="-y" in tan_total_pos, safe)
1.2784 +  apply (rule_tac [3] x = "-x" in exI)
1.2785 +  apply (auto del: exI intro!: exI)
1.2786 +  done
1.2787
1.2788  lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
1.2789 -apply (cut_tac y = y in lemma_tan_total1, auto)
1.2790 -apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
1.2791 -apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
1.2792 -apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
1.2793 -apply (rule_tac [4] Rolle)
1.2794 -apply (rule_tac [2] Rolle)
1.2795 -apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
1.2797 -txt{*Now, simulate TRYALL*}
1.2798 -apply (rule_tac [!] DERIV_tan asm_rl)
1.2799 -apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
1.2800 -            simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
1.2801 -done
1.2802 -
1.2803 -lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
1.2804 +  apply (cut_tac y = y in lemma_tan_total1, auto)
1.2805 +  apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
1.2806 +  apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
1.2807 +  apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
1.2808 +  apply (rule_tac [4] Rolle)
1.2809 +  apply (rule_tac [2] Rolle)
1.2810 +  apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
1.2812 +  txt{*Now, simulate TRYALL*}
1.2813 +  apply (rule_tac [!] DERIV_tan asm_rl)
1.2814 +  apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
1.2815 +              simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
1.2816 +  done
1.2817 +
1.2818 +lemma tan_monotone:
1.2819 +  assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
1.2820    shows "tan y < tan x"
1.2821  proof -
1.2822 -  have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
1.2823 +  have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
1.2824    proof (rule allI, rule impI)
1.2825 -    fix x' :: real assume "y \<le> x' \<and> x' \<le> x"
1.2826 +    fix x' :: real
1.2827 +    assume "y \<le> x' \<and> x' \<le> x"
1.2828      hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
1.2829      from cos_gt_zero_pi[OF this]
1.2830      have "cos x' \<noteq> 0" by auto
1.2831      thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
1.2832    qed
1.2833    from MVT2[OF `y < x` this]
1.2834 -  obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
1.2835 +  obtain z where "y < z" and "z < x"
1.2836 +    and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
1.2837    hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
1.2838    hence "0 < cos z" using cos_gt_zero_pi by auto
1.2839    hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
1.2840 @@ -2837,10 +3039,16 @@
1.2841    thus ?thesis by auto
1.2842  qed
1.2843
1.2844 -lemma tan_monotone': assumes "- (pi / 2) < y" and "y < pi / 2" and "- (pi / 2) < x" and "x < pi / 2"
1.2845 +lemma tan_monotone':
1.2846 +  assumes "- (pi / 2) < y"
1.2847 +    and "y < pi / 2"
1.2848 +    and "- (pi / 2) < x"
1.2849 +    and "x < pi / 2"
1.2850    shows "(y < x) = (tan y < tan x)"
1.2851  proof
1.2852 -  assume "y < x" thus "tan y < tan x" using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
1.2853 +  assume "y < x"
1.2854 +  thus "tan y < tan x"
1.2855 +    using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
1.2856  next
1.2857    assume "tan y < tan x"
1.2858    show "y < x"
1.2859 @@ -2857,26 +3065,37 @@
1.2860    qed
1.2861  qed
1.2862
1.2863 -lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)" unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
1.2864 +lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
1.2865 +  unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
1.2866
1.2867  lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
1.2869
1.2870 -lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
1.2871 +lemma tan_periodic_nat[simp]:
1.2872 +  fixes n :: nat
1.2873 +  shows "tan (x + real n * pi) = tan x"
1.2874  proof (induct n arbitrary: x)
1.2875 +  case 0
1.2876 +  then show ?case by simp
1.2877 +next
1.2878    case (Suc n)
1.2879 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
1.2880 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
1.2881 +    unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
1.2882    show ?case unfolding split_pi_off using Suc by auto
1.2883 -qed auto
1.2884 +qed
1.2885
1.2886  lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
1.2887  proof (cases "0 \<le> i")
1.2888 -  case True hence i_nat: "real i = real (nat i)" by auto
1.2889 +  case True
1.2890 +  hence i_nat: "real i = real (nat i)" by auto
1.2891    show ?thesis unfolding i_nat by auto
1.2892  next
1.2893 -  case False hence i_nat: "real i = - real (nat (-i))" by auto
1.2894 -  have "tan x = tan (x + real i * pi - real i * pi)" by auto
1.2895 -  also have "\<dots> = tan (x + real i * pi)" unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
1.2896 +  case False
1.2897 +  hence i_nat: "real i = - real (nat (-i))" by auto
1.2898 +  have "tan x = tan (x + real i * pi - real i * pi)"
1.2899 +    by auto
1.2900 +  also have "\<dots> = tan (x + real i * pi)"
1.2901 +    unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
1.2902    finally show ?thesis by auto
1.2903  qed
1.2904
1.2905 @@ -2885,150 +3104,144 @@
1.2906
1.2907  subsection {* Inverse Trigonometric Functions *}
1.2908
1.2909 -definition
1.2910 -  arcsin :: "real => real" where
1.2911 -  "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
1.2912 -
1.2913 -definition
1.2914 -  arccos :: "real => real" where
1.2915 -  "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
1.2916 -
1.2917 -definition
1.2918 -  arctan :: "real => real" where
1.2919 -  "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
1.2920 +definition arcsin :: "real => real"
1.2921 +  where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
1.2922 +
1.2923 +definition arccos :: "real => real"
1.2924 +  where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
1.2925 +
1.2926 +definition arctan :: "real => real"
1.2927 +  where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
1.2928
1.2929  lemma arcsin:
1.2930 -     "[| -1 \<le> y; y \<le> 1 |]
1.2931 -      ==> -(pi/2) \<le> arcsin y &
1.2932 -           arcsin y \<le> pi/2 & sin(arcsin y) = y"
1.2933 -unfolding arcsin_def by (rule theI' [OF sin_total])
1.2934 +  "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
1.2935 +    -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
1.2936 +  unfolding arcsin_def by (rule theI' [OF sin_total])
1.2937
1.2938  lemma arcsin_pi:
1.2939 -     "[| -1 \<le> y; y \<le> 1 |]
1.2940 -      ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
1.2941 -apply (drule (1) arcsin)
1.2942 -apply (force intro: order_trans)
1.2943 -done
1.2944 -
1.2945 -lemma sin_arcsin [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> sin(arcsin y) = y"
1.2946 -by (blast dest: arcsin)
1.2947 -
1.2948 -lemma arcsin_bounded:
1.2949 -     "[| -1 \<le> y; y \<le> 1 |] ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
1.2950 -by (blast dest: arcsin)
1.2951 -
1.2952 -lemma arcsin_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> -(pi/2) \<le> arcsin y"
1.2953 -by (blast dest: arcsin)
1.2954 -
1.2955 -lemma arcsin_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcsin y \<le> pi/2"
1.2956 -by (blast dest: arcsin)
1.2957 +  "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
1.2958 +  apply (drule (1) arcsin)
1.2959 +  apply (force intro: order_trans)
1.2960 +  done
1.2961 +
1.2962 +lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
1.2963 +  by (blast dest: arcsin)
1.2964 +
1.2965 +lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
1.2966 +  by (blast dest: arcsin)
1.2967 +
1.2968 +lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
1.2969 +  by (blast dest: arcsin)
1.2970 +
1.2971 +lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
1.2972 +  by (blast dest: arcsin)
1.2973
1.2974  lemma arcsin_lt_bounded:
1.2975       "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
1.2976 -apply (frule order_less_imp_le)
1.2977 -apply (frule_tac y = y in order_less_imp_le)
1.2978 -apply (frule arcsin_bounded)
1.2979 -apply (safe, simp)
1.2980 -apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
1.2981 -apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
1.2982 -apply (drule_tac [!] f = sin in arg_cong, auto)
1.2983 -done
1.2984 +  apply (frule order_less_imp_le)
1.2985 +  apply (frule_tac y = y in order_less_imp_le)
1.2986 +  apply (frule arcsin_bounded)
1.2987 +  apply (safe, simp)
1.2988 +  apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
1.2989 +  apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
1.2990 +  apply (drule_tac [!] f = sin in arg_cong, auto)
1.2991 +  done
1.2992
1.2993  lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
1.2994 -apply (unfold arcsin_def)
1.2995 -apply (rule the1_equality)
1.2996 -apply (rule sin_total, auto)
1.2997 -done
1.2998 +  apply (unfold arcsin_def)
1.2999 +  apply (rule the1_equality)
1.3000 +  apply (rule sin_total, auto)
1.3001 +  done
1.3002
1.3003  lemma arccos:
1.3004       "[| -1 \<le> y; y \<le> 1 |]
1.3005        ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
1.3006 -unfolding arccos_def by (rule theI' [OF cos_total])
1.3007 +  unfolding arccos_def by (rule theI' [OF cos_total])
1.3008
1.3009  lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
1.3010 -by (blast dest: arccos)
1.3011 +  by (blast dest: arccos)
1.3012
1.3013  lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
1.3014 -by (blast dest: arccos)
1.3015 +  by (blast dest: arccos)
1.3016
1.3017  lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
1.3018 -by (blast dest: arccos)
1.3019 +  by (blast dest: arccos)
1.3020
1.3021  lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
1.3022 -by (blast dest: arccos)
1.3023 +  by (blast dest: arccos)
1.3024
1.3025  lemma arccos_lt_bounded:
1.3026       "[| -1 < y; y < 1 |]
1.3027        ==> 0 < arccos y & arccos y < pi"
1.3028 -apply (frule order_less_imp_le)
1.3029 -apply (frule_tac y = y in order_less_imp_le)
1.3030 -apply (frule arccos_bounded, auto)
1.3031 -apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
1.3032 -apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
1.3033 -apply (drule_tac [!] f = cos in arg_cong, auto)
1.3034 -done
1.3035 +  apply (frule order_less_imp_le)
1.3036 +  apply (frule_tac y = y in order_less_imp_le)
1.3037 +  apply (frule arccos_bounded, auto)
1.3038 +  apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
1.3039 +  apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
1.3040 +  apply (drule_tac [!] f = cos in arg_cong, auto)
1.3041 +  done
1.3042
1.3043  lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
1.3045 -apply (auto intro!: the1_equality cos_total)
1.3046 -done
1.3047 +  apply (simp add: arccos_def)
1.3048 +  apply (auto intro!: the1_equality cos_total)
1.3049 +  done
1.3050
1.3051  lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
1.3053 -apply (auto intro!: the1_equality cos_total)
1.3054 -done
1.3055 +  apply (simp add: arccos_def)
1.3056 +  apply (auto intro!: the1_equality cos_total)
1.3057 +  done
1.3058
1.3059  lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
1.3060 -apply (subgoal_tac "x\<^sup>2 \<le> 1")
1.3061 -apply (rule power2_eq_imp_eq)
1.3063 -apply (rule cos_ge_zero)
1.3064 -apply (erule (1) arcsin_lbound)
1.3065 -apply (erule (1) arcsin_ubound)
1.3066 -apply simp
1.3067 -apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
1.3068 -apply (rule power_mono, simp, simp)
1.3069 -done
1.3070 +  apply (subgoal_tac "x\<^sup>2 \<le> 1")
1.3071 +  apply (rule power2_eq_imp_eq)
1.3072 +  apply (simp add: cos_squared_eq)
1.3073 +  apply (rule cos_ge_zero)
1.3074 +  apply (erule (1) arcsin_lbound)
1.3075 +  apply (erule (1) arcsin_ubound)
1.3076 +  apply simp
1.3077 +  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
1.3078 +  apply (rule power_mono, simp, simp)
1.3079 +  done
1.3080
1.3081  lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
1.3082 -apply (subgoal_tac "x\<^sup>2 \<le> 1")
1.3083 -apply (rule power2_eq_imp_eq)
1.3085 -apply (rule sin_ge_zero)
1.3086 -apply (erule (1) arccos_lbound)
1.3087 -apply (erule (1) arccos_ubound)
1.3088 -apply simp
1.3089 -apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
1.3090 -apply (rule power_mono, simp, simp)
1.3091 -done
1.3092 -
1.3093 -lemma arctan [simp]:
1.3094 -     "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
1.3095 -unfolding arctan_def by (rule theI' [OF tan_total])
1.3096 -
1.3097 -lemma tan_arctan: "tan(arctan y) = y"
1.3098 -by auto
1.3099 +  apply (subgoal_tac "x\<^sup>2 \<le> 1")
1.3100 +  apply (rule power2_eq_imp_eq)
1.3101 +  apply (simp add: sin_squared_eq)
1.3102 +  apply (rule sin_ge_zero)
1.3103 +  apply (erule (1) arccos_lbound)
1.3104 +  apply (erule (1) arccos_ubound)
1.3105 +  apply simp
1.3106 +  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
1.3107 +  apply (rule power_mono, simp, simp)
1.3108 +  done
1.3109 +
1.3110 +lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
1.3111 +  unfolding arctan_def by (rule theI' [OF tan_total])
1.3112 +
1.3113 +lemma tan_arctan: "tan (arctan y) = y"
1.3114 +  by auto
1.3115
1.3116  lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
1.3117 -by (auto simp only: arctan)
1.3118 +  by (auto simp only: arctan)
1.3119
1.3120  lemma arctan_lbound: "- (pi/2) < arctan y"
1.3121 -by auto
1.3122 +  by auto
1.3123
1.3124  lemma arctan_ubound: "arctan y < pi/2"
1.3125 -by (auto simp only: arctan)
1.3126 +  by (auto simp only: arctan)
1.3127
1.3128  lemma arctan_unique:
1.3129 -  assumes "-(pi/2) < x" and "x < pi/2" and "tan x = y"
1.3130 +  assumes "-(pi/2) < x"
1.3131 +    and "x < pi/2"
1.3132 +    and "tan x = y"
1.3133    shows "arctan y = x"
1.3134    using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
1.3135
1.3136 -lemma arctan_tan:
1.3137 -      "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x"
1.3138 -  by (rule arctan_unique, simp_all)
1.3139 +lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
1.3140 +  by (rule arctan_unique) simp_all
1.3141
1.3142  lemma arctan_zero_zero [simp]: "arctan 0 = 0"
1.3143 -  by (rule arctan_unique, simp_all)
1.3144 +  by (rule arctan_unique) simp_all
1.3145
1.3146  lemma arctan_minus: "arctan (- x) = - arctan x"
1.3147    apply (rule arctan_unique)
1.3148 @@ -3059,12 +3272,12 @@
1.3150
1.3151  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
1.3152 -apply (rule power_inverse [THEN subst])
1.3153 -apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
1.3154 -apply (auto dest: field_power_not_zero
1.3155 -        simp add: power_mult_distrib distrib_right power_divide tan_def
1.3156 -                  mult_assoc power_inverse [symmetric])
1.3157 -done
1.3158 +  apply (rule power_inverse [THEN subst])
1.3159 +  apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
1.3160 +  apply (auto dest: field_power_not_zero
1.3161 +          simp add: power_mult_distrib distrib_right power_divide tan_def
1.3162 +                    mult_assoc power_inverse [symmetric])
1.3163 +  done
1.3164
1.3165  lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
1.3166    by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
1.3167 @@ -3096,8 +3309,11 @@
1.3168      by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arcsin_sin)
1.3169    also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
1.3170    proof safe
1.3171 -    fix x :: real assume "x \<in> {-1..1}" then show "x \<in> sin ` {- pi / 2..pi / 2}"
1.3172 -      using arcsin_lbound arcsin_ubound by (intro image_eqI[where x="arcsin x"]) auto
1.3173 +    fix x :: real
1.3174 +    assume "x \<in> {-1..1}"
1.3175 +    then show "x \<in> sin ` {- pi / 2..pi / 2}"
1.3176 +      using arcsin_lbound arcsin_ubound
1.3177 +      by (intro image_eqI[where x="arcsin x"]) auto
1.3178    qed simp
1.3179    finally show ?thesis .
1.3180  qed
1.3181 @@ -3117,8 +3333,11 @@
1.3182      by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arccos_cos)
1.3183    also have "cos ` {0 .. pi} = {-1 .. 1}"
1.3184    proof safe
1.3185 -    fix x :: real assume "x \<in> {-1..1}" then show "x \<in> cos ` {0..pi}"
1.3186 -      using arccos_lbound arccos_ubound by (intro image_eqI[where x="arccos x"]) auto
1.3187 +    fix x :: real
1.3188 +    assume "x \<in> {-1..1}"
1.3189 +    then show "x \<in> cos ` {0..pi}"
1.3190 +      using arccos_lbound arccos_ubound
1.3191 +      by (intro image_eqI[where x="arccos x"]) auto
1.3192    qed simp
1.3193    finally show ?thesis .
1.3194  qed
1.3195 @@ -3133,13 +3352,13 @@
1.3196    by (auto simp: continuous_on_eq_continuous_at subset_eq)
1.3197
1.3198  lemma isCont_arctan: "isCont arctan x"
1.3199 -apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
1.3200 -apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
1.3201 -apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
1.3202 -apply (erule (1) isCont_inverse_function2 [where f=tan])
1.3203 -apply (metis arctan_tan order_le_less_trans order_less_le_trans)
1.3204 -apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
1.3205 -done
1.3206 +  apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
1.3207 +  apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
1.3208 +  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
1.3209 +  apply (erule (1) isCont_inverse_function2 [where f=tan])
1.3210 +  apply (metis arctan_tan order_le_less_trans order_less_le_trans)
1.3211 +  apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
1.3212 +  done
1.3213
1.3214  lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
1.3215    by (rule isCont_tendsto_compose [OF isCont_arctan])
1.3216 @@ -3149,42 +3368,42 @@
1.3217
1.3218  lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
1.3219    unfolding continuous_on_def by (auto intro: tendsto_arctan)
1.3220 -
1.3221 +
1.3222  lemma DERIV_arcsin:
1.3223    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
1.3224 -apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
1.3225 -apply (rule DERIV_cong [OF DERIV_sin])
1.3227 -apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
1.3228 -apply (rule power_strict_mono, simp, simp, simp)
1.3229 -apply assumption
1.3230 -apply assumption
1.3231 -apply simp
1.3232 -apply (erule (1) isCont_arcsin)
1.3233 -done
1.3234 +  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
1.3235 +  apply (rule DERIV_cong [OF DERIV_sin])
1.3236 +  apply (simp add: cos_arcsin)
1.3237 +  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
1.3238 +  apply (rule power_strict_mono, simp, simp, simp)
1.3239 +  apply assumption
1.3240 +  apply assumption
1.3241 +  apply simp
1.3242 +  apply (erule (1) isCont_arcsin)
1.3243 +  done
1.3244
1.3245  lemma DERIV_arccos:
1.3246    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
1.3247 -apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
1.3248 -apply (rule DERIV_cong [OF DERIV_cos])
1.3250 -apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
1.3251 -apply (rule power_strict_mono, simp, simp, simp)
1.3252 -apply assumption
1.3253 -apply assumption
1.3254 -apply simp
1.3255 -apply (erule (1) isCont_arccos)
1.3256 -done
1.3257 +  apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
1.3258 +  apply (rule DERIV_cong [OF DERIV_cos])
1.3259 +  apply (simp add: sin_arccos)
1.3260 +  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
1.3261 +  apply (rule power_strict_mono, simp, simp, simp)
1.3262 +  apply assumption
1.3263 +  apply assumption
1.3264 +  apply simp
1.3265 +  apply (erule (1) isCont_arccos)
1.3266 +  done
1.3267
1.3268  lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
1.3269 -apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
1.3270 -apply (rule DERIV_cong [OF DERIV_tan])
1.3271 -apply (rule cos_arctan_not_zero)
1.3272 -apply (simp add: power_inverse tan_sec [symmetric])
1.3273 -apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
1.3275 -apply (simp, simp, simp, rule isCont_arctan)
1.3276 -done
1.3277 +  apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
1.3278 +  apply (rule DERIV_cong [OF DERIV_tan])
1.3279 +  apply (rule cos_arctan_not_zero)
1.3280 +  apply (simp add: power_inverse tan_sec [symmetric])
1.3281 +  apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
1.3283 +  apply (simp, simp, simp, rule isCont_arctan)
1.3284 +  done
1.3285
1.3286  declare
1.3287    DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.3288 @@ -3203,14 +3422,16 @@
1.3289
1.3290  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
1.3291  proof (rule tendstoI)
1.3292 -  fix e :: real assume "0 < e"
1.3293 +  fix e :: real
1.3294 +  assume "0 < e"
1.3295    def y \<equiv> "pi/2 - min (pi/2) e"
1.3296    then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
1.3297      using `0 < e` by auto
1.3298
1.3299    show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
1.3300    proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
1.3301 -    fix x assume "tan y < x"
1.3302 +    fix x
1.3303 +    assume "tan y < x"
1.3304      then have "arctan (tan y) < arctan x"
1.3306      with y have "y < arctan x"
1.3307 @@ -3222,7 +3443,9 @@
1.3308  qed
1.3309
1.3310  lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
1.3311 -  unfolding filterlim_at_bot_mirror arctan_minus by (intro tendsto_minus tendsto_arctan_at_top)
1.3312 +  unfolding filterlim_at_bot_mirror arctan_minus
1.3313 +  by (intro tendsto_minus tendsto_arctan_at_top)
1.3314 +
1.3315
1.3316  subsection {* More Theorems about Sin and Cos *}
1.3317
1.3318 @@ -3262,28 +3485,28 @@
1.3319  qed
1.3320
1.3321  lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
1.3322 -by (simp add: sin_cos_eq cos_45)
1.3323 +  by (simp add: sin_cos_eq cos_45)
1.3324
1.3325  lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
1.3326 -by (simp add: sin_cos_eq cos_30)
1.3327 +  by (simp add: sin_cos_eq cos_30)
1.3328
1.3329  lemma cos_60: "cos (pi / 3) = 1 / 2"
1.3330 -apply (rule power2_eq_imp_eq)
1.3331 -apply (simp add: cos_squared_eq sin_60 power_divide)
1.3332 -apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
1.3333 -done
1.3334 +  apply (rule power2_eq_imp_eq)
1.3335 +  apply (simp add: cos_squared_eq sin_60 power_divide)
1.3336 +  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
1.3337 +  done
1.3338
1.3339  lemma sin_30: "sin (pi / 6) = 1 / 2"
1.3340 -by (simp add: sin_cos_eq cos_60)
1.3341 +  by (simp add: sin_cos_eq cos_60)
1.3342
1.3343  lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
1.3344 -unfolding tan_def by (simp add: sin_30 cos_30)
1.3345 +  unfolding tan_def by (simp add: sin_30 cos_30)
1.3346
1.3347  lemma tan_45: "tan (pi / 4) = 1"
1.3348 -unfolding tan_def by (simp add: sin_45 cos_45)
1.3349 +  unfolding tan_def by (simp add: sin_45 cos_45)
1.3350
1.3351  lemma tan_60: "tan (pi / 3) = sqrt 3"
1.3352 -unfolding tan_def by (simp add: sin_60 cos_60)
1.3353 +  unfolding tan_def by (simp add: sin_60 cos_60)
1.3354
1.3355  lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
1.3356  proof -
1.3357 @@ -3295,47 +3518,52 @@
1.3358  qed
1.3359
1.3360  lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
1.3363
1.3364  lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
1.3365 -apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
1.3367 -done
1.3368 +  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
1.3369 +  apply (subst cos_add, simp)
1.3370 +  done
1.3371
1.3372  lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
1.3373 -by (auto simp add: mult_assoc)
1.3374 +  by (auto simp add: mult_assoc)
1.3375
1.3376  lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
1.3377 -apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
1.3379 -done
1.3380 +  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
1.3381 +  apply (subst sin_add, simp)
1.3382 +  done
1.3383
1.3384  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
1.3386 -
1.3387 -lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
1.3389 +  apply auto
1.3390 +  done
1.3391 +
1.3392 +lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
1.3393    by (auto intro!: DERIV_intros)
1.3394
1.3395  lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
1.3396 -by (auto simp add: sin_zero_iff even_mult_two_ex)
1.3397 +  by (auto simp add: sin_zero_iff even_mult_two_ex)
1.3398
1.3399  lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
1.3400 -by (cut_tac x = x in sin_cos_squared_add3, auto)
1.3401 +  using sin_cos_squared_add3 [where x = x] by auto
1.3402 +
1.3403
1.3404  subsection {* Machins formula *}
1.3405
1.3406  lemma arctan_one: "arctan 1 = pi / 4"
1.3407    by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
1.3408
1.3409 -lemma tan_total_pi4: assumes "\<bar>x\<bar> < 1"
1.3410 -  shows "\<exists> z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
1.3411 +lemma tan_total_pi4:
1.3412 +  assumes "\<bar>x\<bar> < 1"
1.3413 +  shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
1.3414  proof
1.3415    show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
1.3416      unfolding arctan_one [symmetric] arctan_minus [symmetric]
1.3417      unfolding arctan_less_iff using assms by auto
1.3418  qed
1.3419
1.3420 -lemma arctan_add: assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
1.3422 +  assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
1.3423    shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
1.3424  proof (rule arctan_unique [symmetric])
1.3425    have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
1.3426 @@ -3369,115 +3597,162 @@
1.3427    thus ?thesis unfolding arctan_one by algebra
1.3428  qed
1.3429
1.3430 +
1.3431  subsection {* Introducing the arcus tangens power series *}
1.3432
1.3433 -lemma monoseq_arctan_series: fixes x :: real
1.3434 -  assumes "\<bar>x\<bar> \<le> 1" shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
1.3435 -proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def One_nat_def by auto
1.3436 +lemma monoseq_arctan_series:
1.3437 +  fixes x :: real
1.3438 +  assumes "\<bar>x\<bar> \<le> 1"
1.3439 +  shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
1.3440 +proof (cases "x = 0")
1.3441 +  case True
1.3442 +  thus ?thesis unfolding monoseq_def One_nat_def by auto
1.3443  next
1.3444    case False
1.3445    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
1.3446    show "monoseq ?a"
1.3447    proof -
1.3448 -    { fix n fix x :: real assume "0 \<le> x" and "x \<le> 1"
1.3449 -      have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le> 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
1.3450 +    {
1.3451 +      fix n
1.3452 +      fix x :: real
1.3453 +      assume "0 \<le> x" and "x \<le> 1"
1.3454 +      have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
1.3455 +        1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
1.3456        proof (rule mult_mono)
1.3457 -        show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))" by (rule frac_le) simp_all
1.3458 -        show "0 \<le> 1 / real (Suc (n * 2))" by auto
1.3459 -        show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)" by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
1.3460 -        show "0 \<le> x ^ Suc (Suc n * 2)" by (rule zero_le_power) (simp add: `0 \<le> x`)
1.3461 +        show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
1.3462 +          by (rule frac_le) simp_all
1.3463 +        show "0 \<le> 1 / real (Suc (n * 2))"
1.3464 +          by auto
1.3465 +        show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
1.3466 +          by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
1.3467 +        show "0 \<le> x ^ Suc (Suc n * 2)"
1.3468 +          by (rule zero_le_power) (simp add: `0 \<le> x`)
1.3469        qed
1.3470      } note mono = this
1.3471
1.3472      show ?thesis
1.3473      proof (cases "0 \<le> x")
1.3474        case True from mono[OF this `x \<le> 1`, THEN allI]
1.3475 -      show ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI2)
1.3476 +      show ?thesis unfolding Suc_eq_plus1[symmetric]
1.3477 +        by (rule mono_SucI2)
1.3478      next
1.3479 -      case False hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
1.3480 +      case False
1.3481 +      hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
1.3482        from mono[OF this]
1.3483 -      have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge> 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
1.3484 +      have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
1.3485 +        1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
1.3486        thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
1.3487      qed
1.3488    qed
1.3489  qed
1.3490
1.3491 -lemma zeroseq_arctan_series: fixes x :: real
1.3492 -  assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
1.3493 -proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: tendsto_const)
1.3494 +lemma zeroseq_arctan_series:
1.3495 +  fixes x :: real
1.3496 +  assumes "\<bar>x\<bar> \<le> 1"
1.3497 +  shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
1.3498 +proof (cases "x = 0")
1.3499 +  case True
1.3500 +  thus ?thesis
1.3501 +    unfolding One_nat_def by (auto simp add: tendsto_const)
1.3502  next
1.3503    case False
1.3504    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
1.3505    show "?a ----> 0"
1.3506    proof (cases "\<bar>x\<bar> < 1")
1.3507 -    case True hence "norm x < 1" by auto
1.3508 +    case True
1.3509 +    hence "norm x < 1" by auto
1.3510      from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
1.3511      have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
1.3512        unfolding inverse_eq_divide Suc_eq_plus1 by simp
1.3513      then show ?thesis using pos2 by (rule LIMSEQ_linear)
1.3514    next
1.3515 -    case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
1.3516 -    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
1.3517 +    case False
1.3518 +    hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
1.3519 +    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
1.3520 +      unfolding One_nat_def by auto
1.3521      from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
1.3522      show ?thesis unfolding n_eq Suc_eq_plus1 by auto
1.3523    qed
1.3524  qed
1.3525
1.3526 -lemma summable_arctan_series: fixes x :: real and n :: nat
1.3527 -  assumes "\<bar>x\<bar> \<le> 1" shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "summable (?c x)")
1.3528 +lemma summable_arctan_series:
1.3529 +  fixes x :: real and n :: nat
1.3530 +  assumes "\<bar>x\<bar> \<le> 1"
1.3531 +  shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
1.3532 +  (is "summable (?c x)")
1.3533    by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
1.3534
1.3535 -lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x\<^sup>2 < 1"
1.3536 +lemma less_one_imp_sqr_less_one:
1.3537 +  fixes x :: real
1.3538 +  assumes "\<bar>x\<bar> < 1"
1.3539 +  shows "x\<^sup>2 < 1"
1.3540  proof -
1.3541    from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
1.3542    have "\<bar>x\<^sup>2\<bar> < 1" using `\<bar>x\<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
1.3543    thus ?thesis using zero_le_power2 by auto
1.3544  qed
1.3545
1.3546 -lemma DERIV_arctan_series: assumes "\<bar> x \<bar> < 1"
1.3547 -  shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))" (is "DERIV ?arctan _ :> ?Int")
1.3548 +lemma DERIV_arctan_series:
1.3549 +  assumes "\<bar> x \<bar> < 1"
1.3550 +  shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))"
1.3551 +  (is "DERIV ?arctan _ :> ?Int")
1.3552  proof -
1.3553 -  let "?f n" = "if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
1.3554 -
1.3555 -  { fix n :: nat assume "even n" hence "2 * (n div 2) = n" by presburger } note n_even=this
1.3556 -  have if_eq: "\<And> n x'. ?f n * real (Suc n) * x'^n = (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)" using n_even by auto
1.3557 -
1.3558 -  { fix x :: real assume "\<bar>x\<bar> < 1" hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
1.3559 +  let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
1.3560 +
1.3561 +  have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
1.3562 +    by presburger
1.3563 +  then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
1.3564 +    (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
1.3565 +    by auto
1.3566 +
1.3567 +  {
1.3568 +    fix x :: real
1.3569 +    assume "\<bar>x\<bar> < 1"
1.3570 +    hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
1.3571      have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
1.3572        by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
1.3573      hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
1.3574    } note summable_Integral = this
1.3575
1.3576 -  { fix f :: "nat \<Rightarrow> real"
1.3577 -    have "\<And> x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
1.3578 +  {
1.3579 +    fix f :: "nat \<Rightarrow> real"
1.3580 +    have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
1.3581      proof
1.3582 -      fix x :: real assume "f sums x"
1.3583 +      fix x :: real
1.3584 +      assume "f sums x"
1.3585        from sums_if[OF sums_zero this]
1.3586 -      show "(\<lambda> n. if even n then f (n div 2) else 0) sums x" by auto
1.3587 +      show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
1.3588 +        by auto
1.3589      next
1.3590 -      fix x :: real assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
1.3591 +      fix x :: real
1.3592 +      assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
1.3593        from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult_commute]]
1.3594        show "f sums x" unfolding sums_def by auto
1.3595      qed
1.3596      hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
1.3597    } note sums_even = this
1.3598
1.3599 -  have Int_eq: "(\<Sum> n. ?f n * real (Suc n) * x^n) = ?Int" unfolding if_eq mult_commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
1.3600 +  have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
1.3601 +    unfolding if_eq mult_commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
1.3602      by auto
1.3603
1.3604 -  { fix x :: real
1.3605 -    have if_eq': "\<And> n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
1.3606 +  {
1.3607 +    fix x :: real
1.3608 +    have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
1.3609        (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
1.3610        using n_even by auto
1.3611 -    have idx_eq: "\<And> n. n * 2 + 1 = Suc (2 * n)" by auto
1.3612 -    have "(\<Sum> n. ?f n * x^(Suc n)) = ?arctan x" unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
1.3613 +    have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
1.3614 +    have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
1.3615 +      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
1.3616        by auto
1.3617    } note arctan_eq = this
1.3618
1.3619    have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
1.3620    proof (rule DERIV_power_series')
1.3621      show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
1.3622 -    { fix x' :: real assume x'_bounds: "x' \<in> {- 1 <..< 1}"
1.3623 +    {
1.3624 +      fix x' :: real
1.3625 +      assume x'_bounds: "x' \<in> {- 1 <..< 1}"
1.3626        hence "\<bar>x'\<bar> < 1" by auto
1.3627
1.3628        let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
1.3629 @@ -3488,101 +3763,145 @@
1.3630    thus ?thesis unfolding Int_eq arctan_eq .
1.3631  qed
1.3632
1.3633 -lemma arctan_series: assumes "\<bar> x \<bar> \<le> 1"
1.3634 -  shows "arctan x = (\<Sum> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "_ = suminf (\<lambda> n. ?c x n)")
1.3635 +lemma arctan_series:
1.3636 +  assumes "\<bar> x \<bar> \<le> 1"
1.3637 +  shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
1.3638 +  (is "_ = suminf (\<lambda> n. ?c x n)")
1.3639  proof -
1.3640 -  let "?c' x n" = "(-1)^n * x^(n*2)"
1.3641 -
1.3642 -  { fix r x :: real assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
1.3643 +  let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
1.3644 +
1.3645 +  {
1.3646 +    fix r x :: real
1.3647 +    assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
1.3648      have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
1.3649 -    from DERIV_arctan_series[OF this]
1.3650 -    have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
1.3651 +    from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
1.3652    } note DERIV_arctan_suminf = this
1.3653
1.3654 -  { fix x :: real assume "\<bar>x\<bar> \<le> 1" note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] }
1.3655 -  note arctan_series_borders = this
1.3656 -
1.3657 -  { fix x :: real assume "\<bar>x\<bar> < 1" have "arctan x = (\<Sum> k. ?c x k)"
1.3658 -  proof -
1.3659 -    obtain r where "\<bar>x\<bar> < r" and "r < 1" using dense[OF `\<bar>x\<bar> < 1`] by blast
1.3660 -    hence "0 < r" and "-r < x" and "x < r" by auto
1.3661 -
1.3662 -    have suminf_eq_arctan_bounded: "\<And> x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> suminf (?c x) - arctan x = suminf (?c a) - arctan a"
1.3663 +  {
1.3664 +    fix x :: real
1.3665 +    assume "\<bar>x\<bar> \<le> 1"
1.3666 +    note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
1.3667 +  } note arctan_series_borders = this
1.3668 +
1.3669 +  {
1.3670 +    fix x :: real
1.3671 +    assume "\<bar>x\<bar> < 1"
1.3672 +    have "arctan x = (\<Sum>k. ?c x k)"
1.3673      proof -
1.3674 -      fix x a b assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
1.3675 -      hence "\<bar>x\<bar> < r" by auto
1.3676 -      show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
1.3677 -      proof (rule DERIV_isconst2[of "a" "b"])
1.3678 -        show "a < b" and "a \<le> x" and "x \<le> b" using `a < b` `a \<le> x` `x \<le> b` by auto
1.3679 -        have "\<forall> x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
1.3680 -        proof (rule allI, rule impI)
1.3681 -          fix x assume "-r < x \<and> x < r" hence "\<bar>x\<bar> < r" by auto
1.3682 -          hence "\<bar>x\<bar> < 1" using `r < 1` by auto
1.3683 -          have "\<bar> - (x\<^sup>2) \<bar> < 1" using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
1.3684 -          hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums)
1.3685 -          hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto
1.3686 -          hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto
1.3687 -          have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))" unfolding suminf_c'_eq_geom
1.3688 -            by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
1.3689 -          from DERIV_add_minus[OF this DERIV_arctan]
1.3690 -          show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" unfolding diff_minus by auto
1.3691 +      obtain r where "\<bar>x\<bar> < r" and "r < 1"
1.3692 +        using dense[OF `\<bar>x\<bar> < 1`] by blast
1.3693 +      hence "0 < r" and "-r < x" and "x < r" by auto
1.3694 +
1.3695 +      have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
1.3696 +        suminf (?c x) - arctan x = suminf (?c a) - arctan a"
1.3697 +      proof -
1.3698 +        fix x a b
1.3699 +        assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
1.3700 +        hence "\<bar>x\<bar> < r" by auto
1.3701 +        show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
1.3702 +        proof (rule DERIV_isconst2[of "a" "b"])
1.3703 +          show "a < b" and "a \<le> x" and "x \<le> b"
1.3704 +            using `a < b` `a \<le> x` `x \<le> b` by auto
1.3705 +          have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
1.3706 +          proof (rule allI, rule impI)
1.3707 +            fix x
1.3708 +            assume "-r < x \<and> x < r"
1.3709 +            hence "\<bar>x\<bar> < r" by auto
1.3710 +            hence "\<bar>x\<bar> < 1" using `r < 1` by auto
1.3711 +            have "\<bar> - (x\<^sup>2) \<bar> < 1"
1.3712 +              using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
1.3713 +            hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
1.3714 +              unfolding real_norm_def[symmetric] by (rule geometric_sums)
1.3715 +            hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
1.3716 +              unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto
1.3717 +            hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
1.3718 +              using sums_unique unfolding inverse_eq_divide by auto
1.3719 +            have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
1.3720 +              unfolding suminf_c'_eq_geom
1.3721 +              by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
1.3722 +            from DERIV_add_minus[OF this DERIV_arctan]
1.3723 +            show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
1.3724 +              unfolding diff_minus by auto
1.3725 +          qed
1.3726 +          hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
1.3727 +            using `-r < a` `b < r` by auto
1.3728 +          thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
1.3729 +            using `\<bar>x\<bar> < r` by auto
1.3730 +          show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
1.3731 +            using DERIV_in_rball DERIV_isCont by auto
1.3732          qed
1.3733 -        hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0" using `-r < a` `b < r` by auto
1.3734 -        thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0" using `\<bar>x\<bar> < r` by auto
1.3735 -        show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y" using DERIV_in_rball DERIV_isCont by auto
1.3736        qed
1.3737 +
1.3738 +      have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
1.3739 +        unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
1.3740 +        by auto
1.3741 +
1.3742 +      have "suminf (?c x) - arctan x = 0"
1.3743 +      proof (cases "x = 0")
1.3744 +        case True
1.3745 +        thus ?thesis using suminf_arctan_zero by auto
1.3746 +      next
1.3747 +        case False
1.3748 +        hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
1.3749 +        have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
1.3750 +          by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
1.3751 +            (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
1.3752 +        moreover
1.3753 +        have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
1.3754 +          by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
1.3755 +            (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
1.3756 +        ultimately
1.3757 +        show ?thesis using suminf_arctan_zero by auto
1.3758 +      qed
1.3759 +      thus ?thesis by auto
1.3760      qed
1.3761 -
1.3762 -    have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
1.3763 -      unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
1.3764 -
1.3765 -    have "suminf (?c x) - arctan x = 0"
1.3766 -    proof (cases "x = 0")
1.3767 -      case True thus ?thesis using suminf_arctan_zero by auto
1.3768 -    next
1.3769 -      case False hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
1.3770 -      have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
1.3771 -        by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
1.3772 -          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
1.3773 -      moreover
1.3774 -      have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
1.3775 -        by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
1.3776 -          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
1.3777 -      ultimately
1.3778 -      show ?thesis using suminf_arctan_zero by auto
1.3779 -    qed
1.3780 -    thus ?thesis by auto
1.3781 -  qed } note when_less_one = this
1.3782 +  } note when_less_one = this
1.3783
1.3784    show "arctan x = suminf (\<lambda> n. ?c x n)"
1.3785    proof (cases "\<bar>x\<bar> < 1")
1.3786 -    case True thus ?thesis by (rule when_less_one)
1.3787 -  next case False hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
1.3788 -    let "?a x n" = "\<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
1.3789 -    let "?diff x n" = "\<bar> arctan x - (\<Sum> i = 0..<n. ?c x i)\<bar>"
1.3790 -    { fix n :: nat
1.3791 +    case True
1.3792 +    thus ?thesis by (rule when_less_one)
1.3793 +  next
1.3794 +    case False
1.3795 +    hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
1.3796 +    let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
1.3797 +    let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i = 0..<n. ?c x i)\<bar>"
1.3798 +    {
1.3799 +      fix n :: nat
1.3800        have "0 < (1 :: real)" by auto
1.3801        moreover
1.3802 -      { fix x :: real assume "0 < x" and "x < 1" hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
1.3803 -        from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)" by auto
1.3804 +      {
1.3805 +        fix x :: real
1.3806 +        assume "0 < x" and "x < 1"
1.3807 +        hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
1.3808 +        from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
1.3809 +          by auto
1.3810          note bounds = mp[OF arctan_series_borders(2)[OF `\<bar>x\<bar> \<le> 1`] this, unfolded when_less_one[OF `\<bar>x\<bar> < 1`, symmetric], THEN spec]
1.3811 -        have "0 < 1 / real (n*2+1) * x^(n*2+1)" by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
1.3812 -        hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)" by (rule abs_of_pos)
1.3813 +        have "0 < 1 / real (n*2+1) * x^(n*2+1)"
1.3814 +          by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
1.3815 +        hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
1.3816 +          by (rule abs_of_pos)
1.3817          have "?diff x n \<le> ?a x n"
1.3818          proof (cases "even n")
1.3819 -          case True hence sgn_pos: "(-1)^n = (1::real)" by auto
1.3820 -          from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
1.3821 +          case True
1.3822 +          hence sgn_pos: "(-1)^n = (1::real)" by auto
1.3823 +          from `even n` obtain m where "2 * m = n"
1.3824 +            unfolding even_mult_two_ex by auto
1.3825            from bounds[of m, unfolded this atLeastAtMost_iff]
1.3826 -          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))" by auto
1.3827 +          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))"
1.3828 +            by auto
1.3829            also have "\<dots> = ?c x n" unfolding One_nat_def by auto
1.3830            also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
1.3831            finally show ?thesis .
1.3832          next
1.3833 -          case False hence sgn_neg: "(-1)^n = (-1::real)" by auto
1.3834 -          from `odd n` obtain m where m_def: "2 * m + 1 = n" unfolding odd_Suc_mult_two_ex by auto
1.3835 +          case False
1.3836 +          hence sgn_neg: "(-1)^n = (-1::real)" by auto
1.3837 +          from `odd n` obtain m where m_def: "2 * m + 1 = n"
1.3838 +            unfolding odd_Suc_mult_two_ex by auto
1.3839            hence m_plus: "2 * (m + 1) = n + 1" by auto
1.3840            from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
1.3841 -          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))" by auto
1.3842 +          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))"
1.3843 +            by auto
1.3844            also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
1.3845            also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
1.3846            finally show ?thesis .
1.3847 @@ -3592,8 +3911,10 @@
1.3848        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
1.3849        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
1.3850          unfolding diff_minus divide_inverse
1.3851 -        by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
1.3852 -      ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
1.3853 +        by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
1.3854 +          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
1.3855 +      ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
1.3856 +        by (rule LIM_less_bound)
1.3857        hence "?diff 1 n \<le> ?a 1 n" by auto
1.3858      }
1.3859      have "?a 1 ----> 0"
1.3860 @@ -3601,10 +3922,15 @@
1.3861        by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
1.3862      have "?diff 1 ----> 0"
1.3863      proof (rule LIMSEQ_I)
1.3864 -      fix r :: real assume "0 < r"
1.3865 -      obtain N :: nat where N_I: "\<And> n. N \<le> n \<Longrightarrow> ?a 1 n < r" using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
1.3866 -      { fix n assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
1.3867 -        have "norm (?diff 1 n - 0) < r" by auto }
1.3868 +      fix r :: real
1.3869 +      assume "0 < r"
1.3870 +      obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
1.3871 +        using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
1.3872 +      {
1.3873 +        fix n
1.3874 +        assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
1.3875 +        have "norm (?diff 1 n - 0) < r" by auto
1.3876 +      }
1.3877        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
1.3878      qed
1.3879      from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
1.3880 @@ -3612,62 +3938,91 @@
1.3881      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
1.3882
1.3883      show ?thesis
1.3884 -    proof (cases "x = 1", simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
1.3885 -      assume "x \<noteq> 1" hence "x = -1" using `\<bar>x\<bar> = 1` by auto
1.3886 +    proof (cases "x = 1")
1.3887 +      case True
1.3888 +      then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
1.3889 +    next
1.3890 +      case False
1.3891 +      hence "x = -1" using `\<bar>x\<bar> = 1` by auto
1.3892
1.3893        have "- (pi / 2) < 0" using pi_gt_zero by auto
1.3894        have "- (2 * pi) < 0" using pi_gt_zero by auto
1.3895
1.3896 -      have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
1.3897 -
1.3898 -      have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
1.3899 -      also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
1.3900 -      also have "\<dots> = - (arctan (tan (pi / 4)))" unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
1.3901 -      also have "\<dots> = - (arctan 1)" unfolding tan_45 ..
1.3902 -      also have "\<dots> = - (\<Sum> i. ?c 1 i)" using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
1.3903 -      also have "\<dots> = (\<Sum> i. ?c (- 1) i)" using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]] unfolding c_minus_minus by auto
1.3904 +      have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
1.3905 +        unfolding One_nat_def by auto
1.3906 +
1.3907 +      have "arctan (- 1) = arctan (tan (-(pi / 4)))"
1.3908 +        unfolding tan_45 tan_minus ..
1.3909 +      also have "\<dots> = - (pi / 4)"
1.3910 +        by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
1.3911 +      also have "\<dots> = - (arctan (tan (pi / 4)))"
1.3912 +        unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
1.3913 +      also have "\<dots> = - (arctan 1)"
1.3914 +        unfolding tan_45 ..
1.3915 +      also have "\<dots> = - (\<Sum> i. ?c 1 i)"
1.3916 +        using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
1.3917 +      also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
1.3918 +        using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
1.3919 +        unfolding c_minus_minus by auto
1.3920        finally show ?thesis using `x = -1` by auto
1.3921      qed
1.3922    qed
1.3923  qed
1.3924
1.3925 -lemma arctan_half: fixes x :: real
1.3926 +lemma arctan_half:
1.3927 +  fixes x :: real
1.3928    shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
1.3929  proof -
1.3930 -  obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x" using tan_total by blast
1.3931 -  hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto
1.3932 -
1.3933 -  have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)" by auto
1.3934 +  obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
1.3935 +    using tan_total by blast
1.3936 +  hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
1.3937 +    by auto
1.3938 +
1.3939 +  have divide_nonzero_divide: "\<And>A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)"
1.3940 +    by auto
1.3941
1.3942    have "0 < cos y" using cos_gt_zero_pi[OF low high] .
1.3943 -  hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y" by auto
1.3944 -
1.3945 -  have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2" unfolding tan_def power_divide ..
1.3946 -  also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2" using `cos y \<noteq> 0` by auto
1.3947 -  also have "\<dots> = 1 / (cos y)\<^sup>2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
1.3948 +  hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
1.3949 +    by auto
1.3950 +
1.3951 +  have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
1.3952 +    unfolding tan_def power_divide ..
1.3953 +  also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
1.3954 +    using `cos y \<noteq> 0` by auto
1.3955 +  also have "\<dots> = 1 / (cos y)\<^sup>2"
1.3957    finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
1.3958
1.3959 -  have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)" unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
1.3960 -  also have "\<dots> = tan y / (1 + 1 / cos y)" using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
1.3961 -  also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))" unfolding cos_sqrt ..
1.3962 -  also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))" unfolding real_sqrt_divide by auto
1.3963 -  finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))" unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
1.3964 -
1.3965 -  have "arctan x = y" using arctan_tan low high y_eq by auto
1.3966 -  also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto
1.3967 -  also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half by auto
1.3968 -  finally show ?thesis unfolding eq `tan y = x` .
1.3969 +  have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
1.3970 +    unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
1.3971 +  also have "\<dots> = tan y / (1 + 1 / cos y)"
1.3972 +    using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
1.3973 +  also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
1.3974 +    unfolding cos_sqrt ..
1.3975 +  also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
1.3976 +    unfolding real_sqrt_divide by auto
1.3977 +  finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
1.3978 +    unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
1.3979 +
1.3980 +  have "arctan x = y"
1.3981 +    using arctan_tan low high y_eq by auto
1.3982 +  also have "\<dots> = 2 * (arctan (tan (y/2)))"
1.3983 +    using arctan_tan[OF low2 high2] by auto
1.3984 +  also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
1.3985 +    unfolding tan_half by auto
1.3986 +  finally show ?thesis
1.3987 +    unfolding eq `tan y = x` .
1.3988  qed
1.3989
1.3990 -lemma arctan_monotone: assumes "x < y"
1.3991 -  shows "arctan x < arctan y"
1.3992 -  using assms by (simp only: arctan_less_iff)
1.3993 -
1.3994 -lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y"
1.3995 -  using assms by (simp only: arctan_le_iff)
1.3996 +lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
1.3997 +  by (simp only: arctan_less_iff)
1.3998 +
1.3999 +lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
1.4000 +  by (simp only: arctan_le_iff)
1.4001
1.4002  lemma arctan_inverse:
1.4003 -  assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
1.4004 +  assumes "x \<noteq> 0"
1.4005 +  shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
1.4006  proof (rule arctan_unique)
1.4007    show "- (pi / 2) < sgn x * pi / 2 - arctan x"
1.4008      using arctan_bounded [of x] assms
1.4009 @@ -3693,45 +4048,46 @@
1.4010    finally show ?thesis by auto
1.4011  qed
1.4012
1.4013 +
1.4014  subsection {* Existence of Polar Coordinates *}
1.4015
1.4016  lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
1.4017 -apply (rule power2_le_imp_le [OF _ zero_le_one])
1.4018 -apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
1.4019 -done
1.4020 +  apply (rule power2_le_imp_le [OF _ zero_le_one])
1.4021 +  apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
1.4022 +  done
1.4023
1.4024  lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
1.4026 +  by (simp add: abs_le_iff)
1.4027
1.4028  lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
1.4029 -by (simp add: sin_arccos abs_le_iff)
1.4030 +  by (simp add: sin_arccos abs_le_iff)
1.4031
1.4032  lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
1.4033
1.4034  lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
1.4035
1.4036 -lemma polar_ex1:
1.4037 -     "0 < y ==> \<exists>r a. x = r * cos a & y = r * sin a"
1.4038 -apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
1.4039 -apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
1.4043 -apply (simp add: real_sqrt_mult [symmetric])
1.4045 -done
1.4046 -
1.4047 -lemma polar_ex2:
1.4048 -     "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
1.4049 -apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify)
1.4050 -apply (metis cos_minus minus_minus minus_mult_right sin_minus)
1.4051 -done
1.4052 +lemma polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
1.4053 +  apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
1.4054 +  apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
1.4055 +  apply (simp add: cos_arccos_lemma1)
1.4056 +  apply (simp add: sin_arccos_lemma1)
1.4057 +  apply (simp add: power_divide)
1.4058 +  apply (simp add: real_sqrt_mult [symmetric])
1.4059 +  apply (simp add: right_diff_distrib)
1.4060 +  done
1.4061 +
1.4062 +lemma polar_ex2: "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
1.4063 +  using polar_ex1 [where x=x and y="-y"]
1.4064 +  apply simp
1.4065 +  apply clarify
1.4066 +  apply (metis cos_minus minus_minus minus_mult_right sin_minus)
1.4067 +  done
1.4068
1.4069  lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
1.4070 -apply (rule_tac x=0 and y=y in linorder_cases)
1.4071 -apply (erule polar_ex1)
1.4072 -apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
1.4073 -apply (erule polar_ex2)
1.4074 -done
1.4075 +  apply (rule_tac x=0 and y=y in linorder_cases)
1.4076 +  apply (erule polar_ex1)
1.4077 +  apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
1.4078 +  apply (erule polar_ex2)
1.4079 +  done
1.4080
1.4081  end
```