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