src/HOL/Transcendental.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58410 6d46ad54a2ab
child 58656 7f14d5d9b933
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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_field,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 isCont_exp: "isCont exp x"
  1005   by (rule DERIV_exp [THEN DERIV_isCont])
  1006 
  1007 lemma isCont_exp' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
  1008   by (rule isCont_o2 [OF _ isCont_exp])
  1009 
  1010 lemma tendsto_exp [tendsto_intros]:
  1011   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
  1012   by (rule isCont_tendsto_compose [OF isCont_exp])
  1013 
  1014 lemma continuous_exp [continuous_intros]:
  1015   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
  1016   unfolding continuous_def by (rule tendsto_exp)
  1017 
  1018 lemma continuous_on_exp [continuous_intros]:
  1019   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
  1020   unfolding continuous_on_def by (auto intro: tendsto_exp)
  1021 
  1022 
  1023 subsubsection {* Properties of the Exponential Function *}
  1024 
  1025 lemma powser_zero:
  1026   fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
  1027   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
  1028 proof -
  1029   have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
  1030     by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
  1031   thus ?thesis unfolding One_nat_def by simp
  1032 qed
  1033 
  1034 lemma exp_zero [simp]: "exp 0 = 1"
  1035   unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
  1036 
  1037 lemma exp_series_add:
  1038   fixes x y :: "'a::{real_field}"
  1039   defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
  1040   shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
  1041 proof (induct n)
  1042   case 0
  1043   show ?case
  1044     unfolding S_def by simp
  1045 next
  1046   case (Suc n)
  1047   have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
  1048     unfolding S_def by (simp del: mult_Suc)
  1049   hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
  1050     by simp
  1051 
  1052   have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
  1053     by (simp only: times_S)
  1054   also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1055     by (simp only: Suc)
  1056   also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
  1057                 + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1058     by (rule distrib_right)
  1059   also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
  1060                 + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
  1061     by (simp only: setsum_right_distrib ac_simps)
  1062   also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
  1063                 + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1064     by (simp add: times_S Suc_diff_le)
  1065   also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
  1066              (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
  1067     by (subst setsum_atMost_Suc_shift) simp
  1068   also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1069              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1070     by simp
  1071   also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
  1072              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1073              (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
  1074     by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
  1075                    real_of_nat_add [symmetric]) simp
  1076   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
  1077     by (simp only: scaleR_right.setsum)
  1078   finally show
  1079     "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
  1080     by (simp del: setsum_cl_ivl_Suc)
  1081 qed
  1082 
  1083 lemma exp_add: "exp (x + y) = exp x * exp y"
  1084   unfolding exp_def
  1085   by (simp only: Cauchy_product summable_norm_exp exp_series_add)
  1086 
  1087 lemma mult_exp_exp: "exp x * exp y = exp (x + y)"
  1088   by (rule exp_add [symmetric])
  1089 
  1090 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  1091   unfolding exp_def
  1092   apply (subst suminf_of_real)
  1093   apply (rule summable_exp_generic)
  1094   apply (simp add: scaleR_conv_of_real)
  1095   done
  1096 
  1097 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
  1098 proof
  1099   have "exp x * exp (- x) = 1" by (simp add: mult_exp_exp)
  1100   also assume "exp x = 0"
  1101   finally show "False" by simp
  1102 qed
  1103 
  1104 lemma exp_minus: "exp (- x) = inverse (exp x)"
  1105   by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
  1106 
  1107 lemma exp_diff: "exp (x - y) = exp x / exp y"
  1108   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
  1109 
  1110 
  1111 subsubsection {* Properties of the Exponential Function on Reals *}
  1112 
  1113 text {* Comparisons of @{term "exp x"} with zero. *}
  1114 
  1115 text{*Proof: because every exponential can be seen as a square.*}
  1116 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
  1117 proof -
  1118   have "0 \<le> exp (x/2) * exp (x/2)" by simp
  1119   thus ?thesis by (simp add: exp_add [symmetric])
  1120 qed
  1121 
  1122 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
  1123   by (simp add: order_less_le)
  1124 
  1125 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
  1126   by (simp add: not_less)
  1127 
  1128 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
  1129   by (simp add: not_le)
  1130 
  1131 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
  1132   by simp
  1133 
  1134 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  1135   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
  1136 
  1137 text {* Strict monotonicity of exponential. *}
  1138 
  1139 lemma exp_ge_add_one_self_aux: 
  1140   assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
  1141 using order_le_imp_less_or_eq [OF assms]
  1142 proof 
  1143   assume "0 < x"
  1144   have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
  1145     by (auto simp add: numeral_2_eq_2)
  1146   also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
  1147     apply (rule setsum_le_suminf [OF summable_exp])
  1148     using `0 < x`
  1149     apply (auto  simp add:  zero_le_mult_iff)
  1150     done
  1151   finally show "1+x \<le> exp x" 
  1152     by (simp add: exp_def)
  1153 next
  1154   assume "0 = x"
  1155   then show "1 + x \<le> exp x"
  1156     by auto
  1157 qed
  1158 
  1159 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
  1160 proof -
  1161   assume x: "0 < x"
  1162   hence "1 < 1 + x" by simp
  1163   also from x have "1 + x \<le> exp x"
  1164     by (simp add: exp_ge_add_one_self_aux)
  1165   finally show ?thesis .
  1166 qed
  1167 
  1168 lemma exp_less_mono:
  1169   fixes x y :: real
  1170   assumes "x < y"
  1171   shows "exp x < exp y"
  1172 proof -
  1173   from `x < y` have "0 < y - x" by simp
  1174   hence "1 < exp (y - x)" by (rule exp_gt_one)
  1175   hence "1 < exp y / exp x" by (simp only: exp_diff)
  1176   thus "exp x < exp y" by simp
  1177 qed
  1178 
  1179 lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
  1180   unfolding linorder_not_le [symmetric]
  1181   by (auto simp add: order_le_less exp_less_mono)
  1182 
  1183 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
  1184   by (auto intro: exp_less_mono exp_less_cancel)
  1185 
  1186 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
  1187   by (auto simp add: linorder_not_less [symmetric])
  1188 
  1189 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
  1190   by (simp add: order_eq_iff)
  1191 
  1192 text {* Comparisons of @{term "exp x"} with one. *}
  1193 
  1194 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
  1195   using exp_less_cancel_iff [where x=0 and y=x] by simp
  1196 
  1197 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
  1198   using exp_less_cancel_iff [where x=x and y=0] by simp
  1199 
  1200 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
  1201   using exp_le_cancel_iff [where x=0 and y=x] by simp
  1202 
  1203 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
  1204   using exp_le_cancel_iff [where x=x and y=0] by simp
  1205 
  1206 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
  1207   using exp_inj_iff [where x=x and y=0] by simp
  1208 
  1209 lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
  1210 proof (rule IVT)
  1211   assume "1 \<le> y"
  1212   hence "0 \<le> y - 1" by simp
  1213   hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
  1214   thus "y \<le> exp (y - 1)" by simp
  1215 qed (simp_all add: le_diff_eq)
  1216 
  1217 lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
  1218 proof (rule linorder_le_cases [of 1 y])
  1219   assume "1 \<le> y"
  1220   thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
  1221 next
  1222   assume "0 < y" and "y \<le> 1"
  1223   hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
  1224   then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
  1225   hence "exp (- x) = y" by (simp add: exp_minus)
  1226   thus "\<exists>x. exp x = y" ..
  1227 qed
  1228 
  1229 
  1230 subsection {* Natural Logarithm *}
  1231 
  1232 definition ln :: "real \<Rightarrow> real"
  1233   where "ln x = (THE u. exp u = x)"
  1234 
  1235 lemma ln_exp [simp]: "ln (exp x) = x"
  1236   by (simp add: ln_def)
  1237 
  1238 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
  1239   by (auto dest: exp_total)
  1240 
  1241 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
  1242   by (metis exp_gt_zero exp_ln)
  1243 
  1244 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
  1245   by (erule subst, rule ln_exp)
  1246 
  1247 lemma ln_one [simp]: "ln 1 = 0"
  1248   by (rule ln_unique) simp
  1249 
  1250 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
  1251   by (rule ln_unique) (simp add: exp_add)
  1252 
  1253 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
  1254   by (rule ln_unique) (simp add: exp_minus)
  1255 
  1256 lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  1257   by (rule ln_unique) (simp add: exp_diff)
  1258 
  1259 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
  1260   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  1261 
  1262 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  1263   by (subst exp_less_cancel_iff [symmetric]) simp
  1264 
  1265 lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
  1266   by (simp add: linorder_not_less [symmetric])
  1267 
  1268 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
  1269   by (simp add: order_eq_iff)
  1270 
  1271 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  1272   apply (rule exp_le_cancel_iff [THEN iffD1])
  1273   apply (simp add: exp_ge_add_one_self_aux)
  1274   done
  1275 
  1276 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  1277   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  1278 
  1279 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  1280   using ln_le_cancel_iff [of 1 x] by simp
  1281 
  1282 lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  1283   using ln_le_cancel_iff [of 1 x] by simp
  1284 
  1285 lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  1286   using ln_le_cancel_iff [of 1 x] by simp
  1287 
  1288 lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  1289   using ln_less_cancel_iff [of x 1] by simp
  1290 
  1291 lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  1292   using ln_less_cancel_iff [of 1 x] by simp
  1293 
  1294 lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  1295   using ln_less_cancel_iff [of 1 x] by simp
  1296 
  1297 lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  1298   using ln_less_cancel_iff [of 1 x] by simp
  1299 
  1300 lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  1301   using ln_inj_iff [of x 1] by simp
  1302 
  1303 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  1304   by simp
  1305 
  1306 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  1307   by (auto simp add: ln_def intro!: arg_cong[where f=The])
  1308 
  1309 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  1310 proof cases
  1311   assume "0 < x"
  1312   moreover then have "isCont ln (exp (ln x))"
  1313     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
  1314   ultimately show ?thesis
  1315     by simp
  1316 next
  1317   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
  1318     unfolding isCont_def
  1319     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
  1320        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
  1321                 intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
  1322 qed
  1323 
  1324 lemma tendsto_ln [tendsto_intros]:
  1325   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  1326   by (rule isCont_tendsto_compose [OF isCont_ln])
  1327 
  1328 lemma continuous_ln:
  1329   "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  1330   unfolding continuous_def by (rule tendsto_ln)
  1331 
  1332 lemma isCont_ln' [continuous_intros]:
  1333   "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  1334   unfolding continuous_at by (rule tendsto_ln)
  1335 
  1336 lemma continuous_within_ln [continuous_intros]:
  1337   "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  1338   unfolding continuous_within by (rule tendsto_ln)
  1339 
  1340 lemma continuous_on_ln [continuous_intros]:
  1341   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  1342   unfolding continuous_on_def by (auto intro: tendsto_ln)
  1343 
  1344 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  1345   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  1346   apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  1347   done
  1348 
  1349 lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  1350   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  1351 
  1352 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  1353 
  1354 lemma ln_series:
  1355   assumes "0 < x" and "x < 2"
  1356   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
  1357   (is "ln x = suminf (?f (x - 1))")
  1358 proof -
  1359   let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
  1360 
  1361   have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
  1362   proof (rule DERIV_isconst3[where x=x])
  1363     fix x :: real
  1364     assume "x \<in> {0 <..< 2}"
  1365     hence "0 < x" and "x < 2" by auto
  1366     have "norm (1 - x) < 1"
  1367       using `0 < x` and `x < 2` by auto
  1368     have "1 / x = 1 / (1 - (1 - x))" by auto
  1369     also have "\<dots> = (\<Sum> n. (1 - x)^n)"
  1370       using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
  1371     also have "\<dots> = suminf (?f' x)"
  1372       unfolding power_mult_distrib[symmetric]
  1373       by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
  1374     finally have "DERIV ln x :> suminf (?f' x)"
  1375       using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
  1376     moreover
  1377     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
  1378     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
  1379       (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
  1380     proof (rule DERIV_power_series')
  1381       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
  1382         using `0 < x` `x < 2` by auto
  1383       fix x :: real
  1384       assume "x \<in> {- 1<..<1}"
  1385       hence "norm (-x) < 1" by auto
  1386       show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
  1387         unfolding One_nat_def
  1388         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  1389     qed
  1390     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
  1391       unfolding One_nat_def by auto
  1392     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
  1393       unfolding DERIV_def repos .
  1394     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
  1395       by (rule DERIV_diff)
  1396     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
  1397   qed (auto simp add: assms)
  1398   thus ?thesis by auto
  1399 qed
  1400 
  1401 lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  1402 proof -
  1403   have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
  1404     by (simp add: exp_def)
  1405   also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) + 
  1406     (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
  1407     by (rule suminf_split_initial_segment)
  1408   also have "?a = 1 + x"
  1409     by (simp add: numeral_2_eq_2)
  1410   finally show ?thesis
  1411     by simp
  1412 qed
  1413 
  1414 lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
  1415 proof -
  1416   assume a: "0 <= x"
  1417   assume b: "x <= 1"
  1418   {
  1419     fix n :: nat
  1420     have "2 * 2 ^ n \<le> fact (n + 2)"
  1421       by (induct n) simp_all
  1422     hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
  1423       by (simp only: real_of_nat_le_iff)
  1424     hence "2 * 2 ^ n \<le> real (fact (n + 2))"
  1425       by simp
  1426     hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
  1427       by (rule le_imp_inverse_le) simp
  1428     hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
  1429       by (simp add: power_inverse)
  1430     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  1431       by (rule mult_mono)
  1432         (rule mult_mono, simp_all add: power_le_one a b)
  1433     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  1434       unfolding power_add by (simp add: ac_simps del: fact_Suc) }
  1435   note aux1 = this
  1436   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  1437     by (intro sums_mult geometric_sums, simp)
  1438   hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
  1439     by simp
  1440   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
  1441   proof -
  1442     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
  1443         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
  1444       apply (rule suminf_le)
  1445       apply (rule allI, rule aux1)
  1446       apply (rule summable_exp [THEN summable_ignore_initial_segment])
  1447       by (rule sums_summable, rule aux2)
  1448     also have "... = x\<^sup>2"
  1449       by (rule sums_unique [THEN sym], rule aux2)
  1450     finally show ?thesis .
  1451   qed
  1452   thus ?thesis unfolding exp_first_two_terms by auto
  1453 qed
  1454 
  1455 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  1456 proof -
  1457   assume a: "0 <= (x::real)" and b: "x < 1"
  1458   have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  1459     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
  1460   also have "... <= 1"
  1461     by (auto simp add: a)
  1462   finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
  1463   moreover have c: "0 < 1 + x + x\<^sup>2"
  1464     by (simp add: add_pos_nonneg a)
  1465   ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
  1466     by (elim mult_imp_le_div_pos)
  1467   also have "... <= 1 / exp x"
  1468     by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs 
  1469               real_sqrt_pow2_iff real_sqrt_power)
  1470   also have "... = exp (-x)"
  1471     by (auto simp add: exp_minus divide_inverse)
  1472   finally have "1 - x <= exp (- x)" .
  1473   also have "1 - x = exp (ln (1 - x))"
  1474     by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
  1475   finally have "exp (ln (1 - x)) <= exp (- x)" .
  1476   thus ?thesis by (auto simp only: exp_le_cancel_iff)
  1477 qed
  1478 
  1479 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
  1480   apply (case_tac "0 <= x")
  1481   apply (erule exp_ge_add_one_self_aux)
  1482   apply (case_tac "x <= -1")
  1483   apply (subgoal_tac "1 + x <= 0")
  1484   apply (erule order_trans)
  1485   apply simp
  1486   apply simp
  1487   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
  1488   apply (erule ssubst)
  1489   apply (subst exp_le_cancel_iff)
  1490   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
  1491   apply simp
  1492   apply (rule ln_one_minus_pos_upper_bound)
  1493   apply auto
  1494 done
  1495 
  1496 lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  1497 proof -
  1498   assume a: "0 <= x" and b: "x <= 1"
  1499   have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  1500     by (rule exp_diff)
  1501   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
  1502     by (metis a b divide_right_mono exp_bound exp_ge_zero)
  1503   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
  1504     by (simp add: a divide_left_mono add_pos_nonneg)
  1505   also from a have "... <= 1 + x"
  1506     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
  1507   finally have "exp (x - x\<^sup>2) <= 1 + x" .
  1508   also have "... = exp (ln (1 + x))"
  1509   proof -
  1510     from a have "0 < 1 + x" by auto
  1511     thus ?thesis
  1512       by (auto simp only: exp_ln_iff [THEN sym])
  1513   qed
  1514   finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
  1515   thus ?thesis
  1516     by (metis exp_le_cancel_iff) 
  1517 qed
  1518 
  1519 lemma ln_one_minus_pos_lower_bound:
  1520   "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  1521 proof -
  1522   assume a: "0 <= x" and b: "x <= (1 / 2)"
  1523   from b have c: "x < 1" by auto
  1524   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
  1525     apply (subst ln_inverse [symmetric])
  1526     apply (simp add: field_simps)
  1527     apply (rule arg_cong [where f=ln])
  1528     apply (simp add: field_simps)
  1529     done
  1530   also have "- (x / (1 - x)) <= ..."
  1531   proof -
  1532     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
  1533       using a c by (intro ln_add_one_self_le_self) auto
  1534     thus ?thesis
  1535       by auto
  1536   qed
  1537   also have "- (x / (1 - x)) = -x / (1 - x)"
  1538     by auto
  1539   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1540   have "0 < 1 - x" using a b by simp
  1541   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1542     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1543     by (simp add: field_simps power2_eq_square)
  1544   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1545     by (rule order_trans)
  1546 qed
  1547 
  1548 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1549   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1550   apply (subst ln_le_cancel_iff)
  1551   apply auto
  1552   done
  1553 
  1554 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1555   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1556 proof -
  1557   assume x: "0 <= x"
  1558   assume x1: "x <= 1"
  1559   from x have "ln (1 + x) <= x"
  1560     by (rule ln_add_one_self_le_self)
  1561   then have "ln (1 + x) - x <= 0"
  1562     by simp
  1563   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1564     by (rule abs_of_nonpos)
  1565   also have "... = x - ln (1 + x)"
  1566     by simp
  1567   also have "... <= x\<^sup>2"
  1568   proof -
  1569     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1570       by (intro ln_one_plus_pos_lower_bound)
  1571     thus ?thesis
  1572       by simp
  1573   qed
  1574   finally show ?thesis .
  1575 qed
  1576 
  1577 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1578   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1579 proof -
  1580   assume a: "-(1 / 2) <= x"
  1581   assume b: "x <= 0"
  1582   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1583     apply (subst abs_of_nonpos)
  1584     apply simp
  1585     apply (rule ln_add_one_self_le_self2)
  1586     using a apply auto
  1587     done
  1588   also have "... <= 2 * x\<^sup>2"
  1589     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1590     apply (simp add: algebra_simps)
  1591     apply (rule ln_one_minus_pos_lower_bound)
  1592     using a b apply auto
  1593     done
  1594   finally show ?thesis .
  1595 qed
  1596 
  1597 lemma abs_ln_one_plus_x_minus_x_bound:
  1598     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1599   apply (case_tac "0 <= x")
  1600   apply (rule order_trans)
  1601   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1602   apply auto
  1603   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1604   apply auto
  1605   done
  1606 
  1607 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1608 proof -
  1609   assume x: "exp 1 <= x" "x <= y"
  1610   moreover have "0 < exp (1::real)" by simp
  1611   ultimately have a: "0 < x" and b: "0 < y"
  1612     by (fast intro: less_le_trans order_trans)+
  1613   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1614     by (simp add: algebra_simps)
  1615   also have "... = x * ln(y / x)"
  1616     by (simp only: ln_div a b)
  1617   also have "y / x = (x + (y - x)) / x"
  1618     by simp
  1619   also have "... = 1 + (y - x) / x"
  1620     using x a by (simp add: field_simps)
  1621   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1622     using x a 
  1623     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1624   also have "... = y - x" using a by simp
  1625   also have "... = (y - x) * ln (exp 1)" by simp
  1626   also have "... <= (y - x) * ln x"
  1627     apply (rule mult_left_mono)
  1628     apply (subst ln_le_cancel_iff)
  1629     apply fact
  1630     apply (rule a)
  1631     apply (rule x)
  1632     using x apply simp
  1633     done
  1634   also have "... = y * ln x - x * ln x"
  1635     by (rule left_diff_distrib)
  1636   finally have "x * ln y <= y * ln x"
  1637     by arith
  1638   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1639   also have "... = y * (ln x / x)" by simp
  1640   finally show ?thesis using b by (simp add: field_simps)
  1641 qed
  1642 
  1643 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1644   using exp_ge_add_one_self[of "ln x"] by simp
  1645 
  1646 lemma ln_eq_minus_one:
  1647   assumes "0 < x" "ln x = x - 1"
  1648   shows "x = 1"
  1649 proof -
  1650   let ?l = "\<lambda>y. ln y - y + 1"
  1651   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1652     by (auto intro!: derivative_eq_intros)
  1653 
  1654   show ?thesis
  1655   proof (cases rule: linorder_cases)
  1656     assume "x < 1"
  1657     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1658     from `x < a` have "?l x < ?l a"
  1659     proof (rule DERIV_pos_imp_increasing, safe)
  1660       fix y
  1661       assume "x \<le> y" "y \<le> a"
  1662       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1663         by (auto simp: field_simps)
  1664       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1665         by auto
  1666     qed
  1667     also have "\<dots> \<le> 0"
  1668       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1669     finally show "x = 1" using assms by auto
  1670   next
  1671     assume "1 < x"
  1672     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1673     from `a < x` have "?l x < ?l a"
  1674     proof (rule DERIV_neg_imp_decreasing, safe)
  1675       fix y
  1676       assume "a \<le> y" "y \<le> x"
  1677       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1678         by (auto simp: field_simps)
  1679       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1680         by blast
  1681     qed
  1682     also have "\<dots> \<le> 0"
  1683       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1684     finally show "x = 1" using assms by auto
  1685   next
  1686     assume "x = 1"
  1687     then show ?thesis by simp
  1688   qed
  1689 qed
  1690 
  1691 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1692   unfolding tendsto_Zfun_iff
  1693 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1694   fix r :: real assume "0 < r"
  1695   {
  1696     fix x
  1697     assume "x < ln r"
  1698     then have "exp x < exp (ln r)"
  1699       by simp
  1700     with `0 < r` have "exp x < r"
  1701       by simp
  1702   }
  1703   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1704 qed
  1705 
  1706 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1707   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1708      (auto intro: eventually_gt_at_top)
  1709 
  1710 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1711   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1712      (auto simp: eventually_at_filter)
  1713 
  1714 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1715   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1716      (auto intro: eventually_gt_at_top)
  1717 
  1718 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1719 proof (induct k)
  1720   case 0
  1721   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1722     by (simp add: inverse_eq_divide[symmetric])
  1723        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1724               at_top_le_at_infinity order_refl)
  1725 next
  1726   case (Suc k)
  1727   show ?case
  1728   proof (rule lhospital_at_top_at_top)
  1729     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1730       by eventually_elim (intro derivative_eq_intros, auto)
  1731     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1732       by eventually_elim auto
  1733     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1734       by auto
  1735     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1736     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1737       by simp
  1738   qed (rule exp_at_top)
  1739 qed
  1740 
  1741 
  1742 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1743   -- {*exponentation with real exponent*}
  1744   where "x powr a = exp(a * ln x)"
  1745 
  1746 definition log :: "[real,real] => real"
  1747   -- {*logarithm of @{term x} to base @{term a}*}
  1748   where "log a x = ln x / ln a"
  1749 
  1750 
  1751 lemma tendsto_log [tendsto_intros]:
  1752   "\<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"
  1753   unfolding log_def by (intro tendsto_intros) auto
  1754 
  1755 lemma continuous_log:
  1756   assumes "continuous F f"
  1757     and "continuous F g"
  1758     and "0 < f (Lim F (\<lambda>x. x))"
  1759     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1760     and "0 < g (Lim F (\<lambda>x. x))"
  1761   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1762   using assms unfolding continuous_def by (rule tendsto_log)
  1763 
  1764 lemma continuous_at_within_log[continuous_intros]:
  1765   assumes "continuous (at a within s) f"
  1766     and "continuous (at a within s) g"
  1767     and "0 < f a"
  1768     and "f a \<noteq> 1"
  1769     and "0 < g a"
  1770   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1771   using assms unfolding continuous_within by (rule tendsto_log)
  1772 
  1773 lemma isCont_log[continuous_intros, simp]:
  1774   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1775   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1776   using assms unfolding continuous_at by (rule tendsto_log)
  1777 
  1778 lemma continuous_on_log[continuous_intros]:
  1779   assumes "continuous_on s f" "continuous_on s g"
  1780     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1781   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1782   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1783 
  1784 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1785   by (simp add: powr_def)
  1786 
  1787 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1788   by (simp add: powr_def)
  1789 
  1790 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1791   by (simp add: powr_def)
  1792 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1793 
  1794 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1795   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1796 
  1797 lemma powr_gt_zero [simp]: "0 < x powr a"
  1798   by (simp add: powr_def)
  1799 
  1800 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1801   by (rule order_less_imp_le, rule powr_gt_zero)
  1802 
  1803 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1804   by (simp add: powr_def)
  1805 
  1806 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1807   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1808   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1809   done
  1810 
  1811 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1812   apply (simp add: powr_def)
  1813   apply (subst exp_diff [THEN sym])
  1814   apply (simp add: left_diff_distrib)
  1815   done
  1816 
  1817 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1818   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1819 
  1820 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1821   using assms by (auto simp: powr_add)
  1822 
  1823 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1824   by (simp add: powr_def)
  1825 
  1826 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1827   by (simp add: powr_powr mult.commute)
  1828 
  1829 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1830   by (simp add: powr_def exp_minus [symmetric])
  1831 
  1832 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1833   by (simp add: divide_inverse powr_minus)
  1834 
  1835 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1836   by (simp add: powr_def)
  1837 
  1838 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1839   by (simp add: powr_def)
  1840 
  1841 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1842   by (blast intro: powr_less_cancel powr_less_mono)
  1843 
  1844 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1845   by (simp add: linorder_not_less [symmetric])
  1846 
  1847 lemma log_ln: "ln x = log (exp(1)) x"
  1848   by (simp add: log_def)
  1849 
  1850 lemma DERIV_log:
  1851   assumes "x > 0"
  1852   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1853 proof -
  1854   def lb \<equiv> "1 / ln b"
  1855   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1856     using `x > 0` by (auto intro!: derivative_eq_intros)
  1857   ultimately show ?thesis
  1858     by (simp add: log_def)
  1859 qed
  1860 
  1861 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1862 
  1863 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1864   by (simp add: powr_def log_def)
  1865 
  1866 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1867   by (simp add: log_def powr_def)
  1868 
  1869 lemma log_mult:
  1870   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1871     log a (x * y) = log a x + log a y"
  1872   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1873 
  1874 lemma log_eq_div_ln_mult_log:
  1875   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1876     log a x = (ln b/ln a) * log b x"
  1877   by (simp add: log_def divide_inverse)
  1878 
  1879 text{*Base 10 logarithms*}
  1880 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1881   by (simp add: log_def)
  1882 
  1883 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1884   by (simp add: log_def)
  1885 
  1886 lemma log_one [simp]: "log a 1 = 0"
  1887   by (simp add: log_def)
  1888 
  1889 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1890   by (simp add: log_def)
  1891 
  1892 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1893   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1894   apply (simp add: log_mult [symmetric])
  1895   done
  1896 
  1897 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"
  1898   by (simp add: log_mult divide_inverse log_inverse)
  1899 
  1900 lemma log_less_cancel_iff [simp]:
  1901   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  1902   apply safe
  1903   apply (rule_tac [2] powr_less_cancel)
  1904   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  1905   done
  1906 
  1907 lemma log_inj:
  1908   assumes "1 < b"
  1909   shows "inj_on (log b) {0 <..}"
  1910 proof (rule inj_onI, simp)
  1911   fix x y
  1912   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  1913   show "x = y"
  1914   proof (cases rule: linorder_cases)
  1915     assume "x = y"
  1916     then show ?thesis by simp
  1917   next
  1918     assume "x < y" hence "log b x < log b y"
  1919       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1920     then show ?thesis using * by simp
  1921   next
  1922     assume "y < x" hence "log b y < log b x"
  1923       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1924     then show ?thesis using * by simp
  1925   qed
  1926 qed
  1927 
  1928 lemma log_le_cancel_iff [simp]:
  1929   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  1930   by (simp add: linorder_not_less [symmetric])
  1931 
  1932 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  1933   using log_less_cancel_iff[of a 1 x] by simp
  1934 
  1935 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  1936   using log_le_cancel_iff[of a 1 x] by simp
  1937 
  1938 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  1939   using log_less_cancel_iff[of a x 1] by simp
  1940 
  1941 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  1942   using log_le_cancel_iff[of a x 1] by simp
  1943 
  1944 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  1945   using log_less_cancel_iff[of a a x] by simp
  1946 
  1947 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  1948   using log_le_cancel_iff[of a a x] by simp
  1949 
  1950 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  1951   using log_less_cancel_iff[of a x a] by simp
  1952 
  1953 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  1954   using log_le_cancel_iff[of a x a] by simp
  1955 
  1956 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  1957   apply (induct n)
  1958   apply simp
  1959   apply (subgoal_tac "real(Suc n) = real n + 1")
  1960   apply (erule ssubst)
  1961   apply (subst powr_add, simp, simp)
  1962   done
  1963 
  1964 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  1965   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  1966 
  1967 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  1968 by(simp add: powr_realpow_numeral)
  1969 
  1970 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  1971   apply (case_tac "x = 0", simp, simp)
  1972   apply (rule powr_realpow [THEN sym], simp)
  1973   done
  1974 
  1975 lemma powr_int:
  1976   assumes "x > 0"
  1977   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  1978 proof (cases "i < 0")
  1979   case True
  1980   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  1981   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  1982 next
  1983   case False
  1984   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  1985 qed
  1986 
  1987 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  1988   using powr_realpow [of x 1] by simp
  1989 
  1990 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  1991   by (fact powr_realpow_numeral)
  1992 
  1993 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  1994   using powr_int [of x "- 1"] by simp
  1995 
  1996 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  1997   using powr_int [of x "- numeral n"] by simp
  1998 
  1999 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  2000   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  2001 
  2002 lemma ln_powr: "ln (x powr y) = y * ln x"
  2003   by (simp add: powr_def)
  2004 
  2005 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  2006 by(simp add: root_powr_inverse ln_powr)
  2007 
  2008 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
  2009   by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
  2010 
  2011 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  2012 by(simp add: log_def ln_root)
  2013 
  2014 lemma log_powr: "log b (x powr y) = y * log b x"
  2015   by (simp add: log_def ln_powr)
  2016 
  2017 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
  2018   by (simp add: log_powr powr_realpow [symmetric])
  2019 
  2020 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  2021   by (simp add: log_def)
  2022 
  2023 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  2024   by (simp add: log_def ln_realpow)
  2025 
  2026 lemma log_base_powr: "log (a powr b) x = log a x / b"
  2027   by (simp add: log_def ln_powr)
  2028 
  2029 lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  2030 by(simp add: log_def ln_root)
  2031 
  2032 lemma ln_bound: "1 <= x ==> ln x <= x"
  2033   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  2034   apply simp
  2035   apply (rule ln_add_one_self_le_self, simp)
  2036   done
  2037 
  2038 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  2039   apply (cases "x = 1", simp)
  2040   apply (cases "a = b", simp)
  2041   apply (rule order_less_imp_le)
  2042   apply (rule powr_less_mono, auto)
  2043   done
  2044 
  2045 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2046   apply (subst powr_zero_eq_one [THEN sym])
  2047   apply (rule powr_mono, assumption+)
  2048   done
  2049 
  2050 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2051   apply (unfold powr_def)
  2052   apply (rule exp_less_mono)
  2053   apply (rule mult_strict_left_mono)
  2054   apply (subst ln_less_cancel_iff, assumption)
  2055   apply (rule order_less_trans)
  2056   prefer 2
  2057   apply assumption+
  2058   done
  2059 
  2060 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2061   apply (unfold powr_def)
  2062   apply (rule exp_less_mono)
  2063   apply (rule mult_strict_left_mono_neg)
  2064   apply (subst ln_less_cancel_iff)
  2065   apply assumption
  2066   apply (rule order_less_trans)
  2067   prefer 2
  2068   apply assumption+
  2069   done
  2070 
  2071 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2072   apply (case_tac "a = 0", simp)
  2073   apply (case_tac "x = y", simp)
  2074   apply (metis less_eq_real_def powr_less_mono2)
  2075   done
  2076 
  2077 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2078   unfolding powr_def exp_inj_iff by simp
  2079 
  2080 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2081   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute 
  2082             order.strict_trans2 powr_gt_zero zero_less_one)
  2083 
  2084 lemma ln_powr_bound2:
  2085   assumes "1 < x" and "0 < a"
  2086   shows "(ln x) powr a <= (a powr a) * x"
  2087 proof -
  2088   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2089     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2090   also have "... = a * (x powr (1 / a))"
  2091     by simp
  2092   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2093     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2094   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2095     by (metis assms(2) powr_mult powr_gt_zero)
  2096   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2097     by (rule powr_powr)
  2098   also have "... = x" using assms
  2099     by auto
  2100   finally show ?thesis .
  2101 qed
  2102 
  2103 lemma tendsto_powr [tendsto_intros]:
  2104   "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2105   unfolding powr_def by (intro tendsto_intros)
  2106 
  2107 lemma continuous_powr:
  2108   assumes "continuous F f"
  2109     and "continuous F g"
  2110     and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  2111   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2112   using assms unfolding continuous_def by (rule tendsto_powr)
  2113 
  2114 lemma continuous_at_within_powr[continuous_intros]:
  2115   assumes "continuous (at a within s) f"
  2116     and "continuous (at a within s) g"
  2117     and "f a \<noteq> 0"
  2118   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2119   using assms unfolding continuous_within by (rule tendsto_powr)
  2120 
  2121 lemma isCont_powr[continuous_intros, simp]:
  2122   assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  2123   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2124   using assms unfolding continuous_at by (rule tendsto_powr)
  2125 
  2126 lemma continuous_on_powr[continuous_intros]:
  2127   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  2128   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2129   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2130 
  2131 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2132 lemma tendsto_zero_powrI:
  2133   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2134     and "0 < d"
  2135   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2136 proof (rule tendstoI)
  2137   fix e :: real assume "0 < e"
  2138   def Z \<equiv> "e powr (1 / d)"
  2139   with `0 < e` have "0 < Z" by simp
  2140   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2141     by (intro eventually_conj tendstoD)
  2142   moreover
  2143   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2144     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2145   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2146     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2147   ultimately
  2148   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2149 qed
  2150 
  2151 lemma tendsto_neg_powr:
  2152   assumes "s < 0"
  2153     and "LIM x F. f x :> at_top"
  2154   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2155 proof (rule tendstoI)
  2156   fix e :: real assume "0 < e"
  2157   def Z \<equiv> "e powr (1 / s)"
  2158   from assms have "eventually (\<lambda>x. Z < f x) F"
  2159     by (simp add: filterlim_at_top_dense)
  2160   moreover
  2161   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2162     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2163   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2164     by (simp add: powr_powr Z_def dist_real_def)
  2165   ultimately
  2166   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2167 qed
  2168 
  2169 (* it is funny that this isn't in the library! It could go in Transcendental *)
  2170 lemma tendsto_exp_limit_at_right:
  2171   fixes x :: real
  2172   shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  2173 proof cases
  2174   assume "x \<noteq> 0"
  2175 
  2176   have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  2177     by (auto intro!: derivative_eq_intros)
  2178   then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  2179     by (auto simp add: has_field_derivative_def field_has_derivative_at) 
  2180   then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  2181     by (rule tendsto_intros)
  2182   then show ?thesis
  2183   proof (rule filterlim_mono_eventually)
  2184     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  2185       unfolding eventually_at_right[OF zero_less_one]
  2186       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  2187   qed (simp_all add: at_eq_sup_left_right)
  2188 qed (simp add: tendsto_const)
  2189 
  2190 lemma tendsto_exp_limit_at_top:
  2191   fixes x :: real
  2192   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  2193   apply (subst filterlim_at_top_to_right)
  2194   apply (simp add: inverse_eq_divide)
  2195   apply (rule tendsto_exp_limit_at_right)
  2196   done
  2197 
  2198 lemma tendsto_exp_limit_sequentially:
  2199   fixes x :: real
  2200   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  2201 proof (rule filterlim_mono_eventually)
  2202   from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  2203   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  2204     apply (intro eventually_sequentiallyI [of n])
  2205     apply (case_tac "x \<ge> 0")
  2206     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  2207     apply (subgoal_tac "x / real xa > -1")
  2208     apply (auto simp add: field_simps)
  2209     done
  2210   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  2211     by (rule eventually_elim1) (erule powr_realpow)
  2212   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  2213     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  2214 qed auto
  2215 
  2216 subsection {* Sine and Cosine *}
  2217 
  2218 definition sin_coeff :: "nat \<Rightarrow> real" where
  2219   "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
  2220 
  2221 definition cos_coeff :: "nat \<Rightarrow> real" where
  2222   "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
  2223 
  2224 definition sin :: "real \<Rightarrow> real"
  2225   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
  2226 
  2227 definition cos :: "real \<Rightarrow> real"
  2228   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
  2229 
  2230 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2231   unfolding sin_coeff_def by simp
  2232 
  2233 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2234   unfolding cos_coeff_def by simp
  2235 
  2236 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2237   unfolding cos_coeff_def sin_coeff_def
  2238   by (simp del: mult_Suc)
  2239 
  2240 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2241   unfolding cos_coeff_def sin_coeff_def
  2242   by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
  2243 
  2244 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
  2245   unfolding sin_coeff_def
  2246   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2247   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2248   done
  2249 
  2250 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
  2251   unfolding cos_coeff_def
  2252   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2253   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2254   done
  2255 
  2256 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
  2257   unfolding sin_def by (rule summable_sin [THEN summable_sums])
  2258 
  2259 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
  2260   unfolding cos_def by (rule summable_cos [THEN summable_sums])
  2261 
  2262 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2263   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2264 
  2265 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2266   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2267 
  2268 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2269 
  2270 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  2271   unfolding sin_def cos_def
  2272   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2273   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
  2274     summable_minus summable_sin summable_cos)
  2275   done
  2276 
  2277 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2278 
  2279 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  2280   unfolding cos_def sin_def
  2281   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2282   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
  2283     summable_minus summable_sin summable_cos suminf_minus)
  2284   done
  2285 
  2286 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2287 
  2288 lemma isCont_sin: "isCont sin x"
  2289   by (rule DERIV_sin [THEN DERIV_isCont])
  2290 
  2291 lemma isCont_cos: "isCont cos x"
  2292   by (rule DERIV_cos [THEN DERIV_isCont])
  2293 
  2294 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2295   by (rule isCont_o2 [OF _ isCont_sin])
  2296 
  2297 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2298   by (rule isCont_o2 [OF _ isCont_cos])
  2299 
  2300 lemma tendsto_sin [tendsto_intros]:
  2301   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2302   by (rule isCont_tendsto_compose [OF isCont_sin])
  2303 
  2304 lemma tendsto_cos [tendsto_intros]:
  2305   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2306   by (rule isCont_tendsto_compose [OF isCont_cos])
  2307 
  2308 lemma continuous_sin [continuous_intros]:
  2309   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2310   unfolding continuous_def by (rule tendsto_sin)
  2311 
  2312 lemma continuous_on_sin [continuous_intros]:
  2313   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2314   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2315 
  2316 lemma continuous_cos [continuous_intros]:
  2317   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2318   unfolding continuous_def by (rule tendsto_cos)
  2319 
  2320 lemma continuous_on_cos [continuous_intros]:
  2321   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2322   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2323 
  2324 subsection {* Properties of Sine and Cosine *}
  2325 
  2326 lemma sin_zero [simp]: "sin 0 = 0"
  2327   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
  2328 
  2329 lemma cos_zero [simp]: "cos 0 = 1"
  2330   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
  2331 
  2332 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2333 proof -
  2334   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  2335     by (auto intro!: derivative_eq_intros)
  2336   hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  2337     by (rule DERIV_isconst_all)
  2338   thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  2339 qed
  2340 
  2341 lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2342   by (subst add.commute, rule sin_cos_squared_add)
  2343 
  2344 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  2345   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2346 
  2347 lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2348   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2349 
  2350 lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2351   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2352 
  2353 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  2354   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2355 
  2356 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  2357   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2358 
  2359 lemma sin_le_one [simp]: "sin x \<le> 1"
  2360   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2361 
  2362 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  2363   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2364 
  2365 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  2366   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2367 
  2368 lemma cos_le_one [simp]: "cos x \<le> 1"
  2369   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2370 
  2371 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2372       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2373   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2374 
  2375 lemma DERIV_fun_exp:
  2376      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2377   by (auto intro!: derivative_intros)
  2378 
  2379 lemma DERIV_fun_sin:
  2380      "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2381   by (auto intro!: derivative_intros)
  2382 
  2383 lemma DERIV_fun_cos:
  2384      "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2385   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2386 
  2387 lemma sin_cos_add_lemma:
  2388   "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  2389     (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
  2390   (is "?f x = 0")
  2391 proof -
  2392   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2393     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2394   hence "?f x = ?f 0"
  2395     by (rule DERIV_isconst_all)
  2396   thus ?thesis by simp
  2397 qed
  2398 
  2399 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  2400   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2401 
  2402 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  2403   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2404 
  2405 lemma sin_cos_minus_lemma:
  2406   "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  2407 proof -
  2408   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2409     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2410   hence "?f x = ?f 0"
  2411     by (rule DERIV_isconst_all)
  2412   thus ?thesis by simp
  2413 qed
  2414 
  2415 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  2416   using sin_cos_minus_lemma [where x=x] by simp
  2417 
  2418 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  2419   using sin_cos_minus_lemma [where x=x] by simp
  2420 
  2421 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  2422   using sin_add [of x "- y"] by simp
  2423 
  2424 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  2425   by (simp add: sin_diff mult.commute)
  2426 
  2427 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  2428   using cos_add [of x "- y"] by simp
  2429 
  2430 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  2431   by (simp add: cos_diff mult.commute)
  2432 
  2433 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  2434   using sin_add [where x=x and y=x] by simp
  2435 
  2436 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
  2437   using cos_add [where x=x and y=x]
  2438   by (simp add: power2_eq_square)
  2439 
  2440 lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
  2441 proof -
  2442   let ?f = "\<lambda>x. x - sin x"
  2443   from x have "?f x \<ge> ?f 0"
  2444     apply (rule DERIV_nonneg_imp_nondecreasing)
  2445     apply (intro allI impI exI[of _ "1 - cos x" for x])
  2446     apply (auto intro!: derivative_eq_intros simp: field_simps)
  2447     done
  2448   thus "sin x \<le> x" by simp
  2449 qed
  2450 
  2451 lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  2452 proof -
  2453   let ?f = "\<lambda>x. x + sin x"
  2454   from x have "?f x \<ge> ?f 0"
  2455     apply (rule DERIV_nonneg_imp_nondecreasing)
  2456     apply (intro allI impI exI[of _ "1 + cos x" for x])
  2457     apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  2458     done
  2459   thus "sin x \<ge> -x" by simp
  2460 qed
  2461 
  2462 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  2463   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"]
  2464   by (auto simp: abs_real_def)
  2465 
  2466 subsection {* The Constant Pi *}
  2467 
  2468 definition pi :: real
  2469   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2470 
  2471 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2472    hence define pi.*}
  2473 
  2474 lemma sin_paired:
  2475   "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  2476 proof -
  2477   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2478     by (rule sin_converges [THEN sums_group], simp)
  2479   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
  2480 qed
  2481 
  2482 lemma sin_gt_zero:
  2483   assumes "0 < x" and "x < 2"
  2484   shows "0 < sin x"
  2485 proof -
  2486   let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  2487   have pos: "\<forall>n. 0 < ?f n"
  2488   proof
  2489     fix n :: nat
  2490     let ?k2 = "real (Suc (Suc (4 * n)))"
  2491     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2492     have "x * x < ?k2 * ?k3"
  2493       using assms by (intro mult_strict_mono', simp_all)
  2494     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2495       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2496     thus "0 < ?f n"
  2497       by (simp del: mult_Suc,
  2498         simp add: less_divide_eq field_simps del: mult_Suc)
  2499   qed
  2500   have sums: "?f sums sin x"
  2501     by (rule sin_paired [THEN sums_group], simp)
  2502   show "0 < sin x"
  2503     unfolding sums_unique [OF sums]
  2504     using sums_summable [OF sums] pos
  2505     by (rule suminf_pos)
  2506 qed
  2507 
  2508 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2509   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
  2510 
  2511 lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  2512 proof -
  2513   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2514     by (rule cos_converges [THEN sums_group], simp)
  2515   thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
  2516 qed
  2517 
  2518 lemmas realpow_num_eq_if = power_eq_if
  2519 
  2520 lemma sumr_pos_lt_pair:
  2521   fixes f :: "nat \<Rightarrow> real"
  2522   shows "\<lbrakk>summable f;
  2523         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2524       \<Longrightarrow> setsum f {..<k} < suminf f"
  2525 unfolding One_nat_def
  2526 apply (subst suminf_split_initial_segment [where k="k"])
  2527 apply assumption
  2528 apply simp
  2529 apply (drule_tac k="k" in summable_ignore_initial_segment)
  2530 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2531 apply simp
  2532 apply (frule sums_unique)
  2533 apply (drule sums_summable)
  2534 apply simp
  2535 apply (erule suminf_pos)
  2536 apply (simp add: ac_simps)
  2537 done
  2538 
  2539 lemma cos_two_less_zero [simp]:
  2540   "cos 2 < 0"
  2541 proof -
  2542   note fact_Suc [simp del]
  2543   from cos_paired
  2544   have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  2545     by (rule sums_minus)
  2546   then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  2547     by simp
  2548   then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2549     by (rule sums_summable)
  2550   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2551     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  2552   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  2553     < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2554   proof -
  2555     { fix d
  2556       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2557        < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2558            fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2559         by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  2560       then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2561         < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2562         by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  2563       then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  2564         < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2565         by (simp add: inverse_eq_divide less_divide_eq)
  2566     }
  2567     note *** = this
  2568     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2569     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2570       (simp add: divide_inverse mult.assoc [symmetric] ***)
  2571   qed
  2572   ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2573     by (rule order_less_trans)
  2574   moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2575     by (rule sums_unique)
  2576   ultimately have "0 < - cos 2" by simp
  2577   then show ?thesis by simp
  2578 qed
  2579 
  2580 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2581 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2582 
  2583 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2584 proof (rule ex_ex1I)
  2585   show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
  2586     by (rule IVT2, simp_all)
  2587 next
  2588   fix x y
  2589   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2590   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2591   have [simp]: "\<forall>x. cos differentiable (at x)"
  2592     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2593   from x y show "x = y"
  2594     apply (cut_tac less_linear [of x y], auto)
  2595     apply (drule_tac f = cos in Rolle)
  2596     apply (drule_tac [5] f = cos in Rolle)
  2597     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2598     apply (metis order_less_le_trans less_le sin_gt_zero)
  2599     apply (metis order_less_le_trans less_le sin_gt_zero)
  2600     done
  2601 qed
  2602 
  2603 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2604   by (simp add: pi_def)
  2605 
  2606 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2607   by (simp add: pi_half cos_is_zero [THEN theI'])
  2608 
  2609 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2610   apply (rule order_le_neq_trans)
  2611   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2612   apply (metis cos_pi_half cos_zero zero_neq_one)
  2613   done
  2614 
  2615 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2616 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2617 
  2618 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2619   apply (rule order_le_neq_trans)
  2620   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2621   apply (metis cos_pi_half cos_two_neq_zero)
  2622   done
  2623 
  2624 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2625 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2626 
  2627 lemma pi_gt_zero [simp]: "0 < pi"
  2628   using pi_half_gt_zero by simp
  2629 
  2630 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2631   by (rule pi_gt_zero [THEN order_less_imp_le])
  2632 
  2633 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2634   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2635 
  2636 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2637   by (simp add: linorder_not_less)
  2638 
  2639 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2640   by simp
  2641 
  2642 lemma m2pi_less_pi: "- (2 * pi) < pi"
  2643   by simp
  2644 
  2645 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2646   using sin_cos_squared_add2 [where x = "pi/2"]
  2647   using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
  2648   by (simp add: power2_eq_1_iff)
  2649 
  2650 lemma cos_pi [simp]: "cos pi = -1"
  2651   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  2652 
  2653 lemma sin_pi [simp]: "sin pi = 0"
  2654   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  2655 
  2656 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  2657   by (simp add: cos_diff)
  2658 
  2659 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  2660   by (simp add: cos_add)
  2661 
  2662 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  2663   by (simp add: sin_diff)
  2664 
  2665 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  2666   by (simp add: sin_add)
  2667 
  2668 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  2669   by (simp add: sin_add)
  2670 
  2671 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  2672   by (simp add: cos_add)
  2673 
  2674 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  2675   by (simp add: sin_add cos_double)
  2676 
  2677 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  2678   by (simp add: cos_add cos_double)
  2679 
  2680 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  2681   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2682 
  2683 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  2684   by (metis cos_npi mult.commute)
  2685 
  2686 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  2687   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2688 
  2689 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  2690   by (simp add: mult.commute [of pi])
  2691 
  2692 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  2693   by (simp add: cos_double)
  2694 
  2695 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  2696   by simp
  2697 
  2698 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  2699   by (metis sin_gt_zero order_less_trans pi_half_less_two)
  2700 
  2701 lemma sin_less_zero:
  2702   assumes "- pi/2 < x" and "x < 0"
  2703   shows "sin x < 0"
  2704 proof -
  2705   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  2706   thus ?thesis by simp
  2707 qed
  2708 
  2709 lemma pi_less_4: "pi < 4"
  2710   using pi_half_less_two by auto
  2711 
  2712 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  2713   apply (cut_tac pi_less_4)
  2714   apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  2715   apply (cut_tac cos_is_zero, safe)
  2716   apply (rename_tac y z)
  2717   apply (drule_tac x = y in spec)
  2718   apply (drule_tac x = "pi/2" in spec, simp)
  2719   done
  2720 
  2721 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  2722   apply (rule_tac x = x and y = 0 in linorder_cases)
  2723   apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
  2724   apply (auto intro: cos_gt_zero)
  2725   done
  2726 
  2727 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  2728   apply (auto simp add: order_le_less cos_gt_zero_pi)
  2729   apply (subgoal_tac "x = pi/2", auto)
  2730   done
  2731 
  2732 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  2733   by (simp add: sin_cos_eq cos_gt_zero_pi)
  2734 
  2735 lemma pi_ge_two: "2 \<le> pi"
  2736 proof (rule ccontr)
  2737   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  2738   have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
  2739   proof (cases "2 < 2 * pi")
  2740     case True with dense[OF `pi < 2`] show ?thesis by auto
  2741   next
  2742     case False have "pi < 2 * pi" by auto
  2743     from dense[OF this] and False show ?thesis by auto
  2744   qed
  2745   then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
  2746   hence "0 < sin y" using sin_gt_zero by auto
  2747   moreover
  2748   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
  2749   ultimately show False by auto
  2750 qed
  2751 
  2752 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  2753   by (auto simp add: order_le_less sin_gt_zero_pi)
  2754 
  2755 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  2756   It should be possible to factor out some of the common parts. *}
  2757 
  2758 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  2759 proof (rule ex_ex1I)
  2760   assume y: "-1 \<le> y" "y \<le> 1"
  2761   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  2762     by (rule IVT2, simp_all add: y)
  2763 next
  2764   fix a b
  2765   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  2766   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  2767   have [simp]: "\<forall>x. cos differentiable (at x)"
  2768     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2769   from a b show "a = b"
  2770     apply (cut_tac less_linear [of a b], auto)
  2771     apply (drule_tac f = cos in Rolle)
  2772     apply (drule_tac [5] f = cos in Rolle)
  2773     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2774     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2775     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2776     done
  2777 qed
  2778 
  2779 lemma sin_total:
  2780      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  2781 apply (rule ccontr)
  2782 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))")
  2783 apply (erule contrapos_np)
  2784 apply simp
  2785 apply (cut_tac y="-y" in cos_total, simp) apply simp
  2786 apply (erule ex1E)
  2787 apply (rule_tac a = "x - (pi/2)" in ex1I)
  2788 apply (simp (no_asm) add: add.assoc)
  2789 apply (rotate_tac 3)
  2790 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
  2791 done
  2792 
  2793 lemma reals_Archimedean4:
  2794      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  2795 apply (auto dest!: reals_Archimedean3)
  2796 apply (drule_tac x = x in spec, clarify)
  2797 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  2798  prefer 2 apply (erule LeastI)
  2799 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  2800 apply (rename_tac m)
  2801 apply (subgoal_tac "~ x < real m * y")
  2802  prefer 2 apply (rule not_less_Least, simp, force)
  2803 done
  2804 
  2805 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic
  2806    now causes some unwanted re-arrangements of literals!   *)
  2807 lemma cos_zero_lemma:
  2808      "[| 0 \<le> x; cos x = 0 |] ==>
  2809       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  2810 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  2811 apply (subgoal_tac "0 \<le> x - real n * pi &
  2812                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  2813 apply (auto simp add: algebra_simps real_of_nat_Suc)
  2814  prefer 2 apply (simp add: cos_diff)
  2815 apply (simp add: cos_diff)
  2816 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  2817 apply (rule_tac [2] cos_total, safe)
  2818 apply (drule_tac x = "x - real n * pi" in spec)
  2819 apply (drule_tac x = "pi/2" in spec)
  2820 apply (simp add: cos_diff)
  2821 apply (rule_tac x = "Suc (2 * n)" in exI)
  2822 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  2823 done
  2824 
  2825 lemma sin_zero_lemma:
  2826      "[| 0 \<le> x; sin x = 0 |] ==>
  2827       \<exists>n::nat. even n & x = real n * (pi/2)"
  2828 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  2829  apply (clarify, rule_tac x = "n - 1" in exI)
  2830  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
  2831 apply (rule cos_zero_lemma)
  2832 apply (simp_all add: cos_add)
  2833 done
  2834 
  2835 
  2836 lemma cos_zero_iff:
  2837      "(cos x = 0) =
  2838       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
  2839        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  2840 apply (rule iffI)
  2841 apply (cut_tac linorder_linear [of 0 x], safe)
  2842 apply (drule cos_zero_lemma, assumption+)
  2843 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  2844 apply (force simp add: minus_equation_iff [of x])
  2845 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
  2846 apply (auto simp add: cos_diff cos_add)
  2847 done
  2848 
  2849 (* ditto: but to a lesser extent *)
  2850 lemma sin_zero_iff:
  2851      "(sin x = 0) =
  2852       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  2853        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  2854 apply (rule iffI)
  2855 apply (cut_tac linorder_linear [of 0 x], safe)
  2856 apply (drule sin_zero_lemma, assumption+)
  2857 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  2858 apply (force simp add: minus_equation_iff [of x])
  2859 apply (auto simp add: even_mult_two_ex)
  2860 done
  2861 
  2862 lemma cos_monotone_0_pi:
  2863   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  2864   shows "cos x < cos y"
  2865 proof -
  2866   have "- (x - y) < 0" using assms by auto
  2867 
  2868   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  2869   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  2870     by auto
  2871   hence "0 < z" and "z < pi" using assms by auto
  2872   hence "0 < sin z" using sin_gt_zero_pi by auto
  2873   hence "cos x - cos y < 0"
  2874     unfolding cos_diff minus_mult_commute[symmetric]
  2875     using `- (x - y) < 0` by (rule mult_pos_neg2)
  2876   thus ?thesis by auto
  2877 qed
  2878 
  2879 lemma cos_monotone_0_pi':
  2880   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  2881   shows "cos x \<le> cos y"
  2882 proof (cases "y < x")
  2883   case True
  2884   show ?thesis
  2885     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  2886 next
  2887   case False
  2888   hence "y = x" using `y \<le> x` by auto
  2889   thus ?thesis by auto
  2890 qed
  2891 
  2892 lemma cos_monotone_minus_pi_0:
  2893   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  2894   shows "cos y < cos x"
  2895 proof -
  2896   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  2897     using assms by auto
  2898   from cos_monotone_0_pi[OF this] show ?thesis
  2899     unfolding cos_minus .
  2900 qed
  2901 
  2902 lemma cos_monotone_minus_pi_0':
  2903   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  2904   shows "cos y \<le> cos x"
  2905 proof (cases "y < x")
  2906   case True
  2907   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  2908     by auto
  2909 next
  2910   case False
  2911   hence "y = x" using `y \<le> x` by auto
  2912   thus ?thesis by auto
  2913 qed
  2914 
  2915 lemma sin_monotone_2pi':
  2916   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  2917   shows "sin y \<le> sin x"
  2918 proof -
  2919   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  2920     using pi_ge_two and assms by auto
  2921   from cos_monotone_0_pi'[OF this] show ?thesis
  2922     unfolding minus_sin_cos_eq[symmetric] by auto
  2923 qed
  2924 
  2925 
  2926 subsection {* Tangent *}
  2927 
  2928 definition tan :: "real \<Rightarrow> real"
  2929   where "tan = (\<lambda>x. sin x / cos x)"
  2930 
  2931 lemma tan_zero [simp]: "tan 0 = 0"
  2932   by (simp add: tan_def)
  2933 
  2934 lemma tan_pi [simp]: "tan pi = 0"
  2935   by (simp add: tan_def)
  2936 
  2937 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  2938   by (simp add: tan_def)
  2939 
  2940 lemma tan_minus [simp]: "tan (-x) = - tan x"
  2941   by (simp add: tan_def)
  2942 
  2943 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  2944   by (simp add: tan_def)
  2945 
  2946 lemma lemma_tan_add1:
  2947   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  2948   by (simp add: tan_def cos_add field_simps)
  2949 
  2950 lemma add_tan_eq:
  2951   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  2952   by (simp add: tan_def sin_add field_simps)
  2953 
  2954 lemma tan_add:
  2955      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  2956       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  2957   by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  2958 
  2959 lemma tan_double:
  2960      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  2961       ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  2962   using tan_add [of x x] by (simp add: power2_eq_square)
  2963 
  2964 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  2965   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  2966 
  2967 lemma tan_less_zero:
  2968   assumes lb: "- pi/2 < x" and "x < 0"
  2969   shows "tan x < 0"
  2970 proof -
  2971   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  2972   thus ?thesis by simp
  2973 qed
  2974 
  2975 lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  2976   unfolding tan_def sin_double cos_double sin_squared_eq
  2977   by (simp add: power2_eq_square)
  2978 
  2979 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  2980   unfolding tan_def
  2981   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  2982 
  2983 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  2984   by (rule DERIV_tan [THEN DERIV_isCont])
  2985 
  2986 lemma isCont_tan' [simp]:
  2987   "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  2988   by (rule isCont_o2 [OF _ isCont_tan])
  2989 
  2990 lemma tendsto_tan [tendsto_intros]:
  2991   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  2992   by (rule isCont_tendsto_compose [OF isCont_tan])
  2993 
  2994 lemma continuous_tan:
  2995   "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  2996   unfolding continuous_def by (rule tendsto_tan)
  2997 
  2998 lemma isCont_tan'' [continuous_intros]:
  2999   "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  3000   unfolding continuous_at by (rule tendsto_tan)
  3001 
  3002 lemma continuous_within_tan [continuous_intros]:
  3003   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  3004   unfolding continuous_within by (rule tendsto_tan)
  3005 
  3006 lemma continuous_on_tan [continuous_intros]:
  3007   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  3008   unfolding continuous_on_def by (auto intro: tendsto_tan)
  3009 
  3010 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  3011   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  3012 
  3013 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  3014   apply (cut_tac LIM_cos_div_sin)
  3015   apply (simp only: LIM_eq)
  3016   apply (drule_tac x = "inverse y" in spec, safe, force)
  3017   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  3018   apply (rule_tac x = "(pi/2) - e" in exI)
  3019   apply (simp (no_asm_simp))
  3020   apply (drule_tac x = "(pi/2) - e" in spec)
  3021   apply (auto simp add: tan_def sin_diff cos_diff)
  3022   apply (rule inverse_less_iff_less [THEN iffD1])
  3023   apply (auto simp add: divide_inverse)
  3024   apply (rule mult_pos_pos)
  3025   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  3026   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult.commute)
  3027   done
  3028 
  3029 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  3030   apply (frule order_le_imp_less_or_eq, safe)
  3031    prefer 2 apply force
  3032   apply (drule lemma_tan_total, safe)
  3033   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  3034   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  3035   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  3036   apply (auto dest: cos_gt_zero)
  3037   done
  3038 
  3039 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3040   apply (cut_tac linorder_linear [of 0 y], safe)
  3041   apply (drule tan_total_pos)
  3042   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  3043   apply (rule_tac [3] x = "-x" in exI)
  3044   apply (auto del: exI intro!: exI)
  3045   done
  3046 
  3047 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3048   apply (cut_tac y = y in lemma_tan_total1, auto)
  3049   apply hypsubst_thin
  3050   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  3051   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  3052   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  3053   apply (rule_tac [4] Rolle)
  3054   apply (rule_tac [2] Rolle)
  3055   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  3056               simp add: real_differentiable_def)
  3057   txt{*Now, simulate TRYALL*}
  3058   apply (rule_tac [!] DERIV_tan asm_rl)
  3059   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  3060               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  3061   done
  3062 
  3063 lemma tan_monotone:
  3064   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  3065   shows "tan y < tan x"
  3066 proof -
  3067   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  3068   proof (rule allI, rule impI)
  3069     fix x' :: real
  3070     assume "y \<le> x' \<and> x' \<le> x"
  3071     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  3072     from cos_gt_zero_pi[OF this]
  3073     have "cos x' \<noteq> 0" by auto
  3074     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  3075   qed
  3076   from MVT2[OF `y < x` this]
  3077   obtain z where "y < z" and "z < x"
  3078     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  3079   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  3080   hence "0 < cos z" using cos_gt_zero_pi by auto
  3081   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  3082   have "0 < x - y" using `y < x` by auto
  3083   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  3084   thus ?thesis by auto
  3085 qed
  3086 
  3087 lemma tan_monotone':
  3088   assumes "- (pi / 2) < y"
  3089     and "y < pi / 2"
  3090     and "- (pi / 2) < x"
  3091     and "x < pi / 2"
  3092   shows "(y < x) = (tan y < tan x)"
  3093 proof
  3094   assume "y < x"
  3095   thus "tan y < tan x"
  3096     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  3097 next
  3098   assume "tan y < tan x"
  3099   show "y < x"
  3100   proof (rule ccontr)
  3101     assume "\<not> y < x" hence "x \<le> y" by auto
  3102     hence "tan x \<le> tan y"
  3103     proof (cases "x = y")
  3104       case True thus ?thesis by auto
  3105     next
  3106       case False hence "x < y" using `x \<le> y` by auto
  3107       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  3108     qed
  3109     thus False using `tan y < tan x` by auto
  3110   qed
  3111 qed
  3112 
  3113 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  3114   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3115 
  3116 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3117   by (simp add: tan_def)
  3118 
  3119 lemma tan_periodic_nat[simp]:
  3120   fixes n :: nat
  3121   shows "tan (x + real n * pi) = tan x"
  3122 proof (induct n arbitrary: x)
  3123   case 0
  3124   then show ?case by simp
  3125 next
  3126   case (Suc n)
  3127   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3128     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3129   show ?case unfolding split_pi_off using Suc by auto
  3130 qed
  3131 
  3132 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3133 proof (cases "0 \<le> i")
  3134   case True
  3135   hence i_nat: "real i = real (nat i)" by auto
  3136   show ?thesis unfolding i_nat by auto
  3137 next
  3138   case False
  3139   hence i_nat: "real i = - real (nat (-i))" by auto
  3140   have "tan x = tan (x + real i * pi - real i * pi)"
  3141     by auto
  3142   also have "\<dots> = tan (x + real i * pi)"
  3143     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3144   finally show ?thesis by auto
  3145 qed
  3146 
  3147 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3148   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3149 
  3150 subsection {* Inverse Trigonometric Functions *}
  3151 
  3152 definition arcsin :: "real => real"
  3153   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3154 
  3155 definition arccos :: "real => real"
  3156   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3157 
  3158 definition arctan :: "real => real"
  3159   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3160 
  3161 lemma arcsin:
  3162   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3163     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3164   unfolding arcsin_def by (rule theI' [OF sin_total])
  3165 
  3166 lemma arcsin_pi:
  3167   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3168   apply (drule (1) arcsin)
  3169   apply (force intro: order_trans)
  3170   done
  3171 
  3172 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3173   by (blast dest: arcsin)
  3174 
  3175 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3176   by (blast dest: arcsin)
  3177 
  3178 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3179   by (blast dest: arcsin)
  3180 
  3181 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3182   by (blast dest: arcsin)
  3183 
  3184 lemma arcsin_lt_bounded:
  3185      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  3186   apply (frule order_less_imp_le)
  3187   apply (frule_tac y = y in order_less_imp_le)
  3188   apply (frule arcsin_bounded)
  3189   apply (safe, simp)
  3190   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3191   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3192   apply (drule_tac [!] f = sin in arg_cong, auto)
  3193   done
  3194 
  3195 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  3196   apply (unfold arcsin_def)
  3197   apply (rule the1_equality)
  3198   apply (rule sin_total, auto)
  3199   done
  3200 
  3201 lemma arccos:
  3202      "[| -1 \<le> y; y \<le> 1 |]
  3203       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3204   unfolding arccos_def by (rule theI' [OF cos_total])
  3205 
  3206 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  3207   by (blast dest: arccos)
  3208 
  3209 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  3210   by (blast dest: arccos)
  3211 
  3212 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  3213   by (blast dest: arccos)
  3214 
  3215 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  3216   by (blast dest: arccos)
  3217 
  3218 lemma arccos_lt_bounded:
  3219      "[| -1 < y; y < 1 |]
  3220       ==> 0 < arccos y & arccos y < pi"
  3221   apply (frule order_less_imp_le)
  3222   apply (frule_tac y = y in order_less_imp_le)
  3223   apply (frule arccos_bounded, auto)
  3224   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3225   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3226   apply (drule_tac [!] f = cos in arg_cong, auto)
  3227   done
  3228 
  3229 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  3230   apply (simp add: arccos_def)
  3231   apply (auto intro!: the1_equality cos_total)
  3232   done
  3233 
  3234 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  3235   apply (simp add: arccos_def)
  3236   apply (auto intro!: the1_equality cos_total)
  3237   done
  3238 
  3239 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3240   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3241   apply (rule power2_eq_imp_eq)
  3242   apply (simp add: cos_squared_eq)
  3243   apply (rule cos_ge_zero)
  3244   apply (erule (1) arcsin_lbound)
  3245   apply (erule (1) arcsin_ubound)
  3246   apply simp
  3247   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3248   apply (rule power_mono, simp, simp)
  3249   done
  3250 
  3251 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3252   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3253   apply (rule power2_eq_imp_eq)
  3254   apply (simp add: sin_squared_eq)
  3255   apply (rule sin_ge_zero)
  3256   apply (erule (1) arccos_lbound)
  3257   apply (erule (1) arccos_ubound)
  3258   apply simp
  3259   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3260   apply (rule power_mono, simp, simp)
  3261   done
  3262 
  3263 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3264   unfolding arctan_def by (rule theI' [OF tan_total])
  3265 
  3266 lemma tan_arctan: "tan (arctan y) = y"
  3267   by auto
  3268 
  3269 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3270   by (auto simp only: arctan)
  3271 
  3272 lemma arctan_lbound: "- (pi/2) < arctan y"
  3273   by auto
  3274 
  3275 lemma arctan_ubound: "arctan y < pi/2"
  3276   by (auto simp only: arctan)
  3277 
  3278 lemma arctan_unique:
  3279   assumes "-(pi/2) < x"
  3280     and "x < pi/2"
  3281     and "tan x = y"
  3282   shows "arctan y = x"
  3283   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3284 
  3285 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3286   by (rule arctan_unique) simp_all
  3287 
  3288 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3289   by (rule arctan_unique) simp_all
  3290 
  3291 lemma arctan_minus: "arctan (- x) = - arctan x"
  3292   apply (rule arctan_unique)
  3293   apply (simp only: neg_less_iff_less arctan_ubound)
  3294   apply (metis minus_less_iff arctan_lbound)
  3295   apply simp
  3296   done
  3297 
  3298 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3299   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3300     arctan_lbound arctan_ubound)
  3301 
  3302 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3303 proof (rule power2_eq_imp_eq)
  3304   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3305   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3306   show "0 \<le> cos (arctan x)"
  3307     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3308   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3309     unfolding tan_def by (simp add: distrib_left power_divide)
  3310   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3311     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3312 qed
  3313 
  3314 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3315   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3316   using tan_arctan [of x] unfolding tan_def cos_arctan
  3317   by (simp add: eq_divide_eq)
  3318 
  3319 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3320   apply (rule power_inverse [THEN subst])
  3321   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3322   apply (auto dest: field_power_not_zero
  3323           simp add: power_mult_distrib distrib_right power_divide tan_def
  3324                     mult.assoc power_inverse [symmetric])
  3325   done
  3326 
  3327 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3328   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3329 
  3330 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3331   by (simp only: not_less [symmetric] arctan_less_iff)
  3332 
  3333 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3334   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3335 
  3336 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3337   using arctan_less_iff [of 0 x] by simp
  3338 
  3339 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3340   using arctan_less_iff [of x 0] by simp
  3341 
  3342 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3343   using arctan_le_iff [of 0 x] by simp
  3344 
  3345 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3346   using arctan_le_iff [of x 0] by simp
  3347 
  3348 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3349   using arctan_eq_iff [of x 0] by simp
  3350 
  3351 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3352 proof -
  3353   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3354     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3355   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3356   proof safe
  3357     fix x :: real
  3358     assume "x \<in> {-1..1}"
  3359     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3360       using arcsin_lbound arcsin_ubound
  3361       by (intro image_eqI[where x="arcsin x"]) auto
  3362   qed simp
  3363   finally show ?thesis .
  3364 qed
  3365 
  3366 lemma continuous_on_arcsin [continuous_intros]:
  3367   "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))"
  3368   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3369   by (auto simp: comp_def subset_eq)
  3370 
  3371 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3372   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3373   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3374 
  3375 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3376 proof -
  3377   have "continuous_on (cos ` {0 .. pi}) arccos"
  3378     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3379   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3380   proof safe
  3381     fix x :: real
  3382     assume "x \<in> {-1..1}"
  3383     then show "x \<in> cos ` {0..pi}"
  3384       using arccos_lbound arccos_ubound
  3385       by (intro image_eqI[where x="arccos x"]) auto
  3386   qed simp
  3387   finally show ?thesis .
  3388 qed
  3389 
  3390 lemma continuous_on_arccos [continuous_intros]:
  3391   "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))"
  3392   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3393   by (auto simp: comp_def subset_eq)
  3394 
  3395 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3396   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3397   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3398 
  3399 lemma isCont_arctan: "isCont arctan x"
  3400   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3401   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3402   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3403   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3404   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3405   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3406   done
  3407 
  3408 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3409   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3410 
  3411 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3412   unfolding continuous_def by (rule tendsto_arctan)
  3413 
  3414 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3415   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3416 
  3417 lemma DERIV_arcsin:
  3418   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3419   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  3420   apply (rule DERIV_cong [OF DERIV_sin])
  3421   apply (simp add: cos_arcsin)
  3422   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3423   apply (rule power_strict_mono, simp, simp, simp)
  3424   apply assumption
  3425   apply assumption
  3426   apply simp
  3427   apply (erule (1) isCont_arcsin)
  3428   done
  3429 
  3430 lemma DERIV_arccos:
  3431   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3432   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  3433   apply (rule DERIV_cong [OF DERIV_cos])
  3434   apply (simp add: sin_arccos)
  3435   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3436   apply (rule power_strict_mono, simp, simp, simp)
  3437   apply assumption
  3438   apply assumption
  3439   apply simp
  3440   apply (erule (1) isCont_arccos)
  3441   done
  3442 
  3443 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3444   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3445   apply (rule DERIV_cong [OF DERIV_tan])
  3446   apply (rule cos_arctan_not_zero)
  3447   apply (simp add: power_inverse tan_sec [symmetric])
  3448   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3449   apply (simp add: add_pos_nonneg)
  3450   apply (simp, simp, simp, rule isCont_arctan)
  3451   done
  3452 
  3453 declare
  3454   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3455   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3456   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3457 
  3458 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3459   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])
  3460      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3461            intro!: tan_monotone exI[of _ "pi/2"])
  3462 
  3463 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3464   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])
  3465      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3466            intro!: tan_monotone exI[of _ "pi/2"])
  3467 
  3468 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3469 proof (rule tendstoI)
  3470   fix e :: real
  3471   assume "0 < e"
  3472   def y \<equiv> "pi/2 - min (pi/2) e"
  3473   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3474     using `0 < e` by auto
  3475 
  3476   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3477   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3478     fix x
  3479     assume "tan y < x"
  3480     then have "arctan (tan y) < arctan x"
  3481       by (simp add: arctan_less_iff)
  3482     with y have "y < arctan x"
  3483       by (subst (asm) arctan_tan) simp_all
  3484     with arctan_ubound[of x, arith] y `0 < e`
  3485     show "dist (arctan x) (pi / 2) < e"
  3486       by (simp add: dist_real_def)
  3487   qed
  3488 qed
  3489 
  3490 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3491   unfolding filterlim_at_bot_mirror arctan_minus
  3492   by (intro tendsto_minus tendsto_arctan_at_top)
  3493 
  3494 
  3495 subsection {* More Theorems about Sin and Cos *}
  3496 
  3497 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3498 proof -
  3499   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3500   have nonneg: "0 \<le> ?c"
  3501     by (simp add: cos_ge_zero)
  3502   have "0 = cos (pi / 4 + pi / 4)"
  3503     by simp
  3504   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3505     by (simp only: cos_add power2_eq_square)
  3506   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3507     by (simp add: sin_squared_eq)
  3508   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3509     by (simp add: power_divide)
  3510   thus ?thesis
  3511     using nonneg by (rule power2_eq_imp_eq) simp
  3512 qed
  3513 
  3514 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  3515 proof -
  3516   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3517   have pos_c: "0 < ?c"
  3518     by (rule cos_gt_zero, simp, simp)
  3519   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3520     by simp
  3521   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3522     by (simp only: cos_add sin_add)
  3523   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3524     by (simp add: algebra_simps power2_eq_square)
  3525   finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  3526     using pos_c by (simp add: sin_squared_eq power_divide)
  3527   thus ?thesis
  3528     using pos_c [THEN order_less_imp_le]
  3529     by (rule power2_eq_imp_eq) simp
  3530 qed
  3531 
  3532 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  3533   by (simp add: sin_cos_eq cos_45)
  3534 
  3535 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  3536   by (simp add: sin_cos_eq cos_30)
  3537 
  3538 lemma cos_60: "cos (pi / 3) = 1 / 2"
  3539   apply (rule power2_eq_imp_eq)
  3540   apply (simp add: cos_squared_eq sin_60 power_divide)
  3541   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  3542   done
  3543 
  3544 lemma sin_30: "sin (pi / 6) = 1 / 2"
  3545   by (simp add: sin_cos_eq cos_60)
  3546 
  3547 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  3548   unfolding tan_def by (simp add: sin_30 cos_30)
  3549 
  3550 lemma tan_45: "tan (pi / 4) = 1"
  3551   unfolding tan_def by (simp add: sin_45 cos_45)
  3552 
  3553 lemma tan_60: "tan (pi / 3) = sqrt 3"
  3554   unfolding tan_def by (simp add: sin_60 cos_60)
  3555 
  3556 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  3557 proof -
  3558   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  3559     by (auto simp add: algebra_simps sin_add)
  3560   thus ?thesis
  3561     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  3562                   mult.commute [of pi])
  3563 qed
  3564 
  3565 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  3566   by (simp add: cos_double mult.assoc power_add [symmetric] numeral_2_eq_2)
  3567 
  3568 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  3569   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  3570   apply (subst cos_add, simp)
  3571   done
  3572 
  3573 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  3574   by (auto simp add: mult.assoc)
  3575 
  3576 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  3577   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  3578   apply (subst sin_add, simp)
  3579   done
  3580 
  3581 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  3582   apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  3583   apply auto
  3584   done
  3585 
  3586 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  3587   by (auto intro!: derivative_eq_intros)
  3588 
  3589 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  3590   by (auto simp add: sin_zero_iff even_mult_two_ex)
  3591 
  3592 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  3593   using sin_cos_squared_add3 [where x = x] by auto
  3594 
  3595 
  3596 subsection {* Machins formula *}
  3597 
  3598 lemma arctan_one: "arctan 1 = pi / 4"
  3599   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  3600 
  3601 lemma tan_total_pi4:
  3602   assumes "\<bar>x\<bar> < 1"
  3603   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  3604 proof
  3605   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  3606     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3607     unfolding arctan_less_iff using assms by auto
  3608 qed
  3609 
  3610 lemma arctan_add:
  3611   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  3612   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  3613 proof (rule arctan_unique [symmetric])
  3614   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  3615     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3616     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3617   from add_le_less_mono [OF this]
  3618   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  3619   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  3620     unfolding arctan_one [symmetric]
  3621     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3622   from add_le_less_mono [OF this]
  3623   show 2: "arctan x + arctan y < pi / 2" by simp
  3624   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  3625     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  3626 qed
  3627 
  3628 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  3629 proof -
  3630   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  3631   from arctan_add[OF less_imp_le[OF this] this]
  3632   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  3633   moreover
  3634   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  3635   from arctan_add[OF less_imp_le[OF this] this]
  3636   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  3637   moreover
  3638   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  3639   from arctan_add[OF this]
  3640   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  3641   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  3642   thus ?thesis unfolding arctan_one by algebra
  3643 qed
  3644 
  3645 
  3646 subsection {* Introducing the arcus tangens power series *}
  3647 
  3648 lemma monoseq_arctan_series:
  3649   fixes x :: real
  3650   assumes "\<bar>x\<bar> \<le> 1"
  3651   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  3652 proof (cases "x = 0")
  3653   case True
  3654   thus ?thesis unfolding monoseq_def One_nat_def by auto
  3655 next
  3656   case False
  3657   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3658   show "monoseq ?a"
  3659   proof -
  3660     {
  3661       fix n
  3662       fix x :: real
  3663       assume "0 \<le> x" and "x \<le> 1"
  3664       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  3665         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  3666       proof (rule mult_mono)
  3667         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  3668           by (rule frac_le) simp_all
  3669         show "0 \<le> 1 / real (Suc (n * 2))"
  3670           by auto
  3671         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  3672           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  3673         show "0 \<le> x ^ Suc (Suc n * 2)"
  3674           by (rule zero_le_power) (simp add: `0 \<le> x`)
  3675       qed
  3676     } note mono = this
  3677 
  3678     show ?thesis
  3679     proof (cases "0 \<le> x")
  3680       case True from mono[OF this `x \<le> 1`, THEN allI]
  3681       show ?thesis unfolding Suc_eq_plus1[symmetric]
  3682         by (rule mono_SucI2)
  3683     next
  3684       case False
  3685       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  3686       from mono[OF this]
  3687       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  3688         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  3689       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  3690     qed
  3691   qed
  3692 qed
  3693 
  3694 lemma zeroseq_arctan_series:
  3695   fixes x :: real
  3696   assumes "\<bar>x\<bar> \<le> 1"
  3697   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  3698 proof (cases "x = 0")
  3699   case True
  3700   thus ?thesis
  3701     unfolding One_nat_def by (auto simp add: tendsto_const)
  3702 next
  3703   case False
  3704   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3705   show "?a ----> 0"
  3706   proof (cases "\<bar>x\<bar> < 1")
  3707     case True
  3708     hence "norm x < 1" by auto
  3709     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  3710     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  3711       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  3712     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  3713   next
  3714     case False
  3715     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3716     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  3717       unfolding One_nat_def by auto
  3718     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  3719     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  3720   qed
  3721 qed
  3722 
  3723 lemma summable_arctan_series:
  3724   fixes x :: real and n :: nat
  3725   assumes "\<bar>x\<bar> \<le> 1"
  3726   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3727   (is "summable (?c x)")
  3728   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  3729 
  3730 lemma less_one_imp_sqr_less_one:
  3731   fixes x :: real
  3732   assumes "\<bar>x\<bar> < 1"
  3733   shows "x\<^sup>2 < 1"
  3734 proof -
  3735   have "\<bar>x\<^sup>2\<bar> < 1"
  3736     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
  3737   thus ?thesis using zero_le_power2 by auto
  3738 qed
  3739 
  3740 lemma DERIV_arctan_series:
  3741   assumes "\<bar> x \<bar> < 1"
  3742   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))"
  3743   (is "DERIV ?arctan _ :> ?Int")
  3744 proof -
  3745   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  3746 
  3747   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  3748     by presburger
  3749   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  3750     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  3751     by auto
  3752 
  3753   {
  3754     fix x :: real
  3755     assume "\<bar>x\<bar> < 1"
  3756     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  3757     have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  3758       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`])
  3759     hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  3760   } note summable_Integral = this
  3761 
  3762   {
  3763     fix f :: "nat \<Rightarrow> real"
  3764     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3765     proof
  3766       fix x :: real
  3767       assume "f sums x"
  3768       from sums_if[OF sums_zero this]
  3769       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  3770         by auto
  3771     next
  3772       fix x :: real
  3773       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3774       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
  3775       show "f sums x" unfolding sums_def by auto
  3776     qed
  3777     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  3778   } note sums_even = this
  3779 
  3780   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  3781     unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  3782     by auto
  3783 
  3784   {
  3785     fix x :: real
  3786     have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  3787       (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  3788       using n_even by auto
  3789     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  3790     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  3791       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  3792       by auto
  3793   } note arctan_eq = this
  3794 
  3795   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  3796   proof (rule DERIV_power_series')
  3797     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  3798     {
  3799       fix x' :: real
  3800       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  3801       then have "\<bar>x'\<bar> < 1" by auto
  3802       then
  3803         have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  3804         by (rule summable_Integral)
  3805       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  3806       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  3807         apply (rule sums_summable [where l="0 + ?S"])
  3808         apply (rule sums_if)
  3809         apply (rule sums_zero)
  3810         apply (rule summable_sums)
  3811         apply (rule *)
  3812         done
  3813     }
  3814   qed auto
  3815   thus ?thesis unfolding Int_eq arctan_eq .
  3816 qed
  3817 
  3818 lemma arctan_series:
  3819   assumes "\<bar> x \<bar> \<le> 1"
  3820   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3821   (is "_ = suminf (\<lambda> n. ?c x n)")
  3822 proof -
  3823   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  3824 
  3825   {
  3826     fix r x :: real
  3827     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  3828     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  3829     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  3830   } note DERIV_arctan_suminf = this
  3831 
  3832   {
  3833     fix x :: real
  3834     assume "\<bar>x\<bar> \<le> 1"
  3835     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  3836   } note arctan_series_borders = this
  3837 
  3838   {
  3839     fix x :: real
  3840     assume "\<bar>x\<bar> < 1"
  3841     have "arctan x = (\<Sum>k. ?c x k)"
  3842     proof -
  3843       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  3844         using dense[OF `\<bar>x\<bar> < 1`] by blast
  3845       hence "0 < r" and "-r < x" and "x < r" by auto
  3846 
  3847       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  3848         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3849       proof -
  3850         fix x a b
  3851         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  3852         hence "\<bar>x\<bar> < r" by auto
  3853         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3854         proof (rule DERIV_isconst2[of "a" "b"])
  3855           show "a < b" and "a \<le> x" and "x \<le> b"
  3856             using `a < b` `a \<le> x` `x \<le> b` by auto
  3857           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3858           proof (rule allI, rule impI)
  3859             fix x
  3860             assume "-r < x \<and> x < r"
  3861             hence "\<bar>x\<bar> < r" by auto
  3862             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  3863             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  3864               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  3865             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  3866               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  3867             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  3868               unfolding power_mult_distrib[symmetric] power_mult mult.commute[of _ 2] by auto
  3869             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  3870               using sums_unique unfolding inverse_eq_divide by auto
  3871             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  3872               unfolding suminf_c'_eq_geom
  3873               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  3874             from DERIV_diff [OF this DERIV_arctan]
  3875             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3876               by auto
  3877           qed
  3878           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3879             using `-r < a` `b < r` by auto
  3880           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3881             using `\<bar>x\<bar> < r` by auto
  3882           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  3883             using DERIV_in_rball DERIV_isCont by auto
  3884         qed
  3885       qed
  3886 
  3887       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  3888         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  3889         by auto
  3890 
  3891       have "suminf (?c x) - arctan x = 0"
  3892       proof (cases "x = 0")
  3893         case True
  3894         thus ?thesis using suminf_arctan_zero by auto
  3895       next
  3896         case False
  3897         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  3898         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  3899           by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
  3900             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3901         moreover
  3902         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  3903           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
  3904              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3905         ultimately
  3906         show ?thesis using suminf_arctan_zero by auto
  3907       qed
  3908       thus ?thesis by auto
  3909     qed
  3910   } note when_less_one = this
  3911 
  3912   show "arctan x = suminf (\<lambda> n. ?c x n)"
  3913   proof (cases "\<bar>x\<bar> < 1")
  3914     case True
  3915     thus ?thesis by (rule when_less_one)
  3916   next
  3917     case False
  3918     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3919     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  3920     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  3921     {
  3922       fix n :: nat
  3923       have "0 < (1 :: real)" by auto
  3924       moreover
  3925       {
  3926         fix x :: real
  3927         assume "0 < x" and "x < 1"
  3928         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  3929         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  3930           by auto
  3931         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]
  3932         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  3933           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  3934         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  3935           by (rule abs_of_pos)
  3936         have "?diff x n \<le> ?a x n"
  3937         proof (cases "even n")
  3938           case True
  3939           hence sgn_pos: "(-1)^n = (1::real)" by auto
  3940           from `even n` obtain m where "2 * m = n"
  3941             unfolding even_mult_two_ex by auto
  3942           from bounds[of m, unfolded this atLeastAtMost_iff]
  3943           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))"
  3944             by auto
  3945           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  3946           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  3947           finally show ?thesis .
  3948         next
  3949           case False
  3950           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  3951           from `odd n` obtain m where m_def: "2 * m + 1 = n"
  3952             unfolding odd_Suc_mult_two_ex by auto
  3953           hence m_plus: "2 * (m + 1) = n + 1" by auto
  3954           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  3955           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))"
  3956             by auto
  3957           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  3958           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  3959           finally show ?thesis .
  3960         qed
  3961         hence "0 \<le> ?a x n - ?diff x n" by auto
  3962       }
  3963       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  3964       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  3965         unfolding diff_conv_add_uminus divide_inverse
  3966         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  3967           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  3968           simp del: add_uminus_conv_diff)
  3969       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  3970         by (rule LIM_less_bound)
  3971       hence "?diff 1 n \<le> ?a 1 n" by auto
  3972     }
  3973     have "?a 1 ----> 0"
  3974       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  3975       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  3976     have "?diff 1 ----> 0"
  3977     proof (rule LIMSEQ_I)
  3978       fix r :: real
  3979       assume "0 < r"
  3980       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  3981         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  3982       {
  3983         fix n
  3984         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  3985         have "norm (?diff 1 n - 0) < r" by auto
  3986       }
  3987       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  3988     qed
  3989     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  3990     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  3991     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  3992 
  3993     show ?thesis
  3994     proof (cases "x = 1")
  3995       case True
  3996       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  3997     next
  3998       case False
  3999       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  4000 
  4001       have "- (pi / 2) < 0" using pi_gt_zero by auto
  4002       have "- (2 * pi) < 0" using pi_gt_zero by auto
  4003 
  4004       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  4005         unfolding One_nat_def by auto
  4006 
  4007       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  4008         unfolding tan_45 tan_minus ..
  4009       also have "\<dots> = - (pi / 4)"
  4010         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  4011       also have "\<dots> = - (arctan (tan (pi / 4)))"
  4012         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  4013       also have "\<dots> = - (arctan 1)"
  4014         unfolding tan_45 ..
  4015       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  4016         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  4017       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  4018         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  4019         unfolding c_minus_minus by auto
  4020       finally show ?thesis using `x = -1` by auto
  4021     qed
  4022   qed
  4023 qed
  4024 
  4025 lemma arctan_half:
  4026   fixes x :: real
  4027   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  4028 proof -
  4029   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  4030     using tan_total by blast
  4031   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  4032     by auto
  4033 
  4034   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
  4035   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
  4036     by auto
  4037 
  4038   have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4039     unfolding tan_def power_divide ..
  4040   also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4041     using `cos y \<noteq> 0` by auto
  4042   also have "\<dots> = 1 / (cos y)\<^sup>2"
  4043     unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
  4044   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
  4045 
  4046   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
  4047     unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
  4048   also have "\<dots> = tan y / (1 + 1 / cos y)"
  4049     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
  4050   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
  4051     unfolding cos_sqrt ..
  4052   also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
  4053     unfolding real_sqrt_divide by auto
  4054   finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
  4055     unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
  4056 
  4057   have "arctan x = y"
  4058     using arctan_tan low high y_eq by auto
  4059   also have "\<dots> = 2 * (arctan (tan (y/2)))"
  4060     using arctan_tan[OF low2 high2] by auto
  4061   also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
  4062     unfolding tan_half by auto
  4063   finally show ?thesis
  4064     unfolding eq `tan y = x` .
  4065 qed
  4066 
  4067 lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
  4068   by (simp only: arctan_less_iff)
  4069 
  4070 lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
  4071   by (simp only: arctan_le_iff)
  4072 
  4073 lemma arctan_inverse:
  4074   assumes "x \<noteq> 0"
  4075   shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
  4076 proof (rule arctan_unique)
  4077   show "- (pi / 2) < sgn x * pi / 2 - arctan x"
  4078     using arctan_bounded [of x] assms
  4079     unfolding sgn_real_def
  4080     apply (auto simp add: algebra_simps)
  4081     apply (drule zero_less_arctan_iff [THEN iffD2])
  4082     apply arith
  4083     done
  4084   show "sgn x * pi / 2 - arctan x < pi / 2"
  4085     using arctan_bounded [of "- x"] assms
  4086     unfolding sgn_real_def arctan_minus
  4087     by (auto simp add: algebra_simps)
  4088   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
  4089     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
  4090     unfolding sgn_real_def
  4091     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
  4092 qed
  4093 
  4094 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
  4095 proof -
  4096   have "pi / 4 = arctan 1" using arctan_one by auto
  4097   also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
  4098   finally show ?thesis by auto
  4099 qed
  4100 
  4101 
  4102 subsection {* Existence of Polar Coordinates *}
  4103 
  4104 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
  4105   apply (rule power2_le_imp_le [OF _ zero_le_one])
  4106   apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
  4107   done
  4108 
  4109 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  4110   by (simp add: abs_le_iff)
  4111 
  4112 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
  4113   by (simp add: sin_arccos abs_le_iff)
  4114 
  4115 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  4116 
  4117 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  4118 
  4119 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  4120 proof -
  4121   have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  4122     apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
  4123     apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
  4124     apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
  4125                      real_sqrt_mult [symmetric] right_diff_distrib)
  4126     done
  4127   show ?thesis
  4128   proof (cases "0::real" y rule: linorder_cases)
  4129     case less 
  4130       then show ?thesis by (rule polar_ex1)
  4131   next
  4132     case equal
  4133       then show ?thesis
  4134         by (force simp add: intro!: cos_zero sin_zero)
  4135   next
  4136     case greater
  4137       then show ?thesis 
  4138      using polar_ex1 [where y="-y"]
  4139     by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
  4140   qed
  4141 qed
  4142 
  4143 end