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
```