13957
|
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);
|
14320
|
471 |
by Safe_tac;
|
13957
|
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);
|
14320
|
476 |
by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3);
|
13957
|
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);
|
14320
|
750 |
by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1);
|
|
751 |
by (asm_full_simp_tac (simpset() addsimps compare_rls) 2);
|
13957
|
752 |
by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1);
|
|
753 |
by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2);
|
|
754 |
by (auto_tac (claset(),simpset() addsimps
|
|
755 |
[mem_cinfmal_iff RS sym,hcomplex_add_commute]));
|
|
756 |
by (dres_inst_tac [("c","xa + - hcomplex_of_complex x")] capprox_mult1 1);
|
|
757 |
by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite
|
|
758 |
RS subsetD],simpset() addsimps [hcomplex_mult_assoc]));
|
|
759 |
by (dres_inst_tac [("x3","D")] (CFinite_hcomplex_of_complex RSN
|
|
760 |
(2,CInfinitesimal_CFinite_mult) RS (mem_cinfmal_iff RS iffD1)) 1);
|
|
761 |
by (blast_tac (claset() addIs [capprox_trans,hcomplex_mult_commute RS subst,
|
|
762 |
(capprox_minus_iff RS iffD2)]) 1);
|
|
763 |
qed "NSCDERIV_isNSContc";
|
|
764 |
|
|
765 |
Goal "CDERIV f x :> D ==> isContc f x";
|
|
766 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym,
|
|
767 |
isNSContc_isContc_iff RS sym,NSCDERIV_isNSContc]) 1);
|
|
768 |
qed "CDERIV_isContc";
|
|
769 |
|
|
770 |
(*------------------------------------------------------------------------------------*)
|
|
771 |
(* Differentiation rules for combinations of functions follow from clear, *)
|
|
772 |
(* straightforard, algebraic manipulations *)
|
|
773 |
(*------------------------------------------------------------------------------------*)
|
|
774 |
|
|
775 |
(* use simple constant nslimit theorem *)
|
|
776 |
Goal "(NSCDERIV (%x. k) x :> 0)";
|
|
777 |
by (simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff]) 1);
|
|
778 |
qed "NSCDERIV_const";
|
|
779 |
Addsimps [NSCDERIV_const];
|
|
780 |
|
|
781 |
Goal "(CDERIV (%x. k) x :> 0)";
|
|
782 |
by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1);
|
|
783 |
qed "CDERIV_const";
|
|
784 |
Addsimps [CDERIV_const];
|
|
785 |
|
|
786 |
Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \
|
|
787 |
\ ==> NSCDERIV (%x. f x + g x) x :> Da + Db";
|
|
788 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,
|
|
789 |
NSCLIM_def]) 1 THEN REPEAT(Step_tac 1));
|
|
790 |
by (auto_tac (claset(),
|
|
791 |
simpset() addsimps [hcomplex_add_divide_distrib,hcomplex_diff_def]));
|
|
792 |
by (dres_inst_tac [("b","hcomplex_of_complex Da"),
|
|
793 |
("d","hcomplex_of_complex Db")] capprox_add 1);
|
|
794 |
by (auto_tac (claset(), simpset() addsimps hcomplex_add_ac));
|
|
795 |
qed "NSCDERIV_add";
|
|
796 |
|
|
797 |
Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \
|
|
798 |
\ ==> CDERIV (%x. f x + g x) x :> Da + Db";
|
|
799 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_add,
|
|
800 |
NSCDERIV_CDERIV_iff RS sym]) 1);
|
|
801 |
qed "CDERIV_add";
|
|
802 |
|
|
803 |
(*** lemmas for multiplication ***)
|
|
804 |
|
|
805 |
Goal "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))";
|
|
806 |
by (simp_tac (simpset() addsimps [hcomplex_diff_mult_distrib2]) 1);
|
|
807 |
val lemma_nscderiv1 = result();
|
|
808 |
|
|
809 |
Goal "[| (x + y) / z = hcomplex_of_complex D + yb; z ~= 0; \
|
|
810 |
\ z : CInfinitesimal; yb : CInfinitesimal |] \
|
|
811 |
\ ==> x + y @c= 0";
|
|
812 |
by (forw_inst_tac [("c1","z")] (hcomplex_mult_right_cancel RS iffD2) 1
|
|
813 |
THEN assume_tac 1);
|
|
814 |
by (thin_tac "(x + y) / z = hcomplex_of_complex D + yb" 1);
|
|
815 |
by (auto_tac (claset() addSIs [CInfinitesimal_CFinite_mult2, CFinite_add],
|
|
816 |
simpset() addsimps [mem_cinfmal_iff RS sym]));
|
|
817 |
by (etac (CInfinitesimal_subset_CFinite RS subsetD) 1);
|
|
818 |
val lemma_nscderiv2 = result();
|
|
819 |
|
|
820 |
Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \
|
|
821 |
\ ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
|
|
822 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def]) 1
|
|
823 |
THEN REPEAT(Step_tac 1));
|
|
824 |
by (auto_tac (claset(),
|
|
825 |
simpset() addsimps [starfunC_lambda_cancel, lemma_nscderiv1,
|
|
826 |
hcomplex_of_complex_zero]));
|
|
827 |
by (simp_tac (simpset() addsimps [hcomplex_add_divide_distrib]) 1);
|
|
828 |
by (REPEAT(dtac (bex_CInfinitesimal_iff2 RS iffD2) 1));
|
|
829 |
by (auto_tac (claset(),
|
14318
|
830 |
simpset() delsimps [times_divide_eq_right]
|
|
831 |
addsimps [times_divide_eq_right RS sym]));
|
13957
|
832 |
by (rewtac hcomplex_diff_def);
|
|
833 |
by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1);
|
|
834 |
by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4);
|
|
835 |
by (auto_tac (claset() addSIs [capprox_add_mono1],
|
|
836 |
simpset() addsimps [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2,
|
|
837 |
hcomplex_mult_commute, hcomplex_add_assoc]));
|
|
838 |
by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
|
|
839 |
(hcomplex_add_commute RS subst) 1);
|
|
840 |
by (auto_tac (claset() addSIs [CInfinitesimal_add_capprox_self2 RS capprox_sym,
|
|
841 |
CInfinitesimal_add, CInfinitesimal_mult,
|
|
842 |
CInfinitesimal_hcomplex_of_complex_mult,
|
|
843 |
CInfinitesimal_hcomplex_of_complex_mult2],
|
|
844 |
simpset() addsimps [hcomplex_add_assoc RS sym]));
|
|
845 |
qed "NSCDERIV_mult";
|
|
846 |
|
|
847 |
Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \
|
|
848 |
\ ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
|
|
849 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_mult,
|
|
850 |
NSCDERIV_CDERIV_iff RS sym]) 1);
|
|
851 |
qed "CDERIV_mult";
|
|
852 |
|
|
853 |
Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D";
|
|
854 |
by (asm_full_simp_tac
|
|
855 |
(simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff,
|
|
856 |
complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym,
|
|
857 |
complex_diff_def]
|
|
858 |
delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]) 1);
|
|
859 |
by (etac (NSCLIM_const RS NSCLIM_mult) 1);
|
|
860 |
qed "NSCDERIV_cmult";
|
|
861 |
|
|
862 |
Goal "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D";
|
|
863 |
by (auto_tac (claset(),simpset() addsimps [NSCDERIV_cmult,NSCDERIV_CDERIV_iff
|
|
864 |
RS sym]));
|
|
865 |
qed "CDERIV_cmult";
|
|
866 |
|
|
867 |
Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D";
|
|
868 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1);
|
|
869 |
by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1);
|
|
870 |
by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym]
|
|
871 |
delsimps [complex_minus_add_distrib, complex_minus_minus]) 1);
|
|
872 |
by (etac NSCLIM_minus 1);
|
|
873 |
qed "NSCDERIV_minus";
|
|
874 |
|
|
875 |
Goal "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D";
|
|
876 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_minus,NSCDERIV_CDERIV_iff RS sym]) 1);
|
|
877 |
qed "CDERIV_minus";
|
|
878 |
|
|
879 |
Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \
|
|
880 |
\ ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db";
|
|
881 |
by (blast_tac (claset() addDs [NSCDERIV_add,NSCDERIV_minus]) 1);
|
|
882 |
qed "NSCDERIV_add_minus";
|
|
883 |
|
|
884 |
Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \
|
|
885 |
\ ==> CDERIV (%x. f x + -g x) x :> Da + -Db";
|
|
886 |
by (blast_tac (claset() addDs [CDERIV_add,CDERIV_minus]) 1);
|
|
887 |
qed "CDERIV_add_minus";
|
|
888 |
|
|
889 |
Goalw [complex_diff_def]
|
|
890 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \
|
|
891 |
\ ==> NSCDERIV (%x. f x - g x) x :> Da - Db";
|
|
892 |
by (blast_tac (claset() addIs [NSCDERIV_add_minus]) 1);
|
|
893 |
qed "NSCDERIV_diff";
|
|
894 |
|
|
895 |
Goalw [complex_diff_def]
|
|
896 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] \
|
|
897 |
\ ==> CDERIV (%x. f x - g x) x :> Da - Db";
|
|
898 |
by (blast_tac (claset() addIs [CDERIV_add_minus]) 1);
|
|
899 |
qed "CDERIV_diff";
|
|
900 |
|
|
901 |
|
|
902 |
(*--------------------------------------------------*)
|
|
903 |
(* Chain rule *)
|
|
904 |
(*--------------------------------------------------*)
|
|
905 |
|
|
906 |
(* lemmas *)
|
|
907 |
Goalw [nscderiv_def]
|
|
908 |
"[| NSCDERIV g x :> D; \
|
|
909 |
\ ( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);\
|
|
910 |
\ xa : CInfinitesimal; xa ~= 0 \
|
|
911 |
\ |] ==> D = 0";
|
|
912 |
by (dtac bspec 1);
|
|
913 |
by Auto_tac;
|
|
914 |
qed "NSCDERIV_zero";
|
|
915 |
|
|
916 |
Goalw [nscderiv_def]
|
|
917 |
"[| NSCDERIV f x :> D; h: CInfinitesimal; h ~= 0 |] \
|
|
918 |
\ ==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0";
|
|
919 |
by (asm_full_simp_tac (simpset() addsimps [mem_cinfmal_iff RS sym]) 1);
|
|
920 |
by (rtac CInfinitesimal_ratio 1);
|
|
921 |
by (rtac capprox_hcomplex_of_complex_CFinite 3);
|
|
922 |
by Auto_tac;
|
|
923 |
qed "NSCDERIV_capprox";
|
|
924 |
|
|
925 |
|
|
926 |
(*--------------------------------------------------*)
|
|
927 |
(* from one version of differentiability *)
|
|
928 |
(* *)
|
|
929 |
(* f(x) - f(a) *)
|
|
930 |
(* --------------- @= Db *)
|
|
931 |
(* x - a *)
|
|
932 |
(* -------------------------------------------------*)
|
|
933 |
|
|
934 |
Goal "[| NSCDERIV f (g x) :> Da; \
|
|
935 |
\ ( *fc* g) (hcomplex_of_complex(x) + xa) ~= hcomplex_of_complex (g x); \
|
|
936 |
\ ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x) \
|
|
937 |
\ |] ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa)) \
|
|
938 |
\ - hcomplex_of_complex (f (g x))) \
|
|
939 |
\ / (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) \
|
|
940 |
\ @c= hcomplex_of_complex (Da)";
|
|
941 |
by (auto_tac (claset(),simpset() addsimps [NSCDERIV_NSCLIM_iff2, NSCLIM_def]));
|
|
942 |
qed "NSCDERIVD1";
|
|
943 |
|
|
944 |
(*--------------------------------------------------*)
|
|
945 |
(* from other version of differentiability *)
|
|
946 |
(* *)
|
|
947 |
(* f(x + h) - f(x) *)
|
|
948 |
(* ----------------- @= Db *)
|
|
949 |
(* h *)
|
|
950 |
(*--------------------------------------------------*)
|
|
951 |
|
|
952 |
Goal "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa ~= 0 |] \
|
|
953 |
\ ==> (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex(g x)) / xa \
|
|
954 |
\ @c= hcomplex_of_complex (Db)";
|
|
955 |
by (auto_tac (claset(),
|
|
956 |
simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def,
|
|
957 |
mem_cinfmal_iff, starfunC_lambda_cancel]));
|
|
958 |
qed "NSCDERIVD2";
|
|
959 |
|
|
960 |
Goal "(z::hcomplex) ~= 0 ==> x*y = (x*inverse(z))*(z*y)";
|
|
961 |
by Auto_tac;
|
|
962 |
qed "lemma_complex_chain";
|
|
963 |
|
|
964 |
(*** chain rule ***)
|
|
965 |
|
|
966 |
Goal "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] \
|
|
967 |
\ ==> NSCDERIV (f o g) x :> Da * Db";
|
|
968 |
by (asm_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,
|
|
969 |
NSCLIM_def,mem_cinfmal_iff RS sym]) 1 THEN Step_tac 1);
|
|
970 |
by (forw_inst_tac [("f","g")] NSCDERIV_capprox 1);
|
|
971 |
by (auto_tac (claset(),
|
|
972 |
simpset() addsimps [starfunC_lambda_cancel2, starfunC_o RS sym]));
|
|
973 |
by (case_tac "( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex (g x)" 1);
|
|
974 |
by (dres_inst_tac [("g","g")] NSCDERIV_zero 1);
|
|
975 |
by (auto_tac (claset(),simpset() addsimps [hcomplex_divide_def]));
|
|
976 |
by (res_inst_tac [("z1","( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)"),
|
|
977 |
("y1","inverse xa")] (lemma_complex_chain RS ssubst) 1);
|
|
978 |
by (Asm_simp_tac 1);
|
|
979 |
by (rtac capprox_mult_hcomplex_of_complex 1);
|
|
980 |
by (fold_tac [hcomplex_divide_def]);
|
|
981 |
by (blast_tac (claset() addIs [NSCDERIVD2]) 2);
|
|
982 |
by (auto_tac (claset() addSIs [NSCDERIVD1] addIs [capprox_minus_iff RS iffD2],
|
|
983 |
simpset() addsimps [symmetric hcomplex_diff_def]));
|
|
984 |
qed "NSCDERIV_chain";
|
|
985 |
|
|
986 |
(* standard version *)
|
|
987 |
Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \
|
|
988 |
\ ==> CDERIV (f o g) x :> Da * Db";
|
|
989 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym,
|
|
990 |
NSCDERIV_chain]) 1);
|
|
991 |
qed "CDERIV_chain";
|
|
992 |
|
|
993 |
Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \
|
|
994 |
\ ==> CDERIV (%x. f (g x)) x :> Da * Db";
|
|
995 |
by (auto_tac (claset() addDs [CDERIV_chain], simpset() addsimps [o_def]));
|
|
996 |
qed "CDERIV_chain2";
|
|
997 |
|
|
998 |
(*------------------------------------------------------------------------------------*)
|
|
999 |
(* Differentiation of natural number powers *)
|
|
1000 |
(*------------------------------------------------------------------------------------*)
|
|
1001 |
|
|
1002 |
Goal "NSCDERIV (%x. x) x :> 1";
|
|
1003 |
by (auto_tac (claset(),
|
|
1004 |
simpset() addsimps [NSCDERIV_NSCLIM_iff,NSCLIM_def]));
|
|
1005 |
qed "NSCDERIV_Id";
|
|
1006 |
Addsimps [NSCDERIV_Id];
|
|
1007 |
|
|
1008 |
Goal "CDERIV (%x. x) x :> 1";
|
|
1009 |
by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1);
|
|
1010 |
qed "CDERIV_Id";
|
|
1011 |
Addsimps [CDERIV_Id];
|
|
1012 |
|
|
1013 |
bind_thm ("isContc_Id", CDERIV_Id RS CDERIV_isContc);
|
|
1014 |
|
|
1015 |
(*derivative of linear multiplication*)
|
|
1016 |
Goal "CDERIV (op * c) x :> c";
|
|
1017 |
by (cut_inst_tac [("c","c"),("x","x")] (CDERIV_Id RS CDERIV_cmult) 1);
|
|
1018 |
by (Asm_full_simp_tac 1);
|
|
1019 |
qed "CDERIV_cmult_Id";
|
|
1020 |
Addsimps [CDERIV_cmult_Id];
|
|
1021 |
|
|
1022 |
Goal "NSCDERIV (op * c) x :> c";
|
|
1023 |
by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1);
|
|
1024 |
qed "NSCDERIV_cmult_Id";
|
|
1025 |
Addsimps [NSCDERIV_cmult_Id];
|
|
1026 |
|
|
1027 |
Goal "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - 1))";
|
|
1028 |
by (induct_tac "n" 1);
|
|
1029 |
by (dtac (CDERIV_Id RS CDERIV_mult) 2);
|
|
1030 |
by (auto_tac (claset(),
|
|
1031 |
simpset() addsimps [complex_of_real_add RS sym,
|
|
1032 |
complex_add_mult_distrib,real_of_nat_Suc] delsimps [complex_of_real_add]));
|
|
1033 |
by (case_tac "n" 1);
|
|
1034 |
by (auto_tac (claset(),
|
|
1035 |
simpset() addsimps [complex_mult_assoc, complex_add_commute]));
|
|
1036 |
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
|
|
1037 |
qed "CDERIV_pow";
|
|
1038 |
Addsimps [CDERIV_pow,simplify (simpset()) CDERIV_pow];
|
|
1039 |
|
|
1040 |
(* NS version *)
|
|
1041 |
Goal "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))";
|
|
1042 |
by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1);
|
|
1043 |
qed "NSCDERIV_pow";
|
|
1044 |
|
14320
|
1045 |
Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E";
|
13957
|
1046 |
by Auto_tac;
|
|
1047 |
qed "lemma_CDERIV_subst";
|
|
1048 |
|
|
1049 |
(*used once, in NSCDERIV_inverse*)
|
|
1050 |
Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0";
|
14320
|
1051 |
by (Clarify_tac 1);
|
|
1052 |
by (dtac (thm"equals_zero_I") 1);
|
13957
|
1053 |
by Auto_tac;
|
|
1054 |
qed "CInfinitesimal_add_not_zero";
|
|
1055 |
|
|
1056 |
(*Can't get rid of x ~= 0 because it isn't continuous at zero*)
|
|
1057 |
|
|
1058 |
Goalw [nscderiv_def]
|
|
1059 |
"x ~= 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
|
|
1060 |
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
|
|
1061 |
by (forward_tac [CInfinitesimal_add_not_zero] 1);
|
14323
|
1062 |
by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2);
|
13957
|
1063 |
by (auto_tac (claset(),
|
|
1064 |
simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def]
|
|
1065 |
delsimps [hcomplex_minus_mult_eq1 RS sym,
|
|
1066 |
hcomplex_minus_mult_eq2 RS sym]));
|
|
1067 |
by (asm_simp_tac
|
14320
|
1068 |
(simpset() addsimps [inverse_add,
|
14318
|
1069 |
inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym]
|
13957
|
1070 |
@ hcomplex_add_ac @ hcomplex_mult_ac
|
14318
|
1071 |
delsimps [thm"Ring_and_Field.inverse_minus_eq",
|
|
1072 |
inverse_mult_distrib, hcomplex_minus_mult_eq1 RS sym,
|
13957
|
1073 |
hcomplex_minus_mult_eq2 RS sym] ) 1);
|
|
1074 |
by (asm_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym,
|
|
1075 |
hcomplex_add_mult_distrib2]
|
|
1076 |
delsimps [hcomplex_minus_mult_eq1 RS sym,
|
|
1077 |
hcomplex_minus_mult_eq2 RS sym]) 1);
|
|
1078 |
by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")]
|
|
1079 |
capprox_trans 1);
|
|
1080 |
by (rtac inverse_add_CInfinitesimal_capprox2 1);
|
|
1081 |
by (auto_tac (claset() addSDs [hcomplex_of_complex_CFinite_diff_CInfinitesimal] addIs [CFinite_mult],
|
|
1082 |
simpset() addsimps [hcomplex_minus_inverse RS sym]));
|
|
1083 |
by (rtac CInfinitesimal_CFinite_mult2 1);
|
|
1084 |
by Auto_tac;
|
|
1085 |
qed "NSCDERIV_inverse";
|
|
1086 |
|
|
1087 |
Goal "x ~= 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
|
|
1088 |
by (asm_simp_tac (simpset() addsimps [NSCDERIV_inverse,
|
|
1089 |
NSCDERIV_CDERIV_iff RS sym] delsimps [complexpow_Suc]) 1);
|
|
1090 |
qed "CDERIV_inverse";
|
|
1091 |
|
|
1092 |
|
|
1093 |
(*------------------------------------------------------------------------------------*)
|
|
1094 |
(* Derivative of inverse *)
|
|
1095 |
(*------------------------------------------------------------------------------------*)
|
|
1096 |
|
|
1097 |
Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \
|
|
1098 |
\ ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
|
|
1099 |
by (rtac (complex_mult_commute RS subst) 1);
|
|
1100 |
by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
|
|
1101 |
complexpow_inverse] delsimps [complexpow_Suc,
|
|
1102 |
complex_minus_mult_eq1 RS sym]) 1);
|
|
1103 |
by (fold_goals_tac [o_def]);
|
|
1104 |
by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
|
|
1105 |
qed "CDERIV_inverse_fun";
|
|
1106 |
|
|
1107 |
Goal "[| NSCDERIV f x :> d; f(x) ~= 0 |] \
|
|
1108 |
\ ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
|
|
1109 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff,
|
|
1110 |
CDERIV_inverse_fun] delsimps [complexpow_Suc]) 1);
|
|
1111 |
qed "NSCDERIV_inverse_fun";
|
|
1112 |
|
|
1113 |
(*------------------------------------------------------------------------------------*)
|
|
1114 |
(* Derivative of quotient *)
|
|
1115 |
(*------------------------------------------------------------------------------------*)
|
|
1116 |
|
|
1117 |
|
|
1118 |
Goal "x ~= (0::complex) \\<Longrightarrow> (x * inverse(x) ^ 2) = inverse x";
|
14323
|
1119 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
|
13957
|
1120 |
qed "lemma_complex_mult_inverse_squared";
|
|
1121 |
Addsimps [lemma_complex_mult_inverse_squared];
|
|
1122 |
|
|
1123 |
Goalw [complex_diff_def]
|
|
1124 |
"[| CDERIV f x :> d; CDERIV g x :> e; g(x) ~= 0 |] \
|
|
1125 |
\ ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)";
|
|
1126 |
by (dres_inst_tac [("f","g")] CDERIV_inverse_fun 1);
|
|
1127 |
by (dtac CDERIV_mult 2);
|
|
1128 |
by (REPEAT(assume_tac 1));
|
|
1129 |
by (asm_full_simp_tac
|
|
1130 |
(simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
|
|
1131 |
complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac
|
|
1132 |
delsimps [complexpow_Suc, complex_minus_mult_eq1 RS sym,
|
|
1133 |
complex_minus_mult_eq2 RS sym]) 1);
|
|
1134 |
qed "CDERIV_quotient";
|
|
1135 |
|
|
1136 |
Goal "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) ~= 0 |] \
|
|
1137 |
\ ==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)";
|
|
1138 |
by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff,
|
|
1139 |
CDERIV_quotient] delsimps [complexpow_Suc]) 1);
|
|
1140 |
qed "NSCDERIV_quotient";
|
|
1141 |
|
|
1142 |
|
|
1143 |
(*------------------------------------------------------------------------------------*)
|
|
1144 |
(* Caratheodory formulation of derivative at a point: standard proof *)
|
|
1145 |
(*------------------------------------------------------------------------------------*)
|
|
1146 |
|
|
1147 |
|
|
1148 |
Goalw [CLIM_def]
|
|
1149 |
"[| ALL x. x ~= a --> (f x = g x) |] \
|
|
1150 |
\ ==> (f -- a --C> l) = (g -- a --C> l)";
|
|
1151 |
by (auto_tac (claset(), simpset() addsimps [complex_add_minus_iff]));
|
|
1152 |
qed "CLIM_equal";
|
|
1153 |
|
|
1154 |
Goal "[| (%x. f(x) + -g(x)) -- a --C> 0; \
|
|
1155 |
\ g -- a --C> l |] \
|
|
1156 |
\ ==> f -- a --C> l";
|
|
1157 |
by (dtac CLIM_add 1 THEN assume_tac 1);
|
|
1158 |
by (auto_tac (claset(), simpset() addsimps [complex_add_assoc]));
|
|
1159 |
qed "CLIM_trans";
|
|
1160 |
|
|
1161 |
Goal "(CDERIV f x :> l) = \
|
|
1162 |
\ (EX g. (ALL z. f z - f x = g z * (z - x)) & isContc g x & g x = l)";
|
|
1163 |
by (Step_tac 1);
|
|
1164 |
by (res_inst_tac
|
|
1165 |
[("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
|
|
1166 |
by (auto_tac (claset(),simpset() addsimps [complex_mult_assoc,
|
|
1167 |
CLAIM "z ~= x ==> z - x ~= (0::complex)"]));
|
|
1168 |
by (auto_tac (claset(),simpset() addsimps [isContc_iff,CDERIV_iff]));
|
|
1169 |
by (ALLGOALS(rtac (CLIM_equal RS iffD1)));
|
|
1170 |
by Auto_tac;
|
|
1171 |
qed "CARAT_CDERIV";
|
|
1172 |
|
|
1173 |
Goal "NSCDERIV f x :> l ==> \
|
|
1174 |
\ EX g. (ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l";
|
|
1175 |
by (auto_tac (claset(),simpset() addsimps [NSCDERIV_CDERIV_iff,
|
|
1176 |
isNSContc_isContc_iff,CARAT_CDERIV]));
|
|
1177 |
qed "CARAT_NSCDERIV";
|
|
1178 |
|
|
1179 |
(* How about a NS proof? *)
|
|
1180 |
Goal "(ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l \
|
|
1181 |
\ ==> NSCDERIV f x :> l";
|
|
1182 |
by (auto_tac (claset(),
|
|
1183 |
simpset() delsimprocs complex_cancel_factor
|
|
1184 |
addsimps [NSCDERIV_iff2]));
|
|
1185 |
by (asm_full_simp_tac (simpset() addsimps [isNSContc_def]) 1);
|
|
1186 |
qed "CARAT_CDERIVD";
|
|
1187 |
|