author  huffman 
Wed, 24 Dec 2008 08:06:27 0800  
changeset 29165  562f95f06244 
parent 29164  0d49c5b55046 
child 29166  c23b2d108612 
permissions  rwrr 
12196  1 
(* Title : Transcendental.thy 
2 
Author : Jacques D. Fleuriot 

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  6 
*) 
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  10 
theory Transcendental 
25600  11 
imports Fact Series Deriv NthRoot 
15131  12 
begin 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

13 

29164  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  29 
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac 
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  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  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  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  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  46 
lemma lemma_realpow_rev_sumr: 
15539  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  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  117 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  118 

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  127 
lemma sums_Suc_imp: 
128 
assumes f: "f 0 = 0" 

129 
shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s" 

130 
unfolding sums_def 

131 
apply (rule LIMSEQ_imp_Suc) 

132 
apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric]) 

133 
apply (simp only: setsum_shift_bounds_Suc_ivl) 

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  136 
lemma diffs_equiv: 
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  139 
(\<Sum>n. (diffs c)(n) * (x ^ n))" 
29163  140 
unfolding diffs_def 
141 
apply (drule summable_sums) 

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  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  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  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  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  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  165 
apply (cases "n", simp) 
166 
apply (simp add: lemma_realpow_diff_sumr2 h 

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  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  171 
apply simp 
172 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

173 
apply (rule setsum_cong [OF refl]) 

15539  174 
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
20860  175 
apply (clarify) 
176 
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac 

177 
del: setsum_op_ivl_Suc realpow_Suc) 

178 
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) 

179 
apply (simp add: mult_ac) 

180 
done 

181 

182 
lemma real_setsum_nat_ivl_bounded2: 

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..<nk} \<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  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  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  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  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  205 
apply (rule mult_commute) 
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  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  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  218 
apply (intro 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

219 
order_trans [OF norm_setsum] 
20860  220 
real_setsum_nat_ivl_bounded2 
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  223 
zero_le_power K) 
224 
apply (rule le_Kn, simp) 

225 
done 

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  228 
by (simp only: mult_assoc) 
229 
finally show ?thesis . 

230 
qed 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

231 

20860  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  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  237 
shows "f  0 > 0" 
29163  238 
unfolding LIM_def diff_0_right 
239 
proof (safe) 

240 
let ?h = "of_real (k / 2)::'a" 

241 
have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all 

242 
hence "norm (f ?h) \<le> K * norm ?h" by (rule le) 

243 
hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero]) 

244 
hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff) 

245 

20860  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  248 
proof (cases) 
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  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  253 
next 
254 
assume K_neq_zero: "K \<noteq> 0" 

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  257 
proof (rule exI, safe) 
258 
from k r K show "0 < min k (r * inverse K / 2)" 

259 
by (simp add: mult_pos_pos positive_imp_inverse_positive) 

260 
next 

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  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  267 
by (rule mult_strict_left_mono) 
268 
also have "\<dots> = r / 2" 

269 
using K_neq_zero by simp 

270 
also have "r / 2 < r" 

271 
using r by simp 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

272 
finally show "norm (f x) < r" . 
20860  273 
qed 
274 
qed 

275 
qed 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

276 

15229  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  280 
assumes k: "0 < (k::real)" 
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  283 
shows "(\<lambda>h. suminf (g h))  0 > 0" 
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  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  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  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  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  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  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  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  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  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  316 
by (rule order_le_less_trans) 
317 
hence r_neq_0: "r \<noteq> 0" by simp 

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  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  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  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  339 
by (rule diffs_equiv [THEN sums_summable]) 
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  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  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  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  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  362 
apply (simp (no_asm) add: mult_assoc [symmetric]) 
363 
apply (rule lemma_termdiff3) 

364 
apply (rule h) 

365 
apply (rule r1 [THEN order_less_imp_le]) 

366 
apply (rule xh [THEN order_less_imp_le]) 

367 
done 

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  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  373 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
374 
assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 

375 
assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

376 
assumes 4: "norm x < norm K" 
20860  377 
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" 
29163  378 
unfolding deriv_def 
379 
proof (rule LIM_zero_cancel) 

20860  380 
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n)  suminf (\<lambda>n. c n * x ^ n)) / h 
381 
 suminf (\<lambda>n. diffs c n * x ^ n))  0 > 0" 

382 
proof (rule LIM_equal2) 

29163  383 
show "0 < norm K  norm x" using 4 by (simp add: less_diff_eq) 
20860  384 
next 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

385 
fix h :: 'a 
20860  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  391 
have A: "summable (\<lambda>n. c n * x ^ n)" 
392 
by (rule powser_inside [OF 1 4]) 

393 
have B: "summable (\<lambda>n. c n * (x + h) ^ n)" 

394 
by (rule powser_inside [OF 1 5]) 

395 
have C: "summable (\<lambda>n. diffs c n * x ^ n)" 

396 
by (rule powser_inside [OF 2 4]) 

397 
show "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x ^ n)) / h 

398 
 (\<Sum>n. diffs c n * x ^ n) = 

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  400 
apply (subst sums_unique [OF diffs_equiv [OF C]]) 
401 
apply (subst suminf_diff [OF B A]) 

402 
apply (subst suminf_divide [symmetric]) 

403 
apply (rule summable_diff [OF B A]) 

404 
apply (subst suminf_diff) 

405 
apply (rule summable_divide) 

406 
apply (rule summable_diff [OF B A]) 

407 
apply (rule sums_summable [OF diffs_equiv [OF C]]) 

29163  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  410 
done 
411 
next 

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  414 
by (rule termdiffs_aux [OF 3 4]) 
415 
qed 

416 
qed 

417 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

418 

29164  419 
subsection {* Exponential Function *} 
23043  420 

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  423 
"exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))" 
23043  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  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  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  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  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  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  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  468 

25062  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  471 

472 

29164  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  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  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  500 
subsection {* Properties of the Exponential Function *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

501 

23278  502 
lemma powser_zero: 
503 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}" 

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  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  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  511 
lemma exp_zero [simp]: "exp 0 = 1" 
512 
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) 

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  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  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  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  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  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 (ni))" 
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 (ni)) 
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 (ni))" 
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 (ni)) 
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 (ni)))" 
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  544 
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
545 
+ (\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

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  547 
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
548 
(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni)))" 

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  550 
also have "(\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 
551 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

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  553 
also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni))) + 
554 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 

555 
(\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc ni)))" 

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  558 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc ni))" 
23127  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  569 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
570 
unfolding exp_def 

571 
apply (subst of_real.suminf) 

572 
apply (rule summable_exp_generic) 

573 
apply (simp add: scaleR_conv_of_real) 

574 
done 

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  577 
apply (drule order_le_imp_less_or_eq, auto) 
15229  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  580 
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) 
25875  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  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  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  670 
apply (simp add: linorder_not_le [symmetric]) 
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  702 
subsection {* Natural Logarithm *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

703 

23043  704 
definition 
705 
ln :: "real => real" where 

706 
"ln x = (THE u. exp u = x)" 

707 

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  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  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  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  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  833 
subsection {* Sine and Cosine *} 
834 

835 
definition 

836 
sin :: "real => real" where 

837 
"sin x = (\<Sum>n. (if even(n) then 0 else 

838 
(1 ^ ((n  Suc 0) div 2))/(real (fact n))) * x ^ n)" 

839 

840 
definition 

841 
cos :: "real => real" where 

842 
"cos x = (\<Sum>n. (if even(n) then (1 ^ (n div 2))/(real (fact n)) 

843 
else 0) * x ^ n)" 

844 

845 
lemma summable_sin: 

846 
"summable (%n. 

847 
(if even n then 0 

848 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

849 
x ^ n)" 

850 
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test) 

851 
apply (rule_tac [2] summable_exp) 

852 
apply (rule_tac x = 0 in exI) 

853 
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) 

854 
done 

855 

856 
lemma summable_cos: 

857 
"summable (%n. 

858 
(if even n then 

859 
1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)" 

860 
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test) 

861 
apply (rule_tac [2] summable_exp) 

862 
apply (rule_tac x = 0 in exI) 

863 
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) 

864 
done 

865 

866 
lemma lemma_STAR_sin: 

867 
"(if even n then 0 

868 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0" 

869 
by (induct "n", auto) 

870 

871 
lemma lemma_STAR_cos: 

872 
"0 < n > 

873 
1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" 

874 
by (induct "n", auto) 

875 

876 
lemma lemma_STAR_cos1: 

877 
"0 < n > 

878 
(1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" 

879 
by (induct "n", auto) 

880 

881 
lemma lemma_STAR_cos2: 

882 
"(\<Sum>n=1..<n. if even n then 1 ^ (n div 2)/(real (fact n)) * 0 ^ n 

883 
else 0) = 0" 

884 
apply (induct "n") 

885 
apply (case_tac [2] "n", auto) 

886 
done 

887 

888 
lemma sin_converges: 

889 
"(%n. (if even n then 0 

890 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

891 
x ^ n) sums sin(x)" 

892 
unfolding sin_def by (rule summable_sin [THEN summable_sums]) 

893 

894 
lemma cos_converges: 

895 
"(%n. (if even n then 

896 
1 ^ (n div 2)/(real (fact n)) 

897 
else 0) * x ^ n) sums cos(x)" 

898 
unfolding cos_def by (rule summable_cos [THEN summable_sums]) 

899 

900 
lemma sin_fdiffs: 

901 
"diffs(%n. if even n then 0 

902 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) 

903 
= (%n. if even n then 

904 
1 ^ (n div 2)/(real (fact n)) 

905 
else 0)" 

906 
by (auto intro!: ext 

907 
simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult 

908 
simp del: mult_Suc of_nat_Suc) 

909 

910 
lemma sin_fdiffs2: 

911 
"diffs(%n. if even n then 0 

912 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) n 

913 
= (if even n then 

914 
1 ^ (n div 2)/(real (fact n)) 

915 
else 0)" 

916 
by (simp only: sin_fdiffs) 

917 

918 
lemma cos_fdiffs: 

919 
"diffs(%n. if even n then 

920 
1 ^ (n div 2)/(real (fact n)) else 0) 

921 
= (%n.  (if even n then 0 

922 
else 1 ^ ((n  Suc 0)div 2)/(real (fact n))))" 

923 
by (auto intro!: ext 

924 
simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult 

925 
simp del: mult_Suc of_nat_Suc) 

926 

927 

928 
lemma cos_fdiffs2: 

929 
"diffs(%n. if even n then 

930 
1 ^ (n div 2)/(real (fact n)) else 0) n 

931 
=  (if even n then 0 

932 
else 1 ^ ((n  Suc 0)div 2)/(real (fact n)))" 

933 
by (simp only: cos_fdiffs) 

934 

935 
text{*Now at last we can get the derivatives of exp, sin and cos*} 

936 

937 
lemma lemma_sin_minus: 

938 
" sin x = (\<Sum>n.  ((if even n then 0 

939 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * x ^ n))" 

940 
by (auto intro!: sums_unique sums_minus sin_converges) 

941 

942 
lemma lemma_sin_ext: 

943 
"sin = (%x. \<Sum>n. 

944 
(if even n then 0 

945 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

946 
x ^ n)" 

947 
by (auto intro!: ext simp add: sin_def) 

948 

949 
lemma lemma_cos_ext: 

950 
"cos = (%x. \<Sum>n. 

951 
(if even n then 1 ^ (n div 2)/(real (fact n)) else 0) * 

952 
x ^ n)" 

953 
by (auto intro!: ext simp add: cos_def) 

954 

955 
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" 

956 
apply (simp add: cos_def) 

957 
apply (subst lemma_sin_ext) 

958 
apply (auto simp add: sin_fdiffs2 [symmetric]) 

959 
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs) 

960 
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs) 

961 
done 

962 

963 
lemma DERIV_cos [simp]: "DERIV cos x :> sin(x)" 

964 
apply (subst lemma_cos_ext) 

965 
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left) 

966 
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs) 

967 
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus) 

968 
done 

969 

970 
lemma isCont_sin [simp]: "isCont sin x" 

971 
by (rule DERIV_sin [THEN DERIV_isCont]) 

972 

973 
lemma isCont_cos [simp]: "isCont cos x" 

974 
by (rule DERIV_cos [THEN DERIV_isCont]) 

975 

976 

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  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  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  1030 
lemma DERIV_cos_cos_mult3 [simp]: 
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  1039 
apply (simp only: diff_minus, safe) 
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  1044 
lemma DERIV_sin_circle_all_zero [simp]: 
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  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  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  1073 
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1" 
23097  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  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  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  1086 
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1" 
23097  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  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  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  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  1106 
lemma DERIV_fun_exp: 
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  1113 
lemma DERIV_fun_sin: 
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  1120 
lemma DERIV_fun_cos: 
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  1134 
lemma lemma_DERIV_sin_cos_add: 
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  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  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  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  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  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  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  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  1202 
subsection {* The Constant Pi *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1203 

23043  1204 
definition 
1205 
pi :: "real" where 

23053  1206 
"pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" 
23043  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  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  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  1219 
sums sin x" 