1 (* Title : MacLaurin.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2001 University of Edinburgh |
|
4 Description : MacLaurin series |
|
5 *) |
|
6 |
|
7 Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; |
|
8 by (induct_tac "n" 1); |
|
9 by Auto_tac; |
|
10 qed "sumr_offset"; |
|
11 |
|
12 Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; |
|
13 by (induct_tac "n" 1); |
|
14 by Auto_tac; |
|
15 qed "sumr_offset2"; |
|
16 |
|
17 Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; |
|
18 by (simp_tac (simpset() addsimps [sumr_offset]) 1); |
|
19 qed "sumr_offset3"; |
|
20 |
|
21 Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; |
|
22 by (simp_tac (simpset() addsimps [sumr_offset]) 1); |
|
23 qed "sumr_offset4"; |
|
24 |
|
25 Goal "0 < n ==> \ |
|
26 \ sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \ |
|
27 \ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \ |
|
28 \ sumr 0 (Suc n) (%n. (if even(n) then 0 else \ |
|
29 \ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"; |
|
30 by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1); |
|
31 by Auto_tac; |
|
32 qed "sumr_from_1_from_0"; |
|
33 |
|
34 (*---------------------------------------------------------------------------*) |
|
35 (* Maclaurin's theorem with Lagrange form of remainder *) |
|
36 (*---------------------------------------------------------------------------*) |
|
37 |
|
38 (* Annoying: Proof is now even longer due mostly to |
|
39 change in behaviour of simplifier since Isabelle99 *) |
|
40 Goal " [| 0 < h; 0 < n; diff 0 = f; \ |
|
41 \ ALL m t. \ |
|
42 \ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ |
|
43 \ ==> EX t. 0 < t & \ |
|
44 \ t < h & \ |
|
45 \ f h = \ |
|
46 \ sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \ |
|
47 \ (diff n t / real (fact n)) * h ^ n"; |
|
48 by (case_tac "n = 0" 1); |
|
49 by (Force_tac 1); |
|
50 by (dtac not0_implies_Suc 1); |
|
51 by (etac exE 1); |
|
52 by (subgoal_tac |
|
53 "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \ |
|
54 \ + (B * ((h ^ n) / real (fact n)))" 1); |
|
55 |
|
56 by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def, |
|
57 ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2); |
|
58 by (res_inst_tac |
|
59 [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \ |
|
60 \ * real (fact n) / (h ^ n)")] exI 2); |
|
61 by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2); |
|
62 by (rtac (CLAIM "x = (1::real) ==> a = a * (x::real)") 2); |
|
63 by (asm_simp_tac (HOL_ss addsimps |
|
64 [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"] |
|
65 delsimps [realpow_Suc]) 2); |
|
66 by (stac left_inverse 2); |
|
67 by (stac left_inverse 3); |
|
68 by (rtac (real_not_refl2 RS not_sym) 2); |
|
69 by (etac zero_less_power 2); |
|
70 by (rtac real_of_nat_fact_not_zero 2); |
|
71 by (Simp_tac 2); |
|
72 by (etac exE 1); |
|
73 by (cut_inst_tac [("b","%t. f t - \ |
|
74 \ (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \ |
|
75 \ (B * ((t ^ n) / real (fact n))))")] |
|
76 (CLAIM "EX g. g = b") 1); |
|
77 by (etac exE 1); |
|
78 by (subgoal_tac "g 0 = 0 & g h =0" 1); |
|
79 by (asm_simp_tac (simpset() addsimps |
|
80 [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"] |
|
81 delsimps [sumr_Suc]) 2); |
|
82 by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2); |
|
83 by (asm_full_simp_tac (simpset() addsimps |
|
84 [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"] |
|
85 delsimps [sumr_Suc]) 2); |
|
86 by (cut_inst_tac [("b","%m t. diff m t - \ |
|
87 \ (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \ |
|
88 \ + (B * ((t ^ (n - m)) / real (fact(n - m)))))")] |
|
89 (CLAIM "EX difg. difg = b") 1); |
|
90 by (etac exE 1); |
|
91 by (subgoal_tac "difg 0 = g" 1); |
|
92 by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2); |
|
93 by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \ |
|
94 \ DERIV (difg m) t :> difg (Suc m) t" 1); |
|
95 by (Clarify_tac 2); |
|
96 by (rtac DERIV_diff 2); |
|
97 by (Asm_simp_tac 2); |
|
98 by DERIV_tac; |
|
99 by DERIV_tac; |
|
100 by (rtac lemma_DERIV_subst 3); |
|
101 by (rtac DERIV_quotient 3); |
|
102 by (rtac DERIV_const 4); |
|
103 by (rtac DERIV_pow 3); |
|
104 by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib, |
|
105 CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" |
|
106 mult_ac,fact_diff_Suc]) 4); |
|
107 by (Asm_simp_tac 3); |
|
108 by (forw_inst_tac [("m","ma")] less_add_one 2); |
|
109 by (Clarify_tac 2); |
|
110 by (asm_simp_tac (simpset() addsimps |
|
111 [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"] |
|
112 delsimps [sumr_Suc]) 2); |
|
113 by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) |
|
114 (read_instantiate [("k","1")] sumr_offset4))] |
|
115 delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); |
|
116 by (rtac lemma_DERIV_subst 2); |
|
117 by (rtac DERIV_add 2); |
|
118 by (rtac DERIV_const 3); |
|
119 by (rtac DERIV_sumr 2); |
|
120 by (Clarify_tac 2); |
|
121 by (Simp_tac 3); |
|
122 by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc] |
|
123 delsimps [fact_Suc,realpow_Suc]) 2); |
|
124 by (rtac DERIV_cmult 2); |
|
125 by (rtac lemma_DERIV_subst 2); |
|
126 by DERIV_tac; |
|
127 by (stac fact_Suc 2); |
|
128 by (stac real_of_nat_mult 2); |
|
129 by (simp_tac (simpset() addsimps [inverse_mult_distrib] @ |
|
130 mult_ac) 2); |
|
131 by (subgoal_tac "ALL ma. ma < n --> \ |
|
132 \ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1); |
|
133 by (rotate_tac 11 1); |
|
134 by (dres_inst_tac [("x","m")] spec 1); |
|
135 by (etac impE 1); |
|
136 by (Asm_simp_tac 1); |
|
137 by (etac exE 1); |
|
138 by (res_inst_tac [("x","t")] exI 1); |
|
139 by (asm_full_simp_tac (simpset() addsimps |
|
140 [ARITH_PROVE "(x - y = 0) = (y = (x::real))"] |
|
141 delsimps [realpow_Suc,fact_Suc]) 1); |
|
142 by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1); |
|
143 by (Clarify_tac 2); |
|
144 by (Asm_simp_tac 2); |
|
145 by (forw_inst_tac [("m","ma")] less_add_one 2); |
|
146 by (Clarify_tac 2); |
|
147 by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2); |
|
148 by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) |
|
149 (read_instantiate [("k","1")] sumr_offset4))] |
|
150 delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); |
|
151 by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \ |
|
152 \ DERIV (difg m) t :> 0)" 1); |
|
153 by (rtac allI 1 THEN rtac impI 1); |
|
154 by (rotate_tac 12 1); |
|
155 by (dres_inst_tac [("x","ma")] spec 1); |
|
156 by (etac impE 1 THEN assume_tac 1); |
|
157 by (etac exE 1); |
|
158 by (res_inst_tac [("x","t")] exI 1); |
|
159 (* do some tidying up *) |
|
160 by (ALLGOALS(thin_tac "difg = \ |
|
161 \ (%m t. diff m t - \ |
|
162 \ (sumr 0 (n - m) \ |
|
163 \ (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \ |
|
164 \ B * (t ^ (n - m) / real (fact (n - m)))))")); |
|
165 by (ALLGOALS(thin_tac "g = \ |
|
166 \ (%t. f t - \ |
|
167 \ (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + \ |
|
168 \ B * (t ^ n / real (fact n))))")); |
|
169 by (ALLGOALS(thin_tac "f h = \ |
|
170 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
171 \ B * (h ^ n / real (fact n))")); |
|
172 (* back to business *) |
|
173 by (Asm_simp_tac 1); |
|
174 by (rtac DERIV_unique 1); |
|
175 by (Blast_tac 2); |
|
176 by (Force_tac 1); |
|
177 by (rtac allI 1 THEN induct_tac "ma" 1); |
|
178 by (rtac impI 1 THEN rtac Rolle 1); |
|
179 by (assume_tac 1); |
|
180 by (Asm_full_simp_tac 1); |
|
181 by (Asm_full_simp_tac 1); |
|
182 by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1); |
|
183 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
|
184 by (blast_tac (claset() addDs [DERIV_isCont]) 1); |
|
185 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
|
186 by (Clarify_tac 1); |
|
187 by (res_inst_tac [("x","difg (Suc 0) t")] exI 1); |
|
188 by (Force_tac 1); |
|
189 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
|
190 by (Clarify_tac 1); |
|
191 by (res_inst_tac [("x","difg (Suc 0) x")] exI 1); |
|
192 by (Force_tac 1); |
|
193 by (Step_tac 1); |
|
194 by (Force_tac 1); |
|
195 by (subgoal_tac "EX ta. 0 < ta & ta < t & \ |
|
196 \ DERIV difg (Suc n) ta :> 0" 1); |
|
197 by (rtac Rolle 2 THEN assume_tac 2); |
|
198 by (Asm_full_simp_tac 2); |
|
199 by (rotate_tac 2 2); |
|
200 by (dres_inst_tac [("x","n")] spec 2); |
|
201 by (ftac (ARITH_PROVE "n < m ==> n < Suc m") 2); |
|
202 by (rtac DERIV_unique 2); |
|
203 by (assume_tac 3); |
|
204 by (Force_tac 2); |
|
205 by (subgoal_tac |
|
206 "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2); |
|
207 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); |
|
208 by (blast_tac (claset() addSDs [DERIV_isCont]) 2); |
|
209 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); |
|
210 by (Clarify_tac 2); |
|
211 by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2); |
|
212 by (Force_tac 2); |
|
213 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); |
|
214 by (Clarify_tac 2); |
|
215 by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2); |
|
216 by (Force_tac 2); |
|
217 by (Step_tac 1); |
|
218 by (res_inst_tac [("x","ta")] exI 1); |
|
219 by (Force_tac 1); |
|
220 qed "Maclaurin"; |
|
221 |
|
222 Goal "0 < h & 0 < n & diff 0 = f & \ |
|
223 \ (ALL m t. \ |
|
224 \ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ |
|
225 \ --> (EX t. 0 < t & \ |
|
226 \ t < h & \ |
|
227 \ f h = \ |
|
228 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
229 \ diff n t / real (fact n) * h ^ n)"; |
|
230 by (blast_tac (claset() addIs [Maclaurin]) 1); |
|
231 qed "Maclaurin_objl"; |
|
232 |
|
233 Goal " [| 0 < h; diff 0 = f; \ |
|
234 \ ALL m t. \ |
|
235 \ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ |
|
236 \ ==> EX t. 0 < t & \ |
|
237 \ t <= h & \ |
|
238 \ f h = \ |
|
239 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
240 \ diff n t / real (fact n) * h ^ n"; |
|
241 by (case_tac "n" 1); |
|
242 by Auto_tac; |
|
243 by (dtac Maclaurin 1 THEN Auto_tac); |
|
244 qed "Maclaurin2"; |
|
245 |
|
246 Goal "0 < h & diff 0 = f & \ |
|
247 \ (ALL m t. \ |
|
248 \ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ |
|
249 \ --> (EX t. 0 < t & \ |
|
250 \ t <= h & \ |
|
251 \ f h = \ |
|
252 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
253 \ diff n t / real (fact n) * h ^ n)"; |
|
254 by (blast_tac (claset() addIs [Maclaurin2]) 1); |
|
255 qed "Maclaurin2_objl"; |
|
256 |
|
257 Goal " [| h < 0; 0 < n; diff 0 = f; \ |
|
258 \ ALL m t. \ |
|
259 \ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \ |
|
260 \ ==> EX t. h < t & \ |
|
261 \ t < 0 & \ |
|
262 \ f h = \ |
|
263 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
264 \ diff n t / real (fact n) * h ^ n"; |
|
265 by (cut_inst_tac [("f","%x. f (-x)"), |
|
266 ("diff","%n x. ((- 1) ^ n) * diff n (-x)"), |
|
267 ("h","-h"),("n","n")] Maclaurin_objl 1); |
|
268 by (Asm_full_simp_tac 1); |
|
269 by (etac impE 1 THEN Step_tac 1); |
|
270 by (stac minus_mult_right 1); |
|
271 by (rtac DERIV_cmult 1); |
|
272 by (rtac lemma_DERIV_subst 1); |
|
273 by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1); |
|
274 by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2); |
|
275 by (Force_tac 2); |
|
276 by (Force_tac 1); |
|
277 by (res_inst_tac [("x","-t")] exI 1); |
|
278 by Auto_tac; |
|
279 by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1); |
|
280 by (rtac sumr_fun_eq 1); |
|
281 by (Asm_full_simp_tac 1); |
|
282 by (auto_tac (claset(),simpset() addsimps [real_divide_def, |
|
283 CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))", |
|
284 power_mult_distrib RS sym])); |
|
285 qed "Maclaurin_minus"; |
|
286 |
|
287 Goal "(h < 0 & 0 < n & diff 0 = f & \ |
|
288 \ (ALL m t. \ |
|
289 \ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\ |
|
290 \ --> (EX t. h < t & \ |
|
291 \ t < 0 & \ |
|
292 \ f h = \ |
|
293 \ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ |
|
294 \ diff n t / real (fact n) * h ^ n)"; |
|
295 by (blast_tac (claset() addIs [Maclaurin_minus]) 1); |
|
296 qed "Maclaurin_minus_objl"; |
|
297 |
|
298 (* ------------------------------------------------------------------------- *) |
|
299 (* More convenient "bidirectional" version. *) |
|
300 (* ------------------------------------------------------------------------- *) |
|
301 |
|
302 (* not good for PVS sin_approx, cos_approx *) |
|
303 Goal " [| diff 0 = f; \ |
|
304 \ ALL m t. \ |
|
305 \ m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \ |
|
306 \ ==> EX t. abs t <= abs x & \ |
|
307 \ f x = \ |
|
308 \ sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \ |
|
309 \ diff n t / real (fact n) * x ^ n"; |
|
310 by (case_tac "n = 0" 1); |
|
311 by (Force_tac 1); |
|
312 by (case_tac "x = 0" 1); |
|
313 by (res_inst_tac [("x","0")] exI 1); |
|
314 by (Asm_full_simp_tac 1); |
|
315 by (res_inst_tac [("P","0 < n")] impE 1); |
|
316 by (assume_tac 2 THEN assume_tac 2); |
|
317 by (induct_tac "n" 1); |
|
318 by (Simp_tac 1); |
|
319 by Auto_tac; |
|
320 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
|
321 by Auto_tac; |
|
322 by (cut_inst_tac [("f","diff 0"), |
|
323 ("diff","diff"), |
|
324 ("h","x"),("n","n")] Maclaurin_objl 2); |
|
325 by (Step_tac 2); |
|
326 by (blast_tac (claset() addDs |
|
327 [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2); |
|
328 by (res_inst_tac [("x","t")] exI 2); |
|
329 by (force_tac (claset() addIs |
|
330 [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2); |
|
331 by (cut_inst_tac [("f","diff 0"), |
|
332 ("diff","diff"), |
|
333 ("h","x"),("n","n")] Maclaurin_minus_objl 1); |
|
334 by (Step_tac 1); |
|
335 by (blast_tac (claset() addDs |
|
336 [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1); |
|
337 by (res_inst_tac [("x","t")] exI 1); |
|
338 by (force_tac (claset() addIs |
|
339 [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1); |
|
340 qed "Maclaurin_bi_le"; |
|
341 |
|
342 Goal "[| diff 0 = f; \ |
|
343 \ ALL m x. DERIV (diff m) x :> diff(Suc m) x; \ |
|
344 \ x ~= 0; 0 < n \ |
|
345 \ |] ==> EX t. 0 < abs t & abs t < abs x & \ |
|
346 \ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ |
|
347 \ (diff n t / real (fact n)) * x ^ n"; |
|
348 by (res_inst_tac [("x","x"),("y","0")] linorder_cases 1); |
|
349 by (Blast_tac 2); |
|
350 by (dtac Maclaurin_minus 1); |
|
351 by (dtac Maclaurin 5); |
|
352 by (TRYALL(assume_tac)); |
|
353 by (Blast_tac 1); |
|
354 by (Blast_tac 2); |
|
355 by (Step_tac 1); |
|
356 by (ALLGOALS(res_inst_tac [("x","t")] exI)); |
|
357 by (Step_tac 1); |
|
358 by (ALLGOALS(arith_tac)); |
|
359 qed "Maclaurin_all_lt"; |
|
360 |
|
361 Goal "diff 0 = f & \ |
|
362 \ (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \ |
|
363 \ x ~= 0 & 0 < n \ |
|
364 \ --> (EX t. 0 < abs t & abs t < abs x & \ |
|
365 \ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ |
|
366 \ (diff n t / real (fact n)) * x ^ n)"; |
|
367 by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1); |
|
368 qed "Maclaurin_all_lt_objl"; |
|
369 |
|
370 Goal "x = (0::real) \ |
|
371 \ ==> 0 < n --> \ |
|
372 \ sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \ |
|
373 \ diff 0 0"; |
|
374 by (Asm_simp_tac 1); |
|
375 by (induct_tac "n" 1); |
|
376 by Auto_tac; |
|
377 qed_spec_mp "Maclaurin_zero"; |
|
378 |
|
379 Goal "[| diff 0 = f; \ |
|
380 \ ALL m x. DERIV (diff m) x :> diff (Suc m) x \ |
|
381 \ |] ==> EX t. abs t <= abs x & \ |
|
382 \ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ |
|
383 \ (diff n t / real (fact n)) * x ^ n"; |
|
384 by (cut_inst_tac [("n","n"),("m","0")] |
|
385 (ARITH_PROVE "n <= m | m < (n::nat)") 1); |
|
386 by (etac disjE 1); |
|
387 by (Force_tac 1); |
|
388 by (case_tac "x = 0" 1); |
|
389 by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1); |
|
390 by (assume_tac 1); |
|
391 by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); |
|
392 by (res_inst_tac [("x","0")] exI 1); |
|
393 by (Force_tac 1); |
|
394 by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1); |
|
395 by (TRYALL(assume_tac)); |
|
396 by (Step_tac 1); |
|
397 by (res_inst_tac [("x","t")] exI 1); |
|
398 by Auto_tac; |
|
399 qed "Maclaurin_all_le"; |
|
400 |
|
401 Goal "diff 0 = f & \ |
|
402 \ (ALL m x. DERIV (diff m) x :> diff (Suc m) x) \ |
|
403 \ --> (EX t. abs t <= abs x & \ |
|
404 \ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ |
|
405 \ (diff n t / real (fact n)) * x ^ n)"; |
|
406 by (blast_tac (claset() addIs [Maclaurin_all_le]) 1); |
|
407 qed "Maclaurin_all_le_objl"; |
|
408 |
|
409 (* ------------------------------------------------------------------------- *) |
|
410 (* Version for exp. *) |
|
411 (* ------------------------------------------------------------------------- *) |
|
412 |
|
413 Goal "[| x ~= 0; 0 < n |] \ |
|
414 \ ==> (EX t. 0 < abs t & \ |
|
415 \ abs t < abs x & \ |
|
416 \ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ |
|
417 \ (exp t / real (fact n)) * x ^ n)"; |
|
418 by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] |
|
419 Maclaurin_all_lt_objl 1); |
|
420 by Auto_tac; |
|
421 qed "Maclaurin_exp_lt"; |
|
422 |
|
423 Goal "EX t. abs t <= abs x & \ |
|
424 \ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ |
|
425 \ (exp t / real (fact n)) * x ^ n"; |
|
426 by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] |
|
427 Maclaurin_all_le_objl 1); |
|
428 by Auto_tac; |
|
429 qed "Maclaurin_exp_le"; |
|
430 |
|
431 (* ------------------------------------------------------------------------- *) |
|
432 (* Version for sin function *) |
|
433 (* ------------------------------------------------------------------------- *) |
|
434 |
|
435 Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \ |
|
436 \ ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))"; |
|
437 by (dtac MVT 1); |
|
438 by (blast_tac (claset() addIs [DERIV_isCont]) 1); |
|
439 by (force_tac (claset() addDs [order_less_imp_le], |
|
440 simpset() addsimps [differentiable_def]) 1); |
|
441 by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1); |
|
442 qed "MVT2"; |
|
443 |
|
444 Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3"; |
|
445 by (case_tac "d" 1 THEN Auto_tac); |
|
446 qed "lemma_exhaust_less_4"; |
|
447 |
|
448 bind_thm ("real_mult_le_lemma", |
|
449 simplify (simpset()) (inst "b" "1" mult_right_mono)); |
|
450 |
|
451 |
|
452 Goal "abs(sin x - \ |
|
453 \ sumr 0 n (%m. (if even m then 0 \ |
|
454 \ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ |
|
455 \ x ^ m)) \ |
|
456 \ <= inverse(real (fact n)) * abs(x) ^ n"; |
|
457 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), |
|
458 ("diff","%n x. if n mod 4 = 0 then sin(x) \ |
|
459 \ else if n mod 4 = 1 then cos(x) \ |
|
460 \ else if n mod 4 = 2 then -sin(x) \ |
|
461 \ else -cos(x)")] Maclaurin_all_le_objl 1); |
|
462 by (Step_tac 1); |
|
463 by (Asm_full_simp_tac 1); |
|
464 by (stac mod_Suc_eq_Suc_mod 1); |
|
465 by (cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor |
|
466 RS lemma_exhaust_less_4) 1); |
|
467 by (Step_tac 1); |
|
468 by (Asm_simp_tac 1); |
|
469 by (Asm_simp_tac 1); |
|
470 by (Asm_simp_tac 1); |
|
471 by (rtac DERIV_minus 1 THEN Simp_tac 1); |
|
472 by (Asm_simp_tac 1); |
|
473 by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_minus 1 THEN rtac DERIV_cos 1); |
|
474 by (Simp_tac 1); |
|
475 by (dtac ssubst 1 THEN assume_tac 2); |
|
476 by (rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1); |
|
477 by (rtac sumr_fun_eq 1); |
|
478 by (Step_tac 1); |
|
479 by (rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1); |
|
480 by (stac even_even_mod_4_iff 1); |
|
481 by (cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor |
|
482 RS lemma_exhaust_less_4) 1); |
|
483 by (Step_tac 1); |
|
484 by (Asm_simp_tac 1); |
|
485 by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2); |
|
486 by (asm_simp_tac (simpset() addsimps [even_num_iff]) 1); |
|
487 by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2); |
|
488 by (dtac lemma_even_mod_4_div_2 1); |
|
489 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1); |
|
490 by (dtac lemma_odd_mod_4_div_2 1); |
|
491 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1); |
|
492 by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono], |
|
493 simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS |
|
494 sym])); |
|
495 qed "Maclaurin_sin_bound"; |
|
496 |
|
497 Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"; |
|
498 by (induct_tac "n" 1); |
|
499 by Auto_tac; |
|
500 qed_spec_mp "Suc_Suc_mult_two_diff_two"; |
|
501 Addsimps [Suc_Suc_mult_two_diff_two]; |
|
502 |
|
503 Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n"; |
|
504 by (induct_tac "n" 1); |
|
505 by Auto_tac; |
|
506 qed_spec_mp "lemma_Suc_Suc_4n_diff_2"; |
|
507 Addsimps [lemma_Suc_Suc_4n_diff_2]; |
|
508 |
|
509 Goal "0 < n --> Suc (2 * n - 1) = 2*n"; |
|
510 by (induct_tac "n" 1); |
|
511 by Auto_tac; |
|
512 qed_spec_mp "Suc_mult_two_diff_one"; |
|
513 Addsimps [Suc_mult_two_diff_one]; |
|
514 |
|
515 Goal "EX t. sin x = \ |
|
516 \ (sumr 0 n (%m. (if even m then 0 \ |
|
517 \ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ |
|
518 \ x ^ m)) \ |
|
519 \ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
520 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), |
|
521 ("diff","%n x. sin(x + 1/2*real (n)*pi)")] |
|
522 Maclaurin_all_lt_objl 1); |
|
523 by (Safe_tac); |
|
524 by (Simp_tac 1); |
|
525 by (Simp_tac 1); |
|
526 by (case_tac "n" 1); |
|
527 by (Clarify_tac 1); |
|
528 by (Asm_full_simp_tac 1); |
|
529 by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1); |
|
530 by (Asm_full_simp_tac 1); |
|
531 by (rtac ccontr 1); |
|
532 by (Asm_full_simp_tac 1); |
|
533 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); |
|
534 by (dtac ssubst 1 THEN assume_tac 2); |
|
535 by (res_inst_tac [("x","t")] exI 1); |
|
536 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
537 by (rtac sumr_fun_eq 1); |
|
538 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
539 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); |
|
540 (*Could sin_zero_iff help?*) |
|
541 qed "Maclaurin_sin_expansion"; |
|
542 |
|
543 Goal "EX t. abs t <= abs x & \ |
|
544 \ sin x = \ |
|
545 \ (sumr 0 n (%m. (if even m then 0 \ |
|
546 \ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ |
|
547 \ x ^ m)) \ |
|
548 \ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
549 |
|
550 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), |
|
551 ("diff","%n x. sin(x + 1/2*real (n)*pi)")] |
|
552 Maclaurin_all_lt_objl 1); |
|
553 by (Step_tac 1); |
|
554 by (Simp_tac 1); |
|
555 by (Simp_tac 1); |
|
556 by (case_tac "n" 1); |
|
557 by (Clarify_tac 1); |
|
558 by (Asm_full_simp_tac 1); |
|
559 by (Asm_full_simp_tac 1); |
|
560 by (rtac ccontr 1); |
|
561 by (Asm_full_simp_tac 1); |
|
562 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); |
|
563 by (dtac ssubst 1 THEN assume_tac 2); |
|
564 by (res_inst_tac [("x","t")] exI 1); |
|
565 by (rtac conjI 1); |
|
566 by (arith_tac 1); |
|
567 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
568 by (rtac sumr_fun_eq 1); |
|
569 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
570 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); |
|
571 qed "Maclaurin_sin_expansion2"; |
|
572 |
|
573 Goal "[| 0 < n; 0 < x |] ==> \ |
|
574 \ EX t. 0 < t & t < x & \ |
|
575 \ sin x = \ |
|
576 \ (sumr 0 n (%m. (if even m then 0 \ |
|
577 \ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ |
|
578 \ x ^ m)) \ |
|
579 \ + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"; |
|
580 by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), |
|
581 ("diff","%n x. sin(x + 1/2*real (n)*pi)")] |
|
582 Maclaurin_objl 1); |
|
583 by (Step_tac 1); |
|
584 by (Asm_full_simp_tac 1); |
|
585 by (Simp_tac 1); |
|
586 by (dtac ssubst 1 THEN assume_tac 2); |
|
587 by (res_inst_tac [("x","t")] exI 1); |
|
588 by (rtac conjI 1 THEN rtac conjI 2); |
|
589 by (assume_tac 1 THEN assume_tac 1); |
|
590 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
591 by (rtac sumr_fun_eq 1); |
|
592 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
593 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); |
|
594 qed "Maclaurin_sin_expansion3"; |
|
595 |
|
596 Goal "0 < x ==> \ |
|
597 \ EX t. 0 < t & t <= x & \ |
|
598 \ sin x = \ |
|
599 \ (sumr 0 n (%m. (if even m then 0 \ |
|
600 \ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ |
|
601 \ x ^ m)) \ |
|
602 \ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
603 by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), |
|
604 ("diff","%n x. sin(x + 1/2*real (n)*pi)")] |
|
605 Maclaurin2_objl 1); |
|
606 by (Step_tac 1); |
|
607 by (Asm_full_simp_tac 1); |
|
608 by (Simp_tac 1); |
|
609 by (dtac ssubst 1 THEN assume_tac 2); |
|
610 by (res_inst_tac [("x","t")] exI 1); |
|
611 by (rtac conjI 1 THEN rtac conjI 2); |
|
612 by (assume_tac 1 THEN assume_tac 1); |
|
613 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
614 by (rtac sumr_fun_eq 1); |
|
615 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
616 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); |
|
617 qed "Maclaurin_sin_expansion4"; |
|
618 |
|
619 (*-----------------------------------------------------------------------------*) |
|
620 (* Maclaurin expansion for cos *) |
|
621 (*-----------------------------------------------------------------------------*) |
|
622 |
|
623 Goal "sumr 0 (Suc n) \ |
|
624 \ (%m. (if even m \ |
|
625 \ then (- 1) ^ (m div 2)/(real (fact m)) \ |
|
626 \ else 0) * \ |
|
627 \ 0 ^ m) = 1"; |
|
628 by (induct_tac "n" 1); |
|
629 by Auto_tac; |
|
630 qed "sumr_cos_zero_one"; |
|
631 Addsimps [sumr_cos_zero_one]; |
|
632 |
|
633 Goal "EX t. abs t <= abs x & \ |
|
634 \ cos x = \ |
|
635 \ (sumr 0 n (%m. (if even m \ |
|
636 \ then (- 1) ^ (m div 2)/(real (fact m)) \ |
|
637 \ else 0) * \ |
|
638 \ x ^ m)) \ |
|
639 \ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
640 by (cut_inst_tac [("f","cos"),("n","n"),("x","x"), |
|
641 ("diff","%n x. cos(x + 1/2*real (n)*pi)")] |
|
642 Maclaurin_all_lt_objl 1); |
|
643 by (Step_tac 1); |
|
644 by (Simp_tac 1); |
|
645 by (Simp_tac 1); |
|
646 by (case_tac "n" 1); |
|
647 by (Asm_full_simp_tac 1); |
|
648 by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1); |
|
649 by (rtac ccontr 1); |
|
650 by (Asm_full_simp_tac 1); |
|
651 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); |
|
652 by (dtac ssubst 1 THEN assume_tac 2); |
|
653 by (res_inst_tac [("x","t")] exI 1); |
|
654 by (rtac conjI 1); |
|
655 by (arith_tac 1); |
|
656 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
657 by (rtac sumr_fun_eq 1); |
|
658 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
659 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps |
|
660 [fact_Suc,realpow_Suc])); |
|
661 by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); |
|
662 qed "Maclaurin_cos_expansion"; |
|
663 |
|
664 Goal "[| 0 < x; 0 < n |] ==> \ |
|
665 \ EX t. 0 < t & t < x & \ |
|
666 \ cos x = \ |
|
667 \ (sumr 0 n (%m. (if even m \ |
|
668 \ then (- 1) ^ (m div 2)/(real (fact m)) \ |
|
669 \ else 0) * \ |
|
670 \ x ^ m)) \ |
|
671 \ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
672 by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), |
|
673 ("diff","%n x. cos(x + 1/2*real (n)*pi)")] |
|
674 Maclaurin_objl 1); |
|
675 by (Step_tac 1); |
|
676 by (Asm_full_simp_tac 1); |
|
677 by (Simp_tac 1); |
|
678 by (dtac ssubst 1 THEN assume_tac 2); |
|
679 by (res_inst_tac [("x","t")] exI 1); |
|
680 by (rtac conjI 1 THEN rtac conjI 2); |
|
681 by (assume_tac 1 THEN assume_tac 1); |
|
682 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
683 by (rtac sumr_fun_eq 1); |
|
684 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
685 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); |
|
686 by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); |
|
687 qed "Maclaurin_cos_expansion2"; |
|
688 |
|
689 Goal "[| x < 0; 0 < n |] ==> \ |
|
690 \ EX t. x < t & t < 0 & \ |
|
691 \ cos x = \ |
|
692 \ (sumr 0 n (%m. (if even m \ |
|
693 \ then (- 1) ^ (m div 2)/(real (fact m)) \ |
|
694 \ else 0) * \ |
|
695 \ x ^ m)) \ |
|
696 \ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; |
|
697 by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), |
|
698 ("diff","%n x. cos(x + 1/2*real (n)*pi)")] |
|
699 Maclaurin_minus_objl 1); |
|
700 by (Step_tac 1); |
|
701 by (Asm_full_simp_tac 1); |
|
702 by (Simp_tac 1); |
|
703 by (dtac ssubst 1 THEN assume_tac 2); |
|
704 by (res_inst_tac [("x","t")] exI 1); |
|
705 by (rtac conjI 1 THEN rtac conjI 2); |
|
706 by (assume_tac 1 THEN assume_tac 1); |
|
707 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); |
|
708 by (rtac sumr_fun_eq 1); |
|
709 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); |
|
710 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); |
|
711 by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); |
|
712 qed "Maclaurin_minus_cos_expansion"; |
|
713 |
|
714 (* ------------------------------------------------------------------------- *) |
|
715 (* Version for ln(1 +/- x). Where is it?? *) |
|
716 (* ------------------------------------------------------------------------- *) |
|
717 |
|