src/HOL/Transcendental.thy
author huffman
Wed, 24 Dec 2008 08:06:27 -0800
changeset 29165 562f95f06244
parent 29164 0d49c5b55046
child 29166 c23b2d108612
permissions -rw-r--r--
cleaned up some proofs; removed redundant simp rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     1
(*  Title       : Transcendental.thy
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     3
    Copyright   : 1998,1999 University of Cambridge
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents: 12196
diff changeset
     4
                  1999,2001 University of Edinburgh
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     6
*)
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     7
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     8
header{*Power Series, Transcendental Functions etc.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    10
theory Transcendental
25600
73431bd8c4c4 joined EvenOdd theory with Parity
haftmann
parents: 25153
diff changeset
    11
imports Fact Series Deriv NthRoot
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    12
begin
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    13
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
    14
subsection {* Properties of Power Series *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    15
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    16
lemma lemma_realpow_diff:
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    17
  fixes y :: "'a::recpower"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    18
  shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    19
proof -
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    20
  assume "p \<le> n"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    21
  hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    22
  thus ?thesis by (simp add: power_Suc power_commutes)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    23
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    24
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    25
lemma lemma_realpow_diff_sumr:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    26
  fixes y :: "'a::{recpower,comm_semiring_0}" shows
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    27
     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    28
      y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
    29
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
    30
         del: setsum_op_ivl_Suc cong: strong_setsum_cong)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    31
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    32
lemma lemma_realpow_diff_sumr2:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    33
  fixes y :: "'a::{recpower,comm_ring}" shows
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    34
     "x ^ (Suc n) - y ^ (Suc n) =  
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    35
      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
25153
af3c7e99fed0 tuned proof
haftmann
parents: 25062
diff changeset
    36
apply (induct n, simp add: power_Suc)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    37
apply (simp add: power_Suc del: setsum_op_ivl_Suc)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15546
diff changeset
    38
apply (subst setsum_op_ivl_Suc)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    39
apply (subst lemma_realpow_diff_sumr)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    40
apply (simp add: right_distrib del: setsum_op_ivl_Suc)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    41
apply (subst mult_left_commute [where a="x - y"])
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    42
apply (erule subst)
23477
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23441
diff changeset
    43
apply (simp add: power_Suc ring_simps)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    44
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    45
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    46
lemma lemma_realpow_rev_sumr:
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
    47
     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    48
      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    49
apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    50
apply (rule inj_onI, simp)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    51
apply auto
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    52
apply (rule_tac x="n - x" in image_eqI, simp, simp)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    53
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    54
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    55
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    56
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    57
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    58
lemma powser_insidea:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    59
  fixes x z :: "'a::{real_normed_field,banach,recpower}"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    60
  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    61
  assumes 2: "norm z < norm x"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    62
  shows "summable (\<lambda>n. norm (f n * z ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    63
proof -
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    64
  from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    65
  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    66
    by (rule summable_LIMSEQ_zero)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    67
  hence "convergent (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    68
    by (rule convergentI)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    69
  hence "Cauchy (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    70
    by (simp add: Cauchy_convergent_iff)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    71
  hence "Bseq (\<lambda>n. f n * x ^ n)"
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    72
    by (rule Cauchy_Bseq)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    73
  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    74
    by (simp add: Bseq_def, safe)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    75
  have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    76
                   K * norm (z ^ n) * inverse (norm (x ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    77
  proof (intro exI allI impI)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    78
    fix n::nat assume "0 \<le> n"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    79
    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    80
          norm (f n * x ^ n) * norm (z ^ n)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    81
      by (simp add: norm_mult abs_mult)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    82
    also have "\<dots> \<le> K * norm (z ^ n)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    83
      by (simp only: mult_right_mono 4 norm_ge_zero)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    84
    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    85
      by (simp add: x_neq_0)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    86
    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    87
      by (simp only: mult_assoc)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    88
    finally show "norm (norm (f n * z ^ n)) \<le>
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    89
                  K * norm (z ^ n) * inverse (norm (x ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    90
      by (simp add: mult_le_cancel_right x_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    91
  qed
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    92
  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    93
  proof -
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    94
    from 2 have "norm (norm (z * inverse x)) < 1"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    95
      using x_neq_0
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    96
      by (simp add: nonzero_norm_divide divide_inverse [symmetric])
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    97
    hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
    98
      by (rule summable_geometric)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    99
    hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   100
      by (rule summable_mult)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   101
    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   102
      using x_neq_0
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   103
      by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   104
                    power_inverse norm_power mult_assoc)
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   105
  qed
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   106
  ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   107
    by (rule summable_comparison_test)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   108
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   109
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   110
lemma powser_inside:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   111
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   112
     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   113
      ==> summable (%n. f(n) * (z ^ n))"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   114
by (rule powser_insidea [THEN summable_norm_cancel])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   115
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   116
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   117
subsection {* Term-by-Term Differentiability of Power Series *}
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   118
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   119
definition
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   120
  diffs :: "(nat => 'a::ring_1) => nat => 'a" where
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   121
  "diffs c = (%n. of_nat (Suc n) * c(Suc n))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   122
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   123
text{*Lemma about distributing negation over it*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   124
lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   125
by (simp add: diffs_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   126
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   127
lemma sums_Suc_imp:
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   128
  assumes f: "f 0 = 0"
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   129
  shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   130
unfolding sums_def
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   131
apply (rule LIMSEQ_imp_Suc)
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   132
apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   133
apply (simp only: setsum_shift_bounds_Suc_ivl)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   134
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   135
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   136
lemma diffs_equiv:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   137
     "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   138
      (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums  
15546
5188ce7316b7 suminf -> \<Sum>
nipkow
parents: 15544
diff changeset
   139
         (\<Sum>n. (diffs c)(n) * (x ^ n))"
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   140
unfolding diffs_def
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   141
apply (drule summable_sums)
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   142
apply (rule sums_Suc_imp, simp_all)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   143
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   144
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   145
lemma lemma_termdiff1:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   146
  fixes z :: "'a :: {recpower,comm_ring}" shows
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   147
  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   148
   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
16641
fce796ad9c2b Simplified some proofs (thanks to strong_setsum_cong).
berghofe
parents: 15561
diff changeset
   149
by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
fce796ad9c2b Simplified some proofs (thanks to strong_setsum_cong).
berghofe
parents: 15561
diff changeset
   150
  cong: strong_setsum_cong)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   151
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   152
lemma sumr_diff_mult_const2:
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   153
  "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   154
by (simp add: setsum_subtractf)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   155
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   156
lemma lemma_termdiff2:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   157
  fixes h :: "'a :: {recpower,field}"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   158
  assumes h: "h \<noteq> 0" shows
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   159
  "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   160
   h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   161
        (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   162
apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   163
apply (simp add: right_diff_distrib diff_divide_distrib h)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   164
apply (simp add: mult_assoc [symmetric])
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   165
apply (cases "n", simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   166
apply (simp add: lemma_realpow_diff_sumr2 h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   167
                 right_diff_distrib [symmetric] mult_assoc
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   168
            del: realpow_Suc setsum_op_ivl_Suc of_nat_Suc)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   169
apply (subst lemma_realpow_rev_sumr)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   170
apply (subst sumr_diff_mult_const2)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   171
apply simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   172
apply (simp only: lemma_termdiff1 setsum_right_distrib)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   173
apply (rule setsum_cong [OF refl])
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15536
diff changeset
   174
apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   175
apply (clarify)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   176
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   177
            del: setsum_op_ivl_Suc realpow_Suc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   178
apply (subst mult_assoc [symmetric], subst power_add [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   179
apply (simp add: mult_ac)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   180
done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   181
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   182
lemma real_setsum_nat_ivl_bounded2:
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   183
  fixes K :: "'a::ordered_semidom"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   184
  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   185
  assumes K: "0 \<le> K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   186
  shows "setsum f {0..<n-k} \<le> of_nat n * K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   187
apply (rule order_trans [OF setsum_mono])
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   188
apply (rule f, simp)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   189
apply (simp add: mult_right_mono K)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   190
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   191
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   192
lemma lemma_termdiff3:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   193
  fixes h z :: "'a::{real_normed_field,recpower}"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   194
  assumes 1: "h \<noteq> 0"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   195
  assumes 2: "norm z \<le> K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   196
  assumes 3: "norm (z + h) \<le> K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   197
  shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   198
          \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   199
proof -
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   200
  have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   201
        norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   202
          (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   203
    apply (subst lemma_termdiff2 [OF 1])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   204
    apply (subst norm_mult)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   205
    apply (rule mult_commute)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   206
    done
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   207
  also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   208
  proof (rule mult_right_mono [OF _ norm_ge_zero])
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   209
    from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   210
    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   211
      apply (erule subst)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   212
      apply (simp only: norm_mult norm_power power_add)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   213
      apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   214
      done
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   215
    show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   216
              (z + h) ^ q * z ^ (n - 2 - q))
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   217
          \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   218
      apply (intro
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   219
         order_trans [OF norm_setsum]
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   220
         real_setsum_nat_ivl_bounded2
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   221
         mult_nonneg_nonneg
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   222
         zero_le_imp_of_nat
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   223
         zero_le_power K)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   224
      apply (rule le_Kn, simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   225
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   226
  qed
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   227
  also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   228
    by (simp only: mult_assoc)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   229
  finally show ?thesis .
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   230
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   231
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   232
lemma lemma_termdiff4:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   233
  fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   234
              'b::real_normed_vector"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   235
  assumes k: "0 < (k::real)"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   236
  assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   237
  shows "f -- 0 --> 0"
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   238
unfolding LIM_def diff_0_right
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   239
proof (safe)
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   240
  let ?h = "of_real (k / 2)::'a"
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   241
  have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   242
  hence "norm (f ?h) \<le> K * norm ?h" by (rule le)
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   243
  hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero])
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   244
  hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff)
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   245
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   246
  fix r::real assume r: "0 < r"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   247
  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   248
  proof (cases)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   249
    assume "K = 0"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   250
    with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   251
      by simp
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   252
    thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" ..
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   253
  next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   254
    assume K_neq_zero: "K \<noteq> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   255
    with zero_le_K have K: "0 < K" by simp
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   256
    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   257
    proof (rule exI, safe)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   258
      from k r K show "0 < min k (r * inverse K / 2)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   259
        by (simp add: mult_pos_pos positive_imp_inverse_positive)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   260
    next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   261
      fix x::'a
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   262
      assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   263
      from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   264
        by simp_all
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   265
      from x1 x3 le have "norm (f x) \<le> K * norm x" by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   266
      also from x4 K have "K * norm x < K * (r * inverse K / 2)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   267
        by (rule mult_strict_left_mono)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   268
      also have "\<dots> = r / 2"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   269
        using K_neq_zero by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   270
      also have "r / 2 < r"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   271
        using r by simp
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   272
      finally show "norm (f x) < r" .
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   273
    qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   274
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   275
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   276
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   277
lemma lemma_termdiff5:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   278
  fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   279
              nat \<Rightarrow> 'b::banach"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   280
  assumes k: "0 < (k::real)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   281
  assumes f: "summable f"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   282
  assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   283
  shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   284
proof (rule lemma_termdiff4 [OF k])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   285
  fix h::'a assume "h \<noteq> 0" and "norm h < k"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   286
  hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   287
    by (simp add: le)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   288
  hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   289
    by simp
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   290
  moreover from f have B: "summable (\<lambda>n. f n * norm h)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   291
    by (rule summable_mult2)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   292
  ultimately have C: "summable (\<lambda>n. norm (g h n))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   293
    by (rule summable_comparison_test)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   294
  hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   295
    by (rule summable_norm)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   296
  also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   297
    by (rule summable_le)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   298
  also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   299
    by (rule suminf_mult2 [symmetric])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   300
  finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   301
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   302
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   303
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   304
text{* FIXME: Long proofs*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   305
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   306
lemma termdiffs_aux:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   307
  fixes x :: "'a::{recpower,real_normed_field,banach}"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   308
  assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   309
  assumes 2: "norm x < norm K"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   310
  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   311
             - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   312
proof -
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   313
  from dense [OF 2]
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   314
  obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   315
  from norm_ge_zero r1 have r: "0 < r"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   316
    by (rule order_le_less_trans)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   317
  hence r_neq_0: "r \<noteq> 0" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   318
  show ?thesis
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   319
  proof (rule lemma_termdiff5)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   320
    show "0 < r - norm x" using r1 by simp
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   321
  next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   322
    from r r2 have "norm (of_real r::'a) < norm K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   323
      by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   324
    with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   325
      by (rule powser_insidea)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   326
    hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   327
      using r
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   328
      by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   329
    hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   330
      by (rule diffs_equiv [THEN sums_summable])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   331
    also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   332
      = (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   333
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   334
      apply (simp add: diffs_def)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   335
      apply (case_tac n, simp_all add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   336
      done
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   337
    finally have "summable 
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   338
      (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   339
      by (rule diffs_equiv [THEN sums_summable])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   340
    also have
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   341
      "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   342
           r ^ (n - Suc 0)) =
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   343
       (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   344
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   345
      apply (case_tac "n", simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   346
      apply (case_tac "nat", simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   347
      apply (simp add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   348
      done
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   349
    finally show
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   350
      "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   351
  next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   352
    fix h::'a and n::nat
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   353
    assume h: "h \<noteq> 0"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   354
    assume "norm h < r - norm x"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   355
    hence "norm x + norm h < r" by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   356
    with norm_triangle_ineq have xh: "norm (x + h) < r"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   357
      by (rule order_le_less_trans)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   358
    show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   359
          \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   360
      apply (simp only: norm_mult mult_assoc)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   361
      apply (rule mult_left_mono [OF _ norm_ge_zero])
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   362
      apply (simp (no_asm) add: mult_assoc [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   363
      apply (rule lemma_termdiff3)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   364
      apply (rule h)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   365
      apply (rule r1 [THEN order_less_imp_le])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   366
      apply (rule xh [THEN order_less_imp_le])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   367
      done
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   368
  qed
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   369
qed
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   370
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   371
lemma termdiffs:
23112
2bc882fbe51c remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents: 23097
diff changeset
   372
  fixes K x :: "'a::{recpower,real_normed_field,banach}"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   373
  assumes 1: "summable (\<lambda>n. c n * K ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   374
  assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   375
  assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   376
  assumes 4: "norm x < norm K"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   377
  shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   378
unfolding deriv_def
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   379
proof (rule LIM_zero_cancel)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   380
  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   381
            - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   382
  proof (rule LIM_equal2)
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   383
    show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   384
  next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   385
    fix h :: 'a
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   386
    assume "h \<noteq> 0"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   387
    assume "norm (h - 0) < norm K - norm x"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   388
    hence "norm x + norm h < norm K" by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   389
    hence 5: "norm (x + h) < norm K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   390
      by (rule norm_triangle_ineq [THEN order_le_less_trans])
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   391
    have A: "summable (\<lambda>n. c n * x ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   392
      by (rule powser_inside [OF 1 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   393
    have B: "summable (\<lambda>n. c n * (x + h) ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   394
      by (rule powser_inside [OF 1 5])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   395
    have C: "summable (\<lambda>n. diffs c n * x ^ n)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   396
      by (rule powser_inside [OF 2 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   397
    show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   398
             - (\<Sum>n. diffs c n * x ^ n) = 
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   399
          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   400
      apply (subst sums_unique [OF diffs_equiv [OF C]])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   401
      apply (subst suminf_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   402
      apply (subst suminf_divide [symmetric])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   403
      apply (rule summable_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   404
      apply (subst suminf_diff)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   405
      apply (rule summable_divide)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   406
      apply (rule summable_diff [OF B A])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   407
      apply (rule sums_summable [OF diffs_equiv [OF C]])
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   408
      apply (rule arg_cong [where f="suminf"], rule ext)
23477
f4b83f03cac9 tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents: 23441
diff changeset
   409
      apply (simp add: ring_simps)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   410
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   411
  next
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   412
    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   413
               of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   414
        by (rule termdiffs_aux [OF 3 4])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   415
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   416
qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   417
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   418
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   419
subsection {* Exponential Function *}
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   420
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   421
definition
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   422
  exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   423
  "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   424
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   425
lemma summable_exp_generic:
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   426
  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   427
  defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   428
  shows "summable S"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   429
proof -
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   430
  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   431
    unfolding S_def by (simp add: power_Suc del: mult_Suc)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   432
  obtain r :: real where r0: "0 < r" and r1: "r < 1"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   433
    using dense [OF zero_less_one] by fast
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   434
  obtain N :: nat where N: "norm x < real N * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   435
    using reals_Archimedean3 [OF r0] by fast
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   436
  from r1 show ?thesis
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   437
  proof (rule ratio_test [rule_format])
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   438
    fix n :: nat
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   439
    assume n: "N \<le> n"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   440
    have "norm x \<le> real N * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   441
      using N by (rule order_less_imp_le)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   442
    also have "real N * r \<le> real (Suc n) * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   443
      using r0 n by (simp add: mult_right_mono)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   444
    finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   445
      using norm_ge_zero by (rule mult_right_mono)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   446
    hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   447
      by (rule order_trans [OF norm_mult_ineq])
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   448
    hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   449
      by (simp add: pos_divide_le_eq mult_ac)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   450
    thus "norm (S (Suc n)) \<le> r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   451
      by (simp add: S_Suc norm_scaleR inverse_eq_divide)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   452
  qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   453
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   454
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   455
lemma summable_norm_exp:
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   456
  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   457
  shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   458
proof (rule summable_norm_comparison_test [OF exI, rule_format])
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   459
  show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   460
    by (rule summable_exp_generic)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   461
next
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   462
  fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   463
    by (simp add: norm_scaleR norm_power_ineq)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   464
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   465
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   466
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   467
by (insert summable_exp_generic [where x=x], simp)
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   468
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   469
lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   470
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   471
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   472
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   473
subsection {* Formal Derivatives of Exp, Sin, and Cos Series *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   474
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   475
lemma exp_fdiffs: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   476
      "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
23431
25ca91279a9b change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents: 23413
diff changeset
   477
by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   478
         del: mult_Suc of_nat_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   479
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   480
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   481
by (simp add: diffs_def)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   482
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   483
lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   484
by (auto intro!: ext simp add: exp_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   485
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   486
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   487
apply (simp add: exp_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   488
apply (subst lemma_exp_ext)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   489
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)")
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   490
apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   491
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   492
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   493
apply (simp del: of_real_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   494
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   495
23045
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   496
lemma isCont_exp [simp]: "isCont exp x"
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   497
by (rule DERIV_exp [THEN DERIV_isCont])
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   498
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   499
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   500
subsection {* Properties of the Exponential Function *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   501
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   502
lemma powser_zero:
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   503
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   504
  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   505
proof -
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   506
  have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   507
    by (rule sums_unique [OF series_zero], simp add: power_0_left)
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   508
  thus ?thesis by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   509
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   510
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   511
lemma exp_zero [simp]: "exp 0 = 1"
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   512
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   513
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   514
lemma setsum_cl_ivl_Suc2:
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   515
  "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
28069
ba4de3022862 moved lemma into SetInterval where it belongs
nipkow
parents: 27483
diff changeset
   516
by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   517
         del: setsum_cl_ivl_Suc)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   518
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   519
lemma exp_series_add:
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   520
  fixes x y :: "'a::{real_field,recpower}"
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   521
  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   522
  shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   523
proof (induct n)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   524
  case 0
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   525
  show ?case
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   526
    unfolding S_def by simp
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   527
next
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   528
  case (Suc n)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   529
  have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   530
    unfolding S_def by (simp add: power_Suc del: mult_Suc)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   531
  hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   532
    by simp
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   533
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   534
  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   535
    by (simp only: times_S)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   536
  also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   537
    by (simp only: Suc)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   538
  also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   539
                + y * (\<Sum>i=0..n. S x i * S y (n-i))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   540
    by (rule left_distrib)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   541
  also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   542
                + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   543
    by (simp only: setsum_right_distrib mult_ac)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   544
  also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   545
                + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   546
    by (simp add: times_S Suc_diff_le)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   547
  also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   548
             (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   549
    by (subst setsum_cl_ivl_Suc2, simp)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   550
  also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   551
             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   552
    by (subst setsum_cl_ivl_Suc, simp)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   553
  also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   554
             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   555
             (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   556
    by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   557
              real_of_nat_add [symmetric], simp)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
   558
  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
23127
56ee8105c002 simplify names of locale interpretations
huffman
parents: 23115
diff changeset
   559
    by (simp only: scaleR_right.setsum)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   560
  finally show
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   561
    "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   562
    by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   563
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   564
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   565
lemma exp_add: "exp (x + y) = exp x * exp y"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   566
unfolding exp_def
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   567
by (simp only: Cauchy_product summable_norm_exp exp_series_add)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   568
23241
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   569
lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   570
unfolding exp_def
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   571
apply (subst of_real.suminf)
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   572
apply (rule summable_exp_generic)
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   573
apply (simp add: scaleR_conv_of_real)
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   574
done
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
   575
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   576
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
22998
97e1f9c2cc46 avoid using redundant lemmas from RealDef.thy
huffman
parents: 22978
diff changeset
   577
apply (drule order_le_imp_less_or_eq, auto)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   578
apply (simp add: exp_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   579
apply (rule real_le_trans)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   580
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
25875
536dfdc25e0a added simp attributes/ proofs fixed
nipkow
parents: 25600
diff changeset
   581
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   582
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   583
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   584
lemma exp_gt_one [simp]: "0 < (x::real) ==> 1 < exp x"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   585
apply (rule order_less_le_trans)
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   586
apply (rule_tac [2] exp_ge_add_one_self_aux, auto)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   587
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   588
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   589
lemma DERIV_exp_add_const: "DERIV (%x. exp (x + y)) x :> exp(x + y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   590
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   591
  have "DERIV (exp \<circ> (\<lambda>x. x + y)) x :> exp (x + y) * (1+0)"
23069
cdfff0241c12 rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents: 23066
diff changeset
   592
    by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_ident DERIV_const) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   593
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   594
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   595
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   596
lemma DERIV_exp_minus [simp]: "DERIV (%x. exp (-x)) x :> - exp(-x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   597
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   598
  have "DERIV (exp \<circ> uminus) x :> exp (- x) * - 1"
23069
cdfff0241c12 rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents: 23066
diff changeset
   599
    by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_ident)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   600
  thus ?thesis by (simp add: o_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   601
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   602
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   603
lemma DERIV_exp_exp_zero [simp]: "DERIV (%x. exp (x + y) * exp (- x)) x :> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   604
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   605
  have "DERIV (\<lambda>x. exp (x + y) * exp (- x)) x
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   606
       :> exp (x + y) * exp (- x) + - exp (- x) * exp (x + y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   607
    by (fast intro: DERIV_exp_add_const DERIV_exp_minus DERIV_mult) 
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   608
  thus ?thesis by (simp add: mult_commute)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   609
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   610
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   611
lemma exp_add_mult_minus [simp]: "exp(x + y)*exp(-x) = exp(y::real)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   612
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   613
  have "\<forall>x. DERIV (%x. exp (x + y) * exp (- x)) x :> 0" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   614
  hence "exp (x + y) * exp (- x) = exp (0 + y) * exp (- 0)" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   615
    by (rule DERIV_isconst_all) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   616
  thus ?thesis by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   617
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   618
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   619
lemma exp_mult_minus [simp]: "exp x * exp(-x) = 1"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   620
by (simp add: exp_add [symmetric])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   621
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   622
lemma exp_mult_minus2 [simp]: "exp(-x)*exp(x) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   623
by (simp add: mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   624
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   625
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   626
lemma exp_minus: "exp(-x) = inverse(exp(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   627
by (auto intro: inverse_unique [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   628
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   629
text{*Proof: because every exponential can be seen as a square.*}
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   630
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   631
apply (rule_tac t = x in real_sum_of_halves [THEN subst])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   632
apply (subst exp_add, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   633
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   634
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   635
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   636
apply (cut_tac x = x in exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   637
apply (auto simp del: exp_mult_minus2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   638
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   639
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   640
lemma exp_gt_zero [simp]: "0 < exp (x::real)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   641
by (simp add: order_less_le)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   642
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   643
lemma inv_exp_gt_zero: "0 < inverse(exp x::real)"
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   644
by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   645
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   646
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   647
by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   648
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   649
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15241
diff changeset
   650
apply (induct "n")
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   651
apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   652
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   653
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   654
lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   655
apply (simp add: diff_minus divide_inverse)
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   656
apply (simp add: exp_add exp_minus)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   657
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   658
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   659
lemma exp_less_mono:
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   660
  fixes x y :: real
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   661
  assumes "x < y" shows "exp x < exp y"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   662
proof -
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   663
  from `x < y` have "0 < y - x" by simp
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   664
  hence "1 < exp (y - x)" by (rule exp_gt_one)
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   665
  hence "1 < exp y / exp x" by (simp only: exp_diff)
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   666
  thus "exp x < exp y" by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   667
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   668
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   669
lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y"
15228
4d332d10fa3d revised simprules for division
paulson
parents: 15140
diff changeset
   670
apply (simp add: linorder_not_le [symmetric]) 
4d332d10fa3d revised simprules for division
paulson
parents: 15140
diff changeset
   671
apply (auto simp add: order_le_less exp_less_mono) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   672
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   673
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   674
lemma exp_less_cancel_iff [iff]: "(exp(x::real) < exp(y)) = (x < y)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   675
by (auto intro: exp_less_mono exp_less_cancel)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   676
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   677
lemma exp_le_cancel_iff [iff]: "(exp(x::real) \<le> exp(y)) = (x \<le> y)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   678
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   679
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   680
lemma exp_inj_iff [iff]: "(exp (x::real) = exp y) = (x = y)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   681
by (simp add: order_eq_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   682
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   683
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   684
apply (rule IVT)
23045
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   685
apply (auto intro: isCont_exp simp add: le_diff_eq)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   686
apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)") 
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
   687
apply simp
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   688
apply (rule exp_ge_add_one_self_aux, simp)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   689
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   690
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   691
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   692
apply (rule_tac x = 1 and y = y in linorder_cases)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   693
apply (drule order_less_imp_le [THEN lemma_exp_total])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   694
apply (rule_tac [2] x = 0 in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   695
apply (frule_tac [3] real_inverse_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   696
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   697
apply (rule_tac x = "-x" in exI)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   698
apply (simp add: exp_minus)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   699
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   700
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   701
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   702
subsection {* Natural Logarithm *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   703
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   704
definition
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   705
  ln :: "real => real" where
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   706
  "ln x = (THE u. exp u = x)"
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   707
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   708
lemma ln_exp [simp]: "ln (exp x) = x"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   709
by (simp add: ln_def)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   710
22654
c2b6b5a9e136 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents: 22653
diff changeset
   711
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
c2b6b5a9e136 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents: 22653
diff changeset
   712
by (auto dest: exp_total)
c2b6b5a9e136 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents: 22653
diff changeset
   713
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   714
lemma exp_ln_iff [simp]: "(exp (ln x) = x) = (0 < x)"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   715
apply (auto dest: exp_total)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   716
apply (erule subst, simp) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   717
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   718
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   719
lemma ln_mult: "[| 0 < x; 0 < y |] ==> ln(x * y) = ln(x) + ln(y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   720
apply (rule exp_inj_iff [THEN iffD1])
22654
c2b6b5a9e136 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents: 22653
diff changeset
   721
apply (simp add: exp_add exp_ln mult_pos_pos)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   722
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   723
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   724
lemma ln_inj_iff[simp]: "[| 0 < x; 0 < y |] ==> (ln x = ln y) = (x = y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   725
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   726
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   727
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   728
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   729
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   730
lemma ln_one[simp]: "ln 1 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   731
by (rule exp_inj_iff [THEN iffD1], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   732
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   733
lemma ln_inverse: "0 < x ==> ln(inverse x) = - ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   734
apply (rule_tac a1 = "ln x" in add_left_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   735
apply (auto simp add: positive_imp_inverse_positive ln_mult [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   736
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   737
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   738
lemma ln_div: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   739
    "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   740
apply (simp add: divide_inverse)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   741
apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   742
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   743
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   744
lemma ln_less_cancel_iff[simp]: "[| 0 < x; 0 < y|] ==> (ln x < ln y) = (x < y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   745
apply (simp only: exp_ln_iff [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   746
apply (erule subst)+
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   747
apply simp 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   748
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   749
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   750
lemma ln_le_cancel_iff[simp]: "[| 0 < x; 0 < y|] ==> (ln x \<le> ln y) = (x \<le> y)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   751
by (auto simp add: linorder_not_less [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   752
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   753
lemma ln_realpow: "0 < x ==> ln(x ^ n) = real n * ln(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   754
by (auto dest!: exp_total simp add: exp_real_of_nat_mult [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   755
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   756
lemma ln_add_one_self_le_self [simp]: "0 \<le> x ==> ln(1 + x) \<le> x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   757
apply (rule ln_exp [THEN subst])
17014
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   758
apply (rule ln_le_cancel_iff [THEN iffD2]) 
ad5ceb90877d renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents: 16924
diff changeset
   759
apply (auto simp add: exp_ge_add_one_self_aux)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   760
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   761
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   762
lemma ln_less_self [simp]: "0 < x ==> ln x < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   763
apply (rule order_less_le_trans)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   764
apply (rule_tac [2] ln_add_one_self_le_self)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   765
apply (rule ln_less_cancel_iff [THEN iffD2], auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   766
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   767
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   768
lemma ln_ge_zero [simp]:
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   769
  assumes x: "1 \<le> x" shows "0 \<le> ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   770
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   771
  have "0 < x" using x by arith
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   772
  hence "exp 0 \<le> exp (ln x)"
22915
bb8a928a6bfa fix proofs
huffman
parents: 22722
diff changeset
   773
    by (simp add: x)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   774
  thus ?thesis by (simp only: exp_le_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   775
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   776
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   777
lemma ln_ge_zero_imp_ge_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   778
  assumes ln: "0 \<le> ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   779
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   780
  shows "1 \<le> x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   781
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   782
  from ln have "ln 1 \<le> ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   783
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   784
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   785
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   786
lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   787
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   788
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   789
lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   790
by (insert ln_ge_zero_iff [of x], arith)
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   791
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   792
lemma ln_gt_zero:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   793
  assumes x: "1 < x" shows "0 < ln x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   794
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   795
  have "0 < x" using x by arith
22915
bb8a928a6bfa fix proofs
huffman
parents: 22722
diff changeset
   796
  hence "exp 0 < exp (ln x)" by (simp add: x)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   797
  thus ?thesis  by (simp only: exp_less_cancel_iff)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   798
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   799
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   800
lemma ln_gt_zero_imp_gt_one:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   801
  assumes ln: "0 < ln x" 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   802
      and x:  "0 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   803
  shows "1 < x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   804
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   805
  from ln have "ln 1 < ln x" by simp
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   806
  thus ?thesis by (simp add: x del: ln_one) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   807
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   808
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   809
lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   810
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   811
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   812
lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   813
by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   814
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   815
lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   816
by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   817
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   818
lemma exp_ln_eq: "exp u = x ==> ln x = u"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   819
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   820
23045
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   821
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   822
apply (subgoal_tac "isCont ln (exp (ln x))", simp)
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   823
apply (rule isCont_inverse_function [where f=exp], simp_all)
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   824
done
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   825
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   826
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   827
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   828
apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   829
apply (simp_all add: abs_if isCont_ln)
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   830
done
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
   831
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   832
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   833
subsection {* Sine and Cosine *}
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   834
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   835
definition
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   836
  sin :: "real => real" where
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   837
  "sin x = (\<Sum>n. (if even(n) then 0 else
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   838
             (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   839
 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   840
definition
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   841
  cos :: "real => real" where
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   842
  "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n)) 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   843
                            else 0) * x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   844
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   845
lemma summable_sin: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   846
     "summable (%n.  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   847
           (if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   848
           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   849
                x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   850
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   851
apply (rule_tac [2] summable_exp)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   852
apply (rule_tac x = 0 in exI)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   853
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   854
done
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   855
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   856
lemma summable_cos: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   857
      "summable (%n.  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   858
           (if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   859
           -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   860
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   861
apply (rule_tac [2] summable_exp)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   862
apply (rule_tac x = 0 in exI)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   863
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   864
done
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   865
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   866
lemma lemma_STAR_sin:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   867
     "(if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   868
       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   869
by (induct "n", auto)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   870
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   871
lemma lemma_STAR_cos:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   872
     "0 < n -->  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   873
      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   874
by (induct "n", auto)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   875
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   876
lemma lemma_STAR_cos1:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   877
     "0 < n -->  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   878
      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   879
by (induct "n", auto)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   880
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   881
lemma lemma_STAR_cos2:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   882
  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   883
                         else 0) = 0"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   884
apply (induct "n")
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   885
apply (case_tac [2] "n", auto)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   886
done
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   887
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   888
lemma sin_converges: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   889
      "(%n. (if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   890
            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   891
                 x ^ n) sums sin(x)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   892
unfolding sin_def by (rule summable_sin [THEN summable_sums])
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   893
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   894
lemma cos_converges: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   895
      "(%n. (if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   896
           -1 ^ (n div 2)/(real (fact n))  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   897
           else 0) * x ^ n) sums cos(x)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   898
unfolding cos_def by (rule summable_cos [THEN summable_sums])
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   899
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   900
lemma sin_fdiffs: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   901
      "diffs(%n. if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   902
           else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   903
       = (%n. if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   904
                 -1 ^ (n div 2)/(real (fact n))  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   905
              else 0)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   906
by (auto intro!: ext 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   907
         simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   908
         simp del: mult_Suc of_nat_Suc)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   909
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   910
lemma sin_fdiffs2: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   911
       "diffs(%n. if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   912
           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   913
       = (if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   914
                 -1 ^ (n div 2)/(real (fact n))  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   915
              else 0)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   916
by (simp only: sin_fdiffs)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   917
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   918
lemma cos_fdiffs: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   919
      "diffs(%n. if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   920
                 -1 ^ (n div 2)/(real (fact n)) else 0)  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   921
       = (%n. - (if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   922
           else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   923
by (auto intro!: ext 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   924
         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   925
         simp del: mult_Suc of_nat_Suc)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   926
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   927
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   928
lemma cos_fdiffs2: 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   929
      "diffs(%n. if even n then  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   930
                 -1 ^ (n div 2)/(real (fact n)) else 0) n 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   931
       = - (if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   932
           else -1 ^ ((n - Suc 0)div 2)/(real (fact n)))"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   933
by (simp only: cos_fdiffs)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   934
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   935
text{*Now at last we can get the derivatives of exp, sin and cos*}
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   936
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   937
lemma lemma_sin_minus:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   938
     "- sin x = (\<Sum>n. - ((if even n then 0 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   939
                  else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   940
by (auto intro!: sums_unique sums_minus sin_converges)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   941
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   942
lemma lemma_sin_ext:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   943
     "sin = (%x. \<Sum>n. 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   944
                   (if even n then 0  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   945
                       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   946
                   x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   947
by (auto intro!: ext simp add: sin_def)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   948
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   949
lemma lemma_cos_ext:
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   950
     "cos = (%x. \<Sum>n. 
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   951
                   (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   952
                   x ^ n)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   953
by (auto intro!: ext simp add: cos_def)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   954
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   955
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   956
apply (simp add: cos_def)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   957
apply (subst lemma_sin_ext)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   958
apply (auto simp add: sin_fdiffs2 [symmetric])
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   959
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   960
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   961
done
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   962
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   963
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   964
apply (subst lemma_cos_ext)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   965
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   966
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   967
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   968
done
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   969
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   970
lemma isCont_sin [simp]: "isCont sin x"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   971
by (rule DERIV_sin [THEN DERIV_isCont])
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   972
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   973
lemma isCont_cos [simp]: "isCont cos x"
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   974
by (rule DERIV_cos [THEN DERIV_isCont])
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   975
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   976
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   977
subsection {* Properties of Sine and Cosine *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   978
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   979
lemma sin_zero [simp]: "sin 0 = 0"
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   980
unfolding sin_def by (simp add: powser_zero)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   981
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   982
lemma cos_zero [simp]: "cos 0 = 1"
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
   983
unfolding cos_def by (simp add: powser_zero)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   984
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   985
lemma DERIV_sin_sin_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   986
     "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   987
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   988
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   989
lemma DERIV_sin_sin_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   990
     "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   991
apply (cut_tac x = x in DERIV_sin_sin_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   992
apply (auto simp add: mult_assoc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   993
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   994
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   995
lemma DERIV_sin_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   996
     "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   997
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   998
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   999
lemma DERIV_sin_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1000
     "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1001
by (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1002
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1003
lemma DERIV_cos_cos_mult [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1004
     "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1005
by (rule DERIV_mult, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1006
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1007
lemma DERIV_cos_cos_mult2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1008
     "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1009
apply (cut_tac x = x in DERIV_cos_cos_mult)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1010
apply (auto simp add: mult_ac)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1011
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1012
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1013
lemma DERIV_cos_realpow2 [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1014
     "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1015
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1016
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1017
lemma DERIV_cos_realpow2a [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1018
     "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1019
by (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1020
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1021
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1022
by auto
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1023
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1024
lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1025
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1026
apply (rule DERIV_cos_realpow2a, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1027
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1028
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1029
(* most useful *)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1030
lemma DERIV_cos_cos_mult3 [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1031
     "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1032
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1033
apply (rule DERIV_cos_cos_mult2, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1034
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1035
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1036
lemma DERIV_sin_circle_all: 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1037
     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1038
             (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1039
apply (simp only: diff_minus, safe)
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1040
apply (rule DERIV_add) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1041
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1042
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1043
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1044
lemma DERIV_sin_circle_all_zero [simp]:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1045
     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1046
by (cut_tac DERIV_sin_circle_all, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1047
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1048
lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1049
apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1050
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1051
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1052
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1053
lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
23286
huffman
parents: 23278
diff changeset
  1054
apply (subst add_commute)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1055
apply (simp (no_asm) del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1056
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1057
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1058
lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1059
apply (cut_tac x = x in sin_cos_squared_add2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1060
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1061
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1062
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1063
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1064
apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1065
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1066
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1067
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1068
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1069
apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1070
apply (simp del: realpow_Suc)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1071
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1072
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
  1073
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
23097
f4779adcd1a2 simplify some proofs
huffman
parents: 23082
diff changeset
  1074
by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1075
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1076
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1077
apply (insert abs_sin_le_one [of x]) 
22998
97e1f9c2cc46 avoid using redundant lemmas from RealDef.thy
huffman
parents: 22978
diff changeset
  1078
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1079
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1080
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1081
lemma sin_le_one [simp]: "sin x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1082
apply (insert abs_sin_le_one [of x]) 
22998
97e1f9c2cc46 avoid using redundant lemmas from RealDef.thy
huffman
parents: 22978
diff changeset
  1083
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1084
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1085
15081
32402f5624d1 abs notation
paulson
parents: 15079
diff changeset
  1086
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
23097
f4779adcd1a2 simplify some proofs
huffman
parents: 23082
diff changeset
  1087
by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1088
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1089
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1090
apply (insert abs_cos_le_one [of x]) 
22998
97e1f9c2cc46 avoid using redundant lemmas from RealDef.thy
huffman
parents: 22978
diff changeset
  1091
apply (simp add: abs_le_iff del: abs_cos_le_one) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1092
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1093
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1094
lemma cos_le_one [simp]: "cos x \<le> 1"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1095
apply (insert abs_cos_le_one [of x]) 
22998
97e1f9c2cc46 avoid using redundant lemmas from RealDef.thy
huffman
parents: 22978
diff changeset
  1096
apply (simp add: abs_le_iff del: abs_cos_le_one)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1097
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1098
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1099
lemma DERIV_fun_pow: "DERIV g x :> m ==>  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1100
      DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1101
apply (rule lemma_DERIV_subst)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1102
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1103
apply (rule DERIV_pow, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1104
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1105
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1106
lemma DERIV_fun_exp:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1107
     "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1108
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1109
apply (rule_tac f = exp in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1110
apply (rule DERIV_exp, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1111
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1112
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1113
lemma DERIV_fun_sin:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1114
     "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1115
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1116
apply (rule_tac f = sin in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1117
apply (rule DERIV_sin, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1118
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1119
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1120
lemma DERIV_fun_cos:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1121
     "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1122
apply (rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1123
apply (rule_tac f = cos in DERIV_chain2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1124
apply (rule DERIV_cos, auto)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1125
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1126
23069
cdfff0241c12 rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents: 23066
diff changeset
  1127
lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1128
                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1129
                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1130
                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1131
                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1132
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1133
(* lemma *)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1134
lemma lemma_DERIV_sin_cos_add:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1135
     "\<forall>x.  
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1136
         DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1137
               (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1138
apply (safe, rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1139
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1140
  --{*replaces the old @{text DERIV_tac}*}
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1141
apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1142
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1143
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1144
lemma sin_cos_add [simp]:
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1145
     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1146
      (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1147
apply (cut_tac y = 0 and x = x and y7 = y 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1148
       in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1149
apply (auto simp add: numeral_2_eq_2)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1150
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1151
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1152
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1153
apply (cut_tac x = x and y = y in sin_cos_add)
22969
bf523cac9a05 tuned proofs
huffman
parents: 22960
diff changeset
  1154
apply (simp del: sin_cos_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1155
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1156
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1157
lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1158
apply (cut_tac x = x and y = y in sin_cos_add)
22969
bf523cac9a05 tuned proofs
huffman
parents: 22960
diff changeset
  1159
apply (simp del: sin_cos_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1160
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1161
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1162
lemma lemma_DERIV_sin_cos_minus:
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1163
    "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1164
apply (safe, rule lemma_DERIV_subst)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1165
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
  1166
apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1167
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1168
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1169
lemma sin_cos_minus: 
15085
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1170
    "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1171
apply (cut_tac y = 0 and x = x 
5693a977a767 removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents: 15081
diff changeset
  1172
       in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
22969
bf523cac9a05 tuned proofs
huffman
parents: 22960
diff changeset
  1173
apply simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1174
done
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1175
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1176
lemma sin_minus [simp]: "sin (-x) = -sin(x)"
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1177
  using sin_cos_minus [where x=x] by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1178
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1179
lemma cos_minus [simp]: "cos (-x) = cos(x)"
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1180
  using sin_cos_minus [where x=x] by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1181
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1182
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
22969
bf523cac9a05 tuned proofs
huffman
parents: 22960
diff changeset
  1183
by (simp add: diff_minus sin_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1184
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1185
lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1186
by (simp add: sin_diff mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1187
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1188
lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
22969
bf523cac9a05 tuned proofs
huffman
parents: 22960
diff changeset
  1189
by (simp add: diff_minus cos_add)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1190
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1191
lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1192
by (simp add: cos_diff mult_commute)
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1193
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1194
lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1195
  using sin_add [where x=x and y=x] by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1196
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1197
lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
29165
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1198
  using cos_add [where x=x and y=x]
562f95f06244 cleaned up some proofs; removed redundant simp rules
huffman
parents: 29164
diff changeset
  1199
  by (simp add: power2_eq_square)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1200
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1201
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
  1202
subsection {* The Constant Pi *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1203
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
  1204
definition
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
  1205
  pi :: "real" where
23053
03fe1dafa418 define pi with THE instead of SOME; cleaned up
huffman
parents: 23052
diff changeset
  1206
  "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
  1207
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1208
text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1209
   hence define pi.*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1210
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1211
lemma sin_paired:
23177
3004310c95b1 replace (- 1) with -1
huffman
parents: 23176
diff changeset
  1212
     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1213
      sums  sin x"
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1214
proof -
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1215
  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1216
            (if even k then 0
23177
3004310c95b1 replace (- 1) with -1
huffman
parents: 23176
diff changeset
  1217
             else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1218
            x ^ k) 
23176
40a760921d94 simplify some proofs
huffman
parents: 23127
diff changeset
  1219
	sums sin x"