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