|
1 (* Title : CLim.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2001 University of Edinburgh |
|
4 Description : A first theory of limits, continuity and |
|
5 differentiation for complex functions |
|
6 *) |
|
7 |
|
8 (*------------------------------------------------------------------------------------*) |
|
9 (* Limit of complex to complex function *) |
|
10 (*------------------------------------------------------------------------------------*) |
|
11 |
|
12 Goalw [NSCLIM_def,NSCRLIM_def] |
|
13 "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"; |
|
14 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
15 by (auto_tac (claset(),simpset() addsimps [starfunC_approx_Re_Im_iff, |
|
16 hRe_hcomplex_of_complex])); |
|
17 qed "NSCLIM_NSCRLIM_Re"; |
|
18 |
|
19 Goalw [NSCLIM_def,NSCRLIM_def] |
|
20 "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"; |
|
21 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
22 by (auto_tac (claset(),simpset() addsimps [starfunC_approx_Re_Im_iff, |
|
23 hIm_hcomplex_of_complex])); |
|
24 qed "NSCLIM_NSCRLIM_Im"; |
|
25 |
|
26 Goalw [CLIM_def,NSCLIM_def,capprox_def] |
|
27 "f -- x --C> L ==> f -- x --NSC> L"; |
|
28 by Auto_tac; |
|
29 by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); |
|
30 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_def, |
|
31 starfunC,hcomplex_diff,CInfinitesimal_hcmod_iff,hcmod, |
|
32 Infinitesimal_FreeUltrafilterNat_iff])); |
|
33 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); |
|
34 by (Step_tac 1); |
|
35 by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac); |
|
36 by (dres_inst_tac [("x","s")] spec 1 THEN Auto_tac); |
|
37 by (Ultra_tac 1); |
|
38 by (dtac sym 1 THEN Auto_tac); |
|
39 qed "CLIM_NSCLIM"; |
|
40 |
|
41 Goal "(ALL t. P t) = (ALL X. P (Abs_hcomplex(hcomplexrel `` {X})))"; |
|
42 by Auto_tac; |
|
43 by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1); |
|
44 by Auto_tac; |
|
45 qed "eq_Abs_hcomplex_ALL"; |
|
46 |
|
47 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
|
48 \ cmod (xa - x) < s & r <= cmod (f xa - L)) \ |
|
49 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
|
50 \ cmod(xa - x) < inverse(real(Suc n)) & r <= cmod(f xa - L)"; |
|
51 by (Clarify_tac 1); |
|
52 by (cut_inst_tac [("n1","n")] |
|
53 (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); |
|
54 by Auto_tac; |
|
55 val lemma_CLIM = result(); |
|
56 |
|
57 (* not needed? *) |
|
58 Goal "ALL x z. EX y. Q x z y ==> EX f. ALL x z. Q x z (f x z)"; |
|
59 by (rtac choice 1 THEN Step_tac 1); |
|
60 by (blast_tac (claset() addIs [choice]) 1); |
|
61 qed "choice2"; |
|
62 |
|
63 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
|
64 \ cmod (xa - x) < s & r <= cmod (f xa - L)) \ |
|
65 \ ==> EX X. ALL (n::nat). X n ~= x & \ |
|
66 \ cmod(X n - x) < inverse(real(Suc n)) & r <= cmod(f (X n) - L)"; |
|
67 by (dtac lemma_CLIM 1); |
|
68 by (dtac choice 1); |
|
69 by (Blast_tac 1); |
|
70 val lemma_skolemize_CLIM2 = result(); |
|
71 |
|
72 Goal "ALL n. X n ~= x & \ |
|
73 \ cmod (X n - x) < inverse (real(Suc n)) & \ |
|
74 \ r <= cmod (f (X n) - L) ==> \ |
|
75 \ ALL n. cmod (X n - x) < inverse (real(Suc n))"; |
|
76 by (Auto_tac ); |
|
77 val lemma_csimp = result(); |
|
78 |
|
79 Goalw [CLIM_def,NSCLIM_def] |
|
80 "f -- x --NSC> L ==> f -- x --C> L"; |
|
81 by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL, |
|
82 starfunC,CInfinitesimal_capprox_minus RS sym,hcomplex_diff, |
|
83 CInfinitesimal_hcmod_iff,hcomplex_of_complex_def, |
|
84 Infinitesimal_FreeUltrafilterNat_iff,hcmod])); |
|
85 by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
|
86 by (fold_tac [real_le_def]); |
|
87 by (dtac lemma_skolemize_CLIM2 1); |
|
88 by (Step_tac 1); |
|
89 by (dres_inst_tac [("x","X")] spec 1); |
|
90 by Auto_tac; |
|
91 by (dtac (lemma_csimp RS complex_seq_to_hcomplex_CInfinitesimal) 1); |
|
92 by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff, |
|
93 hcomplex_of_complex_def,Infinitesimal_FreeUltrafilterNat_iff, |
|
94 hcomplex_diff,hcmod]) 1); |
|
95 by (Blast_tac 1); |
|
96 by (dres_inst_tac [("x","r")] spec 1); |
|
97 by (Clarify_tac 1); |
|
98 by (dtac FreeUltrafilterNat_all 1); |
|
99 by (Ultra_tac 1); |
|
100 by (arith_tac 1); |
|
101 qed "NSCLIM_CLIM"; |
|
102 |
|
103 (**** First key result ****) |
|
104 |
|
105 Goal "(f -- x --C> L) = (f -- x --NSC> L)"; |
|
106 by (blast_tac (claset() addIs [CLIM_NSCLIM,NSCLIM_CLIM]) 1); |
|
107 qed "CLIM_NSCLIM_iff"; |
|
108 |
|
109 (*------------------------------------------------------------------------------------*) |
|
110 (* Limit of complex to real function *) |
|
111 (*------------------------------------------------------------------------------------*) |
|
112 |
|
113 Goalw [CRLIM_def,NSCRLIM_def,capprox_def] |
|
114 "f -- x --CR> L ==> f -- x --NSCR> L"; |
|
115 by Auto_tac; |
|
116 by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); |
|
117 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_def, |
|
118 starfunCR,hcomplex_diff,CInfinitesimal_hcmod_iff,hcmod,hypreal_diff, |
|
119 Infinitesimal_FreeUltrafilterNat_iff,Infinitesimal_approx_minus RS sym, |
|
120 hypreal_of_real_def])); |
|
121 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); |
|
122 by (Step_tac 1); |
|
123 by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac); |
|
124 by (dres_inst_tac [("x","s")] spec 1 THEN Auto_tac); |
|
125 by (Ultra_tac 1); |
|
126 by (dtac sym 1 THEN Auto_tac); |
|
127 qed "CRLIM_NSCRLIM"; |
|
128 |
|
129 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
|
130 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |
|
131 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
|
132 \ cmod(xa - x) < inverse(real(Suc n)) & r <= abs (f xa - L)"; |
|
133 by (Clarify_tac 1); |
|
134 by (cut_inst_tac [("n1","n")] |
|
135 (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); |
|
136 by Auto_tac; |
|
137 val lemma_CRLIM = result(); |
|
138 |
|
139 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
|
140 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |
|
141 \ ==> EX X. ALL (n::nat). X n ~= x & \ |
|
142 \ cmod(X n - x) < inverse(real(Suc n)) & r <= abs (f (X n) - L)"; |
|
143 by (dtac lemma_CRLIM 1); |
|
144 by (dtac choice 1); |
|
145 by (Blast_tac 1); |
|
146 val lemma_skolemize_CRLIM2 = result(); |
|
147 |
|
148 Goal "ALL n. X n ~= x & \ |
|
149 \ cmod (X n - x) < inverse (real(Suc n)) & \ |
|
150 \ r <= abs (f (X n) - L) ==> \ |
|
151 \ ALL n. cmod (X n - x) < inverse (real(Suc n))"; |
|
152 by (Auto_tac ); |
|
153 val lemma_crsimp = result(); |
|
154 |
|
155 Goalw [CRLIM_def,NSCRLIM_def,capprox_def] |
|
156 "f -- x --NSCR> L ==> f -- x --CR> L"; |
|
157 by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL, |
|
158 starfunCR,hcomplex_diff,hcomplex_of_complex_def,hypreal_diff, |
|
159 CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_approx_minus RS sym, |
|
160 Infinitesimal_FreeUltrafilterNat_iff])); |
|
161 by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
|
162 by (fold_tac [real_le_def]); |
|
163 by (dtac lemma_skolemize_CRLIM2 1); |
|
164 by (Step_tac 1); |
|
165 by (dres_inst_tac [("x","X")] spec 1); |
|
166 by Auto_tac; |
|
167 by (dtac (lemma_crsimp RS complex_seq_to_hcomplex_CInfinitesimal) 1); |
|
168 by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff, |
|
169 hcomplex_of_complex_def,Infinitesimal_FreeUltrafilterNat_iff, |
|
170 hcomplex_diff,hcmod]) 1); |
|
171 by (Blast_tac 1); |
|
172 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, |
|
173 hypreal_diff])); |
|
174 by (dres_inst_tac [("x","r")] spec 1); |
|
175 by (Clarify_tac 1); |
|
176 by (dtac FreeUltrafilterNat_all 1); |
|
177 by (Ultra_tac 1); |
|
178 qed "NSCRLIM_CRLIM"; |
|
179 |
|
180 (** second key result **) |
|
181 Goal "(f -- x --CR> L) = (f -- x --NSCR> L)"; |
|
182 by (blast_tac (claset() addIs [CRLIM_NSCRLIM,NSCRLIM_CRLIM]) 1); |
|
183 qed "CRLIM_NSCRLIM_iff"; |
|
184 |
|
185 (** get this result easily now **) |
|
186 Goal "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"; |
|
187 by (auto_tac (claset() addDs [NSCLIM_NSCRLIM_Re],simpset() |
|
188 addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff RS sym])); |
|
189 qed "CLIM_CRLIM_Re"; |
|
190 |
|
191 Goal "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)"; |
|
192 by (auto_tac (claset() addDs [NSCLIM_NSCRLIM_Im],simpset() |
|
193 addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff RS sym])); |
|
194 qed "CLIM_CRLIM_Im"; |
|
195 |
|
196 Goal "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"; |
|
197 by (auto_tac (claset(),simpset() addsimps [CLIM_def, |
|
198 complex_cnj_diff RS sym])); |
|
199 qed "CLIM_cnj"; |
|
200 |
|
201 Goal "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"; |
|
202 by (auto_tac (claset(),simpset() addsimps [CLIM_def, |
|
203 complex_cnj_diff RS sym])); |
|
204 qed "CLIM_cnj_iff"; |
|
205 |
|
206 (*** NSLIM_add hence CLIM_add *) |
|
207 |
|
208 Goalw [NSCLIM_def] |
|
209 "[| f -- x --NSC> l; g -- x --NSC> m |] \ |
|
210 \ ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"; |
|
211 by (auto_tac (claset() addSIs [capprox_add], simpset())); |
|
212 qed "NSCLIM_add"; |
|
213 |
|
214 Goal "[| f -- x --C> l; g -- x --C> m |] \ |
|
215 \ ==> (%x. f(x) + g(x)) -- x --C> (l + m)"; |
|
216 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_add]) 1); |
|
217 qed "CLIM_add"; |
|
218 |
|
219 (*** NSLIM_mult hence CLIM_mult *) |
|
220 |
|
221 Goalw [NSCLIM_def] |
|
222 "[| f -- x --NSC> l; g -- x --NSC> m |] \ |
|
223 \ ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"; |
|
224 by (auto_tac (claset() addSIs [capprox_mult_CFinite], simpset())); |
|
225 qed "NSCLIM_mult"; |
|
226 |
|
227 Goal "[| f -- x --C> l; g -- x --C> m |] \ |
|
228 \ ==> (%x. f(x) * g(x)) -- x --C> (l * m)"; |
|
229 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_mult]) 1); |
|
230 qed "CLIM_mult"; |
|
231 |
|
232 (*** NSCLIM_const and CLIM_const ***) |
|
233 |
|
234 Goalw [NSCLIM_def] "(%x. k) -- x --NSC> k"; |
|
235 by Auto_tac; |
|
236 qed "NSCLIM_const"; |
|
237 Addsimps [NSCLIM_const]; |
|
238 |
|
239 Goalw [CLIM_def] "(%x. k) -- x --C> k"; |
|
240 by Auto_tac; |
|
241 qed "CLIM_const"; |
|
242 Addsimps [CLIM_const]; |
|
243 |
|
244 (*** NSCLIM_minus and CLIM_minus ***) |
|
245 |
|
246 Goalw [NSCLIM_def] |
|
247 "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"; |
|
248 by Auto_tac; |
|
249 qed "NSCLIM_minus"; |
|
250 |
|
251 Goal "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"; |
|
252 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_minus]) 1); |
|
253 qed "CLIM_minus"; |
|
254 |
|
255 (*** NSCLIM_diff hence CLIM_diff ***) |
|
256 |
|
257 Goalw [complex_diff_def] |
|
258 "[| f -- x --NSC> l; g -- x --NSC> m |] \ |
|
259 \ ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"; |
|
260 by (auto_tac (claset(), simpset() addsimps [NSCLIM_add,NSCLIM_minus])); |
|
261 qed "NSCLIM_diff"; |
|
262 |
|
263 Goal "[| f -- x --C> l; g -- x --C> m |] \ |
|
264 \ ==> (%x. f(x) - g(x)) -- x --C> (l - m)"; |
|
265 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_diff]) 1); |
|
266 qed "CLIM_diff"; |
|
267 |
|
268 (*** NSCLIM_inverse and hence CLIM_inverse *) |
|
269 |
|
270 Goalw [NSCLIM_def] |
|
271 "[| f -- a --NSC> L; L ~= 0 |] \ |
|
272 \ ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"; |
|
273 by (Clarify_tac 1); |
|
274 by (dtac spec 1); |
|
275 by (auto_tac (claset(), |
|
276 simpset() addsimps [hcomplex_of_complex_capprox_inverse])); |
|
277 qed "NSCLIM_inverse"; |
|
278 |
|
279 Goal "[| f -- a --C> L; L ~= 0 |] \ |
|
280 \ ==> (%x. inverse(f(x))) -- a --C> (inverse L)"; |
|
281 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_inverse]) 1); |
|
282 qed "CLIM_inverse"; |
|
283 |
|
284 (*** NSCLIM_zero, CLIM_zero, etc. ***) |
|
285 |
|
286 Goal "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"; |
|
287 by (res_inst_tac [("z1","l")] (complex_add_minus_right_zero RS subst) 1); |
|
288 by (rewtac complex_diff_def); |
|
289 by (rtac NSCLIM_add 1 THEN Auto_tac); |
|
290 qed "NSCLIM_zero"; |
|
291 |
|
292 Goal "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"; |
|
293 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_zero]) 1); |
|
294 qed "CLIM_zero"; |
|
295 |
|
296 Goal "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"; |
|
297 by (dres_inst_tac [("g","%x. l"),("m","l")] NSCLIM_add 1); |
|
298 by Auto_tac; |
|
299 qed "NSCLIM_zero_cancel"; |
|
300 |
|
301 Goal "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"; |
|
302 by (dres_inst_tac [("g","%x. l"),("m","l")] CLIM_add 1); |
|
303 by Auto_tac; |
|
304 qed "CLIM_zero_cancel"; |
|
305 |
|
306 (*** NSCLIM_not zero and hence CLIM_not_zero ***) |
|
307 |
|
308 (*not in simpset?*) |
|
309 Addsimps [hypreal_epsilon_not_zero]; |
|
310 |
|
311 Goalw [NSCLIM_def] "k ~= 0 ==> ~ ((%x. k) -- x --NSC> 0)"; |
|
312 by (auto_tac (claset(),simpset() delsimps [hcomplex_of_complex_zero])); |
|
313 by (res_inst_tac [("x","hcomplex_of_complex x + hcomplex_of_hypreal epsilon")] exI 1); |
|
314 by (auto_tac (claset() addIs [CInfinitesimal_add_capprox_self RS capprox_sym],simpset() |
|
315 delsimps [hcomplex_of_complex_zero])); |
|
316 qed "NSCLIM_not_zero"; |
|
317 |
|
318 (* [| k ~= 0; (%x. k) -- x --NSC> 0 |] ==> R *) |
|
319 bind_thm("NSCLIM_not_zeroE", NSCLIM_not_zero RS notE); |
|
320 |
|
321 Goal "k ~= 0 ==> ~ ((%x. k) -- x --C> 0)"; |
|
322 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_not_zero]) 1); |
|
323 qed "CLIM_not_zero"; |
|
324 |
|
325 (*** NSCLIM_const hence CLIM_const ***) |
|
326 |
|
327 Goal "(%x. k) -- x --NSC> L ==> k = L"; |
|
328 by (rtac ccontr 1); |
|
329 by (dtac NSCLIM_zero 1); |
|
330 by (rtac NSCLIM_not_zeroE 1 THEN assume_tac 2); |
|
331 by Auto_tac; |
|
332 qed "NSCLIM_const_eq"; |
|
333 |
|
334 Goal "(%x. k) -- x --C> L ==> k = L"; |
|
335 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff,NSCLIM_const_eq]) 1); |
|
336 qed "CLIM_const_eq"; |
|
337 |
|
338 (*** NSCLIM and hence CLIM are unique ***) |
|
339 |
|
340 Goal "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M"; |
|
341 by (dtac NSCLIM_minus 1); |
|
342 by (dtac NSCLIM_add 1 THEN assume_tac 1); |
|
343 by (auto_tac (claset() addSDs [NSCLIM_const_eq RS sym], simpset())); |
|
344 qed "NSCLIM_unique"; |
|
345 |
|
346 Goal "[| f -- x --C> L; f -- x --C> M |] ==> L = M"; |
|
347 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_unique]) 1); |
|
348 qed "CLIM_unique"; |
|
349 |
|
350 (*** NSCLIM_mult_zero and CLIM_mult_zero ***) |
|
351 |
|
352 Goal "[| f -- x --NSC> 0; g -- x --NSC> 0 |] \ |
|
353 \ ==> (%x. f(x)*g(x)) -- x --NSC> 0"; |
|
354 by (dtac NSCLIM_mult 1 THEN Auto_tac); |
|
355 qed "NSCLIM_mult_zero"; |
|
356 |
|
357 Goal "[| f -- x --C> 0; g -- x --C> 0 |] \ |
|
358 \ ==> (%x. f(x)*g(x)) -- x --C> 0"; |
|
359 by (dtac CLIM_mult 1 THEN Auto_tac); |
|
360 qed "CLIM_mult_zero"; |
|
361 |
|
362 (*** NSCLIM_self hence CLIM_self ***) |
|
363 |
|
364 Goalw [NSCLIM_def] "(%x. x) -- a --NSC> a"; |
|
365 by (auto_tac (claset() addIs [starfunC_Idfun_capprox],simpset())); |
|
366 qed "NSCLIM_self"; |
|
367 |
|
368 Goal "(%x. x) -- a --C> a"; |
|
369 by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff,NSCLIM_self]) 1); |
|
370 qed "CLIM_self"; |
|
371 |
|
372 (** another equivalence result **) |
|
373 Goalw [NSCLIM_def,NSCRLIM_def] |
|
374 "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"; |
|
375 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_capprox_minus |
|
376 RS sym,CInfinitesimal_hcmod_iff])); |
|
377 by (ALLGOALS(dtac spec) THEN Auto_tac); |
|
378 by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hcomplex)); |
|
379 by (auto_tac (claset(),simpset() addsimps [hcomplex_diff, |
|
380 starfunC,starfunCR,hcomplex_of_complex_def,hcmod,mem_infmal_iff])); |
|
381 qed "NSCLIM_NSCRLIM_iff"; |
|
382 |
|
383 (** much, much easier standard proof **) |
|
384 Goalw [CLIM_def,CRLIM_def] |
|
385 "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)"; |
|
386 by Auto_tac; |
|
387 qed "CLIM_CRLIM_iff"; |
|
388 |
|
389 (* so this is nicer nonstandard proof *) |
|
390 Goal "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"; |
|
391 by (auto_tac (claset(),simpset() addsimps [CRLIM_NSCRLIM_iff RS sym, |
|
392 CLIM_CRLIM_iff,CLIM_NSCLIM_iff RS sym])); |
|
393 qed "NSCLIM_NSCRLIM_iff2"; |
|
394 |
|
395 Goal "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) & \ |
|
396 \ (%x. Im(f x)) -- a --NSCR> Im(L))"; |
|
397 by (auto_tac (claset() addIs [NSCLIM_NSCRLIM_Re,NSCLIM_NSCRLIM_Im],simpset())); |
|
398 by (auto_tac (claset(),simpset() addsimps [NSCLIM_def,NSCRLIM_def])); |
|
399 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
400 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
401 by (auto_tac (claset(),simpset() addsimps [capprox_approx_iff,starfunC, |
|
402 hcomplex_of_complex_def,starfunCR,hypreal_of_real_def])); |
|
403 qed "NSCLIM_NSCRLIM_Re_Im_iff"; |
|
404 |
|
405 Goal "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & \ |
|
406 \ (%x. Im(f x)) -- a --CR> Im(L))"; |
|
407 by (auto_tac (claset(),simpset() addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff, |
|
408 NSCLIM_NSCRLIM_Re_Im_iff])); |
|
409 qed "CLIM_CRLIM_Re_Im_iff"; |
|
410 |
|
411 |
|
412 (*------------------------------------------------------------------------------------*) |
|
413 (* Continuity *) |
|
414 (*------------------------------------------------------------------------------------*) |
|
415 |
|
416 Goalw [isNSContc_def] |
|
417 "[| isNSContc f a; y @c= hcomplex_of_complex a |] \ |
|
418 \ ==> ( *fc* f) y @c= hcomplex_of_complex (f a)"; |
|
419 by (Blast_tac 1); |
|
420 qed "isNSContcD"; |
|
421 |
|
422 Goalw [isNSContc_def,NSCLIM_def] |
|
423 "isNSContc f a ==> f -- a --NSC> (f a) "; |
|
424 by (Blast_tac 1); |
|
425 qed "isNSContc_NSCLIM"; |
|
426 |
|
427 Goalw [isNSContc_def,NSCLIM_def] |
|
428 "f -- a --NSC> (f a) ==> isNSContc f a"; |
|
429 by Auto_tac; |
|
430 by (res_inst_tac [("Q","y = hcomplex_of_complex a")] |
|
431 (excluded_middle RS disjE) 1); |
|
432 by Auto_tac; |
|
433 qed "NSCLIM_isNSContc"; |
|
434 |
|
435 (*--------------------------------------------------*) |
|
436 (* NS continuity can be defined using NS Limit in *) |
|
437 (* similar fashion to standard def of continuity *) |
|
438 (* -------------------------------------------------*) |
|
439 |
|
440 Goal "(isNSContc f a) = (f -- a --NSC> (f a))"; |
|
441 by (blast_tac (claset() addIs [isNSContc_NSCLIM,NSCLIM_isNSContc]) 1); |
|
442 qed "isNSContc_NSCLIM_iff"; |
|
443 |
|
444 Goal "(isNSContc f a) = (f -- a --C> (f a))"; |
|
445 by (asm_full_simp_tac (simpset() addsimps |
|
446 [CLIM_NSCLIM_iff,isNSContc_NSCLIM_iff]) 1); |
|
447 qed "isNSContc_CLIM_iff"; |
|
448 |
|
449 (*** key result for continuity ***) |
|
450 Goalw [isContc_def] "(isNSContc f a) = (isContc f a)"; |
|
451 by (rtac isNSContc_CLIM_iff 1); |
|
452 qed "isNSContc_isContc_iff"; |
|
453 |
|
454 Goal "isContc f a ==> isNSContc f a"; |
|
455 by (etac (isNSContc_isContc_iff RS iffD2) 1); |
|
456 qed "isContc_isNSContc"; |
|
457 |
|
458 Goal "isNSContc f a ==> isContc f a"; |
|
459 by (etac (isNSContc_isContc_iff RS iffD1) 1); |
|
460 qed "isNSContc_isContc"; |
|
461 |
|
462 (*--------------------------------------------------*) |
|
463 (* Alternative definition of continuity *) |
|
464 (* -------------------------------------------------*) |
|
465 |
|
466 Goalw [NSCLIM_def] |
|
467 "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"; |
|
468 by Auto_tac; |
|
469 by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1); |
|
470 by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2); |
|
471 by (Step_tac 1); |
|
472 by (Asm_full_simp_tac 1); |
|
473 by (rtac ((mem_cinfmal_iff RS iffD2) RS |
|
474 (CInfinitesimal_add_capprox_self RS capprox_sym)) 1); |
|
475 by (rtac (capprox_minus_iff2 RS iffD1) 4); |
|
476 by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 3); |
|
477 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); |
|
478 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4); |
|
479 by (auto_tac (claset(), |
|
480 simpset() addsimps [starfunC, hcomplex_of_complex_def, |
|
481 hcomplex_minus, hcomplex_add])); |
|
482 qed "NSCLIM_h_iff"; |
|
483 |
|
484 Goal "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"; |
|
485 by (rtac NSCLIM_h_iff 1); |
|
486 qed "NSCLIM_isContc_iff"; |
|
487 |
|
488 Goal "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"; |
|
489 by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_isContc_iff]) 1); |
|
490 qed "CLIM_isContc_iff"; |
|
491 |
|
492 Goalw [isContc_def] "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"; |
|
493 by (simp_tac (simpset() addsimps [CLIM_isContc_iff]) 1); |
|
494 qed "isContc_iff"; |
|
495 |
|
496 Goal "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"; |
|
497 by (auto_tac (claset() addIs [capprox_add], |
|
498 simpset() addsimps [isNSContc_isContc_iff RS sym, isNSContc_def])); |
|
499 qed "isContc_add"; |
|
500 |
|
501 Goal "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"; |
|
502 by (auto_tac (claset() addSIs [starfunC_mult_CFinite_capprox], |
|
503 simpset() delsimps [starfunC_mult RS sym] |
|
504 addsimps [isNSContc_isContc_iff RS sym, isNSContc_def])); |
|
505 qed "isContc_mult"; |
|
506 |
|
507 (*** more theorems: note simple proofs ***) |
|
508 |
|
509 Goal "[| isContc f a; isContc g (f a) |] \ |
|
510 \ ==> isContc (g o f) a"; |
|
511 by (auto_tac (claset(),simpset() addsimps [isNSContc_isContc_iff RS sym, |
|
512 isNSContc_def,starfunC_o RS sym])); |
|
513 qed "isContc_o"; |
|
514 |
|
515 Goal "[| isContc f a; isContc g (f a) |] \ |
|
516 \ ==> isContc (%x. g (f x)) a"; |
|
517 by (auto_tac (claset() addDs [isContc_o],simpset() addsimps [o_def])); |
|
518 qed "isContc_o2"; |
|
519 |
|
520 Goalw [isNSContc_def] "isNSContc f a ==> isNSContc (%x. - f x) a"; |
|
521 by Auto_tac; |
|
522 qed "isNSContc_minus"; |
|
523 |
|
524 Goal "isContc f a ==> isContc (%x. - f x) a"; |
|
525 by (auto_tac (claset(),simpset() addsimps [isNSContc_isContc_iff RS sym, |
|
526 isNSContc_minus])); |
|
527 qed "isContc_minus"; |
|
528 |
|
529 Goalw [isContc_def] |
|
530 "[| isContc f x; f x ~= 0 |] ==> isContc (%x. inverse (f x)) x"; |
|
531 by (blast_tac (claset() addIs [CLIM_inverse]) 1); |
|
532 qed "isContc_inverse"; |
|
533 |
|
534 Goal "[| isNSContc f x; f x ~= 0 |] ==> isNSContc (%x. inverse (f x)) x"; |
|
535 by (auto_tac (claset() addIs [isContc_inverse],simpset() addsimps |
|
536 [isNSContc_isContc_iff])); |
|
537 qed "isNSContc_inverse"; |
|
538 |
|
539 Goalw [complex_diff_def] |
|
540 "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"; |
|
541 by (auto_tac (claset() addIs [isContc_add,isContc_minus],simpset())); |
|
542 qed "isContc_diff"; |
|
543 |
|
544 Goalw [isContc_def] "isContc (%x. k) a"; |
|
545 by (Simp_tac 1); |
|
546 qed "isContc_const"; |
|
547 Addsimps [isContc_const]; |
|
548 |
|
549 Goalw [isNSContc_def] "isNSContc (%x. k) a"; |
|
550 by (Simp_tac 1); |
|
551 qed "isNSContc_const"; |
|
552 Addsimps [isNSContc_const]; |
|
553 |
|
554 |
|
555 (*------------------------------------------------------------------------------------*) |
|
556 (* functions from complex to reals *) |
|
557 (* -----------------------------------------------------------------------------------*) |
|
558 |
|
559 Goalw [isNSContCR_def] |
|
560 "[| isNSContCR f a; y @c= hcomplex_of_complex a |] \ |
|
561 \ ==> ( *fcR* f) y @= hypreal_of_real (f a)"; |
|
562 by (Blast_tac 1); |
|
563 qed "isNSContCRD"; |
|
564 |
|
565 Goalw [isNSContCR_def,NSCRLIM_def] |
|
566 "isNSContCR f a ==> f -- a --NSCR> (f a) "; |
|
567 by (Blast_tac 1); |
|
568 qed "isNSContCR_NSCRLIM"; |
|
569 |
|
570 Goalw [isNSContCR_def,NSCRLIM_def] |
|
571 "f -- a --NSCR> (f a) ==> isNSContCR f a"; |
|
572 by Auto_tac; |
|
573 by (res_inst_tac [("Q","y = hcomplex_of_complex a")] |
|
574 (excluded_middle RS disjE) 1); |
|
575 by Auto_tac; |
|
576 qed "NSCRLIM_isNSContCR"; |
|
577 |
|
578 Goal "(isNSContCR f a) = (f -- a --NSCR> (f a))"; |
|
579 by (blast_tac (claset() addIs [isNSContCR_NSCRLIM,NSCRLIM_isNSContCR]) 1); |
|
580 qed "isNSContCR_NSCRLIM_iff"; |
|
581 |
|
582 Goal "(isNSContCR f a) = (f -- a --CR> (f a))"; |
|
583 by (asm_full_simp_tac (simpset() addsimps |
|
584 [CRLIM_NSCRLIM_iff,isNSContCR_NSCRLIM_iff]) 1); |
|
585 qed "isNSContCR_CRLIM_iff"; |
|
586 |
|
587 (*** another key result for continuity ***) |
|
588 Goalw [isContCR_def] "(isNSContCR f a) = (isContCR f a)"; |
|
589 by (rtac isNSContCR_CRLIM_iff 1); |
|
590 qed "isNSContCR_isContCR_iff"; |
|
591 |
|
592 Goal "isContCR f a ==> isNSContCR f a"; |
|
593 by (etac (isNSContCR_isContCR_iff RS iffD2) 1); |
|
594 qed "isContCR_isNSContCR"; |
|
595 |
|
596 Goal "isNSContCR f a ==> isContCR f a"; |
|
597 by (etac (isNSContCR_isContCR_iff RS iffD1) 1); |
|
598 qed "isNSContCR_isContCR"; |
|
599 |
|
600 Goalw [isNSContCR_def] "isNSContCR cmod (a)"; |
|
601 by (auto_tac (claset() addIs [capprox_hcmod_approx], |
|
602 simpset() addsimps [starfunCR_cmod,hcmod_hcomplex_of_complex |
|
603 RS sym])); |
|
604 qed "isNSContCR_cmod"; |
|
605 Addsimps [isNSContCR_cmod]; |
|
606 |
|
607 Goal "isContCR cmod (a)"; |
|
608 by (auto_tac (claset(),simpset() addsimps [isNSContCR_isContCR_iff RS sym])); |
|
609 qed "isContCR_cmod"; |
|
610 Addsimps [isContCR_cmod]; |
|
611 |
|
612 Goalw [isContc_def,isContCR_def] |
|
613 "isContc f a ==> isContCR (%x. Re (f x)) a"; |
|
614 by (etac CLIM_CRLIM_Re 1); |
|
615 qed "isContc_isContCR_Re"; |
|
616 |
|
617 Goalw [isContc_def,isContCR_def] |
|
618 "isContc f a ==> isContCR (%x. Im (f x)) a"; |
|
619 by (etac CLIM_CRLIM_Im 1); |
|
620 qed "isContc_isContCR_Im"; |
|
621 |
|
622 (*------------------------------------------------------------------------------------*) |
|
623 (* Derivatives *) |
|
624 (*------------------------------------------------------------------------------------*) |
|
625 |
|
626 Goalw [cderiv_def] |
|
627 "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"; |
|
628 by (Blast_tac 1); |
|
629 qed "CDERIV_iff"; |
|
630 |
|
631 Goalw [cderiv_def] |
|
632 "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"; |
|
633 by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff]) 1); |
|
634 qed "CDERIV_NSC_iff"; |
|
635 |
|
636 Goalw [cderiv_def] |
|
637 "CDERIV f x :> D \ |
|
638 \ ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D"; |
|
639 by (Blast_tac 1); |
|
640 qed "CDERIVD"; |
|
641 |
|
642 Goalw [cderiv_def] |
|
643 "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D"; |
|
644 by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff]) 1); |
|
645 qed "NSC_DERIVD"; |
|
646 |
|
647 (*** Uniqueness ***) |
|
648 |
|
649 Goalw [cderiv_def] |
|
650 "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E"; |
|
651 by (blast_tac (claset() addIs [CLIM_unique]) 1); |
|
652 qed "CDERIV_unique"; |
|
653 |
|
654 (*** uniqueness: a nonstandard proof ***) |
|
655 Goalw [nscderiv_def] |
|
656 "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E"; |
|
657 by (auto_tac (claset() addSDs [inst "x" "hcomplex_of_hypreal epsilon" bspec] |
|
658 addSIs [inj_hcomplex_of_complex RS injD] |
|
659 addDs [capprox_trans3], |
|
660 simpset())); |
|
661 qed "NSCDeriv_unique"; |
|
662 |
|
663 |
|
664 (*------------------------------------------------------------------------------------*) |
|
665 (* Differentiability *) |
|
666 (*------------------------------------------------------------------------------------*) |
|
667 |
|
668 Goalw [cdifferentiable_def] |
|
669 "f cdifferentiable x ==> EX D. CDERIV f x :> D"; |
|
670 by (assume_tac 1); |
|
671 qed "cdifferentiableD"; |
|
672 |
|
673 Goalw [cdifferentiable_def] |
|
674 "CDERIV f x :> D ==> f cdifferentiable x"; |
|
675 by (Blast_tac 1); |
|
676 qed "cdifferentiableI"; |
|
677 |
|
678 Goalw [NSCdifferentiable_def] |
|
679 "f NSCdifferentiable x ==> EX D. NSCDERIV f x :> D"; |
|
680 by (assume_tac 1); |
|
681 qed "NSCdifferentiableD"; |
|
682 |
|
683 Goalw [NSCdifferentiable_def] |
|
684 "NSCDERIV f x :> D ==> f NSCdifferentiable x"; |
|
685 by (Blast_tac 1); |
|
686 qed "NSCdifferentiableI"; |
|
687 |
|
688 |
|
689 (*------------------------------------------------------------------------------------*) |
|
690 (* Alternative definition for differentiability *) |
|
691 (*------------------------------------------------------------------------------------*) |
|
692 |
|
693 Goalw [CLIM_def] |
|
694 "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = \ |
|
695 \ ((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)"; |
|
696 by (Step_tac 1); |
|
697 by (ALLGOALS(dtac spec)); |
|
698 by (Step_tac 1); |
|
699 by (Blast_tac 1 THEN Blast_tac 2); |
|
700 by (ALLGOALS(res_inst_tac [("x","s")] exI)); |
|
701 by (Step_tac 1); |
|
702 by (dres_inst_tac [("x","x - a")] spec 1); |
|
703 by (dres_inst_tac [("x","x + a")] spec 2); |
|
704 by (auto_tac (claset(), simpset() addsimps complex_add_ac)); |
|
705 qed "CDERIV_CLIM_iff"; |
|
706 |
|
707 Goalw [cderiv_def] "(CDERIV f x :> D) = \ |
|
708 \ ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)"; |
|
709 by (simp_tac (simpset() addsimps [CDERIV_CLIM_iff]) 1); |
|
710 qed "CDERIV_iff2"; |
|
711 |
|
712 |
|
713 (*------------------------------------------------------------------------------------*) |
|
714 (* Equivalence of NS and standard defs of differentiation *) |
|
715 (*------------------------------------------------------------------------------------*) |
|
716 |
|
717 (*** first equivalence ***) |
|
718 Goalw [nscderiv_def,NSCLIM_def] |
|
719 "(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"; |
|
720 by Auto_tac; |
|
721 by (dres_inst_tac [("x","xa")] bspec 1); |
|
722 by (rtac ccontr 3); |
|
723 by (dres_inst_tac [("x","h")] spec 3); |
|
724 by (auto_tac (claset(), |
|
725 simpset() addsimps [mem_cinfmal_iff, starfunC_lambda_cancel])); |
|
726 qed "NSCDERIV_NSCLIM_iff"; |
|
727 |
|
728 (*** 2nd equivalence ***) |
|
729 Goal "(NSCDERIV f x :> D) = \ |
|
730 \ ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)"; |
|
731 by (full_simp_tac (simpset() addsimps |
|
732 [NSCDERIV_NSCLIM_iff, CDERIV_CLIM_iff, CLIM_NSCLIM_iff RS sym]) 1); |
|
733 qed "NSCDERIV_NSCLIM_iff2"; |
|
734 |
|
735 Goal "(NSCDERIV f x :> D) = \ |
|
736 \ (ALL xa. xa ~= hcomplex_of_complex x & xa @c= hcomplex_of_complex x --> \ |
|
737 \ ( *fc* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"; |
|
738 by (auto_tac (claset(), simpset() addsimps [NSCDERIV_NSCLIM_iff2, NSCLIM_def])); |
|
739 qed "NSCDERIV_iff2"; |
|
740 |
|
741 Goalw [cderiv_def] "(NSCDERIV f x :> D) = (CDERIV f x :> D)"; |
|
742 by (simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,CLIM_NSCLIM_iff]) 1); |
|
743 qed "NSCDERIV_CDERIV_iff"; |
|
744 |
|
745 Goalw [nscderiv_def] |
|
746 "NSCDERIV f x :> D ==> isNSContc f x"; |
|
747 by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff, |
|
748 NSCLIM_def,hcomplex_diff_def])); |
|
749 by (dtac (capprox_minus_iff RS iffD1) 1); |
|
750 by (dtac (CLAIM "x ~= a ==> x + - a ~= (0::hcomplex)") 1); |
|
751 by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1); |
|
752 by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2); |
|
753 by (auto_tac (claset(),simpset() addsimps |
|
754 [mem_cinfmal_iff RS sym,hcomplex_add_commute])); |
|
755 by (dres_inst_tac [("c","xa + - hcomplex_of_complex x")] capprox_mult1 1); |
|
756 by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite |
|
757 RS subsetD],simpset() addsimps [hcomplex_mult_assoc])); |
|
758 by (dres_inst_tac [("x3","D")] (CFinite_hcomplex_of_complex RSN |
|
759 (2,CInfinitesimal_CFinite_mult) RS (mem_cinfmal_iff RS iffD1)) 1); |
|
760 by (blast_tac (claset() addIs [capprox_trans,hcomplex_mult_commute RS subst, |
|
761 (capprox_minus_iff RS iffD2)]) 1); |
|
762 qed "NSCDERIV_isNSContc"; |
|
763 |
|
764 Goal "CDERIV f x :> D ==> isContc f x"; |
|
765 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym, |
|
766 isNSContc_isContc_iff RS sym,NSCDERIV_isNSContc]) 1); |
|
767 qed "CDERIV_isContc"; |
|
768 |
|
769 (*------------------------------------------------------------------------------------*) |
|
770 (* Differentiation rules for combinations of functions follow from clear, *) |
|
771 (* straightforard, algebraic manipulations *) |
|
772 (*------------------------------------------------------------------------------------*) |
|
773 |
|
774 (* use simple constant nslimit theorem *) |
|
775 Goal "(NSCDERIV (%x. k) x :> 0)"; |
|
776 by (simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff]) 1); |
|
777 qed "NSCDERIV_const"; |
|
778 Addsimps [NSCDERIV_const]; |
|
779 |
|
780 Goal "(CDERIV (%x. k) x :> 0)"; |
|
781 by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1); |
|
782 qed "CDERIV_const"; |
|
783 Addsimps [CDERIV_const]; |
|
784 |
|
785 Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ |
|
786 \ ==> NSCDERIV (%x. f x + g x) x :> Da + Db"; |
|
787 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, |
|
788 NSCLIM_def]) 1 THEN REPEAT(Step_tac 1)); |
|
789 by (auto_tac (claset(), |
|
790 simpset() addsimps [hcomplex_add_divide_distrib,hcomplex_diff_def])); |
|
791 by (dres_inst_tac [("b","hcomplex_of_complex Da"), |
|
792 ("d","hcomplex_of_complex Db")] capprox_add 1); |
|
793 by (auto_tac (claset(), simpset() addsimps hcomplex_add_ac)); |
|
794 qed "NSCDERIV_add"; |
|
795 |
|
796 Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ |
|
797 \ ==> CDERIV (%x. f x + g x) x :> Da + Db"; |
|
798 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_add, |
|
799 NSCDERIV_CDERIV_iff RS sym]) 1); |
|
800 qed "CDERIV_add"; |
|
801 |
|
802 (*** lemmas for multiplication ***) |
|
803 |
|
804 Goal "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"; |
|
805 by (simp_tac (simpset() addsimps [hcomplex_diff_mult_distrib2]) 1); |
|
806 val lemma_nscderiv1 = result(); |
|
807 |
|
808 Goal "[| (x + y) / z = hcomplex_of_complex D + yb; z ~= 0; \ |
|
809 \ z : CInfinitesimal; yb : CInfinitesimal |] \ |
|
810 \ ==> x + y @c= 0"; |
|
811 by (forw_inst_tac [("c1","z")] (hcomplex_mult_right_cancel RS iffD2) 1 |
|
812 THEN assume_tac 1); |
|
813 by (thin_tac "(x + y) / z = hcomplex_of_complex D + yb" 1); |
|
814 by (auto_tac (claset() addSIs [CInfinitesimal_CFinite_mult2, CFinite_add], |
|
815 simpset() addsimps [mem_cinfmal_iff RS sym])); |
|
816 by (etac (CInfinitesimal_subset_CFinite RS subsetD) 1); |
|
817 val lemma_nscderiv2 = result(); |
|
818 |
|
819 Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ |
|
820 \ ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
821 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def]) 1 |
|
822 THEN REPEAT(Step_tac 1)); |
|
823 by (auto_tac (claset(), |
|
824 simpset() addsimps [starfunC_lambda_cancel, lemma_nscderiv1, |
|
825 hcomplex_of_complex_zero])); |
|
826 by (simp_tac (simpset() addsimps [hcomplex_add_divide_distrib]) 1); |
|
827 by (REPEAT(dtac (bex_CInfinitesimal_iff2 RS iffD2) 1)); |
|
828 by (auto_tac (claset(), |
|
829 simpset() delsimps [hcomplex_times_divide1_eq] |
|
830 addsimps [hcomplex_times_divide1_eq RS sym])); |
|
831 by (rewtac hcomplex_diff_def); |
|
832 by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1); |
|
833 by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4); |
|
834 by (auto_tac (claset() addSIs [capprox_add_mono1], |
|
835 simpset() addsimps [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2, |
|
836 hcomplex_mult_commute, hcomplex_add_assoc])); |
|
837 by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")] |
|
838 (hcomplex_add_commute RS subst) 1); |
|
839 by (auto_tac (claset() addSIs [CInfinitesimal_add_capprox_self2 RS capprox_sym, |
|
840 CInfinitesimal_add, CInfinitesimal_mult, |
|
841 CInfinitesimal_hcomplex_of_complex_mult, |
|
842 CInfinitesimal_hcomplex_of_complex_mult2], |
|
843 simpset() addsimps [hcomplex_add_assoc RS sym])); |
|
844 qed "NSCDERIV_mult"; |
|
845 |
|
846 Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ |
|
847 \ ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
848 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_mult, |
|
849 NSCDERIV_CDERIV_iff RS sym]) 1); |
|
850 qed "CDERIV_mult"; |
|
851 |
|
852 Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"; |
|
853 by (asm_full_simp_tac |
|
854 (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff, |
|
855 complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym, |
|
856 complex_diff_def] |
|
857 delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]) 1); |
|
858 by (etac (NSCLIM_const RS NSCLIM_mult) 1); |
|
859 qed "NSCDERIV_cmult"; |
|
860 |
|
861 Goal "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"; |
|
862 by (auto_tac (claset(),simpset() addsimps [NSCDERIV_cmult,NSCDERIV_CDERIV_iff |
|
863 RS sym])); |
|
864 qed "CDERIV_cmult"; |
|
865 |
|
866 Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"; |
|
867 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1); |
|
868 by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1); |
|
869 by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym] |
|
870 delsimps [complex_minus_add_distrib, complex_minus_minus]) 1); |
|
871 by (etac NSCLIM_minus 1); |
|
872 qed "NSCDERIV_minus"; |
|
873 |
|
874 Goal "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D"; |
|
875 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_minus,NSCDERIV_CDERIV_iff RS sym]) 1); |
|
876 qed "CDERIV_minus"; |
|
877 |
|
878 Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ |
|
879 \ ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db"; |
|
880 by (blast_tac (claset() addDs [NSCDERIV_add,NSCDERIV_minus]) 1); |
|
881 qed "NSCDERIV_add_minus"; |
|
882 |
|
883 Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ |
|
884 \ ==> CDERIV (%x. f x + -g x) x :> Da + -Db"; |
|
885 by (blast_tac (claset() addDs [CDERIV_add,CDERIV_minus]) 1); |
|
886 qed "CDERIV_add_minus"; |
|
887 |
|
888 Goalw [complex_diff_def] |
|
889 "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ |
|
890 \ ==> NSCDERIV (%x. f x - g x) x :> Da - Db"; |
|
891 by (blast_tac (claset() addIs [NSCDERIV_add_minus]) 1); |
|
892 qed "NSCDERIV_diff"; |
|
893 |
|
894 Goalw [complex_diff_def] |
|
895 "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ |
|
896 \ ==> CDERIV (%x. f x - g x) x :> Da - Db"; |
|
897 by (blast_tac (claset() addIs [CDERIV_add_minus]) 1); |
|
898 qed "CDERIV_diff"; |
|
899 |
|
900 |
|
901 (*--------------------------------------------------*) |
|
902 (* Chain rule *) |
|
903 (*--------------------------------------------------*) |
|
904 |
|
905 (* lemmas *) |
|
906 Goalw [nscderiv_def] |
|
907 "[| NSCDERIV g x :> D; \ |
|
908 \ ( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);\ |
|
909 \ xa : CInfinitesimal; xa ~= 0 \ |
|
910 \ |] ==> D = 0"; |
|
911 by (dtac bspec 1); |
|
912 by Auto_tac; |
|
913 qed "NSCDERIV_zero"; |
|
914 |
|
915 Goalw [nscderiv_def] |
|
916 "[| NSCDERIV f x :> D; h: CInfinitesimal; h ~= 0 |] \ |
|
917 \ ==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0"; |
|
918 by (asm_full_simp_tac (simpset() addsimps [mem_cinfmal_iff RS sym]) 1); |
|
919 by (rtac CInfinitesimal_ratio 1); |
|
920 by (rtac capprox_hcomplex_of_complex_CFinite 3); |
|
921 by Auto_tac; |
|
922 qed "NSCDERIV_capprox"; |
|
923 |
|
924 |
|
925 (*--------------------------------------------------*) |
|
926 (* from one version of differentiability *) |
|
927 (* *) |
|
928 (* f(x) - f(a) *) |
|
929 (* --------------- @= Db *) |
|
930 (* x - a *) |
|
931 (* -------------------------------------------------*) |
|
932 |
|
933 Goal "[| NSCDERIV f (g x) :> Da; \ |
|
934 \ ( *fc* g) (hcomplex_of_complex(x) + xa) ~= hcomplex_of_complex (g x); \ |
|
935 \ ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x) \ |
|
936 \ |] ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa)) \ |
|
937 \ - hcomplex_of_complex (f (g x))) \ |
|
938 \ / (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) \ |
|
939 \ @c= hcomplex_of_complex (Da)"; |
|
940 by (auto_tac (claset(),simpset() addsimps [NSCDERIV_NSCLIM_iff2, NSCLIM_def])); |
|
941 qed "NSCDERIVD1"; |
|
942 |
|
943 (*--------------------------------------------------*) |
|
944 (* from other version of differentiability *) |
|
945 (* *) |
|
946 (* f(x + h) - f(x) *) |
|
947 (* ----------------- @= Db *) |
|
948 (* h *) |
|
949 (*--------------------------------------------------*) |
|
950 |
|
951 Goal "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa ~= 0 |] \ |
|
952 \ ==> (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex(g x)) / xa \ |
|
953 \ @c= hcomplex_of_complex (Db)"; |
|
954 by (auto_tac (claset(), |
|
955 simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def, |
|
956 mem_cinfmal_iff, starfunC_lambda_cancel])); |
|
957 qed "NSCDERIVD2"; |
|
958 |
|
959 Goal "(z::hcomplex) ~= 0 ==> x*y = (x*inverse(z))*(z*y)"; |
|
960 by Auto_tac; |
|
961 qed "lemma_complex_chain"; |
|
962 |
|
963 (*** chain rule ***) |
|
964 |
|
965 Goal "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] \ |
|
966 \ ==> NSCDERIV (f o g) x :> Da * Db"; |
|
967 by (asm_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, |
|
968 NSCLIM_def,mem_cinfmal_iff RS sym]) 1 THEN Step_tac 1); |
|
969 by (forw_inst_tac [("f","g")] NSCDERIV_capprox 1); |
|
970 by (auto_tac (claset(), |
|
971 simpset() addsimps [starfunC_lambda_cancel2, starfunC_o RS sym])); |
|
972 by (case_tac "( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex (g x)" 1); |
|
973 by (dres_inst_tac [("g","g")] NSCDERIV_zero 1); |
|
974 by (auto_tac (claset(),simpset() addsimps [hcomplex_divide_def])); |
|
975 by (res_inst_tac [("z1","( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)"), |
|
976 ("y1","inverse xa")] (lemma_complex_chain RS ssubst) 1); |
|
977 by (Asm_simp_tac 1); |
|
978 by (rtac capprox_mult_hcomplex_of_complex 1); |
|
979 by (fold_tac [hcomplex_divide_def]); |
|
980 by (blast_tac (claset() addIs [NSCDERIVD2]) 2); |
|
981 by (auto_tac (claset() addSIs [NSCDERIVD1] addIs [capprox_minus_iff RS iffD2], |
|
982 simpset() addsimps [symmetric hcomplex_diff_def])); |
|
983 qed "NSCDERIV_chain"; |
|
984 |
|
985 (* standard version *) |
|
986 Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \ |
|
987 \ ==> CDERIV (f o g) x :> Da * Db"; |
|
988 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym, |
|
989 NSCDERIV_chain]) 1); |
|
990 qed "CDERIV_chain"; |
|
991 |
|
992 Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \ |
|
993 \ ==> CDERIV (%x. f (g x)) x :> Da * Db"; |
|
994 by (auto_tac (claset() addDs [CDERIV_chain], simpset() addsimps [o_def])); |
|
995 qed "CDERIV_chain2"; |
|
996 |
|
997 (*------------------------------------------------------------------------------------*) |
|
998 (* Differentiation of natural number powers *) |
|
999 (*------------------------------------------------------------------------------------*) |
|
1000 |
|
1001 Goal "NSCDERIV (%x. x) x :> 1"; |
|
1002 by (auto_tac (claset(), |
|
1003 simpset() addsimps [NSCDERIV_NSCLIM_iff,NSCLIM_def])); |
|
1004 qed "NSCDERIV_Id"; |
|
1005 Addsimps [NSCDERIV_Id]; |
|
1006 |
|
1007 Goal "CDERIV (%x. x) x :> 1"; |
|
1008 by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1); |
|
1009 qed "CDERIV_Id"; |
|
1010 Addsimps [CDERIV_Id]; |
|
1011 |
|
1012 bind_thm ("isContc_Id", CDERIV_Id RS CDERIV_isContc); |
|
1013 |
|
1014 (*derivative of linear multiplication*) |
|
1015 Goal "CDERIV (op * c) x :> c"; |
|
1016 by (cut_inst_tac [("c","c"),("x","x")] (CDERIV_Id RS CDERIV_cmult) 1); |
|
1017 by (Asm_full_simp_tac 1); |
|
1018 qed "CDERIV_cmult_Id"; |
|
1019 Addsimps [CDERIV_cmult_Id]; |
|
1020 |
|
1021 Goal "NSCDERIV (op * c) x :> c"; |
|
1022 by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1); |
|
1023 qed "NSCDERIV_cmult_Id"; |
|
1024 Addsimps [NSCDERIV_cmult_Id]; |
|
1025 |
|
1026 Goal "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - 1))"; |
|
1027 by (induct_tac "n" 1); |
|
1028 by (dtac (CDERIV_Id RS CDERIV_mult) 2); |
|
1029 by (auto_tac (claset(), |
|
1030 simpset() addsimps [complex_of_real_add RS sym, |
|
1031 complex_add_mult_distrib,real_of_nat_Suc] delsimps [complex_of_real_add])); |
|
1032 by (case_tac "n" 1); |
|
1033 by (auto_tac (claset(), |
|
1034 simpset() addsimps [complex_mult_assoc, complex_add_commute])); |
|
1035 by (auto_tac (claset(),simpset() addsimps [complex_mult_commute])); |
|
1036 qed "CDERIV_pow"; |
|
1037 Addsimps [CDERIV_pow,simplify (simpset()) CDERIV_pow]; |
|
1038 |
|
1039 (* NS version *) |
|
1040 Goal "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"; |
|
1041 by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1); |
|
1042 qed "NSCDERIV_pow"; |
|
1043 |
|
1044 Goal "\\<lbrakk> CDERIV f x :> D; D = E \\<rbrakk> \\<Longrightarrow> CDERIV f x :> E"; |
|
1045 by Auto_tac; |
|
1046 qed "lemma_CDERIV_subst"; |
|
1047 |
|
1048 (*used once, in NSCDERIV_inverse*) |
|
1049 Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0"; |
|
1050 by Auto_tac; |
|
1051 qed "CInfinitesimal_add_not_zero"; |
|
1052 |
|
1053 (*** |
|
1054 Goal "[|(x::hcomplex) ~= 0; y ~= 0 |] \ |
|
1055 \ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; |
|
1056 by (asm_full_simp_tac (simpset() addsimps [hcomplex_inverse_distrib, |
|
1057 hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1); |
|
1058 qed "hcomplex_inverse_add"; |
|
1059 ***) |
|
1060 |
|
1061 (*Can't get rid of x ~= 0 because it isn't continuous at zero*) |
|
1062 |
|
1063 Goalw [nscderiv_def] |
|
1064 "x ~= 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"; |
|
1065 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
|
1066 by (forward_tac [CInfinitesimal_add_not_zero] 1); |
|
1067 by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,two_eq_Suc_Suc]) 2); |
|
1068 by (auto_tac (claset(), |
|
1069 simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] |
|
1070 delsimps [hcomplex_minus_mult_eq1 RS sym, |
|
1071 hcomplex_minus_mult_eq2 RS sym])); |
|
1072 by (asm_simp_tac |
|
1073 (simpset() addsimps [hcomplex_inverse_add, |
|
1074 hcomplex_inverse_distrib RS sym, hcomplex_minus_inverse RS sym] |
|
1075 @ hcomplex_add_ac @ hcomplex_mult_ac |
|
1076 delsimps [hcomplex_minus_mult_eq1 RS sym, |
|
1077 hcomplex_minus_mult_eq2 RS sym] ) 1); |
|
1078 by (asm_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym, |
|
1079 hcomplex_add_mult_distrib2] |
|
1080 delsimps [hcomplex_minus_mult_eq1 RS sym, |
|
1081 hcomplex_minus_mult_eq2 RS sym]) 1); |
|
1082 by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")] |
|
1083 capprox_trans 1); |
|
1084 by (rtac inverse_add_CInfinitesimal_capprox2 1); |
|
1085 by (auto_tac (claset() addSDs [hcomplex_of_complex_CFinite_diff_CInfinitesimal] addIs [CFinite_mult], |
|
1086 simpset() addsimps [hcomplex_minus_inverse RS sym])); |
|
1087 by (rtac CInfinitesimal_CFinite_mult2 1); |
|
1088 by Auto_tac; |
|
1089 qed "NSCDERIV_inverse"; |
|
1090 |
|
1091 Goal "x ~= 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"; |
|
1092 by (asm_simp_tac (simpset() addsimps [NSCDERIV_inverse, |
|
1093 NSCDERIV_CDERIV_iff RS sym] delsimps [complexpow_Suc]) 1); |
|
1094 qed "CDERIV_inverse"; |
|
1095 |
|
1096 |
|
1097 (*------------------------------------------------------------------------------------*) |
|
1098 (* Derivative of inverse *) |
|
1099 (*------------------------------------------------------------------------------------*) |
|
1100 |
|
1101 Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \ |
|
1102 \ ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"; |
|
1103 by (rtac (complex_mult_commute RS subst) 1); |
|
1104 by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1, |
|
1105 complexpow_inverse] delsimps [complexpow_Suc, |
|
1106 complex_minus_mult_eq1 RS sym]) 1); |
|
1107 by (fold_goals_tac [o_def]); |
|
1108 by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1); |
|
1109 qed "CDERIV_inverse_fun"; |
|
1110 |
|
1111 Goal "[| NSCDERIV f x :> d; f(x) ~= 0 |] \ |
|
1112 \ ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"; |
|
1113 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff, |
|
1114 CDERIV_inverse_fun] delsimps [complexpow_Suc]) 1); |
|
1115 qed "NSCDERIV_inverse_fun"; |
|
1116 |
|
1117 (*------------------------------------------------------------------------------------*) |
|
1118 (* Derivative of quotient *) |
|
1119 (*------------------------------------------------------------------------------------*) |
|
1120 |
|
1121 |
|
1122 Goal "x ~= (0::complex) \\<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"; |
|
1123 by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc])); |
|
1124 qed "lemma_complex_mult_inverse_squared"; |
|
1125 Addsimps [lemma_complex_mult_inverse_squared]; |
|
1126 |
|
1127 Goalw [complex_diff_def] |
|
1128 "[| CDERIV f x :> d; CDERIV g x :> e; g(x) ~= 0 |] \ |
|
1129 \ ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"; |
|
1130 by (dres_inst_tac [("f","g")] CDERIV_inverse_fun 1); |
|
1131 by (dtac CDERIV_mult 2); |
|
1132 by (REPEAT(assume_tac 1)); |
|
1133 by (asm_full_simp_tac |
|
1134 (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2, |
|
1135 complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac |
|
1136 delsimps [complexpow_Suc, complex_minus_mult_eq1 RS sym, |
|
1137 complex_minus_mult_eq2 RS sym]) 1); |
|
1138 qed "CDERIV_quotient"; |
|
1139 |
|
1140 Goal "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) ~= 0 |] \ |
|
1141 \ ==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"; |
|
1142 by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff, |
|
1143 CDERIV_quotient] delsimps [complexpow_Suc]) 1); |
|
1144 qed "NSCDERIV_quotient"; |
|
1145 |
|
1146 |
|
1147 (*------------------------------------------------------------------------------------*) |
|
1148 (* Caratheodory formulation of derivative at a point: standard proof *) |
|
1149 (*------------------------------------------------------------------------------------*) |
|
1150 |
|
1151 |
|
1152 Goalw [CLIM_def] |
|
1153 "[| ALL x. x ~= a --> (f x = g x) |] \ |
|
1154 \ ==> (f -- a --C> l) = (g -- a --C> l)"; |
|
1155 by (auto_tac (claset(), simpset() addsimps [complex_add_minus_iff])); |
|
1156 qed "CLIM_equal"; |
|
1157 |
|
1158 Goal "[| (%x. f(x) + -g(x)) -- a --C> 0; \ |
|
1159 \ g -- a --C> l |] \ |
|
1160 \ ==> f -- a --C> l"; |
|
1161 by (dtac CLIM_add 1 THEN assume_tac 1); |
|
1162 by (auto_tac (claset(), simpset() addsimps [complex_add_assoc])); |
|
1163 qed "CLIM_trans"; |
|
1164 |
|
1165 Goal "(CDERIV f x :> l) = \ |
|
1166 \ (EX g. (ALL z. f z - f x = g z * (z - x)) & isContc g x & g x = l)"; |
|
1167 by (Step_tac 1); |
|
1168 by (res_inst_tac |
|
1169 [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1); |
|
1170 by (auto_tac (claset(),simpset() addsimps [complex_mult_assoc, |
|
1171 CLAIM "z ~= x ==> z - x ~= (0::complex)"])); |
|
1172 by (auto_tac (claset(),simpset() addsimps [isContc_iff,CDERIV_iff])); |
|
1173 by (ALLGOALS(rtac (CLIM_equal RS iffD1))); |
|
1174 by Auto_tac; |
|
1175 qed "CARAT_CDERIV"; |
|
1176 |
|
1177 Goal "NSCDERIV f x :> l ==> \ |
|
1178 \ EX g. (ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"; |
|
1179 by (auto_tac (claset(),simpset() addsimps [NSCDERIV_CDERIV_iff, |
|
1180 isNSContc_isContc_iff,CARAT_CDERIV])); |
|
1181 qed "CARAT_NSCDERIV"; |
|
1182 |
|
1183 (* How about a NS proof? *) |
|
1184 Goal "(ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l \ |
|
1185 \ ==> NSCDERIV f x :> l"; |
|
1186 by (auto_tac (claset(), |
|
1187 simpset() delsimprocs complex_cancel_factor |
|
1188 addsimps [NSCDERIV_iff2])); |
|
1189 by (asm_full_simp_tac (simpset() addsimps [isNSContc_def]) 1); |
|
1190 qed "CARAT_CDERIVD"; |
|
1191 |