src/HOL/Transcendental.thy
author haftmann
Sun Oct 19 18:05:26 2014 +0200 (2014-10-19)
changeset 58709 efdc6c533bd3
parent 58656 7f14d5d9b933
child 58710 7216a10d69ba
permissions -rw-r--r--
prefer generic elimination rules for even/odd over specialized unfold rules for nat
     1 (*  Title:      HOL/Transcendental.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4     Author:     Jeremy Avigad
     5 *)
     6 
     7 header{*Power Series, Transcendental Functions etc.*}
     8 
     9 theory Transcendental
    10 imports Fact Series Deriv NthRoot
    11 begin
    12 
    13 lemma root_test_convergence:
    14   fixes f :: "nat \<Rightarrow> 'a::banach"
    15   assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
    16   assumes "x < 1"
    17   shows "summable f"
    18 proof -
    19   have "0 \<le> x"
    20     by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
    21   from `x < 1` obtain z where z: "x < z" "z < 1"
    22     by (metis dense)
    23   from f `x < z`
    24   have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
    25     by (rule order_tendstoD)
    26   then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
    27     using eventually_ge_at_top
    28   proof eventually_elim
    29     fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
    30     from power_strict_mono[OF less, of n] n
    31     show "norm (f n) \<le> z ^ n"
    32       by simp
    33   qed
    34   then show "summable f"
    35     unfolding eventually_sequentially
    36     using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
    37 qed
    38 
    39 subsection {* Properties of Power Series *}
    40 
    41 lemma lemma_realpow_diff:
    42   fixes y :: "'a::monoid_mult"
    43   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
    44 proof -
    45   assume "p \<le> n"
    46   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
    47   thus ?thesis by (simp add: power_commutes)
    48 qed
    49 
    50 lemma lemma_realpow_diff_sumr2:
    51   fixes y :: "'a::{comm_ring,monoid_mult}"
    52   shows
    53     "x ^ (Suc n) - y ^ (Suc n) =
    54       (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    55 proof (induct n)
    56   case (Suc n)
    57   have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    58     by simp
    59   also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    60     by (simp add: algebra_simps)
    61   also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    62     by (simp only: Suc)
    63   also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    64     by (simp only: mult.left_commute)
    65   also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    66     by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    67   finally show ?case .
    68 qed simp
    69 
    70 corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
    71   fixes x :: "'a::{comm_ring,monoid_mult}"
    72   shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
    73 using lemma_realpow_diff_sumr2[of x "n - 1" y]
    74 by (cases "n = 0") (simp_all add: field_simps)
    75 
    76 lemma lemma_realpow_rev_sumr:
    77    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
    78     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
    79   by (subst nat_diff_setsum_reindex[symmetric]) simp
    80 
    81 lemma power_diff_1_eq:
    82   fixes x :: "'a::{comm_ring,monoid_mult}"
    83   shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
    84 using lemma_realpow_diff_sumr2 [of x _ 1] 
    85   by (cases n) auto
    86 
    87 lemma one_diff_power_eq':
    88   fixes x :: "'a::{comm_ring,monoid_mult}"
    89   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
    90 using lemma_realpow_diff_sumr2 [of 1 _ x] 
    91   by (cases n) auto
    92 
    93 lemma one_diff_power_eq:
    94   fixes x :: "'a::{comm_ring,monoid_mult}"
    95   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
    96 by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
    97 
    98 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    99   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
   100 
   101 lemma powser_insidea:
   102   fixes x z :: "'a::real_normed_div_algebra"
   103   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
   104     and 2: "norm z < norm x"
   105   shows "summable (\<lambda>n. norm (f n * z ^ n))"
   106 proof -
   107   from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
   108   from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
   109     by (rule summable_LIMSEQ_zero)
   110   hence "convergent (\<lambda>n. f n * x ^ n)"
   111     by (rule convergentI)
   112   hence "Cauchy (\<lambda>n. f n * x ^ n)"
   113     by (rule convergent_Cauchy)
   114   hence "Bseq (\<lambda>n. f n * x ^ n)"
   115     by (rule Cauchy_Bseq)
   116   then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
   117     by (simp add: Bseq_def, safe)
   118   have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
   119                    K * norm (z ^ n) * inverse (norm (x ^ n))"
   120   proof (intro exI allI impI)
   121     fix n::nat
   122     assume "0 \<le> n"
   123     have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
   124           norm (f n * x ^ n) * norm (z ^ n)"
   125       by (simp add: norm_mult abs_mult)
   126     also have "\<dots> \<le> K * norm (z ^ n)"
   127       by (simp only: mult_right_mono 4 norm_ge_zero)
   128     also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
   129       by (simp add: x_neq_0)
   130     also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
   131       by (simp only: mult.assoc)
   132     finally show "norm (norm (f n * z ^ n)) \<le>
   133                   K * norm (z ^ n) * inverse (norm (x ^ n))"
   134       by (simp add: mult_le_cancel_right x_neq_0)
   135   qed
   136   moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   137   proof -
   138     from 2 have "norm (norm (z * inverse x)) < 1"
   139       using x_neq_0
   140       by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
   141     hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
   142       by (rule summable_geometric)
   143     hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
   144       by (rule summable_mult)
   145     thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   146       using x_neq_0
   147       by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
   148                     power_inverse norm_power mult.assoc)
   149   qed
   150   ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
   151     by (rule summable_comparison_test)
   152 qed
   153 
   154 lemma powser_inside:
   155   fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   156   shows
   157     "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
   158       summable (\<lambda>n. f n * (z ^ n))"
   159   by (rule powser_insidea [THEN summable_norm_cancel])
   160 
   161 lemma sum_split_even_odd:
   162   fixes f :: "nat \<Rightarrow> real"
   163   shows
   164     "(\<Sum>i<2 * n. if even i then f i else g i) =
   165      (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1))"
   166 proof (induct n)
   167   case 0
   168   then show ?case by simp
   169 next
   170   case (Suc n)
   171   have "(\<Sum>i<2 * Suc n. if even i then f i else g i) =
   172     (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
   173     using Suc.hyps unfolding One_nat_def by auto
   174   also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))"
   175     by auto
   176   finally show ?case .
   177 qed
   178 
   179 lemma sums_if':
   180   fixes g :: "nat \<Rightarrow> real"
   181   assumes "g sums x"
   182   shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   183   unfolding sums_def
   184 proof (rule LIMSEQ_I)
   185   fix r :: real
   186   assume "0 < r"
   187   from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
   188   obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n} - x) < r)" by blast
   189 
   190   let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i - 1) div 2)"
   191   {
   192     fix m
   193     assume "m \<ge> 2 * no"
   194     hence "m div 2 \<ge> no" by auto
   195     have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}"
   196       using sum_split_even_odd by auto
   197     hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
   198       using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
   199     moreover
   200     have "?SUM (2 * (m div 2)) = ?SUM m"
   201     proof (cases "even m")
   202       case True
   203       show ?thesis
   204         unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
   205     next
   206       case False
   207       hence "even (Suc m)" by auto
   208       from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
   209         odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
   210       have eq: "Suc (2 * (m div 2)) = m" by auto
   211       hence "even (2 * (m div 2))" using `odd m` by auto
   212       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
   213       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
   214       finally show ?thesis by auto
   215     qed
   216     ultimately have "(norm (?SUM m - x) < r)" by auto
   217   }
   218   thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
   219 qed
   220 
   221 lemma sums_if:
   222   fixes g :: "nat \<Rightarrow> real"
   223   assumes "g sums x" and "f sums y"
   224   shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
   225 proof -
   226   let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
   227   {
   228     fix B T E
   229     have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
   230       by (cases B) auto
   231   } note if_sum = this
   232   have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   233     using sums_if'[OF `g sums x`] .
   234   {
   235     have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
   236 
   237     have "?s sums y" using sums_if'[OF `f sums y`] .
   238     from this[unfolded sums_def, THEN LIMSEQ_Suc]
   239     have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
   240       by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
   241   }
   242   from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
   243 qed
   244 
   245 subsection {* Alternating series test / Leibniz formula *}
   246 
   247 lemma sums_alternating_upper_lower:
   248   fixes a :: "nat \<Rightarrow> real"
   249   assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
   250   shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
   251              ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
   252   (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
   253 proof (rule nested_sequence_unique)
   254   have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
   255 
   256   show "\<forall>n. ?f n \<le> ?f (Suc n)"
   257   proof
   258     fix n
   259     show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto
   260   qed
   261   show "\<forall>n. ?g (Suc n) \<le> ?g n"
   262   proof
   263     fix n
   264     show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
   265       unfolding One_nat_def by auto
   266   qed
   267   show "\<forall>n. ?f n \<le> ?g n"
   268   proof
   269     fix n
   270     show "?f n \<le> ?g n" using fg_diff a_pos
   271       unfolding One_nat_def by auto
   272   qed
   273   show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
   274   proof (rule LIMSEQ_I)
   275     fix r :: real
   276     assume "0 < r"
   277     with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
   278       by auto
   279     hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   280     thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   281   qed
   282 qed
   283 
   284 lemma summable_Leibniz':
   285   fixes a :: "nat \<Rightarrow> real"
   286   assumes a_zero: "a ----> 0"
   287     and a_pos: "\<And> n. 0 \<le> a n"
   288     and a_monotone: "\<And> n. a (Suc n) \<le> a n"
   289   shows summable: "summable (\<lambda> n. (-1)^n * a n)"
   290     and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
   291     and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   292     and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
   293     and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   294 proof -
   295   let ?S = "\<lambda>n. (-1)^n * a n"
   296   let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
   297   let ?f = "\<lambda>n. ?P (2 * n)"
   298   let ?g = "\<lambda>n. ?P (2 * n + 1)"
   299   obtain l :: real
   300     where below_l: "\<forall> n. ?f n \<le> l"
   301       and "?f ----> l"
   302       and above_l: "\<forall> n. l \<le> ?g n"
   303       and "?g ----> l"
   304     using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
   305 
   306   let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
   307   have "?Sa ----> l"
   308   proof (rule LIMSEQ_I)
   309     fix r :: real
   310     assume "0 < r"
   311     with `?f ----> l`[THEN LIMSEQ_D]
   312     obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
   313 
   314     from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
   315     obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
   316 
   317     {
   318       fix n :: nat
   319       assume "n \<ge> (max (2 * f_no) (2 * g_no))"
   320       hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
   321       have "norm (?Sa n - l) < r"
   322       proof (cases "even n")
   323         case True
   324         from even_nat_div_two_times_two[OF this]
   325         have n_eq: "2 * (n div 2) = n"
   326           unfolding numeral_2_eq_2[symmetric] by auto
   327         with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
   328           by auto
   329         from f[OF this] show ?thesis
   330           unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
   331       next
   332         case False
   333         hence "even (n - 1)" by simp
   334         from even_nat_div_two_times_two[OF this]
   335         have n_eq: "2 * ((n - 1) div 2) = n - 1"
   336           unfolding numeral_2_eq_2[symmetric] by auto
   337         hence range_eq: "n - 1 + 1 = n"
   338           using odd_pos[OF False] by auto
   339 
   340         from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
   341           by auto
   342         from g[OF this] show ?thesis
   343           unfolding n_eq range_eq .
   344       qed
   345     }
   346     thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
   347   qed
   348   hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
   349     unfolding sums_def .
   350   thus "summable ?S" using summable_def by auto
   351 
   352   have "l = suminf ?S" using sums_unique[OF sums_l] .
   353 
   354   fix n
   355   show "suminf ?S \<le> ?g n"
   356     unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
   357   show "?f n \<le> suminf ?S"
   358     unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
   359   show "?g ----> suminf ?S"
   360     using `?g ----> l` `l = suminf ?S` by auto
   361   show "?f ----> suminf ?S"
   362     using `?f ----> l` `l = suminf ?S` by auto
   363 qed
   364 
   365 theorem summable_Leibniz:
   366   fixes a :: "nat \<Rightarrow> real"
   367   assumes a_zero: "a ----> 0" and "monoseq a"
   368   shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
   369     and "0 < a 0 \<longrightarrow>
   370       (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
   371     and "a 0 < 0 \<longrightarrow>
   372       (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
   373     and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
   374     and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
   375 proof -
   376   have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   377   proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
   378     case True
   379     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n"
   380       by auto
   381     {
   382       fix n
   383       have "a (Suc n) \<le> a n"
   384         using ord[where n="Suc n" and m=n] by auto
   385     } note mono = this
   386     note leibniz = summable_Leibniz'[OF `a ----> 0` ge0]
   387     from leibniz[OF mono]
   388     show ?thesis using `0 \<le> a 0` by auto
   389   next
   390     let ?a = "\<lambda> n. - a n"
   391     case False
   392     with monoseq_le[OF `monoseq a` `a ----> 0`]
   393     have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
   394     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
   395       by auto
   396     {
   397       fix n
   398       have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n]
   399         by auto
   400     } note monotone = this
   401     note leibniz =
   402       summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
   403         OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
   404     have "summable (\<lambda> n. (-1)^n * ?a n)"
   405       using leibniz(1) by auto
   406     then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
   407       unfolding summable_def by auto
   408     from this[THEN sums_minus] have "(\<lambda> n. (-1)^n * a n) sums -l"
   409       by auto
   410     hence ?summable unfolding summable_def by auto
   411     moreover
   412     have "\<And>a b :: real. \<bar>- a - - b\<bar> = \<bar>a - b\<bar>"
   413       unfolding minus_diff_minus by auto
   414 
   415     from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
   416     have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
   417       by auto
   418 
   419     have ?pos using `0 \<le> ?a 0` by auto
   420     moreover have ?neg
   421       using leibniz(2,4)
   422       unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le
   423       by auto
   424     moreover have ?f and ?g
   425       using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel]
   426       by auto
   427     ultimately show ?thesis by auto
   428   qed
   429   then show ?summable and ?pos and ?neg and ?f and ?g 
   430     by safe
   431 qed
   432 
   433 subsection {* Term-by-Term Differentiability of Power Series *}
   434 
   435 definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a"
   436   where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))"
   437 
   438 text{*Lemma about distributing negation over it*}
   439 lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
   440   by (simp add: diffs_def)
   441 
   442 lemma sums_Suc_imp:
   443   "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   444   using sums_Suc_iff[of f] by simp
   445 
   446 lemma diffs_equiv:
   447   fixes x :: "'a::{real_normed_vector, ring_1}"
   448   shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>
   449       (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
   450   unfolding diffs_def
   451   by (simp add: summable_sums sums_Suc_imp)
   452 
   453 lemma lemma_termdiff1:
   454   fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   455   "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
   456    (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   457   by (auto simp add: algebra_simps power_add [symmetric])
   458 
   459 lemma sumr_diff_mult_const2:
   460   "setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
   461   by (simp add: setsum_subtractf)
   462 
   463 lemma lemma_termdiff2:
   464   fixes h :: "'a :: {field}"
   465   assumes h: "h \<noteq> 0"
   466   shows
   467     "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   468      h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p.
   469           (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
   470   apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
   471   apply (simp add: right_diff_distrib diff_divide_distrib h)
   472   apply (simp add: mult.assoc [symmetric])
   473   apply (cases "n", simp)
   474   apply (simp add: lemma_realpow_diff_sumr2 h
   475                    right_diff_distrib [symmetric] mult.assoc
   476               del: power_Suc setsum_lessThan_Suc of_nat_Suc)
   477   apply (subst lemma_realpow_rev_sumr)
   478   apply (subst sumr_diff_mult_const2)
   479   apply simp
   480   apply (simp only: lemma_termdiff1 setsum_right_distrib)
   481   apply (rule setsum.cong [OF refl])
   482   apply (simp add: less_iff_Suc_add)
   483   apply (clarify)
   484   apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
   485               del: setsum_lessThan_Suc power_Suc)
   486   apply (subst mult.assoc [symmetric], subst power_add [symmetric])
   487   apply (simp add: ac_simps)
   488   done
   489 
   490 lemma real_setsum_nat_ivl_bounded2:
   491   fixes K :: "'a::linordered_semidom"
   492   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
   493     and K: "0 \<le> K"
   494   shows "setsum f {..<n-k} \<le> of_nat n * K"
   495   apply (rule order_trans [OF setsum_mono])
   496   apply (rule f, simp)
   497   apply (simp add: mult_right_mono K)
   498   done
   499 
   500 lemma lemma_termdiff3:
   501   fixes h z :: "'a::{real_normed_field}"
   502   assumes 1: "h \<noteq> 0"
   503     and 2: "norm z \<le> K"
   504     and 3: "norm (z + h) \<le> K"
   505   shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
   506           \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   507 proof -
   508   have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
   509         norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p.
   510           (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
   511     by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
   512   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   513   proof (rule mult_right_mono [OF _ norm_ge_zero])
   514     from norm_ge_zero 2 have K: "0 \<le> K"
   515       by (rule order_trans)
   516     have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
   517       apply (erule subst)
   518       apply (simp only: norm_mult norm_power power_add)
   519       apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
   520       done
   521     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
   522           \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
   523       apply (intro
   524          order_trans [OF norm_setsum]
   525          real_setsum_nat_ivl_bounded2
   526          mult_nonneg_nonneg
   527          of_nat_0_le_iff
   528          zero_le_power K)
   529       apply (rule le_Kn, simp)
   530       done
   531   qed
   532   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   533     by (simp only: mult.assoc)
   534   finally show ?thesis .
   535 qed
   536 
   537 lemma lemma_termdiff4:
   538   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   539   assumes k: "0 < (k::real)"
   540     and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   541   shows "f -- 0 --> 0"
   542 proof (rule tendsto_norm_zero_cancel)
   543   show "(\<lambda>h. norm (f h)) -- 0 --> 0"
   544   proof (rule real_tendsto_sandwich)
   545     show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
   546       by simp
   547     show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
   548       using k by (auto simp add: eventually_at dist_norm le)
   549     show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
   550       by (rule tendsto_const)
   551     have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
   552       by (intro tendsto_intros)
   553     then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
   554       by simp
   555   qed
   556 qed
   557 
   558 lemma lemma_termdiff5:
   559   fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach"
   560   assumes k: "0 < (k::real)"
   561   assumes f: "summable f"
   562   assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   563   shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
   564 proof (rule lemma_termdiff4 [OF k])
   565   fix h::'a
   566   assume "h \<noteq> 0" and "norm h < k"
   567   hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
   568     by (simp add: le)
   569   hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
   570     by simp
   571   moreover from f have B: "summable (\<lambda>n. f n * norm h)"
   572     by (rule summable_mult2)
   573   ultimately have C: "summable (\<lambda>n. norm (g h n))"
   574     by (rule summable_comparison_test)
   575   hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
   576     by (rule summable_norm)
   577   also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
   578     by (rule suminf_le)
   579   also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
   580     by (rule suminf_mult2 [symmetric])
   581   finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
   582 qed
   583 
   584 
   585 text{* FIXME: Long proofs*}
   586 
   587 lemma termdiffs_aux:
   588   fixes x :: "'a::{real_normed_field,banach}"
   589   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   590     and 2: "norm x < norm K"
   591   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
   592              - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   593 proof -
   594   from dense [OF 2]
   595   obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
   596   from norm_ge_zero r1 have r: "0 < r"
   597     by (rule order_le_less_trans)
   598   hence r_neq_0: "r \<noteq> 0" by simp
   599   show ?thesis
   600   proof (rule lemma_termdiff5)
   601     show "0 < r - norm x" using r1 by simp
   602     from r r2 have "norm (of_real r::'a) < norm K"
   603       by simp
   604     with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
   605       by (rule powser_insidea)
   606     hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
   607       using r
   608       by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
   609     hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
   610       by (rule diffs_equiv [THEN sums_summable])
   611     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
   612       (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
   613       apply (rule ext)
   614       apply (simp add: diffs_def)
   615       apply (case_tac n, simp_all add: r_neq_0)
   616       done
   617     finally have "summable
   618       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
   619       by (rule diffs_equiv [THEN sums_summable])
   620     also have
   621       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
   622            r ^ (n - Suc 0)) =
   623        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
   624       apply (rule ext)
   625       apply (case_tac "n", simp)
   626       apply (rename_tac nat)
   627       apply (case_tac "nat", simp)
   628       apply (simp add: r_neq_0)
   629       done
   630     finally
   631     show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   632   next
   633     fix h::'a and n::nat
   634     assume h: "h \<noteq> 0"
   635     assume "norm h < r - norm x"
   636     hence "norm x + norm h < r" by simp
   637     with norm_triangle_ineq have xh: "norm (x + h) < r"
   638       by (rule order_le_less_trans)
   639     show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
   640           \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
   641       apply (simp only: norm_mult mult.assoc)
   642       apply (rule mult_left_mono [OF _ norm_ge_zero])
   643       apply (simp add: mult.assoc [symmetric])
   644       apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
   645       done
   646   qed
   647 qed
   648 
   649 lemma termdiffs:
   650   fixes K x :: "'a::{real_normed_field,banach}"
   651   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   652       and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   653       and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   654       and 4: "norm x < norm K"
   655   shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
   656   unfolding DERIV_def
   657 proof (rule LIM_zero_cancel)
   658   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
   659             - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   660   proof (rule LIM_equal2)
   661     show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   662   next
   663     fix h :: 'a
   664     assume "norm (h - 0) < norm K - norm x"
   665     hence "norm x + norm h < norm K" by simp
   666     hence 5: "norm (x + h) < norm K"
   667       by (rule norm_triangle_ineq [THEN order_le_less_trans])
   668     have "summable (\<lambda>n. c n * x ^ n)"
   669       and "summable (\<lambda>n. c n * (x + h) ^ n)"
   670       and "summable (\<lambda>n. diffs c n * x ^ n)"
   671       using 1 2 4 5 by (auto elim: powser_inside)
   672     then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   673           (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   674       by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
   675     then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   676           (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   677       by (simp add: algebra_simps)
   678   next
   679     show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   680       by (rule termdiffs_aux [OF 3 4])
   681   qed
   682 qed
   683 
   684 
   685 subsection {* Derivability of power series *}
   686 
   687 lemma DERIV_series':
   688   fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
   689   assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)"
   690     and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
   691     and "summable (f' x0)"
   692     and "summable L"
   693     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>"
   694   shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
   695   unfolding DERIV_def
   696 proof (rule LIM_I)
   697   fix r :: real
   698   assume "0 < r" hence "0 < r/3" by auto
   699 
   700   obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
   701     using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
   702 
   703   obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
   704     using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto
   705 
   706   let ?N = "Suc (max N_L N_f')"
   707   have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and
   708     L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto
   709 
   710   let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
   711 
   712   let ?r = "r / (3 * real ?N)"
   713   from `0 < r` have "0 < ?r" by simp
   714 
   715   let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
   716   def S' \<equiv> "Min (?s ` {..< ?N })"
   717 
   718   have "0 < S'" unfolding S'_def
   719   proof (rule iffD2[OF Min_gr_iff])
   720     show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x"
   721     proof
   722       fix x
   723       assume "x \<in> ?s ` {..<?N}"
   724       then obtain n where "x = ?s n" and "n \<in> {..<?N}"
   725         using image_iff[THEN iffD1] by blast
   726       from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
   727       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)"
   728         by auto
   729       have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
   730       thus "0 < x" unfolding `x = ?s n` .
   731     qed
   732   qed auto
   733 
   734   def S \<equiv> "min (min (x0 - a) (b - x0)) S'"
   735   hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0"
   736     and "S \<le> S'" using x0_in_I and `0 < S'`
   737     by auto
   738 
   739   {
   740     fix x
   741     assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
   742     hence x_in_I: "x0 + x \<in> { a <..< b }"
   743       using S_a S_b by auto
   744 
   745     note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
   746     note div_smbl = summable_divide[OF diff_smbl]
   747     note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`]
   748     note ign = summable_ignore_initial_segment[where k="?N"]
   749     note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]]
   750     note div_shft_smbl = summable_divide[OF diff_shft_smbl]
   751     note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
   752 
   753     { fix n
   754       have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
   755         using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
   756         unfolding abs_divide .
   757       hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)"
   758         using `x \<noteq> 0` by auto }
   759     note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
   760     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
   761       by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
   762     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
   763       using L_estimate by auto
   764 
   765     have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n<?N. \<bar>?diff n x - f' x0 n \<bar>)" ..
   766     also have "\<dots> < (\<Sum>n<?N. ?r)"
   767     proof (rule setsum_strict_mono)
   768       fix n
   769       assume "n \<in> {..< ?N}"
   770       have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` .
   771       also have "S \<le> S'" using `S \<le> S'` .
   772       also have "S' \<le> ?s n" unfolding S'_def
   773       proof (rule Min_le_iff[THEN iffD2])
   774         have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n"
   775           using `n \<in> {..< ?N}` by auto
   776         thus "\<exists> a \<in> (?s ` {..<?N}). a \<le> ?s n" by blast
   777       qed auto
   778       finally have "\<bar>x\<bar> < ?s n" .
   779 
   780       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]
   781       have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r" .
   782       with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
   783         by blast
   784     qed auto
   785     also have "\<dots> = of_nat (card {..<?N}) * ?r"
   786       by (rule setsum_constant)
   787     also have "\<dots> = real ?N * ?r"
   788       unfolding real_eq_of_nat by auto
   789     also have "\<dots> = r/3" by auto
   790     finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
   791 
   792     from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
   793     have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
   794         \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"
   795       unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric]
   796       using suminf_divide[OF diff_smbl, symmetric] by auto
   797     also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>"
   798       unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
   799       unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]]
   800       apply (subst (5) add.commute)
   801       by (rule abs_triangle_ineq)
   802     also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
   803       using abs_triangle_ineq4 by auto
   804     also have "\<dots> < r /3 + r/3 + r/3"
   805       using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
   806       by (rule add_strict_mono [OF add_less_le_mono])
   807     finally have "\<bar>(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\<bar> < r"
   808       by auto
   809   }
   810   thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
   811       norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r"
   812     using `0 < S` unfolding real_norm_def diff_0_right by blast
   813 qed
   814 
   815 lemma DERIV_power_series':
   816   fixes f :: "nat \<Rightarrow> real"
   817   assumes converges: "\<And> x. x \<in> {-R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)"
   818     and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R"
   819   shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)"
   820   (is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))")
   821 proof -
   822   {
   823     fix R'
   824     assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'"
   825     hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}"
   826       by auto
   827     have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))"
   828     proof (rule DERIV_series')
   829       show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)"
   830       proof -
   831         have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
   832           using `0 < R'` `0 < R` `R' < R` by auto
   833         hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}"
   834           using `R' < R` by auto
   835         have "norm R' < norm ((R' + R) / 2)"
   836           using `0 < R'` `0 < R` `R' < R` by auto
   837         from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
   838           by auto
   839       qed
   840       {
   841         fix n x y
   842         assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
   843         show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
   844         proof -
   845           have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
   846             (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
   847             unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
   848             by auto
   849           also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
   850           proof (rule mult_left_mono)
   851             have "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
   852               by (rule setsum_abs)
   853             also have "\<dots> \<le> (\<Sum>p<Suc n. R' ^ n)"
   854             proof (rule setsum_mono)
   855               fix p
   856               assume "p \<in> {..<Suc n}"
   857               hence "p \<le> n" by auto
   858               {
   859                 fix n
   860                 fix x :: real
   861                 assume "x \<in> {-R'<..<R'}"
   862                 hence "\<bar>x\<bar> \<le> R'"  by auto
   863                 hence "\<bar>x^n\<bar> \<le> R'^n"
   864                   unfolding power_abs by (rule power_mono, auto)
   865               }
   866               from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'`
   867               have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)"
   868                 unfolding abs_mult by auto
   869               thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n"
   870                 unfolding power_add[symmetric] using `p \<le> n` by auto
   871             qed
   872             also have "\<dots> = real (Suc n) * R' ^ n"
   873               unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
   874             finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
   875               unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
   876             show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
   877               unfolding abs_mult[symmetric] by auto
   878           qed
   879           also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>"
   880             unfolding abs_mult mult.assoc[symmetric] by algebra
   881           finally show ?thesis .
   882         qed
   883       }
   884       {
   885         fix n
   886         show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
   887           by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
   888       }
   889       {
   890         fix x
   891         assume "x \<in> {-R' <..< R'}"
   892         hence "R' \<in> {-R <..< R}" and "norm x < norm R'"
   893           using assms `R' < R` by auto
   894         have "summable (\<lambda> n. f n * x^n)"
   895         proof (rule summable_comparison_test, intro exI allI impI)
   896           fix n
   897           have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
   898             by (rule mult_left_mono) auto
   899           show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
   900             unfolding real_norm_def abs_mult
   901             by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
   902         qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
   903         from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
   904         show "summable (?f x)" by auto
   905       }
   906       show "summable (?f' x0)"
   907         using converges[OF `x0 \<in> {-R <..< R}`] .
   908       show "x0 \<in> {-R' <..< R'}"
   909         using `x0 \<in> {-R' <..< R'}` .
   910     qed
   911   } note for_subinterval = this
   912   let ?R = "(R + \<bar>x0\<bar>) / 2"
   913   have "\<bar>x0\<bar> < ?R" using assms by auto
   914   hence "- ?R < x0"
   915   proof (cases "x0 < 0")
   916     case True
   917     hence "- x0 < ?R" using `\<bar>x0\<bar> < ?R` by auto
   918     thus ?thesis unfolding neg_less_iff_less[symmetric, of "- x0"] by auto
   919   next
   920     case False
   921     have "- ?R < 0" using assms by auto
   922     also have "\<dots> \<le> x0" using False by auto
   923     finally show ?thesis .
   924   qed
   925   hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
   926     using assms by auto
   927   from for_subinterval[OF this]
   928   show ?thesis .
   929 qed
   930 
   931 
   932 subsection {* Exponential Function *}
   933 
   934 definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
   935   where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
   936 
   937 lemma summable_exp_generic:
   938   fixes x :: "'a::{real_normed_algebra_1,banach}"
   939   defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
   940   shows "summable S"
   941 proof -
   942   have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
   943     unfolding S_def by (simp del: mult_Suc)
   944   obtain r :: real where r0: "0 < r" and r1: "r < 1"
   945     using dense [OF zero_less_one] by fast
   946   obtain N :: nat where N: "norm x < real N * r"
   947     using reals_Archimedean3 [OF r0] by fast
   948   from r1 show ?thesis
   949   proof (rule summable_ratio_test [rule_format])
   950     fix n :: nat
   951     assume n: "N \<le> n"
   952     have "norm x \<le> real N * r"
   953       using N by (rule order_less_imp_le)
   954     also have "real N * r \<le> real (Suc n) * r"
   955       using r0 n by (simp add: mult_right_mono)
   956     finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)"
   957       using norm_ge_zero by (rule mult_right_mono)
   958     hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
   959       by (rule order_trans [OF norm_mult_ineq])
   960     hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
   961       by (simp add: pos_divide_le_eq ac_simps)
   962     thus "norm (S (Suc n)) \<le> r * norm (S n)"
   963       by (simp add: S_Suc inverse_eq_divide)
   964   qed
   965 qed
   966 
   967 lemma summable_norm_exp:
   968   fixes x :: "'a::{real_normed_algebra_1,banach}"
   969   shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
   970 proof (rule summable_norm_comparison_test [OF exI, rule_format])
   971   show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
   972     by (rule summable_exp_generic)
   973   fix n
   974   show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
   975     by (simp add: norm_power_ineq)
   976 qed
   977 
   978 lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
   979   using summable_exp_generic [where x=x] by simp
   980 
   981 lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
   982   unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
   983 
   984 
   985 lemma exp_fdiffs:
   986       "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
   987   by (simp add: diffs_def mult.assoc [symmetric] real_of_nat_def of_nat_mult
   988         del: mult_Suc of_nat_Suc)
   989 
   990 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
   991   by (simp add: diffs_def)
   992 
   993 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
   994   unfolding exp_def scaleR_conv_of_real
   995   apply (rule DERIV_cong)
   996   apply (rule termdiffs [where K="of_real (1 + norm x)"])
   997   apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
   998   apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
   999   apply (simp del: of_real_add)
  1000   done
  1001 
  1002 declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
  1003 
  1004 lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
  1005 proof -
  1006   from summable_norm[OF summable_norm_exp, of x]
  1007   have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
  1008     by (simp add: exp_def)
  1009   also have "\<dots> \<le> exp (norm x)"
  1010     using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
  1011     by (auto simp: exp_def intro!: suminf_le norm_power_ineq)
  1012   finally show ?thesis .
  1013 qed
  1014 
  1015 lemma isCont_exp:
  1016   fixes x::"'a::{real_normed_field,banach}"
  1017   shows "isCont exp x"
  1018   by (rule DERIV_exp [THEN DERIV_isCont])
  1019 
  1020 lemma isCont_exp' [simp]:
  1021   fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
  1022   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
  1023   by (rule isCont_o2 [OF _ isCont_exp])
  1024 
  1025 lemma tendsto_exp [tendsto_intros]:
  1026   fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
  1027   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
  1028   by (rule isCont_tendsto_compose [OF isCont_exp])
  1029 
  1030 lemma continuous_exp [continuous_intros]:
  1031   fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
  1032   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
  1033   unfolding continuous_def by (rule tendsto_exp)
  1034 
  1035 lemma continuous_on_exp [continuous_intros]:
  1036   fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
  1037   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
  1038   unfolding continuous_on_def by (auto intro: tendsto_exp)
  1039 
  1040 
  1041 subsubsection {* Properties of the Exponential Function *}
  1042 
  1043 lemma powser_zero:
  1044   fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
  1045   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
  1046 proof -
  1047   have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
  1048     by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
  1049   thus ?thesis unfolding One_nat_def by simp
  1050 qed
  1051 
  1052 lemma exp_zero [simp]: "exp 0 = 1"
  1053   unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
  1054 
  1055 lemma exp_series_add_commuting:
  1056   fixes x y :: "'a::{real_normed_algebra_1, banach}"
  1057   defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
  1058   assumes comm: "x * y = y * x"
  1059   shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
  1060 proof (induct n)
  1061   case 0
  1062   show ?case
  1063     unfolding S_def by simp
  1064 next
  1065   case (Suc n)
  1066   have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
  1067     unfolding S_def by (simp del: mult_Suc)
  1068   hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
  1069     by simp
  1070   have S_comm: "\<And>n. S x n * y = y * S x n"
  1071     by (simp add: power_commuting_commutes comm S_def)
  1072 
  1073   have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
  1074     by (simp only: times_S)
  1075   also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1076     by (simp only: Suc)
  1077   also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
  1078                 + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1079     by (rule distrib_right)
  1080   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
  1081                 + (\<Sum>i\<le>n. S x i * y * S y (n-i))"
  1082     by (simp add: setsum_right_distrib ac_simps S_comm)
  1083   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
  1084                 + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
  1085     by (simp add: ac_simps)
  1086   also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
  1087                 + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1088     by (simp add: times_S Suc_diff_le)
  1089   also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
  1090              (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
  1091     by (subst setsum_atMost_Suc_shift) simp
  1092   also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1093              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1094     by simp
  1095   also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
  1096              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1097              (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
  1098     by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
  1099                    real_of_nat_add [symmetric]) simp
  1100   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
  1101     by (simp only: scaleR_right.setsum)
  1102   finally show
  1103     "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
  1104     by (simp del: setsum_cl_ivl_Suc)
  1105 qed
  1106 
  1107 lemma exp_add_commuting: "x * y = y * x \<Longrightarrow> exp (x + y) = exp x * exp y"
  1108   unfolding exp_def
  1109   by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting)
  1110 
  1111 lemma exp_add:
  1112   fixes x y::"'a::{real_normed_field,banach}"
  1113   shows "exp (x + y) = exp x * exp y"
  1114   by (rule exp_add_commuting) (simp add: ac_simps)
  1115 
  1116 lemmas mult_exp_exp = exp_add [symmetric]
  1117 
  1118 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  1119   unfolding exp_def
  1120   apply (subst suminf_of_real)
  1121   apply (rule summable_exp_generic)
  1122   apply (simp add: scaleR_conv_of_real)
  1123   done
  1124 
  1125 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
  1126 proof
  1127   have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
  1128   also assume "exp x = 0"
  1129   finally show "False" by simp
  1130 qed
  1131 
  1132 lemma exp_minus_inverse:
  1133   shows "exp x * exp (- x) = 1"
  1134   by (simp add: exp_add_commuting[symmetric])
  1135 
  1136 lemma exp_minus:
  1137   fixes x :: "'a::{real_normed_field, banach}"
  1138   shows "exp (- x) = inverse (exp x)"
  1139   by (intro inverse_unique [symmetric] exp_minus_inverse)
  1140 
  1141 lemma exp_diff:
  1142   fixes x :: "'a::{real_normed_field, banach}"
  1143   shows "exp (x - y) = exp x / exp y"
  1144   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
  1145 
  1146 
  1147 subsubsection {* Properties of the Exponential Function on Reals *}
  1148 
  1149 text {* Comparisons of @{term "exp x"} with zero. *}
  1150 
  1151 text{*Proof: because every exponential can be seen as a square.*}
  1152 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
  1153 proof -
  1154   have "0 \<le> exp (x/2) * exp (x/2)" by simp
  1155   thus ?thesis by (simp add: exp_add [symmetric])
  1156 qed
  1157 
  1158 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
  1159   by (simp add: order_less_le)
  1160 
  1161 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
  1162   by (simp add: not_less)
  1163 
  1164 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
  1165   by (simp add: not_le)
  1166 
  1167 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
  1168   by simp
  1169 
  1170 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  1171   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
  1172 
  1173 text {* Strict monotonicity of exponential. *}
  1174 
  1175 lemma exp_ge_add_one_self_aux: 
  1176   assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
  1177 using order_le_imp_less_or_eq [OF assms]
  1178 proof 
  1179   assume "0 < x"
  1180   have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
  1181     by (auto simp add: numeral_2_eq_2)
  1182   also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
  1183     apply (rule setsum_le_suminf [OF summable_exp])
  1184     using `0 < x`
  1185     apply (auto  simp add:  zero_le_mult_iff)
  1186     done
  1187   finally show "1+x \<le> exp x" 
  1188     by (simp add: exp_def)
  1189 next
  1190   assume "0 = x"
  1191   then show "1 + x \<le> exp x"
  1192     by auto
  1193 qed
  1194 
  1195 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
  1196 proof -
  1197   assume x: "0 < x"
  1198   hence "1 < 1 + x" by simp
  1199   also from x have "1 + x \<le> exp x"
  1200     by (simp add: exp_ge_add_one_self_aux)
  1201   finally show ?thesis .
  1202 qed
  1203 
  1204 lemma exp_less_mono:
  1205   fixes x y :: real
  1206   assumes "x < y"
  1207   shows "exp x < exp y"
  1208 proof -
  1209   from `x < y` have "0 < y - x" by simp
  1210   hence "1 < exp (y - x)" by (rule exp_gt_one)
  1211   hence "1 < exp y / exp x" by (simp only: exp_diff)
  1212   thus "exp x < exp y" by simp
  1213 qed
  1214 
  1215 lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
  1216   unfolding linorder_not_le [symmetric]
  1217   by (auto simp add: order_le_less exp_less_mono)
  1218 
  1219 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
  1220   by (auto intro: exp_less_mono exp_less_cancel)
  1221 
  1222 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
  1223   by (auto simp add: linorder_not_less [symmetric])
  1224 
  1225 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
  1226   by (simp add: order_eq_iff)
  1227 
  1228 text {* Comparisons of @{term "exp x"} with one. *}
  1229 
  1230 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
  1231   using exp_less_cancel_iff [where x=0 and y=x] by simp
  1232 
  1233 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
  1234   using exp_less_cancel_iff [where x=x and y=0] by simp
  1235 
  1236 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
  1237   using exp_le_cancel_iff [where x=0 and y=x] by simp
  1238 
  1239 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
  1240   using exp_le_cancel_iff [where x=x and y=0] by simp
  1241 
  1242 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
  1243   using exp_inj_iff [where x=x and y=0] by simp
  1244 
  1245 lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
  1246 proof (rule IVT)
  1247   assume "1 \<le> y"
  1248   hence "0 \<le> y - 1" by simp
  1249   hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
  1250   thus "y \<le> exp (y - 1)" by simp
  1251 qed (simp_all add: le_diff_eq)
  1252 
  1253 lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
  1254 proof (rule linorder_le_cases [of 1 y])
  1255   assume "1 \<le> y"
  1256   thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
  1257 next
  1258   assume "0 < y" and "y \<le> 1"
  1259   hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
  1260   then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
  1261   hence "exp (- x) = y" by (simp add: exp_minus)
  1262   thus "\<exists>x. exp x = y" ..
  1263 qed
  1264 
  1265 
  1266 subsection {* Natural Logarithm *}
  1267 
  1268 definition ln :: "real \<Rightarrow> real"
  1269   where "ln x = (THE u. exp u = x)"
  1270 
  1271 lemma ln_exp [simp]: "ln (exp x) = x"
  1272   by (simp add: ln_def)
  1273 
  1274 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
  1275   by (auto dest: exp_total)
  1276 
  1277 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
  1278   by (metis exp_gt_zero exp_ln)
  1279 
  1280 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
  1281   by (erule subst, rule ln_exp)
  1282 
  1283 lemma ln_one [simp]: "ln 1 = 0"
  1284   by (rule ln_unique) simp
  1285 
  1286 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
  1287   by (rule ln_unique) (simp add: exp_add)
  1288 
  1289 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
  1290   by (rule ln_unique) (simp add: exp_minus)
  1291 
  1292 lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  1293   by (rule ln_unique) (simp add: exp_diff)
  1294 
  1295 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
  1296   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  1297 
  1298 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  1299   by (subst exp_less_cancel_iff [symmetric]) simp
  1300 
  1301 lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
  1302   by (simp add: linorder_not_less [symmetric])
  1303 
  1304 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
  1305   by (simp add: order_eq_iff)
  1306 
  1307 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  1308   apply (rule exp_le_cancel_iff [THEN iffD1])
  1309   apply (simp add: exp_ge_add_one_self_aux)
  1310   done
  1311 
  1312 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  1313   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  1314 
  1315 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  1316   using ln_le_cancel_iff [of 1 x] by simp
  1317 
  1318 lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  1319   using ln_le_cancel_iff [of 1 x] by simp
  1320 
  1321 lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  1322   using ln_le_cancel_iff [of 1 x] by simp
  1323 
  1324 lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  1325   using ln_less_cancel_iff [of x 1] by simp
  1326 
  1327 lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  1328   using ln_less_cancel_iff [of 1 x] by simp
  1329 
  1330 lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  1331   using ln_less_cancel_iff [of 1 x] by simp
  1332 
  1333 lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  1334   using ln_less_cancel_iff [of 1 x] by simp
  1335 
  1336 lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  1337   using ln_inj_iff [of x 1] by simp
  1338 
  1339 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  1340   by simp
  1341 
  1342 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  1343   by (auto simp add: ln_def intro!: arg_cong[where f=The])
  1344 
  1345 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  1346 proof cases
  1347   assume "0 < x"
  1348   moreover then have "isCont ln (exp (ln x))"
  1349     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
  1350   ultimately show ?thesis
  1351     by simp
  1352 next
  1353   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
  1354     unfolding isCont_def
  1355     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
  1356        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
  1357                 intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
  1358 qed
  1359 
  1360 lemma tendsto_ln [tendsto_intros]:
  1361   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  1362   by (rule isCont_tendsto_compose [OF isCont_ln])
  1363 
  1364 lemma continuous_ln:
  1365   "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  1366   unfolding continuous_def by (rule tendsto_ln)
  1367 
  1368 lemma isCont_ln' [continuous_intros]:
  1369   "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  1370   unfolding continuous_at by (rule tendsto_ln)
  1371 
  1372 lemma continuous_within_ln [continuous_intros]:
  1373   "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  1374   unfolding continuous_within by (rule tendsto_ln)
  1375 
  1376 lemma continuous_on_ln [continuous_intros]:
  1377   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  1378   unfolding continuous_on_def by (auto intro: tendsto_ln)
  1379 
  1380 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  1381   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  1382   apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  1383   done
  1384 
  1385 lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  1386   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  1387 
  1388 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  1389 
  1390 lemma ln_series:
  1391   assumes "0 < x" and "x < 2"
  1392   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
  1393   (is "ln x = suminf (?f (x - 1))")
  1394 proof -
  1395   let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
  1396 
  1397   have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
  1398   proof (rule DERIV_isconst3[where x=x])
  1399     fix x :: real
  1400     assume "x \<in> {0 <..< 2}"
  1401     hence "0 < x" and "x < 2" by auto
  1402     have "norm (1 - x) < 1"
  1403       using `0 < x` and `x < 2` by auto
  1404     have "1 / x = 1 / (1 - (1 - x))" by auto
  1405     also have "\<dots> = (\<Sum> n. (1 - x)^n)"
  1406       using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
  1407     also have "\<dots> = suminf (?f' x)"
  1408       unfolding power_mult_distrib[symmetric]
  1409       by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
  1410     finally have "DERIV ln x :> suminf (?f' x)"
  1411       using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
  1412     moreover
  1413     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
  1414     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
  1415       (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
  1416     proof (rule DERIV_power_series')
  1417       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
  1418         using `0 < x` `x < 2` by auto
  1419       fix x :: real
  1420       assume "x \<in> {- 1<..<1}"
  1421       hence "norm (-x) < 1" by auto
  1422       show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
  1423         unfolding One_nat_def
  1424         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  1425     qed
  1426     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
  1427       unfolding One_nat_def by auto
  1428     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
  1429       unfolding DERIV_def repos .
  1430     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
  1431       by (rule DERIV_diff)
  1432     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
  1433   qed (auto simp add: assms)
  1434   thus ?thesis by auto
  1435 qed
  1436 
  1437 lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  1438 proof -
  1439   have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
  1440     by (simp add: exp_def)
  1441   also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) + 
  1442     (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
  1443     by (rule suminf_split_initial_segment)
  1444   also have "?a = 1 + x"
  1445     by (simp add: numeral_2_eq_2)
  1446   finally show ?thesis
  1447     by simp
  1448 qed
  1449 
  1450 lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
  1451 proof -
  1452   assume a: "0 <= x"
  1453   assume b: "x <= 1"
  1454   {
  1455     fix n :: nat
  1456     have "2 * 2 ^ n \<le> fact (n + 2)"
  1457       by (induct n) simp_all
  1458     hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
  1459       by (simp only: real_of_nat_le_iff)
  1460     hence "2 * 2 ^ n \<le> real (fact (n + 2))"
  1461       by simp
  1462     hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
  1463       by (rule le_imp_inverse_le) simp
  1464     hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
  1465       by (simp add: power_inverse)
  1466     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  1467       by (rule mult_mono)
  1468         (rule mult_mono, simp_all add: power_le_one a b)
  1469     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  1470       unfolding power_add by (simp add: ac_simps del: fact_Suc) }
  1471   note aux1 = this
  1472   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  1473     by (intro sums_mult geometric_sums, simp)
  1474   hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
  1475     by simp
  1476   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
  1477   proof -
  1478     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
  1479         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
  1480       apply (rule suminf_le)
  1481       apply (rule allI, rule aux1)
  1482       apply (rule summable_exp [THEN summable_ignore_initial_segment])
  1483       by (rule sums_summable, rule aux2)
  1484     also have "... = x\<^sup>2"
  1485       by (rule sums_unique [THEN sym], rule aux2)
  1486     finally show ?thesis .
  1487   qed
  1488   thus ?thesis unfolding exp_first_two_terms by auto
  1489 qed
  1490 
  1491 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  1492 proof -
  1493   assume a: "0 <= (x::real)" and b: "x < 1"
  1494   have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  1495     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
  1496   also have "... <= 1"
  1497     by (auto simp add: a)
  1498   finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
  1499   moreover have c: "0 < 1 + x + x\<^sup>2"
  1500     by (simp add: add_pos_nonneg a)
  1501   ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
  1502     by (elim mult_imp_le_div_pos)
  1503   also have "... <= 1 / exp x"
  1504     by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs 
  1505               real_sqrt_pow2_iff real_sqrt_power)
  1506   also have "... = exp (-x)"
  1507     by (auto simp add: exp_minus divide_inverse)
  1508   finally have "1 - x <= exp (- x)" .
  1509   also have "1 - x = exp (ln (1 - x))"
  1510     by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
  1511   finally have "exp (ln (1 - x)) <= exp (- x)" .
  1512   thus ?thesis by (auto simp only: exp_le_cancel_iff)
  1513 qed
  1514 
  1515 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
  1516   apply (case_tac "0 <= x")
  1517   apply (erule exp_ge_add_one_self_aux)
  1518   apply (case_tac "x <= -1")
  1519   apply (subgoal_tac "1 + x <= 0")
  1520   apply (erule order_trans)
  1521   apply simp
  1522   apply simp
  1523   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
  1524   apply (erule ssubst)
  1525   apply (subst exp_le_cancel_iff)
  1526   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
  1527   apply simp
  1528   apply (rule ln_one_minus_pos_upper_bound)
  1529   apply auto
  1530 done
  1531 
  1532 lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  1533 proof -
  1534   assume a: "0 <= x" and b: "x <= 1"
  1535   have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  1536     by (rule exp_diff)
  1537   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
  1538     by (metis a b divide_right_mono exp_bound exp_ge_zero)
  1539   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
  1540     by (simp add: a divide_left_mono add_pos_nonneg)
  1541   also from a have "... <= 1 + x"
  1542     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
  1543   finally have "exp (x - x\<^sup>2) <= 1 + x" .
  1544   also have "... = exp (ln (1 + x))"
  1545   proof -
  1546     from a have "0 < 1 + x" by auto
  1547     thus ?thesis
  1548       by (auto simp only: exp_ln_iff [THEN sym])
  1549   qed
  1550   finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
  1551   thus ?thesis
  1552     by (metis exp_le_cancel_iff) 
  1553 qed
  1554 
  1555 lemma ln_one_minus_pos_lower_bound:
  1556   "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  1557 proof -
  1558   assume a: "0 <= x" and b: "x <= (1 / 2)"
  1559   from b have c: "x < 1" by auto
  1560   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
  1561     apply (subst ln_inverse [symmetric])
  1562     apply (simp add: field_simps)
  1563     apply (rule arg_cong [where f=ln])
  1564     apply (simp add: field_simps)
  1565     done
  1566   also have "- (x / (1 - x)) <= ..."
  1567   proof -
  1568     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
  1569       using a c by (intro ln_add_one_self_le_self) auto
  1570     thus ?thesis
  1571       by auto
  1572   qed
  1573   also have "- (x / (1 - x)) = -x / (1 - x)"
  1574     by auto
  1575   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1576   have "0 < 1 - x" using a b by simp
  1577   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1578     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1579     by (simp add: field_simps power2_eq_square)
  1580   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1581     by (rule order_trans)
  1582 qed
  1583 
  1584 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1585   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1586   apply (subst ln_le_cancel_iff)
  1587   apply auto
  1588   done
  1589 
  1590 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1591   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1592 proof -
  1593   assume x: "0 <= x"
  1594   assume x1: "x <= 1"
  1595   from x have "ln (1 + x) <= x"
  1596     by (rule ln_add_one_self_le_self)
  1597   then have "ln (1 + x) - x <= 0"
  1598     by simp
  1599   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1600     by (rule abs_of_nonpos)
  1601   also have "... = x - ln (1 + x)"
  1602     by simp
  1603   also have "... <= x\<^sup>2"
  1604   proof -
  1605     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1606       by (intro ln_one_plus_pos_lower_bound)
  1607     thus ?thesis
  1608       by simp
  1609   qed
  1610   finally show ?thesis .
  1611 qed
  1612 
  1613 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1614   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1615 proof -
  1616   assume a: "-(1 / 2) <= x"
  1617   assume b: "x <= 0"
  1618   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1619     apply (subst abs_of_nonpos)
  1620     apply simp
  1621     apply (rule ln_add_one_self_le_self2)
  1622     using a apply auto
  1623     done
  1624   also have "... <= 2 * x\<^sup>2"
  1625     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1626     apply (simp add: algebra_simps)
  1627     apply (rule ln_one_minus_pos_lower_bound)
  1628     using a b apply auto
  1629     done
  1630   finally show ?thesis .
  1631 qed
  1632 
  1633 lemma abs_ln_one_plus_x_minus_x_bound:
  1634     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1635   apply (case_tac "0 <= x")
  1636   apply (rule order_trans)
  1637   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1638   apply auto
  1639   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1640   apply auto
  1641   done
  1642 
  1643 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1644 proof -
  1645   assume x: "exp 1 <= x" "x <= y"
  1646   moreover have "0 < exp (1::real)" by simp
  1647   ultimately have a: "0 < x" and b: "0 < y"
  1648     by (fast intro: less_le_trans order_trans)+
  1649   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1650     by (simp add: algebra_simps)
  1651   also have "... = x * ln(y / x)"
  1652     by (simp only: ln_div a b)
  1653   also have "y / x = (x + (y - x)) / x"
  1654     by simp
  1655   also have "... = 1 + (y - x) / x"
  1656     using x a by (simp add: field_simps)
  1657   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1658     using x a 
  1659     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1660   also have "... = y - x" using a by simp
  1661   also have "... = (y - x) * ln (exp 1)" by simp
  1662   also have "... <= (y - x) * ln x"
  1663     apply (rule mult_left_mono)
  1664     apply (subst ln_le_cancel_iff)
  1665     apply fact
  1666     apply (rule a)
  1667     apply (rule x)
  1668     using x apply simp
  1669     done
  1670   also have "... = y * ln x - x * ln x"
  1671     by (rule left_diff_distrib)
  1672   finally have "x * ln y <= y * ln x"
  1673     by arith
  1674   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1675   also have "... = y * (ln x / x)" by simp
  1676   finally show ?thesis using b by (simp add: field_simps)
  1677 qed
  1678 
  1679 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1680   using exp_ge_add_one_self[of "ln x"] by simp
  1681 
  1682 lemma ln_eq_minus_one:
  1683   assumes "0 < x" "ln x = x - 1"
  1684   shows "x = 1"
  1685 proof -
  1686   let ?l = "\<lambda>y. ln y - y + 1"
  1687   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1688     by (auto intro!: derivative_eq_intros)
  1689 
  1690   show ?thesis
  1691   proof (cases rule: linorder_cases)
  1692     assume "x < 1"
  1693     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1694     from `x < a` have "?l x < ?l a"
  1695     proof (rule DERIV_pos_imp_increasing, safe)
  1696       fix y
  1697       assume "x \<le> y" "y \<le> a"
  1698       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1699         by (auto simp: field_simps)
  1700       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1701         by auto
  1702     qed
  1703     also have "\<dots> \<le> 0"
  1704       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1705     finally show "x = 1" using assms by auto
  1706   next
  1707     assume "1 < x"
  1708     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1709     from `a < x` have "?l x < ?l a"
  1710     proof (rule DERIV_neg_imp_decreasing, safe)
  1711       fix y
  1712       assume "a \<le> y" "y \<le> x"
  1713       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1714         by (auto simp: field_simps)
  1715       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1716         by blast
  1717     qed
  1718     also have "\<dots> \<le> 0"
  1719       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1720     finally show "x = 1" using assms by auto
  1721   next
  1722     assume "x = 1"
  1723     then show ?thesis by simp
  1724   qed
  1725 qed
  1726 
  1727 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1728   unfolding tendsto_Zfun_iff
  1729 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1730   fix r :: real assume "0 < r"
  1731   {
  1732     fix x
  1733     assume "x < ln r"
  1734     then have "exp x < exp (ln r)"
  1735       by simp
  1736     with `0 < r` have "exp x < r"
  1737       by simp
  1738   }
  1739   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1740 qed
  1741 
  1742 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1743   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1744      (auto intro: eventually_gt_at_top)
  1745 
  1746 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1747   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1748      (auto simp: eventually_at_filter)
  1749 
  1750 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1751   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1752      (auto intro: eventually_gt_at_top)
  1753 
  1754 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1755 proof (induct k)
  1756   case 0
  1757   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1758     by (simp add: inverse_eq_divide[symmetric])
  1759        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1760               at_top_le_at_infinity order_refl)
  1761 next
  1762   case (Suc k)
  1763   show ?case
  1764   proof (rule lhospital_at_top_at_top)
  1765     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1766       by eventually_elim (intro derivative_eq_intros, auto)
  1767     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1768       by eventually_elim auto
  1769     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1770       by auto
  1771     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1772     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1773       by simp
  1774   qed (rule exp_at_top)
  1775 qed
  1776 
  1777 
  1778 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1779   -- {*exponentation with real exponent*}
  1780   where "x powr a = exp(a * ln x)"
  1781 
  1782 definition log :: "[real,real] => real"
  1783   -- {*logarithm of @{term x} to base @{term a}*}
  1784   where "log a x = ln x / ln a"
  1785 
  1786 
  1787 lemma tendsto_log [tendsto_intros]:
  1788   "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) ---> log a b) F"
  1789   unfolding log_def by (intro tendsto_intros) auto
  1790 
  1791 lemma continuous_log:
  1792   assumes "continuous F f"
  1793     and "continuous F g"
  1794     and "0 < f (Lim F (\<lambda>x. x))"
  1795     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1796     and "0 < g (Lim F (\<lambda>x. x))"
  1797   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1798   using assms unfolding continuous_def by (rule tendsto_log)
  1799 
  1800 lemma continuous_at_within_log[continuous_intros]:
  1801   assumes "continuous (at a within s) f"
  1802     and "continuous (at a within s) g"
  1803     and "0 < f a"
  1804     and "f a \<noteq> 1"
  1805     and "0 < g a"
  1806   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1807   using assms unfolding continuous_within by (rule tendsto_log)
  1808 
  1809 lemma isCont_log[continuous_intros, simp]:
  1810   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1811   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1812   using assms unfolding continuous_at by (rule tendsto_log)
  1813 
  1814 lemma continuous_on_log[continuous_intros]:
  1815   assumes "continuous_on s f" "continuous_on s g"
  1816     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1817   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1818   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1819 
  1820 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1821   by (simp add: powr_def)
  1822 
  1823 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1824   by (simp add: powr_def)
  1825 
  1826 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1827   by (simp add: powr_def)
  1828 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1829 
  1830 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1831   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1832 
  1833 lemma powr_gt_zero [simp]: "0 < x powr a"
  1834   by (simp add: powr_def)
  1835 
  1836 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1837   by (rule order_less_imp_le, rule powr_gt_zero)
  1838 
  1839 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1840   by (simp add: powr_def)
  1841 
  1842 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1843   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1844   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1845   done
  1846 
  1847 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1848   apply (simp add: powr_def)
  1849   apply (subst exp_diff [THEN sym])
  1850   apply (simp add: left_diff_distrib)
  1851   done
  1852 
  1853 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1854   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1855 
  1856 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1857   using assms by (auto simp: powr_add)
  1858 
  1859 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1860   by (simp add: powr_def)
  1861 
  1862 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1863   by (simp add: powr_powr mult.commute)
  1864 
  1865 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1866   by (simp add: powr_def exp_minus [symmetric])
  1867 
  1868 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1869   by (simp add: divide_inverse powr_minus)
  1870 
  1871 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1872   by (simp add: powr_def)
  1873 
  1874 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1875   by (simp add: powr_def)
  1876 
  1877 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1878   by (blast intro: powr_less_cancel powr_less_mono)
  1879 
  1880 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1881   by (simp add: linorder_not_less [symmetric])
  1882 
  1883 lemma log_ln: "ln x = log (exp(1)) x"
  1884   by (simp add: log_def)
  1885 
  1886 lemma DERIV_log:
  1887   assumes "x > 0"
  1888   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1889 proof -
  1890   def lb \<equiv> "1 / ln b"
  1891   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1892     using `x > 0` by (auto intro!: derivative_eq_intros)
  1893   ultimately show ?thesis
  1894     by (simp add: log_def)
  1895 qed
  1896 
  1897 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1898 
  1899 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1900   by (simp add: powr_def log_def)
  1901 
  1902 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1903   by (simp add: log_def powr_def)
  1904 
  1905 lemma log_mult:
  1906   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1907     log a (x * y) = log a x + log a y"
  1908   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1909 
  1910 lemma log_eq_div_ln_mult_log:
  1911   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1912     log a x = (ln b/ln a) * log b x"
  1913   by (simp add: log_def divide_inverse)
  1914 
  1915 text{*Base 10 logarithms*}
  1916 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1917   by (simp add: log_def)
  1918 
  1919 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1920   by (simp add: log_def)
  1921 
  1922 lemma log_one [simp]: "log a 1 = 0"
  1923   by (simp add: log_def)
  1924 
  1925 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1926   by (simp add: log_def)
  1927 
  1928 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1929   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1930   apply (simp add: log_mult [symmetric])
  1931   done
  1932 
  1933 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"
  1934   by (simp add: log_mult divide_inverse log_inverse)
  1935 
  1936 lemma log_less_cancel_iff [simp]:
  1937   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  1938   apply safe
  1939   apply (rule_tac [2] powr_less_cancel)
  1940   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  1941   done
  1942 
  1943 lemma log_inj:
  1944   assumes "1 < b"
  1945   shows "inj_on (log b) {0 <..}"
  1946 proof (rule inj_onI, simp)
  1947   fix x y
  1948   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  1949   show "x = y"
  1950   proof (cases rule: linorder_cases)
  1951     assume "x = y"
  1952     then show ?thesis by simp
  1953   next
  1954     assume "x < y" hence "log b x < log b y"
  1955       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1956     then show ?thesis using * by simp
  1957   next
  1958     assume "y < x" hence "log b y < log b x"
  1959       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1960     then show ?thesis using * by simp
  1961   qed
  1962 qed
  1963 
  1964 lemma log_le_cancel_iff [simp]:
  1965   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  1966   by (simp add: linorder_not_less [symmetric])
  1967 
  1968 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  1969   using log_less_cancel_iff[of a 1 x] by simp
  1970 
  1971 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  1972   using log_le_cancel_iff[of a 1 x] by simp
  1973 
  1974 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  1975   using log_less_cancel_iff[of a x 1] by simp
  1976 
  1977 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  1978   using log_le_cancel_iff[of a x 1] by simp
  1979 
  1980 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  1981   using log_less_cancel_iff[of a a x] by simp
  1982 
  1983 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  1984   using log_le_cancel_iff[of a a x] by simp
  1985 
  1986 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  1987   using log_less_cancel_iff[of a x a] by simp
  1988 
  1989 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  1990   using log_le_cancel_iff[of a x a] by simp
  1991 
  1992 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  1993   apply (induct n)
  1994   apply simp
  1995   apply (subgoal_tac "real(Suc n) = real n + 1")
  1996   apply (erule ssubst)
  1997   apply (subst powr_add, simp, simp)
  1998   done
  1999 
  2000 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  2001   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  2002 
  2003 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  2004 by(simp add: powr_realpow_numeral)
  2005 
  2006 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  2007   apply (case_tac "x = 0", simp, simp)
  2008   apply (rule powr_realpow [THEN sym], simp)
  2009   done
  2010 
  2011 lemma powr_int:
  2012   assumes "x > 0"
  2013   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  2014 proof (cases "i < 0")
  2015   case True
  2016   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  2017   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  2018 next
  2019   case False
  2020   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  2021 qed
  2022 
  2023 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  2024   using powr_realpow [of x 1] by simp
  2025 
  2026 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  2027   by (fact powr_realpow_numeral)
  2028 
  2029 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  2030   using powr_int [of x "- 1"] by simp
  2031 
  2032 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  2033   using powr_int [of x "- numeral n"] by simp
  2034 
  2035 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  2036   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  2037 
  2038 lemma ln_powr: "ln (x powr y) = y * ln x"
  2039   by (simp add: powr_def)
  2040 
  2041 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  2042 by(simp add: root_powr_inverse ln_powr)
  2043 
  2044 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
  2045   by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
  2046 
  2047 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  2048 by(simp add: log_def ln_root)
  2049 
  2050 lemma log_powr: "log b (x powr y) = y * log b x"
  2051   by (simp add: log_def ln_powr)
  2052 
  2053 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
  2054   by (simp add: log_powr powr_realpow [symmetric])
  2055 
  2056 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  2057   by (simp add: log_def)
  2058 
  2059 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  2060   by (simp add: log_def ln_realpow)
  2061 
  2062 lemma log_base_powr: "log (a powr b) x = log a x / b"
  2063   by (simp add: log_def ln_powr)
  2064 
  2065 lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  2066 by(simp add: log_def ln_root)
  2067 
  2068 lemma ln_bound: "1 <= x ==> ln x <= x"
  2069   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  2070   apply simp
  2071   apply (rule ln_add_one_self_le_self, simp)
  2072   done
  2073 
  2074 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  2075   apply (cases "x = 1", simp)
  2076   apply (cases "a = b", simp)
  2077   apply (rule order_less_imp_le)
  2078   apply (rule powr_less_mono, auto)
  2079   done
  2080 
  2081 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2082   apply (subst powr_zero_eq_one [THEN sym])
  2083   apply (rule powr_mono, assumption+)
  2084   done
  2085 
  2086 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2087   apply (unfold powr_def)
  2088   apply (rule exp_less_mono)
  2089   apply (rule mult_strict_left_mono)
  2090   apply (subst ln_less_cancel_iff, assumption)
  2091   apply (rule order_less_trans)
  2092   prefer 2
  2093   apply assumption+
  2094   done
  2095 
  2096 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2097   apply (unfold powr_def)
  2098   apply (rule exp_less_mono)
  2099   apply (rule mult_strict_left_mono_neg)
  2100   apply (subst ln_less_cancel_iff)
  2101   apply assumption
  2102   apply (rule order_less_trans)
  2103   prefer 2
  2104   apply assumption+
  2105   done
  2106 
  2107 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2108   apply (case_tac "a = 0", simp)
  2109   apply (case_tac "x = y", simp)
  2110   apply (metis less_eq_real_def powr_less_mono2)
  2111   done
  2112 
  2113 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2114   unfolding powr_def exp_inj_iff by simp
  2115 
  2116 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2117   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute 
  2118             order.strict_trans2 powr_gt_zero zero_less_one)
  2119 
  2120 lemma ln_powr_bound2:
  2121   assumes "1 < x" and "0 < a"
  2122   shows "(ln x) powr a <= (a powr a) * x"
  2123 proof -
  2124   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2125     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2126   also have "... = a * (x powr (1 / a))"
  2127     by simp
  2128   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2129     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2130   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2131     by (metis assms(2) powr_mult powr_gt_zero)
  2132   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2133     by (rule powr_powr)
  2134   also have "... = x" using assms
  2135     by auto
  2136   finally show ?thesis .
  2137 qed
  2138 
  2139 lemma tendsto_powr [tendsto_intros]:
  2140   "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2141   unfolding powr_def by (intro tendsto_intros)
  2142 
  2143 lemma continuous_powr:
  2144   assumes "continuous F f"
  2145     and "continuous F g"
  2146     and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  2147   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2148   using assms unfolding continuous_def by (rule tendsto_powr)
  2149 
  2150 lemma continuous_at_within_powr[continuous_intros]:
  2151   assumes "continuous (at a within s) f"
  2152     and "continuous (at a within s) g"
  2153     and "f a \<noteq> 0"
  2154   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2155   using assms unfolding continuous_within by (rule tendsto_powr)
  2156 
  2157 lemma isCont_powr[continuous_intros, simp]:
  2158   assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  2159   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2160   using assms unfolding continuous_at by (rule tendsto_powr)
  2161 
  2162 lemma continuous_on_powr[continuous_intros]:
  2163   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  2164   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2165   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2166 
  2167 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2168 lemma tendsto_zero_powrI:
  2169   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2170     and "0 < d"
  2171   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2172 proof (rule tendstoI)
  2173   fix e :: real assume "0 < e"
  2174   def Z \<equiv> "e powr (1 / d)"
  2175   with `0 < e` have "0 < Z" by simp
  2176   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2177     by (intro eventually_conj tendstoD)
  2178   moreover
  2179   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2180     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2181   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2182     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2183   ultimately
  2184   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2185 qed
  2186 
  2187 lemma tendsto_neg_powr:
  2188   assumes "s < 0"
  2189     and "LIM x F. f x :> at_top"
  2190   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2191 proof (rule tendstoI)
  2192   fix e :: real assume "0 < e"
  2193   def Z \<equiv> "e powr (1 / s)"
  2194   from assms have "eventually (\<lambda>x. Z < f x) F"
  2195     by (simp add: filterlim_at_top_dense)
  2196   moreover
  2197   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2198     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2199   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2200     by (simp add: powr_powr Z_def dist_real_def)
  2201   ultimately
  2202   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2203 qed
  2204 
  2205 (* it is funny that this isn't in the library! It could go in Transcendental *)
  2206 lemma tendsto_exp_limit_at_right:
  2207   fixes x :: real
  2208   shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  2209 proof cases
  2210   assume "x \<noteq> 0"
  2211 
  2212   have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  2213     by (auto intro!: derivative_eq_intros)
  2214   then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  2215     by (auto simp add: has_field_derivative_def field_has_derivative_at) 
  2216   then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  2217     by (rule tendsto_intros)
  2218   then show ?thesis
  2219   proof (rule filterlim_mono_eventually)
  2220     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  2221       unfolding eventually_at_right[OF zero_less_one]
  2222       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  2223   qed (simp_all add: at_eq_sup_left_right)
  2224 qed (simp add: tendsto_const)
  2225 
  2226 lemma tendsto_exp_limit_at_top:
  2227   fixes x :: real
  2228   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  2229   apply (subst filterlim_at_top_to_right)
  2230   apply (simp add: inverse_eq_divide)
  2231   apply (rule tendsto_exp_limit_at_right)
  2232   done
  2233 
  2234 lemma tendsto_exp_limit_sequentially:
  2235   fixes x :: real
  2236   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  2237 proof (rule filterlim_mono_eventually)
  2238   from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  2239   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  2240     apply (intro eventually_sequentiallyI [of n])
  2241     apply (case_tac "x \<ge> 0")
  2242     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  2243     apply (subgoal_tac "x / real xa > -1")
  2244     apply (auto simp add: field_simps)
  2245     done
  2246   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  2247     by (rule eventually_elim1) (erule powr_realpow)
  2248   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  2249     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  2250 qed auto
  2251 
  2252 subsection {* Sine and Cosine *}
  2253 
  2254 definition sin_coeff :: "nat \<Rightarrow> real" where
  2255   "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
  2256 
  2257 definition cos_coeff :: "nat \<Rightarrow> real" where
  2258   "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
  2259 
  2260 definition sin :: "real \<Rightarrow> real"
  2261   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
  2262 
  2263 definition cos :: "real \<Rightarrow> real"
  2264   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
  2265 
  2266 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2267   unfolding sin_coeff_def by simp
  2268 
  2269 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2270   unfolding cos_coeff_def by simp
  2271 
  2272 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2273   unfolding cos_coeff_def sin_coeff_def
  2274   by (simp del: mult_Suc)
  2275 
  2276 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2277   unfolding cos_coeff_def sin_coeff_def
  2278   by (simp del: mult_Suc) (auto elim: oddE)
  2279 
  2280 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
  2281   unfolding sin_coeff_def
  2282   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2283   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2284   done
  2285 
  2286 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
  2287   unfolding cos_coeff_def
  2288   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2289   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2290   done
  2291 
  2292 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
  2293   unfolding sin_def by (rule summable_sin [THEN summable_sums])
  2294 
  2295 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
  2296   unfolding cos_def by (rule summable_cos [THEN summable_sums])
  2297 
  2298 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2299   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2300 
  2301 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2302   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2303 
  2304 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2305 
  2306 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  2307   unfolding sin_def cos_def
  2308   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2309   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
  2310     summable_minus summable_sin summable_cos)
  2311   done
  2312 
  2313 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2314 
  2315 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  2316   unfolding cos_def sin_def
  2317   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2318   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
  2319     summable_minus summable_sin summable_cos suminf_minus)
  2320   done
  2321 
  2322 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2323 
  2324 lemma isCont_sin: "isCont sin x"
  2325   by (rule DERIV_sin [THEN DERIV_isCont])
  2326 
  2327 lemma isCont_cos: "isCont cos x"
  2328   by (rule DERIV_cos [THEN DERIV_isCont])
  2329 
  2330 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2331   by (rule isCont_o2 [OF _ isCont_sin])
  2332 
  2333 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2334   by (rule isCont_o2 [OF _ isCont_cos])
  2335 
  2336 lemma tendsto_sin [tendsto_intros]:
  2337   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2338   by (rule isCont_tendsto_compose [OF isCont_sin])
  2339 
  2340 lemma tendsto_cos [tendsto_intros]:
  2341   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2342   by (rule isCont_tendsto_compose [OF isCont_cos])
  2343 
  2344 lemma continuous_sin [continuous_intros]:
  2345   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2346   unfolding continuous_def by (rule tendsto_sin)
  2347 
  2348 lemma continuous_on_sin [continuous_intros]:
  2349   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2350   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2351 
  2352 lemma continuous_cos [continuous_intros]:
  2353   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2354   unfolding continuous_def by (rule tendsto_cos)
  2355 
  2356 lemma continuous_on_cos [continuous_intros]:
  2357   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2358   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2359 
  2360 subsection {* Properties of Sine and Cosine *}
  2361 
  2362 lemma sin_zero [simp]: "sin 0 = 0"
  2363   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
  2364 
  2365 lemma cos_zero [simp]: "cos 0 = 1"
  2366   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
  2367 
  2368 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2369 proof -
  2370   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  2371     by (auto intro!: derivative_eq_intros)
  2372   hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  2373     by (rule DERIV_isconst_all)
  2374   thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  2375 qed
  2376 
  2377 lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2378   by (subst add.commute, rule sin_cos_squared_add)
  2379 
  2380 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  2381   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2382 
  2383 lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2384   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2385 
  2386 lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2387   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2388 
  2389 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  2390   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2391 
  2392 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  2393   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2394 
  2395 lemma sin_le_one [simp]: "sin x \<le> 1"
  2396   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2397 
  2398 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  2399   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2400 
  2401 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  2402   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2403 
  2404 lemma cos_le_one [simp]: "cos x \<le> 1"
  2405   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2406 
  2407 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2408       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2409   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2410 
  2411 lemma DERIV_fun_exp:
  2412      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2413   by (auto intro!: derivative_intros)
  2414 
  2415 lemma DERIV_fun_sin:
  2416      "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2417   by (auto intro!: derivative_intros)
  2418 
  2419 lemma DERIV_fun_cos:
  2420      "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2421   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2422 
  2423 lemma sin_cos_add_lemma:
  2424   "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  2425     (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
  2426   (is "?f x = 0")
  2427 proof -
  2428   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2429     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2430   hence "?f x = ?f 0"
  2431     by (rule DERIV_isconst_all)
  2432   thus ?thesis by simp
  2433 qed
  2434 
  2435 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  2436   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2437 
  2438 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  2439   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2440 
  2441 lemma sin_cos_minus_lemma:
  2442   "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  2443 proof -
  2444   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2445     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2446   hence "?f x = ?f 0"
  2447     by (rule DERIV_isconst_all)
  2448   thus ?thesis by simp
  2449 qed
  2450 
  2451 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  2452   using sin_cos_minus_lemma [where x=x] by simp
  2453 
  2454 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  2455   using sin_cos_minus_lemma [where x=x] by simp
  2456 
  2457 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  2458   using sin_add [of x "- y"] by simp
  2459 
  2460 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  2461   by (simp add: sin_diff mult.commute)
  2462 
  2463 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  2464   using cos_add [of x "- y"] by simp
  2465 
  2466 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  2467   by (simp add: cos_diff mult.commute)
  2468 
  2469 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  2470   using sin_add [where x=x and y=x] by simp
  2471 
  2472 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
  2473   using cos_add [where x=x and y=x]
  2474   by (simp add: power2_eq_square)
  2475 
  2476 lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
  2477 proof -
  2478   let ?f = "\<lambda>x. x - sin x"
  2479   from x have "?f x \<ge> ?f 0"
  2480     apply (rule DERIV_nonneg_imp_nondecreasing)
  2481     apply (intro allI impI exI[of _ "1 - cos x" for x])
  2482     apply (auto intro!: derivative_eq_intros simp: field_simps)
  2483     done
  2484   thus "sin x \<le> x" by simp
  2485 qed
  2486 
  2487 lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  2488 proof -
  2489   let ?f = "\<lambda>x. x + sin x"
  2490   from x have "?f x \<ge> ?f 0"
  2491     apply (rule DERIV_nonneg_imp_nondecreasing)
  2492     apply (intro allI impI exI[of _ "1 + cos x" for x])
  2493     apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  2494     done
  2495   thus "sin x \<ge> -x" by simp
  2496 qed
  2497 
  2498 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  2499   using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
  2500   by (auto simp: abs_real_def)
  2501 
  2502 subsection {* The Constant Pi *}
  2503 
  2504 definition pi :: real
  2505   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2506 
  2507 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2508    hence define pi.*}
  2509 
  2510 lemma sin_paired:
  2511   "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  2512 proof -
  2513   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2514     by (rule sin_converges [THEN sums_group], simp)
  2515   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
  2516 qed
  2517 
  2518 lemma sin_gt_zero:
  2519   assumes "0 < x" and "x < 2"
  2520   shows "0 < sin x"
  2521 proof -
  2522   let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  2523   have pos: "\<forall>n. 0 < ?f n"
  2524   proof
  2525     fix n :: nat
  2526     let ?k2 = "real (Suc (Suc (4 * n)))"
  2527     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2528     have "x * x < ?k2 * ?k3"
  2529       using assms by (intro mult_strict_mono', simp_all)
  2530     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2531       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2532     thus "0 < ?f n"
  2533       by (simp del: mult_Suc,
  2534         simp add: less_divide_eq field_simps del: mult_Suc)
  2535   qed
  2536   have sums: "?f sums sin x"
  2537     by (rule sin_paired [THEN sums_group], simp)
  2538   show "0 < sin x"
  2539     unfolding sums_unique [OF sums]
  2540     using sums_summable [OF sums] pos
  2541     by (rule suminf_pos)
  2542 qed
  2543 
  2544 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2545   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
  2546 
  2547 lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  2548 proof -
  2549   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2550     by (rule cos_converges [THEN sums_group], simp)
  2551   thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
  2552 qed
  2553 
  2554 lemmas realpow_num_eq_if = power_eq_if
  2555 
  2556 lemma sumr_pos_lt_pair:
  2557   fixes f :: "nat \<Rightarrow> real"
  2558   shows "\<lbrakk>summable f;
  2559         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2560       \<Longrightarrow> setsum f {..<k} < suminf f"
  2561 unfolding One_nat_def
  2562 apply (subst suminf_split_initial_segment [where k="k"])
  2563 apply assumption
  2564 apply simp
  2565 apply (drule_tac k="k" in summable_ignore_initial_segment)
  2566 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2567 apply simp
  2568 apply (frule sums_unique)
  2569 apply (drule sums_summable)
  2570 apply simp
  2571 apply (erule suminf_pos)
  2572 apply (simp add: ac_simps)
  2573 done
  2574 
  2575 lemma cos_two_less_zero [simp]:
  2576   "cos 2 < 0"
  2577 proof -
  2578   note fact_Suc [simp del]
  2579   from cos_paired
  2580   have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  2581     by (rule sums_minus)
  2582   then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  2583     by simp
  2584   then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2585     by (rule sums_summable)
  2586   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2587     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  2588   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  2589     < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2590   proof -
  2591     { fix d
  2592       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2593        < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2594            fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2595         by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  2596       then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2597         < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2598         by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  2599       then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  2600         < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2601         by (simp add: inverse_eq_divide less_divide_eq)
  2602     }
  2603     note *** = this
  2604     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2605     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2606       (simp add: divide_inverse mult.assoc [symmetric] ***)
  2607   qed
  2608   ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2609     by (rule order_less_trans)
  2610   moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2611     by (rule sums_unique)
  2612   ultimately have "0 < - cos 2" by simp
  2613   then show ?thesis by simp
  2614 qed
  2615 
  2616 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2617 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2618 
  2619 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2620 proof (rule ex_ex1I)
  2621   show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
  2622     by (rule IVT2, simp_all)
  2623 next
  2624   fix x y
  2625   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2626   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2627   have [simp]: "\<forall>x. cos differentiable (at x)"
  2628     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2629   from x y show "x = y"
  2630     apply (cut_tac less_linear [of x y], auto)
  2631     apply (drule_tac f = cos in Rolle)
  2632     apply (drule_tac [5] f = cos in Rolle)
  2633     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2634     apply (metis order_less_le_trans less_le sin_gt_zero)
  2635     apply (metis order_less_le_trans less_le sin_gt_zero)
  2636     done
  2637 qed
  2638 
  2639 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2640   by (simp add: pi_def)
  2641 
  2642 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2643   by (simp add: pi_half cos_is_zero [THEN theI'])
  2644 
  2645 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2646   apply (rule order_le_neq_trans)
  2647   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2648   apply (metis cos_pi_half cos_zero zero_neq_one)
  2649   done
  2650 
  2651 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2652 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2653 
  2654 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2655   apply (rule order_le_neq_trans)
  2656   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2657   apply (metis cos_pi_half cos_two_neq_zero)
  2658   done
  2659 
  2660 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2661 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2662 
  2663 lemma pi_gt_zero [simp]: "0 < pi"
  2664   using pi_half_gt_zero by simp
  2665 
  2666 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2667   by (rule pi_gt_zero [THEN order_less_imp_le])
  2668 
  2669 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2670   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2671 
  2672 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2673   by (simp add: linorder_not_less)
  2674 
  2675 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2676   by simp
  2677 
  2678 lemma m2pi_less_pi: "- (2 * pi) < pi"
  2679   by simp
  2680 
  2681 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2682   using sin_cos_squared_add2 [where x = "pi/2"]
  2683   using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
  2684   by (simp add: power2_eq_1_iff)
  2685 
  2686 lemma cos_pi [simp]: "cos pi = -1"
  2687   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  2688 
  2689 lemma sin_pi [simp]: "sin pi = 0"
  2690   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  2691 
  2692 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  2693   by (simp add: cos_diff)
  2694 
  2695 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  2696   by (simp add: cos_add)
  2697 
  2698 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  2699   by (simp add: sin_diff)
  2700 
  2701 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  2702   by (simp add: sin_add)
  2703 
  2704 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  2705   by (simp add: sin_add)
  2706 
  2707 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  2708   by (simp add: cos_add)
  2709 
  2710 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  2711   by (simp add: sin_add cos_double)
  2712 
  2713 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  2714   by (simp add: cos_add cos_double)
  2715 
  2716 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  2717   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2718 
  2719 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  2720   by (metis cos_npi mult.commute)
  2721 
  2722 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  2723   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2724 
  2725 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  2726   by (simp add: mult.commute [of pi])
  2727 
  2728 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  2729   by (simp add: cos_double)
  2730 
  2731 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  2732   by simp
  2733 
  2734 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  2735   by (metis sin_gt_zero order_less_trans pi_half_less_two)
  2736 
  2737 lemma sin_less_zero:
  2738   assumes "- pi/2 < x" and "x < 0"
  2739   shows "sin x < 0"
  2740 proof -
  2741   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  2742   thus ?thesis by simp
  2743 qed
  2744 
  2745 lemma pi_less_4: "pi < 4"
  2746   using pi_half_less_two by auto
  2747 
  2748 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  2749   apply (cut_tac pi_less_4)
  2750   apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  2751   apply (cut_tac cos_is_zero, safe)
  2752   apply (rename_tac y z)
  2753   apply (drule_tac x = y in spec)
  2754   apply (drule_tac x = "pi/2" in spec, simp)
  2755   done
  2756 
  2757 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  2758   apply (rule_tac x = x and y = 0 in linorder_cases)
  2759   apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
  2760   apply (auto intro: cos_gt_zero)
  2761   done
  2762 
  2763 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  2764   apply (auto simp add: order_le_less cos_gt_zero_pi)
  2765   apply (subgoal_tac "x = pi/2", auto)
  2766   done
  2767 
  2768 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  2769   by (simp add: sin_cos_eq cos_gt_zero_pi)
  2770 
  2771 lemma pi_ge_two: "2 \<le> pi"
  2772 proof (rule ccontr)
  2773   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  2774   have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
  2775   proof (cases "2 < 2 * pi")
  2776     case True with dense[OF `pi < 2`] show ?thesis by auto
  2777   next
  2778     case False have "pi < 2 * pi" by auto
  2779     from dense[OF this] and False show ?thesis by auto
  2780   qed
  2781   then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
  2782   hence "0 < sin y" using sin_gt_zero by auto
  2783   moreover
  2784   have "sin y < 0" using sin_gt_zero_pi[of "y - pi"] `pi < y` and `y < 2 * pi` sin_periodic_pi[of "y - pi"] by auto
  2785   ultimately show False by auto
  2786 qed
  2787 
  2788 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  2789   by (auto simp add: order_le_less sin_gt_zero_pi)
  2790 
  2791 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  2792   It should be possible to factor out some of the common parts. *}
  2793 
  2794 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  2795 proof (rule ex_ex1I)
  2796   assume y: "-1 \<le> y" "y \<le> 1"
  2797   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  2798     by (rule IVT2, simp_all add: y)
  2799 next
  2800   fix a b
  2801   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  2802   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  2803   have [simp]: "\<forall>x. cos differentiable (at x)"
  2804     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2805   from a b show "a = b"
  2806     apply (cut_tac less_linear [of a b], auto)
  2807     apply (drule_tac f = cos in Rolle)
  2808     apply (drule_tac [5] f = cos in Rolle)
  2809     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2810     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2811     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2812     done
  2813 qed
  2814 
  2815 lemma sin_total:
  2816      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  2817 apply (rule ccontr)
  2818 apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
  2819 apply (erule contrapos_np)
  2820 apply simp
  2821 apply (cut_tac y="-y" in cos_total, simp) apply simp
  2822 apply (erule ex1E)
  2823 apply (rule_tac a = "x - (pi/2)" in ex1I)
  2824 apply (simp (no_asm) add: add.assoc)
  2825 apply (rotate_tac 3)
  2826 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
  2827 done
  2828 
  2829 lemma reals_Archimedean4:
  2830      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  2831 apply (auto dest!: reals_Archimedean3)
  2832 apply (drule_tac x = x in spec, clarify)
  2833 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  2834  prefer 2 apply (erule LeastI)
  2835 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  2836 apply (rename_tac m)
  2837 apply (subgoal_tac "~ x < real m * y")
  2838  prefer 2 apply (rule not_less_Least, simp, force)
  2839 done
  2840 
  2841 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic
  2842    now causes some unwanted re-arrangements of literals!   *)
  2843 lemma cos_zero_lemma:
  2844      "[| 0 \<le> x; cos x = 0 |] ==>
  2845       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  2846 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  2847 apply (subgoal_tac "0 \<le> x - real n * pi &
  2848                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  2849 apply (auto simp add: algebra_simps real_of_nat_Suc)
  2850  prefer 2 apply (simp add: cos_diff)
  2851 apply (simp add: cos_diff)
  2852 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  2853 apply (rule_tac [2] cos_total, safe)
  2854 apply (drule_tac x = "x - real n * pi" in spec)
  2855 apply (drule_tac x = "pi/2" in spec)
  2856 apply (simp add: cos_diff)
  2857 apply (rule_tac x = "Suc (2 * n)" in exI)
  2858 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  2859 done
  2860 
  2861 lemma sin_zero_lemma:
  2862      "[| 0 \<le> x; sin x = 0 |] ==>
  2863       \<exists>n::nat. even n & x = real n * (pi/2)"
  2864 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  2865  apply (clarify, rule_tac x = "n - 1" in exI)
  2866  apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
  2867  apply (rule cos_zero_lemma)
  2868  apply (auto simp add: cos_add)
  2869 done
  2870 
  2871 lemma cos_zero_iff:
  2872      "(cos x = 0) =
  2873       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
  2874        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  2875 proof -
  2876   { fix n :: nat
  2877     assume "odd n"
  2878     then obtain m where "n = 2 * m + 1" ..
  2879     then have "cos (real n * pi / 2) = 0"
  2880       by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
  2881   } note * = this
  2882   show ?thesis
  2883   apply (rule iffI)
  2884   apply (cut_tac linorder_linear [of 0 x], safe)
  2885   apply (drule cos_zero_lemma, assumption+)
  2886   apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  2887   apply (auto dest: *)
  2888   done
  2889 qed
  2890 
  2891 (* ditto: but to a lesser extent *)
  2892 lemma sin_zero_iff:
  2893      "(sin x = 0) =
  2894       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  2895        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  2896 apply (rule iffI)
  2897 apply (cut_tac linorder_linear [of 0 x], safe)
  2898 apply (drule sin_zero_lemma, assumption+)
  2899 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  2900 apply (force simp add: minus_equation_iff [of x])
  2901 apply (auto elim: evenE)
  2902 done
  2903 
  2904 lemma cos_monotone_0_pi:
  2905   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  2906   shows "cos x < cos y"
  2907 proof -
  2908   have "- (x - y) < 0" using assms by auto
  2909 
  2910   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  2911   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  2912     by auto
  2913   hence "0 < z" and "z < pi" using assms by auto
  2914   hence "0 < sin z" using sin_gt_zero_pi by auto
  2915   hence "cos x - cos y < 0"
  2916     unfolding cos_diff minus_mult_commute[symmetric]
  2917     using `- (x - y) < 0` by (rule mult_pos_neg2)
  2918   thus ?thesis by auto
  2919 qed
  2920 
  2921 lemma cos_monotone_0_pi':
  2922   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  2923   shows "cos x \<le> cos y"
  2924 proof (cases "y < x")
  2925   case True
  2926   show ?thesis
  2927     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  2928 next
  2929   case False
  2930   hence "y = x" using `y \<le> x` by auto
  2931   thus ?thesis by auto
  2932 qed
  2933 
  2934 lemma cos_monotone_minus_pi_0:
  2935   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  2936   shows "cos y < cos x"
  2937 proof -
  2938   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  2939     using assms by auto
  2940   from cos_monotone_0_pi[OF this] show ?thesis
  2941     unfolding cos_minus .
  2942 qed
  2943 
  2944 lemma cos_monotone_minus_pi_0':
  2945   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  2946   shows "cos y \<le> cos x"
  2947 proof (cases "y < x")
  2948   case True
  2949   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  2950     by auto
  2951 next
  2952   case False
  2953   hence "y = x" using `y \<le> x` by auto
  2954   thus ?thesis by auto
  2955 qed
  2956 
  2957 lemma sin_monotone_2pi':
  2958   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  2959   shows "sin y \<le> sin x"
  2960 proof -
  2961   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  2962     using pi_ge_two and assms by auto
  2963   from cos_monotone_0_pi'[OF this] show ?thesis
  2964     unfolding minus_sin_cos_eq[symmetric] by auto
  2965 qed
  2966 
  2967 
  2968 subsection {* Tangent *}
  2969 
  2970 definition tan :: "real \<Rightarrow> real"
  2971   where "tan = (\<lambda>x. sin x / cos x)"
  2972 
  2973 lemma tan_zero [simp]: "tan 0 = 0"
  2974   by (simp add: tan_def)
  2975 
  2976 lemma tan_pi [simp]: "tan pi = 0"
  2977   by (simp add: tan_def)
  2978 
  2979 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  2980   by (simp add: tan_def)
  2981 
  2982 lemma tan_minus [simp]: "tan (-x) = - tan x"
  2983   by (simp add: tan_def)
  2984 
  2985 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  2986   by (simp add: tan_def)
  2987 
  2988 lemma lemma_tan_add1:
  2989   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  2990   by (simp add: tan_def cos_add field_simps)
  2991 
  2992 lemma add_tan_eq:
  2993   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  2994   by (simp add: tan_def sin_add field_simps)
  2995 
  2996 lemma tan_add:
  2997      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  2998       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  2999   by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  3000 
  3001 lemma tan_double:
  3002      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  3003       ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  3004   using tan_add [of x x] by (simp add: power2_eq_square)
  3005 
  3006 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  3007   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  3008 
  3009 lemma tan_less_zero:
  3010   assumes lb: "- pi/2 < x" and "x < 0"
  3011   shows "tan x < 0"
  3012 proof -
  3013   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  3014   thus ?thesis by simp
  3015 qed
  3016 
  3017 lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  3018   unfolding tan_def sin_double cos_double sin_squared_eq
  3019   by (simp add: power2_eq_square)
  3020 
  3021 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  3022   unfolding tan_def
  3023   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  3024 
  3025 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  3026   by (rule DERIV_tan [THEN DERIV_isCont])
  3027 
  3028 lemma isCont_tan' [simp]:
  3029   "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  3030   by (rule isCont_o2 [OF _ isCont_tan])
  3031 
  3032 lemma tendsto_tan [tendsto_intros]:
  3033   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  3034   by (rule isCont_tendsto_compose [OF isCont_tan])
  3035 
  3036 lemma continuous_tan:
  3037   "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  3038   unfolding continuous_def by (rule tendsto_tan)
  3039 
  3040 lemma isCont_tan'' [continuous_intros]:
  3041   "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  3042   unfolding continuous_at by (rule tendsto_tan)
  3043 
  3044 lemma continuous_within_tan [continuous_intros]:
  3045   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  3046   unfolding continuous_within by (rule tendsto_tan)
  3047 
  3048 lemma continuous_on_tan [continuous_intros]:
  3049   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  3050   unfolding continuous_on_def by (auto intro: tendsto_tan)
  3051 
  3052 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  3053   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  3054 
  3055 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  3056   apply (cut_tac LIM_cos_div_sin)
  3057   apply (simp only: LIM_eq)
  3058   apply (drule_tac x = "inverse y" in spec, safe, force)
  3059   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  3060   apply (rule_tac x = "(pi/2) - e" in exI)
  3061   apply (simp (no_asm_simp))
  3062   apply (drule_tac x = "(pi/2) - e" in spec)
  3063   apply (auto simp add: tan_def sin_diff cos_diff)
  3064   apply (rule inverse_less_iff_less [THEN iffD1])
  3065   apply (auto simp add: divide_inverse)
  3066   apply (rule mult_pos_pos)
  3067   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  3068   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult.commute)
  3069   done
  3070 
  3071 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  3072   apply (frule order_le_imp_less_or_eq, safe)
  3073    prefer 2 apply force
  3074   apply (drule lemma_tan_total, safe)
  3075   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  3076   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  3077   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  3078   apply (auto dest: cos_gt_zero)
  3079   done
  3080 
  3081 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3082   apply (cut_tac linorder_linear [of 0 y], safe)
  3083   apply (drule tan_total_pos)
  3084   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  3085   apply (rule_tac [3] x = "-x" in exI)
  3086   apply (auto del: exI intro!: exI)
  3087   done
  3088 
  3089 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3090   apply (cut_tac y = y in lemma_tan_total1, auto)
  3091   apply hypsubst_thin
  3092   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  3093   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  3094   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  3095   apply (rule_tac [4] Rolle)
  3096   apply (rule_tac [2] Rolle)
  3097   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  3098               simp add: real_differentiable_def)
  3099   txt{*Now, simulate TRYALL*}
  3100   apply (rule_tac [!] DERIV_tan asm_rl)
  3101   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  3102               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  3103   done
  3104 
  3105 lemma tan_monotone:
  3106   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  3107   shows "tan y < tan x"
  3108 proof -
  3109   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  3110   proof (rule allI, rule impI)
  3111     fix x' :: real
  3112     assume "y \<le> x' \<and> x' \<le> x"
  3113     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  3114     from cos_gt_zero_pi[OF this]
  3115     have "cos x' \<noteq> 0" by auto
  3116     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  3117   qed
  3118   from MVT2[OF `y < x` this]
  3119   obtain z where "y < z" and "z < x"
  3120     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  3121   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  3122   hence "0 < cos z" using cos_gt_zero_pi by auto
  3123   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  3124   have "0 < x - y" using `y < x` by auto
  3125   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  3126   thus ?thesis by auto
  3127 qed
  3128 
  3129 lemma tan_monotone':
  3130   assumes "- (pi / 2) < y"
  3131     and "y < pi / 2"
  3132     and "- (pi / 2) < x"
  3133     and "x < pi / 2"
  3134   shows "(y < x) = (tan y < tan x)"
  3135 proof
  3136   assume "y < x"
  3137   thus "tan y < tan x"
  3138     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  3139 next
  3140   assume "tan y < tan x"
  3141   show "y < x"
  3142   proof (rule ccontr)
  3143     assume "\<not> y < x" hence "x \<le> y" by auto
  3144     hence "tan x \<le> tan y"
  3145     proof (cases "x = y")
  3146       case True thus ?thesis by auto
  3147     next
  3148       case False hence "x < y" using `x \<le> y` by auto
  3149       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  3150     qed
  3151     thus False using `tan y < tan x` by auto
  3152   qed
  3153 qed
  3154 
  3155 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  3156   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3157 
  3158 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3159   by (simp add: tan_def)
  3160 
  3161 lemma tan_periodic_nat[simp]:
  3162   fixes n :: nat
  3163   shows "tan (x + real n * pi) = tan x"
  3164 proof (induct n arbitrary: x)
  3165   case 0
  3166   then show ?case by simp
  3167 next
  3168   case (Suc n)
  3169   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3170     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3171   show ?case unfolding split_pi_off using Suc by auto
  3172 qed
  3173 
  3174 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3175 proof (cases "0 \<le> i")
  3176   case True
  3177   hence i_nat: "real i = real (nat i)" by auto
  3178   show ?thesis unfolding i_nat by auto
  3179 next
  3180   case False
  3181   hence i_nat: "real i = - real (nat (-i))" by auto
  3182   have "tan x = tan (x + real i * pi - real i * pi)"
  3183     by auto
  3184   also have "\<dots> = tan (x + real i * pi)"
  3185     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3186   finally show ?thesis by auto
  3187 qed
  3188 
  3189 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3190   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3191 
  3192 subsection {* Inverse Trigonometric Functions *}
  3193 
  3194 definition arcsin :: "real => real"
  3195   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3196 
  3197 definition arccos :: "real => real"
  3198   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3199 
  3200 definition arctan :: "real => real"
  3201   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3202 
  3203 lemma arcsin:
  3204   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3205     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3206   unfolding arcsin_def by (rule theI' [OF sin_total])
  3207 
  3208 lemma arcsin_pi:
  3209   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3210   apply (drule (1) arcsin)
  3211   apply (force intro: order_trans)
  3212   done
  3213 
  3214 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3215   by (blast dest: arcsin)
  3216 
  3217 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3218   by (blast dest: arcsin)
  3219 
  3220 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3221   by (blast dest: arcsin)
  3222 
  3223 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3224   by (blast dest: arcsin)
  3225 
  3226 lemma arcsin_lt_bounded:
  3227      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  3228   apply (frule order_less_imp_le)
  3229   apply (frule_tac y = y in order_less_imp_le)
  3230   apply (frule arcsin_bounded)
  3231   apply (safe, simp)
  3232   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3233   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3234   apply (drule_tac [!] f = sin in arg_cong, auto)
  3235   done
  3236 
  3237 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  3238   apply (unfold arcsin_def)
  3239   apply (rule the1_equality)
  3240   apply (rule sin_total, auto)
  3241   done
  3242 
  3243 lemma arccos:
  3244      "[| -1 \<le> y; y \<le> 1 |]
  3245       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3246   unfolding arccos_def by (rule theI' [OF cos_total])
  3247 
  3248 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  3249   by (blast dest: arccos)
  3250 
  3251 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  3252   by (blast dest: arccos)
  3253 
  3254 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  3255   by (blast dest: arccos)
  3256 
  3257 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  3258   by (blast dest: arccos)
  3259 
  3260 lemma arccos_lt_bounded:
  3261      "[| -1 < y; y < 1 |]
  3262       ==> 0 < arccos y & arccos y < pi"
  3263   apply (frule order_less_imp_le)
  3264   apply (frule_tac y = y in order_less_imp_le)
  3265   apply (frule arccos_bounded, auto)
  3266   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3267   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3268   apply (drule_tac [!] f = cos in arg_cong, auto)
  3269   done
  3270 
  3271 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  3272   apply (simp add: arccos_def)
  3273   apply (auto intro!: the1_equality cos_total)
  3274   done
  3275 
  3276 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  3277   apply (simp add: arccos_def)
  3278   apply (auto intro!: the1_equality cos_total)
  3279   done
  3280 
  3281 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3282   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3283   apply (rule power2_eq_imp_eq)
  3284   apply (simp add: cos_squared_eq)
  3285   apply (rule cos_ge_zero)
  3286   apply (erule (1) arcsin_lbound)
  3287   apply (erule (1) arcsin_ubound)
  3288   apply simp
  3289   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3290   apply (rule power_mono, simp, simp)
  3291   done
  3292 
  3293 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3294   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3295   apply (rule power2_eq_imp_eq)
  3296   apply (simp add: sin_squared_eq)
  3297   apply (rule sin_ge_zero)
  3298   apply (erule (1) arccos_lbound)
  3299   apply (erule (1) arccos_ubound)
  3300   apply simp
  3301   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3302   apply (rule power_mono, simp, simp)
  3303   done
  3304 
  3305 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3306   unfolding arctan_def by (rule theI' [OF tan_total])
  3307 
  3308 lemma tan_arctan: "tan (arctan y) = y"
  3309   by auto
  3310 
  3311 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3312   by (auto simp only: arctan)
  3313 
  3314 lemma arctan_lbound: "- (pi/2) < arctan y"
  3315   by auto
  3316 
  3317 lemma arctan_ubound: "arctan y < pi/2"
  3318   by (auto simp only: arctan)
  3319 
  3320 lemma arctan_unique:
  3321   assumes "-(pi/2) < x"
  3322     and "x < pi/2"
  3323     and "tan x = y"
  3324   shows "arctan y = x"
  3325   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3326 
  3327 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3328   by (rule arctan_unique) simp_all
  3329 
  3330 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3331   by (rule arctan_unique) simp_all
  3332 
  3333 lemma arctan_minus: "arctan (- x) = - arctan x"
  3334   apply (rule arctan_unique)
  3335   apply (simp only: neg_less_iff_less arctan_ubound)
  3336   apply (metis minus_less_iff arctan_lbound)
  3337   apply simp
  3338   done
  3339 
  3340 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3341   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3342     arctan_lbound arctan_ubound)
  3343 
  3344 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3345 proof (rule power2_eq_imp_eq)
  3346   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3347   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3348   show "0 \<le> cos (arctan x)"
  3349     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3350   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3351     unfolding tan_def by (simp add: distrib_left power_divide)
  3352   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3353     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3354 qed
  3355 
  3356 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3357   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3358   using tan_arctan [of x] unfolding tan_def cos_arctan
  3359   by (simp add: eq_divide_eq)
  3360 
  3361 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3362   apply (rule power_inverse [THEN subst])
  3363   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3364   apply (auto dest: field_power_not_zero
  3365           simp add: power_mult_distrib distrib_right power_divide tan_def
  3366                     mult.assoc power_inverse [symmetric])
  3367   done
  3368 
  3369 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3370   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3371 
  3372 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3373   by (simp only: not_less [symmetric] arctan_less_iff)
  3374 
  3375 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3376   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3377 
  3378 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3379   using arctan_less_iff [of 0 x] by simp
  3380 
  3381 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3382   using arctan_less_iff [of x 0] by simp
  3383 
  3384 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3385   using arctan_le_iff [of 0 x] by simp
  3386 
  3387 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3388   using arctan_le_iff [of x 0] by simp
  3389 
  3390 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3391   using arctan_eq_iff [of x 0] by simp
  3392 
  3393 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3394 proof -
  3395   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3396     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3397   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3398   proof safe
  3399     fix x :: real
  3400     assume "x \<in> {-1..1}"
  3401     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3402       using arcsin_lbound arcsin_ubound
  3403       by (intro image_eqI[where x="arcsin x"]) auto
  3404   qed simp
  3405   finally show ?thesis .
  3406 qed
  3407 
  3408 lemma continuous_on_arcsin [continuous_intros]:
  3409   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arcsin (f x))"
  3410   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3411   by (auto simp: comp_def subset_eq)
  3412 
  3413 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3414   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3415   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3416 
  3417 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3418 proof -
  3419   have "continuous_on (cos ` {0 .. pi}) arccos"
  3420     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3421   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3422   proof safe
  3423     fix x :: real
  3424     assume "x \<in> {-1..1}"
  3425     then show "x \<in> cos ` {0..pi}"
  3426       using arccos_lbound arccos_ubound
  3427       by (intro image_eqI[where x="arccos x"]) auto
  3428   qed simp
  3429   finally show ?thesis .
  3430 qed
  3431 
  3432 lemma continuous_on_arccos [continuous_intros]:
  3433   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arccos (f x))"
  3434   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3435   by (auto simp: comp_def subset_eq)
  3436 
  3437 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3438   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3439   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3440 
  3441 lemma isCont_arctan: "isCont arctan x"
  3442   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3443   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3444   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3445   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3446   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3447   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3448   done
  3449 
  3450 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3451   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3452 
  3453 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3454   unfolding continuous_def by (rule tendsto_arctan)
  3455 
  3456 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3457   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3458 
  3459 lemma DERIV_arcsin:
  3460   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3461   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  3462   apply (rule DERIV_cong [OF DERIV_sin])
  3463   apply (simp add: cos_arcsin)
  3464   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3465   apply (rule power_strict_mono, simp, simp, simp)
  3466   apply assumption
  3467   apply assumption
  3468   apply simp
  3469   apply (erule (1) isCont_arcsin)
  3470   done
  3471 
  3472 lemma DERIV_arccos:
  3473   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3474   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  3475   apply (rule DERIV_cong [OF DERIV_cos])
  3476   apply (simp add: sin_arccos)
  3477   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3478   apply (rule power_strict_mono, simp, simp, simp)
  3479   apply assumption
  3480   apply assumption
  3481   apply simp
  3482   apply (erule (1) isCont_arccos)
  3483   done
  3484 
  3485 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3486   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3487   apply (rule DERIV_cong [OF DERIV_tan])
  3488   apply (rule cos_arctan_not_zero)
  3489   apply (simp add: power_inverse tan_sec [symmetric])
  3490   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3491   apply (simp add: add_pos_nonneg)
  3492   apply (simp, simp, simp, rule isCont_arctan)
  3493   done
  3494 
  3495 declare
  3496   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3497   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3498   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3499 
  3500 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3501   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  3502      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3503            intro!: tan_monotone exI[of _ "pi/2"])
  3504 
  3505 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3506   by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  3507      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3508            intro!: tan_monotone exI[of _ "pi/2"])
  3509 
  3510 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3511 proof (rule tendstoI)
  3512   fix e :: real
  3513   assume "0 < e"
  3514   def y \<equiv> "pi/2 - min (pi/2) e"
  3515   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3516     using `0 < e` by auto
  3517 
  3518   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3519   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3520     fix x
  3521     assume "tan y < x"
  3522     then have "arctan (tan y) < arctan x"
  3523       by (simp add: arctan_less_iff)
  3524     with y have "y < arctan x"
  3525       by (subst (asm) arctan_tan) simp_all
  3526     with arctan_ubound[of x, arith] y `0 < e`
  3527     show "dist (arctan x) (pi / 2) < e"
  3528       by (simp add: dist_real_def)
  3529   qed
  3530 qed
  3531 
  3532 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3533   unfolding filterlim_at_bot_mirror arctan_minus
  3534   by (intro tendsto_minus tendsto_arctan_at_top)
  3535 
  3536 
  3537 subsection {* More Theorems about Sin and Cos *}
  3538 
  3539 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3540 proof -
  3541   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3542   have nonneg: "0 \<le> ?c"
  3543     by (simp add: cos_ge_zero)
  3544   have "0 = cos (pi / 4 + pi / 4)"
  3545     by simp
  3546   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3547     by (simp only: cos_add power2_eq_square)
  3548   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3549     by (simp add: sin_squared_eq)
  3550   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3551     by (simp add: power_divide)
  3552   thus ?thesis
  3553     using nonneg by (rule power2_eq_imp_eq) simp
  3554 qed
  3555 
  3556 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  3557 proof -
  3558   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3559   have pos_c: "0 < ?c"
  3560     by (rule cos_gt_zero, simp, simp)
  3561   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3562     by simp
  3563   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3564     by (simp only: cos_add sin_add)
  3565   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3566     by (simp add: algebra_simps power2_eq_square)
  3567   finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  3568     using pos_c by (simp add: sin_squared_eq power_divide)
  3569   thus ?thesis
  3570     using pos_c [THEN order_less_imp_le]
  3571     by (rule power2_eq_imp_eq) simp
  3572 qed
  3573 
  3574 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  3575   by (simp add: sin_cos_eq cos_45)
  3576 
  3577 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  3578   by (simp add: sin_cos_eq cos_30)
  3579 
  3580 lemma cos_60: "cos (pi / 3) = 1 / 2"
  3581   apply (rule power2_eq_imp_eq)
  3582   apply (simp add: cos_squared_eq sin_60 power_divide)
  3583   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  3584   done
  3585 
  3586 lemma sin_30: "sin (pi / 6) = 1 / 2"
  3587   by (simp add: sin_cos_eq cos_60)
  3588 
  3589 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  3590   unfolding tan_def by (simp add: sin_30 cos_30)
  3591 
  3592 lemma tan_45: "tan (pi / 4) = 1"
  3593   unfolding tan_def by (simp add: sin_45 cos_45)
  3594 
  3595 lemma tan_60: "tan (pi / 3) = sqrt 3"
  3596   unfolding tan_def by (simp add: sin_60 cos_60)
  3597 
  3598 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  3599 proof -
  3600   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  3601     by (auto simp add: algebra_simps sin_add)
  3602   thus ?thesis
  3603     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  3604                   mult.commute [of pi])
  3605 qed
  3606 
  3607 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  3608   by (simp add: cos_double mult.assoc power_add [symmetric] numeral_2_eq_2)
  3609 
  3610 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  3611   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  3612   apply (subst cos_add, simp)
  3613   done
  3614 
  3615 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  3616   by (auto simp add: mult.assoc)
  3617 
  3618 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  3619   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  3620   apply (subst sin_add, simp)
  3621   done
  3622 
  3623 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  3624   apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  3625   apply auto
  3626   done
  3627 
  3628 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  3629   by (auto intro!: derivative_eq_intros)
  3630 
  3631 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  3632   by (auto simp add: sin_zero_iff elim: evenE)
  3633 
  3634 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  3635   using sin_cos_squared_add3 [where x = x] by auto
  3636 
  3637 
  3638 subsection {* Machins formula *}
  3639 
  3640 lemma arctan_one: "arctan 1 = pi / 4"
  3641   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  3642 
  3643 lemma tan_total_pi4:
  3644   assumes "\<bar>x\<bar> < 1"
  3645   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  3646 proof
  3647   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  3648     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3649     unfolding arctan_less_iff using assms by auto
  3650 qed
  3651 
  3652 lemma arctan_add:
  3653   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  3654   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  3655 proof (rule arctan_unique [symmetric])
  3656   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  3657     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3658     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3659   from add_le_less_mono [OF this]
  3660   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  3661   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  3662     unfolding arctan_one [symmetric]
  3663     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3664   from add_le_less_mono [OF this]
  3665   show 2: "arctan x + arctan y < pi / 2" by simp
  3666   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  3667     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  3668 qed
  3669 
  3670 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  3671 proof -
  3672   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  3673   from arctan_add[OF less_imp_le[OF this] this]
  3674   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  3675   moreover
  3676   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  3677   from arctan_add[OF less_imp_le[OF this] this]
  3678   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  3679   moreover
  3680   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  3681   from arctan_add[OF this]
  3682   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  3683   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  3684   thus ?thesis unfolding arctan_one by algebra
  3685 qed
  3686 
  3687 
  3688 subsection {* Introducing the arcus tangens power series *}
  3689 
  3690 lemma monoseq_arctan_series:
  3691   fixes x :: real
  3692   assumes "\<bar>x\<bar> \<le> 1"
  3693   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  3694 proof (cases "x = 0")
  3695   case True
  3696   thus ?thesis unfolding monoseq_def One_nat_def by auto
  3697 next
  3698   case False
  3699   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3700   show "monoseq ?a"
  3701   proof -
  3702     {
  3703       fix n
  3704       fix x :: real
  3705       assume "0 \<le> x" and "x \<le> 1"
  3706       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  3707         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  3708       proof (rule mult_mono)
  3709         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  3710           by (rule frac_le) simp_all
  3711         show "0 \<le> 1 / real (Suc (n * 2))"
  3712           by auto
  3713         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  3714           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  3715         show "0 \<le> x ^ Suc (Suc n * 2)"
  3716           by (rule zero_le_power) (simp add: `0 \<le> x`)
  3717       qed
  3718     } note mono = this
  3719 
  3720     show ?thesis
  3721     proof (cases "0 \<le> x")
  3722       case True from mono[OF this `x \<le> 1`, THEN allI]
  3723       show ?thesis unfolding Suc_eq_plus1[symmetric]
  3724         by (rule mono_SucI2)
  3725     next
  3726       case False
  3727       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  3728       from mono[OF this]
  3729       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  3730         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  3731       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  3732     qed
  3733   qed
  3734 qed
  3735 
  3736 lemma zeroseq_arctan_series:
  3737   fixes x :: real
  3738   assumes "\<bar>x\<bar> \<le> 1"
  3739   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  3740 proof (cases "x = 0")
  3741   case True
  3742   thus ?thesis
  3743     unfolding One_nat_def by (auto simp add: tendsto_const)
  3744 next
  3745   case False
  3746   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3747   show "?a ----> 0"
  3748   proof (cases "\<bar>x\<bar> < 1")
  3749     case True
  3750     hence "norm x < 1" by auto
  3751     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  3752     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  3753       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  3754     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  3755   next
  3756     case False
  3757     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3758     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  3759       unfolding One_nat_def by auto
  3760     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  3761     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  3762   qed
  3763 qed
  3764 
  3765 lemma summable_arctan_series:
  3766   fixes x :: real and n :: nat
  3767   assumes "\<bar>x\<bar> \<le> 1"
  3768   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3769   (is "summable (?c x)")
  3770   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  3771 
  3772 lemma less_one_imp_sqr_less_one:
  3773   fixes x :: real
  3774   assumes "\<bar>x\<bar> < 1"
  3775   shows "x\<^sup>2 < 1"
  3776 proof -
  3777   have "\<bar>x\<^sup>2\<bar> < 1"
  3778     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
  3779   thus ?thesis using zero_le_power2 by auto
  3780 qed
  3781 
  3782 lemma DERIV_arctan_series:
  3783   assumes "\<bar> x \<bar> < 1"
  3784   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))"
  3785   (is "DERIV ?arctan _ :> ?Int")
  3786 proof -
  3787   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  3788 
  3789   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  3790     by presburger
  3791   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  3792     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  3793     by auto
  3794 
  3795   {
  3796     fix x :: real
  3797     assume "\<bar>x\<bar> < 1"
  3798     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  3799     have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  3800       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`])
  3801     hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  3802   } note summable_Integral = this
  3803 
  3804   {
  3805     fix f :: "nat \<Rightarrow> real"
  3806     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3807     proof
  3808       fix x :: real
  3809       assume "f sums x"
  3810       from sums_if[OF sums_zero this]
  3811       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  3812         by auto
  3813     next
  3814       fix x :: real
  3815       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3816       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
  3817       show "f sums x" unfolding sums_def by auto
  3818     qed
  3819     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  3820   } note sums_even = this
  3821 
  3822   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  3823     unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  3824     by auto
  3825 
  3826   {
  3827     fix x :: real
  3828     have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  3829       (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  3830       using n_even by auto
  3831     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  3832     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  3833       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  3834       by auto
  3835   } note arctan_eq = this
  3836 
  3837   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  3838   proof (rule DERIV_power_series')
  3839     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  3840     {
  3841       fix x' :: real
  3842       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  3843       then have "\<bar>x'\<bar> < 1" by auto
  3844       then
  3845         have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  3846         by (rule summable_Integral)
  3847       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  3848       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  3849         apply (rule sums_summable [where l="0 + ?S"])
  3850         apply (rule sums_if)
  3851         apply (rule sums_zero)
  3852         apply (rule summable_sums)
  3853         apply (rule *)
  3854         done
  3855     }
  3856   qed auto
  3857   thus ?thesis unfolding Int_eq arctan_eq .
  3858 qed
  3859 
  3860 lemma arctan_series:
  3861   assumes "\<bar> x \<bar> \<le> 1"
  3862   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3863   (is "_ = suminf (\<lambda> n. ?c x n)")
  3864 proof -
  3865   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  3866 
  3867   {
  3868     fix r x :: real
  3869     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  3870     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  3871     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  3872   } note DERIV_arctan_suminf = this
  3873 
  3874   {
  3875     fix x :: real
  3876     assume "\<bar>x\<bar> \<le> 1"
  3877     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  3878   } note arctan_series_borders = this
  3879 
  3880   {
  3881     fix x :: real
  3882     assume "\<bar>x\<bar> < 1"
  3883     have "arctan x = (\<Sum>k. ?c x k)"
  3884     proof -
  3885       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  3886         using dense[OF `\<bar>x\<bar> < 1`] by blast
  3887       hence "0 < r" and "-r < x" and "x < r" by auto
  3888 
  3889       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  3890         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3891       proof -
  3892         fix x a b
  3893         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  3894         hence "\<bar>x\<bar> < r" by auto
  3895         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3896         proof (rule DERIV_isconst2[of "a" "b"])
  3897           show "a < b" and "a \<le> x" and "x \<le> b"
  3898             using `a < b` `a \<le> x` `x \<le> b` by auto
  3899           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3900           proof (rule allI, rule impI)
  3901             fix x
  3902             assume "-r < x \<and> x < r"
  3903             hence "\<bar>x\<bar> < r" by auto
  3904             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  3905             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  3906               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  3907             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  3908               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  3909             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  3910               unfolding power_mult_distrib[symmetric] power_mult mult.commute[of _ 2] by auto
  3911             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  3912               using sums_unique unfolding inverse_eq_divide by auto
  3913             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  3914               unfolding suminf_c'_eq_geom
  3915               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  3916             from DERIV_diff [OF this DERIV_arctan]
  3917             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3918               by auto
  3919           qed
  3920           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3921             using `-r < a` `b < r` by auto
  3922           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3923             using `\<bar>x\<bar> < r` by auto
  3924           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  3925             using DERIV_in_rball DERIV_isCont by auto
  3926         qed
  3927       qed
  3928 
  3929       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  3930         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  3931         by auto
  3932 
  3933       have "suminf (?c x) - arctan x = 0"
  3934       proof (cases "x = 0")
  3935         case True
  3936         thus ?thesis using suminf_arctan_zero by auto
  3937       next
  3938         case False
  3939         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  3940         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  3941           by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
  3942             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3943         moreover
  3944         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  3945           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
  3946              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3947         ultimately
  3948         show ?thesis using suminf_arctan_zero by auto
  3949       qed
  3950       thus ?thesis by auto
  3951     qed
  3952   } note when_less_one = this
  3953 
  3954   show "arctan x = suminf (\<lambda> n. ?c x n)"
  3955   proof (cases "\<bar>x\<bar> < 1")
  3956     case True
  3957     thus ?thesis by (rule when_less_one)
  3958   next
  3959     case False
  3960     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3961     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  3962     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  3963     {
  3964       fix n :: nat
  3965       have "0 < (1 :: real)" by auto
  3966       moreover
  3967       {
  3968         fix x :: real
  3969         assume "0 < x" and "x < 1"
  3970         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  3971         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  3972           by auto
  3973         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]
  3974         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  3975           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  3976         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  3977           by (rule abs_of_pos)
  3978         have "?diff x n \<le> ?a x n"
  3979         proof (cases "even n")
  3980           case True
  3981           hence sgn_pos: "(-1)^n = (1::real)" by auto
  3982           from `even n` obtain m where "n = 2 * m" ..
  3983           then have "2 * m = n" ..
  3984           from bounds[of m, unfolded this atLeastAtMost_iff]
  3985           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n + 1. (?c x i)) - (\<Sum>i<n. (?c x i))"
  3986             by auto
  3987           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  3988           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  3989           finally show ?thesis .
  3990         next
  3991           case False
  3992           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  3993           from `odd n` obtain m where "n = 2 * m + 1" ..
  3994           then have m_def: "2 * m + 1 = n" ..
  3995           hence m_plus: "2 * (m + 1) = n + 1" by auto
  3996           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  3997           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n. (?c x i)) - (\<Sum>i<n+1. (?c x i))"
  3998             by auto
  3999           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  4000           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  4001           finally show ?thesis .
  4002         qed
  4003         hence "0 \<le> ?a x n - ?diff x n" by auto
  4004       }
  4005       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  4006       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  4007         unfolding diff_conv_add_uminus divide_inverse
  4008         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  4009           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  4010           simp del: add_uminus_conv_diff)
  4011       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  4012         by (rule LIM_less_bound)
  4013       hence "?diff 1 n \<le> ?a 1 n" by auto
  4014     }
  4015     have "?a 1 ----> 0"
  4016       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  4017       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  4018     have "?diff 1 ----> 0"
  4019     proof (rule LIMSEQ_I)
  4020       fix r :: real
  4021       assume "0 < r"
  4022       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  4023         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  4024       {
  4025         fix n
  4026         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  4027         have "norm (?diff 1 n - 0) < r" by auto
  4028       }
  4029       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  4030     qed
  4031     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  4032     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  4033     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  4034 
  4035     show ?thesis
  4036     proof (cases "x = 1")
  4037       case True
  4038       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  4039     next
  4040       case False
  4041       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  4042 
  4043       have "- (pi / 2) < 0" using pi_gt_zero by auto
  4044       have "- (2 * pi) < 0" using pi_gt_zero by auto
  4045 
  4046       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  4047         unfolding One_nat_def by auto
  4048 
  4049       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  4050         unfolding tan_45 tan_minus ..
  4051       also have "\<dots> = - (pi / 4)"
  4052         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  4053       also have "\<dots> = - (arctan (tan (pi / 4)))"
  4054         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  4055       also have "\<dots> = - (arctan 1)"
  4056         unfolding tan_45 ..
  4057       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  4058         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  4059       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  4060         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  4061         unfolding c_minus_minus by auto
  4062       finally show ?thesis using `x = -1` by auto
  4063     qed
  4064   qed
  4065 qed
  4066 
  4067 lemma arctan_half:
  4068   fixes x :: real
  4069   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  4070 proof -
  4071   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  4072     using tan_total by blast
  4073   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  4074     by auto
  4075 
  4076   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
  4077   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
  4078     by auto
  4079 
  4080   have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4081     unfolding tan_def power_divide ..
  4082   also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4083     using `cos y \<noteq> 0` by auto
  4084   also have "\<dots> = 1 / (cos y)\<^sup>2"
  4085     unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
  4086   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
  4087 
  4088   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
  4089     unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
  4090   also have "\<dots> = tan y / (1 + 1 / cos y)"
  4091     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
  4092   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
  4093     unfolding cos_sqrt ..
  4094   also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
  4095     unfolding real_sqrt_divide by auto
  4096   finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
  4097     unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
  4098 
  4099   have "arctan x = y"
  4100     using arctan_tan low high y_eq by auto
  4101   also have "\<dots> = 2 * (arctan (tan (y/2)))"
  4102     using arctan_tan[OF low2 high2] by auto
  4103   also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
  4104     unfolding tan_half by auto
  4105   finally show ?thesis
  4106     unfolding eq `tan y = x` .
  4107 qed
  4108 
  4109 lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
  4110   by (simp only: arctan_less_iff)
  4111 
  4112 lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
  4113   by (simp only: arctan_le_iff)
  4114 
  4115 lemma arctan_inverse:
  4116   assumes "x \<noteq> 0"
  4117   shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
  4118 proof (rule arctan_unique)
  4119   show "- (pi / 2) < sgn x * pi / 2 - arctan x"
  4120     using arctan_bounded [of x] assms
  4121     unfolding sgn_real_def
  4122     apply (auto simp add: algebra_simps)
  4123     apply (drule zero_less_arctan_iff [THEN iffD2])
  4124     apply arith
  4125     done
  4126   show "sgn x * pi / 2 - arctan x < pi / 2"
  4127     using arctan_bounded [of "- x"] assms
  4128     unfolding sgn_real_def arctan_minus
  4129     by (auto simp add: algebra_simps)
  4130   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
  4131     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
  4132     unfolding sgn_real_def
  4133     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
  4134 qed
  4135 
  4136 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
  4137 proof -
  4138   have "pi / 4 = arctan 1" using arctan_one by auto
  4139   also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
  4140   finally show ?thesis by auto
  4141 qed
  4142 
  4143 
  4144 subsection {* Existence of Polar Coordinates *}
  4145 
  4146 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
  4147   apply (rule power2_le_imp_le [OF _ zero_le_one])
  4148   apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
  4149   done
  4150 
  4151 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  4152   by (simp add: abs_le_iff)
  4153 
  4154 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
  4155   by (simp add: sin_arccos abs_le_iff)
  4156 
  4157 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  4158 
  4159 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  4160 
  4161 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  4162 proof -
  4163   have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  4164     apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
  4165     apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
  4166     apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
  4167                      real_sqrt_mult [symmetric] right_diff_distrib)
  4168     done
  4169   show ?thesis
  4170   proof (cases "0::real" y rule: linorder_cases)
  4171     case less 
  4172       then show ?thesis by (rule polar_ex1)
  4173   next
  4174     case equal
  4175       then show ?thesis
  4176         by (force simp add: intro!: cos_zero sin_zero)
  4177   next
  4178     case greater
  4179       then show ?thesis 
  4180      using polar_ex1 [where y="-y"]
  4181     by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
  4182   qed
  4183 qed
  4184 
  4185 end