author  huffman 
Wed, 24 Dec 2008 13:16:26 0800  
changeset 29170  dad3933c88dd 
parent 29167  37a952bb9ebc 
child 29171  5eff800a695f 
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 

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

473 
lemma exp_fdiffs: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

474 
"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

475 
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

476 
del: mult_Suc of_nat_Suc) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

477 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

478 
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

479 
by (simp add: diffs_def) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

480 

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

482 
by (auto intro!: ext simp add: exp_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

483 

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

484 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
15229  485 
apply (simp add: exp_def) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

486 
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

487 
apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)") 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

488 
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

489 
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

490 
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

491 
apply (simp del: of_real_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

493 

23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

494 
lemma isCont_exp [simp]: "isCont exp x" 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

495 
by (rule DERIV_exp [THEN DERIV_isCont]) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

496 

95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

497 

29167  498 
subsubsection {* Properties of the Exponential Function *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

499 

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

502 
shows "(\<Sum>n. f n * 0 ^ n) = f 0" 

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

503 
proof  
23278  504 
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

505 
by (rule sums_unique [OF series_zero], simp add: power_0_left) 
23278  506 
thus ?thesis by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

508 

23278  509 
lemma exp_zero [simp]: "exp 0 = 1" 
510 
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) 

511 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

512 
lemma setsum_cl_ivl_Suc2: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

513 
"(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))" 
28069  514 
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

515 
del: setsum_cl_ivl_Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

516 

4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

517 
lemma exp_series_add: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

518 
fixes x y :: "'a::{real_field,recpower}" 
25062  519 
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

520 
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

521 
proof (induct n) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

522 
case 0 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

523 
show ?case 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

524 
unfolding S_def by simp 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

525 
next 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

526 
case (Suc n) 
25062  527 
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

528 
unfolding S_def by (simp add: power_Suc del: mult_Suc) 
25062  529 
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

530 
by simp 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

531 

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

533 
by (simp only: times_S) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

534 
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

535 
by (simp only: Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

536 
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

537 
+ 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

538 
by (rule left_distrib) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

539 
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

540 
+ (\<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

541 
by (simp only: setsum_right_distrib mult_ac) 
25062  542 
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
543 
+ (\<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

544 
by (simp add: times_S Suc_diff_le) 
25062  545 
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
546 
(\<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

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

550 
by (subst setsum_cl_ivl_Suc, simp) 
25062  551 
also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni))) + 
552 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 

553 
(\<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

554 
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

555 
real_of_nat_add [symmetric], simp) 
25062  556 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc ni))" 
23127  557 
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

558 
finally show 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

559 
"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

560 
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

561 
qed 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

562 

4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

563 
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

564 
unfolding exp_def 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

565 
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

566 

29170  567 
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" 
568 
by (rule exp_add [symmetric]) 

569 

23241  570 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
571 
unfolding exp_def 

572 
apply (subst of_real.suminf) 

573 
apply (rule summable_exp_generic) 

574 
apply (simp add: scaleR_conv_of_real) 

575 
done 

576 

29170  577 
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0" 
578 
proof 

579 
have "exp x * exp ( x) = 1" by (simp add: mult_exp_exp) 

580 
also assume "exp x = 0" 

581 
finally show "False" by simp 

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

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

583 

29170  584 
lemma exp_minus: "exp ( x) = inverse (exp x)" 
585 
by (rule inverse_unique [symmetric], simp add: mult_exp_exp) 

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

586 

29170  587 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
588 
unfolding diff_minus divide_inverse 

589 
by (simp add: exp_add exp_minus) 

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

590 

29167  591 

592 
subsubsection {* Properties of the Exponential Function on Reals *} 

593 

29170  594 
text {* Comparisons of @{term "exp x"} with zero. *} 
29167  595 

596 
text{*Proof: because every exponential can be seen as a square.*} 

597 
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)" 

598 
proof  

599 
have "0 \<le> exp (x/2) * exp (x/2)" by simp 

600 
thus ?thesis by (simp add: exp_add [symmetric]) 

601 
qed 

602 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

603 
lemma exp_gt_zero [simp]: "0 < exp (x::real)" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

604 
by (simp add: order_less_le) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

605 

29170  606 
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" 
607 
by (simp add: not_less) 

608 

609 
lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0" 

610 
by (simp add: not_le) 

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

611 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

612 
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

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

614 

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

615 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
15251  616 
apply (induct "n") 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

617 
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

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

619 

29170  620 
text {* Strict monotonicity of exponential. *} 
621 

622 
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)" 

623 
apply (drule order_le_imp_less_or_eq, auto) 

624 
apply (simp add: exp_def) 

625 
apply (rule real_le_trans) 

626 
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) 

627 
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff) 

628 
done 

629 

630 
lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x" 

631 
proof  

632 
assume x: "0 < x" 

633 
hence "1 < 1 + x" by simp 

634 
also from x have "1 + x \<le> exp x" 

635 
by (simp add: exp_ge_add_one_self_aux) 

636 
finally show ?thesis . 

637 
qed 

638 

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

639 
lemma exp_less_mono: 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

640 
fixes x y :: real 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

641 
assumes "x < y" shows "exp x < exp y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

642 
proof  
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

643 
from `x < y` have "0 < y  x" by simp 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

644 
hence "1 < exp (y  x)" by (rule exp_gt_one) 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

645 
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

646 
thus "exp x < exp y" by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

648 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

649 
lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y" 
29170  650 
apply (simp add: linorder_not_le [symmetric]) 
651 
apply (auto simp add: order_le_less exp_less_mono) 

15077
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 

29170  654 
lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

655 
by (auto intro: exp_less_mono exp_less_cancel) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

656 

29170  657 
lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

658 
by (auto simp add: linorder_not_less [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

659 

29170  660 
lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

661 
by (simp add: order_eq_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

662 

29170  663 
text {* Comparisons of @{term "exp x"} with one. *} 
664 

665 
lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x" 

666 
using exp_less_cancel_iff [where x=0 and y=x] by simp 

667 

668 
lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0" 

669 
using exp_less_cancel_iff [where x=x and y=0] by simp 

670 

671 
lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x" 

672 
using exp_le_cancel_iff [where x=0 and y=x] by simp 

673 

674 
lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0" 

675 
using exp_le_cancel_iff [where x=x and y=0] by simp 

676 

677 
lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0" 

678 
using exp_inj_iff [where x=x and y=0] by simp 

679 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

680 
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

681 
apply (rule IVT) 
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

682 
apply (auto intro: isCont_exp simp add: le_diff_eq) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

683 
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

684 
apply simp 
17014
ad5ceb90877d
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents:
16924
diff
changeset

685 
apply (rule exp_ge_add_one_self_aux, simp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

687 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

688 
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

689 
apply (rule_tac x = 1 and y = y in linorder_cases) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

690 
apply (drule order_less_imp_le [THEN lemma_exp_total]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

691 
apply (rule_tac [2] x = 0 in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

692 
apply (frule_tac [3] real_inverse_gt_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

693 
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

694 
apply (rule_tac x = "x" in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

695 
apply (simp add: exp_minus) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

697 

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

698 

29164  699 
subsection {* Natural Logarithm *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

700 

23043  701 
definition 
702 
ln :: "real => real" where 

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

704 

705 
lemma ln_exp [simp]: "ln (exp x) = x" 

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

706 
by (simp add: ln_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

707 

22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

708 
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

709 
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

710 

23043  711 
lemma exp_ln_iff [simp]: "(exp (ln x) = x) = (0 < x)" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

712 
apply (auto dest: exp_total) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

713 
apply (erule subst, simp) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

715 

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

716 
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

717 
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

718 
apply (simp add: exp_add exp_ln mult_pos_pos) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

720 

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

721 
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

722 
apply (simp only: exp_ln_iff [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

723 
apply (erule subst)+ 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

724 
apply simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

726 

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

727 
lemma ln_one[simp]: "ln 1 = 0" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

728 
by (rule exp_inj_iff [THEN iffD1], auto) 
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_inverse: "0 < x ==> ln(inverse x) =  ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

731 
apply (rule_tac a1 = "ln x" in add_left_cancel [THEN iffD1]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

732 
apply (auto simp add: positive_imp_inverse_positive ln_mult [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

734 

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

735 
lemma ln_div: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

736 
"[0 < x; 0 < y] ==> ln(x/y) = ln x  ln y" 
15229  737 
apply (simp add: divide_inverse) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

738 
apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

740 

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

741 
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

742 
apply (simp only: exp_ln_iff [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

743 
apply (erule subst)+ 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

744 
apply simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

746 

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

747 
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

748 
by (auto simp add: linorder_not_less [symmetric]) 
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_realpow: "0 < x ==> ln(x ^ n) = real n * ln(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

751 
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

752 

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

753 
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

754 
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

755 
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

756 
apply (auto simp add: exp_ge_add_one_self_aux) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

758 

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

759 
lemma ln_less_self [simp]: "0 < x ==> ln x < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

760 
apply (rule order_less_le_trans) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

761 
apply (rule_tac [2] ln_add_one_self_le_self) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

762 
apply (rule ln_less_cancel_iff [THEN iffD2], auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

764 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

765 
lemma ln_ge_zero [simp]: 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

766 
assumes x: "1 \<le> x" shows "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

768 
have "0 < x" using x by arith 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

769 
hence "exp 0 \<le> exp (ln x)" 
22915  770 
by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

771 
thus ?thesis by (simp only: exp_le_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

773 

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

774 
lemma ln_ge_zero_imp_ge_one: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

775 
assumes ln: "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

776 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

777 
shows "1 \<le> x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

779 
from ln have "ln 1 \<le> ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

780 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

782 

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

783 
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

784 
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

785 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

786 
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

787 
by (insert ln_ge_zero_iff [of x], arith) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

788 

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

789 
lemma ln_gt_zero: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

790 
assumes x: "1 < x" shows "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

792 
have "0 < x" using x by arith 
22915  793 
hence "exp 0 < exp (ln x)" by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

794 
thus ?thesis by (simp only: exp_less_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

796 

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

797 
lemma ln_gt_zero_imp_gt_one: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

798 
assumes ln: "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

799 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

800 
shows "1 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

802 
from ln have "ln 1 < ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

803 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

805 

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

806 
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

807 
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

808 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

809 
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

810 
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

811 

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

812 
lemma ln_less_zero: "[ 0 < x; x < 1 ] ==> ln x < 0" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

813 
by simp 
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 exp_ln_eq: "exp u = x ==> ln x = u" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

816 
by auto 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

817 

23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

818 
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

819 
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

820 
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

821 
done 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

822 

95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

823 
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

824 
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

825 
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

826 
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

827 
done 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

828 

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

829 

29164  830 
subsection {* Sine and Cosine *} 
831 

832 
definition 

833 
sin :: "real => real" where 

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

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

836 

837 
definition 

838 
cos :: "real => real" where 

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

840 
else 0) * x ^ n)" 

841 

842 
lemma summable_sin: 

843 
"summable (%n. 

844 
(if even n then 0 

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

846 
x ^ n)" 

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

848 
apply (rule_tac [2] summable_exp) 

849 
apply (rule_tac x = 0 in exI) 

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

851 
done 

852 

853 
lemma summable_cos: 

854 
"summable (%n. 

855 
(if even n then 

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

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

858 
apply (rule_tac [2] summable_exp) 

859 
apply (rule_tac x = 0 in exI) 

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

861 
done 

862 

863 
lemma lemma_STAR_sin: 

864 
"(if even n then 0 

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

866 
by (induct "n", auto) 

867 

868 
lemma lemma_STAR_cos: 

869 
"0 < n > 

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

871 
by (induct "n", auto) 

872 

873 
lemma lemma_STAR_cos1: 

874 
"0 < n > 

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

876 
by (induct "n", auto) 

877 

878 
lemma lemma_STAR_cos2: 

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

880 
else 0) = 0" 

881 
apply (induct "n") 

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

883 
done 

884 

885 
lemma sin_converges: 

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

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

888 
x ^ n) sums sin(x)" 

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

890 

891 
lemma cos_converges: 

892 
"(%n. (if even n then 

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

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

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

896 

897 
lemma sin_fdiffs: 

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

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

900 
= (%n. if even n then 

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

902 
else 0)" 

903 
by (auto intro!: ext 

904 
simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult 

905 
simp del: mult_Suc of_nat_Suc) 

906 

907 
lemma sin_fdiffs2: 

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

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

910 
= (if even n then 

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

912 
else 0)" 

913 
by (simp only: sin_fdiffs) 

914 

915 
lemma cos_fdiffs: 

916 
"diffs(%n. if even n then 

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

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

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

920 
by (auto intro!: ext 

921 
simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult 

922 
simp del: mult_Suc of_nat_Suc) 

923 

924 

925 
lemma cos_fdiffs2: 

926 
"diffs(%n. if even n then 

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

928 
=  (if even n then 0 

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

930 
by (simp only: cos_fdiffs) 

931 

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

933 

934 
lemma lemma_sin_minus: 

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

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

937 
by (auto intro!: sums_unique sums_minus sin_converges) 

938 

939 
lemma lemma_sin_ext: 

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

941 
(if even n then 0 

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

943 
x ^ n)" 

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

945 

946 
lemma lemma_cos_ext: 

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

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

949 
x ^ n)" 

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

951 

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

953 
apply (simp add: cos_def) 

954 
apply (subst lemma_sin_ext) 

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

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

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

958 
done 

959 

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

961 
apply (subst lemma_cos_ext) 

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

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

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

965 
done 

966 

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

968 
by (rule DERIV_sin [THEN DERIV_isCont]) 

969 

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

971 
by (rule DERIV_cos [THEN DERIV_isCont]) 

972 

973 

974 
subsection {* Properties of Sine and Cosine *} 

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

975 

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

976 
lemma sin_zero [simp]: "sin 0 = 0" 
23278  977 
unfolding sin_def by (simp add: powser_zero) 
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 cos_zero [simp]: "cos 0 = 1" 
23278  980 
unfolding cos_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 DERIV_sin_sin_mult [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

983 
"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

984 
by (rule DERIV_mult, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

985 

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

986 
lemma DERIV_sin_sin_mult2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

987 
"DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

988 
apply (cut_tac x = x in DERIV_sin_sin_mult) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

989 
apply (auto simp add: mult_assoc) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

991 

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

992 
lemma DERIV_sin_realpow2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

993 
"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

994 
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

995 

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

996 
lemma DERIV_sin_realpow2a [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

997 
"DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

998 
by (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

999 

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

1000 
lemma DERIV_cos_cos_mult [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1001 
"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

1002 
by (rule DERIV_mult, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1003 

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

1004 
lemma DERIV_cos_cos_mult2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1005 
"DERIV (%x. cos(x)*cos(x)) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1006 
apply (cut_tac x = x in DERIV_cos_cos_mult) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1007 
apply (auto simp add: mult_ac) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1009 

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

1010 
lemma DERIV_cos_realpow2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1011 
"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

1012 
by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1013 

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

1014 
lemma DERIV_cos_realpow2a [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1015 
"DERIV (%x. (cos x)\<twosuperior>) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1016 
by (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1017 

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

1018 
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

1019 
by auto 
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 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

1022 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1023 
apply (rule DERIV_cos_realpow2a, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1025 

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

1026 
(* most useful *) 
15229  1027 
lemma DERIV_cos_cos_mult3 [simp]: 
1028 
"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

1029 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1030 
apply (rule DERIV_cos_cos_mult2, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1032 

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

1033 
lemma DERIV_sin_circle_all: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1034 
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1035 
(2*cos(x)*sin(x)  2*cos(x)*sin(x))" 
15229  1036 
apply (simp only: diff_minus, safe) 
1037 
apply (rule DERIV_add) 

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

1038 
apply (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1040 

15229  1041 
lemma DERIV_sin_circle_all_zero [simp]: 
1042 
"\<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

1043 
by (cut_tac DERIV_sin_circle_all, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1044 

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

1045 
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

1046 
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

1047 
apply (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1049 

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

1050 
lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1" 
23286  1051 
apply (subst add_commute) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1052 
apply (simp (no_asm) del: realpow_Suc) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1054 

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

1055 
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

1056 
apply (cut_tac x = x in sin_cos_squared_add2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1057 
apply (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1059 

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

1060 
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1  (cos x)\<twosuperior>" 
15229  1061 
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

1062 
apply (simp del: realpow_Suc) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1064 

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

1065 
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1  (sin x)\<twosuperior>" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1066 
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

1067 
apply (simp del: realpow_Suc) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1069 

15081  1070 
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1" 
23097  1071 
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

1072 

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

1073 
lemma sin_ge_minus_one [simp]: "1 \<le> sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1074 
apply (insert abs_sin_le_one [of x]) 
22998  1075 
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1077 

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

1078 
lemma sin_le_one [simp]: "sin x \<le> 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1079 
apply (insert abs_sin_le_one [of x]) 
22998  1080 
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1082 

15081  1083 
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1" 
23097  1084 
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

1085 

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

1086 
lemma cos_ge_minus_one [simp]: "1 \<le> cos x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1087 
apply (insert abs_cos_le_one [of x]) 
22998  1088 
apply (simp add: abs_le_iff del: abs_cos_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1090 

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

1091 
lemma cos_le_one [simp]: "cos x \<le> 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1092 
apply (insert abs_cos_le_one [of x]) 
22998  1093 
apply (simp add: abs_le_iff del: abs_cos_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1095 

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

1096 
lemma DERIV_fun_pow: "DERIV g x :> m ==> 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1097 
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

1098 
apply (rule lemma_DERIV_subst) 
15229  1099 
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1100 
apply (rule DERIV_pow, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1102 

15229  1103 
lemma DERIV_fun_exp: 
1104 
"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

1105 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1106 
apply (rule_tac f = exp in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1107 
apply (rule DERIV_exp, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1109 

15229  1110 
lemma DERIV_fun_sin: 
1111 
"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

1112 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1113 
apply (rule_tac f = sin in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1114 
apply (rule DERIV_sin, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1116 

15229  1117 
lemma DERIV_fun_cos: 
1118 
"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

1119 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1120 
apply (rule_tac f = cos in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1121 
apply (rule DERIV_cos, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1123 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23066
diff
changeset

1124 
lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1125 
DERIV_sin DERIV_exp DERIV_inverse DERIV_pow 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1126 
DERIV_add DERIV_diff DERIV_mult DERIV_minus 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1127 
DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1128 
DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1129 

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

1130 
(* lemma *) 
15229  1131 
lemma lemma_DERIV_sin_cos_add: 
1132 
"\<forall>x. 

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

1133 
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

1134 
(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

1135 
apply (safe, rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1136 
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1137 
{*replaces the old @{text DERIV_tac}*} 
15229  1138 
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

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

1140 

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

1141 
lemma sin_cos_add [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1142 
"(sin (x + y)  (sin x * cos y + cos x * sin y)) ^ 2 + 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1143 
(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

1144 
apply (cut_tac y = 0 and x = x and y7 = y 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1145 
in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1146 
apply (auto simp add: numeral_2_eq_2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1148 

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

1149 
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

1150 
apply (cut_tac x = x and y = y in sin_cos_add) 
22969  1151 
apply (simp del: sin_cos_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1153 

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

1154 
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

1155 
apply (cut_tac x = x and y = y in sin_cos_add) 
22969  1156 
apply (simp del: sin_cos_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1158 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1159 
lemma lemma_DERIV_sin_cos_minus: 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1160 
"\<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

1161 
apply (safe, rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1162 
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
15229  1163 
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

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

1165 

29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1166 
lemma sin_cos_minus: 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1167 
"(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

1168 
apply (cut_tac y = 0 and x = x 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1169 
in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all]) 
22969  1170 
apply simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1172 

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

1173 
lemma sin_minus [simp]: "sin (x) = sin(x)" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1174 
using sin_cos_minus [where x=x] by simp 
15077
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 cos_minus [simp]: "cos (x) = cos(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 sin_diff: "sin (x  y) = sin x * cos y  cos x * sin y" 
22969  1180 
by (simp add: diff_minus sin_add) 
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_diff2: "sin (x  y) = cos y * sin x  sin y * cos x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1183 
by (simp add: sin_diff mult_commute) 
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 cos_diff: "cos (x  y) = cos x * cos y + sin x * sin y" 
22969  1186 
by (simp add: diff_minus cos_add) 
15077
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_diff2: "cos (x  y) = cos y * cos x + sin y * sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1189 
by (simp add: cos_diff mult_commute) 
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 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

1192 
using sin_add [where x=x and y=x] by simp 
15077
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 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

1195 
using cos_add [where x=x and y=x] 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1196 
by (simp add: power2_eq_square) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1197 

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

1198 

29164  1199 
subsection {* The Constant Pi *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1200 

23043  1201 
definition 
1202 
pi :: "real" where 

23053  1203 
"pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" 
23043  1204 

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

1205 
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

1206 
hence define pi.*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1207 

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

1208 
lemma sin_paired: 
23177  1209 
"(%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

1210 
sums sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1212 
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1213 
(if even k then 0 
23177  1214 
else 1 ^ ((k  Suc 0) div 2) / real (fact k)) * 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1215 
x ^ k) 
23176  1216 
sums sin x" 
1217 
unfolding sin_def 

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

1218 
by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
23176  1219 
thus ?thesis by (simp add: mult_ac) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1221 

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

1222 
lemma sin_gt_zero: "[0 < x; x < 2 ] ==> 0 < sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1223 
apply (subgoal_tac 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1224 
"(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. 
23177
3004310c95b1
replace ( 1) with 1
h& 