src/HOL/Transcendental.thy
author huffman
Mon Jan 12 12:09:54 2009 -0800 (2009-01-12)
changeset 29460 ad87e5d1488b
parent 29171 5eff800a695f
child 29667 53103fc8ffa3
permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
     1 (*  Title       : Transcendental.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998,1999 University of Cambridge
     4                   1999,2001 University of Edinburgh
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6 *)
     7 
     8 header{*Power Series, Transcendental Functions etc.*}
     9 
    10 theory Transcendental
    11 imports Fact Series Deriv NthRoot
    12 begin
    13 
    14 subsection {* Properties of Power Series *}
    15 
    16 lemma lemma_realpow_diff:
    17   fixes y :: "'a::recpower"
    18   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
    19 proof -
    20   assume "p \<le> n"
    21   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
    22   thus ?thesis by (simp add: power_Suc power_commutes)
    23 qed
    24 
    25 lemma lemma_realpow_diff_sumr:
    26   fixes y :: "'a::{recpower,comm_semiring_0}" shows
    27      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
    28       y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
    29 by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
    30          del: setsum_op_ivl_Suc cong: strong_setsum_cong)
    31 
    32 lemma lemma_realpow_diff_sumr2:
    33   fixes y :: "'a::{recpower,comm_ring}" shows
    34      "x ^ (Suc n) - y ^ (Suc n) =  
    35       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
    36 apply (induct n, simp add: power_Suc)
    37 apply (simp add: power_Suc del: setsum_op_ivl_Suc)
    38 apply (subst setsum_op_ivl_Suc)
    39 apply (subst lemma_realpow_diff_sumr)
    40 apply (simp add: right_distrib del: setsum_op_ivl_Suc)
    41 apply (subst mult_left_commute [where a="x - y"])
    42 apply (erule subst)
    43 apply (simp add: power_Suc ring_simps)
    44 done
    45 
    46 lemma lemma_realpow_rev_sumr:
    47      "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
    48       (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
    49 apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
    50 apply (rule inj_onI, simp)
    51 apply auto
    52 apply (rule_tac x="n - x" in image_eqI, simp, simp)
    53 done
    54 
    55 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    56 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
    57 
    58 lemma powser_insidea:
    59   fixes x z :: "'a::{real_normed_field,banach,recpower}"
    60   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
    61   assumes 2: "norm z < norm x"
    62   shows "summable (\<lambda>n. norm (f n * z ^ n))"
    63 proof -
    64   from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
    65   from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
    66     by (rule summable_LIMSEQ_zero)
    67   hence "convergent (\<lambda>n. f n * x ^ n)"
    68     by (rule convergentI)
    69   hence "Cauchy (\<lambda>n. f n * x ^ n)"
    70     by (simp add: Cauchy_convergent_iff)
    71   hence "Bseq (\<lambda>n. f n * x ^ n)"
    72     by (rule Cauchy_Bseq)
    73   then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
    74     by (simp add: Bseq_def, safe)
    75   have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
    76                    K * norm (z ^ n) * inverse (norm (x ^ n))"
    77   proof (intro exI allI impI)
    78     fix n::nat assume "0 \<le> n"
    79     have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
    80           norm (f n * x ^ n) * norm (z ^ n)"
    81       by (simp add: norm_mult abs_mult)
    82     also have "\<dots> \<le> K * norm (z ^ n)"
    83       by (simp only: mult_right_mono 4 norm_ge_zero)
    84     also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
    85       by (simp add: x_neq_0)
    86     also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
    87       by (simp only: mult_assoc)
    88     finally show "norm (norm (f n * z ^ n)) \<le>
    89                   K * norm (z ^ n) * inverse (norm (x ^ n))"
    90       by (simp add: mult_le_cancel_right x_neq_0)
    91   qed
    92   moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
    93   proof -
    94     from 2 have "norm (norm (z * inverse x)) < 1"
    95       using x_neq_0
    96       by (simp add: nonzero_norm_divide divide_inverse [symmetric])
    97     hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
    98       by (rule summable_geometric)
    99     hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
   100       by (rule summable_mult)
   101     thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   102       using x_neq_0
   103       by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
   104                     power_inverse norm_power mult_assoc)
   105   qed
   106   ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
   107     by (rule summable_comparison_test)
   108 qed
   109 
   110 lemma powser_inside:
   111   fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
   112      "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
   113       ==> summable (%n. f(n) * (z ^ n))"
   114 by (rule powser_insidea [THEN summable_norm_cancel])
   115 
   116 
   117 subsection {* Term-by-Term Differentiability of Power Series *}
   118 
   119 definition
   120   diffs :: "(nat => 'a::ring_1) => nat => 'a" where
   121   "diffs c = (%n. of_nat (Suc n) * c(Suc n))"
   122 
   123 text{*Lemma about distributing negation over it*}
   124 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
   125 by (simp add: diffs_def)
   126 
   127 lemma sums_Suc_imp:
   128   assumes f: "f 0 = 0"
   129   shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   130 unfolding sums_def
   131 apply (rule LIMSEQ_imp_Suc)
   132 apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
   133 apply (simp only: setsum_shift_bounds_Suc_ivl)
   134 done
   135 
   136 lemma diffs_equiv:
   137      "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
   138       (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums  
   139          (\<Sum>n. (diffs c)(n) * (x ^ n))"
   140 unfolding diffs_def
   141 apply (drule summable_sums)
   142 apply (rule sums_Suc_imp, simp_all)
   143 done
   144 
   145 lemma lemma_termdiff1:
   146   fixes z :: "'a :: {recpower,comm_ring}" shows
   147   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
   148    (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   149 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
   150   cong: strong_setsum_cong)
   151 
   152 lemma sumr_diff_mult_const2:
   153   "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
   154 by (simp add: setsum_subtractf)
   155 
   156 lemma lemma_termdiff2:
   157   fixes h :: "'a :: {recpower,field}"
   158   assumes h: "h \<noteq> 0" shows
   159   "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   160    h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
   161         (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
   162 apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
   163 apply (simp add: right_diff_distrib diff_divide_distrib h)
   164 apply (simp add: mult_assoc [symmetric])
   165 apply (cases "n", simp)
   166 apply (simp add: lemma_realpow_diff_sumr2 h
   167                  right_diff_distrib [symmetric] mult_assoc
   168             del: realpow_Suc setsum_op_ivl_Suc of_nat_Suc)
   169 apply (subst lemma_realpow_rev_sumr)
   170 apply (subst sumr_diff_mult_const2)
   171 apply simp
   172 apply (simp only: lemma_termdiff1 setsum_right_distrib)
   173 apply (rule setsum_cong [OF refl])
   174 apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
   175 apply (clarify)
   176 apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
   177             del: setsum_op_ivl_Suc realpow_Suc)
   178 apply (subst mult_assoc [symmetric], subst power_add [symmetric])
   179 apply (simp add: mult_ac)
   180 done
   181 
   182 lemma real_setsum_nat_ivl_bounded2:
   183   fixes K :: "'a::ordered_semidom"
   184   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
   185   assumes K: "0 \<le> K"
   186   shows "setsum f {0..<n-k} \<le> of_nat n * K"
   187 apply (rule order_trans [OF setsum_mono])
   188 apply (rule f, simp)
   189 apply (simp add: mult_right_mono K)
   190 done
   191 
   192 lemma lemma_termdiff3:
   193   fixes h z :: "'a::{real_normed_field,recpower}"
   194   assumes 1: "h \<noteq> 0"
   195   assumes 2: "norm z \<le> K"
   196   assumes 3: "norm (z + h) \<le> K"
   197   shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
   198           \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   199 proof -
   200   have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
   201         norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
   202           (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
   203     apply (subst lemma_termdiff2 [OF 1])
   204     apply (subst norm_mult)
   205     apply (rule mult_commute)
   206     done
   207   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   208   proof (rule mult_right_mono [OF _ norm_ge_zero])
   209     from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
   210     have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
   211       apply (erule subst)
   212       apply (simp only: norm_mult norm_power power_add)
   213       apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
   214       done
   215     show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
   216               (z + h) ^ q * z ^ (n - 2 - q))
   217           \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
   218       apply (intro
   219          order_trans [OF norm_setsum]
   220          real_setsum_nat_ivl_bounded2
   221          mult_nonneg_nonneg
   222          zero_le_imp_of_nat
   223          zero_le_power K)
   224       apply (rule le_Kn, simp)
   225       done
   226   qed
   227   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   228     by (simp only: mult_assoc)
   229   finally show ?thesis .
   230 qed
   231 
   232 lemma lemma_termdiff4:
   233   fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
   234               'b::real_normed_vector"
   235   assumes k: "0 < (k::real)"
   236   assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   237   shows "f -- 0 --> 0"
   238 unfolding LIM_def diff_0_right
   239 proof (safe)
   240   let ?h = "of_real (k / 2)::'a"
   241   have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
   242   hence "norm (f ?h) \<le> K * norm ?h" by (rule le)
   243   hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero])
   244   hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff)
   245 
   246   fix r::real assume r: "0 < r"
   247   show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
   248   proof (cases)
   249     assume "K = 0"
   250     with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)"
   251       by simp
   252     thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" ..
   253   next
   254     assume K_neq_zero: "K \<noteq> 0"
   255     with zero_le_K have K: "0 < K" by simp
   256     show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
   257     proof (rule exI, safe)
   258       from k r K show "0 < min k (r * inverse K / 2)"
   259         by (simp add: mult_pos_pos positive_imp_inverse_positive)
   260     next
   261       fix x::'a
   262       assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)"
   263       from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2"
   264         by simp_all
   265       from x1 x3 le have "norm (f x) \<le> K * norm x" by simp
   266       also from x4 K have "K * norm x < K * (r * inverse K / 2)"
   267         by (rule mult_strict_left_mono)
   268       also have "\<dots> = r / 2"
   269         using K_neq_zero by simp
   270       also have "r / 2 < r"
   271         using r by simp
   272       finally show "norm (f x) < r" .
   273     qed
   274   qed
   275 qed
   276 
   277 lemma lemma_termdiff5:
   278   fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
   279               nat \<Rightarrow> 'b::banach"
   280   assumes k: "0 < (k::real)"
   281   assumes f: "summable f"
   282   assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   283   shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
   284 proof (rule lemma_termdiff4 [OF k])
   285   fix h::'a assume "h \<noteq> 0" and "norm h < k"
   286   hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
   287     by (simp add: le)
   288   hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
   289     by simp
   290   moreover from f have B: "summable (\<lambda>n. f n * norm h)"
   291     by (rule summable_mult2)
   292   ultimately have C: "summable (\<lambda>n. norm (g h n))"
   293     by (rule summable_comparison_test)
   294   hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
   295     by (rule summable_norm)
   296   also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
   297     by (rule summable_le)
   298   also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
   299     by (rule suminf_mult2 [symmetric])
   300   finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
   301 qed
   302 
   303 
   304 text{* FIXME: Long proofs*}
   305 
   306 lemma termdiffs_aux:
   307   fixes x :: "'a::{recpower,real_normed_field,banach}"
   308   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   309   assumes 2: "norm x < norm K"
   310   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
   311              - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   312 proof -
   313   from dense [OF 2]
   314   obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
   315   from norm_ge_zero r1 have r: "0 < r"
   316     by (rule order_le_less_trans)
   317   hence r_neq_0: "r \<noteq> 0" by simp
   318   show ?thesis
   319   proof (rule lemma_termdiff5)
   320     show "0 < r - norm x" using r1 by simp
   321   next
   322     from r r2 have "norm (of_real r::'a) < norm K"
   323       by simp
   324     with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
   325       by (rule powser_insidea)
   326     hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
   327       using r
   328       by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
   329     hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
   330       by (rule diffs_equiv [THEN sums_summable])
   331     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))
   332       = (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
   333       apply (rule ext)
   334       apply (simp add: diffs_def)
   335       apply (case_tac n, simp_all add: r_neq_0)
   336       done
   337     finally have "summable 
   338       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
   339       by (rule diffs_equiv [THEN sums_summable])
   340     also have
   341       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
   342            r ^ (n - Suc 0)) =
   343        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
   344       apply (rule ext)
   345       apply (case_tac "n", simp)
   346       apply (case_tac "nat", simp)
   347       apply (simp add: r_neq_0)
   348       done
   349     finally show
   350       "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   351   next
   352     fix h::'a and n::nat
   353     assume h: "h \<noteq> 0"
   354     assume "norm h < r - norm x"
   355     hence "norm x + norm h < r" by simp
   356     with norm_triangle_ineq have xh: "norm (x + h) < r"
   357       by (rule order_le_less_trans)
   358     show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
   359           \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
   360       apply (simp only: norm_mult mult_assoc)
   361       apply (rule mult_left_mono [OF _ norm_ge_zero])
   362       apply (simp (no_asm) add: mult_assoc [symmetric])
   363       apply (rule lemma_termdiff3)
   364       apply (rule h)
   365       apply (rule r1 [THEN order_less_imp_le])
   366       apply (rule xh [THEN order_less_imp_le])
   367       done
   368   qed
   369 qed
   370 
   371 lemma termdiffs:
   372   fixes K x :: "'a::{recpower,real_normed_field,banach}"
   373   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   374   assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   375   assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   376   assumes 4: "norm x < norm K"
   377   shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
   378 unfolding deriv_def
   379 proof (rule LIM_zero_cancel)
   380   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
   381             - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   382   proof (rule LIM_equal2)
   383     show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   384   next
   385     fix h :: 'a
   386     assume "h \<noteq> 0"
   387     assume "norm (h - 0) < norm K - norm x"
   388     hence "norm x + norm h < norm K" by simp
   389     hence 5: "norm (x + h) < norm K"
   390       by (rule norm_triangle_ineq [THEN order_le_less_trans])
   391     have A: "summable (\<lambda>n. c n * x ^ n)"
   392       by (rule powser_inside [OF 1 4])
   393     have B: "summable (\<lambda>n. c n * (x + h) ^ n)"
   394       by (rule powser_inside [OF 1 5])
   395     have C: "summable (\<lambda>n. diffs c n * x ^ n)"
   396       by (rule powser_inside [OF 2 4])
   397     show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
   398              - (\<Sum>n. diffs c n * x ^ n) = 
   399           (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   400       apply (subst sums_unique [OF diffs_equiv [OF C]])
   401       apply (subst suminf_diff [OF B A])
   402       apply (subst suminf_divide [symmetric])
   403       apply (rule summable_diff [OF B A])
   404       apply (subst suminf_diff)
   405       apply (rule summable_divide)
   406       apply (rule summable_diff [OF B A])
   407       apply (rule sums_summable [OF diffs_equiv [OF C]])
   408       apply (rule arg_cong [where f="suminf"], rule ext)
   409       apply (simp add: ring_simps)
   410       done
   411   next
   412     show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
   413                of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   414         by (rule termdiffs_aux [OF 3 4])
   415   qed
   416 qed
   417 
   418 
   419 subsection {* Exponential Function *}
   420 
   421 definition
   422   exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
   423   "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
   424 
   425 lemma summable_exp_generic:
   426   fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
   427   defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
   428   shows "summable S"
   429 proof -
   430   have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
   431     unfolding S_def by (simp add: power_Suc del: mult_Suc)
   432   obtain r :: real where r0: "0 < r" and r1: "r < 1"
   433     using dense [OF zero_less_one] by fast
   434   obtain N :: nat where N: "norm x < real N * r"
   435     using reals_Archimedean3 [OF r0] by fast
   436   from r1 show ?thesis
   437   proof (rule ratio_test [rule_format])
   438     fix n :: nat
   439     assume n: "N \<le> n"
   440     have "norm x \<le> real N * r"
   441       using N by (rule order_less_imp_le)
   442     also have "real N * r \<le> real (Suc n) * r"
   443       using r0 n by (simp add: mult_right_mono)
   444     finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)"
   445       using norm_ge_zero by (rule mult_right_mono)
   446     hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
   447       by (rule order_trans [OF norm_mult_ineq])
   448     hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
   449       by (simp add: pos_divide_le_eq mult_ac)
   450     thus "norm (S (Suc n)) \<le> r * norm (S n)"
   451       by (simp add: S_Suc norm_scaleR inverse_eq_divide)
   452   qed
   453 qed
   454 
   455 lemma summable_norm_exp:
   456   fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
   457   shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
   458 proof (rule summable_norm_comparison_test [OF exI, rule_format])
   459   show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
   460     by (rule summable_exp_generic)
   461 next
   462   fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
   463     by (simp add: norm_scaleR norm_power_ineq)
   464 qed
   465 
   466 lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
   467 by (insert summable_exp_generic [where x=x], simp)
   468 
   469 lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
   470 unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
   471 
   472 
   473 lemma exp_fdiffs: 
   474       "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
   475 by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
   476          del: mult_Suc of_nat_Suc)
   477 
   478 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
   479 by (simp add: diffs_def)
   480 
   481 lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
   482 by (auto intro!: ext simp add: exp_def)
   483 
   484 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
   485 apply (simp add: exp_def)
   486 apply (subst lemma_exp_ext)
   487 apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)")
   488 apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
   489 apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
   490 apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
   491 apply (simp del: of_real_add)
   492 done
   493 
   494 lemma isCont_exp [simp]: "isCont exp x"
   495 by (rule DERIV_exp [THEN DERIV_isCont])
   496 
   497 
   498 subsubsection {* Properties of the Exponential Function *}
   499 
   500 lemma powser_zero:
   501   fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
   502   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
   503 proof -
   504   have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
   505     by (rule sums_unique [OF series_zero], simp add: power_0_left)
   506   thus ?thesis by simp
   507 qed
   508 
   509 lemma exp_zero [simp]: "exp 0 = 1"
   510 unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
   511 
   512 lemma setsum_cl_ivl_Suc2:
   513   "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
   514 by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
   515          del: setsum_cl_ivl_Suc)
   516 
   517 lemma exp_series_add:
   518   fixes x y :: "'a::{real_field,recpower}"
   519   defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
   520   shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
   521 proof (induct n)
   522   case 0
   523   show ?case
   524     unfolding S_def by simp
   525 next
   526   case (Suc n)
   527   have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
   528     unfolding S_def by (simp add: power_Suc del: mult_Suc)
   529   hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
   530     by simp
   531 
   532   have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
   533     by (simp only: times_S)
   534   also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
   535     by (simp only: Suc)
   536   also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
   537                 + y * (\<Sum>i=0..n. S x i * S y (n-i))"
   538     by (rule left_distrib)
   539   also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
   540                 + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
   541     by (simp only: setsum_right_distrib mult_ac)
   542   also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
   543                 + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
   544     by (simp add: times_S Suc_diff_le)
   545   also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
   546              (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
   547     by (subst setsum_cl_ivl_Suc2, simp)
   548   also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
   549              (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
   550     by (subst setsum_cl_ivl_Suc, simp)
   551   also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
   552              (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
   553              (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
   554     by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
   555               real_of_nat_add [symmetric], simp)
   556   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
   557     by (simp only: scaleR_right.setsum)
   558   finally show
   559     "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
   560     by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
   561 qed
   562 
   563 lemma exp_add: "exp (x + y) = exp x * exp y"
   564 unfolding exp_def
   565 by (simp only: Cauchy_product summable_norm_exp exp_series_add)
   566 
   567 lemma mult_exp_exp: "exp x * exp y = exp (x + y)"
   568 by (rule exp_add [symmetric])
   569 
   570 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
   571 unfolding exp_def
   572 apply (subst of_real.suminf)
   573 apply (rule summable_exp_generic)
   574 apply (simp add: scaleR_conv_of_real)
   575 done
   576 
   577 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
   578 proof
   579   have "exp x * exp (- x) = 1" by (simp add: mult_exp_exp)
   580   also assume "exp x = 0"
   581   finally show "False" by simp
   582 qed
   583 
   584 lemma exp_minus: "exp (- x) = inverse (exp x)"
   585 by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
   586 
   587 lemma exp_diff: "exp (x - y) = exp x / exp y"
   588   unfolding diff_minus divide_inverse
   589   by (simp add: exp_add exp_minus)
   590 
   591 
   592 subsubsection {* Properties of the Exponential Function on Reals *}
   593 
   594 text {* Comparisons of @{term "exp x"} with zero. *}
   595 
   596 text{*Proof: because every exponential can be seen as a square.*}
   597 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
   598 proof -
   599   have "0 \<le> exp (x/2) * exp (x/2)" by simp
   600   thus ?thesis by (simp add: exp_add [symmetric])
   601 qed
   602 
   603 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
   604 by (simp add: order_less_le)
   605 
   606 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
   607 by (simp add: not_less)
   608 
   609 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
   610 by (simp add: not_le)
   611 
   612 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
   613 by simp
   614 
   615 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
   616 apply (induct "n")
   617 apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
   618 done
   619 
   620 text {* Strict monotonicity of exponential. *}
   621 
   622 lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
   623 apply (drule order_le_imp_less_or_eq, auto)
   624 apply (simp add: exp_def)
   625 apply (rule real_le_trans)
   626 apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
   627 apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
   628 done
   629 
   630 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
   631 proof -
   632   assume x: "0 < x"
   633   hence "1 < 1 + x" by simp
   634   also from x have "1 + x \<le> exp x"
   635     by (simp add: exp_ge_add_one_self_aux)
   636   finally show ?thesis .
   637 qed
   638 
   639 lemma exp_less_mono:
   640   fixes x y :: real
   641   assumes "x < y" shows "exp x < exp y"
   642 proof -
   643   from `x < y` have "0 < y - x" by simp
   644   hence "1 < exp (y - x)" by (rule exp_gt_one)
   645   hence "1 < exp y / exp x" by (simp only: exp_diff)
   646   thus "exp x < exp y" by simp
   647 qed
   648 
   649 lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y"
   650 apply (simp add: linorder_not_le [symmetric])
   651 apply (auto simp add: order_le_less exp_less_mono)
   652 done
   653 
   654 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
   655 by (auto intro: exp_less_mono exp_less_cancel)
   656 
   657 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
   658 by (auto simp add: linorder_not_less [symmetric])
   659 
   660 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
   661 by (simp add: order_eq_iff)
   662 
   663 text {* Comparisons of @{term "exp x"} with one. *}
   664 
   665 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
   666   using exp_less_cancel_iff [where x=0 and y=x] by simp
   667 
   668 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
   669   using exp_less_cancel_iff [where x=x and y=0] by simp
   670 
   671 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
   672   using exp_le_cancel_iff [where x=0 and y=x] by simp
   673 
   674 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
   675   using exp_le_cancel_iff [where x=x and y=0] by simp
   676 
   677 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
   678   using exp_inj_iff [where x=x and y=0] by simp
   679 
   680 lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
   681 apply (rule IVT)
   682 apply (auto intro: isCont_exp simp add: le_diff_eq)
   683 apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)") 
   684 apply simp
   685 apply (rule exp_ge_add_one_self_aux, simp)
   686 done
   687 
   688 lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y"
   689 apply (rule_tac x = 1 and y = y in linorder_cases)
   690 apply (drule order_less_imp_le [THEN lemma_exp_total])
   691 apply (rule_tac [2] x = 0 in exI)
   692 apply (frule_tac [3] real_inverse_gt_one)
   693 apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
   694 apply (rule_tac x = "-x" in exI)
   695 apply (simp add: exp_minus)
   696 done
   697 
   698 
   699 subsection {* Natural Logarithm *}
   700 
   701 definition
   702   ln :: "real => real" where
   703   "ln x = (THE u. exp u = x)"
   704 
   705 lemma ln_exp [simp]: "ln (exp x) = x"
   706 by (simp add: ln_def)
   707 
   708 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
   709 by (auto dest: exp_total)
   710 
   711 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
   712 apply (rule iffI)
   713 apply (erule subst, rule exp_gt_zero)
   714 apply (erule exp_ln)
   715 done
   716 
   717 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
   718 by (erule subst, rule ln_exp)
   719 
   720 lemma ln_one [simp]: "ln 1 = 0"
   721 by (rule ln_unique, simp)
   722 
   723 lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
   724 by (rule ln_unique, simp add: exp_add)
   725 
   726 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   727 by (rule ln_unique, simp add: exp_minus)
   728 
   729 lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
   730 by (rule ln_unique, simp add: exp_diff)
   731 
   732 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
   733 by (rule ln_unique, simp add: exp_real_of_nat_mult)
   734 
   735 lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   736 by (subst exp_less_cancel_iff [symmetric], simp)
   737 
   738 lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
   739 by (simp add: linorder_not_less [symmetric])
   740 
   741 lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   742 by (simp add: order_eq_iff)
   743 
   744 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   745 apply (rule exp_le_cancel_iff [THEN iffD1])
   746 apply (simp add: exp_ge_add_one_self_aux)
   747 done
   748 
   749 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
   750 by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
   751 
   752 lemma ln_ge_zero [simp]:
   753   assumes x: "1 \<le> x" shows "0 \<le> ln x"
   754 proof -
   755   have "0 < x" using x by arith
   756   hence "exp 0 \<le> exp (ln x)"
   757     by (simp add: x)
   758   thus ?thesis by (simp only: exp_le_cancel_iff)
   759 qed
   760 
   761 lemma ln_ge_zero_imp_ge_one:
   762   assumes ln: "0 \<le> ln x" 
   763       and x:  "0 < x"
   764   shows "1 \<le> x"
   765 proof -
   766   from ln have "ln 1 \<le> ln x" by simp
   767   thus ?thesis by (simp add: x del: ln_one) 
   768 qed
   769 
   770 lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
   771 by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
   772 
   773 lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
   774 by (insert ln_ge_zero_iff [of x], arith)
   775 
   776 lemma ln_gt_zero:
   777   assumes x: "1 < x" shows "0 < ln x"
   778 proof -
   779   have "0 < x" using x by arith
   780   hence "exp 0 < exp (ln x)" by (simp add: x)
   781   thus ?thesis  by (simp only: exp_less_cancel_iff)
   782 qed
   783 
   784 lemma ln_gt_zero_imp_gt_one:
   785   assumes ln: "0 < ln x" 
   786       and x:  "0 < x"
   787   shows "1 < x"
   788 proof -
   789   from ln have "ln 1 < ln x" by simp
   790   thus ?thesis by (simp add: x del: ln_one) 
   791 qed
   792 
   793 lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
   794 by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
   795 
   796 lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
   797 by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
   798 
   799 lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
   800 by simp
   801 
   802 lemma exp_ln_eq: "exp u = x ==> ln x = u"
   803 by auto
   804 
   805 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
   806 apply (subgoal_tac "isCont ln (exp (ln x))", simp)
   807 apply (rule isCont_inverse_function [where f=exp], simp_all)
   808 done
   809 
   810 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
   811 apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
   812 apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
   813 apply (simp_all add: abs_if isCont_ln)
   814 done
   815 
   816 
   817 subsection {* Sine and Cosine *}
   818 
   819 definition
   820   sin :: "real => real" where
   821   "sin x = (\<Sum>n. (if even(n) then 0 else
   822              (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
   823  
   824 definition
   825   cos :: "real => real" where
   826   "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n)) 
   827                             else 0) * x ^ n)"
   828 
   829 lemma summable_sin: 
   830      "summable (%n.  
   831            (if even n then 0  
   832            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
   833                 x ^ n)"
   834 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
   835 apply (rule_tac [2] summable_exp)
   836 apply (rule_tac x = 0 in exI)
   837 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
   838 done
   839 
   840 lemma summable_cos: 
   841       "summable (%n.  
   842            (if even n then  
   843            -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
   844 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
   845 apply (rule_tac [2] summable_exp)
   846 apply (rule_tac x = 0 in exI)
   847 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
   848 done
   849 
   850 lemma lemma_STAR_sin:
   851      "(if even n then 0  
   852        else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
   853 by (induct "n", auto)
   854 
   855 lemma lemma_STAR_cos:
   856      "0 < n -->  
   857       -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
   858 by (induct "n", auto)
   859 
   860 lemma lemma_STAR_cos1:
   861      "0 < n -->  
   862       (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
   863 by (induct "n", auto)
   864 
   865 lemma lemma_STAR_cos2:
   866   "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
   867                          else 0) = 0"
   868 apply (induct "n")
   869 apply (case_tac [2] "n", auto)
   870 done
   871 
   872 lemma sin_converges: 
   873       "(%n. (if even n then 0  
   874             else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
   875                  x ^ n) sums sin(x)"
   876 unfolding sin_def by (rule summable_sin [THEN summable_sums])
   877 
   878 lemma cos_converges: 
   879       "(%n. (if even n then  
   880            -1 ^ (n div 2)/(real (fact n))  
   881            else 0) * x ^ n) sums cos(x)"
   882 unfolding cos_def by (rule summable_cos [THEN summable_sums])
   883 
   884 lemma sin_fdiffs: 
   885       "diffs(%n. if even n then 0  
   886            else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))  
   887        = (%n. if even n then  
   888                  -1 ^ (n div 2)/(real (fact n))  
   889               else 0)"
   890 by (auto intro!: ext 
   891          simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
   892          simp del: mult_Suc of_nat_Suc)
   893 
   894 lemma sin_fdiffs2: 
   895        "diffs(%n. if even n then 0  
   896            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n  
   897        = (if even n then  
   898                  -1 ^ (n div 2)/(real (fact n))  
   899               else 0)"
   900 by (simp only: sin_fdiffs)
   901 
   902 lemma cos_fdiffs: 
   903       "diffs(%n. if even n then  
   904                  -1 ^ (n div 2)/(real (fact n)) else 0)  
   905        = (%n. - (if even n then 0  
   906            else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
   907 by (auto intro!: ext 
   908          simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
   909          simp del: mult_Suc of_nat_Suc)
   910 
   911 
   912 lemma cos_fdiffs2: 
   913       "diffs(%n. if even n then  
   914                  -1 ^ (n div 2)/(real (fact n)) else 0) n 
   915        = - (if even n then 0  
   916            else -1 ^ ((n - Suc 0)div 2)/(real (fact n)))"
   917 by (simp only: cos_fdiffs)
   918 
   919 text{*Now at last we can get the derivatives of exp, sin and cos*}
   920 
   921 lemma lemma_sin_minus:
   922      "- sin x = (\<Sum>n. - ((if even n then 0 
   923                   else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
   924 by (auto intro!: sums_unique sums_minus sin_converges)
   925 
   926 lemma lemma_sin_ext:
   927      "sin = (%x. \<Sum>n. 
   928                    (if even n then 0  
   929                        else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
   930                    x ^ n)"
   931 by (auto intro!: ext simp add: sin_def)
   932 
   933 lemma lemma_cos_ext:
   934      "cos = (%x. \<Sum>n. 
   935                    (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
   936                    x ^ n)"
   937 by (auto intro!: ext simp add: cos_def)
   938 
   939 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
   940 apply (simp add: cos_def)
   941 apply (subst lemma_sin_ext)
   942 apply (auto simp add: sin_fdiffs2 [symmetric])
   943 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
   944 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
   945 done
   946 
   947 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
   948 apply (subst lemma_cos_ext)
   949 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
   950 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
   951 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
   952 done
   953 
   954 lemma isCont_sin [simp]: "isCont sin x"
   955 by (rule DERIV_sin [THEN DERIV_isCont])
   956 
   957 lemma isCont_cos [simp]: "isCont cos x"
   958 by (rule DERIV_cos [THEN DERIV_isCont])
   959 
   960 
   961 subsection {* Properties of Sine and Cosine *}
   962 
   963 lemma sin_zero [simp]: "sin 0 = 0"
   964 unfolding sin_def by (simp add: powser_zero)
   965 
   966 lemma cos_zero [simp]: "cos 0 = 1"
   967 unfolding cos_def by (simp add: powser_zero)
   968 
   969 lemma DERIV_sin_sin_mult [simp]:
   970      "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
   971 by (rule DERIV_mult, auto)
   972 
   973 lemma DERIV_sin_sin_mult2 [simp]:
   974      "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
   975 apply (cut_tac x = x in DERIV_sin_sin_mult)
   976 apply (auto simp add: mult_assoc)
   977 done
   978 
   979 lemma DERIV_sin_realpow2 [simp]:
   980      "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
   981 by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
   982 
   983 lemma DERIV_sin_realpow2a [simp]:
   984      "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
   985 by (auto simp add: numeral_2_eq_2)
   986 
   987 lemma DERIV_cos_cos_mult [simp]:
   988      "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
   989 by (rule DERIV_mult, auto)
   990 
   991 lemma DERIV_cos_cos_mult2 [simp]:
   992      "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
   993 apply (cut_tac x = x in DERIV_cos_cos_mult)
   994 apply (auto simp add: mult_ac)
   995 done
   996 
   997 lemma DERIV_cos_realpow2 [simp]:
   998      "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
   999 by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
  1000 
  1001 lemma DERIV_cos_realpow2a [simp]:
  1002      "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
  1003 by (auto simp add: numeral_2_eq_2)
  1004 
  1005 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
  1006 by auto
  1007 
  1008 lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
  1009 apply (rule lemma_DERIV_subst)
  1010 apply (rule DERIV_cos_realpow2a, auto)
  1011 done
  1012 
  1013 (* most useful *)
  1014 lemma DERIV_cos_cos_mult3 [simp]:
  1015      "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
  1016 apply (rule lemma_DERIV_subst)
  1017 apply (rule DERIV_cos_cos_mult2, auto)
  1018 done
  1019 
  1020 lemma DERIV_sin_circle_all: 
  1021      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
  1022              (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
  1023 apply (simp only: diff_minus, safe)
  1024 apply (rule DERIV_add) 
  1025 apply (auto simp add: numeral_2_eq_2)
  1026 done
  1027 
  1028 lemma DERIV_sin_circle_all_zero [simp]:
  1029      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
  1030 by (cut_tac DERIV_sin_circle_all, auto)
  1031 
  1032 lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
  1033 apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
  1034 apply (auto simp add: numeral_2_eq_2)
  1035 done
  1036 
  1037 lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
  1038 apply (subst add_commute)
  1039 apply (simp (no_asm) del: realpow_Suc)
  1040 done
  1041 
  1042 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  1043 apply (cut_tac x = x in sin_cos_squared_add2)
  1044 apply (auto simp add: numeral_2_eq_2)
  1045 done
  1046 
  1047 lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
  1048 apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
  1049 apply (simp del: realpow_Suc)
  1050 done
  1051 
  1052 lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
  1053 apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
  1054 apply (simp del: realpow_Suc)
  1055 done
  1056 
  1057 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  1058 by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  1059 
  1060 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  1061 apply (insert abs_sin_le_one [of x]) 
  1062 apply (simp add: abs_le_iff del: abs_sin_le_one) 
  1063 done
  1064 
  1065 lemma sin_le_one [simp]: "sin x \<le> 1"
  1066 apply (insert abs_sin_le_one [of x]) 
  1067 apply (simp add: abs_le_iff del: abs_sin_le_one) 
  1068 done
  1069 
  1070 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  1071 by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  1072 
  1073 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  1074 apply (insert abs_cos_le_one [of x]) 
  1075 apply (simp add: abs_le_iff del: abs_cos_le_one) 
  1076 done
  1077 
  1078 lemma cos_le_one [simp]: "cos x \<le> 1"
  1079 apply (insert abs_cos_le_one [of x]) 
  1080 apply (simp add: abs_le_iff del: abs_cos_le_one)
  1081 done
  1082 
  1083 lemma DERIV_fun_pow: "DERIV g x :> m ==>  
  1084       DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  1085 apply (rule lemma_DERIV_subst)
  1086 apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
  1087 apply (rule DERIV_pow, auto)
  1088 done
  1089 
  1090 lemma DERIV_fun_exp:
  1091      "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
  1092 apply (rule lemma_DERIV_subst)
  1093 apply (rule_tac f = exp in DERIV_chain2)
  1094 apply (rule DERIV_exp, auto)
  1095 done
  1096 
  1097 lemma DERIV_fun_sin:
  1098      "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
  1099 apply (rule lemma_DERIV_subst)
  1100 apply (rule_tac f = sin in DERIV_chain2)
  1101 apply (rule DERIV_sin, auto)
  1102 done
  1103 
  1104 lemma DERIV_fun_cos:
  1105      "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
  1106 apply (rule lemma_DERIV_subst)
  1107 apply (rule_tac f = cos in DERIV_chain2)
  1108 apply (rule DERIV_cos, auto)
  1109 done
  1110 
  1111 lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
  1112                     DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
  1113                     DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
  1114                     DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
  1115                     DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
  1116 
  1117 (* lemma *)
  1118 lemma lemma_DERIV_sin_cos_add:
  1119      "\<forall>x.  
  1120          DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
  1121                (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
  1122 apply (safe, rule lemma_DERIV_subst)
  1123 apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  1124   --{*replaces the old @{text DERIV_tac}*}
  1125 apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
  1126 done
  1127 
  1128 lemma sin_cos_add [simp]:
  1129      "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
  1130       (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
  1131 apply (cut_tac y = 0 and x = x and y7 = y 
  1132        in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
  1133 apply (auto simp add: numeral_2_eq_2)
  1134 done
  1135 
  1136 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  1137 apply (cut_tac x = x and y = y in sin_cos_add)
  1138 apply (simp del: sin_cos_add)
  1139 done
  1140 
  1141 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  1142 apply (cut_tac x = x and y = y in sin_cos_add)
  1143 apply (simp del: sin_cos_add)
  1144 done
  1145 
  1146 lemma lemma_DERIV_sin_cos_minus:
  1147     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
  1148 apply (safe, rule lemma_DERIV_subst)
  1149 apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  1150 apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
  1151 done
  1152 
  1153 lemma sin_cos_minus: 
  1154     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
  1155 apply (cut_tac y = 0 and x = x 
  1156        in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
  1157 apply simp
  1158 done
  1159 
  1160 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  1161   using sin_cos_minus [where x=x] by simp
  1162 
  1163 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  1164   using sin_cos_minus [where x=x] by simp
  1165 
  1166 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  1167 by (simp add: diff_minus sin_add)
  1168 
  1169 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  1170 by (simp add: sin_diff mult_commute)
  1171 
  1172 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  1173 by (simp add: diff_minus cos_add)
  1174 
  1175 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  1176 by (simp add: cos_diff mult_commute)
  1177 
  1178 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  1179   using sin_add [where x=x and y=x] by simp
  1180 
  1181 lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
  1182   using cos_add [where x=x and y=x]
  1183   by (simp add: power2_eq_square)
  1184 
  1185 
  1186 subsection {* The Constant Pi *}
  1187 
  1188 definition
  1189   pi :: "real" where
  1190   "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  1191 
  1192 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
  1193    hence define pi.*}
  1194 
  1195 lemma sin_paired:
  1196      "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
  1197       sums  sin x"
  1198 proof -
  1199   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
  1200             (if even k then 0
  1201              else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
  1202             x ^ k) 
  1203 	sums sin x"
  1204     unfolding sin_def
  1205     by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
  1206   thus ?thesis by (simp add: mult_ac)
  1207 qed
  1208 
  1209 lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
  1210 apply (subgoal_tac 
  1211        "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
  1212               -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1)) 
  1213      sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
  1214  prefer 2
  1215  apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
  1216 apply (rotate_tac 2)
  1217 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
  1218 apply (auto simp del: fact_Suc realpow_Suc)
  1219 apply (frule sums_unique)
  1220 apply (auto simp del: fact_Suc realpow_Suc)
  1221 apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
  1222 apply (auto simp del: fact_Suc realpow_Suc)
  1223 apply (erule sums_summable)
  1224 apply (case_tac "m=0")
  1225 apply (simp (no_asm_simp))
  1226 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x") 
  1227 apply (simp only: mult_less_cancel_left, simp)  
  1228 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
  1229 apply (subgoal_tac "x*x < 2*3", simp) 
  1230 apply (rule mult_strict_mono)
  1231 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
  1232 apply (subst fact_Suc)
  1233 apply (subst fact_Suc)
  1234 apply (subst fact_Suc)
  1235 apply (subst fact_Suc)
  1236 apply (subst real_of_nat_mult)
  1237 apply (subst real_of_nat_mult)
  1238 apply (subst real_of_nat_mult)
  1239 apply (subst real_of_nat_mult)
  1240 apply (simp (no_asm) add: divide_inverse del: fact_Suc)
  1241 apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
  1242 apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
  1243 apply (auto simp add: mult_assoc simp del: fact_Suc)
  1244 apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
  1245 apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
  1246 apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
  1247 apply (erule ssubst)+
  1248 apply (auto simp del: fact_Suc)
  1249 apply (subgoal_tac "0 < x ^ (4 * m) ")
  1250  prefer 2 apply (simp only: zero_less_power) 
  1251 apply (simp (no_asm_simp) add: mult_less_cancel_left)
  1252 apply (rule mult_strict_mono)
  1253 apply (simp_all (no_asm_simp))
  1254 done
  1255 
  1256 lemma sin_gt_zero1: "[|0 < x; x < 2 |] ==> 0 < sin x"
  1257 by (auto intro: sin_gt_zero)
  1258 
  1259 lemma cos_double_less_one: "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"
  1260 apply (cut_tac x = x in sin_gt_zero1)
  1261 apply (auto simp add: cos_squared_eq cos_double)
  1262 done
  1263 
  1264 lemma cos_paired:
  1265      "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  1266 proof -
  1267   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
  1268             (if even k then -1 ^ (k div 2) / real (fact k) else 0) *
  1269             x ^ k) 
  1270         sums cos x"
  1271     unfolding cos_def
  1272     by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) 
  1273   thus ?thesis by (simp add: mult_ac)
  1274 qed
  1275 
  1276 lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
  1277 by simp
  1278 
  1279 lemma cos_two_less_zero [simp]: "cos (2) < 0"
  1280 apply (cut_tac x = 2 in cos_paired)
  1281 apply (drule sums_minus)
  1282 apply (rule neg_less_iff_less [THEN iffD1]) 
  1283 apply (frule sums_unique, auto)
  1284 apply (rule_tac y =
  1285  "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
  1286        in order_less_trans)
  1287 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
  1288 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
  1289 apply (rule sumr_pos_lt_pair)
  1290 apply (erule sums_summable, safe)
  1291 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
  1292             del: fact_Suc)
  1293 apply (rule real_mult_inverse_cancel2)
  1294 apply (rule real_of_nat_fact_gt_zero)+
  1295 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
  1296 apply (subst fact_lemma) 
  1297 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  1298 apply (simp only: real_of_nat_mult)
  1299 apply (rule mult_strict_mono, force)
  1300   apply (rule_tac [3] real_of_nat_ge_zero)
  1301  prefer 2 apply force
  1302 apply (rule real_of_nat_less_iff [THEN iffD2])
  1303 apply (rule fact_less_mono, auto)
  1304 done
  1305 
  1306 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  1307 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  1308 
  1309 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
  1310 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0")
  1311 apply (rule_tac [2] IVT2)
  1312 apply (auto intro: DERIV_isCont DERIV_cos)
  1313 apply (cut_tac x = xa and y = y in linorder_less_linear)
  1314 apply (rule ccontr)
  1315 apply (subgoal_tac " (\<forall>x. cos differentiable x) & (\<forall>x. isCont cos x) ")
  1316 apply (auto intro: DERIV_cos DERIV_isCont simp add: differentiable_def)
  1317 apply (drule_tac f = cos in Rolle)
  1318 apply (drule_tac [5] f = cos in Rolle)
  1319 apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
  1320 apply (drule_tac y1 = xa in order_le_less_trans [THEN sin_gt_zero])
  1321 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
  1322 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
  1323 done
  1324     
  1325 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  1326 by (simp add: pi_def)
  1327 
  1328 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  1329 by (simp add: pi_half cos_is_zero [THEN theI'])
  1330 
  1331 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  1332 apply (rule order_le_neq_trans)
  1333 apply (simp add: pi_half cos_is_zero [THEN theI'])
  1334 apply (rule notI, drule arg_cong [where f=cos], simp)
  1335 done
  1336 
  1337 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  1338 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  1339 
  1340 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  1341 apply (rule order_le_neq_trans)
  1342 apply (simp add: pi_half cos_is_zero [THEN theI'])
  1343 apply (rule notI, drule arg_cong [where f=cos], simp)
  1344 done
  1345 
  1346 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  1347 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  1348 
  1349 lemma pi_gt_zero [simp]: "0 < pi"
  1350 by (insert pi_half_gt_zero, simp)
  1351 
  1352 lemma pi_ge_zero [simp]: "0 \<le> pi"
  1353 by (rule pi_gt_zero [THEN order_less_imp_le])
  1354 
  1355 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  1356 by (rule pi_gt_zero [THEN less_imp_neq, THEN not_sym])
  1357 
  1358 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  1359 by (simp add: linorder_not_less)
  1360 
  1361 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  1362 by simp
  1363 
  1364 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  1365 apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
  1366 apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
  1367 apply (simp add: power2_eq_square)
  1368 done
  1369 
  1370 lemma cos_pi [simp]: "cos pi = -1"
  1371 by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
  1372 
  1373 lemma sin_pi [simp]: "sin pi = 0"
  1374 by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
  1375 
  1376 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  1377 by (simp add: diff_minus cos_add)
  1378 declare sin_cos_eq [symmetric, simp]
  1379 
  1380 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  1381 by (simp add: cos_add)
  1382 declare minus_sin_cos_eq [symmetric, simp]
  1383 
  1384 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  1385 by (simp add: diff_minus sin_add)
  1386 declare cos_sin_eq [symmetric, simp]
  1387 
  1388 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  1389 by (simp add: sin_add)
  1390 
  1391 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  1392 by (simp add: sin_add)
  1393 
  1394 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  1395 by (simp add: cos_add)
  1396 
  1397 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  1398 by (simp add: sin_add cos_double)
  1399 
  1400 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  1401 by (simp add: cos_add cos_double)
  1402 
  1403 lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
  1404 apply (induct "n")
  1405 apply (auto simp add: real_of_nat_Suc left_distrib)
  1406 done
  1407 
  1408 lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
  1409 proof -
  1410   have "cos (pi * real n) = cos (real n * pi)" by (simp only: mult_commute)
  1411   also have "... = -1 ^ n" by (rule cos_npi) 
  1412   finally show ?thesis .
  1413 qed
  1414 
  1415 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  1416 apply (induct "n")
  1417 apply (auto simp add: real_of_nat_Suc left_distrib)
  1418 done
  1419 
  1420 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  1421 by (simp add: mult_commute [of pi]) 
  1422 
  1423 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  1424 by (simp add: cos_double)
  1425 
  1426 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  1427 by simp
  1428 
  1429 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  1430 apply (rule sin_gt_zero, assumption)
  1431 apply (rule order_less_trans, assumption)
  1432 apply (rule pi_half_less_two)
  1433 done
  1434 
  1435 lemma sin_less_zero: 
  1436   assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
  1437 proof -
  1438   have "0 < sin (- x)" using prems by (simp only: sin_gt_zero2) 
  1439   thus ?thesis by simp
  1440 qed
  1441 
  1442 lemma pi_less_4: "pi < 4"
  1443 by (cut_tac pi_half_less_two, auto)
  1444 
  1445 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  1446 apply (cut_tac pi_less_4)
  1447 apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  1448 apply (cut_tac cos_is_zero, safe)
  1449 apply (rename_tac y z)
  1450 apply (drule_tac x = y in spec)
  1451 apply (drule_tac x = "pi/2" in spec, simp) 
  1452 done
  1453 
  1454 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  1455 apply (rule_tac x = x and y = 0 in linorder_cases)
  1456 apply (rule cos_minus [THEN subst])
  1457 apply (rule cos_gt_zero)
  1458 apply (auto intro: cos_gt_zero)
  1459 done
  1460  
  1461 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  1462 apply (auto simp add: order_le_less cos_gt_zero_pi)
  1463 apply (subgoal_tac "x = pi/2", auto) 
  1464 done
  1465 
  1466 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  1467 apply (subst sin_cos_eq)
  1468 apply (rotate_tac 1)
  1469 apply (drule real_sum_of_halves [THEN ssubst])
  1470 apply (auto intro!: cos_gt_zero_pi simp del: sin_cos_eq [symmetric])
  1471 done
  1472 
  1473 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  1474 by (auto simp add: order_le_less sin_gt_zero_pi)
  1475 
  1476 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  1477 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y")
  1478 apply (rule_tac [2] IVT2)
  1479 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos)
  1480 apply (cut_tac x = xa and y = y in linorder_less_linear)
  1481 apply (rule ccontr, auto)
  1482 apply (drule_tac f = cos in Rolle)
  1483 apply (drule_tac [5] f = cos in Rolle)
  1484 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos
  1485             dest!: DERIV_cos [THEN DERIV_unique] 
  1486             simp add: differentiable_def)
  1487 apply (auto dest: sin_gt_zero_pi [OF order_le_less_trans order_less_le_trans])
  1488 done
  1489 
  1490 lemma sin_total:
  1491      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  1492 apply (rule ccontr)
  1493 apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
  1494 apply (erule contrapos_np)
  1495 apply (simp del: minus_sin_cos_eq [symmetric])
  1496 apply (cut_tac y="-y" in cos_total, simp) apply simp 
  1497 apply (erule ex1E)
  1498 apply (rule_tac a = "x - (pi/2)" in ex1I)
  1499 apply (simp (no_asm) add: add_assoc)
  1500 apply (rotate_tac 3)
  1501 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all) 
  1502 done
  1503 
  1504 lemma reals_Archimedean4:
  1505      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  1506 apply (auto dest!: reals_Archimedean3)
  1507 apply (drule_tac x = x in spec, clarify) 
  1508 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  1509  prefer 2 apply (erule LeastI) 
  1510 apply (case_tac "LEAST m::nat. x < real m * y", simp) 
  1511 apply (subgoal_tac "~ x < real nat * y")
  1512  prefer 2 apply (rule not_less_Least, simp, force)  
  1513 done
  1514 
  1515 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic 
  1516    now causes some unwanted re-arrangements of literals!   *)
  1517 lemma cos_zero_lemma:
  1518      "[| 0 \<le> x; cos x = 0 |] ==>  
  1519       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  1520 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  1521 apply (subgoal_tac "0 \<le> x - real n * pi & 
  1522                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  1523 apply (auto simp add: compare_rls) 
  1524   prefer 3 apply (simp add: cos_diff) 
  1525  prefer 2 apply (simp add: real_of_nat_Suc left_distrib) 
  1526 apply (simp add: cos_diff)
  1527 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  1528 apply (rule_tac [2] cos_total, safe)
  1529 apply (drule_tac x = "x - real n * pi" in spec)
  1530 apply (drule_tac x = "pi/2" in spec)
  1531 apply (simp add: cos_diff)
  1532 apply (rule_tac x = "Suc (2 * n)" in exI)
  1533 apply (simp add: real_of_nat_Suc left_distrib, auto)
  1534 done
  1535 
  1536 lemma sin_zero_lemma:
  1537      "[| 0 \<le> x; sin x = 0 |] ==>  
  1538       \<exists>n::nat. even n & x = real n * (pi/2)"
  1539 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  1540  apply (clarify, rule_tac x = "n - 1" in exI)
  1541  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
  1542 apply (rule cos_zero_lemma)
  1543 apply (simp_all add: add_increasing)  
  1544 done
  1545 
  1546 
  1547 lemma cos_zero_iff:
  1548      "(cos x = 0) =  
  1549       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |    
  1550        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  1551 apply (rule iffI)
  1552 apply (cut_tac linorder_linear [of 0 x], safe)
  1553 apply (drule cos_zero_lemma, assumption+)
  1554 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp) 
  1555 apply (force simp add: minus_equation_iff [of x]) 
  1556 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) 
  1557 apply (auto simp add: cos_add)
  1558 done
  1559 
  1560 (* ditto: but to a lesser extent *)
  1561 lemma sin_zero_iff:
  1562      "(sin x = 0) =  
  1563       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |    
  1564        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  1565 apply (rule iffI)
  1566 apply (cut_tac linorder_linear [of 0 x], safe)
  1567 apply (drule sin_zero_lemma, assumption+)
  1568 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  1569 apply (force simp add: minus_equation_iff [of x]) 
  1570 apply (auto simp add: even_mult_two_ex)
  1571 done
  1572 
  1573 
  1574 subsection {* Tangent *}
  1575 
  1576 definition
  1577   tan :: "real => real" where
  1578   "tan x = (sin x)/(cos x)"
  1579 
  1580 lemma tan_zero [simp]: "tan 0 = 0"
  1581 by (simp add: tan_def)
  1582 
  1583 lemma tan_pi [simp]: "tan pi = 0"
  1584 by (simp add: tan_def)
  1585 
  1586 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  1587 by (simp add: tan_def)
  1588 
  1589 lemma tan_minus [simp]: "tan (-x) = - tan x"
  1590 by (simp add: tan_def minus_mult_left)
  1591 
  1592 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  1593 by (simp add: tan_def)
  1594 
  1595 lemma lemma_tan_add1: 
  1596       "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
  1597         ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"
  1598 apply (simp add: tan_def divide_inverse)
  1599 apply (auto simp del: inverse_mult_distrib 
  1600             simp add: inverse_mult_distrib [symmetric] mult_ac)
  1601 apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
  1602 apply (auto simp del: inverse_mult_distrib 
  1603             simp add: mult_assoc left_diff_distrib cos_add)
  1604 done  
  1605 
  1606 lemma add_tan_eq: 
  1607       "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
  1608        ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
  1609 apply (simp add: tan_def)
  1610 apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
  1611 apply (auto simp add: mult_assoc left_distrib)
  1612 apply (simp add: sin_add)
  1613 done
  1614 
  1615 lemma tan_add:
  1616      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]  
  1617       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  1618 apply (simp (no_asm_simp) add: add_tan_eq lemma_tan_add1)
  1619 apply (simp add: tan_def)
  1620 done
  1621 
  1622 lemma tan_double:
  1623      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]  
  1624       ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
  1625 apply (insert tan_add [of x x]) 
  1626 apply (simp add: mult_2 [symmetric])  
  1627 apply (auto simp add: numeral_2_eq_2)
  1628 done
  1629 
  1630 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  1631 by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi) 
  1632 
  1633 lemma tan_less_zero: 
  1634   assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
  1635 proof -
  1636   have "0 < tan (- x)" using prems by (simp only: tan_gt_zero) 
  1637   thus ?thesis by simp
  1638 qed
  1639 
  1640 lemma lemma_DERIV_tan:
  1641      "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
  1642 apply (rule lemma_DERIV_subst)
  1643 apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  1644 apply (auto simp add: divide_inverse numeral_2_eq_2)
  1645 done
  1646 
  1647 lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
  1648 by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
  1649 
  1650 lemma isCont_tan [simp]: "cos x \<noteq> 0 ==> isCont tan x"
  1651 by (rule DERIV_tan [THEN DERIV_isCont])
  1652 
  1653 lemma LIM_cos_div_sin [simp]: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
  1654 apply (subgoal_tac "(\<lambda>x. cos x * inverse (sin x)) -- pi * inverse 2 --> 0*1")
  1655 apply (simp add: divide_inverse [symmetric])
  1656 apply (rule LIM_mult)
  1657 apply (rule_tac [2] inverse_1 [THEN subst])
  1658 apply (rule_tac [2] LIM_inverse)
  1659 apply (simp_all add: divide_inverse [symmetric]) 
  1660 apply (simp_all only: isCont_def [symmetric] cos_pi_half [symmetric] sin_pi_half [symmetric]) 
  1661 apply (blast intro!: DERIV_isCont DERIV_sin DERIV_cos)+
  1662 done
  1663 
  1664 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  1665 apply (cut_tac LIM_cos_div_sin)
  1666 apply (simp only: LIM_def)
  1667 apply (drule_tac x = "inverse y" in spec, safe, force)
  1668 apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  1669 apply (rule_tac x = "(pi/2) - e" in exI)
  1670 apply (simp (no_asm_simp))
  1671 apply (drule_tac x = "(pi/2) - e" in spec)
  1672 apply (auto simp add: tan_def)
  1673 apply (rule inverse_less_iff_less [THEN iffD1])
  1674 apply (auto simp add: divide_inverse)
  1675 apply (rule real_mult_order) 
  1676 apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  1677 apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute) 
  1678 done
  1679 
  1680 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  1681 apply (frule order_le_imp_less_or_eq, safe)
  1682  prefer 2 apply force
  1683 apply (drule lemma_tan_total, safe)
  1684 apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  1685 apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  1686 apply (drule_tac y = xa in order_le_imp_less_or_eq)
  1687 apply (auto dest: cos_gt_zero)
  1688 done
  1689 
  1690 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  1691 apply (cut_tac linorder_linear [of 0 y], safe)
  1692 apply (drule tan_total_pos)
  1693 apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  1694 apply (rule_tac [3] x = "-x" in exI)
  1695 apply (auto intro!: exI)
  1696 done
  1697 
  1698 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  1699 apply (cut_tac y = y in lemma_tan_total1, auto)
  1700 apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  1701 apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  1702 apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  1703 apply (rule_tac [4] Rolle)
  1704 apply (rule_tac [2] Rolle)
  1705 apply (auto intro!: DERIV_tan DERIV_isCont exI 
  1706             simp add: differentiable_def)
  1707 txt{*Now, simulate TRYALL*}
  1708 apply (rule_tac [!] DERIV_tan asm_rl)
  1709 apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  1710 	    simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym]) 
  1711 done
  1712 
  1713 
  1714 subsection {* Inverse Trigonometric Functions *}
  1715 
  1716 definition
  1717   arcsin :: "real => real" where
  1718   "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  1719 
  1720 definition
  1721   arccos :: "real => real" where
  1722   "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  1723 
  1724 definition     
  1725   arctan :: "real => real" where
  1726   "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  1727 
  1728 lemma arcsin:
  1729      "[| -1 \<le> y; y \<le> 1 |]  
  1730       ==> -(pi/2) \<le> arcsin y &  
  1731            arcsin y \<le> pi/2 & sin(arcsin y) = y"
  1732 unfolding arcsin_def by (rule theI' [OF sin_total])
  1733 
  1734 lemma arcsin_pi:
  1735      "[| -1 \<le> y; y \<le> 1 |]  
  1736       ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  1737 apply (drule (1) arcsin)
  1738 apply (force intro: order_trans)
  1739 done
  1740 
  1741 lemma sin_arcsin [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> sin(arcsin y) = y"
  1742 by (blast dest: arcsin)
  1743       
  1744 lemma arcsin_bounded:
  1745      "[| -1 \<le> y; y \<le> 1 |] ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  1746 by (blast dest: arcsin)
  1747 
  1748 lemma arcsin_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> -(pi/2) \<le> arcsin y"
  1749 by (blast dest: arcsin)
  1750 
  1751 lemma arcsin_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcsin y \<le> pi/2"
  1752 by (blast dest: arcsin)
  1753 
  1754 lemma arcsin_lt_bounded:
  1755      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  1756 apply (frule order_less_imp_le)
  1757 apply (frule_tac y = y in order_less_imp_le)
  1758 apply (frule arcsin_bounded)
  1759 apply (safe, simp)
  1760 apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  1761 apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  1762 apply (drule_tac [!] f = sin in arg_cong, auto)
  1763 done
  1764 
  1765 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  1766 apply (unfold arcsin_def)
  1767 apply (rule the1_equality)
  1768 apply (rule sin_total, auto)
  1769 done
  1770 
  1771 lemma arccos:
  1772      "[| -1 \<le> y; y \<le> 1 |]  
  1773       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  1774 unfolding arccos_def by (rule theI' [OF cos_total])
  1775 
  1776 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  1777 by (blast dest: arccos)
  1778       
  1779 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  1780 by (blast dest: arccos)
  1781 
  1782 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  1783 by (blast dest: arccos)
  1784 
  1785 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  1786 by (blast dest: arccos)
  1787 
  1788 lemma arccos_lt_bounded:
  1789      "[| -1 < y; y < 1 |]  
  1790       ==> 0 < arccos y & arccos y < pi"
  1791 apply (frule order_less_imp_le)
  1792 apply (frule_tac y = y in order_less_imp_le)
  1793 apply (frule arccos_bounded, auto)
  1794 apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  1795 apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  1796 apply (drule_tac [!] f = cos in arg_cong, auto)
  1797 done
  1798 
  1799 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  1800 apply (simp add: arccos_def)
  1801 apply (auto intro!: the1_equality cos_total)
  1802 done
  1803 
  1804 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  1805 apply (simp add: arccos_def)
  1806 apply (auto intro!: the1_equality cos_total)
  1807 done
  1808 
  1809 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<twosuperior>)"
  1810 apply (subgoal_tac "x\<twosuperior> \<le> 1")
  1811 apply (rule power2_eq_imp_eq)
  1812 apply (simp add: cos_squared_eq)
  1813 apply (rule cos_ge_zero)
  1814 apply (erule (1) arcsin_lbound)
  1815 apply (erule (1) arcsin_ubound)
  1816 apply simp
  1817 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
  1818 apply (rule power_mono, simp, simp)
  1819 done
  1820 
  1821 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<twosuperior>)"
  1822 apply (subgoal_tac "x\<twosuperior> \<le> 1")
  1823 apply (rule power2_eq_imp_eq)
  1824 apply (simp add: sin_squared_eq)
  1825 apply (rule sin_ge_zero)
  1826 apply (erule (1) arccos_lbound)
  1827 apply (erule (1) arccos_ubound)
  1828 apply simp
  1829 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
  1830 apply (rule power_mono, simp, simp)
  1831 done
  1832 
  1833 lemma arctan [simp]:
  1834      "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  1835 unfolding arctan_def by (rule theI' [OF tan_total])
  1836 
  1837 lemma tan_arctan: "tan(arctan y) = y"
  1838 by auto
  1839 
  1840 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  1841 by (auto simp only: arctan)
  1842 
  1843 lemma arctan_lbound: "- (pi/2) < arctan y"
  1844 by auto
  1845 
  1846 lemma arctan_ubound: "arctan y < pi/2"
  1847 by (auto simp only: arctan)
  1848 
  1849 lemma arctan_tan: 
  1850       "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x"
  1851 apply (unfold arctan_def)
  1852 apply (rule the1_equality)
  1853 apply (rule tan_total, auto)
  1854 done
  1855 
  1856 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  1857 by (insert arctan_tan [of 0], simp)
  1858 
  1859 lemma cos_arctan_not_zero [simp]: "cos(arctan x) \<noteq> 0"
  1860 apply (auto simp add: cos_zero_iff)
  1861 apply (case_tac "n")
  1862 apply (case_tac [3] "n")
  1863 apply (cut_tac [2] y = x in arctan_ubound)
  1864 apply (cut_tac [4] y = x in arctan_lbound) 
  1865 apply (auto simp add: real_of_nat_Suc left_distrib mult_less_0_iff)
  1866 done
  1867 
  1868 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
  1869 apply (rule power_inverse [THEN subst])
  1870 apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
  1871 apply (auto dest: field_power_not_zero
  1872         simp add: power_mult_distrib left_distrib power_divide tan_def 
  1873                   mult_assoc power_inverse [symmetric] 
  1874         simp del: realpow_Suc)
  1875 done
  1876 
  1877 lemma isCont_inverse_function2:
  1878   fixes f g :: "real \<Rightarrow> real" shows
  1879   "\<lbrakk>a < x; x < b;
  1880     \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
  1881     \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
  1882    \<Longrightarrow> isCont g (f x)"
  1883 apply (rule isCont_inverse_function
  1884        [where f=f and d="min (x - a) (b - x)"])
  1885 apply (simp_all add: abs_le_iff)
  1886 done
  1887 
  1888 lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
  1889 apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
  1890 apply (rule isCont_inverse_function2 [where f=sin])
  1891 apply (erule (1) arcsin_lt_bounded [THEN conjunct1])
  1892 apply (erule (1) arcsin_lt_bounded [THEN conjunct2])
  1893 apply (fast intro: arcsin_sin, simp)
  1894 done
  1895 
  1896 lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
  1897 apply (subgoal_tac "isCont arccos (cos (arccos x))", simp)
  1898 apply (rule isCont_inverse_function2 [where f=cos])
  1899 apply (erule (1) arccos_lt_bounded [THEN conjunct1])
  1900 apply (erule (1) arccos_lt_bounded [THEN conjunct2])
  1901 apply (fast intro: arccos_cos, simp)
  1902 done
  1903 
  1904 lemma isCont_arctan: "isCont arctan x"
  1905 apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  1906 apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  1907 apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  1908 apply (erule (1) isCont_inverse_function2 [where f=tan])
  1909 apply (clarify, rule arctan_tan)
  1910 apply (erule (1) order_less_le_trans)
  1911 apply (erule (1) order_le_less_trans)
  1912 apply (clarify, rule isCont_tan)
  1913 apply (rule less_imp_neq [symmetric])
  1914 apply (rule cos_gt_zero_pi)
  1915 apply (erule (1) order_less_le_trans)
  1916 apply (erule (1) order_le_less_trans)
  1917 done
  1918 
  1919 lemma DERIV_arcsin:
  1920   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
  1921 apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  1922 apply (rule lemma_DERIV_subst [OF DERIV_sin])
  1923 apply (simp add: cos_arcsin)
  1924 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
  1925 apply (rule power_strict_mono, simp, simp, simp)
  1926 apply assumption
  1927 apply assumption
  1928 apply simp
  1929 apply (erule (1) isCont_arcsin)
  1930 done
  1931 
  1932 lemma DERIV_arccos:
  1933   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
  1934 apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  1935 apply (rule lemma_DERIV_subst [OF DERIV_cos])
  1936 apply (simp add: sin_arccos)
  1937 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
  1938 apply (rule power_strict_mono, simp, simp, simp)
  1939 apply assumption
  1940 apply assumption
  1941 apply simp
  1942 apply (erule (1) isCont_arccos)
  1943 done
  1944 
  1945 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
  1946 apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  1947 apply (rule lemma_DERIV_subst [OF DERIV_tan])
  1948 apply (rule cos_arctan_not_zero)
  1949 apply (simp add: power_inverse tan_sec [symmetric])
  1950 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
  1951 apply (simp add: add_pos_nonneg)
  1952 apply (simp, simp, simp, rule isCont_arctan)
  1953 done
  1954 
  1955 
  1956 subsection {* More Theorems about Sin and Cos *}
  1957 
  1958 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  1959 proof -
  1960   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  1961   have nonneg: "0 \<le> ?c"
  1962     by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  1963   have "0 = cos (pi / 4 + pi / 4)"
  1964     by simp
  1965   also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"
  1966     by (simp only: cos_add power2_eq_square)
  1967   also have "\<dots> = 2 * ?c\<twosuperior> - 1"
  1968     by (simp add: sin_squared_eq)
  1969   finally have "?c\<twosuperior> = (sqrt 2 / 2)\<twosuperior>"
  1970     by (simp add: power_divide)
  1971   thus ?thesis
  1972     using nonneg by (rule power2_eq_imp_eq) simp
  1973 qed
  1974 
  1975 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  1976 proof -
  1977   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  1978   have pos_c: "0 < ?c"
  1979     by (rule cos_gt_zero, simp, simp)
  1980   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  1981     by simp
  1982   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  1983     by (simp only: cos_add sin_add)
  1984   also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
  1985     by (simp add: ring_simps power2_eq_square)
  1986   finally have "?c\<twosuperior> = (sqrt 3 / 2)\<twosuperior>"
  1987     using pos_c by (simp add: sin_squared_eq power_divide)
  1988   thus ?thesis
  1989     using pos_c [THEN order_less_imp_le]
  1990     by (rule power2_eq_imp_eq) simp
  1991 qed
  1992 
  1993 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  1994 proof -
  1995   have "sin (pi / 4) = cos (pi / 2 - pi / 4)" by (rule sin_cos_eq)
  1996   also have "pi / 2 - pi / 4 = pi / 4" by simp
  1997   also have "cos (pi / 4) = sqrt 2 / 2" by (rule cos_45)
  1998   finally show ?thesis .
  1999 qed
  2000 
  2001 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  2002 proof -
  2003   have "sin (pi / 3) = cos (pi / 2 - pi / 3)" by (rule sin_cos_eq)
  2004   also have "pi / 2 - pi / 3 = pi / 6" by simp
  2005   also have "cos (pi / 6) = sqrt 3 / 2" by (rule cos_30)
  2006   finally show ?thesis .
  2007 qed
  2008 
  2009 lemma cos_60: "cos (pi / 3) = 1 / 2"
  2010 apply (rule power2_eq_imp_eq)
  2011 apply (simp add: cos_squared_eq sin_60 power_divide)
  2012 apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  2013 done
  2014 
  2015 lemma sin_30: "sin (pi / 6) = 1 / 2"
  2016 proof -
  2017   have "sin (pi / 6) = cos (pi / 2 - pi / 6)" by (rule sin_cos_eq)
  2018   also have "pi / 2 - pi / 6 = pi / 3" by simp
  2019   also have "cos (pi / 3) = 1 / 2" by (rule cos_60)
  2020   finally show ?thesis .
  2021 qed
  2022 
  2023 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  2024 unfolding tan_def by (simp add: sin_30 cos_30)
  2025 
  2026 lemma tan_45: "tan (pi / 4) = 1"
  2027 unfolding tan_def by (simp add: sin_45 cos_45)
  2028 
  2029 lemma tan_60: "tan (pi / 3) = sqrt 3"
  2030 unfolding tan_def by (simp add: sin_60 cos_60)
  2031 
  2032 text{*NEEDED??*}
  2033 lemma [simp]:
  2034      "sin (x + 1 / 2 * real (Suc m) * pi) =  
  2035       cos (x + 1 / 2 * real  (m) * pi)"
  2036 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
  2037 
  2038 text{*NEEDED??*}
  2039 lemma [simp]:
  2040      "sin (x + real (Suc m) * pi / 2) =  
  2041       cos (x + real (m) * pi / 2)"
  2042 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
  2043 
  2044 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
  2045 apply (rule lemma_DERIV_subst)
  2046 apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
  2047 apply (best intro!: DERIV_intros intro: DERIV_chain2)+
  2048 apply (simp (no_asm))
  2049 done
  2050 
  2051 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  2052 proof -
  2053   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  2054     by (auto simp add: right_distrib sin_add left_distrib mult_ac)
  2055   thus ?thesis
  2056     by (simp add: real_of_nat_Suc left_distrib add_divide_distrib 
  2057                   mult_commute [of pi])
  2058 qed
  2059 
  2060 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  2061 by (simp add: cos_double mult_assoc power_add [symmetric] numeral_2_eq_2)
  2062 
  2063 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  2064 apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  2065 apply (subst cos_add, simp)
  2066 done
  2067 
  2068 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  2069 by (auto simp add: mult_assoc)
  2070 
  2071 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  2072 apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  2073 apply (subst sin_add, simp)
  2074 done
  2075 
  2076 (*NEEDED??*)
  2077 lemma [simp]:
  2078      "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
  2079 apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
  2080 done
  2081 
  2082 (*NEEDED??*)
  2083 lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
  2084 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
  2085 
  2086 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  2087 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
  2088 
  2089 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
  2090 apply (rule lemma_DERIV_subst)
  2091 apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
  2092 apply (best intro!: DERIV_intros intro: DERIV_chain2)+
  2093 apply (simp (no_asm))
  2094 done
  2095 
  2096 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  2097 by (auto simp add: sin_zero_iff even_mult_two_ex)
  2098 
  2099 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  2100 by (cut_tac x = x in sin_cos_squared_add3, auto)
  2101 
  2102 
  2103 subsection {* Existence of Polar Coordinates *}
  2104 
  2105 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1"
  2106 apply (rule power2_le_imp_le [OF _ zero_le_one])
  2107 apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero)
  2108 done
  2109 
  2110 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  2111 by (simp add: abs_le_iff)
  2112 
  2113 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<twosuperior>)"
  2114 by (simp add: sin_arccos abs_le_iff)
  2115 
  2116 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  2117 
  2118 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  2119 
  2120 lemma polar_ex1:
  2121      "0 < y ==> \<exists>r a. x = r * cos a & y = r * sin a"
  2122 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
  2123 apply (rule_tac x = "arccos (x / sqrt (x\<twosuperior> + y\<twosuperior>))" in exI)
  2124 apply (simp add: cos_arccos_lemma1)
  2125 apply (simp add: sin_arccos_lemma1)
  2126 apply (simp add: power_divide)
  2127 apply (simp add: real_sqrt_mult [symmetric])
  2128 apply (simp add: right_diff_distrib)
  2129 done
  2130 
  2131 lemma polar_ex2:
  2132      "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
  2133 apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify)
  2134 apply (rule_tac x = r in exI)
  2135 apply (rule_tac x = "-a" in exI, simp)
  2136 done
  2137 
  2138 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  2139 apply (rule_tac x=0 and y=y in linorder_cases)
  2140 apply (erule polar_ex1)
  2141 apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
  2142 apply (erule polar_ex2)
  2143 done
  2144 
  2145 end