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