|
1 (* Title : Lim.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Theory of limits, continuity and |
|
5 differentiation of real=>real functions |
|
6 *) |
|
7 |
|
8 |
|
9 fun ARITH_PROVE str = prove_goal thy str |
|
10 (fn prems => [cut_facts_tac prems 1,arith_tac 1]); |
|
11 |
|
12 (*--------------------------------------------------------------- |
|
13 Theory of limits, continuity and differentiation of |
|
14 real=>real functions |
|
15 ----------------------------------------------------------------*) |
|
16 Goalw [LIM_def] "(f -- a --> L) = (ALL r. #0 < r --> \ |
|
17 \ (EX s. #0 < s & (ALL x. (#0 < abs(x + -a) & (abs(x + -a) < s) \ |
|
18 \ --> abs(f x + -L) < r))))"; |
|
19 by (Blast_tac 1); |
|
20 qed "LIM_iff"; |
|
21 |
|
22 Goalw [LIM_def] |
|
23 "!!a. [| f -- a --> L; #0 < r |] \ |
|
24 \ ==> (EX s. #0 < s & (ALL x. (#0 < abs(x + -a) \ |
|
25 \ & (abs(x + -a) < s) --> abs(f x + -L) < r)))"; |
|
26 by (Blast_tac 1); |
|
27 qed "LIMD"; |
|
28 |
|
29 Goalw [LIM_def] "(%x. k) -- x --> k"; |
|
30 by (Auto_tac); |
|
31 qed "LIM_const"; |
|
32 Addsimps [LIM_const]; |
|
33 |
|
34 (***-----------------------------------------------------------***) |
|
35 (*** Some Purely Standard Proofs - Can be used for comparison ***) |
|
36 (***-----------------------------------------------------------***) |
|
37 |
|
38 (*--------------- |
|
39 LIM_add |
|
40 ---------------*) |
|
41 Goalw [LIM_def] |
|
42 "[| f -- x --> l; g -- x --> m |] \ |
|
43 \ ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
|
44 by (Step_tac 1); |
|
45 by (REPEAT(dres_inst_tac [("x","r*rinv(#1 + #1)")] spec 1)); |
|
46 by (dtac (rename_numerals (real_zero_less_two RS real_rinv_gt_zero |
|
47 RSN (2,real_mult_less_mono2))) 1); |
|
48 by (Asm_full_simp_tac 1); |
|
49 by (Clarify_tac 1); |
|
50 by (res_inst_tac [("R1.0","s"),("R2.0","sa")] |
|
51 real_linear_less2 1); |
|
52 by (res_inst_tac [("x","s")] exI 1); |
|
53 by (res_inst_tac [("x","sa")] exI 2); |
|
54 by (res_inst_tac [("x","sa")] exI 3); |
|
55 by (Step_tac 1); |
|
56 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
|
57 THEN step_tac (claset() addSEs [real_less_trans]) 1); |
|
58 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
|
59 THEN step_tac (claset() addSEs [real_less_trans]) 2); |
|
60 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
|
61 THEN step_tac (claset() addSEs [real_less_trans]) 3); |
|
62 by (ALLGOALS(rtac (abs_sum_triangle_ineq RS real_le_less_trans))); |
|
63 by (ALLGOALS(rtac (real_sum_of_halves RS subst))); |
|
64 by (auto_tac (claset() addIs [real_add_less_mono],simpset())); |
|
65 qed "LIM_add"; |
|
66 |
|
67 Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; |
|
68 by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym, |
|
69 abs_minus_cancel] delsimps [real_minus_add_distrib,real_minus_minus]) 1); |
|
70 qed "LIM_minus"; |
|
71 |
|
72 (*---------------------------------------------- |
|
73 LIM_add_minus |
|
74 ----------------------------------------------*) |
|
75 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
76 \ ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"; |
|
77 by (blast_tac (claset() addDs [LIM_add,LIM_minus]) 1); |
|
78 qed "LIM_add_minus"; |
|
79 |
|
80 (*---------------------------------------------- |
|
81 LIM_zero |
|
82 ----------------------------------------------*) |
|
83 Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0"; |
|
84 by (res_inst_tac [("z1","l")] (rename_numerals |
|
85 (real_add_minus RS subst)) 1); |
|
86 by (rtac LIM_add_minus 1 THEN Auto_tac); |
|
87 qed "LIM_zero"; |
|
88 |
|
89 (*-------------------------- |
|
90 Limit not zero |
|
91 --------------------------*) |
|
92 Goalw [LIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --> #0)"; |
|
93 by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1); |
|
94 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
|
95 by (dtac (rename_numerals (real_minus_zero_less_iff RS iffD2)) 1); |
|
96 by (res_inst_tac [("x","-k")] exI 1); |
|
97 by (res_inst_tac [("x","k")] exI 2); |
|
98 by Auto_tac; |
|
99 by (ALLGOALS(dres_inst_tac [("y","s")] real_dense)); |
|
100 by (Step_tac 1); |
|
101 by (ALLGOALS(res_inst_tac [("x","r + x")] exI)); |
|
102 by (auto_tac (claset(),simpset() addsimps [real_add_assoc,abs_eqI2])); |
|
103 qed "LIM_not_zero"; |
|
104 |
|
105 (* [| k ~= #0; (%x. k) -- x --> #0 |] ==> R *) |
|
106 bind_thm("LIM_not_zeroE", (LIM_not_zero RS notE)); |
|
107 |
|
108 Goal "(%x. k) -- x --> L ==> k = L"; |
|
109 by (rtac ccontr 1); |
|
110 by (dtac LIM_zero 1); |
|
111 by (rtac LIM_not_zeroE 1 THEN assume_tac 2); |
|
112 by (arith_tac 1); |
|
113 qed "LIM_const_eq"; |
|
114 |
|
115 (*------------------------ |
|
116 Limit is Unique |
|
117 ------------------------*) |
|
118 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M"; |
|
119 by (dtac LIM_minus 1); |
|
120 by (dtac LIM_add 1 THEN assume_tac 1); |
|
121 by (auto_tac (claset() addSDs [LIM_const_eq RS sym], |
|
122 simpset())); |
|
123 qed "LIM_unique"; |
|
124 |
|
125 (*------------- |
|
126 LIM_mult_zero |
|
127 -------------*) |
|
128 Goalw [LIM_def] "!!f. [| f -- x --> #0; g -- x --> #0 |] \ |
|
129 \ ==> (%x. f(x)*g(x)) -- x --> #0"; |
|
130 by (Step_tac 1); |
|
131 by (dres_inst_tac [("x","#1")] spec 1); |
|
132 by (dres_inst_tac [("x","r")] spec 1); |
|
133 by (cut_facts_tac [real_zero_less_one] 1); |
|
134 by (asm_full_simp_tac (simpset() addsimps |
|
135 [abs_mult]) 1); |
|
136 by (Clarify_tac 1); |
|
137 by (res_inst_tac [("R1.0","s"),("R2.0","sa")] |
|
138 real_linear_less2 1); |
|
139 by (res_inst_tac [("x","s")] exI 1); |
|
140 by (res_inst_tac [("x","sa")] exI 2); |
|
141 by (res_inst_tac [("x","sa")] exI 3); |
|
142 by (Step_tac 1); |
|
143 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
|
144 THEN step_tac (claset() addSEs [real_less_trans]) 1); |
|
145 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
|
146 THEN step_tac (claset() addSEs [real_less_trans]) 2); |
|
147 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
|
148 THEN step_tac (claset() addSEs [real_less_trans]) 3); |
|
149 by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst))); |
|
150 by (ALLGOALS(rtac abs_mult_less2)); |
|
151 by Auto_tac; |
|
152 qed "LIM_mult_zero"; |
|
153 |
|
154 Goalw [LIM_def] "(%x. x) -- a --> a"; |
|
155 by (Auto_tac); |
|
156 qed "LIM_self"; |
|
157 |
|
158 Goal "(#0::real) < abs (x + -a) ==> x ~= a"; |
|
159 by (arith_tac 1); |
|
160 qed "lemma_rabs_not_eq"; |
|
161 |
|
162 (*-------------------------------------------------------------- |
|
163 Limits are equal for functions equal except at limit point |
|
164 --------------------------------------------------------------*) |
|
165 Goalw [LIM_def] |
|
166 "[| ALL x. x ~= a --> (f x = g x) |] \ |
|
167 \ ==> (f -- a --> l) = (g -- a --> l)"; |
|
168 by (auto_tac (claset(),simpset() addsimps [lemma_rabs_not_eq])); |
|
169 qed "LIM_equal"; |
|
170 |
|
171 Goal "[| (%x. f(x) + -g(x)) -- a --> #0; \ |
|
172 \ g -- a --> l |] \ |
|
173 \ ==> f -- a --> l"; |
|
174 by (dtac LIM_add 1 THEN assume_tac 1); |
|
175 by (auto_tac (claset(),simpset() addsimps |
|
176 [real_add_assoc])); |
|
177 qed "LIM_trans"; |
|
178 |
|
179 (***-------------------------------------------------------------***) |
|
180 (*** End of Purely Standard Proofs ***) |
|
181 (***-------------------------------------------------------------***) |
|
182 (*-------------------------------------------------------------- |
|
183 Standard and NS definitions of Limit |
|
184 --------------------------------------------------------------*) |
|
185 Goalw [LIM_def,NSLIM_def,inf_close_def] |
|
186 "f -- x --> L ==> f -- x --NS> L"; |
|
187 by (asm_full_simp_tac (simpset() addsimps |
|
188 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
189 by (Step_tac 1); |
|
190 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
|
191 by (auto_tac (claset(),simpset() addsimps [starfun, |
|
192 hypreal_minus,hypreal_of_real_minus RS sym, |
|
193 hypreal_of_real_def,hypreal_add])); |
|
194 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1); |
|
195 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1); |
|
196 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1); |
|
197 by (subgoal_tac "ALL n::nat. (#0::real) < abs ((xa n) + - x) & \ |
|
198 \ abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u" 1); |
|
199 by (Blast_tac 2); |
|
200 by (dtac FreeUltrafilterNat_all 1); |
|
201 by (Ultra_tac 1 THEN arith_tac 1); |
|
202 qed "LIM_NSLIM"; |
|
203 |
|
204 (*--------------------------------------------------------------------- |
|
205 Limit: NS definition ==> standard definition |
|
206 ---------------------------------------------------------------------*) |
|
207 |
|
208 Goal "ALL s. #0 < s --> (EX xa. #0 < abs (xa + - x) & \ |
|
209 \ abs (xa + - x) < s & r <= abs (f xa + -L)) \ |
|
210 \ ==> ALL n::nat. EX xa. #0 < abs (xa + - x) & \ |
|
211 \ abs(xa + -x) < rinv(real_of_posnat n) & r <= abs(f xa + -L)"; |
|
212 by (Step_tac 1); |
|
213 by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_rinv_gt_zero) 1); |
|
214 by Auto_tac; |
|
215 val lemma_LIM = result(); |
|
216 |
|
217 Goal "ALL s. #0 < s --> (EX xa. #0 < abs (xa + - x) & \ |
|
218 \ abs (xa + - x) < s & r <= abs (f xa + -L)) \ |
|
219 \ ==> EX X. ALL n::nat. #0 < abs (X n + - x) & \ |
|
220 \ abs(X n + -x) < rinv(real_of_posnat n) & r <= abs(f (X n) + -L)"; |
|
221 by (dtac lemma_LIM 1); |
|
222 by (dtac choice 1); |
|
223 by (Blast_tac 1); |
|
224 val lemma_skolemize_LIM2 = result(); |
|
225 |
|
226 Goal "{n. f (X n) + - L = Y n} Int \ |
|
227 \ {n. #0 < abs (X n + - x) & \ |
|
228 \ abs (X n + - x) < rinv (real_of_posnat n) & \ |
|
229 \ r <= abs (f (X n) + - L)} <= \ |
|
230 \ {n. r <= abs (Y n)}"; |
|
231 by (Auto_tac); |
|
232 val lemma_Int = result (); |
|
233 |
|
234 Goal "!!X. ALL n. #0 < abs (X n + - x) & \ |
|
235 \ abs (X n + - x) < rinv (real_of_posnat n) & \ |
|
236 \ r <= abs (f (X n) + - L) ==> \ |
|
237 \ ALL n. abs (X n + - x) < rinv (real_of_posnat n)"; |
|
238 by (Auto_tac ); |
|
239 val lemma_simp = result(); |
|
240 |
|
241 (*------------------- |
|
242 NSLIM => LIM |
|
243 -------------------*) |
|
244 |
|
245 Goalw [LIM_def,NSLIM_def,inf_close_def] |
|
246 "!!f. f -- x --NS> L ==> f -- x --> L"; |
|
247 by (asm_full_simp_tac (simpset() addsimps |
|
248 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
249 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
|
250 by (fold_tac [real_le_def]); |
|
251 by (dtac lemma_skolemize_LIM2 1); |
|
252 by (Step_tac 1); |
|
253 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1); |
|
254 by (asm_full_simp_tac (simpset() addsimps [starfun, |
|
255 hypreal_minus,hypreal_of_real_minus RS sym, |
|
256 hypreal_of_real_def,hypreal_add]) 1); |
|
257 by (Step_tac 1); |
|
258 by (dtac FreeUltrafilterNat_Ex_P 1 THEN etac exE 1); |
|
259 by (dres_inst_tac [("x","n")] spec 1); |
|
260 by (asm_full_simp_tac (simpset() addsimps |
|
261 [real_add_minus,real_less_not_refl]) 1); |
|
262 by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1); |
|
263 by (asm_full_simp_tac (simpset() addsimps |
|
264 [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def, |
|
265 hypreal_minus,hypreal_of_real_minus,hypreal_add]) 1); |
|
266 by (rotate_tac 2 1); |
|
267 by (dres_inst_tac [("x","r")] spec 1); |
|
268 by (Clarify_tac 1); |
|
269 by (dtac FreeUltrafilterNat_all 1); |
|
270 by (Ultra_tac 1); |
|
271 qed "NSLIM_LIM"; |
|
272 |
|
273 (**** Key result ****) |
|
274 Goal "(f -- x --> L) = (f -- x --NS> L)"; |
|
275 by (blast_tac (claset() addIs [LIM_NSLIM,NSLIM_LIM]) 1); |
|
276 qed "LIM_NSLIM_iff"; |
|
277 |
|
278 (*-------------------------------------------------------------------*) |
|
279 (* Proving properties of limits using nonstandard definition and *) |
|
280 (* hence, the properties hold for standard limits as well *) |
|
281 (*-------------------------------------------------------------------*) |
|
282 (*------------------------------------------------ |
|
283 NSLIM_mult and hence (trivially) LIM_mult |
|
284 ------------------------------------------------*) |
|
285 |
|
286 Goalw [NSLIM_def] |
|
287 "[| f -- x --NS> l; g -- x --NS> m |] \ |
|
288 \ ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"; |
|
289 by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close], |
|
290 simpset() addsimps [hypreal_of_real_mult])); |
|
291 qed "NSLIM_mult"; |
|
292 |
|
293 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
294 \ ==> (%x. f(x) * g(x)) -- x --> (l * m)"; |
|
295 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
296 NSLIM_mult]) 1); |
|
297 qed "LIM_mult2"; |
|
298 |
|
299 (*---------------------------------------------- |
|
300 NSLIM_add and hence (trivially) LIM_add |
|
301 Note the much shorter proof |
|
302 ----------------------------------------------*) |
|
303 Goalw [NSLIM_def] |
|
304 "[| f -- x --NS> l; g -- x --NS> m |] \ |
|
305 \ ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"; |
|
306 by (auto_tac (claset() addSIs [starfun_add_inf_close], |
|
307 simpset() addsimps [hypreal_of_real_add])); |
|
308 qed "NSLIM_add"; |
|
309 |
|
310 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
311 \ ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
|
312 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
313 NSLIM_add]) 1); |
|
314 qed "LIM_add2"; |
|
315 |
|
316 (*---------------------------------------------- |
|
317 NSLIM_const |
|
318 ----------------------------------------------*) |
|
319 Goalw [NSLIM_def] "(%x. k) -- x --NS> k"; |
|
320 by (Auto_tac); |
|
321 qed "NSLIM_const"; |
|
322 |
|
323 Addsimps [NSLIM_const]; |
|
324 |
|
325 Goal "(%x. k) -- x --> k"; |
|
326 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
327 qed "LIM_const2"; |
|
328 |
|
329 (*---------------------------------------------- |
|
330 NSLIM_minus |
|
331 ----------------------------------------------*) |
|
332 Goalw [NSLIM_def] |
|
333 "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"; |
|
334 by (auto_tac (claset() addIs [inf_close_minus], |
|
335 simpset() addsimps [starfun_minus RS sym, |
|
336 hypreal_of_real_minus])); |
|
337 qed "NSLIM_minus"; |
|
338 |
|
339 Goal "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; |
|
340 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
341 NSLIM_minus]) 1); |
|
342 qed "LIM_minus2"; |
|
343 |
|
344 (*---------------------------------------------- |
|
345 NSLIM_add_minus |
|
346 ----------------------------------------------*) |
|
347 Goal "!!f. [| f -- x --NS> l; g -- x --NS> m |] \ |
|
348 \ ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"; |
|
349 by (blast_tac (claset() addDs [NSLIM_add,NSLIM_minus]) 1); |
|
350 qed "NSLIM_add_minus"; |
|
351 |
|
352 Goal "!!f. [| f -- x --> l; g -- x --> m |] \ |
|
353 \ ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"; |
|
354 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
355 NSLIM_add_minus]) 1); |
|
356 qed "LIM_add_minus2"; |
|
357 |
|
358 (*----------------------------- |
|
359 NSLIM_rinv |
|
360 -----------------------------*) |
|
361 Goalw [NSLIM_def] |
|
362 "!!f. [| f -- a --NS> L; \ |
|
363 \ L ~= #0 \ |
|
364 \ |] ==> (%x. rinv(f(x))) -- a --NS> (rinv L)"; |
|
365 by (Step_tac 1); |
|
366 by (dtac spec 1 THEN auto_tac (claset(),simpset() |
|
367 addsimps [hypreal_of_real_not_zero_iff RS sym, |
|
368 hypreal_of_real_hrinv RS sym])); |
|
369 by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 |
|
370 THEN assume_tac 1); |
|
371 by (auto_tac (claset() addSEs [(starfun_hrinv2 RS subst), |
|
372 inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal], |
|
373 simpset())); |
|
374 qed "NSLIM_rinv"; |
|
375 |
|
376 Goal "[| f -- a --> L; \ |
|
377 \ L ~= #0 |] ==> (%x. rinv(f(x))) -- a --> (rinv L)"; |
|
378 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
379 NSLIM_rinv]) 1); |
|
380 qed "LIM_rinv"; |
|
381 |
|
382 (*------------------------------ |
|
383 NSLIM_zero |
|
384 ------------------------------*) |
|
385 Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> #0"; |
|
386 by (res_inst_tac [("z1","l")] (rename_numerals |
|
387 (real_add_minus RS subst)) 1); |
|
388 by (rtac NSLIM_add_minus 1 THEN Auto_tac); |
|
389 qed "NSLIM_zero"; |
|
390 |
|
391 Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0"; |
|
392 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
393 NSLIM_zero]) 1); |
|
394 qed "LIM_zero2"; |
|
395 |
|
396 Goal "(%x. f(x) - l) -- x --NS> #0 ==> f -- x --NS> l"; |
|
397 by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1); |
|
398 by (auto_tac (claset(),simpset() addsimps [real_diff_def, |
|
399 real_add_assoc])); |
|
400 qed "NSLIM_zero_cancel"; |
|
401 |
|
402 Goal "(%x. f(x) - l) -- x --> #0 ==> f -- x --> l"; |
|
403 by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1); |
|
404 by (auto_tac (claset(),simpset() addsimps [real_diff_def, |
|
405 real_add_assoc])); |
|
406 qed "LIM_zero_cancel"; |
|
407 |
|
408 (*-------------------------- |
|
409 NSLIM_not_zero |
|
410 --------------------------*) |
|
411 Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)"; |
|
412 by (Auto_tac); |
|
413 by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1); |
|
414 by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self |
|
415 RS inf_close_sym],simpset())); |
|
416 by (dres_inst_tac [("x1","-hypreal_of_real x")] (hypreal_add_left_cancel RS iffD2) 1); |
|
417 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym, |
|
418 hypreal_epsilon_not_zero]) 1); |
|
419 qed "NSLIM_not_zero"; |
|
420 |
|
421 (* [| k ~= #0; (%x. k) -- x --NS> #0 |] ==> R *) |
|
422 bind_thm("NSLIM_not_zeroE", (NSLIM_not_zero RS notE)); |
|
423 |
|
424 Goal "k ~= #0 ==> ~ ((%x. k) -- x --> #0)"; |
|
425 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
426 NSLIM_not_zero]) 1); |
|
427 qed "LIM_not_zero2"; |
|
428 |
|
429 (*------------------------------------- |
|
430 NSLIM of constant function |
|
431 -------------------------------------*) |
|
432 Goal "(%x. k) -- x --NS> L ==> k = L"; |
|
433 by (rtac ccontr 1); |
|
434 by (dtac NSLIM_zero 1); |
|
435 by (rtac NSLIM_not_zeroE 1 THEN assume_tac 2); |
|
436 by (arith_tac 1); |
|
437 qed "NSLIM_const_eq"; |
|
438 |
|
439 Goal "(%x. k) -- x --> L ==> k = L"; |
|
440 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
441 NSLIM_const_eq]) 1); |
|
442 qed "LIM_const_eq2"; |
|
443 |
|
444 (*------------------------ |
|
445 NS Limit is Unique |
|
446 ------------------------*) |
|
447 (* can actually be proved more easily by unfolding def! *) |
|
448 Goal "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M"; |
|
449 by (dtac NSLIM_minus 1); |
|
450 by (dtac NSLIM_add 1 THEN assume_tac 1); |
|
451 by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym], |
|
452 simpset() addsimps [real_add_minus])); |
|
453 qed "NSLIM_unique"; |
|
454 |
|
455 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M"; |
|
456 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
457 NSLIM_unique]) 1); |
|
458 qed "LIM_unique2"; |
|
459 |
|
460 (*-------------------- |
|
461 NSLIM_mult_zero |
|
462 --------------------*) |
|
463 Goal "[| f -- x --NS> #0; g -- x --NS> #0 |] \ |
|
464 \ ==> (%x. f(x)*g(x)) -- x --NS> #0"; |
|
465 by (dtac NSLIM_mult 1 THEN Auto_tac); |
|
466 qed "NSLIM_mult_zero"; |
|
467 |
|
468 (* we can use the corresponding thm LIM_mult2 *) |
|
469 (* for standard definition of limit *) |
|
470 |
|
471 Goal "[| f -- x --> #0; g -- x --> #0 |] \ |
|
472 \ ==> (%x. f(x)*g(x)) -- x --> #0"; |
|
473 by (dtac LIM_mult2 1 THEN Auto_tac); |
|
474 qed "LIM_mult_zero2"; |
|
475 |
|
476 (*---------------------------- |
|
477 NSLIM_self |
|
478 ----------------------------*) |
|
479 Goalw [NSLIM_def] "(%x. x) -- a --NS> a"; |
|
480 by (auto_tac (claset() addIs [starfun_Idfun_inf_close],simpset())); |
|
481 qed "NSLIM_self"; |
|
482 |
|
483 Goal "(%x. x) -- a --> a"; |
|
484 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff,NSLIM_self]) 1); |
|
485 qed "LIM_self2"; |
|
486 |
|
487 (*----------------------------------------------------------------------------- |
|
488 Derivatives and Continuity - NS and Standard properties |
|
489 -----------------------------------------------------------------------------*) |
|
490 (*--------------- |
|
491 Continuity |
|
492 ---------------*) |
|
493 |
|
494 Goalw [isNSCont_def] |
|
495 "!!f. [| isNSCont f a; y @= hypreal_of_real a |] \ |
|
496 \ ==> (*f* f) y @= hypreal_of_real (f a)"; |
|
497 by (Blast_tac 1); |
|
498 qed "isNSContD"; |
|
499 |
|
500 Goalw [isNSCont_def,NSLIM_def] |
|
501 "!!f. isNSCont f a ==> f -- a --NS> (f a) "; |
|
502 by (Blast_tac 1); |
|
503 qed "isNSCont_NSLIM"; |
|
504 |
|
505 Goalw [isNSCont_def,NSLIM_def] |
|
506 "!!f. f -- a --NS> (f a) ==> isNSCont f a"; |
|
507 by (Auto_tac); |
|
508 by (res_inst_tac [("Q","y = hypreal_of_real a")] |
|
509 (excluded_middle RS disjE) 1); |
|
510 by (Auto_tac); |
|
511 qed "NSLIM_isNSCont"; |
|
512 |
|
513 (*----------------------------------------------------- |
|
514 NS continuity can be defined using NS Limit in |
|
515 similar fashion to standard def of continuity |
|
516 -----------------------------------------------------*) |
|
517 Goal "(isNSCont f a) = (f -- a --NS> (f a))"; |
|
518 by (blast_tac (claset() addIs [isNSCont_NSLIM,NSLIM_isNSCont]) 1); |
|
519 qed "isNSCont_NSLIM_iff"; |
|
520 |
|
521 (*---------------------------------------------- |
|
522 Hence, NS continuity can be given |
|
523 in terms of standard limit |
|
524 ---------------------------------------------*) |
|
525 Goal "(isNSCont f a) = (f -- a --> (f a))"; |
|
526 by (asm_full_simp_tac (simpset() addsimps |
|
527 [LIM_NSLIM_iff,isNSCont_NSLIM_iff]) 1); |
|
528 qed "isNSCont_LIM_iff"; |
|
529 |
|
530 (*----------------------------------------------- |
|
531 Moreover, it's trivial now that NS continuity |
|
532 is equivalent to standard continuity |
|
533 -----------------------------------------------*) |
|
534 Goalw [isCont_def] "(isNSCont f a) = (isCont f a)"; |
|
535 by (rtac isNSCont_LIM_iff 1); |
|
536 qed "isNSCont_isCont_iff"; |
|
537 |
|
538 (*---------------------------------------- |
|
539 Standard continuity ==> NS continuity |
|
540 ----------------------------------------*) |
|
541 Goal "!!f. isCont f a ==> isNSCont f a"; |
|
542 by (etac (isNSCont_isCont_iff RS iffD2) 1); |
|
543 qed "isCont_isNSCont"; |
|
544 |
|
545 (*---------------------------------------- |
|
546 NS continuity ==> Standard continuity |
|
547 ----------------------------------------*) |
|
548 Goal "!!f. isNSCont f a ==> isCont f a"; |
|
549 by (etac (isNSCont_isCont_iff RS iffD1) 1); |
|
550 qed "isNSCont_isCont"; |
|
551 |
|
552 (*-------------------------------------------------------------------------- |
|
553 Alternative definition of continuity |
|
554 --------------------------------------------------------------------------*) |
|
555 (* Prove equivalence between NS limits - *) |
|
556 (* seems easier than using standard def *) |
|
557 Goalw [NSLIM_def] |
|
558 "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)"; |
|
559 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero])); |
|
560 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1); |
|
561 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2); |
|
562 by (Step_tac 1); |
|
563 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 1); |
|
564 by (rtac ((mem_infmal_iff RS iffD2) RS |
|
565 (Infinitesimal_add_inf_close_self RS inf_close_sym)) 2); |
|
566 by (rtac (inf_close_minus_iff2 RS iffD1) 5); |
|
567 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 4); |
|
568 by (dtac (sym RS (hypreal_eq_minus_iff RS iffD2)) 4); |
|
569 by (res_inst_tac [("z","x")] eq_Abs_hypreal 3); |
|
570 by (res_inst_tac [("z","x")] eq_Abs_hypreal 6); |
|
571 by (auto_tac (claset(),simpset() addsimps [starfun, |
|
572 hypreal_of_real_def,hypreal_minus,hypreal_add, |
|
573 real_add_assoc,inf_close_refl,hypreal_zero_def])); |
|
574 qed "NSLIM_h_iff"; |
|
575 |
|
576 Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)"; |
|
577 by (rtac NSLIM_h_iff 1); |
|
578 qed "NSLIM_isCont_iff"; |
|
579 |
|
580 Goal "(f -- a --> f a) = ((%h. f(a + h)) -- #0 --> f(a))"; |
|
581 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
582 NSLIM_isCont_iff]) 1); |
|
583 qed "LIM_isCont_iff"; |
|
584 |
|
585 Goalw [isCont_def] |
|
586 "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))"; |
|
587 by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1); |
|
588 qed "isCont_iff"; |
|
589 |
|
590 (*-------------------------------------------------------------------------- |
|
591 Immediate application of nonstandard criterion for continuity can offer |
|
592 very simple proofs of some standard property of continuous functions |
|
593 --------------------------------------------------------------------------*) |
|
594 (*------------------------ |
|
595 sum continuous |
|
596 ------------------------*) |
|
597 Goal "!!f. [| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"; |
|
598 by (auto_tac (claset() addIs [starfun_add_inf_close],simpset() addsimps |
|
599 [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_add])); |
|
600 qed "isCont_add"; |
|
601 |
|
602 (*------------------------ |
|
603 mult continuous |
|
604 ------------------------*) |
|
605 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"; |
|
606 by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],simpset() addsimps |
|
607 [isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_mult])); |
|
608 qed "isCont_mult"; |
|
609 |
|
610 (*------------------------------------------- |
|
611 composition of continuous functions |
|
612 Note very short straightforard proof! |
|
613 ------------------------------------------*) |
|
614 Goal "[| isCont f a; isCont g (f a) |] \ |
|
615 \ ==> isCont (g o f) a"; |
|
616 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
|
617 isNSCont_def,starfun_o RS sym])); |
|
618 qed "isCont_o"; |
|
619 |
|
620 Goal "[| isCont f a; isCont g (f a) |] \ |
|
621 \ ==> isCont (%x. g (f x)) a"; |
|
622 by (auto_tac (claset() addDs [isCont_o],simpset() addsimps [o_def])); |
|
623 qed "isCont_o2"; |
|
624 |
|
625 Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a"; |
|
626 by (auto_tac (claset(),simpset() addsimps [starfun_minus RS sym, |
|
627 hypreal_of_real_minus])); |
|
628 qed "isNSCont_minus"; |
|
629 |
|
630 Goal "isCont f a ==> isCont (%x. - f x) a"; |
|
631 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
|
632 isNSCont_minus])); |
|
633 qed "isCont_minus"; |
|
634 |
|
635 Goalw [isCont_def] |
|
636 "[| isCont f x; f x ~= #0 |] ==> isCont (%x. rinv (f x)) x"; |
|
637 by (blast_tac (claset() addIs [LIM_rinv]) 1); |
|
638 qed "isCont_rinv"; |
|
639 |
|
640 Goal "[| isNSCont f x; f x ~= #0 |] ==> isNSCont (%x. rinv (f x)) x"; |
|
641 by (auto_tac (claset() addIs [isCont_rinv],simpset() addsimps |
|
642 [isNSCont_isCont_iff])); |
|
643 qed "isNSCont_rinv"; |
|
644 |
|
645 Goalw [real_diff_def] |
|
646 "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"; |
|
647 by (auto_tac (claset() addIs [isCont_add,isCont_minus],simpset())); |
|
648 qed "isCont_diff"; |
|
649 |
|
650 Goalw [isCont_def] "isCont (%x. k) a"; |
|
651 by (Simp_tac 1); |
|
652 qed "isCont_const"; |
|
653 Addsimps [isCont_const]; |
|
654 |
|
655 Goalw [isNSCont_def] "isNSCont (%x. k) a"; |
|
656 by (Simp_tac 1); |
|
657 qed "isNSCont_const"; |
|
658 Addsimps [isNSCont_const]; |
|
659 |
|
660 Goalw [isNSCont_def] "isNSCont abs a"; |
|
661 by (auto_tac (claset() addIs [inf_close_hrabs],simpset() addsimps |
|
662 [hypreal_of_real_hrabs RS sym,starfun_rabs_hrabs])); |
|
663 qed "isNSCont_rabs"; |
|
664 Addsimps [isNSCont_rabs]; |
|
665 |
|
666 Goal "isCont abs a"; |
|
667 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym])); |
|
668 qed "isCont_rabs"; |
|
669 Addsimps [isCont_rabs]; |
|
670 |
|
671 (**************************************************************** |
|
672 (* Leave as commented until I add topology theory or remove? *) |
|
673 (*------------------------------------------------------------ |
|
674 Elementary topology proof for a characterisation of |
|
675 continuity now: a function f is continuous if and only |
|
676 if the inverse image, {x. f(x) : A}, of any open set A |
|
677 is always an open set |
|
678 ------------------------------------------------------------*) |
|
679 Goal "!!A. [| isNSopen A; ALL x. isNSCont f x |] \ |
|
680 \ ==> isNSopen {x. f x : A}"; |
|
681 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
|
682 by (dtac (mem_monad_inf_close RS inf_close_sym) 1); |
|
683 by (dres_inst_tac [("x","a")] spec 1); |
|
684 by (dtac isNSContD 1 THEN assume_tac 1); |
|
685 by (dtac bspec 1 THEN assume_tac 1); |
|
686 by (dres_inst_tac [("x","( *f* f) x")] inf_close_mem_monad2 1); |
|
687 by (blast_tac (claset() addIs [starfun_mem_starset]) 1); |
|
688 qed "isNSCont_isNSopen"; |
|
689 |
|
690 Goalw [isNSCont_def] |
|
691 "!!x. ALL A. isNSopen A --> isNSopen {x. f x : A} \ |
|
692 \ ==> isNSCont f x"; |
|
693 by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS |
|
694 (inf_close_minus_iff RS iffD2)],simpset() addsimps |
|
695 [Infinitesimal_def,SReal_iff])); |
|
696 by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); |
|
697 by (etac (isNSopen_open_interval RSN (2,impE)) 1); |
|
698 by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); |
|
699 by (dres_inst_tac [("x","x")] spec 1); |
|
700 by (auto_tac (claset() addDs [inf_close_sym RS inf_close_mem_monad], |
|
701 simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); |
|
702 qed "isNSopen_isNSCont"; |
|
703 |
|
704 Goal "(ALL x. isNSCont f x) = \ |
|
705 \ (ALL A. isNSopen A --> isNSopen {x. f(x) : A})"; |
|
706 by (blast_tac (claset() addIs [isNSCont_isNSopen, |
|
707 isNSopen_isNSCont]) 1); |
|
708 qed "isNSCont_isNSopen_iff"; |
|
709 |
|
710 (*------- Standard version of same theorem --------*) |
|
711 Goal "(ALL x. isCont f x) = \ |
|
712 \ (ALL A. isopen A --> isopen {x. f(x) : A})"; |
|
713 by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], |
|
714 simpset() addsimps [isNSopen_isopen_iff RS sym, |
|
715 isNSCont_isCont_iff RS sym])); |
|
716 qed "isCont_isopen_iff"; |
|
717 *******************************************************************) |
|
718 |
|
719 (*----------------------------------------------------------------- |
|
720 Uniform continuity |
|
721 ------------------------------------------------------------------*) |
|
722 Goalw [isNSUCont_def] |
|
723 "[| isNSUCont f; x @= y|] ==> (*f* f) x @= (*f* f) y"; |
|
724 by (Blast_tac 1); |
|
725 qed "isNSUContD"; |
|
726 |
|
727 Goalw [isUCont_def,isCont_def,LIM_def] |
|
728 "isUCont f ==> EX x. isCont f x"; |
|
729 by (Fast_tac 1); |
|
730 qed "isUCont_isCont"; |
|
731 |
|
732 Goalw [isNSUCont_def,isUCont_def,inf_close_def] |
|
733 "isUCont f ==> isNSUCont f"; |
|
734 by (asm_full_simp_tac (simpset() addsimps |
|
735 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
736 by (Step_tac 1); |
|
737 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
738 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
739 by (auto_tac (claset(),simpset() addsimps [starfun, |
|
740 hypreal_minus, hypreal_add])); |
|
741 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1); |
|
742 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1); |
|
743 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1); |
|
744 by (subgoal_tac "ALL n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u" 1); |
|
745 by (Blast_tac 2); |
|
746 by (thin_tac "ALL x y. abs (x + - y) < s --> abs (f x + - f y) < u" 1); |
|
747 by (dtac FreeUltrafilterNat_all 1); |
|
748 by (Ultra_tac 1); |
|
749 qed "isUCont_isNSUCont"; |
|
750 |
|
751 Goal "!!x. ALL s. #0 < s --> \ |
|
752 \ (EX xa y. abs (xa + - y) < s & \ |
|
753 \ r <= abs (f xa + -f y)) ==> \ |
|
754 \ ALL n::nat. EX xa y. \ |
|
755 \ abs(xa + -y) < rinv(real_of_posnat n) & \ |
|
756 \ r <= abs(f xa + -f y)"; |
|
757 by (Step_tac 1); |
|
758 by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_rinv_gt_zero) 1); |
|
759 by Auto_tac; |
|
760 val lemma_LIMu = result(); |
|
761 |
|
762 Goal "!!x. ALL s. #0 < s --> \ |
|
763 \ (EX xa y. abs (xa + - y) < s & \ |
|
764 \ r <= abs (f xa + -f y)) ==> \ |
|
765 \ EX X Y. ALL n::nat. \ |
|
766 \ abs(X n + -(Y n)) < rinv(real_of_posnat n) & \ |
|
767 \ r <= abs(f (X n) + -f (Y n))"; |
|
768 by (dtac lemma_LIMu 1); |
|
769 by (dtac choice 1); |
|
770 by (Step_tac 1); |
|
771 by (dtac choice 1); |
|
772 by (Blast_tac 1); |
|
773 val lemma_skolemize_LIM2u = result(); |
|
774 |
|
775 Goal "ALL n. abs (X n + -Y n) < rinv (real_of_posnat n) & \ |
|
776 \ r <= abs (f (X n) + - f(Y n)) ==> \ |
|
777 \ ALL n. abs (X n + - Y n) < rinv (real_of_posnat n)"; |
|
778 by (Auto_tac ); |
|
779 val lemma_simpu = result(); |
|
780 |
|
781 Goal "{n. f (X n) + - f(Y n) = Ya n} Int \ |
|
782 \ {n. abs (X n + - Y n) < rinv (real_of_posnat n) & \ |
|
783 \ r <= abs (f (X n) + - f(Y n))} <= \ |
|
784 \ {n. r <= abs (Ya n)}"; |
|
785 by (Auto_tac); |
|
786 val lemma_Intu = result (); |
|
787 |
|
788 Goalw [isNSUCont_def,isUCont_def,inf_close_def] |
|
789 "isNSUCont f ==> isUCont f"; |
|
790 by (asm_full_simp_tac (simpset() addsimps |
|
791 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
792 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
|
793 by (fold_tac [real_le_def]); |
|
794 by (dtac lemma_skolemize_LIM2u 1); |
|
795 by (Step_tac 1); |
|
796 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1); |
|
797 by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1); |
|
798 by (asm_full_simp_tac (simpset() addsimps [starfun, |
|
799 hypreal_minus,hypreal_add]) 1); |
|
800 by (Auto_tac); |
|
801 by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1); |
|
802 by (asm_full_simp_tac (simpset() addsimps |
|
803 [Infinitesimal_FreeUltrafilterNat_iff, |
|
804 hypreal_minus,hypreal_add]) 1); |
|
805 by (Blast_tac 1); |
|
806 by (rotate_tac 2 1); |
|
807 by (dres_inst_tac [("x","r")] spec 1); |
|
808 by (Clarify_tac 1); |
|
809 by (dtac FreeUltrafilterNat_all 1); |
|
810 by (Ultra_tac 1); |
|
811 qed "isNSUCont_isUCont"; |
|
812 |
|
813 (*------------------------------------------------------------------ |
|
814 Derivatives |
|
815 ------------------------------------------------------------------*) |
|
816 Goalw [deriv_def] |
|
817 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --> D)"; |
|
818 by (Blast_tac 1); |
|
819 qed "DERIV_iff"; |
|
820 |
|
821 Goalw [deriv_def] |
|
822 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D)"; |
|
823 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
824 qed "DERIV_NS_iff"; |
|
825 |
|
826 Goalw [deriv_def] |
|
827 "DERIV f x :> D \ |
|
828 \ ==> (%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --> D"; |
|
829 by (Blast_tac 1); |
|
830 qed "DERIVD"; |
|
831 |
|
832 Goalw [deriv_def] "DERIV f x :> D ==> \ |
|
833 \ (%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D"; |
|
834 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
835 qed "NS_DERIVD"; |
|
836 |
|
837 (* Uniqueness *) |
|
838 Goalw [deriv_def] |
|
839 "!!f. [| DERIV f x :> D; DERIV f x :> E |] ==> D = E"; |
|
840 by (blast_tac (claset() addIs [LIM_unique]) 1); |
|
841 qed "DERIV_unique"; |
|
842 |
|
843 Goalw [nsderiv_def] |
|
844 "!!f. [| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"; |
|
845 by (cut_facts_tac [Infinitesimal_epsilon, |
|
846 hypreal_epsilon_not_zero] 1); |
|
847 by (auto_tac (claset() addSDs [bspec] addSIs |
|
848 [inj_hypreal_of_real RS injD] addDs [inf_close_trans3],simpset())); |
|
849 qed "NSDeriv_unique"; |
|
850 |
|
851 (*------------------------------------------------------------------------ |
|
852 Differentiable |
|
853 ------------------------------------------------------------------------*) |
|
854 |
|
855 Goalw [differentiable_def] |
|
856 "!!f. f differentiable x ==> EX D. DERIV f x :> D"; |
|
857 by (assume_tac 1); |
|
858 qed "differentiableD"; |
|
859 |
|
860 Goalw [differentiable_def] |
|
861 "!!f. DERIV f x :> D ==> f differentiable x"; |
|
862 by (Blast_tac 1); |
|
863 qed "differentiableI"; |
|
864 |
|
865 Goalw [NSdifferentiable_def] |
|
866 "!!f. f NSdifferentiable x ==> EX D. NSDERIV f x :> D"; |
|
867 by (assume_tac 1); |
|
868 qed "NSdifferentiableD"; |
|
869 |
|
870 Goalw [NSdifferentiable_def] |
|
871 "!!f. NSDERIV f x :> D ==> f NSdifferentiable x"; |
|
872 by (Blast_tac 1); |
|
873 qed "NSdifferentiableI"; |
|
874 |
|
875 (*-------------------------------------------------------- |
|
876 Alternative definition for differentiability |
|
877 -------------------------------------------------------*) |
|
878 |
|
879 Goalw [LIM_def] |
|
880 "((%h. (f(a + h) + - f(a))*rinv(h)) -- #0 --> D) = \ |
|
881 \ ((%x. (f(x) + -f(a))*rinv(x + -a)) -- a --> D)"; |
|
882 by (Step_tac 1); |
|
883 by (ALLGOALS(dtac spec)); |
|
884 by (Step_tac 1); |
|
885 by (Blast_tac 1 THEN Blast_tac 2); |
|
886 by (ALLGOALS(res_inst_tac [("x","s")] exI)); |
|
887 by (Step_tac 1); |
|
888 by (dres_inst_tac [("x","x + -a")] spec 1); |
|
889 by (dres_inst_tac [("x","x + a")] spec 2); |
|
890 by (auto_tac (claset(),simpset() addsimps |
|
891 real_add_ac)); |
|
892 qed "DERIV_LIM_iff"; |
|
893 |
|
894 Goalw [deriv_def] "(DERIV f x :> D) = \ |
|
895 \ ((%z. (f(z) + -f(x))*rinv(z + -x)) -- x --> D)"; |
|
896 by (simp_tac (simpset() addsimps [DERIV_LIM_iff]) 1); |
|
897 qed "DERIV_iff2"; |
|
898 |
|
899 (*-------------------------------------------------------- |
|
900 Equivalence of NS and standard defs of differentiation |
|
901 -------------------------------------------------------*) |
|
902 (*------------------------------------------- |
|
903 First NSDERIV in terms of NSLIM |
|
904 -------------------------------------------*) |
|
905 (*--- first equivalence ---*) |
|
906 Goalw [nsderiv_def,NSLIM_def] |
|
907 "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D)"; |
|
908 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero])); |
|
909 by (dres_inst_tac [("x","xa")] bspec 1); |
|
910 by (rtac ccontr 3); |
|
911 by (dres_inst_tac [("x","h")] spec 3); |
|
912 by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff, |
|
913 starfun_mult RS sym,starfun_rinv_hrinv,starfun_add RS sym, |
|
914 hypreal_of_real_minus,starfun_lambda_cancel])); |
|
915 qed "NSDERIV_NSLIM_iff"; |
|
916 |
|
917 (*--- second equivalence ---*) |
|
918 Goal "(NSDERIV f x :> D) = \ |
|
919 \ ((%z. (f(z) + -f(x))*rinv(z + -x)) -- x --NS> D)"; |
|
920 by (full_simp_tac (simpset() addsimps |
|
921 [NSDERIV_NSLIM_iff,DERIV_LIM_iff,LIM_NSLIM_iff RS sym]) 1); |
|
922 qed "NSDERIV_NSLIM_iff2"; |
|
923 |
|
924 (* while we're at it! *) |
|
925 Goalw [real_diff_def] |
|
926 "(NSDERIV f x :> D) = \ |
|
927 \ (ALL xa. \ |
|
928 \ xa ~= hypreal_of_real x & xa @= hypreal_of_real x --> \ |
|
929 \ (*f* (%z. (f z - f x) * rinv (z - x))) xa @= hypreal_of_real D)"; |
|
930 by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2, |
|
931 NSLIM_def])); |
|
932 qed "NSDERIV_iff2"; |
|
933 |
|
934 Addsimps [inf_close_refl]; |
|
935 Goal "(NSDERIV f x :> D) ==> \ |
|
936 \ (ALL xa. \ |
|
937 \ xa @= hypreal_of_real x --> \ |
|
938 \ (*f* (%z. f z - f x)) xa @= hypreal_of_real D * (xa - hypreal_of_real x))"; |
|
939 by (auto_tac (claset(),simpset() addsimps [NSDERIV_iff2])); |
|
940 by (case_tac "xa = hypreal_of_real x" 1); |
|
941 by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def, |
|
942 hypreal_of_real_zero])); |
|
943 by (dres_inst_tac [("x","xa")] spec 1); |
|
944 by Auto_tac; |
|
945 by (dres_inst_tac [("c","xa - hypreal_of_real x"),("b","hypreal_of_real D")] |
|
946 inf_close_mult1 1); |
|
947 by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1))); |
|
948 by (subgoal_tac "(*f* (%z. z - x)) xa ~= (0::hypreal)" 2); |
|
949 by (dtac (starfun_hrinv2 RS sym) 2); |
|
950 by (auto_tac (claset() addDs [hypreal_mult_hrinv_left], |
|
951 simpset() addsimps [starfun_mult RS sym, |
|
952 hypreal_mult_assoc,starfun_add RS sym,real_diff_def, |
|
953 starfun_Id,hypreal_of_real_minus,hypreal_diff_def, |
|
954 (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2), |
|
955 Infinitesimal_subset_HFinite RS subsetD])); |
|
956 qed "NSDERIVD5"; |
|
957 |
|
958 Goal "(NSDERIV f x :> D) ==> \ |
|
959 \ (ALL h: Infinitesimal. \ |
|
960 \ ((*f* f)(hypreal_of_real x + h) - \ |
|
961 \ hypreal_of_real (f x))@= (hypreal_of_real D) * h)"; |
|
962 by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); |
|
963 by (case_tac "h = (0::hypreal)" 1); |
|
964 by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def])); |
|
965 by (dres_inst_tac [("x","h")] bspec 1); |
|
966 by (dres_inst_tac [("c","h")] inf_close_mult1 2); |
|
967 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
968 simpset() addsimps [hypreal_mult_assoc,hypreal_diff_def])); |
|
969 qed "NSDERIVD4"; |
|
970 |
|
971 Goal "(NSDERIV f x :> D) ==> \ |
|
972 \ (ALL h: Infinitesimal - {0}. \ |
|
973 \ ((*f* f)(hypreal_of_real x + h) - \ |
|
974 \ hypreal_of_real (f x))@= (hypreal_of_real D) * h)"; |
|
975 by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); |
|
976 by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1); |
|
977 by (dres_inst_tac [("c","h")] inf_close_mult1 2); |
|
978 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
979 simpset() addsimps [hypreal_mult_assoc,hypreal_diff_def])); |
|
980 qed "NSDERIVD3"; |
|
981 |
|
982 (*-------------------------------------------------------------- |
|
983 Now equivalence between NSDERIV and DERIV |
|
984 -------------------------------------------------------------*) |
|
985 Goalw [deriv_def] "(NSDERIV f x :> D) = (DERIV f x :> D)"; |
|
986 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,LIM_NSLIM_iff]) 1); |
|
987 qed "NSDERIV_DERIV_iff"; |
|
988 |
|
989 (*--------------------------------------------------- |
|
990 Differentiability implies continuity |
|
991 nice and simple "algebraic" proof |
|
992 --------------------------------------------------*) |
|
993 Goalw [nsderiv_def] |
|
994 "NSDERIV f x :> D ==> isNSCont f x"; |
|
995 by (auto_tac (claset(),simpset() addsimps |
|
996 [isNSCont_NSLIM_iff,NSLIM_def])); |
|
997 by (dtac (inf_close_minus_iff RS iffD1) 1); |
|
998 by (dtac (hypreal_not_eq_minus_iff RS iffD1) 1); |
|
999 by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1); |
|
1000 by (asm_full_simp_tac (simpset() addsimps |
|
1001 [hypreal_add_assoc RS sym]) 2); |
|
1002 by (auto_tac (claset(),simpset() addsimps |
|
1003 [mem_infmal_iff RS sym,hypreal_add_commute])); |
|
1004 by (dres_inst_tac [("c","xa + -hypreal_of_real x")] inf_close_mult1 1); |
|
1005 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite |
|
1006 RS subsetD],simpset() addsimps [hypreal_mult_assoc])); |
|
1007 by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN |
|
1008 (2,Infinitesimal_HFinite_mult) RS (mem_infmal_iff RS iffD1)) 1); |
|
1009 by (blast_tac (claset() addIs [inf_close_trans, |
|
1010 hypreal_mult_commute RS subst, |
|
1011 (inf_close_minus_iff RS iffD2)]) 1); |
|
1012 qed "NSDERIV_isNSCont"; |
|
1013 |
|
1014 (* Now Sandard proof *) |
|
1015 Goal "DERIV f x :> D ==> isCont f x"; |
|
1016 by (asm_full_simp_tac (simpset() addsimps |
|
1017 [NSDERIV_DERIV_iff RS sym, isNSCont_isCont_iff RS sym, |
|
1018 NSDERIV_isNSCont]) 1); |
|
1019 qed "DERIV_isCont"; |
|
1020 |
|
1021 (*---------------------------------------------------------------------------- |
|
1022 Differentiation rules for combinations of functions |
|
1023 follow from clear, straightforard, algebraic |
|
1024 manipulations |
|
1025 ----------------------------------------------------------------------------*) |
|
1026 (*------------------------- |
|
1027 Constant function |
|
1028 ------------------------*) |
|
1029 |
|
1030 (* use simple constant nslimit theorem *) |
|
1031 Goal "(NSDERIV (%x. k) x :> #0)"; |
|
1032 by (simp_tac (simpset() addsimps |
|
1033 [NSDERIV_NSLIM_iff,real_add_minus]) 1); |
|
1034 qed "NSDERIV_const"; |
|
1035 Addsimps [NSDERIV_const]; |
|
1036 |
|
1037 Goal "(DERIV (%x. k) x :> #0)"; |
|
1038 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1); |
|
1039 qed "DERIV_const"; |
|
1040 Addsimps [DERIV_const]; |
|
1041 |
|
1042 (*----------------------------------------------------- |
|
1043 Sum of functions- proved easily |
|
1044 ----------------------------------------------------*) |
|
1045 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1046 \ ==> NSDERIV (%x. f x + g x) x :> Da + Db"; |
|
1047 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1048 NSLIM_def]) 1 THEN REPEAT(Step_tac 1)); |
|
1049 by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym, |
|
1050 starfun_mult RS sym,hypreal_of_real_minus,hypreal_of_real_add, |
|
1051 hypreal_minus_add_distrib,hypreal_add_mult_distrib])); |
|
1052 by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1); |
|
1053 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1054 qed "NSDERIV_add"; |
|
1055 |
|
1056 (* Standard theorem *) |
|
1057 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1058 \ ==> DERIV (%x. f x + g x) x :> Da + Db"; |
|
1059 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_add, |
|
1060 NSDERIV_DERIV_iff RS sym]) 1); |
|
1061 qed "DERIV_add"; |
|
1062 |
|
1063 (*----------------------------------------------------- |
|
1064 Product of functions - Proof is trivial but tedious |
|
1065 and long due to rearrangement of terms |
|
1066 ----------------------------------------------------*) |
|
1067 (* lemma - terms manipulation tedious as usual*) |
|
1068 |
|
1069 Goal "((a::real)*b) + -(c*d) = (b*(a + -c)) + \ |
|
1070 \ (c*(b + -d))"; |
|
1071 by (full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
|
1072 real_minus_mult_eq2 RS sym,real_mult_commute]) 1); |
|
1073 val lemma_nsderiv1 = result(); |
|
1074 |
|
1075 Goal "[| (x + y) * hrinv z = hypreal_of_real D + yb; z ~= 0; \ |
|
1076 \ z : Infinitesimal; yb : Infinitesimal |] \ |
|
1077 \ ==> x + y @= 0"; |
|
1078 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel |
|
1079 RS iffD2) 1 THEN assume_tac 1); |
|
1080 by (thin_tac "(x + y) * hrinv z = hypreal_of_real D + yb" 1); |
|
1081 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, |
|
1082 HFinite_add],simpset() addsimps [hypreal_mult_assoc, |
|
1083 mem_infmal_iff RS sym])); |
|
1084 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
|
1085 val lemma_nsderiv2 = result(); |
|
1086 |
|
1087 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1088 \ ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
1089 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1090 NSLIM_def]) 1 THEN REPEAT(Step_tac 1)); |
|
1091 by (auto_tac (claset(),simpset() addsimps [starfun_mult RS sym, |
|
1092 starfun_add RS sym,starfun_lambda_cancel, |
|
1093 starfun_rinv_hrinv,hypreal_of_real_zero,lemma_nsderiv1])); |
|
1094 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1); |
|
1095 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); |
|
1096 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc, |
|
1097 hypreal_of_real_minus])); |
|
1098 by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1); |
|
1099 by (dtac ((inf_close_minus_iff RS iffD2) RS |
|
1100 (bex_Infinitesimal_iff2 RS iffD2)) 4); |
|
1101 by (auto_tac (claset() addSIs [inf_close_add_mono1], |
|
1102 simpset() addsimps [hypreal_of_real_add,hypreal_add_mult_distrib, |
|
1103 hypreal_add_mult_distrib2,hypreal_of_real_mult,hypreal_mult_commute, |
|
1104 hypreal_add_assoc])); |
|
1105 by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")] |
|
1106 (hypreal_add_commute RS subst) 1); |
|
1107 by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS |
|
1108 inf_close_sym,Infinitesimal_add,Infinitesimal_mult, |
|
1109 Infinitesimal_hypreal_of_real_mult,Infinitesimal_hypreal_of_real_mult2 ], |
|
1110 simpset() addsimps [hypreal_add_assoc RS sym])); |
|
1111 qed "NSDERIV_mult"; |
|
1112 |
|
1113 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1114 \ ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
1115 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_mult, |
|
1116 NSDERIV_DERIV_iff RS sym]) 1); |
|
1117 qed "DERIV_mult"; |
|
1118 |
|
1119 (*---------------------------- |
|
1120 Multiplying by a constant |
|
1121 ---------------------------*) |
|
1122 Goal "NSDERIV f x :> D \ |
|
1123 \ ==> NSDERIV (%x. c * f x) x :> c*D"; |
|
1124 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1125 real_minus_mult_eq2,real_add_mult_distrib2 RS sym, |
|
1126 real_mult_assoc] delsimps [real_minus_mult_eq2 RS sym]) 1); |
|
1127 by (etac (NSLIM_const RS NSLIM_mult) 1); |
|
1128 qed "NSDERIV_cmult"; |
|
1129 |
|
1130 (* let's do the standard proof though theorem *) |
|
1131 (* LIM_mult2 follows from a NS proof *) |
|
1132 |
|
1133 Goalw [deriv_def] |
|
1134 "DERIV f x :> D \ |
|
1135 \ ==> DERIV (%x. c * f x) x :> c*D"; |
|
1136 by (asm_full_simp_tac (simpset() addsimps [ |
|
1137 real_minus_mult_eq2,real_add_mult_distrib2 RS sym, |
|
1138 real_mult_assoc] delsimps [real_minus_mult_eq2 RS sym]) 1); |
|
1139 by (etac (LIM_const RS LIM_mult2) 1); |
|
1140 qed "DERIV_cmult"; |
|
1141 |
|
1142 (*-------------------------------- |
|
1143 Negation of function |
|
1144 -------------------------------*) |
|
1145 Goal "NSDERIV f x :> D \ |
|
1146 \ ==> NSDERIV (%x. -(f x)) x :> -D"; |
|
1147 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); |
|
1148 by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1); |
|
1149 by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym, |
|
1150 real_minus_mult_eq1 RS sym] delsimps [real_minus_add_distrib, |
|
1151 real_minus_minus]) 1); |
|
1152 by (etac NSLIM_minus 1); |
|
1153 qed "NSDERIV_minus"; |
|
1154 |
|
1155 Goal "DERIV f x :> D \ |
|
1156 \ ==> DERIV (%x. -(f x)) x :> -D"; |
|
1157 by (asm_full_simp_tac (simpset() addsimps |
|
1158 [NSDERIV_minus,NSDERIV_DERIV_iff RS sym]) 1); |
|
1159 qed "DERIV_minus"; |
|
1160 |
|
1161 (*------------------------------- |
|
1162 Subtraction |
|
1163 ------------------------------*) |
|
1164 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1165 \ ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"; |
|
1166 by (blast_tac (claset() addDs [NSDERIV_add,NSDERIV_minus]) 1); |
|
1167 qed "NSDERIV_add_minus"; |
|
1168 |
|
1169 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1170 \ ==> DERIV (%x. f x + -g x) x :> Da + -Db"; |
|
1171 by (blast_tac (claset() addDs [DERIV_add,DERIV_minus]) 1); |
|
1172 qed "DERIV_add_minus"; |
|
1173 |
|
1174 Goalw [real_diff_def] |
|
1175 "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1176 \ ==> NSDERIV (%x. f x - g x) x :> Da - Db"; |
|
1177 by (blast_tac (claset() addIs [NSDERIV_add_minus]) 1); |
|
1178 qed "NSDERIV_diff"; |
|
1179 |
|
1180 Goalw [real_diff_def] |
|
1181 "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1182 \ ==> DERIV (%x. f x - g x) x :> Da - Db"; |
|
1183 by (blast_tac (claset() addIs [DERIV_add_minus]) 1); |
|
1184 qed "DERIV_diff"; |
|
1185 |
|
1186 (*--------------------------------------------------------------- |
|
1187 (NS) Increment |
|
1188 ---------------------------------------------------------------*) |
|
1189 Goalw [increment_def] |
|
1190 "f NSdifferentiable x ==> \ |
|
1191 \ increment f x h = (*f* f) (hypreal_of_real(x) + h) + \ |
|
1192 \ -hypreal_of_real (f x)"; |
|
1193 by (Blast_tac 1); |
|
1194 qed "incrementI"; |
|
1195 |
|
1196 Goal "NSDERIV f x :> D ==> \ |
|
1197 \ increment f x h = (*f* f) (hypreal_of_real(x) + h) + \ |
|
1198 \ -hypreal_of_real (f x)"; |
|
1199 by (etac (NSdifferentiableI RS incrementI) 1); |
|
1200 qed "incrementI2"; |
|
1201 |
|
1202 (* The Increment theorem -- Keisler p. 65 *) |
|
1203 Goal "[| NSDERIV f x :> D; h: Infinitesimal; h ~= 0 |] \ |
|
1204 \ ==> EX e: Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"; |
|
1205 by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def); |
|
1206 by (dtac bspec 1 THEN Auto_tac); |
|
1207 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1); |
|
1208 by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] |
|
1209 (hypreal_mult_right_cancel RS iffD2) 1); |
|
1210 by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \ |
|
1211 \ - hypreal_of_real (f x)) * hrinv h = hypreal_of_real(D) + y" 2); |
|
1212 by (assume_tac 1); |
|
1213 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc, |
|
1214 hypreal_add_mult_distrib])); |
|
1215 qed "increment_thm"; |
|
1216 |
|
1217 Goal "[| NSDERIV f x :> D; h @= 0; h ~= 0 |] \ |
|
1218 \ ==> EX e: Infinitesimal. increment f x h = \ |
|
1219 \ hypreal_of_real(D)*h + e*h"; |
|
1220 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2] |
|
1221 addSIs [increment_thm]) 1); |
|
1222 qed "increment_thm2"; |
|
1223 |
|
1224 Goal "[| NSDERIV f x :> D; h @= 0; h ~= 0 |] \ |
|
1225 \ ==> increment f x h @= 0"; |
|
1226 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs |
|
1227 [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps |
|
1228 [hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym])); |
|
1229 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
|
1230 qed "increment_inf_close_zero"; |
|
1231 |
|
1232 (*--------------------------------------------------------------- |
|
1233 Similarly to the above, the chain rule admits an entirely |
|
1234 straightforward derivation. Compare this with Harrison's |
|
1235 HOL proof of the chain rule, which proved to be trickier and |
|
1236 required an alternative characterisation of differentiability- |
|
1237 the so-called Carathedory derivative. Our main problem is |
|
1238 manipulation of terms. |
|
1239 --------------------------------------------------------------*) |
|
1240 (* lemmas *) |
|
1241 Goalw [nsderiv_def] |
|
1242 "!!f. [| NSDERIV g x :> D; \ |
|
1243 \ (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ |
|
1244 \ xa : Infinitesimal;\ |
|
1245 \ xa ~= 0 \ |
|
1246 \ |] ==> D = #0"; |
|
1247 by (dtac bspec 1); |
|
1248 by (Auto_tac); |
|
1249 by (asm_full_simp_tac (simpset() addsimps |
|
1250 [hypreal_of_real_zero RS sym]) 1); |
|
1251 qed "NSDERIV_zero"; |
|
1252 |
|
1253 (* can be proved differently using NSLIM_isCont_iff *) |
|
1254 Goalw [nsderiv_def] |
|
1255 "!!f. [| NSDERIV f x :> D; \ |
|
1256 \ h: Infinitesimal; h ~= 0 \ |
|
1257 \ |] ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) @= 0"; |
|
1258 by (asm_full_simp_tac (simpset() addsimps |
|
1259 [mem_infmal_iff RS sym]) 1); |
|
1260 by (rtac Infinitesimal_ratio 1); |
|
1261 by (rtac inf_close_hypreal_of_real_HFinite 3); |
|
1262 by (Auto_tac); |
|
1263 qed "NSDERIV_inf_close"; |
|
1264 |
|
1265 (*--------------------------------------------------------------- |
|
1266 from one version of differentiability |
|
1267 |
|
1268 f(x) - f(a) |
|
1269 --------------- @= Db |
|
1270 x - a |
|
1271 ---------------------------------------------------------------*) |
|
1272 Goal "[| NSDERIV f (g x) :> Da; \ |
|
1273 \ (*f* g) (hypreal_of_real(x) + xa) ~= hypreal_of_real (g x); \ |
|
1274 \ (*f* g) (hypreal_of_real(x) + xa) @= hypreal_of_real (g x) \ |
|
1275 \ |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \ |
|
1276 \ + - hypreal_of_real (f (g x)))* \ |
|
1277 \ hrinv ((*f* g) (hypreal_of_real(x) + xa) + \ |
|
1278 \ - hypreal_of_real (g x)) @= hypreal_of_real(Da)"; |
|
1279 by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2, |
|
1280 NSLIM_def,starfun_mult RS sym,hypreal_of_real_minus, |
|
1281 starfun_add RS sym,starfun_hrinv3])); |
|
1282 qed "NSDERIVD1"; |
|
1283 |
|
1284 (*-------------------------------------------------------------- |
|
1285 from other version of differentiability |
|
1286 |
|
1287 f(x + h) - f(x) |
|
1288 ----------------- @= Db |
|
1289 h |
|
1290 --------------------------------------------------------------*) |
|
1291 Goal "[| NSDERIV g x :> Db; xa: Infinitesimal; xa ~= 0 |] \ |
|
1292 \ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) * \ |
|
1293 \ hrinv xa @= hypreal_of_real(Db)"; |
|
1294 by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1295 NSLIM_def,starfun_mult RS sym,starfun_rinv_hrinv, |
|
1296 starfun_add RS sym,hypreal_of_real_zero,mem_infmal_iff, |
|
1297 starfun_lambda_cancel,hypreal_of_real_minus])); |
|
1298 qed "NSDERIVD2"; |
|
1299 |
|
1300 (*--------------------------------------------- |
|
1301 This proof uses both possible definitions |
|
1302 for differentiability. |
|
1303 --------------------------------------------*) |
|
1304 Goal "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] \ |
|
1305 \ ==> NSDERIV (f o g) x :> Da * Db"; |
|
1306 by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1307 NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1); |
|
1308 by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1); |
|
1309 by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym, |
|
1310 hypreal_of_real_minus,starfun_rinv_hrinv,hypreal_of_real_mult, |
|
1311 starfun_lambda_cancel2,starfun_o RS sym,starfun_mult RS sym])); |
|
1312 by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1); |
|
1313 by (dres_inst_tac [("g","g")] NSDERIV_zero 1); |
|
1314 by (auto_tac (claset(),simpset() |
|
1315 addsimps [hypreal_of_real_zero,inf_close_refl])); |
|
1316 by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"), |
|
1317 ("y1","hrinv xa")] (lemma_chain RS ssubst) 1); |
|
1318 by (etac (hypreal_not_eq_minus_iff RS iffD1) 1); |
|
1319 by (rtac inf_close_mult_hypreal_of_real 1); |
|
1320 by (blast_tac (claset() addIs [NSDERIVD1, |
|
1321 inf_close_minus_iff RS iffD2]) 1); |
|
1322 by (blast_tac (claset() addIs [NSDERIVD2]) 1); |
|
1323 qed "NSDERIV_chain"; |
|
1324 |
|
1325 (* standard version *) |
|
1326 Goal "!!f. [| DERIV f (g x) :> Da; \ |
|
1327 \ DERIV g x :> Db \ |
|
1328 \ |] ==> DERIV (f o g) x :> Da * Db"; |
|
1329 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
1330 NSDERIV_chain]) 1); |
|
1331 qed "DERIV_chain"; |
|
1332 |
|
1333 Goal "[| DERIV f g x :> Da; DERIV g x :> Db |] \ |
|
1334 \ ==> DERIV (%x. f (g x)) x :> Da * Db"; |
|
1335 by (auto_tac (claset() addDs [DERIV_chain],simpset() addsimps [o_def])); |
|
1336 qed "DERIV_chain2"; |
|
1337 |
|
1338 Goal "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"; |
|
1339 by (Auto_tac); |
|
1340 val lemma_DERIV_tac = result(); |
|
1341 |
|
1342 (*------------------------------------------------------------------ |
|
1343 Differentiation of natural number powers |
|
1344 ------------------------------------------------------------------*) |
|
1345 Goal "NSDERIV (%x. x) x :> #1"; |
|
1346 by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1347 NSLIM_def,starfun_mult RS sym,starfun_Id,hypreal_of_real_zero, |
|
1348 starfun_rinv_hrinv,hypreal_of_real_one] |
|
1349 @ real_add_ac)); |
|
1350 qed "NSDERIV_Id"; |
|
1351 Addsimps [NSDERIV_Id]; |
|
1352 |
|
1353 Goal "DERIV (%x. x) x :> #1"; |
|
1354 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1); |
|
1355 qed "DERIV_Id"; |
|
1356 Addsimps [DERIV_Id]; |
|
1357 |
|
1358 Goal "DERIV op * c x :> c"; |
|
1359 by (cut_inst_tac [("c","c"),("x","x")] (DERIV_Id RS DERIV_cmult) 1); |
|
1360 by (Asm_full_simp_tac 1); |
|
1361 qed "DERIV_cmult_Id"; |
|
1362 Addsimps [DERIV_cmult_Id]; |
|
1363 |
|
1364 Goal "NSDERIV op * c x :> c"; |
|
1365 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff]) 1); |
|
1366 qed "NSDERIV_cmult_Id"; |
|
1367 Addsimps [NSDERIV_cmult_Id]; |
|
1368 |
|
1369 Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))"; |
|
1370 by (induct_tac "n" 1); |
|
1371 by (dtac (DERIV_Id RS DERIV_mult) 2); |
|
1372 by (auto_tac (claset(),simpset() addsimps |
|
1373 [real_add_mult_distrib])); |
|
1374 by (case_tac "0 < n" 1); |
|
1375 by (dres_inst_tac [("x","x")] realpow_minus_mult 1); |
|
1376 by (auto_tac (claset(),simpset() addsimps |
|
1377 [real_mult_assoc,real_add_commute])); |
|
1378 qed "DERIV_pow"; |
|
1379 |
|
1380 (* NS version *) |
|
1381 Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))"; |
|
1382 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,DERIV_pow]) 1); |
|
1383 qed "NSDERIV_pow"; |
|
1384 |
|
1385 (*--------------------------------------------------------------- |
|
1386 Power of -1 |
|
1387 ---------------------------------------------------------------*) |
|
1388 Goalw [nsderiv_def] |
|
1389 "x ~= #0 ==> NSDERIV (%x. rinv(x)) x :> (- (rinv x ^ 2))"; |
|
1390 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
|
1391 by (forward_tac [Infinitesimal_add_not_zero] 1); |
|
1392 by (auto_tac (claset(),simpset() addsimps [starfun_rinv_hrinv, |
|
1393 hypreal_of_real_hrinv RS sym,hypreal_of_real_minus,realpow_two, |
|
1394 hypreal_of_real_mult] delsimps [hypreal_minus_mult_eq1 RS |
|
1395 sym,hypreal_minus_mult_eq2 RS sym])); |
|
1396 by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1); |
|
1397 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_add, |
|
1398 hrinv_mult_eq RS sym, hypreal_minus_hrinv RS sym] |
|
1399 @ hypreal_add_ac @ hypreal_mult_ac delsimps [hypreal_minus_mult_eq1 RS |
|
1400 sym,hypreal_minus_mult_eq2 RS sym] ) 1); |
|
1401 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym, |
|
1402 hypreal_add_mult_distrib2] delsimps [hypreal_minus_mult_eq1 RS |
|
1403 sym,hypreal_minus_mult_eq2 RS sym]) 1); |
|
1404 by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN |
|
1405 (2,Infinitesimal_HFinite_mult2)) RS |
|
1406 (Infinitesimal_minus_iff RS iffD1)) 1); |
|
1407 by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")] hypreal_mult_not_0 1); |
|
1408 by (res_inst_tac [("y"," hrinv(- hypreal_of_real x * hypreal_of_real x)")] inf_close_trans 2); |
|
1409 by (rtac hrinv_add_Infinitesimal_inf_close2 2); |
|
1410 by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1] |
|
1411 addSDs [Infinitesimal_minus_iff RS iffD2, |
|
1412 hypreal_of_real_HFinite_diff_Infinitesimal], simpset() addsimps |
|
1413 [hypreal_minus_hrinv RS sym,hypreal_of_real_mult RS sym])); |
|
1414 qed "NSDERIV_rinv"; |
|
1415 |
|
1416 Goal "x ~= #0 ==> DERIV (%x. rinv(x)) x :> (-(rinv x ^ 2))"; |
|
1417 by (asm_simp_tac (simpset() addsimps [NSDERIV_rinv, |
|
1418 NSDERIV_DERIV_iff RS sym] delsimps [thm "realpow_Suc"]) 1); |
|
1419 qed "DERIV_rinv"; |
|
1420 |
|
1421 (*-------------------------------------------------------------- |
|
1422 Derivative of inverse |
|
1423 -------------------------------------------------------------*) |
|
1424 Goal "[| DERIV f x :> d; f(x) ~= #0 |] \ |
|
1425 \ ==> DERIV (%x. rinv(f x)) x :> (- (d * rinv(f(x) ^ 2)))"; |
|
1426 by (rtac (real_mult_commute RS subst) 1); |
|
1427 by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1, |
|
1428 realpow_rinv] delsimps [thm "realpow_Suc", |
|
1429 real_minus_mult_eq1 RS sym]) 1); |
|
1430 by (fold_goals_tac [o_def]); |
|
1431 by (blast_tac (claset() addSIs [DERIV_chain,DERIV_rinv]) 1); |
|
1432 qed "DERIV_rinv_fun"; |
|
1433 |
|
1434 Goal "[| NSDERIV f x :> d; f(x) ~= #0 |] \ |
|
1435 \ ==> NSDERIV (%x. rinv(f x)) x :> (- (d * rinv(f(x) ^ 2)))"; |
|
1436 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
|
1437 DERIV_rinv_fun] delsimps [thm "realpow_Suc"]) 1); |
|
1438 qed "NSDERIV_rinv_fun"; |
|
1439 |
|
1440 (*-------------------------------------------------------------- |
|
1441 Derivative of quotient |
|
1442 -------------------------------------------------------------*) |
|
1443 Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \ |
|
1444 \ ==> DERIV (%y. f(y)*rinv(g y)) x :> (d*g(x) \ |
|
1445 \ + -(e*f(x)))*rinv(g(x) ^ 2)"; |
|
1446 by (dres_inst_tac [("f","g")] DERIV_rinv_fun 1); |
|
1447 by (dtac DERIV_mult 2); |
|
1448 by (REPEAT(assume_tac 1)); |
|
1449 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
|
1450 realpow_rinv,real_minus_mult_eq1] @ real_mult_ac delsimps |
|
1451 [thm "realpow_Suc",real_minus_mult_eq1 RS sym, |
|
1452 real_minus_mult_eq2 RS sym]) 1); |
|
1453 qed "DERIV_quotient"; |
|
1454 |
|
1455 Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \ |
|
1456 \ ==> NSDERIV (%y. f(y)*rinv(g y)) x :> (d*g(x) \ |
|
1457 \ + -(e*f(x)))*rinv(g(x) ^ 2)"; |
|
1458 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
|
1459 DERIV_quotient] delsimps [thm "realpow_Suc"]) 1); |
|
1460 qed "NSDERIV_quotient"; |
|
1461 |
|
1462 (* ------------------------------------------------------------------------ *) |
|
1463 (* Caratheodory formulation of derivative at a point: standard proof *) |
|
1464 (* ------------------------------------------------------------------------ *) |
|
1465 |
|
1466 Goal "(DERIV f x :> l) = \ |
|
1467 \ (EX g. (ALL z. f z - f x = g z * (z - x)) & isCont g x & g x = l)"; |
|
1468 by (Step_tac 1); |
|
1469 by (res_inst_tac |
|
1470 [("x","%z. if z = x then l else (f(z) - f(x)) * rinv (z - x)")] exI 1); |
|
1471 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc, |
|
1472 ARITH_PROVE "z ~= x ==> z - x ~= (#0::real)"])); |
|
1473 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff])); |
|
1474 by (ALLGOALS(rtac (LIM_equal RS iffD1))); |
|
1475 by (auto_tac (claset(),simpset() addsimps [real_diff_def,real_mult_assoc])); |
|
1476 qed "CARAT_DERIV"; |
|
1477 |
|
1478 Goal "NSDERIV f x :> l ==> \ |
|
1479 \ EX g. (ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l"; |
|
1480 by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff, |
|
1481 isNSCont_isCont_iff,CARAT_DERIV])); |
|
1482 qed "CARAT_NSDERIV"; |
|
1483 |
|
1484 (* How about a NS proof? *) |
|
1485 Goal "(ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \ |
|
1486 \ ==> NSDERIV f x :> l"; |
|
1487 by (auto_tac (claset(),simpset() addsimps [NSDERIV_iff2,starfun_mult |
|
1488 RS sym])); |
|
1489 by (rtac (starfun_hrinv2 RS subst) 1); |
|
1490 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc, |
|
1491 starfun_diff RS sym,starfun_Id])); |
|
1492 by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym, |
|
1493 hypreal_diff_def]) 1); |
|
1494 by (dtac (CLAIM_SIMP "x ~= y ==> x - y ~= (0::hypreal)" [hypreal_eq_minus_iff3 RS sym, |
|
1495 hypreal_diff_def]) 1); |
|
1496 by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1); |
|
1497 qed "CARAT_DERIVD"; |
|
1498 |
|
1499 (*--------------------------------------------------------------------*) |
|
1500 (* In this theory, still have to include Bisection theorem, IVT, MVT, *) |
|
1501 (* Rolle etc. *) |
|
1502 (*--------------------------------------------------------------------*) |
|
1503 |
|
1504 |
|
1505 |
|
1506 |
|
1507 |
|
1508 |