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 fun ARITH_PROVE str = prove_goal thy str |
|
9 (fn prems => [cut_facts_tac prems 1,arith_tac 1]); |
|
10 |
|
11 |
|
12 (*--------------------------------------------------------------- |
|
13 Theory of limits, continuity and differentiation of |
|
14 real=>real functions |
|
15 ----------------------------------------------------------------*) |
|
16 |
|
17 Goalw [LIM_def] "(%x. k) -- x --> k"; |
|
18 by Auto_tac; |
|
19 qed "LIM_const"; |
|
20 Addsimps [LIM_const]; |
|
21 |
|
22 (***-----------------------------------------------------------***) |
|
23 (*** Some Purely Standard Proofs - Can be used for comparison ***) |
|
24 (***-----------------------------------------------------------***) |
|
25 |
|
26 (*--------------- |
|
27 LIM_add |
|
28 ---------------*) |
|
29 Goalw [LIM_def] |
|
30 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
|
31 by (Clarify_tac 1); |
|
32 by (REPEAT(dres_inst_tac [("x","r/2")] spec 1)); |
|
33 by (Asm_full_simp_tac 1); |
|
34 by (Clarify_tac 1); |
|
35 by (res_inst_tac [("x","s"),("y","sa")] linorder_cases 1); |
|
36 by (res_inst_tac [("x","s")] exI 1); |
|
37 by (res_inst_tac [("x","sa")] exI 2); |
|
38 by (res_inst_tac [("x","sa")] exI 3); |
|
39 by Safe_tac; |
|
40 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
|
41 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
|
42 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
|
43 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
|
44 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
|
45 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
|
46 by (ALLGOALS(rtac (abs_sum_triangle_ineq RS order_le_less_trans))); |
|
47 by (ALLGOALS(rtac (real_sum_of_halves RS subst))); |
|
48 by (auto_tac (claset() addIs [add_strict_mono],simpset())); |
|
49 qed "LIM_add"; |
|
50 |
|
51 Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; |
|
52 by (subgoal_tac "ALL x. abs(- f x + L) = abs(f x + - L)" 1); |
|
53 by (Asm_full_simp_tac 1); |
|
54 by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1); |
|
55 qed "LIM_minus"; |
|
56 |
|
57 (*---------------------------------------------- |
|
58 LIM_add_minus |
|
59 ----------------------------------------------*) |
|
60 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
61 \ ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"; |
|
62 by (blast_tac (claset() addDs [LIM_add,LIM_minus]) 1); |
|
63 qed "LIM_add_minus"; |
|
64 |
|
65 (*---------------------------------------------- |
|
66 LIM_zero |
|
67 ----------------------------------------------*) |
|
68 Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"; |
|
69 by (res_inst_tac [("a1","l")] ((right_minus RS subst)) 1); |
|
70 by (rtac LIM_add_minus 1 THEN Auto_tac); |
|
71 qed "LIM_zero"; |
|
72 |
|
73 (*-------------------------- |
|
74 Limit not zero |
|
75 --------------------------*) |
|
76 Goalw [LIM_def] "k \\<noteq> 0 ==> ~ ((%x. k) -- x --> 0)"; |
|
77 by (res_inst_tac [("x","k"),("y","0")] linorder_cases 1); |
|
78 by (auto_tac (claset(), simpset() addsimps [real_abs_def])); |
|
79 by (res_inst_tac [("x","-k")] exI 1); |
|
80 by (res_inst_tac [("x","k")] exI 2); |
|
81 by Auto_tac; |
|
82 by (ALLGOALS(dres_inst_tac [("y","s")] real_dense)); |
|
83 by Safe_tac; |
|
84 by (ALLGOALS(res_inst_tac [("x","r + x")] exI)); |
|
85 by Auto_tac; |
|
86 qed "LIM_not_zero"; |
|
87 |
|
88 (* [| k \\<noteq> 0; (%x. k) -- x --> 0 |] ==> R *) |
|
89 bind_thm("LIM_not_zeroE", LIM_not_zero RS notE); |
|
90 |
|
91 Goal "(%x. k) -- x --> L ==> k = L"; |
|
92 by (rtac ccontr 1); |
|
93 by (dtac LIM_zero 1); |
|
94 by (rtac LIM_not_zeroE 1 THEN assume_tac 2); |
|
95 by (arith_tac 1); |
|
96 qed "LIM_const_eq"; |
|
97 |
|
98 (*------------------------ |
|
99 Limit is Unique |
|
100 ------------------------*) |
|
101 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M"; |
|
102 by (dtac LIM_minus 1); |
|
103 by (dtac LIM_add 1 THEN assume_tac 1); |
|
104 by (auto_tac (claset() addSDs [LIM_const_eq RS sym], simpset())); |
|
105 qed "LIM_unique"; |
|
106 |
|
107 (*------------- |
|
108 LIM_mult_zero |
|
109 -------------*) |
|
110 Goalw [LIM_def] |
|
111 "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"; |
|
112 by Safe_tac; |
|
113 by (dres_inst_tac [("x","1")] spec 1); |
|
114 by (dres_inst_tac [("x","r")] spec 1); |
|
115 by (cut_facts_tac [real_zero_less_one] 1); |
|
116 by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1); |
|
117 by (Clarify_tac 1); |
|
118 by (res_inst_tac [("x","s"),("y","sa")] |
|
119 linorder_cases 1); |
|
120 by (res_inst_tac [("x","s")] exI 1); |
|
121 by (res_inst_tac [("x","sa")] exI 2); |
|
122 by (res_inst_tac [("x","sa")] exI 3); |
|
123 by Safe_tac; |
|
124 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
|
125 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
|
126 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
|
127 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
|
128 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
|
129 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
|
130 by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst))); |
|
131 by (ALLGOALS(rtac abs_mult_less)); |
|
132 by Auto_tac; |
|
133 qed "LIM_mult_zero"; |
|
134 |
|
135 Goalw [LIM_def] "(%x. x) -- a --> a"; |
|
136 by Auto_tac; |
|
137 qed "LIM_self"; |
|
138 |
|
139 (*-------------------------------------------------------------- |
|
140 Limits are equal for functions equal except at limit point |
|
141 --------------------------------------------------------------*) |
|
142 Goalw [LIM_def] |
|
143 "[| \\<forall>x. x \\<noteq> a --> (f x = g x) |] \ |
|
144 \ ==> (f -- a --> l) = (g -- a --> l)"; |
|
145 by (auto_tac (claset(), simpset() addsimps [real_add_minus_iff])); |
|
146 qed "LIM_equal"; |
|
147 |
|
148 Goal "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] \ |
|
149 \ ==> f -- a --> l"; |
|
150 by (dtac LIM_add 1 THEN assume_tac 1); |
|
151 by (auto_tac (claset(), simpset() addsimps [real_add_assoc])); |
|
152 qed "LIM_trans"; |
|
153 |
|
154 (***-------------------------------------------------------------***) |
|
155 (*** End of Purely Standard Proofs ***) |
|
156 (***-------------------------------------------------------------***) |
|
157 (*-------------------------------------------------------------- |
|
158 Standard and NS definitions of Limit |
|
159 --------------------------------------------------------------*) |
|
160 Goalw [LIM_def,NSLIM_def,approx_def] |
|
161 "f -- x --> L ==> f -- x --NS> L"; |
|
162 by (asm_full_simp_tac |
|
163 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
164 by Safe_tac; |
|
165 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
|
166 by (auto_tac (claset(), |
|
167 simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus, |
|
168 hypreal_of_real_def, hypreal_add])); |
|
169 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1); |
|
170 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1); |
|
171 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1); |
|
172 by (subgoal_tac "\\<forall>n::nat. (xa n) \\<noteq> x & \ |
|
173 \ abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u" 1); |
|
174 by (Blast_tac 2); |
|
175 by (dtac FreeUltrafilterNat_all 1); |
|
176 by (Ultra_tac 1); |
|
177 qed "LIM_NSLIM"; |
|
178 |
|
179 (*--------------------------------------------------------------------- |
|
180 Limit: NS definition ==> standard definition |
|
181 ---------------------------------------------------------------------*) |
|
182 |
|
183 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
|
184 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
|
185 \ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \ |
|
186 \ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)"; |
|
187 by (Clarify_tac 1); |
|
188 by (cut_inst_tac [("n1","n")] |
|
189 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
|
190 by Auto_tac; |
|
191 qed "lemma_LIM"; |
|
192 |
|
193 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
|
194 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
|
195 \ ==> \\<exists>X. \\<forall>n::nat. X n \\<noteq> x & \ |
|
196 \ abs(X n + -x) < inverse(real(Suc n)) & r \\<le> abs(f (X n) + -L)"; |
|
197 by (dtac lemma_LIM 1); |
|
198 by (dtac choice 1); |
|
199 by (Blast_tac 1); |
|
200 qed "lemma_skolemize_LIM2"; |
|
201 |
|
202 Goal "\\<forall>n. X n \\<noteq> x & \ |
|
203 \ abs (X n + - x) < inverse (real(Suc n)) & \ |
|
204 \ r \\<le> abs (f (X n) + - L) ==> \ |
|
205 \ \\<forall>n. abs (X n + - x) < inverse (real(Suc n))"; |
|
206 by (Auto_tac ); |
|
207 qed "lemma_simp"; |
|
208 |
|
209 (*------------------- |
|
210 NSLIM => LIM |
|
211 -------------------*) |
|
212 |
|
213 Goalw [LIM_def,NSLIM_def,approx_def] |
|
214 "f -- x --NS> L ==> f -- x --> L"; |
|
215 by (asm_full_simp_tac |
|
216 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
217 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
|
218 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
|
219 by (dtac lemma_skolemize_LIM2 1); |
|
220 by Safe_tac; |
|
221 by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1); |
|
222 by (auto_tac |
|
223 (claset(), |
|
224 simpset() addsimps [starfun, hypreal_minus, |
|
225 hypreal_of_real_def,hypreal_add])); |
|
226 by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1); |
|
227 by (asm_full_simp_tac |
|
228 (simpset() addsimps |
|
229 [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def, |
|
230 hypreal_minus, hypreal_add]) 1); |
|
231 by (Blast_tac 1); |
|
232 by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1); |
|
233 by (dtac FreeUltrafilterNat_all 1); |
|
234 by (Ultra_tac 1); |
|
235 qed "NSLIM_LIM"; |
|
236 |
|
237 |
|
238 (**** Key result ****) |
|
239 Goal "(f -- x --> L) = (f -- x --NS> L)"; |
|
240 by (blast_tac (claset() addIs [LIM_NSLIM,NSLIM_LIM]) 1); |
|
241 qed "LIM_NSLIM_iff"; |
|
242 |
|
243 (*-------------------------------------------------------------------*) |
|
244 (* Proving properties of limits using nonstandard definition and *) |
|
245 (* hence, the properties hold for standard limits as well *) |
|
246 (*-------------------------------------------------------------------*) |
|
247 (*------------------------------------------------ |
|
248 NSLIM_mult and hence (trivially) LIM_mult |
|
249 ------------------------------------------------*) |
|
250 |
|
251 Goalw [NSLIM_def] |
|
252 "[| f -- x --NS> l; g -- x --NS> m |] \ |
|
253 \ ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"; |
|
254 by (auto_tac (claset() addSIs [approx_mult_HFinite], simpset())); |
|
255 qed "NSLIM_mult"; |
|
256 |
|
257 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
258 \ ==> (%x. f(x) * g(x)) -- x --> (l * m)"; |
|
259 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_mult]) 1); |
|
260 qed "LIM_mult2"; |
|
261 |
|
262 (*---------------------------------------------- |
|
263 NSLIM_add and hence (trivially) LIM_add |
|
264 Note the much shorter proof |
|
265 ----------------------------------------------*) |
|
266 Goalw [NSLIM_def] |
|
267 "[| f -- x --NS> l; g -- x --NS> m |] \ |
|
268 \ ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"; |
|
269 by (auto_tac (claset() addSIs [approx_add], simpset())); |
|
270 qed "NSLIM_add"; |
|
271 |
|
272 Goal "[| f -- x --> l; g -- x --> m |] \ |
|
273 \ ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
|
274 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_add]) 1); |
|
275 qed "LIM_add2"; |
|
276 |
|
277 (*---------------------------------------------- |
|
278 NSLIM_const |
|
279 ----------------------------------------------*) |
|
280 Goalw [NSLIM_def] "(%x. k) -- x --NS> k"; |
|
281 by Auto_tac; |
|
282 qed "NSLIM_const"; |
|
283 |
|
284 Addsimps [NSLIM_const]; |
|
285 |
|
286 Goal "(%x. k) -- x --> k"; |
|
287 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
288 qed "LIM_const2"; |
|
289 |
|
290 (*---------------------------------------------- |
|
291 NSLIM_minus |
|
292 ----------------------------------------------*) |
|
293 Goalw [NSLIM_def] |
|
294 "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"; |
|
295 by Auto_tac; |
|
296 qed "NSLIM_minus"; |
|
297 |
|
298 Goal "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; |
|
299 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_minus]) 1); |
|
300 qed "LIM_minus2"; |
|
301 |
|
302 (*---------------------------------------------- |
|
303 NSLIM_add_minus |
|
304 ----------------------------------------------*) |
|
305 Goal "[| f -- x --NS> l; g -- x --NS> m |] \ |
|
306 \ ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"; |
|
307 by (blast_tac (claset() addDs [NSLIM_add,NSLIM_minus]) 1); |
|
308 qed "NSLIM_add_minus"; |
|
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_minus]) 1); |
|
314 qed "LIM_add_minus2"; |
|
315 |
|
316 (*----------------------------- |
|
317 NSLIM_inverse |
|
318 -----------------------------*) |
|
319 Goalw [NSLIM_def] |
|
320 "[| f -- a --NS> L; L \\<noteq> 0 |] \ |
|
321 \ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"; |
|
322 by (Clarify_tac 1); |
|
323 by (dtac spec 1); |
|
324 by (auto_tac (claset(), |
|
325 simpset() addsimps [hypreal_of_real_approx_inverse])); |
|
326 qed "NSLIM_inverse"; |
|
327 |
|
328 Goal "[| f -- a --> L; \ |
|
329 \ L \\<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"; |
|
330 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1); |
|
331 qed "LIM_inverse"; |
|
332 |
|
333 (*------------------------------ |
|
334 NSLIM_zero |
|
335 ------------------------------*) |
|
336 Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> 0"; |
|
337 by (res_inst_tac [("a1","l")] ((right_minus RS subst)) 1); |
|
338 by (rtac NSLIM_add_minus 1 THEN Auto_tac); |
|
339 qed "NSLIM_zero"; |
|
340 |
|
341 Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"; |
|
342 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1); |
|
343 qed "LIM_zero2"; |
|
344 |
|
345 Goal "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"; |
|
346 by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1); |
|
347 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc])); |
|
348 qed "NSLIM_zero_cancel"; |
|
349 |
|
350 Goal "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"; |
|
351 by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1); |
|
352 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc])); |
|
353 qed "LIM_zero_cancel"; |
|
354 |
|
355 |
|
356 (*-------------------------- |
|
357 NSLIM_not_zero |
|
358 --------------------------*) |
|
359 Goalw [NSLIM_def] "k \\<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"; |
|
360 by Auto_tac; |
|
361 by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1); |
|
362 by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym], |
|
363 simpset() addsimps [hypreal_epsilon_not_zero])); |
|
364 qed "NSLIM_not_zero"; |
|
365 |
|
366 (* [| k \\<noteq> 0; (%x. k) -- x --NS> 0 |] ==> R *) |
|
367 bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE); |
|
368 |
|
369 Goal "k \\<noteq> 0 ==> ~ ((%x. k) -- x --> 0)"; |
|
370 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1); |
|
371 qed "LIM_not_zero2"; |
|
372 |
|
373 (*------------------------------------- |
|
374 NSLIM of constant function |
|
375 -------------------------------------*) |
|
376 Goal "(%x. k) -- x --NS> L ==> k = L"; |
|
377 by (rtac ccontr 1); |
|
378 by (dtac NSLIM_zero 1); |
|
379 by (rtac NSLIM_not_zeroE 1 THEN assume_tac 2); |
|
380 by (arith_tac 1); |
|
381 qed "NSLIM_const_eq"; |
|
382 |
|
383 Goal "(%x. k) -- x --> L ==> k = L"; |
|
384 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, |
|
385 NSLIM_const_eq]) 1); |
|
386 qed "LIM_const_eq2"; |
|
387 |
|
388 (*------------------------ |
|
389 NS Limit is Unique |
|
390 ------------------------*) |
|
391 (* can actually be proved more easily by unfolding def! *) |
|
392 Goal "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M"; |
|
393 by (dtac NSLIM_minus 1); |
|
394 by (dtac NSLIM_add 1 THEN assume_tac 1); |
|
395 by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym], simpset())); |
|
396 qed "NSLIM_unique"; |
|
397 |
|
398 Goal "[| f -- x --> L; f -- x --> M |] ==> L = M"; |
|
399 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_unique]) 1); |
|
400 qed "LIM_unique2"; |
|
401 |
|
402 (*-------------------- |
|
403 NSLIM_mult_zero |
|
404 --------------------*) |
|
405 Goal "[| f -- x --NS> 0; g -- x --NS> 0 |] \ |
|
406 \ ==> (%x. f(x)*g(x)) -- x --NS> 0"; |
|
407 by (dtac NSLIM_mult 1 THEN Auto_tac); |
|
408 qed "NSLIM_mult_zero"; |
|
409 |
|
410 (* we can use the corresponding thm LIM_mult2 *) |
|
411 (* for standard definition of limit *) |
|
412 |
|
413 Goal "[| f -- x --> 0; g -- x --> 0 |] \ |
|
414 \ ==> (%x. f(x)*g(x)) -- x --> 0"; |
|
415 by (dtac LIM_mult2 1 THEN Auto_tac); |
|
416 qed "LIM_mult_zero2"; |
|
417 |
|
418 (*---------------------------- |
|
419 NSLIM_self |
|
420 ----------------------------*) |
|
421 Goalw [NSLIM_def] "(%x. x) -- a --NS> a"; |
|
422 by (auto_tac (claset() addIs [starfun_Idfun_approx],simpset())); |
|
423 qed "NSLIM_self"; |
|
424 |
|
425 Goal "(%x. x) -- a --> a"; |
|
426 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff,NSLIM_self]) 1); |
|
427 qed "LIM_self2"; |
|
428 |
|
429 (*----------------------------------------------------------------------------- |
|
430 Derivatives and Continuity - NS and Standard properties |
|
431 -----------------------------------------------------------------------------*) |
|
432 (*--------------- |
|
433 Continuity |
|
434 ---------------*) |
|
435 |
|
436 Goalw [isNSCont_def] |
|
437 "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \ |
|
438 \ ==> ( *f* f) y \\<approx> hypreal_of_real (f a)"; |
|
439 by (Blast_tac 1); |
|
440 qed "isNSContD"; |
|
441 |
|
442 Goalw [isNSCont_def,NSLIM_def] |
|
443 "isNSCont f a ==> f -- a --NS> (f a) "; |
|
444 by (Blast_tac 1); |
|
445 qed "isNSCont_NSLIM"; |
|
446 |
|
447 Goalw [isNSCont_def,NSLIM_def] |
|
448 "f -- a --NS> (f a) ==> isNSCont f a"; |
|
449 by Auto_tac; |
|
450 by (res_inst_tac [("Q","y = hypreal_of_real a")] |
|
451 (excluded_middle RS disjE) 1); |
|
452 by Auto_tac; |
|
453 qed "NSLIM_isNSCont"; |
|
454 |
|
455 (*----------------------------------------------------- |
|
456 NS continuity can be defined using NS Limit in |
|
457 similar fashion to standard def of continuity |
|
458 -----------------------------------------------------*) |
|
459 Goal "(isNSCont f a) = (f -- a --NS> (f a))"; |
|
460 by (blast_tac (claset() addIs [isNSCont_NSLIM,NSLIM_isNSCont]) 1); |
|
461 qed "isNSCont_NSLIM_iff"; |
|
462 |
|
463 (*---------------------------------------------- |
|
464 Hence, NS continuity can be given |
|
465 in terms of standard limit |
|
466 ---------------------------------------------*) |
|
467 Goal "(isNSCont f a) = (f -- a --> (f a))"; |
|
468 by (asm_full_simp_tac (simpset() addsimps |
|
469 [LIM_NSLIM_iff,isNSCont_NSLIM_iff]) 1); |
|
470 qed "isNSCont_LIM_iff"; |
|
471 |
|
472 (*----------------------------------------------- |
|
473 Moreover, it's trivial now that NS continuity |
|
474 is equivalent to standard continuity |
|
475 -----------------------------------------------*) |
|
476 Goalw [isCont_def] "(isNSCont f a) = (isCont f a)"; |
|
477 by (rtac isNSCont_LIM_iff 1); |
|
478 qed "isNSCont_isCont_iff"; |
|
479 |
|
480 (*---------------------------------------- |
|
481 Standard continuity ==> NS continuity |
|
482 ----------------------------------------*) |
|
483 Goal "isCont f a ==> isNSCont f a"; |
|
484 by (etac (isNSCont_isCont_iff RS iffD2) 1); |
|
485 qed "isCont_isNSCont"; |
|
486 |
|
487 (*---------------------------------------- |
|
488 NS continuity ==> Standard continuity |
|
489 ----------------------------------------*) |
|
490 Goal "isNSCont f a ==> isCont f a"; |
|
491 by (etac (isNSCont_isCont_iff RS iffD1) 1); |
|
492 qed "isNSCont_isCont"; |
|
493 |
|
494 (*-------------------------------------------------------------------------- |
|
495 Alternative definition of continuity |
|
496 --------------------------------------------------------------------------*) |
|
497 (* Prove equivalence between NS limits - *) |
|
498 (* seems easier than using standard def *) |
|
499 Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"; |
|
500 by Auto_tac; |
|
501 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1); |
|
502 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2); |
|
503 by Safe_tac; |
|
504 by (Asm_full_simp_tac 1); |
|
505 by (rtac ((mem_infmal_iff RS iffD2) RS |
|
506 (Infinitesimal_add_approx_self RS approx_sym)) 1); |
|
507 by (rtac (approx_minus_iff2 RS iffD1) 4); |
|
508 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3); |
|
509 by (res_inst_tac [("z","x")] eq_Abs_hypreal 2); |
|
510 by (res_inst_tac [("z","x")] eq_Abs_hypreal 4); |
|
511 by (auto_tac (claset(), |
|
512 simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus, |
|
513 hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def])); |
|
514 qed "NSLIM_h_iff"; |
|
515 |
|
516 Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"; |
|
517 by (rtac NSLIM_h_iff 1); |
|
518 qed "NSLIM_isCont_iff"; |
|
519 |
|
520 Goal "(f -- a --> f a) = ((%h. f(a + h)) -- 0 --> f(a))"; |
|
521 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1); |
|
522 qed "LIM_isCont_iff"; |
|
523 |
|
524 Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))"; |
|
525 by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1); |
|
526 qed "isCont_iff"; |
|
527 |
|
528 (*-------------------------------------------------------------------------- |
|
529 Immediate application of nonstandard criterion for continuity can offer |
|
530 very simple proofs of some standard property of continuous functions |
|
531 --------------------------------------------------------------------------*) |
|
532 (*------------------------ |
|
533 sum continuous |
|
534 ------------------------*) |
|
535 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"; |
|
536 by (auto_tac (claset() addIs [approx_add], |
|
537 simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def])); |
|
538 qed "isCont_add"; |
|
539 |
|
540 (*------------------------ |
|
541 mult continuous |
|
542 ------------------------*) |
|
543 Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"; |
|
544 by (auto_tac (claset() addSIs [starfun_mult_HFinite_approx], |
|
545 simpset() delsimps [starfun_mult RS sym] |
|
546 addsimps [isNSCont_isCont_iff RS sym, isNSCont_def])); |
|
547 qed "isCont_mult"; |
|
548 |
|
549 (*------------------------------------------- |
|
550 composition of continuous functions |
|
551 Note very short straightforard proof! |
|
552 ------------------------------------------*) |
|
553 Goal "[| isCont f a; isCont g (f a) |] \ |
|
554 \ ==> isCont (g o f) a"; |
|
555 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
|
556 isNSCont_def,starfun_o RS sym])); |
|
557 qed "isCont_o"; |
|
558 |
|
559 Goal "[| isCont f a; isCont g (f a) |] \ |
|
560 \ ==> isCont (%x. g (f x)) a"; |
|
561 by (auto_tac (claset() addDs [isCont_o],simpset() addsimps [o_def])); |
|
562 qed "isCont_o2"; |
|
563 |
|
564 Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a"; |
|
565 by Auto_tac; |
|
566 qed "isNSCont_minus"; |
|
567 |
|
568 Goal "isCont f a ==> isCont (%x. - f x) a"; |
|
569 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
|
570 isNSCont_minus])); |
|
571 qed "isCont_minus"; |
|
572 |
|
573 Goalw [isCont_def] |
|
574 "[| isCont f x; f x \\<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"; |
|
575 by (blast_tac (claset() addIs [LIM_inverse]) 1); |
|
576 qed "isCont_inverse"; |
|
577 |
|
578 Goal "[| isNSCont f x; f x \\<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"; |
|
579 by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps |
|
580 [isNSCont_isCont_iff])); |
|
581 qed "isNSCont_inverse"; |
|
582 |
|
583 Goalw [real_diff_def] |
|
584 "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"; |
|
585 by (auto_tac (claset() addIs [isCont_add,isCont_minus],simpset())); |
|
586 qed "isCont_diff"; |
|
587 |
|
588 Goalw [isCont_def] "isCont (%x. k) a"; |
|
589 by (Simp_tac 1); |
|
590 qed "isCont_const"; |
|
591 Addsimps [isCont_const]; |
|
592 |
|
593 Goalw [isNSCont_def] "isNSCont (%x. k) a"; |
|
594 by (Simp_tac 1); |
|
595 qed "isNSCont_const"; |
|
596 Addsimps [isNSCont_const]; |
|
597 |
|
598 Goalw [isNSCont_def] "isNSCont abs a"; |
|
599 by (auto_tac (claset() addIs [approx_hrabs], |
|
600 simpset() addsimps [hypreal_of_real_hrabs RS sym, |
|
601 starfun_rabs_hrabs])); |
|
602 qed "isNSCont_rabs"; |
|
603 Addsimps [isNSCont_rabs]; |
|
604 |
|
605 Goal "isCont abs a"; |
|
606 by (auto_tac (claset(), simpset() addsimps [isNSCont_isCont_iff RS sym])); |
|
607 qed "isCont_rabs"; |
|
608 Addsimps [isCont_rabs]; |
|
609 |
|
610 (**************************************************************** |
|
611 (%* Leave as commented until I add topology theory or remove? *%) |
|
612 (%*------------------------------------------------------------ |
|
613 Elementary topology proof for a characterisation of |
|
614 continuity now: a function f is continuous if and only |
|
615 if the inverse image, {x. f(x) \\<in> A}, of any open set A |
|
616 is always an open set |
|
617 ------------------------------------------------------------*%) |
|
618 Goal "[| isNSopen A; \\<forall>x. isNSCont f x |] \ |
|
619 \ ==> isNSopen {x. f x \\<in> A}"; |
|
620 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
|
621 by (dtac (mem_monad_approx RS approx_sym) 1); |
|
622 by (dres_inst_tac [("x","a")] spec 1); |
|
623 by (dtac isNSContD 1 THEN assume_tac 1); |
|
624 by (dtac bspec 1 THEN assume_tac 1); |
|
625 by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); |
|
626 by (blast_tac (claset() addIs [starfun_mem_starset]) 1); |
|
627 qed "isNSCont_isNSopen"; |
|
628 |
|
629 Goalw [isNSCont_def] |
|
630 "\\<forall>A. isNSopen A --> isNSopen {x. f x \\<in> A} \ |
|
631 \ ==> isNSCont f x"; |
|
632 by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS |
|
633 (approx_minus_iff RS iffD2)],simpset() addsimps |
|
634 [Infinitesimal_def,SReal_iff])); |
|
635 by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); |
|
636 by (etac (isNSopen_open_interval RSN (2,impE)) 1); |
|
637 by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); |
|
638 by (dres_inst_tac [("x","x")] spec 1); |
|
639 by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], |
|
640 simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); |
|
641 qed "isNSopen_isNSCont"; |
|
642 |
|
643 Goal "(\\<forall>x. isNSCont f x) = \ |
|
644 \ (\\<forall>A. isNSopen A --> isNSopen {x. f(x) \\<in> A})"; |
|
645 by (blast_tac (claset() addIs [isNSCont_isNSopen, |
|
646 isNSopen_isNSCont]) 1); |
|
647 qed "isNSCont_isNSopen_iff"; |
|
648 |
|
649 (%*------- Standard version of same theorem --------*%) |
|
650 Goal "(\\<forall>x. isCont f x) = \ |
|
651 \ (\\<forall>A. isopen A --> isopen {x. f(x) \\<in> A})"; |
|
652 by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], |
|
653 simpset() addsimps [isNSopen_isopen_iff RS sym, |
|
654 isNSCont_isCont_iff RS sym])); |
|
655 qed "isCont_isopen_iff"; |
|
656 *******************************************************************) |
|
657 |
|
658 (*----------------------------------------------------------------- |
|
659 Uniform continuity |
|
660 ------------------------------------------------------------------*) |
|
661 Goalw [isNSUCont_def] |
|
662 "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y"; |
|
663 by (Blast_tac 1); |
|
664 qed "isNSUContD"; |
|
665 |
|
666 Goalw [isUCont_def,isCont_def,LIM_def] |
|
667 "isUCont f ==> isCont f x"; |
|
668 by (Clarify_tac 1); |
|
669 by (dtac spec 1); |
|
670 by (Blast_tac 1); |
|
671 qed "isUCont_isCont"; |
|
672 |
|
673 Goalw [isNSUCont_def,isUCont_def,approx_def] |
|
674 "isUCont f ==> isNSUCont f"; |
|
675 by (asm_full_simp_tac (simpset() addsimps |
|
676 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
677 by Safe_tac; |
|
678 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
679 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
680 by (auto_tac (claset(),simpset() addsimps [starfun, |
|
681 hypreal_minus, hypreal_add])); |
|
682 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1); |
|
683 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1); |
|
684 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1); |
|
685 by (subgoal_tac "\\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u" 1); |
|
686 by (Blast_tac 2); |
|
687 by (thin_tac "\\<forall>x y. abs (x + - y) < s --> abs (f x + - f y) < u" 1); |
|
688 by (dtac FreeUltrafilterNat_all 1); |
|
689 by (Ultra_tac 1); |
|
690 qed "isUCont_isNSUCont"; |
|
691 |
|
692 Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \ |
|
693 \ ==> \\<forall>n::nat. \\<exists>z y. \ |
|
694 \ abs(z + -y) < inverse(real(Suc n)) & \ |
|
695 \ r \\<le> abs(f z + -f y)"; |
|
696 by (Clarify_tac 1); |
|
697 by (cut_inst_tac [("n1","n")] |
|
698 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
|
699 by Auto_tac; |
|
700 qed "lemma_LIMu"; |
|
701 |
|
702 Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \ |
|
703 \ ==> \\<exists>X Y. \\<forall>n::nat. \ |
|
704 \ abs(X n + -(Y n)) < inverse(real(Suc n)) & \ |
|
705 \ r \\<le> abs(f (X n) + -f (Y n))"; |
|
706 by (dtac lemma_LIMu 1); |
|
707 by (dtac choice 1); |
|
708 by Safe_tac; |
|
709 by (dtac choice 1); |
|
710 by (Blast_tac 1); |
|
711 qed "lemma_skolemize_LIM2u"; |
|
712 |
|
713 Goal "\\<forall>n. abs (X n + -Y n) < inverse (real(Suc n)) & \ |
|
714 \ r \\<le> abs (f (X n) + - f(Y n)) ==> \ |
|
715 \ \\<forall>n. abs (X n + - Y n) < inverse (real(Suc n))"; |
|
716 by (Auto_tac ); |
|
717 qed "lemma_simpu"; |
|
718 |
|
719 Goalw [isNSUCont_def,isUCont_def,approx_def] |
|
720 "isNSUCont f ==> isUCont f"; |
|
721 by (asm_full_simp_tac (simpset() addsimps |
|
722 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
|
723 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
|
724 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
|
725 by (dtac lemma_skolemize_LIM2u 1); |
|
726 by Safe_tac; |
|
727 by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1); |
|
728 by (dres_inst_tac [("x","Abs_hypreal(hyprel``{Y})")] spec 1); |
|
729 by (asm_full_simp_tac |
|
730 (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1); |
|
731 by Auto_tac; |
|
732 by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1); |
|
733 by (asm_full_simp_tac (simpset() addsimps |
|
734 [Infinitesimal_FreeUltrafilterNat_iff, hypreal_minus,hypreal_add]) 1); |
|
735 by (Blast_tac 1); |
|
736 by (rotate_tac 2 1); |
|
737 by (dres_inst_tac [("x","r")] spec 1); |
|
738 by (Clarify_tac 1); |
|
739 by (dtac FreeUltrafilterNat_all 1); |
|
740 by (Ultra_tac 1); |
|
741 qed "isNSUCont_isUCont"; |
|
742 |
|
743 (*------------------------------------------------------------------ |
|
744 Derivatives |
|
745 ------------------------------------------------------------------*) |
|
746 Goalw [deriv_def] |
|
747 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)"; |
|
748 by (Blast_tac 1); |
|
749 qed "DERIV_iff"; |
|
750 |
|
751 Goalw [deriv_def] |
|
752 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"; |
|
753 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
754 qed "DERIV_NS_iff"; |
|
755 |
|
756 Goalw [deriv_def] |
|
757 "DERIV f x :> D \ |
|
758 \ ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"; |
|
759 by (Blast_tac 1); |
|
760 qed "DERIVD"; |
|
761 |
|
762 Goalw [deriv_def] "DERIV f x :> D ==> \ |
|
763 \ (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"; |
|
764 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
|
765 qed "NS_DERIVD"; |
|
766 |
|
767 (* Uniqueness *) |
|
768 Goalw [deriv_def] |
|
769 "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"; |
|
770 by (blast_tac (claset() addIs [LIM_unique]) 1); |
|
771 qed "DERIV_unique"; |
|
772 |
|
773 Goalw [nsderiv_def] |
|
774 "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"; |
|
775 by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1); |
|
776 by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec] |
|
777 addSIs [inj_hypreal_of_real RS injD] |
|
778 addDs [approx_trans3], |
|
779 simpset())); |
|
780 qed "NSDeriv_unique"; |
|
781 |
|
782 (*------------------------------------------------------------------------ |
|
783 Differentiable |
|
784 ------------------------------------------------------------------------*) |
|
785 |
|
786 Goalw [differentiable_def] |
|
787 "f differentiable x ==> \\<exists>D. DERIV f x :> D"; |
|
788 by (assume_tac 1); |
|
789 qed "differentiableD"; |
|
790 |
|
791 Goalw [differentiable_def] |
|
792 "DERIV f x :> D ==> f differentiable x"; |
|
793 by (Blast_tac 1); |
|
794 qed "differentiableI"; |
|
795 |
|
796 Goalw [NSdifferentiable_def] |
|
797 "f NSdifferentiable x ==> \\<exists>D. NSDERIV f x :> D"; |
|
798 by (assume_tac 1); |
|
799 qed "NSdifferentiableD"; |
|
800 |
|
801 Goalw [NSdifferentiable_def] |
|
802 "NSDERIV f x :> D ==> f NSdifferentiable x"; |
|
803 by (Blast_tac 1); |
|
804 qed "NSdifferentiableI"; |
|
805 |
|
806 (*-------------------------------------------------------- |
|
807 Alternative definition for differentiability |
|
808 -------------------------------------------------------*) |
|
809 |
|
810 Goalw [LIM_def] |
|
811 "((%h. (f(a + h) + - f(a))/h) -- 0 --> D) = \ |
|
812 \ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)"; |
|
813 by Safe_tac; |
|
814 by (ALLGOALS(dtac spec)); |
|
815 by Safe_tac; |
|
816 by (Blast_tac 1 THEN Blast_tac 2); |
|
817 by (ALLGOALS(res_inst_tac [("x","s")] exI)); |
|
818 by Safe_tac; |
|
819 by (dres_inst_tac [("x","x + -a")] spec 1); |
|
820 by (dres_inst_tac [("x","x + a")] spec 2); |
|
821 by (auto_tac (claset(), simpset() addsimps add_ac)); |
|
822 qed "DERIV_LIM_iff"; |
|
823 |
|
824 Goalw [deriv_def] "(DERIV f x :> D) = \ |
|
825 \ ((%z. (f(z) + -f(x)) / (z + -x)) -- x --> D)"; |
|
826 by (simp_tac (simpset() addsimps [DERIV_LIM_iff]) 1); |
|
827 qed "DERIV_iff2"; |
|
828 |
|
829 (*-------------------------------------------------------- |
|
830 Equivalence of NS and standard defs of differentiation |
|
831 -------------------------------------------------------*) |
|
832 (*------------------------------------------- |
|
833 First NSDERIV in terms of NSLIM |
|
834 -------------------------------------------*) |
|
835 |
|
836 (*--- first equivalence ---*) |
|
837 Goalw [nsderiv_def,NSLIM_def] |
|
838 "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"; |
|
839 by Auto_tac; |
|
840 by (dres_inst_tac [("x","xa")] bspec 1); |
|
841 by (rtac ccontr 3); |
|
842 by (dres_inst_tac [("x","h")] spec 3); |
|
843 by (auto_tac (claset(), |
|
844 simpset() addsimps [mem_infmal_iff, starfun_lambda_cancel])); |
|
845 qed "NSDERIV_NSLIM_iff"; |
|
846 |
|
847 (*--- second equivalence ---*) |
|
848 Goal "(NSDERIV f x :> D) = \ |
|
849 \ ((%z. (f(z) + -f(x)) / (z + -x)) -- x --NS> D)"; |
|
850 by (full_simp_tac (simpset() addsimps |
|
851 [NSDERIV_NSLIM_iff, DERIV_LIM_iff, LIM_NSLIM_iff RS sym]) 1); |
|
852 qed "NSDERIV_NSLIM_iff2"; |
|
853 |
|
854 (* while we're at it! *) |
|
855 Goalw [real_diff_def] |
|
856 "(NSDERIV f x :> D) = \ |
|
857 \ (\\<forall>xa. \ |
|
858 \ xa \\<noteq> hypreal_of_real x & xa \\<approx> hypreal_of_real x --> \ |
|
859 \ ( *f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)"; |
|
860 by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); |
|
861 qed "NSDERIV_iff2"; |
|
862 |
|
863 |
|
864 Goal "(NSDERIV f x :> D) ==> \ |
|
865 \ (\\<forall>u. \ |
|
866 \ u \\<approx> hypreal_of_real x --> \ |
|
867 \ ( *f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))"; |
|
868 by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2])); |
|
869 by (case_tac "u = hypreal_of_real x" 1); |
|
870 by (auto_tac (claset(), simpset() addsimps [hypreal_diff_def])); |
|
871 by (dres_inst_tac [("x","u")] spec 1); |
|
872 by Auto_tac; |
|
873 by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")] |
|
874 approx_mult1 1); |
|
875 by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1))); |
|
876 by (subgoal_tac "( *f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2); |
|
877 by (auto_tac (claset(), |
|
878 simpset() addsimps [real_diff_def, hypreal_diff_def, |
|
879 (approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2), |
|
880 Infinitesimal_subset_HFinite RS subsetD])); |
|
881 qed "NSDERIVD5"; |
|
882 |
|
883 Goal "(NSDERIV f x :> D) ==> \ |
|
884 \ (\\<forall>h \\<in> Infinitesimal. \ |
|
885 \ (( *f* f)(hypreal_of_real x + h) - \ |
|
886 \ hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)"; |
|
887 by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); |
|
888 by (case_tac "h = (0::hypreal)" 1); |
|
889 by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def])); |
|
890 by (dres_inst_tac [("x","h")] bspec 1); |
|
891 by (dres_inst_tac [("c","h")] approx_mult1 2); |
|
892 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
893 simpset() addsimps [hypreal_diff_def])); |
|
894 qed "NSDERIVD4"; |
|
895 |
|
896 Goal "(NSDERIV f x :> D) ==> \ |
|
897 \ (\\<forall>h \\<in> Infinitesimal - {0}. \ |
|
898 \ (( *f* f)(hypreal_of_real x + h) - \ |
|
899 \ hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)"; |
|
900 by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); |
|
901 by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1); |
|
902 by (dres_inst_tac [("c","h")] approx_mult1 2); |
|
903 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
904 simpset() addsimps [hypreal_mult_assoc, hypreal_diff_def])); |
|
905 qed "NSDERIVD3"; |
|
906 |
|
907 (*-------------------------------------------------------------- |
|
908 Now equivalence between NSDERIV and DERIV |
|
909 -------------------------------------------------------------*) |
|
910 Goalw [deriv_def] "(NSDERIV f x :> D) = (DERIV f x :> D)"; |
|
911 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,LIM_NSLIM_iff]) 1); |
|
912 qed "NSDERIV_DERIV_iff"; |
|
913 |
|
914 (*--------------------------------------------------- |
|
915 Differentiability implies continuity |
|
916 nice and simple "algebraic" proof |
|
917 --------------------------------------------------*) |
|
918 Goalw [nsderiv_def] |
|
919 "NSDERIV f x :> D ==> isNSCont f x"; |
|
920 by (auto_tac (claset(),simpset() addsimps |
|
921 [isNSCont_NSLIM_iff,NSLIM_def])); |
|
922 by (dtac (approx_minus_iff RS iffD1) 1); |
|
923 by (dtac (hypreal_not_eq_minus_iff RS iffD1) 1); |
|
924 by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1); |
|
925 by (asm_full_simp_tac (simpset() addsimps |
|
926 [hypreal_add_assoc RS sym]) 2); |
|
927 by (auto_tac (claset(),simpset() addsimps |
|
928 [mem_infmal_iff RS sym,hypreal_add_commute])); |
|
929 by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1); |
|
930 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite |
|
931 RS subsetD],simpset() addsimps [hypreal_mult_assoc])); |
|
932 by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN |
|
933 (2,Infinitesimal_HFinite_mult) RS (mem_infmal_iff RS iffD1)) 1); |
|
934 by (blast_tac (claset() addIs [approx_trans, |
|
935 hypreal_mult_commute RS subst, |
|
936 (approx_minus_iff RS iffD2)]) 1); |
|
937 qed "NSDERIV_isNSCont"; |
|
938 |
|
939 (* Now Sandard proof *) |
|
940 Goal "DERIV f x :> D ==> isCont f x"; |
|
941 by (asm_full_simp_tac (simpset() addsimps |
|
942 [NSDERIV_DERIV_iff RS sym, isNSCont_isCont_iff RS sym, |
|
943 NSDERIV_isNSCont]) 1); |
|
944 qed "DERIV_isCont"; |
|
945 |
|
946 (*---------------------------------------------------------------------------- |
|
947 Differentiation rules for combinations of functions |
|
948 follow from clear, straightforard, algebraic |
|
949 manipulations |
|
950 ----------------------------------------------------------------------------*) |
|
951 (*------------------------- |
|
952 Constant function |
|
953 ------------------------*) |
|
954 |
|
955 (* use simple constant nslimit theorem *) |
|
956 Goal "(NSDERIV (%x. k) x :> 0)"; |
|
957 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); |
|
958 qed "NSDERIV_const"; |
|
959 Addsimps [NSDERIV_const]; |
|
960 |
|
961 Goal "(DERIV (%x. k) x :> 0)"; |
|
962 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1); |
|
963 qed "DERIV_const"; |
|
964 Addsimps [DERIV_const]; |
|
965 |
|
966 (*----------------------------------------------------- |
|
967 Sum of functions- proved easily |
|
968 ----------------------------------------------------*) |
|
969 |
|
970 |
|
971 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
972 \ ==> NSDERIV (%x. f x + g x) x :> Da + Db"; |
|
973 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
974 NSLIM_def]) 1 THEN REPEAT (Step_tac 1)); |
|
975 by (auto_tac (claset(), |
|
976 simpset() addsimps [add_divide_distrib])); |
|
977 by (dres_inst_tac [("b","hypreal_of_real Da"), |
|
978 ("d","hypreal_of_real Db")] approx_add 1); |
|
979 by (auto_tac (claset(), simpset() addsimps add_ac)); |
|
980 qed "NSDERIV_add"; |
|
981 |
|
982 (* Standard theorem *) |
|
983 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
984 \ ==> DERIV (%x. f x + g x) x :> Da + Db"; |
|
985 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_add, |
|
986 NSDERIV_DERIV_iff RS sym]) 1); |
|
987 qed "DERIV_add"; |
|
988 |
|
989 (*----------------------------------------------------- |
|
990 Product of functions - Proof is trivial but tedious |
|
991 and long due to rearrangement of terms |
|
992 ----------------------------------------------------*) |
|
993 |
|
994 Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"; |
|
995 by (simp_tac (simpset() addsimps [right_distrib]) 1); |
|
996 qed "lemma_nsderiv1"; |
|
997 |
|
998 Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \ |
|
999 \ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \ |
|
1000 \ ==> x + y \\<approx> 0"; |
|
1001 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1 |
|
1002 THEN assume_tac 1); |
|
1003 by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1); |
|
1004 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, HFinite_add], |
|
1005 simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym])); |
|
1006 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
|
1007 qed "lemma_nsderiv2"; |
|
1008 |
|
1009 |
|
1010 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1011 \ ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
1012 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1); |
|
1013 by (REPEAT (Step_tac 1)); |
|
1014 by (auto_tac (claset(), |
|
1015 simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1])); |
|
1016 by (simp_tac (simpset() addsimps [add_divide_distrib]) 1); |
|
1017 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); |
|
1018 by (auto_tac (claset(), |
|
1019 simpset() delsimps [times_divide_eq_right] |
|
1020 addsimps [times_divide_eq_right RS sym])); |
|
1021 by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1); |
|
1022 by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4); |
|
1023 by (auto_tac (claset() addSIs [approx_add_mono1], |
|
1024 simpset() addsimps [left_distrib, right_distrib, |
|
1025 hypreal_mult_commute, hypreal_add_assoc])); |
|
1026 by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")] |
|
1027 (hypreal_add_commute RS subst) 1); |
|
1028 by (auto_tac (claset() addSIs [Infinitesimal_add_approx_self2 RS approx_sym, |
|
1029 Infinitesimal_add, Infinitesimal_mult, |
|
1030 Infinitesimal_hypreal_of_real_mult, |
|
1031 Infinitesimal_hypreal_of_real_mult2], |
|
1032 simpset() addsimps [hypreal_add_assoc RS sym])); |
|
1033 qed "NSDERIV_mult"; |
|
1034 |
|
1035 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1036 \ ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
|
1037 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_mult, |
|
1038 NSDERIV_DERIV_iff RS sym]) 1); |
|
1039 qed "DERIV_mult"; |
|
1040 |
|
1041 (*---------------------------- |
|
1042 Multiplying by a constant |
|
1043 ---------------------------*) |
|
1044 Goal "NSDERIV f x :> D \ |
|
1045 \ ==> NSDERIV (%x. c * f x) x :> c*D"; |
|
1046 by (asm_full_simp_tac |
|
1047 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
|
1048 minus_mult_right, right_distrib RS sym]) 1); |
|
1049 by (etac (NSLIM_const RS NSLIM_mult) 1); |
|
1050 qed "NSDERIV_cmult"; |
|
1051 |
|
1052 (* let's do the standard proof though theorem *) |
|
1053 (* LIM_mult2 follows from a NS proof *) |
|
1054 |
|
1055 Goalw [deriv_def] |
|
1056 "DERIV f x :> D \ |
|
1057 \ ==> DERIV (%x. c * f x) x :> c*D"; |
|
1058 by (asm_full_simp_tac |
|
1059 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
|
1060 minus_mult_right, right_distrib RS sym]) 1); |
|
1061 by (etac (LIM_const RS LIM_mult2) 1); |
|
1062 qed "DERIV_cmult"; |
|
1063 |
|
1064 (*-------------------------------- |
|
1065 Negation of function |
|
1066 -------------------------------*) |
|
1067 Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"; |
|
1068 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); |
|
1069 by (dtac NSLIM_minus 1); |
|
1070 by (subgoal_tac "ALL a::real. ALL b. - a + b = - (a + - b)" 1); |
|
1071 by (asm_full_simp_tac (HOL_ss addsimps [thm"minus_divide_left" RS sym]) 1); |
|
1072 by (Asm_full_simp_tac 1); |
|
1073 qed "NSDERIV_minus"; |
|
1074 |
|
1075 Goal "DERIV f x :> D \ |
|
1076 \ ==> DERIV (%x. -(f x)) x :> -D"; |
|
1077 by (asm_full_simp_tac (simpset() addsimps |
|
1078 [NSDERIV_minus,NSDERIV_DERIV_iff RS sym]) 1); |
|
1079 qed "DERIV_minus"; |
|
1080 |
|
1081 (*------------------------------- |
|
1082 Subtraction |
|
1083 ------------------------------*) |
|
1084 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1085 \ ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"; |
|
1086 by (blast_tac (claset() addDs [NSDERIV_add,NSDERIV_minus]) 1); |
|
1087 qed "NSDERIV_add_minus"; |
|
1088 |
|
1089 Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1090 \ ==> DERIV (%x. f x + -g x) x :> Da + -Db"; |
|
1091 by (blast_tac (claset() addDs [DERIV_add,DERIV_minus]) 1); |
|
1092 qed "DERIV_add_minus"; |
|
1093 |
|
1094 Goalw [real_diff_def] |
|
1095 "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
|
1096 \ ==> NSDERIV (%x. f x - g x) x :> Da - Db"; |
|
1097 by (blast_tac (claset() addIs [NSDERIV_add_minus]) 1); |
|
1098 qed "NSDERIV_diff"; |
|
1099 |
|
1100 Goalw [real_diff_def] |
|
1101 "[| DERIV f x :> Da; DERIV g x :> Db |] \ |
|
1102 \ ==> DERIV (%x. f x - g x) x :> Da - Db"; |
|
1103 by (blast_tac (claset() addIs [DERIV_add_minus]) 1); |
|
1104 qed "DERIV_diff"; |
|
1105 |
|
1106 (*--------------------------------------------------------------- |
|
1107 (NS) Increment |
|
1108 ---------------------------------------------------------------*) |
|
1109 Goalw [increment_def] |
|
1110 "f NSdifferentiable x ==> \ |
|
1111 \ increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \ |
|
1112 \ -hypreal_of_real (f x)"; |
|
1113 by (Blast_tac 1); |
|
1114 qed "incrementI"; |
|
1115 |
|
1116 Goal "NSDERIV f x :> D ==> \ |
|
1117 \ increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \ |
|
1118 \ -hypreal_of_real (f x)"; |
|
1119 by (etac (NSdifferentiableI RS incrementI) 1); |
|
1120 qed "incrementI2"; |
|
1121 |
|
1122 (* The Increment theorem -- Keisler p. 65 *) |
|
1123 Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \ |
|
1124 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"; |
|
1125 by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def); |
|
1126 by (dtac bspec 1 THEN Auto_tac); |
|
1127 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1); |
|
1128 by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] |
|
1129 ((hypreal_mult_right_cancel RS iffD2)) 1); |
|
1130 by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \ |
|
1131 \ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2); |
|
1132 by (assume_tac 1); |
|
1133 by (asm_full_simp_tac (simpset() addsimps [times_divide_eq_right RS sym] |
|
1134 delsimps [times_divide_eq_right]) 1); |
|
1135 by (auto_tac (claset(), |
|
1136 simpset() addsimps [left_distrib])); |
|
1137 qed "increment_thm"; |
|
1138 |
|
1139 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
|
1140 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \ |
|
1141 \ hypreal_of_real(D)*h + e*h"; |
|
1142 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2] |
|
1143 addSIs [increment_thm]) 1); |
|
1144 qed "increment_thm2"; |
|
1145 |
|
1146 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
|
1147 \ ==> increment f x h \\<approx> 0"; |
|
1148 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs |
|
1149 [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps |
|
1150 [left_distrib RS sym,mem_infmal_iff RS sym])); |
|
1151 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
|
1152 qed "increment_approx_zero"; |
|
1153 |
|
1154 (*--------------------------------------------------------------- |
|
1155 Similarly to the above, the chain rule admits an entirely |
|
1156 straightforward derivation. Compare this with Harrison's |
|
1157 HOL proof of the chain rule, which proved to be trickier and |
|
1158 required an alternative characterisation of differentiability- |
|
1159 the so-called Carathedory derivative. Our main problem is |
|
1160 manipulation of terms. |
|
1161 --------------------------------------------------------------*) |
|
1162 |
|
1163 (* lemmas *) |
|
1164 Goalw [nsderiv_def] |
|
1165 "[| NSDERIV g x :> D; \ |
|
1166 \ ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ |
|
1167 \ xa \\<in> Infinitesimal;\ |
|
1168 \ xa \\<noteq> 0 \ |
|
1169 \ |] ==> D = 0"; |
|
1170 by (dtac bspec 1); |
|
1171 by Auto_tac; |
|
1172 qed "NSDERIV_zero"; |
|
1173 |
|
1174 (* can be proved differently using NSLIM_isCont_iff *) |
|
1175 Goalw [nsderiv_def] |
|
1176 "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \ |
|
1177 \ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0"; |
|
1178 by (asm_full_simp_tac (simpset() addsimps |
|
1179 [mem_infmal_iff RS sym]) 1); |
|
1180 by (rtac Infinitesimal_ratio 1); |
|
1181 by (rtac approx_hypreal_of_real_HFinite 3); |
|
1182 by Auto_tac; |
|
1183 qed "NSDERIV_approx"; |
|
1184 |
|
1185 (*--------------------------------------------------------------- |
|
1186 from one version of differentiability |
|
1187 |
|
1188 f(x) - f(a) |
|
1189 --------------- \\<approx> Db |
|
1190 x - a |
|
1191 ---------------------------------------------------------------*) |
|
1192 Goal "[| NSDERIV f (g x) :> Da; \ |
|
1193 \ ( *f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \ |
|
1194 \ ( *f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \ |
|
1195 \ |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) \ |
|
1196 \ + - hypreal_of_real (f (g x))) \ |
|
1197 \ / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \ |
|
1198 \ \\<approx> hypreal_of_real(Da)"; |
|
1199 by (auto_tac (claset(), |
|
1200 simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); |
|
1201 qed "NSDERIVD1"; |
|
1202 |
|
1203 (*-------------------------------------------------------------- |
|
1204 from other version of differentiability |
|
1205 |
|
1206 f(x + h) - f(x) |
|
1207 ----------------- \\<approx> Db |
|
1208 h |
|
1209 --------------------------------------------------------------*) |
|
1210 Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> 0 |] \ |
|
1211 \ ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \ |
|
1212 \ \\<approx> hypreal_of_real(Db)"; |
|
1213 by (auto_tac (claset(), |
|
1214 simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, |
|
1215 mem_infmal_iff, starfun_lambda_cancel])); |
|
1216 qed "NSDERIVD2"; |
|
1217 |
|
1218 Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"; |
|
1219 by Auto_tac; |
|
1220 qed "lemma_chain"; |
|
1221 |
|
1222 (*------------------------------------------------------ |
|
1223 This proof uses both definitions of differentiability. |
|
1224 ------------------------------------------------------*) |
|
1225 Goal "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] \ |
|
1226 \ ==> NSDERIV (f o g) x :> Da * Db"; |
|
1227 by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, |
|
1228 NSLIM_def,mem_infmal_iff RS sym]) 1 THEN Step_tac 1); |
|
1229 by (forw_inst_tac [("f","g")] NSDERIV_approx 1); |
|
1230 by (auto_tac (claset(), |
|
1231 simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym])); |
|
1232 by (case_tac "( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1); |
|
1233 by (dres_inst_tac [("g","g")] NSDERIV_zero 1); |
|
1234 by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def])); |
|
1235 by (res_inst_tac [("z1","( *f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"), |
|
1236 ("y1","inverse xa")] (lemma_chain RS ssubst) 1); |
|
1237 by (etac (hypreal_not_eq_minus_iff RS iffD1) 1); |
|
1238 by (rtac approx_mult_hypreal_of_real 1); |
|
1239 by (fold_tac [hypreal_divide_def]); |
|
1240 by (blast_tac (claset() addIs [NSDERIVD1, |
|
1241 approx_minus_iff RS iffD2]) 1); |
|
1242 by (blast_tac (claset() addIs [NSDERIVD2]) 1); |
|
1243 qed "NSDERIV_chain"; |
|
1244 |
|
1245 (* standard version *) |
|
1246 Goal "[| DERIV f (g x) :> Da; \ |
|
1247 \ DERIV g x :> Db \ |
|
1248 \ |] ==> DERIV (f o g) x :> Da * Db"; |
|
1249 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
1250 NSDERIV_chain]) 1); |
|
1251 qed "DERIV_chain"; |
|
1252 |
|
1253 Goal "[| DERIV f (g x) :> Da; DERIV g x :> Db |] \ |
|
1254 \ ==> DERIV (%x. f (g x)) x :> Da * Db"; |
|
1255 by (auto_tac (claset() addDs [DERIV_chain], simpset() addsimps [o_def])); |
|
1256 qed "DERIV_chain2"; |
|
1257 |
|
1258 (*------------------------------------------------------------------ |
|
1259 Differentiation of natural number powers |
|
1260 ------------------------------------------------------------------*) |
|
1261 Goal "NSDERIV (%x. x) x :> 1"; |
|
1262 by (auto_tac (claset(), |
|
1263 simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def ,starfun_Id])); |
|
1264 qed "NSDERIV_Id"; |
|
1265 Addsimps [NSDERIV_Id]; |
|
1266 |
|
1267 (*derivative of the identity function*) |
|
1268 Goal "DERIV (%x. x) x :> 1"; |
|
1269 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1); |
|
1270 qed "DERIV_Id"; |
|
1271 Addsimps [DERIV_Id]; |
|
1272 |
|
1273 bind_thm ("isCont_Id", DERIV_Id RS DERIV_isCont); |
|
1274 |
|
1275 (*derivative of linear multiplication*) |
|
1276 Goal "DERIV (op * c) x :> c"; |
|
1277 by (cut_inst_tac [("c","c"),("x","x")] (DERIV_Id RS DERIV_cmult) 1); |
|
1278 by (Asm_full_simp_tac 1); |
|
1279 qed "DERIV_cmult_Id"; |
|
1280 Addsimps [DERIV_cmult_Id]; |
|
1281 |
|
1282 Goal "NSDERIV (op * c) x :> c"; |
|
1283 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff]) 1); |
|
1284 qed "NSDERIV_cmult_Id"; |
|
1285 Addsimps [NSDERIV_cmult_Id]; |
|
1286 |
|
1287 Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"; |
|
1288 by (induct_tac "n" 1); |
|
1289 by (dtac (DERIV_Id RS DERIV_mult) 2); |
|
1290 by (auto_tac (claset(), |
|
1291 simpset() addsimps [real_of_nat_Suc, left_distrib])); |
|
1292 by (case_tac "0 < n" 1); |
|
1293 by (dres_inst_tac [("x","x")] realpow_minus_mult 1); |
|
1294 by (auto_tac (claset(), |
|
1295 simpset() addsimps [real_mult_assoc, real_add_commute])); |
|
1296 qed "DERIV_pow"; |
|
1297 |
|
1298 (* NS version *) |
|
1299 Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"; |
|
1300 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1); |
|
1301 qed "NSDERIV_pow"; |
|
1302 |
|
1303 (*--------------------------------------------------------------- |
|
1304 Power of -1 |
|
1305 ---------------------------------------------------------------*) |
|
1306 |
|
1307 (*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*) |
|
1308 Goalw [nsderiv_def] |
|
1309 "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"; |
|
1310 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
|
1311 by (ftac Infinitesimal_add_not_zero 1); |
|
1312 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); |
|
1313 by (auto_tac (claset(), |
|
1314 simpset() addsimps [starfun_inverse_inverse, realpow_two] |
|
1315 delsimps [minus_mult_left RS sym, |
|
1316 minus_mult_right RS sym])); |
|
1317 by (asm_full_simp_tac |
|
1318 (simpset() addsimps [hypreal_inverse_add, |
|
1319 hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] |
|
1320 @ add_ac @ mult_ac |
|
1321 delsimps [inverse_mult_distrib,inverse_minus_eq, |
|
1322 minus_mult_left RS sym, |
|
1323 minus_mult_right RS sym] ) 1); |
|
1324 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym, |
|
1325 right_distrib] |
|
1326 delsimps [minus_mult_left RS sym, |
|
1327 minus_mult_right RS sym]) 1); |
|
1328 by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] |
|
1329 approx_trans 1); |
|
1330 by (rtac inverse_add_Infinitesimal_approx2 1); |
|
1331 by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal], |
|
1332 simpset() addsimps [hypreal_minus_inverse RS sym, |
|
1333 HFinite_minus_iff])); |
|
1334 by (rtac Infinitesimal_HFinite_mult2 1); |
|
1335 by Auto_tac; |
|
1336 qed "NSDERIV_inverse"; |
|
1337 |
|
1338 |
|
1339 Goal "x \\<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"; |
|
1340 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse, |
|
1341 NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1); |
|
1342 qed "DERIV_inverse"; |
|
1343 |
|
1344 (*-------------------------------------------------------------- |
|
1345 Derivative of inverse |
|
1346 -------------------------------------------------------------*) |
|
1347 Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \ |
|
1348 \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; |
|
1349 by (rtac (real_mult_commute RS subst) 1); |
|
1350 by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1); |
|
1351 by (fold_goals_tac [o_def]); |
|
1352 by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1); |
|
1353 qed "DERIV_inverse_fun"; |
|
1354 |
|
1355 Goal "[| NSDERIV f x :> d; f(x) \\<noteq> 0 |] \ |
|
1356 \ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; |
|
1357 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
|
1358 DERIV_inverse_fun] delsimps [realpow_Suc]) 1); |
|
1359 qed "NSDERIV_inverse_fun"; |
|
1360 |
|
1361 (*-------------------------------------------------------------- |
|
1362 Derivative of quotient |
|
1363 -------------------------------------------------------------*) |
|
1364 Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \ |
|
1365 \ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"; |
|
1366 by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1); |
|
1367 by (dtac DERIV_mult 2); |
|
1368 by (REPEAT(assume_tac 1)); |
|
1369 by (asm_full_simp_tac |
|
1370 (simpset() addsimps [real_divide_def, right_distrib, |
|
1371 power_inverse,minus_mult_left] @ mult_ac |
|
1372 delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); |
|
1373 qed "DERIV_quotient"; |
|
1374 |
|
1375 Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \ |
|
1376 \ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \ |
|
1377 \ + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"; |
|
1378 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
|
1379 DERIV_quotient] delsimps [realpow_Suc]) 1); |
|
1380 qed "NSDERIV_quotient"; |
|
1381 |
|
1382 (* ------------------------------------------------------------------------ *) |
|
1383 (* Caratheodory formulation of derivative at a point: standard proof *) |
|
1384 (* ------------------------------------------------------------------------ *) |
|
1385 |
|
1386 Goal "(DERIV f x :> l) = \ |
|
1387 \ (\\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isCont g x & g x = l)"; |
|
1388 by Safe_tac; |
|
1389 by (res_inst_tac |
|
1390 [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1); |
|
1391 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc, |
|
1392 ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (0::real)"])); |
|
1393 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff])); |
|
1394 by (ALLGOALS(rtac (LIM_equal RS iffD1))); |
|
1395 by (auto_tac (claset(),simpset() addsimps [real_diff_def,real_mult_assoc])); |
|
1396 qed "CARAT_DERIV"; |
|
1397 |
|
1398 Goal "NSDERIV f x :> l ==> \ |
|
1399 \ \\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l"; |
|
1400 by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff, |
|
1401 isNSCont_isCont_iff,CARAT_DERIV])); |
|
1402 qed "CARAT_NSDERIV"; |
|
1403 |
|
1404 (* How about a NS proof? *) |
|
1405 Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \ |
|
1406 \ ==> NSDERIV f x :> l"; |
|
1407 by (auto_tac (claset(), |
|
1408 simpset() delsimprocs field_cancel_factor |
|
1409 addsimps [NSDERIV_iff2])); |
|
1410 by (auto_tac (claset(), |
|
1411 simpset() addsimps [hypreal_mult_assoc])); |
|
1412 by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym, |
|
1413 hypreal_diff_def]) 1); |
|
1414 by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1); |
|
1415 qed "CARAT_DERIVD"; |
|
1416 |
|
1417 |
|
1418 |
|
1419 (*--------------------------------------------------------------------------*) |
|
1420 (* Lemmas about nested intervals and proof by bisection (cf.Harrison) *) |
|
1421 (* All considerably tidied by lcp *) |
|
1422 (*--------------------------------------------------------------------------*) |
|
1423 |
|
1424 Goal "(\\<forall>n. (f::nat=>real) n \\<le> f (Suc n)) --> f m \\<le> f(m + no)"; |
|
1425 by (induct_tac "no" 1); |
|
1426 by (auto_tac (claset() addIs [order_trans], simpset())); |
|
1427 qed_spec_mp "lemma_f_mono_add"; |
|
1428 |
|
1429 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
|
1430 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
|
1431 \ \\<forall>n. f(n) \\<le> g(n) |] \ |
|
1432 \ ==> Bseq f"; |
|
1433 by (res_inst_tac [("k","f 0"),("K","g 0")] BseqI2 1 THEN rtac allI 1); |
|
1434 by (induct_tac "n" 1); |
|
1435 by (auto_tac (claset() addIs [order_trans], simpset())); |
|
1436 by (res_inst_tac [("y","g(Suc na)")] order_trans 1); |
|
1437 by (induct_tac "na" 2); |
|
1438 by (auto_tac (claset() addIs [order_trans], simpset())); |
|
1439 qed "f_inc_g_dec_Beq_f"; |
|
1440 |
|
1441 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
|
1442 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
|
1443 \ \\<forall>n. f(n) \\<le> g(n) |] \ |
|
1444 \ ==> Bseq g"; |
|
1445 by (stac (Bseq_minus_iff RS sym) 1); |
|
1446 by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1); |
|
1447 by Auto_tac; |
|
1448 qed "f_inc_g_dec_Beq_g"; |
|
1449 |
|
1450 Goal "[| \\<forall>n. f n \\<le> f (Suc n); convergent f |] ==> f n \\<le> lim f"; |
|
1451 by (rtac (linorder_not_less RS iffD1) 1); |
|
1452 by (auto_tac (claset(), |
|
1453 simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc])); |
|
1454 by (dtac real_less_sum_gt_zero 1); |
|
1455 by (dres_inst_tac [("x","f n + - lim f")] spec 1); |
|
1456 by Safe_tac; |
|
1457 by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 1); |
|
1458 by Auto_tac; |
|
1459 by (subgoal_tac "lim f \\<le> f(no + n)" 1); |
|
1460 by (induct_tac "no" 2); |
|
1461 by (auto_tac (claset() addIs [order_trans], |
|
1462 simpset() addsimps [real_diff_def, real_abs_def])); |
|
1463 by (dres_inst_tac [("x","f(no + n)"),("no1","no")] |
|
1464 (lemma_f_mono_add RSN (2,order_less_le_trans)) 1); |
|
1465 by (auto_tac (claset(), simpset() addsimps [add_commute])); |
|
1466 qed "f_inc_imp_le_lim"; |
|
1467 |
|
1468 Goal "convergent g ==> lim (%x. - g x) = - (lim g)"; |
|
1469 by (rtac (LIMSEQ_minus RS limI) 1); |
|
1470 by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1); |
|
1471 qed "lim_uminus"; |
|
1472 |
|
1473 Goal "[| \\<forall>n. g(Suc n) \\<le> g(n); convergent g |] ==> lim g \\<le> g n"; |
|
1474 by (subgoal_tac "- (g n) \\<le> - (lim g)" 1); |
|
1475 by (cut_inst_tac [("f", "%x. - (g x)")] f_inc_imp_le_lim 2); |
|
1476 by (auto_tac (claset(), |
|
1477 simpset() addsimps [lim_uminus, convergent_minus_iff RS sym])); |
|
1478 qed "g_dec_imp_lim_le"; |
|
1479 |
|
1480 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
|
1481 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
|
1482 \ \\<forall>n. f(n) \\<le> g(n) |] \ |
|
1483 \ ==> \\<exists>l m. l \\<le> m & ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \ |
|
1484 \ ((\\<forall>n. m \\<le> g(n)) & g ----> m)"; |
|
1485 by (subgoal_tac "monoseq f & monoseq g" 1); |
|
1486 by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2); |
|
1487 by (subgoal_tac "Bseq f & Bseq g" 1); |
|
1488 by (blast_tac (claset() addIs [f_inc_g_dec_Beq_f, f_inc_g_dec_Beq_g]) 2); |
|
1489 by (auto_tac (claset() addSDs [Bseq_monoseq_convergent], |
|
1490 simpset() addsimps [convergent_LIMSEQ_iff])); |
|
1491 by (res_inst_tac [("x","lim f")] exI 1); |
|
1492 by (res_inst_tac [("x","lim g")] exI 1); |
|
1493 by (auto_tac (claset() addIs [LIMSEQ_le], simpset())); |
|
1494 by (auto_tac (claset(), |
|
1495 simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le, |
|
1496 convergent_LIMSEQ_iff])); |
|
1497 qed "lemma_nest"; |
|
1498 |
|
1499 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
|
1500 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
|
1501 \ \\<forall>n. f(n) \\<le> g(n); \ |
|
1502 \ (%n. f(n) - g(n)) ----> 0 |] \ |
|
1503 \ ==> \\<exists>l. ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \ |
|
1504 \ ((\\<forall>n. l \\<le> g(n)) & g ----> l)"; |
|
1505 by (dtac lemma_nest 1 THEN Auto_tac); |
|
1506 by (subgoal_tac "l = m" 1); |
|
1507 by (dres_inst_tac [("X","f")] LIMSEQ_diff 2); |
|
1508 by (auto_tac (claset() addIs [LIMSEQ_unique], simpset())); |
|
1509 qed "lemma_nest_unique"; |
|
1510 |
|
1511 |
|
1512 Goal "a \\<le> b ==> \ |
|
1513 \ \\<forall>n. fst (Bolzano_bisect P a b n) \\<le> snd (Bolzano_bisect P a b n)"; |
|
1514 by (rtac allI 1); |
|
1515 by (induct_tac "n" 1); |
|
1516 by (auto_tac (claset(), simpset() addsimps [Let_def, split_def])); |
|
1517 qed "Bolzano_bisect_le"; |
|
1518 |
|
1519 Goal "a \\<le> b ==> \ |
|
1520 \ \\<forall>n. fst(Bolzano_bisect P a b n) \\<le> fst (Bolzano_bisect P a b (Suc n))"; |
|
1521 by (rtac allI 1); |
|
1522 by (induct_tac "n" 1); |
|
1523 by (auto_tac (claset(), |
|
1524 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
|
1525 qed "Bolzano_bisect_fst_le_Suc"; |
|
1526 |
|
1527 Goal "a \\<le> b ==> \ |
|
1528 \ \\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \\<le> snd (Bolzano_bisect P a b n)"; |
|
1529 by (rtac allI 1); |
|
1530 by (induct_tac "n" 1); |
|
1531 by (auto_tac (claset(), |
|
1532 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
|
1533 qed "Bolzano_bisect_Suc_le_snd"; |
|
1534 |
|
1535 Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)"; |
|
1536 by Auto_tac; |
|
1537 by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1); |
|
1538 by Auto_tac; |
|
1539 qed "eq_divide_2_times_iff"; |
|
1540 |
|
1541 Goal "a \\<le> b ==> \ |
|
1542 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \ |
|
1543 \ (b-a) / (2 ^ n)"; |
|
1544 by (induct_tac "n" 1); |
|
1545 by (auto_tac (claset(), |
|
1546 simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib, |
|
1547 Let_def, split_def])); |
|
1548 by (auto_tac (claset(), |
|
1549 simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def]))); |
|
1550 qed "Bolzano_bisect_diff"; |
|
1551 |
|
1552 val Bolzano_nest_unique = |
|
1553 [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le] |
|
1554 MRS lemma_nest_unique; |
|
1555 |
|
1556 (*P_prem is a looping simprule, so it works better if it isn't an assumption*) |
|
1557 val P_prem::notP_prem::rest = |
|
1558 Goal "[| !!a b c. [| P(a,b); P(b,c); a \\<le> b; b \\<le> c|] ==> P(a,c); \ |
|
1559 \ ~ P(a,b); a \\<le> b |] ==> \ |
|
1560 \ ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"; |
|
1561 by (cut_facts_tac rest 1); |
|
1562 by (induct_tac "n" 1); |
|
1563 by (auto_tac (claset(), |
|
1564 simpset() delsimps [surjective_pairing RS sym] |
|
1565 addsimps [notP_prem, Let_def, split_def])); |
|
1566 by (swap_res_tac [P_prem] 1); |
|
1567 by (assume_tac 1); |
|
1568 by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le])); |
|
1569 qed "not_P_Bolzano_bisect"; |
|
1570 |
|
1571 (*Now we re-package P_prem as a formula*) |
|
1572 Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \ |
|
1573 \ ~ P(a,b); a \\<le> b |] ==> \ |
|
1574 \ \\<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"; |
|
1575 by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1); |
|
1576 qed "not_P_Bolzano_bisect'"; |
|
1577 |
|
1578 |
|
1579 Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \ |
|
1580 \ \\<forall>x. \\<exists>d::real. 0 < d & \ |
|
1581 \ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)); \ |
|
1582 \ a \\<le> b |] \ |
|
1583 \ ==> P(a,b)"; |
|
1584 by (rtac (inst "P1" "P" Bolzano_nest_unique RS exE) 1); |
|
1585 by (REPEAT (assume_tac 1)); |
|
1586 by (rtac LIMSEQ_minus_cancel 1); |
|
1587 by (asm_simp_tac (simpset() addsimps [Bolzano_bisect_diff, |
|
1588 LIMSEQ_divide_realpow_zero]) 1); |
|
1589 by (rtac ccontr 1); |
|
1590 by (dtac not_P_Bolzano_bisect' 1); |
|
1591 by (REPEAT (assume_tac 1)); |
|
1592 by (rename_tac "l" 1); |
|
1593 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1); |
|
1594 by (rewtac LIMSEQ_def); |
|
1595 by (dres_inst_tac [("P", "%r. 0<r --> ?Q r"), ("x","d/2")] spec 1); |
|
1596 by (dres_inst_tac [("P", "%r. 0<r --> ?Q r"), ("x","d/2")] spec 1); |
|
1597 by (dtac real_less_half_sum 1); |
|
1598 by Safe_tac; |
|
1599 (*linear arithmetic bug if we just use Asm_simp_tac*) |
|
1600 by (ALLGOALS Asm_full_simp_tac); |
|
1601 by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1); |
|
1602 by (dres_inst_tac [("x","snd(Bolzano_bisect P a b (no + noa))")] spec 1); |
|
1603 by Safe_tac; |
|
1604 by (ALLGOALS Asm_simp_tac); |
|
1605 by (res_inst_tac [("y","abs(fst(Bolzano_bisect P a b(no + noa)) - l) + \ |
|
1606 \ abs(snd(Bolzano_bisect P a b(no + noa)) - l)")] |
|
1607 order_le_less_trans 1); |
|
1608 by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1); |
|
1609 by (rtac (real_sum_of_halves RS subst) 1); |
|
1610 by (rtac add_strict_mono 1); |
|
1611 by (ALLGOALS |
|
1612 (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def]))); |
|
1613 qed "lemma_BOLZANO"; |
|
1614 |
|
1615 |
|
1616 Goal "((\\<forall>a b c. (a \\<le> b & b \\<le> c & P(a,b) & P(b,c)) --> P(a,c)) & \ |
|
1617 \ (\\<forall>x. \\<exists>d::real. 0 < d & \ |
|
1618 \ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \ |
|
1619 \ --> (\\<forall>a b. a \\<le> b --> P(a,b))"; |
|
1620 by (Clarify_tac 1); |
|
1621 by (blast_tac (claset() addIs [lemma_BOLZANO]) 1); |
|
1622 qed "lemma_BOLZANO2"; |
|
1623 |
|
1624 |
|
1625 (*----------------------------------------------------------------------------*) |
|
1626 (* Intermediate Value Theorem (prove contrapositive by bisection) *) |
|
1627 (*----------------------------------------------------------------------------*) |
|
1628 |
|
1629 Goal "[| f(a) \\<le> y & y \\<le> f(b); \ |
|
1630 \ a \\<le> b; \ |
|
1631 \ (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x) |] \ |
|
1632 \ ==> \\<exists>x. a \\<le> x & x \\<le> b & f(x) = y"; |
|
1633 by (rtac contrapos_pp 1); |
|
1634 by (assume_tac 1); |
|
1635 by (cut_inst_tac |
|
1636 [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> ~(f(u) \\<le> y & y \\<le> f(v))")] |
|
1637 lemma_BOLZANO2 1); |
|
1638 by Safe_tac; |
|
1639 by (ALLGOALS(Asm_full_simp_tac)); |
|
1640 by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1); |
|
1641 by (rtac ccontr 1); |
|
1642 by (subgoal_tac "a \\<le> x & x \\<le> b" 1); |
|
1643 by (Asm_full_simp_tac 2); |
|
1644 by (dres_inst_tac [("P", "%d. 0<d --> ?P d"),("x","1")] spec 2); |
|
1645 by (Step_tac 2); |
|
1646 by (Asm_full_simp_tac 2); |
|
1647 by (Asm_full_simp_tac 2); |
|
1648 by (REPEAT(blast_tac (claset() addIs [order_trans]) 2)); |
|
1649 by (REPEAT(dres_inst_tac [("x","x")] spec 1)); |
|
1650 by (Asm_full_simp_tac 1); |
|
1651 by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. 0<s & ?Q r s)"), |
|
1652 ("x","abs(y - f x)")] spec 1); |
|
1653 by Safe_tac; |
|
1654 by (asm_full_simp_tac (simpset() addsimps []) 1); |
|
1655 by (dres_inst_tac [("x","s")] spec 1); |
|
1656 by (Clarify_tac 1); |
|
1657 by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1); |
|
1658 by Safe_tac; |
|
1659 by (dres_inst_tac [("x","ba - x")] spec 1); |
|
1660 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [thm"abs_if"]))); |
|
1661 by (dres_inst_tac [("x","aa - x")] spec 1); |
|
1662 by (case_tac "x \\<le> aa" 1); |
|
1663 by (ALLGOALS Asm_full_simp_tac); |
|
1664 by (dres_inst_tac [("z","x"),("w","aa")] real_le_anti_sym 1); |
|
1665 by (assume_tac 1 THEN Asm_full_simp_tac 1); |
|
1666 qed "IVT"; |
|
1667 |
|
1668 |
|
1669 Goal "[| f(b) \\<le> y & y \\<le> f(a); \ |
|
1670 \ a \\<le> b; \ |
|
1671 \ (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x) \ |
|
1672 \ |] ==> \\<exists>x. a \\<le> x & x \\<le> b & f(x) = y"; |
|
1673 by (subgoal_tac "- f a \\<le> -y & -y \\<le> - f b" 1); |
|
1674 by (thin_tac "f b \\<le> y & y \\<le> f a" 1); |
|
1675 by (dres_inst_tac [("f","%x. - f x")] IVT 1); |
|
1676 by (auto_tac (claset() addIs [isCont_minus],simpset())); |
|
1677 qed "IVT2"; |
|
1678 |
|
1679 |
|
1680 (*HOL style here: object-level formulations*) |
|
1681 Goal "(f(a) \\<le> y & y \\<le> f(b) & a \\<le> b & \ |
|
1682 \ (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x)) \ |
|
1683 \ --> (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = y)"; |
|
1684 by (blast_tac (claset() addIs [IVT]) 1); |
|
1685 qed "IVT_objl"; |
|
1686 |
|
1687 Goal "(f(b) \\<le> y & y \\<le> f(a) & a \\<le> b & \ |
|
1688 \ (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x)) \ |
|
1689 \ --> (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = y)"; |
|
1690 by (blast_tac (claset() addIs [IVT2]) 1); |
|
1691 qed "IVT2_objl"; |
|
1692 |
|
1693 (*---------------------------------------------------------------------------*) |
|
1694 (* By bisection, function continuous on closed interval is bounded above *) |
|
1695 (*---------------------------------------------------------------------------*) |
|
1696 |
|
1697 Goal "abs (real x) = real (x::nat)"; |
|
1698 by (auto_tac (claset() addIs [abs_eqI1], simpset())); |
|
1699 qed "abs_real_of_nat_cancel"; |
|
1700 Addsimps [abs_real_of_nat_cancel]; |
|
1701 |
|
1702 Goal "~ abs(x) + (1::real) < x"; |
|
1703 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
|
1704 by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset())); |
|
1705 qed "abs_add_one_not_less_self"; |
|
1706 Addsimps [abs_add_one_not_less_self]; |
|
1707 |
|
1708 |
|
1709 Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |]\ |
|
1710 \ ==> \\<exists>M. \\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M"; |
|
1711 by (cut_inst_tac [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> \ |
|
1712 \ (\\<exists>M. \\<forall>x. u \\<le> x & x \\<le> v --> f x \\<le> M)")] |
|
1713 lemma_BOLZANO2 1); |
|
1714 by Safe_tac; |
|
1715 by (ALLGOALS Asm_full_simp_tac); |
|
1716 by (rename_tac "x xa ya M Ma" 1); |
|
1717 by (cut_inst_tac [("x","M"),("y","Ma")] linorder_linear 1); |
|
1718 by Safe_tac; |
|
1719 by (res_inst_tac [("x","Ma")] exI 1); |
|
1720 by (Clarify_tac 1); |
|
1721 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
|
1722 by (Force_tac 1); |
|
1723 by (res_inst_tac [("x","M")] exI 1); |
|
1724 by (Clarify_tac 1); |
|
1725 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
|
1726 by (Force_tac 1); |
|
1727 by (case_tac "a \\<le> x & x \\<le> b" 1); |
|
1728 by (res_inst_tac [("x","1")] exI 2); |
|
1729 by (Force_tac 2); |
|
1730 by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1); |
|
1731 by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac); |
|
1732 by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1); |
|
1733 by (dres_inst_tac [("x","1")] spec 1); |
|
1734 by Auto_tac; |
|
1735 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1); |
|
1736 by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1); |
|
1737 by (dres_inst_tac [("x","xa - x")] spec 1); |
|
1738 by (auto_tac (claset(), simpset() addsimps [abs_ge_self])); |
|
1739 by (REPEAT (arith_tac 1)); |
|
1740 qed "isCont_bounded"; |
|
1741 |
|
1742 (*----------------------------------------------------------------------------*) |
|
1743 (* Refine the above to existence of least upper bound *) |
|
1744 (*----------------------------------------------------------------------------*) |
|
1745 |
|
1746 Goal "((\\<exists>x. x \\<in> S) & (\\<exists>y. isUb UNIV S (y::real))) --> \ |
|
1747 \ (\\<exists>t. isLub UNIV S t)"; |
|
1748 by (blast_tac (claset() addIs [reals_complete]) 1); |
|
1749 qed "lemma_reals_complete"; |
|
1750 |
|
1751 Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \ |
|
1752 \ ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M) & \ |
|
1753 \ (\\<forall>N. N < M --> (\\<exists>x. a \\<le> x & x \\<le> b & N < f(x)))"; |
|
1754 by (cut_inst_tac [("S","Collect (%y. \\<exists>x. a \\<le> x & x \\<le> b & y = f x)")] |
|
1755 lemma_reals_complete 1); |
|
1756 by Auto_tac; |
|
1757 by (dtac isCont_bounded 1 THEN assume_tac 1); |
|
1758 by (auto_tac (claset(),simpset() addsimps [isUb_def,leastP_def, |
|
1759 isLub_def,setge_def,setle_def])); |
|
1760 by (rtac exI 1 THEN Auto_tac); |
|
1761 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
1762 by (dres_inst_tac [("x","x")] spec 1); |
|
1763 by (auto_tac (claset() addSIs [(linorder_not_less RS iffD1)],simpset())); |
|
1764 qed "isCont_has_Ub"; |
|
1765 |
|
1766 (*----------------------------------------------------------------------------*) |
|
1767 (* Now show that it attains its upper bound *) |
|
1768 (*----------------------------------------------------------------------------*) |
|
1769 |
|
1770 Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \ |
|
1771 \ ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M) & \ |
|
1772 \ (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = M)"; |
|
1773 by (ftac isCont_has_Ub 1 THEN assume_tac 1); |
|
1774 by (Clarify_tac 1); |
|
1775 by (res_inst_tac [("x","M")] exI 1); |
|
1776 by (Asm_full_simp_tac 1); |
|
1777 by (rtac ccontr 1); |
|
1778 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> f x < M" 1 THEN Step_tac 1); |
|
1779 by (rtac ccontr 2 THEN dtac (linorder_not_less RS iffD1) 2); |
|
1780 by (dres_inst_tac [("z","M")] real_le_anti_sym 2); |
|
1781 by (REPEAT(Blast_tac 2)); |
|
1782 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. inverse(M - f x)) x" 1); |
|
1783 by Safe_tac; |
|
1784 by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]); |
|
1785 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [diff_eq_eq]))); |
|
1786 by (Blast_tac 2); |
|
1787 by (subgoal_tac |
|
1788 "\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1); |
|
1789 by (rtac isCont_bounded 2); |
|
1790 by Safe_tac; |
|
1791 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> 0 < inverse(M - f(x))" 1); |
|
1792 by (Asm_full_simp_tac 1); |
|
1793 by Safe_tac; |
|
1794 by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2); |
|
1795 by (subgoal_tac |
|
1796 "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1); |
|
1797 by Safe_tac; |
|
1798 by (res_inst_tac [("y","k")] order_le_less_trans 2); |
|
1799 by (asm_full_simp_tac (simpset() addsimps [zero_less_one]) 3); |
|
1800 by (Asm_full_simp_tac 2); |
|
1801 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \ |
|
1802 \ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1); |
|
1803 by Safe_tac; |
|
1804 by (rtac less_imp_inverse_less 2); |
|
1805 by (ALLGOALS Asm_full_simp_tac); |
|
1806 by (dres_inst_tac [("P", "%N. N<M --> ?Q N"), |
|
1807 ("x","M - inverse(k + 1)")] spec 1); |
|
1808 by (Step_tac 1 THEN dtac (linorder_not_less RS iffD1) 1); |
|
1809 by (dtac (le_diff_eq RS iffD1) 1); |
|
1810 by (REPEAT(dres_inst_tac [("x","a")] spec 1)); |
|
1811 by (Asm_full_simp_tac 1); |
|
1812 by (asm_full_simp_tac |
|
1813 (simpset() addsimps [inverse_eq_divide, pos_divide_le_eq]) 1); |
|
1814 by (cut_inst_tac [("a","k"),("b","M-f a")] zero_less_mult_iff 1); |
|
1815 by (Asm_full_simp_tac 1); |
|
1816 (*last one*) |
|
1817 by (REPEAT(dres_inst_tac [("x","x")] spec 1)); |
|
1818 by (Asm_full_simp_tac 1); |
|
1819 qed "isCont_eq_Ub"; |
|
1820 |
|
1821 |
|
1822 (*----------------------------------------------------------------------------*) |
|
1823 (* Same theorem for lower bound *) |
|
1824 (*----------------------------------------------------------------------------*) |
|
1825 |
|
1826 Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \ |
|
1827 \ ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> M \\<le> f(x)) & \ |
|
1828 \ (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = M)"; |
|
1829 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. -(f x)) x" 1); |
|
1830 by (blast_tac (claset() addIs [isCont_minus]) 2); |
|
1831 by (dres_inst_tac [("f","(%x. -(f x))")] isCont_eq_Ub 1); |
|
1832 by Safe_tac; |
|
1833 by Auto_tac; |
|
1834 qed "isCont_eq_Lb"; |
|
1835 |
|
1836 |
|
1837 (* ------------------------------------------------------------------------- *) |
|
1838 (* Another version. *) |
|
1839 (* ------------------------------------------------------------------------- *) |
|
1840 |
|
1841 Goal "[|a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \ |
|
1842 \ ==> \\<exists>L M. (\\<forall>x. a \\<le> x & x \\<le> b --> L \\<le> f(x) & f(x) \\<le> M) & \ |
|
1843 \ (\\<forall>y. L \\<le> y & y \\<le> M --> (\\<exists>x. a \\<le> x & x \\<le> b & (f(x) = y)))"; |
|
1844 by (ftac isCont_eq_Lb 1); |
|
1845 by (ftac isCont_eq_Ub 2); |
|
1846 by (REPEAT(assume_tac 1)); |
|
1847 by Safe_tac; |
|
1848 by (res_inst_tac [("x","f x")] exI 1); |
|
1849 by (res_inst_tac [("x","f xa")] exI 1); |
|
1850 by (Asm_full_simp_tac 1); |
|
1851 by Safe_tac; |
|
1852 by (cut_inst_tac [("x","x"),("y","xa")] linorder_linear 1); |
|
1853 by Safe_tac; |
|
1854 by (cut_inst_tac [("f","f"),("a","x"),("b","xa"),("y","y")] IVT_objl 1); |
|
1855 by (cut_inst_tac [("f","f"),("a","xa"),("b","x"),("y","y")] IVT2_objl 2); |
|
1856 by Safe_tac; |
|
1857 by (res_inst_tac [("x","xb")] exI 2); |
|
1858 by (res_inst_tac [("x","xb")] exI 4); |
|
1859 by (ALLGOALS(Asm_full_simp_tac)); |
|
1860 qed "isCont_Lb_Ub"; |
|
1861 |
|
1862 (*----------------------------------------------------------------------------*) |
|
1863 (* If f'(x) > 0 then x is locally strictly increasing at the right *) |
|
1864 (*----------------------------------------------------------------------------*) |
|
1865 |
|
1866 Goalw [deriv_def,LIM_def] |
|
1867 "[| DERIV f x :> l; 0 < l |] \ |
|
1868 \ ==> \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"; |
|
1869 by (dtac spec 1 THEN Auto_tac); |
|
1870 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
|
1871 by (subgoal_tac "0 < l*h" 1); |
|
1872 by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2); |
|
1873 by (dres_inst_tac [("x","h")] spec 1); |
|
1874 by (asm_full_simp_tac |
|
1875 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
|
1876 pos_le_divide_eq, pos_less_divide_eq] |
|
1877 addsplits [split_if_asm]) 1); |
|
1878 qed "DERIV_left_inc"; |
|
1879 |
|
1880 val prems = goalw (the_context()) [deriv_def,LIM_def] |
|
1881 "[| DERIV f x :> l; l < 0 |] ==> \ |
|
1882 \ \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x - h))"; |
|
1883 by (cut_facts_tac prems 1); (*needed because arith removes the assumption l<0*) |
|
1884 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); |
|
1885 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
|
1886 by (dres_inst_tac [("x","-h")] spec 1); |
|
1887 by (asm_full_simp_tac |
|
1888 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
|
1889 pos_less_divide_eq, |
|
1890 symmetric real_diff_def] |
|
1891 addsplits [split_if_asm]) 1); |
|
1892 by (subgoal_tac "0 < (f (x - h) - f x)/h" 1); |
|
1893 by (asm_full_simp_tac (simpset() addsimps [pos_less_divide_eq]) 1); |
|
1894 by (cut_facts_tac prems 1); |
|
1895 by (arith_tac 1); |
|
1896 qed "DERIV_left_dec"; |
|
1897 |
|
1898 (*????previous proof, revealing arith problem: |
|
1899 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); |
|
1900 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
|
1901 by (subgoal_tac "l*h < 0" 1); |
|
1902 by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2); |
|
1903 by (dres_inst_tac [("x","-h")] spec 1); |
|
1904 by (asm_full_simp_tac |
|
1905 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
|
1906 pos_less_divide_eq, |
|
1907 symmetric real_diff_def] |
|
1908 addsplits [split_if_asm] |
|
1909 delsimprocs [fast_real_arith_simproc]) 1); |
|
1910 by (subgoal_tac "0 < (f (x - h) - f x)/h" 1); |
|
1911 by (arith_tac 2); |
|
1912 by (asm_full_simp_tac |
|
1913 (simpset() addsimps [pos_less_divide_eq]) 1); |
|
1914 qed "DERIV_left_dec"; |
|
1915 *) |
|
1916 |
|
1917 |
|
1918 Goal "[| DERIV f x :> l; \ |
|
1919 \ \\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \ |
|
1920 \ ==> l = 0"; |
|
1921 by (res_inst_tac [("x","l"),("y","0")] linorder_cases 1); |
|
1922 by Safe_tac; |
|
1923 by (dtac DERIV_left_dec 1); |
|
1924 by (dtac DERIV_left_inc 3); |
|
1925 by Safe_tac; |
|
1926 by (dres_inst_tac [("d1.0","d"),("d2.0","da")] real_lbound_gt_zero 1); |
|
1927 by (dres_inst_tac [("d1.0","d"),("d2.0","da")] real_lbound_gt_zero 3); |
|
1928 by Safe_tac; |
|
1929 by (dres_inst_tac [("x","x - e")] spec 1); |
|
1930 by (dres_inst_tac [("x","x + e")] spec 2); |
|
1931 by (auto_tac (claset(), simpset() addsimps [real_abs_def])); |
|
1932 qed "DERIV_local_max"; |
|
1933 |
|
1934 (*----------------------------------------------------------------------------*) |
|
1935 (* Similar theorem for a local minimum *) |
|
1936 (*----------------------------------------------------------------------------*) |
|
1937 |
|
1938 Goal "[| DERIV f x :> l; \ |
|
1939 \ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \ |
|
1940 \ ==> l = 0"; |
|
1941 by (dtac (DERIV_minus RS DERIV_local_max) 1); |
|
1942 by Auto_tac; |
|
1943 qed "DERIV_local_min"; |
|
1944 |
|
1945 (*----------------------------------------------------------------------------*) |
|
1946 (* In particular if a function is locally flat *) |
|
1947 (*----------------------------------------------------------------------------*) |
|
1948 |
|
1949 Goal "[| DERIV f x :> l; \ |
|
1950 \ \\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \ |
|
1951 \ ==> l = 0"; |
|
1952 by (auto_tac (claset() addSDs [DERIV_local_max],simpset())); |
|
1953 qed "DERIV_local_const"; |
|
1954 |
|
1955 (*----------------------------------------------------------------------------*) |
|
1956 (* Lemma about introducing open ball in open interval *) |
|
1957 (*----------------------------------------------------------------------------*) |
|
1958 |
|
1959 Goal "[| a < x; x < b |] ==> \ |
|
1960 \ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> a < y & y < b)"; |
|
1961 by (simp_tac (simpset() addsimps [abs_interval_iff]) 1); |
|
1962 by (cut_inst_tac [("x","x - a"),("y","b - x")] linorder_linear 1); |
|
1963 by Safe_tac; |
|
1964 by (res_inst_tac [("x","x - a")] exI 1); |
|
1965 by (res_inst_tac [("x","b - x")] exI 2); |
|
1966 by Auto_tac; |
|
1967 by (auto_tac (claset(),simpset() addsimps [less_diff_eq])); |
|
1968 qed "lemma_interval_lt"; |
|
1969 |
|
1970 Goal "[| a < x; x < b |] ==> \ |
|
1971 \ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)"; |
|
1972 by (dtac lemma_interval_lt 1); |
|
1973 by Auto_tac; |
|
1974 by (auto_tac (claset() addSIs [exI] ,simpset())); |
|
1975 qed "lemma_interval"; |
|
1976 |
|
1977 (*----------------------------------------------------------------------- |
|
1978 Rolle's Theorem |
|
1979 If f is defined and continuous on the finite closed interval [a,b] |
|
1980 and differentiable a least on the open interval (a,b), and f(a) = f(b), |
|
1981 then x0 \\<in> (a,b) such that f'(x0) = 0 |
|
1982 ----------------------------------------------------------------------*) |
|
1983 |
|
1984 Goal "[| a < b; f(a) = f(b); \ |
|
1985 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \ |
|
1986 \ \\<forall>x. a < x & x < b --> f differentiable x \ |
|
1987 \ |] ==> \\<exists>z. a < z & z < b & DERIV f z :> 0"; |
|
1988 by (ftac (order_less_imp_le RS isCont_eq_Ub) 1); |
|
1989 by (EVERY1[assume_tac,Step_tac]); |
|
1990 by (ftac (order_less_imp_le RS isCont_eq_Lb) 1); |
|
1991 by (EVERY1[assume_tac,Step_tac]); |
|
1992 by (case_tac "a < x & x < b" 1 THEN etac conjE 1); |
|
1993 by (Asm_full_simp_tac 2); |
|
1994 by (forw_inst_tac [("a","a"),("x","x")] lemma_interval 1); |
|
1995 by (EVERY1[assume_tac,etac exE]); |
|
1996 by (res_inst_tac [("x","x")] exI 1 THEN Asm_full_simp_tac 1); |
|
1997 by (subgoal_tac "(\\<exists>l. DERIV f x :> l) & \ |
|
1998 \ (\\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1); |
|
1999 by (Clarify_tac 1 THEN rtac conjI 2); |
|
2000 by (blast_tac (claset() addIs [differentiableD]) 2); |
|
2001 by (Blast_tac 2); |
|
2002 by (ftac DERIV_local_max 1); |
|
2003 by (EVERY1[Blast_tac,Blast_tac]); |
|
2004 by (case_tac "a < xa & xa < b" 1 THEN etac conjE 1); |
|
2005 by (Asm_full_simp_tac 2); |
|
2006 by (forw_inst_tac [("a","a"),("x","xa")] lemma_interval 1); |
|
2007 by (EVERY1[assume_tac,etac exE]); |
|
2008 by (res_inst_tac [("x","xa")] exI 1 THEN Asm_full_simp_tac 1); |
|
2009 by (subgoal_tac "(\\<exists>l. DERIV f xa :> l) & \ |
|
2010 \ (\\<exists>d. 0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1); |
|
2011 by (Clarify_tac 1 THEN rtac conjI 2); |
|
2012 by (blast_tac (claset() addIs [differentiableD]) 2); |
|
2013 by (Blast_tac 2); |
|
2014 by (ftac DERIV_local_min 1); |
|
2015 by (EVERY1[Blast_tac,Blast_tac]); |
|
2016 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> f(x) = f(b)" 1); |
|
2017 by (Clarify_tac 2); |
|
2018 by (rtac real_le_anti_sym 2); |
|
2019 by (subgoal_tac "f b = f x" 2); |
|
2020 by (Asm_full_simp_tac 2); |
|
2021 by (res_inst_tac [("x1","a"),("y1","x")] (order_le_imp_less_or_eq RS disjE) 2); |
|
2022 by (assume_tac 2); |
|
2023 by (dres_inst_tac [("z","x"),("w","b")] real_le_anti_sym 2); |
|
2024 by (subgoal_tac "f b = f xa" 5); |
|
2025 by (Asm_full_simp_tac 5); |
|
2026 by (res_inst_tac [("x1","a"),("y1","xa")] (order_le_imp_less_or_eq RS disjE) 5); |
|
2027 by (assume_tac 5); |
|
2028 by (dres_inst_tac [("z","xa"),("w","b")] real_le_anti_sym 5); |
|
2029 by (REPEAT(Asm_full_simp_tac 2)); |
|
2030 by (dtac real_dense 1 THEN etac exE 1); |
|
2031 by (res_inst_tac [("x","r")] exI 1 THEN Asm_simp_tac 1); |
|
2032 by (etac conjE 1); |
|
2033 by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1); |
|
2034 by (EVERY1[assume_tac, etac exE]); |
|
2035 by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \ |
|
2036 \ (\\<exists>d. 0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1); |
|
2037 by (Clarify_tac 1 THEN rtac conjI 2); |
|
2038 by (blast_tac (claset() addIs [differentiableD]) 2); |
|
2039 by (EVERY1[ftac DERIV_local_const, Blast_tac, Blast_tac]); |
|
2040 by (res_inst_tac [("x","d")] exI 1); |
|
2041 by (EVERY1[rtac conjI, Blast_tac, rtac allI, rtac impI]); |
|
2042 by (res_inst_tac [("s","f b")] trans 1); |
|
2043 by (blast_tac (claset() addSDs [order_less_imp_le]) 1); |
|
2044 by (rtac sym 1 THEN Blast_tac 1); |
|
2045 qed "Rolle"; |
|
2046 |
|
2047 (*----------------------------------------------------------------------------*) |
|
2048 (* Mean value theorem *) |
|
2049 (*----------------------------------------------------------------------------*) |
|
2050 |
|
2051 Goal "f a - (f b - f a)/(b - a) * a = \ |
|
2052 \ f b - (f b - f a)/(b - a) * (b::real)"; |
|
2053 by (case_tac "a = b" 1); |
|
2054 by (Asm_full_simp_tac 1); |
|
2055 by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1); |
|
2056 by (arith_tac 1); |
|
2057 by (auto_tac (claset(), simpset() addsimps [right_diff_distrib])); |
|
2058 by (auto_tac (claset(), simpset() addsimps [left_diff_distrib])); |
|
2059 qed "lemma_MVT"; |
|
2060 |
|
2061 Goal "[| a < b; \ |
|
2062 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \ |
|
2063 \ \\<forall>x. a < x & x < b --> f differentiable x |] \ |
|
2064 \ ==> \\<exists>l z. a < z & z < b & DERIV f z :> l & \ |
|
2065 \ (f(b) - f(a) = (b - a) * l)"; |
|
2066 by (dres_inst_tac [("f","%x. f(x) - (((f(b) - f(a)) / (b - a)) * x)")] |
|
2067 Rolle 1); |
|
2068 by (rtac lemma_MVT 1); |
|
2069 by Safe_tac; |
|
2070 by (rtac isCont_diff 1 THEN Blast_tac 1); |
|
2071 by (rtac (isCont_const RS isCont_mult) 1); |
|
2072 by (rtac isCont_Id 1); |
|
2073 by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"), |
|
2074 ("x","x")] spec 1); |
|
2075 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
|
2076 by Safe_tac; |
|
2077 by (res_inst_tac [("x","xa - ((f(b) - f(a)) / (b - a))")] exI 1); |
|
2078 by (rtac DERIV_diff 1 THEN assume_tac 1); |
|
2079 (*derivative of a linear function is the constant...*) |
|
2080 by (subgoal_tac "(%x. (f b - f a) * x / (b - a)) = \ |
|
2081 \ op * ((f b - f a) / (b - a))" 1); |
|
2082 by (rtac ext 2 THEN Simp_tac 2); |
|
2083 by (Asm_full_simp_tac 1); |
|
2084 (*final case*) |
|
2085 by (res_inst_tac [("x","((f(b) - f(a)) / (b - a))")] exI 1); |
|
2086 by (res_inst_tac [("x","z")] exI 1); |
|
2087 by Safe_tac; |
|
2088 by (Asm_full_simp_tac 2); |
|
2089 by (subgoal_tac "DERIV (%x. ((f(b) - f(a)) / (b - a)) * x) z :> \ |
|
2090 \ ((f(b) - f(a)) / (b - a))" 1); |
|
2091 by (rtac DERIV_cmult_Id 2); |
|
2092 by (dtac DERIV_add 1 THEN assume_tac 1); |
|
2093 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc, real_diff_def]) 1); |
|
2094 qed "MVT"; |
|
2095 |
|
2096 (*----------------------------------------------------------------------------*) |
|
2097 (* Theorem that function is constant if its derivative is 0 over an interval. *) |
|
2098 (*----------------------------------------------------------------------------*) |
|
2099 |
|
2100 Goal "[| a < b; \ |
|
2101 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \ |
|
2102 \ \\<forall>x. a < x & x < b --> DERIV f x :> 0 |] \ |
|
2103 \ ==> (f b = f a)"; |
|
2104 by (dtac MVT 1 THEN assume_tac 1); |
|
2105 by (blast_tac (claset() addIs [differentiableI]) 1); |
|
2106 by (auto_tac (claset() addSDs [DERIV_unique],simpset() |
|
2107 addsimps [diff_eq_eq])); |
|
2108 qed "DERIV_isconst_end"; |
|
2109 |
|
2110 Goal "[| a < b; \ |
|
2111 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \ |
|
2112 \ \\<forall>x. a < x & x < b --> DERIV f x :> 0 |] \ |
|
2113 \ ==> \\<forall>x. a \\<le> x & x \\<le> b --> f x = f a"; |
|
2114 by Safe_tac; |
|
2115 by (dres_inst_tac [("x","a")] order_le_imp_less_or_eq 1); |
|
2116 by Safe_tac; |
|
2117 by (dres_inst_tac [("b","x")] DERIV_isconst_end 1); |
|
2118 by Auto_tac; |
|
2119 qed "DERIV_isconst1"; |
|
2120 |
|
2121 Goal "[| a < b; \ |
|
2122 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \ |
|
2123 \ \\<forall>x. a < x & x < b --> DERIV f x :> 0; \ |
|
2124 \ a \\<le> x; x \\<le> b |] \ |
|
2125 \ ==> f x = f a"; |
|
2126 by (blast_tac (claset() addDs [DERIV_isconst1]) 1); |
|
2127 qed "DERIV_isconst2"; |
|
2128 |
|
2129 Goal "\\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)"; |
|
2130 by (res_inst_tac [("x","x"),("y","y")] linorder_cases 1); |
|
2131 by (rtac sym 1); |
|
2132 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_isconst_end],simpset())); |
|
2133 qed "DERIV_isconst_all"; |
|
2134 |
|
2135 Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k"; |
|
2136 by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1); |
|
2137 by Auto_tac; |
|
2138 by (ALLGOALS(dres_inst_tac [("f","f")] MVT)); |
|
2139 by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps |
|
2140 [differentiable_def])); |
|
2141 by (auto_tac (claset() addDs [DERIV_unique], |
|
2142 simpset() addsimps [left_distrib, real_diff_def])); |
|
2143 qed "DERIV_const_ratio_const"; |
|
2144 |
|
2145 Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k"; |
|
2146 by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1); |
|
2147 by (auto_tac (claset() addSDs [DERIV_const_ratio_const], |
|
2148 simpset() addsimps [real_mult_assoc])); |
|
2149 qed "DERIV_const_ratio_const2"; |
|
2150 |
|
2151 Goal "((a + b) /2 - a) = (b - a)/(2::real)"; |
|
2152 by Auto_tac; |
|
2153 qed "real_average_minus_first"; |
|
2154 Addsimps [real_average_minus_first]; |
|
2155 |
|
2156 Goal "((b + a)/2 - a) = (b - a)/(2::real)"; |
|
2157 by Auto_tac; |
|
2158 qed "real_average_minus_second"; |
|
2159 Addsimps [real_average_minus_second]; |
|
2160 |
|
2161 |
|
2162 (* Gallileo's "trick": average velocity = av. of end velocities *) |
|
2163 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \ |
|
2164 \ ==> v((a + b)/2) = (v a + v b)/2"; |
|
2165 by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1); |
|
2166 by Safe_tac; |
|
2167 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1); |
|
2168 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2); |
|
2169 by (dtac real_less_half_sum 1); |
|
2170 by (dtac real_gt_half_sum 2); |
|
2171 by (ftac (real_not_refl2 RS DERIV_const_ratio_const2) 1 THEN assume_tac 1); |
|
2172 by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2 |
|
2173 THEN assume_tac 2); |
|
2174 by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong)); |
|
2175 by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide])); |
|
2176 by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1); |
|
2177 qed "DERIV_const_average"; |
|
2178 |
|
2179 |
|
2180 (* ------------------------------------------------------------------------ *) |
|
2181 (* Dull lemma that an continuous injection on an interval must have a strict*) |
|
2182 (* maximum at an end point, not in the middle. *) |
|
2183 (* ------------------------------------------------------------------------ *) |
|
2184 |
|
2185 Goal "[|0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \ |
|
2186 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \ |
|
2187 \ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(z) \\<le> f(x))"; |
|
2188 by (rtac notI 1); |
|
2189 by (rotate_tac 3 1); |
|
2190 by (forw_inst_tac [("x","x - d")] spec 1); |
|
2191 by (forw_inst_tac [("x","x + d")] spec 1); |
|
2192 by Safe_tac; |
|
2193 by (cut_inst_tac [("x","f(x - d)"),("y","f(x + d)")] |
|
2194 (ARITH_PROVE "x \\<le> y | y \\<le> (x::real)") 4); |
|
2195 by (etac disjE 4); |
|
2196 by (REPEAT(arith_tac 1)); |
|
2197 by (cut_inst_tac [("f","f"),("a","x - d"),("b","x"),("y","f(x + d)")] |
|
2198 IVT_objl 1); |
|
2199 by Safe_tac; |
|
2200 by (arith_tac 1); |
|
2201 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2202 by (dres_inst_tac [("f","g")] arg_cong 1); |
|
2203 by (rotate_tac 2 1); |
|
2204 by (forw_inst_tac [("x","xa")] spec 1); |
|
2205 by (dres_inst_tac [("x","x + d")] spec 1); |
|
2206 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2207 (* 2nd case: similar *) |
|
2208 by (cut_inst_tac [("f","f"),("a","x"),("b","x + d"),("y","f(x - d)")] |
|
2209 IVT2_objl 1); |
|
2210 by Safe_tac; |
|
2211 by (arith_tac 1); |
|
2212 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2213 by (dres_inst_tac [("f","g")] arg_cong 1); |
|
2214 by (rotate_tac 2 1); |
|
2215 by (forw_inst_tac [("x","xa")] spec 1); |
|
2216 by (dres_inst_tac [("x","x - d")] spec 1); |
|
2217 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2218 qed "lemma_isCont_inj"; |
|
2219 |
|
2220 (* ------------------------------------------------------------------------ *) |
|
2221 (* Similar version for lower bound *) |
|
2222 (* ------------------------------------------------------------------------ *) |
|
2223 |
|
2224 Goal "[|0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \ |
|
2225 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \ |
|
2226 \ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(x) \\<le> f(z))"; |
|
2227 by (auto_tac (claset() addSDs [(asm_full_simplify (simpset()) |
|
2228 (read_instantiate [("f","%x. - f x"),("g","%y. g(-y)"),("x","x"),("d","d")] |
|
2229 lemma_isCont_inj))],simpset() addsimps [isCont_minus])); |
|
2230 qed "lemma_isCont_inj2"; |
|
2231 |
|
2232 (* ------------------------------------------------------------------------ *) |
|
2233 (* Show there's an interval surrounding f(x) in f[[x - d, x + d]] *) |
|
2234 (* Also from John's theory *) |
|
2235 (* ------------------------------------------------------------------------ *) |
|
2236 |
|
2237 val lemma_le = ARITH_PROVE "0 \\<le> (d::real) ==> -d \\<le> d"; |
|
2238 |
|
2239 (* FIXME: awful proof - needs improvement *) |
|
2240 Goal "[| 0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \ |
|
2241 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \ |
|
2242 \ ==> \\<exists>e. 0 < e & \ |
|
2243 \ (\\<forall>y. \ |
|
2244 \ abs(y - f(x)) \\<le> e --> \ |
|
2245 \ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))"; |
|
2246 by (ftac order_less_imp_le 1); |
|
2247 by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate |
|
2248 [("f","f"),("a","x - d"),("b","x + d")] isCont_Lb_Ub))) 1); |
|
2249 by Safe_tac; |
|
2250 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2251 by (subgoal_tac "L \\<le> f x & f x \\<le> M" 1); |
|
2252 by (dres_inst_tac [("P", "%v. ?P v --> ?Q v & ?R v"), ("x","x")] spec 2); |
|
2253 by (Asm_full_simp_tac 2); |
|
2254 by (subgoal_tac "L < f x & f x < M" 1); |
|
2255 by Safe_tac; |
|
2256 by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1); |
|
2257 by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1); |
|
2258 by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")] |
|
2259 (real_lbound_gt_zero) 1); |
|
2260 by Safe_tac; |
|
2261 by (res_inst_tac [("x","e")] exI 1); |
|
2262 by Safe_tac; |
|
2263 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
|
2264 by (dres_inst_tac [("P","%v. ?PP v --> (\\<exists>xa. ?Q v xa)"),("x","y")] spec 1); |
|
2265 by (Step_tac 1 THEN REPEAT(arith_tac 1)); |
|
2266 by (res_inst_tac [("x","xa")] exI 1); |
|
2267 by (arith_tac 1); |
|
2268 by (ALLGOALS(etac (ARITH_PROVE "[|x \\<le> y; x \\<noteq> y |] ==> x < (y::real)"))); |
|
2269 by (ALLGOALS(rotate_tac 3)); |
|
2270 by (dtac lemma_isCont_inj2 1); |
|
2271 by (assume_tac 2); |
|
2272 by (dtac lemma_isCont_inj 3); |
|
2273 by (assume_tac 4); |
|
2274 by (TRYALL(assume_tac)); |
|
2275 by Safe_tac; |
|
2276 by (ALLGOALS(dres_inst_tac [("x","z")] spec)); |
|
2277 by (ALLGOALS(arith_tac)); |
|
2278 qed "isCont_inj_range"; |
|
2279 |
|
2280 |
|
2281 (* ------------------------------------------------------------------------ *) |
|
2282 (* Continuity of inverse function *) |
|
2283 (* ------------------------------------------------------------------------ *) |
|
2284 |
|
2285 Goal "[| 0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \ |
|
2286 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \ |
|
2287 \ ==> isCont g (f x)"; |
|
2288 by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1); |
|
2289 by Safe_tac; |
|
2290 by (dres_inst_tac [("d1.0","r")] (real_lbound_gt_zero) 1); |
|
2291 by (assume_tac 1 THEN Step_tac 1); |
|
2292 by (subgoal_tac "\\<forall>z. abs(z - x) \\<le> e --> (g(f z) = z)" 1); |
|
2293 by (Force_tac 2); |
|
2294 by (subgoal_tac "\\<forall>z. abs(z - x) \\<le> e --> isCont f z" 1); |
|
2295 by (Force_tac 2); |
|
2296 by (dres_inst_tac [("d","e")] isCont_inj_range 1); |
|
2297 by (assume_tac 2 THEN assume_tac 1); |
|
2298 by Safe_tac; |
|
2299 by (res_inst_tac [("x","ea")] exI 1); |
|
2300 by Auto_tac; |
|
2301 by (rotate_tac 4 1); |
|
2302 by (dres_inst_tac [("x","f(x) + xa")] spec 1); |
|
2303 by Auto_tac; |
|
2304 by (dtac sym 1 THEN Auto_tac); |
|
2305 by (arith_tac 1); |
|
2306 qed "isCont_inverse_function"; |
|
2307 |
|