author  avigad 
Fri, 17 Jul 2009 13:12:18 0400  
changeset 32047  c141f139ce26 
parent 32038  4127b89f48ab 
child 36974  b877866b5b00 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
27239
diff
changeset

1 
(* Author : Jacques D. Fleuriot 
12224  2 
Copyright : 2001 University of Edinburgh 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

3 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
12224  4 
*) 
5 

15944  6 
header{*MacLaurin Series*} 
7 

15131  8 
theory MacLaurin 
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29803
diff
changeset

9 
imports Transcendental 
15131  10 
begin 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

11 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

12 
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

13 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

14 
text{*This is a very long, messy proof even now that it's been broken down 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

15 
into lemmas.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

16 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

17 
lemma Maclaurin_lemma: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

18 
"0 < h ==> 
15539  19 
\<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

20 
(B * ((h^n) / real(fact n)))" 
15539  21 
apply (rule_tac x = "(f h  (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) * 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

22 
real(fact n) / (h^n)" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

23 
in exI) 
15539  24 
apply (simp) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

25 
done 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

26 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

27 
lemma eq_diff_eq': "(x = y  z) = (y = x + (z::real))" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

28 
by arith 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

29 

32038  30 
lemma fact_diff_Suc [rule_format]: 
31 
"n < Suc m ==> fact (Suc m  n) = (Suc m  n) * fact (m  n)" 

32 
by (subst fact_reduce_nat, auto) 

33 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

34 
lemma Maclaurin_lemma2: 
29187  35 
assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 
36 
assumes n: "n = Suc k" 

37 
assumes difg: "difg = 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

38 
(\<lambda>m t. diff m t  
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

39 
((\<Sum>p = 0..<n  m. diff (m + p) 0 / real (fact p) * t ^ p) + 
29187  40 
B * (t ^ (n  m) / real (fact (n  m)))))" 
41 
shows 

42 
"\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (difg m) t :> difg (Suc m) t" 

43 
unfolding difg 

44 
apply clarify 

45 
apply (rule DERIV_diff) 

46 
apply (simp add: diff) 

47 
apply (simp only: n) 

48 
apply (rule DERIV_add) 

49 
apply (rule_tac [2] DERIV_cmult) 

50 
apply (rule_tac [2] lemma_DERIV_subst) 

51 
apply (rule_tac [2] DERIV_quotient) 

52 
apply (rule_tac [3] DERIV_const) 

53 
apply (rule_tac [2] DERIV_pow) 

32038  54 
prefer 3 
55 

56 
apply (simp add: fact_diff_Suc) 

29187  57 
prefer 2 apply simp 
58 
apply (frule less_iff_Suc_add [THEN iffD1], clarify) 

59 
apply (simp del: setsum_op_ivl_Suc) 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29811
diff
changeset

60 
apply (insert sumr_offset4 [of "Suc 0"]) 
32047  61 
apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc) 
29187  62 
apply (rule lemma_DERIV_subst) 
63 
apply (rule DERIV_add) 

64 
apply (rule_tac [2] DERIV_const) 

65 
apply (rule DERIV_sumr, clarify) 

66 
prefer 2 apply simp 

32047  67 
apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc) 
29187  68 
apply (rule DERIV_cmult) 
69 
apply (rule lemma_DERIV_subst) 

31881  70 
apply (best intro!: DERIV_intros) 
32047  71 
apply (subst fact_Suc) 
29187  72 
apply (subst real_of_nat_mult) 
73 
apply (simp add: mult_ac) 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

74 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

75 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

76 
lemma Maclaurin: 
29187  77 
assumes h: "0 < h" 
78 
assumes n: "0 < n" 

79 
assumes diff_0: "diff 0 = f" 

80 
assumes diff_Suc: 

81 
"\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t" 

82 
shows 

83 
"\<exists>t. 0 < t & t < h & 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

84 
f h = 
15539  85 
setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

86 
(diff n t / real (fact n)) * h ^ n" 
29187  87 
proof  
88 
from n obtain m where m: "n = Suc m" 

89 
by (cases n, simp add: n) 

90 

91 
obtain B where f_h: "f h = 

92 
(\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) + 

93 
B * (h ^ n / real (fact n))" 

94 
using Maclaurin_lemma [OF h] .. 

95 

96 
obtain g where g_def: "g = (%t. f t  

97 
(setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} 

98 
+ (B * (t^n / real(fact n)))))" by blast 

99 

100 
have g2: "g 0 = 0 & g h = 0" 

101 
apply (simp add: m f_h g_def del: setsum_op_ivl_Suc) 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29811
diff
changeset

102 
apply (cut_tac n = m and k = "Suc 0" in sumr_offset2) 
29187  103 
apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc) 
104 
done 

105 

106 
obtain difg where difg_def: "difg = (%m t. diff m t  

107 
(setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<nm} 

108 
+ (B * ((t ^ (n  m)) / real (fact (n  m))))))" by blast 

109 

110 
have difg_0: "difg 0 = g" 

111 
unfolding difg_def g_def by (simp add: diff_0) 

112 

113 
have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real. 

114 
m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t" 

115 
using diff_Suc m difg_def by (rule Maclaurin_lemma2) 

116 

117 
have difg_eq_0: "\<forall>m. m < n > difg m 0 = 0" 

118 
apply clarify 

119 
apply (simp add: m difg_def) 

120 
apply (frule less_iff_Suc_add [THEN iffD1], clarify) 

121 
apply (simp del: setsum_op_ivl_Suc) 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29811
diff
changeset

122 
apply (insert sumr_offset4 [of "Suc 0"]) 
32047  123 
apply (simp del: setsum_op_ivl_Suc fact_Suc) 
29187  124 
done 
125 

126 
have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" 

127 
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp 

128 

129 
have differentiable_difg: 

130 
"\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x" 

131 
by (rule differentiableI [OF difg_Suc [rule_format]]) simp 

132 

133 
have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk> 

134 
\<Longrightarrow> difg (Suc m) t = 0" 

135 
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp 

136 

137 
have "m < n" using m by simp 

138 

139 
have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0" 

140 
using `m < n` 

141 
proof (induct m) 

142 
case 0 

143 
show ?case 

144 
proof (rule Rolle) 

145 
show "0 < h" by fact 

146 
show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) 

147 
show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x" 

148 
by (simp add: isCont_difg n) 

149 
show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x" 

150 
by (simp add: differentiable_difg n) 

151 
qed 

152 
next 

153 
case (Suc m') 

154 
hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp 

155 
then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast 

156 
have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0" 

157 
proof (rule Rolle) 

158 
show "0 < t" by fact 

159 
show "difg (Suc m') 0 = difg (Suc m') t" 

160 
using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0) 

161 
show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x" 

162 
using `t < h` `Suc m' < n` by (simp add: isCont_difg) 

163 
show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x" 

164 
using `t < h` `Suc m' < n` by (simp add: differentiable_difg) 

165 
qed 

166 
thus ?case 

167 
using `t < h` by auto 

168 
qed 

169 

170 
then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast 

171 

172 
hence "difg (Suc m) t = 0" 

173 
using `m < n` by (simp add: difg_Suc_eq_0) 

174 

175 
show ?thesis 

176 
proof (intro exI conjI) 

177 
show "0 < t" by fact 

178 
show "t < h" by fact 

179 
show "f h = 

180 
(\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + 

181 
diff n t / real (fact n) * h ^ n" 

182 
using `difg (Suc m) t = 0` 

32047  183 
by (simp add: m f_h difg_def del: fact_Suc) 
29187  184 
qed 
185 

186 
qed 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

187 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

188 
lemma Maclaurin_objl: 
25162  189 
"0 < h & n>0 & diff 0 = f & 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

190 
(\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

191 
> (\<exists>t. 0 < t & t < h & 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

192 
f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

193 
diff n t / real (fact n) * h ^ n)" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

194 
by (blast intro: Maclaurin) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

195 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

196 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

197 
lemma Maclaurin2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

198 
"[ 0 < h; diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

199 
\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

200 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

201 
==> \<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

202 
t \<le> h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

203 
f h = 
15539  204 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

205 
diff n t / real (fact n) * h ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

206 
apply (case_tac "n", auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

207 
apply (drule Maclaurin, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

208 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

209 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

210 
lemma Maclaurin2_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

211 
"0 < h & diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

212 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

213 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

214 
> (\<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

215 
t \<le> h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

216 
f h = 
15539  217 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

218 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

219 
by (blast intro: Maclaurin2) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

220 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

221 
lemma Maclaurin_minus: 
25162  222 
"[ h < 0; n > 0; diff 0 = f; 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

223 
\<forall>m t. m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

224 
==> \<exists>t. h < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

225 
t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

226 
f h = 
15539  227 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

228 
diff n t / real (fact n) * h ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

229 
apply (cut_tac f = "%x. f (x)" 
23177  230 
and diff = "%n x. (1 ^ n) * diff n (x)" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

231 
and h = "h" and n = n in Maclaurin_objl) 
15539  232 
apply (simp) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

233 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

234 
apply (subst minus_mult_right) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

235 
apply (rule DERIV_cmult) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

236 
apply (rule lemma_DERIV_subst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

237 
apply (rule DERIV_chain2 [where g=uminus]) 
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
22985
diff
changeset

238 
apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

239 
prefer 2 apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

240 
apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

241 
apply (rule_tac x = "t" in exI, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

242 
apply (subgoal_tac "(\<Sum>m = 0..<n. 1 ^ m * diff m 0 * (h)^m / real(fact m)) = 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

243 
(\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))") 
15536  244 
apply (rule_tac [2] setsum_cong[OF refl]) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

245 
apply (auto simp add: divide_inverse power_mult_distrib [symmetric]) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

246 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

247 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

248 
lemma Maclaurin_minus_objl: 
25162  249 
"(h < 0 & n > 0 & diff 0 = f & 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

250 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

251 
m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

252 
> (\<exists>t. h < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

253 
t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

254 
f h = 
15539  255 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

256 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

257 
by (blast intro: Maclaurin_minus) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

258 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

259 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

260 
subsection{*More Convenient "Bidirectional" Version.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

261 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

262 
(* not good for PVS sin_approx, cos_approx *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

263 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

264 
lemma Maclaurin_bi_le_lemma [rule_format]: 
25162  265 
"n>0 \<longrightarrow> 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

266 
diff 0 0 = 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

267 
(\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) + 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

268 
diff n 0 * 0 ^ n / real (fact n)" 
15251  269 
by (induct "n", auto) 
14738  270 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

271 
lemma Maclaurin_bi_le: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

272 
"[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

273 
\<forall>m t. m < n & abs t \<le> abs x > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

274 
==> \<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

275 
f x = 
15539  276 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

277 
diff n t / real (fact n) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

278 
apply (case_tac "n = 0", force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

279 
apply (case_tac "x = 0") 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

280 
apply (rule_tac x = 0 in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

281 
apply (force simp add: Maclaurin_bi_le_lemma) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

282 
apply (cut_tac x = x and y = 0 in linorder_less_linear, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

283 
txt{*Case 1, where @{term "x < 0"}*} 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

284 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

285 
apply (simp add: abs_if) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

286 
apply (rule_tac x = t in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

287 
apply (simp add: abs_if) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

288 
txt{*Case 2, where @{term "0 < x"}*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

289 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

290 
apply (simp add: abs_if) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

291 
apply (rule_tac x = t in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

292 
apply (simp add: abs_if) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

293 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

294 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

295 
lemma Maclaurin_all_lt: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

296 
"[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

297 
\<forall>m x. DERIV (diff m) x :> diff(Suc m) x; 
25162  298 
x ~= 0; n > 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

299 
] ==> \<exists>t. 0 < abs t & abs t < abs x & 
15539  300 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

301 
(diff n t / real (fact n)) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

302 
apply (rule_tac x = x and y = 0 in linorder_cases) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

303 
prefer 2 apply blast 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

304 
apply (drule_tac [2] diff=diff in Maclaurin) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

305 
apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe) 
15229  306 
apply (rule_tac [!] x = t in exI, auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

307 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

308 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

309 
lemma Maclaurin_all_lt_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

310 
"diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

311 
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) & 
25162  312 
x ~= 0 & n > 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

313 
> (\<exists>t. 0 < abs t & abs t < abs x & 
15539  314 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

315 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

316 
by (blast intro: Maclaurin_all_lt) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

317 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

318 
lemma Maclaurin_zero [rule_format]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

319 
"x = (0::real) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

320 
==> n \<noteq> 0 > 
15539  321 
(\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) = 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

322 
diff 0 0" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

323 
by (induct n, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

324 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

325 
lemma Maclaurin_all_le: "[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

326 
\<forall>m x. DERIV (diff m) x :> diff (Suc m) x 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

327 
] ==> \<exists>t. abs t \<le> abs x & 
15539  328 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

329 
(diff n t / real (fact n)) * x ^ n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

330 
apply(cases "n=0") 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

331 
apply (force) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

332 
apply (case_tac "x = 0") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

333 
apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

334 
apply (drule not0_implies_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

335 
apply (rule_tac x = 0 in exI, force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

336 
apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

337 
apply (rule_tac x = t in exI, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

338 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

339 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

340 
lemma Maclaurin_all_le_objl: "diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

341 
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

342 
> (\<exists>t. abs t \<le> abs x & 
15539  343 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

344 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

345 
by (blast intro: Maclaurin_all_le) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

346 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

347 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

348 
subsection{*Version for Exponential Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

349 

25162  350 
lemma Maclaurin_exp_lt: "[ x ~= 0; n > 0 ] 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

351 
==> (\<exists>t. 0 < abs t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

352 
abs t < abs x & 
15539  353 
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

354 
(exp t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

355 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

356 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

357 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

358 
lemma Maclaurin_exp_le: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

359 
"\<exists>t. abs t \<le> abs x & 
15539  360 
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

361 
(exp t / real (fact n)) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

362 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

363 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

364 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

365 
subsection{*Version for Sine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

366 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

367 
lemma mod_exhaust_less_4: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

368 
"m mod 4 = 0  m mod 4 = 1  m mod 4 = 2  m mod 4 = (3::nat)" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

369 
by auto 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

370 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

371 
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

372 
"n\<noteq>0 > Suc (Suc (2 * n  2)) = 2*n" 
15251  373 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

374 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

375 
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

376 
"n\<noteq>0 > Suc (Suc (4*n  2)) = 4*n" 
15251  377 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

378 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

379 
lemma Suc_mult_two_diff_one [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

380 
"n\<noteq>0 > Suc (2 * n  1) = 2*n" 
15251  381 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

382 

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

383 

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

384 
text{*It is unclear why so many variant results are needed.*} 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

385 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

386 
lemma Maclaurin_sin_expansion2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

387 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

388 
sin x = 
15539  389 
(\<Sum>m=0..<n. (if even m then 0 
23177  390 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  391 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

392 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

393 
apply (cut_tac f = sin and n = n and x = x 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

394 
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

395 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

396 
apply (simp (no_asm)) 
15539  397 
apply (simp (no_asm)) 
23242  398 
apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

399 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

400 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

401 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

402 
apply (rule_tac x = t in exI, simp) 
15536  403 
apply (rule setsum_cong[OF refl]) 
15539  404 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

405 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

406 

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

407 
lemma Maclaurin_sin_expansion: 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

408 
"\<exists>t. sin x = 
15539  409 
(\<Sum>m=0..<n. (if even m then 0 
23177  410 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  411 
x ^ m) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

412 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

413 
apply (insert Maclaurin_sin_expansion2 [of x n]) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

414 
apply (blast intro: elim:); 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

416 

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

417 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

418 
lemma Maclaurin_sin_expansion3: 
25162  419 
"[ n > 0; 0 < x ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

420 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

421 
sin x = 
15539  422 
(\<Sum>m=0..<n. (if even m then 0 
23177  423 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  424 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

425 
+ ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

426 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

427 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

428 
apply simp 
15539  429 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

430 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

431 
apply (rule_tac x = t in exI, simp) 
15536  432 
apply (rule setsum_cong[OF refl]) 
15539  433 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

434 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

435 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

436 
lemma Maclaurin_sin_expansion4: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

437 
"0 < x ==> 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

438 
\<exists>t. 0 < t & t \<le> x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

439 
sin x = 
15539  440 
(\<Sum>m=0..<n. (if even m then 0 
23177  441 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  442 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

443 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

444 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

445 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

446 
apply simp 
15539  447 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

448 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

449 
apply (rule_tac x = t in exI, simp) 
15536  450 
apply (rule setsum_cong[OF refl]) 
15539  451 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

452 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

453 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

454 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

455 
subsection{*Maclaurin Expansion for Cosine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

456 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

457 
lemma sumr_cos_zero_one [simp]: 
15539  458 
"(\<Sum>m=0..<(Suc n). 
23177  459 
(if even m then 1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" 
15251  460 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

461 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

462 
lemma Maclaurin_cos_expansion: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

463 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

464 
cos x = 
15539  465 
(\<Sum>m=0..<n. (if even m 
23177  466 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

467 
else 0) * 
15539  468 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

469 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

470 
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

471 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

472 
apply (simp (no_asm)) 
15539  473 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

474 
apply (case_tac "n", simp) 
15561  475 
apply (simp del: setsum_op_ivl_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

476 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

477 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

478 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

479 
apply (rule_tac x = t in exI, simp) 
15536  480 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

481 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

482 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

483 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

484 
lemma Maclaurin_cos_expansion2: 
25162  485 
"[ 0 < x; n > 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

486 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

487 
cos x = 
15539  488 
(\<Sum>m=0..<n. (if even m 
23177  489 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

490 
else 0) * 
15539  491 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

492 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

493 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

494 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

495 
apply simp 
15539  496 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

497 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

498 
apply (rule_tac x = t in exI, simp) 
15536  499 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

500 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

501 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

502 

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

503 
lemma Maclaurin_minus_cos_expansion: 
25162  504 
"[ x < 0; n > 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

505 
\<exists>t. x < t & t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

506 
cos x = 
15539  507 
(\<Sum>m=0..<n. (if even m 
23177  508 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

509 
else 0) * 
15539  510 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

511 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

512 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

513 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

514 
apply simp 
15539  515 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

516 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

517 
apply (rule_tac x = t in exI, simp) 
15536  518 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

519 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

520 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

521 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

522 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

523 
(* Version for ln(1 +/ x). Where is it?? *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

524 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

525 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

526 
lemma sin_bound_lemma: 
15081  527 
"[x = y; abs u \<le> (v::real) ] ==> \<bar>(x + u)  y\<bar> \<le> v" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

528 
by auto 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

529 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

530 
lemma Maclaurin_sin_bound: 
23177  531 
"abs(sin x  (\<Sum>m=0..<n. (if even m then 0 else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15081  532 
x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n" 
14738  533 
proof  
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

534 
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" 
14738  535 
by (rule_tac mult_right_mono,simp_all) 
536 
note est = this[simplified] 

22985  537 
let ?diff = "\<lambda>(n::nat) x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then sin(x) else cos(x)" 
538 
have diff_0: "?diff 0 = sin" by simp 

539 
have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x" 

540 
apply (clarify) 

541 
apply (subst (1 2 3) mod_Suc_eq_Suc_mod) 

542 
apply (cut_tac m=m in mod_exhaust_less_4) 

31881  543 
apply (safe, auto intro!: DERIV_intros) 
22985  544 
done 
545 
from Maclaurin_all_le [OF diff_0 DERIV_diff] 

546 
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and 

547 
t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) + 

548 
?diff n t / real (fact n) * x ^ n" by fast 

549 
have diff_m_0: 

550 
"\<And>m. ?diff m 0 = (if even m then 0 

23177  551 
else 1 ^ ((m  Suc 0) div 2))" 
22985  552 
apply (subst even_even_mod_4_iff) 
553 
apply (cut_tac m=m in mod_exhaust_less_4) 

554 
apply (elim disjE, simp_all) 

555 
apply (safe dest!: mod_eqD, simp_all) 

556 
done 

14738  557 
show ?thesis 
22985  558 
apply (subst t2) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

559 
apply (rule sin_bound_lemma) 
15536  560 
apply (rule setsum_cong[OF refl]) 
22985  561 
apply (subst diff_m_0, simp) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

562 
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15944
diff
changeset

563 
simp add: est mult_nonneg_nonneg mult_ac divide_inverse 
16924  564 
power_abs [symmetric] abs_mult) 
14738  565 
done 
566 
qed 

567 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

568 
end 