1 (* Title : Lim.ML |
1 (* Title : Lim.ML |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Description : Theory of limits, continuity and |
4 Description : Theory of limits, continuity and |
5 differentiation of real=>real functions |
5 differentiation of real=>real functions |
6 *) |
6 *) |
7 |
7 |
8 fun ARITH_PROVE str = prove_goal thy str |
8 fun ARITH_PROVE str = prove_goal thy str |
9 (fn prems => [cut_facts_tac prems 1,arith_tac 1]); |
9 (fn prems => [cut_facts_tac prems 1,arith_tac 1]); |
10 |
10 |
11 |
11 |
12 (*--------------------------------------------------------------- |
12 (*--------------------------------------------------------------- |
13 Theory of limits, continuity and differentiation of |
13 Theory of limits, continuity and differentiation of |
14 real=>real functions |
14 real=>real functions |
15 ----------------------------------------------------------------*) |
15 ----------------------------------------------------------------*) |
16 |
16 |
17 Goalw [LIM_def] "(%x. k) -- x --> k"; |
17 Goalw [LIM_def] "(%x. k) -- x --> k"; |
18 by Auto_tac; |
18 by Auto_tac; |
19 qed "LIM_const"; |
19 qed "LIM_const"; |
20 Addsimps [LIM_const]; |
20 Addsimps [LIM_const]; |
21 |
21 |
22 (***-----------------------------------------------------------***) |
22 (***-----------------------------------------------------------***) |
23 (*** Some Purely Standard Proofs - Can be used for comparison ***) |
23 (*** Some Purely Standard Proofs - Can be used for comparison ***) |
24 (***-----------------------------------------------------------***) |
24 (***-----------------------------------------------------------***) |
25 |
25 |
26 (*--------------- |
26 (*--------------- |
27 LIM_add |
27 LIM_add |
28 ---------------*) |
28 ---------------*) |
29 Goalw [LIM_def] |
29 Goalw [LIM_def] |
30 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
30 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
31 by (Clarify_tac 1); |
31 by (Clarify_tac 1); |
32 by (REPEAT(dres_inst_tac [("x","r/2")] spec 1)); |
32 by (REPEAT(dres_inst_tac [("x","r/2")] spec 1)); |
33 by (Asm_full_simp_tac 1); |
33 by (Asm_full_simp_tac 1); |
34 by (Clarify_tac 1); |
34 by (Clarify_tac 1); |
35 by (res_inst_tac [("x","s"),("y","sa")] linorder_cases 1); |
35 by (res_inst_tac [("x","s"),("y","sa")] linorder_cases 1); |
36 by (res_inst_tac [("x","s")] exI 1); |
36 by (res_inst_tac [("x","s")] exI 1); |
37 by (res_inst_tac [("x","sa")] exI 2); |
37 by (res_inst_tac [("x","sa")] exI 2); |
38 by (res_inst_tac [("x","sa")] exI 3); |
38 by (res_inst_tac [("x","sa")] exI 3); |
39 by Safe_tac; |
39 by Safe_tac; |
40 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
40 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
41 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
41 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
42 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
42 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
43 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
43 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
44 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
44 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
45 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
45 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
46 by (ALLGOALS(rtac (abs_sum_triangle_ineq RS order_le_less_trans))); |
46 by (ALLGOALS(rtac (abs_sum_triangle_ineq RS order_le_less_trans))); |
47 by (ALLGOALS(rtac (real_sum_of_halves RS subst))); |
47 by (ALLGOALS(rtac (real_sum_of_halves RS subst))); |
48 by (auto_tac (claset() addIs [add_strict_mono],simpset())); |
48 by (auto_tac (claset() addIs [add_strict_mono],simpset())); |
49 qed "LIM_add"; |
49 qed "LIM_add"; |
50 |
50 |
51 Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; |
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); |
52 by (subgoal_tac "ALL x. abs(- f x + L) = abs(f x + - L)" 1); |
53 by (Asm_full_simp_tac 1); |
53 by (Asm_full_simp_tac 1); |
54 by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1); |
54 by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1); |
55 qed "LIM_minus"; |
55 qed "LIM_minus"; |
56 |
56 |
57 (*---------------------------------------------- |
57 (*---------------------------------------------- |
58 LIM_add_minus |
58 LIM_add_minus |
59 ----------------------------------------------*) |
59 ----------------------------------------------*) |
113 by (dres_inst_tac [("x","1")] spec 1); |
113 by (dres_inst_tac [("x","1")] spec 1); |
114 by (dres_inst_tac [("x","r")] spec 1); |
114 by (dres_inst_tac [("x","r")] spec 1); |
115 by (cut_facts_tac [real_zero_less_one] 1); |
115 by (cut_facts_tac [real_zero_less_one] 1); |
116 by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1); |
116 by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1); |
117 by (Clarify_tac 1); |
117 by (Clarify_tac 1); |
118 by (res_inst_tac [("x","s"),("y","sa")] |
118 by (res_inst_tac [("x","s"),("y","sa")] |
119 linorder_cases 1); |
119 linorder_cases 1); |
120 by (res_inst_tac [("x","s")] exI 1); |
120 by (res_inst_tac [("x","s")] exI 1); |
121 by (res_inst_tac [("x","sa")] exI 2); |
121 by (res_inst_tac [("x","sa")] exI 2); |
122 by (res_inst_tac [("x","sa")] exI 3); |
122 by (res_inst_tac [("x","sa")] exI 3); |
123 by Safe_tac; |
123 by Safe_tac; |
124 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
124 by (REPEAT(dres_inst_tac [("x","xa")] spec 1) |
125 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
125 THEN step_tac (claset() addSEs [order_less_trans]) 1); |
126 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
126 by (REPEAT(dres_inst_tac [("x","xa")] spec 2) |
127 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
127 THEN step_tac (claset() addSEs [order_less_trans]) 2); |
128 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
128 by (REPEAT(dres_inst_tac [("x","xa")] spec 3) |
129 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
129 THEN step_tac (claset() addSEs [order_less_trans]) 3); |
130 by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst))); |
130 by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst))); |
131 by (ALLGOALS(rtac abs_mult_less)); |
131 by (ALLGOALS(rtac abs_mult_less)); |
132 by Auto_tac; |
132 by Auto_tac; |
133 qed "LIM_mult_zero"; |
133 qed "LIM_mult_zero"; |
155 (*** End of Purely Standard Proofs ***) |
155 (*** End of Purely Standard Proofs ***) |
156 (***-------------------------------------------------------------***) |
156 (***-------------------------------------------------------------***) |
157 (*-------------------------------------------------------------- |
157 (*-------------------------------------------------------------- |
158 Standard and NS definitions of Limit |
158 Standard and NS definitions of Limit |
159 --------------------------------------------------------------*) |
159 --------------------------------------------------------------*) |
160 Goalw [LIM_def,NSLIM_def,approx_def] |
160 Goalw [LIM_def,NSLIM_def,approx_def] |
161 "f -- x --> L ==> f -- x --NS> L"; |
161 "f -- x --> L ==> f -- x --NS> L"; |
162 by (asm_full_simp_tac |
162 by (asm_full_simp_tac |
163 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
163 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
164 by Safe_tac; |
164 by Safe_tac; |
165 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
165 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
166 by (auto_tac (claset(), |
166 by (auto_tac (claset(), |
167 simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus, |
167 simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus, |
168 hypreal_of_real_def, hypreal_add])); |
168 hypreal_of_real_def, hypreal_add])); |
169 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1); |
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); |
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); |
171 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1); |
172 by (subgoal_tac "\\<forall>n::nat. (xa n) \\<noteq> x & \ |
172 by (subgoal_tac "\\<forall>n::nat. (xa n) \\<noteq> x & \ |
173 \ abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u" 1); |
173 \ abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u" 1); |
174 by (Blast_tac 2); |
174 by (Blast_tac 2); |
175 by (dtac FreeUltrafilterNat_all 1); |
175 by (dtac FreeUltrafilterNat_all 1); |
176 by (Ultra_tac 1); |
176 by (Ultra_tac 1); |
177 qed "LIM_NSLIM"; |
177 qed "LIM_NSLIM"; |
178 |
178 |
179 (*--------------------------------------------------------------------- |
179 (*--------------------------------------------------------------------- |
180 Limit: NS definition ==> standard definition |
180 Limit: NS definition ==> standard definition |
181 ---------------------------------------------------------------------*) |
181 ---------------------------------------------------------------------*) |
182 |
182 |
183 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
183 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
184 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
184 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
185 \ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \ |
185 \ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \ |
186 \ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)"; |
186 \ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)"; |
187 by (Clarify_tac 1); |
187 by (Clarify_tac 1); |
188 by (cut_inst_tac [("n1","n")] |
188 by (cut_inst_tac [("n1","n")] |
189 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
189 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
190 by Auto_tac; |
190 by Auto_tac; |
191 val lemma_LIM = result(); |
191 qed "lemma_LIM"; |
192 |
192 |
193 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
193 Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \ |
194 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
194 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \ |
195 \ ==> \\<exists>X. \\<forall>n::nat. X n \\<noteq> x & \ |
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)"; |
196 \ abs(X n + -x) < inverse(real(Suc n)) & r \\<le> abs(f (X n) + -L)"; |
197 by (dtac lemma_LIM 1); |
197 by (dtac lemma_LIM 1); |
198 by (dtac choice 1); |
198 by (dtac choice 1); |
199 by (Blast_tac 1); |
199 by (Blast_tac 1); |
200 val lemma_skolemize_LIM2 = result(); |
200 qed "lemma_skolemize_LIM2"; |
201 |
201 |
202 Goal "\\<forall>n. X n \\<noteq> x & \ |
202 Goal "\\<forall>n. X n \\<noteq> x & \ |
203 \ abs (X n + - x) < inverse (real(Suc n)) & \ |
203 \ abs (X n + - x) < inverse (real(Suc n)) & \ |
204 \ r \\<le> abs (f (X n) + - L) ==> \ |
204 \ r \\<le> abs (f (X n) + - L) ==> \ |
205 \ \\<forall>n. abs (X n + - x) < inverse (real(Suc n))"; |
205 \ \\<forall>n. abs (X n + - x) < inverse (real(Suc n))"; |
206 by (Auto_tac ); |
206 by (Auto_tac ); |
207 val lemma_simp = result(); |
207 qed "lemma_simp"; |
208 |
208 |
209 (*------------------- |
209 (*------------------- |
210 NSLIM => LIM |
210 NSLIM => LIM |
211 -------------------*) |
211 -------------------*) |
212 |
212 |
213 Goalw [LIM_def,NSLIM_def,approx_def] |
213 Goalw [LIM_def,NSLIM_def,approx_def] |
214 "f -- x --NS> L ==> f -- x --> L"; |
214 "f -- x --NS> L ==> f -- x --> L"; |
215 by (asm_full_simp_tac |
215 by (asm_full_simp_tac |
216 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
216 (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
217 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
217 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
218 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
218 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
219 by (dtac lemma_skolemize_LIM2 1); |
219 by (dtac lemma_skolemize_LIM2 1); |
220 by Safe_tac; |
220 by Safe_tac; |
221 by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1); |
221 by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1); |
222 by (auto_tac |
222 by (auto_tac |
223 (claset(), |
223 (claset(), |
224 simpset() addsimps [starfun, hypreal_minus, |
224 simpset() addsimps [starfun, hypreal_minus, |
225 hypreal_of_real_def,hypreal_add])); |
225 hypreal_of_real_def,hypreal_add])); |
226 by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1); |
226 by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1); |
227 by (asm_full_simp_tac |
227 by (asm_full_simp_tac |
228 (simpset() addsimps |
228 (simpset() addsimps |
229 [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def, |
229 [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def, |
230 hypreal_minus, hypreal_add]) 1); |
230 hypreal_minus, hypreal_add]) 1); |
231 by (Blast_tac 1); |
231 by (Blast_tac 1); |
232 by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1); |
232 by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1); |
233 by (dtac FreeUltrafilterNat_all 1); |
233 by (dtac FreeUltrafilterNat_all 1); |
234 by (Ultra_tac 1); |
234 by (Ultra_tac 1); |
235 qed "NSLIM_LIM"; |
235 qed "NSLIM_LIM"; |
236 |
236 |
428 |
428 |
429 (*----------------------------------------------------------------------------- |
429 (*----------------------------------------------------------------------------- |
430 Derivatives and Continuity - NS and Standard properties |
430 Derivatives and Continuity - NS and Standard properties |
431 -----------------------------------------------------------------------------*) |
431 -----------------------------------------------------------------------------*) |
432 (*--------------- |
432 (*--------------- |
433 Continuity |
433 Continuity |
434 ---------------*) |
434 ---------------*) |
435 |
435 |
436 Goalw [isNSCont_def] |
436 Goalw [isNSCont_def] |
437 "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \ |
437 "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \ |
438 \ ==> ( *f* f) y \\<approx> hypreal_of_real (f a)"; |
438 \ ==> ( *f* f) y \\<approx> hypreal_of_real (f a)"; |
439 by (Blast_tac 1); |
439 by (Blast_tac 1); |
440 qed "isNSContD"; |
440 qed "isNSContD"; |
441 |
441 |
442 Goalw [isNSCont_def,NSLIM_def] |
442 Goalw [isNSCont_def,NSLIM_def] |
443 "isNSCont f a ==> f -- a --NS> (f a) "; |
443 "isNSCont f a ==> f -- a --NS> (f a) "; |
444 by (Blast_tac 1); |
444 by (Blast_tac 1); |
445 qed "isNSCont_NSLIM"; |
445 qed "isNSCont_NSLIM"; |
446 |
446 |
447 Goalw [isNSCont_def,NSLIM_def] |
447 Goalw [isNSCont_def,NSLIM_def] |
448 "f -- a --NS> (f a) ==> isNSCont f a"; |
448 "f -- a --NS> (f a) ==> isNSCont f a"; |
449 by Auto_tac; |
449 by Auto_tac; |
450 by (res_inst_tac [("Q","y = hypreal_of_real a")] |
450 by (res_inst_tac [("Q","y = hypreal_of_real a")] |
451 (excluded_middle RS disjE) 1); |
451 (excluded_middle RS disjE) 1); |
452 by Auto_tac; |
452 by Auto_tac; |
453 qed "NSLIM_isNSCont"; |
453 qed "NSLIM_isNSCont"; |
454 |
454 |
455 (*----------------------------------------------------- |
455 (*----------------------------------------------------- |
463 (*---------------------------------------------- |
463 (*---------------------------------------------- |
464 Hence, NS continuity can be given |
464 Hence, NS continuity can be given |
465 in terms of standard limit |
465 in terms of standard limit |
466 ---------------------------------------------*) |
466 ---------------------------------------------*) |
467 Goal "(isNSCont f a) = (f -- a --> (f a))"; |
467 Goal "(isNSCont f a) = (f -- a --> (f a))"; |
468 by (asm_full_simp_tac (simpset() addsimps |
468 by (asm_full_simp_tac (simpset() addsimps |
469 [LIM_NSLIM_iff,isNSCont_NSLIM_iff]) 1); |
469 [LIM_NSLIM_iff,isNSCont_NSLIM_iff]) 1); |
470 qed "isNSCont_LIM_iff"; |
470 qed "isNSCont_LIM_iff"; |
471 |
471 |
472 (*----------------------------------------------- |
472 (*----------------------------------------------- |
473 Moreover, it's trivial now that NS continuity |
473 Moreover, it's trivial now that NS continuity |
474 is equivalent to standard continuity |
474 is equivalent to standard continuity |
475 -----------------------------------------------*) |
475 -----------------------------------------------*) |
476 Goalw [isCont_def] "(isNSCont f a) = (isCont f a)"; |
476 Goalw [isCont_def] "(isNSCont f a) = (isCont f a)"; |
477 by (rtac isNSCont_LIM_iff 1); |
477 by (rtac isNSCont_LIM_iff 1); |
478 qed "isNSCont_isCont_iff"; |
478 qed "isNSCont_isCont_iff"; |
479 |
479 |
480 (*---------------------------------------- |
480 (*---------------------------------------- |
481 Standard continuity ==> NS continuity |
481 Standard continuity ==> NS continuity |
482 ----------------------------------------*) |
482 ----------------------------------------*) |
483 Goal "isCont f a ==> isNSCont f a"; |
483 Goal "isCont f a ==> isNSCont f a"; |
484 by (etac (isNSCont_isCont_iff RS iffD2) 1); |
484 by (etac (isNSCont_isCont_iff RS iffD2) 1); |
485 qed "isCont_isNSCont"; |
485 qed "isCont_isNSCont"; |
486 |
486 |
487 (*---------------------------------------- |
487 (*---------------------------------------- |
488 NS continuity ==> Standard continuity |
488 NS continuity ==> Standard continuity |
489 ----------------------------------------*) |
489 ----------------------------------------*) |
490 Goal "isNSCont f a ==> isCont f a"; |
490 Goal "isNSCont f a ==> isCont f a"; |
491 by (etac (isNSCont_isCont_iff RS iffD1) 1); |
491 by (etac (isNSCont_isCont_iff RS iffD1) 1); |
492 qed "isNSCont_isCont"; |
492 qed "isNSCont_isCont"; |
493 |
493 |
560 \ ==> isCont (%x. g (f x)) a"; |
560 \ ==> isCont (%x. g (f x)) a"; |
561 by (auto_tac (claset() addDs [isCont_o],simpset() addsimps [o_def])); |
561 by (auto_tac (claset() addDs [isCont_o],simpset() addsimps [o_def])); |
562 qed "isCont_o2"; |
562 qed "isCont_o2"; |
563 |
563 |
564 Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a"; |
564 Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a"; |
565 by Auto_tac; |
565 by Auto_tac; |
566 qed "isNSCont_minus"; |
566 qed "isNSCont_minus"; |
567 |
567 |
568 Goal "isCont f a ==> isCont (%x. - f x) a"; |
568 Goal "isCont f a ==> isCont (%x. - f x) a"; |
569 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
569 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym, |
570 isNSCont_minus])); |
570 isNSCont_minus])); |
571 qed "isCont_minus"; |
571 qed "isCont_minus"; |
572 |
572 |
573 Goalw [isCont_def] |
573 Goalw [isCont_def] |
574 "[| isCont f x; f x \\<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"; |
574 "[| isCont f x; f x \\<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"; |
575 by (blast_tac (claset() addIs [LIM_inverse]) 1); |
575 by (blast_tac (claset() addIs [LIM_inverse]) 1); |
576 qed "isCont_inverse"; |
576 qed "isCont_inverse"; |
577 |
577 |
578 Goal "[| isNSCont f x; f x \\<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"; |
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 |
579 by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps |
580 [isNSCont_isCont_iff])); |
580 [isNSCont_isCont_iff])); |
581 qed "isNSCont_inverse"; |
581 qed "isNSCont_inverse"; |
582 |
582 |
583 Goalw [real_diff_def] |
583 Goalw [real_diff_def] |
584 "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"; |
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())); |
585 by (auto_tac (claset() addIs [isCont_add,isCont_minus],simpset())); |
586 qed "isCont_diff"; |
586 qed "isCont_diff"; |
587 |
587 |
588 Goalw [isCont_def] "isCont (%x. k) a"; |
588 Goalw [isCont_def] "isCont (%x. k) a"; |
608 Addsimps [isCont_rabs]; |
608 Addsimps [isCont_rabs]; |
609 |
609 |
610 (**************************************************************** |
610 (**************************************************************** |
611 (%* Leave as commented until I add topology theory or remove? *%) |
611 (%* Leave as commented until I add topology theory or remove? *%) |
612 (%*------------------------------------------------------------ |
612 (%*------------------------------------------------------------ |
613 Elementary topology proof for a characterisation of |
613 Elementary topology proof for a characterisation of |
614 continuity now: a function f is continuous if and only |
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 |
615 if the inverse image, {x. f(x) \\<in> A}, of any open set A |
616 is always an open set |
616 is always an open set |
617 ------------------------------------------------------------*%) |
617 ------------------------------------------------------------*%) |
618 Goal "[| isNSopen A; \\<forall>x. isNSCont f x |] \ |
618 Goal "[| isNSopen A; \\<forall>x. isNSCont f x |] \ |
619 \ ==> isNSopen {x. f x \\<in> A}"; |
619 \ ==> isNSopen {x. f x \\<in> A}"; |
620 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
620 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
656 *******************************************************************) |
656 *******************************************************************) |
657 |
657 |
658 (*----------------------------------------------------------------- |
658 (*----------------------------------------------------------------- |
659 Uniform continuity |
659 Uniform continuity |
660 ------------------------------------------------------------------*) |
660 ------------------------------------------------------------------*) |
661 Goalw [isNSUCont_def] |
661 Goalw [isNSUCont_def] |
662 "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y"; |
662 "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y"; |
663 by (Blast_tac 1); |
663 by (Blast_tac 1); |
664 qed "isNSUContD"; |
664 qed "isNSUContD"; |
665 |
665 |
666 Goalw [isUCont_def,isCont_def,LIM_def] |
666 Goalw [isUCont_def,isCont_def,LIM_def] |
667 "isUCont f ==> isCont f x"; |
667 "isUCont f ==> isCont f x"; |
668 by (Clarify_tac 1); |
668 by (Clarify_tac 1); |
669 by (dtac spec 1); |
669 by (dtac spec 1); |
670 by (Blast_tac 1); |
670 by (Blast_tac 1); |
671 qed "isUCont_isCont"; |
671 qed "isUCont_isCont"; |
672 |
672 |
673 Goalw [isNSUCont_def,isUCont_def,approx_def] |
673 Goalw [isNSUCont_def,isUCont_def,approx_def] |
674 "isUCont f ==> isNSUCont f"; |
674 "isUCont f ==> isNSUCont f"; |
675 by (asm_full_simp_tac (simpset() addsimps |
675 by (asm_full_simp_tac (simpset() addsimps |
676 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
676 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
677 by Safe_tac; |
677 by Safe_tac; |
678 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
678 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
679 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
679 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
680 by (auto_tac (claset(),simpset() addsimps [starfun, |
680 by (auto_tac (claset(),simpset() addsimps [starfun, |
691 |
691 |
692 Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \ |
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. \ |
693 \ ==> \\<forall>n::nat. \\<exists>z y. \ |
694 \ abs(z + -y) < inverse(real(Suc n)) & \ |
694 \ abs(z + -y) < inverse(real(Suc n)) & \ |
695 \ r \\<le> abs(f z + -f y)"; |
695 \ r \\<le> abs(f z + -f y)"; |
696 by (Clarify_tac 1); |
696 by (Clarify_tac 1); |
697 by (cut_inst_tac [("n1","n")] |
697 by (cut_inst_tac [("n1","n")] |
698 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
698 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
699 by Auto_tac; |
699 by Auto_tac; |
700 val lemma_LIMu = result(); |
700 qed "lemma_LIMu"; |
701 |
701 |
702 Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \ |
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. \ |
703 \ ==> \\<exists>X Y. \\<forall>n::nat. \ |
704 \ abs(X n + -(Y n)) < inverse(real(Suc n)) & \ |
704 \ abs(X n + -(Y n)) < inverse(real(Suc n)) & \ |
705 \ r \\<le> abs(f (X n) + -f (Y n))"; |
705 \ r \\<le> abs(f (X n) + -f (Y n))"; |
706 by (dtac lemma_LIMu 1); |
706 by (dtac lemma_LIMu 1); |
707 by (dtac choice 1); |
707 by (dtac choice 1); |
708 by Safe_tac; |
708 by Safe_tac; |
709 by (dtac choice 1); |
709 by (dtac choice 1); |
710 by (Blast_tac 1); |
710 by (Blast_tac 1); |
711 val lemma_skolemize_LIM2u = result(); |
711 qed "lemma_skolemize_LIM2u"; |
712 |
712 |
713 Goal "\\<forall>n. abs (X n + -Y n) < inverse (real(Suc n)) & \ |
713 Goal "\\<forall>n. abs (X n + -Y n) < inverse (real(Suc n)) & \ |
714 \ r \\<le> abs (f (X n) + - f(Y n)) ==> \ |
714 \ r \\<le> abs (f (X n) + - f(Y n)) ==> \ |
715 \ \\<forall>n. abs (X n + - Y n) < inverse (real(Suc n))"; |
715 \ \\<forall>n. abs (X n + - Y n) < inverse (real(Suc n))"; |
716 by (Auto_tac ); |
716 by (Auto_tac ); |
717 val lemma_simpu = result(); |
717 qed "lemma_simpu"; |
718 |
718 |
719 Goalw [isNSUCont_def,isUCont_def,approx_def] |
719 Goalw [isNSUCont_def,isUCont_def,approx_def] |
720 "isNSUCont f ==> isUCont f"; |
720 "isNSUCont f ==> isUCont f"; |
721 by (asm_full_simp_tac (simpset() addsimps |
721 by (asm_full_simp_tac (simpset() addsimps |
722 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
722 [Infinitesimal_FreeUltrafilterNat_iff]) 1); |
723 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
723 by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]); |
724 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
724 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
725 by (dtac lemma_skolemize_LIM2u 1); |
725 by (dtac lemma_skolemize_LIM2u 1); |
726 by Safe_tac; |
726 by Safe_tac; |
741 qed "isNSUCont_isUCont"; |
741 qed "isNSUCont_isUCont"; |
742 |
742 |
743 (*------------------------------------------------------------------ |
743 (*------------------------------------------------------------------ |
744 Derivatives |
744 Derivatives |
745 ------------------------------------------------------------------*) |
745 ------------------------------------------------------------------*) |
746 Goalw [deriv_def] |
746 Goalw [deriv_def] |
747 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)"; |
747 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)"; |
748 by (Blast_tac 1); |
748 by (Blast_tac 1); |
749 qed "DERIV_iff"; |
749 qed "DERIV_iff"; |
750 |
750 |
751 Goalw [deriv_def] |
751 Goalw [deriv_def] |
752 "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"; |
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); |
753 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
754 qed "DERIV_NS_iff"; |
754 qed "DERIV_NS_iff"; |
755 |
755 |
756 Goalw [deriv_def] |
756 Goalw [deriv_def] |
757 "DERIV f x :> D \ |
757 "DERIV f x :> D \ |
758 \ ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"; |
758 \ ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"; |
759 by (Blast_tac 1); |
759 by (Blast_tac 1); |
760 qed "DERIVD"; |
760 qed "DERIVD"; |
761 |
761 |
762 Goalw [deriv_def] "DERIV f x :> D ==> \ |
762 Goalw [deriv_def] "DERIV f x :> D ==> \ |
763 \ (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"; |
763 \ (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"; |
764 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
764 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1); |
765 qed "NS_DERIVD"; |
765 qed "NS_DERIVD"; |
766 |
766 |
767 (* Uniqueness *) |
767 (* Uniqueness *) |
768 Goalw [deriv_def] |
768 Goalw [deriv_def] |
769 "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"; |
769 "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"; |
770 by (blast_tac (claset() addIs [LIM_unique]) 1); |
770 by (blast_tac (claset() addIs [LIM_unique]) 1); |
771 qed "DERIV_unique"; |
771 qed "DERIV_unique"; |
772 |
772 |
773 Goalw [nsderiv_def] |
773 Goalw [nsderiv_def] |
774 "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"; |
774 "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"; |
775 by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1); |
775 by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1); |
776 by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec] |
776 by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec] |
777 addSIs [inj_hypreal_of_real RS injD] |
777 addSIs [inj_hypreal_of_real RS injD] |
778 addDs [approx_trans3], |
778 addDs [approx_trans3], |
779 simpset())); |
779 simpset())); |
780 qed "NSDeriv_unique"; |
780 qed "NSDeriv_unique"; |
781 |
781 |
782 (*------------------------------------------------------------------------ |
782 (*------------------------------------------------------------------------ |
783 Differentiable |
783 Differentiable |
784 ------------------------------------------------------------------------*) |
784 ------------------------------------------------------------------------*) |
785 |
785 |
786 Goalw [differentiable_def] |
786 Goalw [differentiable_def] |
787 "f differentiable x ==> \\<exists>D. DERIV f x :> D"; |
787 "f differentiable x ==> \\<exists>D. DERIV f x :> D"; |
788 by (assume_tac 1); |
788 by (assume_tac 1); |
789 qed "differentiableD"; |
789 qed "differentiableD"; |
790 |
790 |
791 Goalw [differentiable_def] |
791 Goalw [differentiable_def] |
792 "DERIV f x :> D ==> f differentiable x"; |
792 "DERIV f x :> D ==> f differentiable x"; |
793 by (Blast_tac 1); |
793 by (Blast_tac 1); |
794 qed "differentiableI"; |
794 qed "differentiableI"; |
795 |
795 |
796 Goalw [NSdifferentiable_def] |
796 Goalw [NSdifferentiable_def] |
797 "f NSdifferentiable x ==> \\<exists>D. NSDERIV f x :> D"; |
797 "f NSdifferentiable x ==> \\<exists>D. NSDERIV f x :> D"; |
798 by (assume_tac 1); |
798 by (assume_tac 1); |
799 qed "NSdifferentiableD"; |
799 qed "NSdifferentiableD"; |
800 |
800 |
801 Goalw [NSdifferentiable_def] |
801 Goalw [NSdifferentiable_def] |
802 "NSDERIV f x :> D ==> f NSdifferentiable x"; |
802 "NSDERIV f x :> D ==> f NSdifferentiable x"; |
803 by (Blast_tac 1); |
803 by (Blast_tac 1); |
804 qed "NSdifferentiableI"; |
804 qed "NSdifferentiableI"; |
805 |
805 |
806 (*-------------------------------------------------------- |
806 (*-------------------------------------------------------- |
807 Alternative definition for differentiability |
807 Alternative definition for differentiability |
808 -------------------------------------------------------*) |
808 -------------------------------------------------------*) |
809 |
809 |
810 Goalw [LIM_def] |
810 Goalw [LIM_def] |
811 "((%h. (f(a + h) + - f(a))/h) -- 0 --> D) = \ |
811 "((%h. (f(a + h) + - f(a))/h) -- 0 --> D) = \ |
812 \ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)"; |
812 \ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)"; |
813 by Safe_tac; |
813 by Safe_tac; |
814 by (ALLGOALS(dtac spec)); |
814 by (ALLGOALS(dtac spec)); |
815 by Safe_tac; |
815 by Safe_tac; |
910 Goalw [deriv_def] "(NSDERIV f x :> D) = (DERIV f x :> D)"; |
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); |
911 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,LIM_NSLIM_iff]) 1); |
912 qed "NSDERIV_DERIV_iff"; |
912 qed "NSDERIV_DERIV_iff"; |
913 |
913 |
914 (*--------------------------------------------------- |
914 (*--------------------------------------------------- |
915 Differentiability implies continuity |
915 Differentiability implies continuity |
916 nice and simple "algebraic" proof |
916 nice and simple "algebraic" proof |
917 --------------------------------------------------*) |
917 --------------------------------------------------*) |
918 Goalw [nsderiv_def] |
918 Goalw [nsderiv_def] |
919 "NSDERIV f x :> D ==> isNSCont f x"; |
919 "NSDERIV f x :> D ==> isNSCont f x"; |
920 by (auto_tac (claset(),simpset() addsimps |
920 by (auto_tac (claset(),simpset() addsimps |
921 [isNSCont_NSLIM_iff,NSLIM_def])); |
921 [isNSCont_NSLIM_iff,NSLIM_def])); |
922 by (dtac (approx_minus_iff RS iffD1) 1); |
922 by (dtac (approx_minus_iff RS iffD1) 1); |
923 by (dtac (hypreal_not_eq_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); |
924 by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1); |
925 by (asm_full_simp_tac (simpset() addsimps |
925 by (asm_full_simp_tac (simpset() addsimps |
926 [hypreal_add_assoc RS sym]) 2); |
926 [hypreal_add_assoc RS sym]) 2); |
927 by (auto_tac (claset(),simpset() addsimps |
927 by (auto_tac (claset(),simpset() addsimps |
928 [mem_infmal_iff RS sym,hypreal_add_commute])); |
928 [mem_infmal_iff RS sym,hypreal_add_commute])); |
929 by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1); |
929 by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1); |
930 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite |
930 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite |
931 RS subsetD],simpset() addsimps [hypreal_mult_assoc])); |
931 RS subsetD],simpset() addsimps [hypreal_mult_assoc])); |
932 by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN |
932 by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN |
936 (approx_minus_iff RS iffD2)]) 1); |
936 (approx_minus_iff RS iffD2)]) 1); |
937 qed "NSDERIV_isNSCont"; |
937 qed "NSDERIV_isNSCont"; |
938 |
938 |
939 (* Now Sandard proof *) |
939 (* Now Sandard proof *) |
940 Goal "DERIV f x :> D ==> isCont f x"; |
940 Goal "DERIV f x :> D ==> isCont f x"; |
941 by (asm_full_simp_tac (simpset() addsimps |
941 by (asm_full_simp_tac (simpset() addsimps |
942 [NSDERIV_DERIV_iff RS sym, isNSCont_isCont_iff RS sym, |
942 [NSDERIV_DERIV_iff RS sym, isNSCont_isCont_iff RS sym, |
943 NSDERIV_isNSCont]) 1); |
943 NSDERIV_isNSCont]) 1); |
944 qed "DERIV_isCont"; |
944 qed "DERIV_isCont"; |
945 |
945 |
946 (*---------------------------------------------------------------------------- |
946 (*---------------------------------------------------------------------------- |
947 Differentiation rules for combinations of functions |
947 Differentiation rules for combinations of functions |
948 follow from clear, straightforard, algebraic |
948 follow from clear, straightforard, algebraic |
949 manipulations |
949 manipulations |
950 ----------------------------------------------------------------------------*) |
950 ----------------------------------------------------------------------------*) |
951 (*------------------------- |
951 (*------------------------- |
952 Constant function |
952 Constant function |
953 ------------------------*) |
953 ------------------------*) |
986 NSDERIV_DERIV_iff RS sym]) 1); |
986 NSDERIV_DERIV_iff RS sym]) 1); |
987 qed "DERIV_add"; |
987 qed "DERIV_add"; |
988 |
988 |
989 (*----------------------------------------------------- |
989 (*----------------------------------------------------- |
990 Product of functions - Proof is trivial but tedious |
990 Product of functions - Proof is trivial but tedious |
991 and long due to rearrangement of terms |
991 and long due to rearrangement of terms |
992 ----------------------------------------------------*) |
992 ----------------------------------------------------*) |
993 |
993 |
994 Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"; |
994 Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"; |
995 by (simp_tac (simpset() addsimps [right_distrib]) 1); |
995 by (simp_tac (simpset() addsimps [right_distrib]) 1); |
996 val lemma_nsderiv1 = result(); |
996 qed "lemma_nsderiv1"; |
997 |
997 |
998 Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \ |
998 Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \ |
999 \ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \ |
999 \ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \ |
1000 \ ==> x + y \\<approx> 0"; |
1000 \ ==> x + y \\<approx> 0"; |
1001 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1 |
1001 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1 |
1002 THEN assume_tac 1); |
1002 THEN assume_tac 1); |
1003 by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 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], |
1004 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, HFinite_add], |
1005 simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym])); |
1005 simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym])); |
1006 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
1006 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
1007 val lemma_nsderiv2 = result(); |
1007 qed "lemma_nsderiv2"; |
1008 |
1008 |
1009 |
1009 |
1010 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
1010 Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \ |
1011 \ ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; |
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); |
1012 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1); |
1013 by (REPEAT (Step_tac 1)); |
1013 by (REPEAT (Step_tac 1)); |
1014 by (auto_tac (claset(), |
1014 by (auto_tac (claset(), |
1015 simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1])); |
1015 simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1])); |
1016 by (simp_tac (simpset() addsimps [add_divide_distrib]) 1); |
1016 by (simp_tac (simpset() addsimps [add_divide_distrib]) 1); |
1017 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); |
1017 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); |
1018 by (auto_tac (claset(), |
1018 by (auto_tac (claset(), |
1019 simpset() delsimps [times_divide_eq_right] |
1019 simpset() delsimps [times_divide_eq_right] |
1020 addsimps [times_divide_eq_right RS sym])); |
1020 addsimps [times_divide_eq_right RS sym])); |
1021 by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1); |
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); |
1022 by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4); |
1023 by (auto_tac (claset() addSIs [approx_add_mono1], |
1023 by (auto_tac (claset() addSIs [approx_add_mono1], |
1024 simpset() addsimps [left_distrib, right_distrib, |
1024 simpset() addsimps [left_distrib, right_distrib, |
1025 hypreal_mult_commute, hypreal_add_assoc])); |
1025 hypreal_mult_commute, hypreal_add_assoc])); |
1026 by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")] |
1026 by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")] |
1027 (hypreal_add_commute RS subst) 1); |
1027 (hypreal_add_commute RS subst) 1); |
1028 by (auto_tac (claset() addSIs [Infinitesimal_add_approx_self2 RS approx_sym, |
1028 by (auto_tac (claset() addSIs [Infinitesimal_add_approx_self2 RS approx_sym, |
1029 Infinitesimal_add, Infinitesimal_mult, |
1029 Infinitesimal_add, Infinitesimal_mult, |
1041 (*---------------------------- |
1041 (*---------------------------- |
1042 Multiplying by a constant |
1042 Multiplying by a constant |
1043 ---------------------------*) |
1043 ---------------------------*) |
1044 Goal "NSDERIV f x :> D \ |
1044 Goal "NSDERIV f x :> D \ |
1045 \ ==> NSDERIV (%x. c * f x) x :> c*D"; |
1045 \ ==> NSDERIV (%x. c * f x) x :> c*D"; |
1046 by (asm_full_simp_tac |
1046 by (asm_full_simp_tac |
1047 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
1047 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
1048 minus_mult_right, right_distrib RS sym]) 1); |
1048 minus_mult_right, right_distrib RS sym]) 1); |
1049 by (etac (NSLIM_const RS NSLIM_mult) 1); |
1049 by (etac (NSLIM_const RS NSLIM_mult) 1); |
1050 qed "NSDERIV_cmult"; |
1050 qed "NSDERIV_cmult"; |
1051 |
1051 |
1052 (* let's do the standard proof though theorem *) |
1052 (* let's do the standard proof though theorem *) |
1053 (* LIM_mult2 follows from a NS proof *) |
1053 (* LIM_mult2 follows from a NS proof *) |
1054 |
1054 |
1055 Goalw [deriv_def] |
1055 Goalw [deriv_def] |
1056 "DERIV f x :> D \ |
1056 "DERIV f x :> D \ |
1057 \ ==> DERIV (%x. c * f x) x :> c*D"; |
1057 \ ==> DERIV (%x. c * f x) x :> c*D"; |
1058 by (asm_full_simp_tac |
1058 by (asm_full_simp_tac |
1059 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
1059 (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, |
1060 minus_mult_right, right_distrib RS sym]) 1); |
1060 minus_mult_right, right_distrib RS sym]) 1); |
1061 by (etac (LIM_const RS LIM_mult2) 1); |
1061 by (etac (LIM_const RS LIM_mult2) 1); |
1062 qed "DERIV_cmult"; |
1062 qed "DERIV_cmult"; |
1063 |
1063 |
1137 qed "increment_thm"; |
1137 qed "increment_thm"; |
1138 |
1138 |
1139 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
1139 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
1140 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \ |
1140 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \ |
1141 \ hypreal_of_real(D)*h + e*h"; |
1141 \ hypreal_of_real(D)*h + e*h"; |
1142 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2] |
1142 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2] |
1143 addSIs [increment_thm]) 1); |
1143 addSIs [increment_thm]) 1); |
1144 qed "increment_thm2"; |
1144 qed "increment_thm2"; |
1145 |
1145 |
1146 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
1146 Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \ |
1147 \ ==> increment f x h \\<approx> 0"; |
1147 \ ==> increment f x h \\<approx> 0"; |
1148 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs |
1148 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs |
1149 [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps |
1149 [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps |
1150 [left_distrib RS sym,mem_infmal_iff RS sym])); |
1150 [left_distrib RS sym,mem_infmal_iff RS sym])); |
1151 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
1151 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); |
1152 qed "increment_approx_zero"; |
1152 qed "increment_approx_zero"; |
1153 |
1153 |
1154 (*--------------------------------------------------------------- |
1154 (*--------------------------------------------------------------- |
1155 Similarly to the above, the chain rule admits an entirely |
1155 Similarly to the above, the chain rule admits an entirely |
1156 straightforward derivation. Compare this with Harrison's |
1156 straightforward derivation. Compare this with Harrison's |
1157 HOL proof of the chain rule, which proved to be trickier and |
1157 HOL proof of the chain rule, which proved to be trickier and |
1158 required an alternative characterisation of differentiability- |
1158 required an alternative characterisation of differentiability- |
1159 the so-called Carathedory derivative. Our main problem is |
1159 the so-called Carathedory derivative. Our main problem is |
1160 manipulation of terms. |
1160 manipulation of terms. |
1161 --------------------------------------------------------------*) |
1161 --------------------------------------------------------------*) |
1162 |
1162 |
1163 (* lemmas *) |
1163 (* lemmas *) |
1164 Goalw [nsderiv_def] |
1164 Goalw [nsderiv_def] |
1165 "[| NSDERIV g x :> D; \ |
1165 "[| NSDERIV g x :> D; \ |
1166 \ ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ |
1166 \ ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ |
1167 \ xa \\<in> Infinitesimal;\ |
1167 \ xa \\<in> Infinitesimal;\ |
1168 \ xa \\<noteq> 0 \ |
1168 \ xa \\<noteq> 0 \ |
1169 \ |] ==> D = 0"; |
1169 \ |] ==> D = 0"; |
1170 by (dtac bspec 1); |
1170 by (dtac bspec 1); |
1171 by Auto_tac; |
1171 by Auto_tac; |
1172 qed "NSDERIV_zero"; |
1172 qed "NSDERIV_zero"; |
1173 |
1173 |
1174 (* can be proved differently using NSLIM_isCont_iff *) |
1174 (* can be proved differently using NSLIM_isCont_iff *) |
1175 Goalw [nsderiv_def] |
1175 Goalw [nsderiv_def] |
1176 "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \ |
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"; |
1177 \ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0"; |
1178 by (asm_full_simp_tac (simpset() addsimps |
1178 by (asm_full_simp_tac (simpset() addsimps |
1179 [mem_infmal_iff RS sym]) 1); |
1179 [mem_infmal_iff RS sym]) 1); |
1180 by (rtac Infinitesimal_ratio 1); |
1180 by (rtac Infinitesimal_ratio 1); |
1181 by (rtac approx_hypreal_of_real_HFinite 3); |
1181 by (rtac approx_hypreal_of_real_HFinite 3); |
1182 by Auto_tac; |
1182 by Auto_tac; |
1183 qed "NSDERIV_approx"; |
1183 qed "NSDERIV_approx"; |
1184 |
1184 |
1185 (*--------------------------------------------------------------- |
1185 (*--------------------------------------------------------------- |
1186 from one version of differentiability |
1186 from one version of differentiability |
1187 |
1187 |
1188 f(x) - f(a) |
1188 f(x) - f(a) |
1189 --------------- \\<approx> Db |
1189 --------------- \\<approx> Db |
1190 x - a |
1190 x - a |
1191 ---------------------------------------------------------------*) |
1191 ---------------------------------------------------------------*) |
1192 Goal "[| NSDERIV f (g x) :> Da; \ |
1192 Goal "[| NSDERIV f (g x) :> Da; \ |
1198 \ \\<approx> hypreal_of_real(Da)"; |
1198 \ \\<approx> hypreal_of_real(Da)"; |
1199 by (auto_tac (claset(), |
1199 by (auto_tac (claset(), |
1200 simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); |
1200 simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); |
1201 qed "NSDERIVD1"; |
1201 qed "NSDERIVD1"; |
1202 |
1202 |
1203 (*-------------------------------------------------------------- |
1203 (*-------------------------------------------------------------- |
1204 from other version of differentiability |
1204 from other version of differentiability |
1205 |
1205 |
1206 f(x + h) - f(x) |
1206 f(x + h) - f(x) |
1207 ----------------- \\<approx> Db |
1207 ----------------- \\<approx> Db |
1208 h |
1208 h |
1209 --------------------------------------------------------------*) |
1209 --------------------------------------------------------------*) |
1210 Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> 0 |] \ |
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 \ |
1211 \ ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \ |
1212 \ \\<approx> hypreal_of_real(Db)"; |
1212 \ \\<approx> hypreal_of_real(Db)"; |
1213 by (auto_tac (claset(), |
1213 by (auto_tac (claset(), |
1214 simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, |
1214 simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, |
1215 mem_infmal_iff, starfun_lambda_cancel])); |
1215 mem_infmal_iff, starfun_lambda_cancel])); |
1216 qed "NSDERIVD2"; |
1216 qed "NSDERIVD2"; |
1217 |
1217 |
1218 Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"; |
1218 Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"; |
1219 by Auto_tac; |
1219 by Auto_tac; |
1220 qed "lemma_chain"; |
1220 qed "lemma_chain"; |
1221 |
1221 |
1222 (*------------------------------------------------------ |
1222 (*------------------------------------------------------ |
1223 This proof uses both definitions of differentiability. |
1223 This proof uses both definitions of differentiability. |
1224 ------------------------------------------------------*) |
1224 ------------------------------------------------------*) |
1285 Addsimps [NSDERIV_cmult_Id]; |
1285 Addsimps [NSDERIV_cmult_Id]; |
1286 |
1286 |
1287 Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"; |
1287 Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"; |
1288 by (induct_tac "n" 1); |
1288 by (induct_tac "n" 1); |
1289 by (dtac (DERIV_Id RS DERIV_mult) 2); |
1289 by (dtac (DERIV_Id RS DERIV_mult) 2); |
1290 by (auto_tac (claset(), |
1290 by (auto_tac (claset(), |
1291 simpset() addsimps [real_of_nat_Suc, left_distrib])); |
1291 simpset() addsimps [real_of_nat_Suc, left_distrib])); |
1292 by (case_tac "0 < n" 1); |
1292 by (case_tac "0 < n" 1); |
1293 by (dres_inst_tac [("x","x")] realpow_minus_mult 1); |
1293 by (dres_inst_tac [("x","x")] realpow_minus_mult 1); |
1294 by (auto_tac (claset(), |
1294 by (auto_tac (claset(), |
1295 simpset() addsimps [real_mult_assoc, real_add_commute])); |
1295 simpset() addsimps [real_mult_assoc, real_add_commute])); |
1296 qed "DERIV_pow"; |
1296 qed "DERIV_pow"; |
1297 |
1297 |
1298 (* NS version *) |
1298 (* NS version *) |
1299 Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"; |
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); |
1300 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1); |
1301 qed "NSDERIV_pow"; |
1301 qed "NSDERIV_pow"; |
1302 |
1302 |
1303 (*--------------------------------------------------------------- |
1303 (*--------------------------------------------------------------- |
1304 Power of -1 |
1304 Power of -1 |
1305 ---------------------------------------------------------------*) |
1305 ---------------------------------------------------------------*) |
1306 |
1306 |
1307 (*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*) |
1307 (*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*) |
1308 Goalw [nsderiv_def] |
1308 Goalw [nsderiv_def] |
1309 "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"; |
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); |
1310 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
1311 by (ftac Infinitesimal_add_not_zero 1); |
1311 by (ftac Infinitesimal_add_not_zero 1); |
1312 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); |
1312 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); |
1313 by (auto_tac (claset(), |
1313 by (auto_tac (claset(), |
1314 simpset() addsimps [starfun_inverse_inverse, realpow_two] |
1314 simpset() addsimps [starfun_inverse_inverse, realpow_two] |
1315 delsimps [minus_mult_left RS sym, |
1315 delsimps [minus_mult_left RS sym, |
1316 minus_mult_right RS sym])); |
1316 minus_mult_right RS sym])); |
1317 by (asm_full_simp_tac |
1317 by (asm_full_simp_tac |
1318 (simpset() addsimps [hypreal_inverse_add, |
1318 (simpset() addsimps [hypreal_inverse_add, |
1319 hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] |
1319 hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] |
1320 @ add_ac @ mult_ac |
1320 @ add_ac @ mult_ac |
1321 delsimps [inverse_mult_distrib,inverse_minus_eq, |
1321 delsimps [inverse_mult_distrib,inverse_minus_eq, |
1322 minus_mult_left RS sym, |
1322 minus_mult_left RS sym, |
1323 minus_mult_right RS sym] ) 1); |
1323 minus_mult_right RS sym] ) 1); |
1324 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym, |
1324 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym, |
1325 right_distrib] |
1325 right_distrib] |
1326 delsimps [minus_mult_left RS sym, |
1326 delsimps [minus_mult_left RS sym, |
1327 minus_mult_right RS sym]) 1); |
1327 minus_mult_right RS sym]) 1); |
1328 by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] |
1328 by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] |
1329 approx_trans 1); |
1329 approx_trans 1); |
1330 by (rtac inverse_add_Infinitesimal_approx2 1); |
1330 by (rtac inverse_add_Infinitesimal_approx2 1); |
1331 by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal], |
1331 by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal], |
1332 simpset() addsimps [hypreal_minus_inverse RS sym, |
1332 simpset() addsimps [hypreal_minus_inverse RS sym, |
1333 HFinite_minus_iff])); |
1333 HFinite_minus_iff])); |
1334 by (rtac Infinitesimal_HFinite_mult2 1); |
1334 by (rtac Infinitesimal_HFinite_mult2 1); |
1335 by Auto_tac; |
1335 by Auto_tac; |
1336 qed "NSDERIV_inverse"; |
1336 qed "NSDERIV_inverse"; |
1337 |
1337 |
1338 |
1338 |
1339 Goal "x \\<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"; |
1339 Goal "x \\<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"; |
1340 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse, |
1340 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse, |
1341 NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1); |
1341 NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1); |
1342 qed "DERIV_inverse"; |
1342 qed "DERIV_inverse"; |
1343 |
1343 |
1344 (*-------------------------------------------------------------- |
1344 (*-------------------------------------------------------------- |
1345 Derivative of inverse |
1345 Derivative of inverse |
1346 -------------------------------------------------------------*) |
1346 -------------------------------------------------------------*) |
1347 Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \ |
1347 Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \ |
1348 \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; |
1348 \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; |
1349 by (rtac (real_mult_commute RS subst) 1); |
1349 by (rtac (real_mult_commute RS subst) 1); |
1350 by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1); |
1350 by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1); |
1357 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
1357 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
1358 DERIV_inverse_fun] delsimps [realpow_Suc]) 1); |
1358 DERIV_inverse_fun] delsimps [realpow_Suc]) 1); |
1359 qed "NSDERIV_inverse_fun"; |
1359 qed "NSDERIV_inverse_fun"; |
1360 |
1360 |
1361 (*-------------------------------------------------------------- |
1361 (*-------------------------------------------------------------- |
1362 Derivative of quotient |
1362 Derivative of quotient |
1363 -------------------------------------------------------------*) |
1363 -------------------------------------------------------------*) |
1364 Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \ |
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))"; |
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); |
1366 by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1); |
1367 by (dtac DERIV_mult 2); |
1367 by (dtac DERIV_mult 2); |
1368 by (REPEAT(assume_tac 1)); |
1368 by (REPEAT(assume_tac 1)); |
1369 by (asm_full_simp_tac |
1369 by (asm_full_simp_tac |
1370 (simpset() addsimps [real_divide_def, right_distrib, |
1370 (simpset() addsimps [real_divide_def, right_distrib, |
1371 power_inverse,minus_mult_left] @ mult_ac |
1371 power_inverse,minus_mult_left] @ mult_ac |
1372 delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); |
1372 delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); |
1373 qed "DERIV_quotient"; |
1373 qed "DERIV_quotient"; |
1374 |
1374 |
1375 Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \ |
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) \ |
1376 \ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \ |
1377 \ + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"; |
1377 \ + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"; |
1378 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
1378 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, |
1379 DERIV_quotient] delsimps [realpow_Suc]) 1); |
1379 DERIV_quotient] delsimps [realpow_Suc]) 1); |
1380 qed "NSDERIV_quotient"; |
1380 qed "NSDERIV_quotient"; |
1381 |
1381 |
1382 (* ------------------------------------------------------------------------ *) |
1382 (* ------------------------------------------------------------------------ *) |
1383 (* Caratheodory formulation of derivative at a point: standard proof *) |
1383 (* Caratheodory formulation of derivative at a point: standard proof *) |
1384 (* ------------------------------------------------------------------------ *) |
1384 (* ------------------------------------------------------------------------ *) |
1385 |
1385 |
1386 Goal "(DERIV f x :> l) = \ |
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)"; |
1387 \ (\\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isCont g x & g x = l)"; |
1388 by Safe_tac; |
1388 by Safe_tac; |
1389 by (res_inst_tac |
1389 by (res_inst_tac |
1390 [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1); |
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, |
1391 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc, |
1392 ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (0::real)"])); |
1392 ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (0::real)"])); |
1393 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff])); |
1393 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff])); |
1394 by (ALLGOALS(rtac (LIM_equal RS iffD1))); |
1394 by (ALLGOALS(rtac (LIM_equal RS iffD1))); |
1402 qed "CARAT_NSDERIV"; |
1402 qed "CARAT_NSDERIV"; |
1403 |
1403 |
1404 (* How about a NS proof? *) |
1404 (* How about a NS proof? *) |
1405 Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \ |
1405 Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \ |
1406 \ ==> NSDERIV f x :> l"; |
1406 \ ==> NSDERIV f x :> l"; |
1407 by (auto_tac (claset(), |
1407 by (auto_tac (claset(), |
1408 simpset() delsimprocs field_cancel_factor |
1408 simpset() delsimprocs field_cancel_factor |
1409 addsimps [NSDERIV_iff2])); |
1409 addsimps [NSDERIV_iff2])); |
1410 by (auto_tac (claset(), |
1410 by (auto_tac (claset(), |
1411 simpset() addsimps [hypreal_mult_assoc])); |
1411 simpset() addsimps [hypreal_mult_assoc])); |
1412 by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym, |
1412 by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym, |
1413 hypreal_diff_def]) 1); |
1413 hypreal_diff_def]) 1); |
1414 by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1); |
1414 by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1); |
1415 qed "CARAT_DERIVD"; |
1415 qed "CARAT_DERIVD"; |
1416 |
1416 |
1417 |
1417 |
1418 |
1418 |
1419 (*--------------------------------------------------------------------------*) |
1419 (*--------------------------------------------------------------------------*) |
1420 (* Lemmas about nested intervals and proof by bisection (cf.Harrison) *) |
1420 (* Lemmas about nested intervals and proof by bisection (cf.Harrison) *) |
1421 (* All considerably tidied by lcp *) |
1421 (* All considerably tidied by lcp *) |
1441 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1441 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1442 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1442 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1443 \ \\<forall>n. f(n) \\<le> g(n) |] \ |
1443 \ \\<forall>n. f(n) \\<le> g(n) |] \ |
1444 \ ==> Bseq g"; |
1444 \ ==> Bseq g"; |
1445 by (stac (Bseq_minus_iff RS sym) 1); |
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); |
1446 by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1); |
1447 by Auto_tac; |
1447 by Auto_tac; |
1448 qed "f_inc_g_dec_Beq_g"; |
1448 qed "f_inc_g_dec_Beq_g"; |
1449 |
1449 |
1450 Goal "[| \\<forall>n. f n \\<le> f (Suc n); convergent f |] ==> f n \\<le> lim f"; |
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); |
1451 by (rtac (linorder_not_less RS iffD1) 1); |
1452 by (auto_tac (claset(), |
1452 by (auto_tac (claset(), |
1453 simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc])); |
1453 simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc])); |
1454 by (dtac real_less_sum_gt_zero 1); |
1454 by (dtac real_less_sum_gt_zero 1); |
1455 by (dres_inst_tac [("x","f n + - lim f")] spec 1); |
1455 by (dres_inst_tac [("x","f n + - lim f")] spec 1); |
1456 by Safe_tac; |
1456 by Safe_tac; |
1457 by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 1); |
1457 by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 1); |
1458 by Auto_tac; |
1458 by Auto_tac; |
1459 by (subgoal_tac "lim f \\<le> f(no + n)" 1); |
1459 by (subgoal_tac "lim f \\<le> f(no + n)" 1); |
1460 by (induct_tac "no" 2); |
1460 by (induct_tac "no" 2); |
1461 by (auto_tac (claset() addIs [order_trans], |
1461 by (auto_tac (claset() addIs [order_trans], |
1462 simpset() addsimps [real_diff_def, real_abs_def])); |
1462 simpset() addsimps [real_diff_def, real_abs_def])); |
1463 by (dres_inst_tac [("x","f(no + n)"),("no1","no")] |
1463 by (dres_inst_tac [("x","f(no + n)"),("no1","no")] |
1464 (lemma_f_mono_add RSN (2,order_less_le_trans)) 1); |
1464 (lemma_f_mono_add RSN (2,order_less_le_trans)) 1); |
1465 by (auto_tac (claset(), simpset() addsimps [add_commute])); |
1465 by (auto_tac (claset(), simpset() addsimps [add_commute])); |
1466 qed "f_inc_imp_le_lim"; |
1466 qed "f_inc_imp_le_lim"; |
1467 |
1467 |
1468 Goal "convergent g ==> lim (%x. - g x) = - (lim g)"; |
1468 Goal "convergent g ==> lim (%x. - g x) = - (lim g)"; |
1469 by (rtac (LIMSEQ_minus RS limI) 1); |
1469 by (rtac (LIMSEQ_minus RS limI) 1); |
1470 by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1); |
1470 by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1); |
1471 qed "lim_uminus"; |
1471 qed "lim_uminus"; |
1472 |
1472 |
1473 Goal "[| \\<forall>n. g(Suc n) \\<le> g(n); convergent g |] ==> lim g \\<le> g n"; |
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); |
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); |
1475 by (cut_inst_tac [("f", "%x. - (g x)")] f_inc_imp_le_lim 2); |
1476 by (auto_tac (claset(), |
1476 by (auto_tac (claset(), |
1477 simpset() addsimps [lim_uminus, convergent_minus_iff RS sym])); |
1477 simpset() addsimps [lim_uminus, convergent_minus_iff RS sym])); |
1478 qed "g_dec_imp_lim_le"; |
1478 qed "g_dec_imp_lim_le"; |
1479 |
1479 |
1480 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1480 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1481 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1481 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1482 \ \\<forall>n. f(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) & \ |
1483 \ ==> \\<exists>l m. l \\<le> m & ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \ |
1484 \ ((\\<forall>n. m \\<le> g(n)) & g ----> m)"; |
1484 \ ((\\<forall>n. m \\<le> g(n)) & g ----> m)"; |
1485 by (subgoal_tac "monoseq f & monoseq g" 1); |
1485 by (subgoal_tac "monoseq f & monoseq g" 1); |
1486 by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2); |
1486 by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2); |
1487 by (subgoal_tac "Bseq f & Bseq g" 1); |
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); |
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], |
1489 by (auto_tac (claset() addSDs [Bseq_monoseq_convergent], |
1490 simpset() addsimps [convergent_LIMSEQ_iff])); |
1490 simpset() addsimps [convergent_LIMSEQ_iff])); |
1491 by (res_inst_tac [("x","lim f")] exI 1); |
1491 by (res_inst_tac [("x","lim f")] exI 1); |
1492 by (res_inst_tac [("x","lim g")] exI 1); |
1492 by (res_inst_tac [("x","lim g")] exI 1); |
1493 by (auto_tac (claset() addIs [LIMSEQ_le], simpset())); |
1493 by (auto_tac (claset() addIs [LIMSEQ_le], simpset())); |
1494 by (auto_tac (claset(), |
1494 by (auto_tac (claset(), |
1495 simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le, |
1495 simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le, |
1496 convergent_LIMSEQ_iff])); |
1496 convergent_LIMSEQ_iff])); |
1497 qed "lemma_nest"; |
1497 qed "lemma_nest"; |
1498 |
1498 |
1499 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1499 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \ |
1500 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1500 \ \\<forall>n. g(Suc n) \\<le> g(n); \ |
1501 \ \\<forall>n. f(n) \\<le> g(n); \ |
1501 \ \\<forall>n. f(n) \\<le> g(n); \ |
1511 |
1511 |
1512 Goal "a \\<le> b ==> \ |
1512 Goal "a \\<le> b ==> \ |
1513 \ \\<forall>n. fst (Bolzano_bisect P a b n) \\<le> snd (Bolzano_bisect P a b n)"; |
1513 \ \\<forall>n. fst (Bolzano_bisect P a b n) \\<le> snd (Bolzano_bisect P a b n)"; |
1514 by (rtac allI 1); |
1514 by (rtac allI 1); |
1515 by (induct_tac "n" 1); |
1515 by (induct_tac "n" 1); |
1516 by (auto_tac (claset(), simpset() addsimps [Let_def, split_def])); |
1516 by (auto_tac (claset(), simpset() addsimps [Let_def, split_def])); |
1517 qed "Bolzano_bisect_le"; |
1517 qed "Bolzano_bisect_le"; |
1518 |
1518 |
1519 Goal "a \\<le> b ==> \ |
1519 Goal "a \\<le> b ==> \ |
1520 \ \\<forall>n. fst(Bolzano_bisect P a b n) \\<le> fst (Bolzano_bisect P a b (Suc n))"; |
1520 \ \\<forall>n. fst(Bolzano_bisect P a b n) \\<le> fst (Bolzano_bisect P a b (Suc n))"; |
1521 by (rtac allI 1); |
1521 by (rtac allI 1); |
1522 by (induct_tac "n" 1); |
1522 by (induct_tac "n" 1); |
1523 by (auto_tac (claset(), |
1523 by (auto_tac (claset(), |
1524 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1524 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1525 qed "Bolzano_bisect_fst_le_Suc"; |
1525 qed "Bolzano_bisect_fst_le_Suc"; |
1526 |
1526 |
1527 Goal "a \\<le> b ==> \ |
1527 Goal "a \\<le> b ==> \ |
1528 \ \\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \\<le> snd (Bolzano_bisect P a b n)"; |
1528 \ \\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \\<le> snd (Bolzano_bisect P a b n)"; |
1529 by (rtac allI 1); |
1529 by (rtac allI 1); |
1530 by (induct_tac "n" 1); |
1530 by (induct_tac "n" 1); |
1531 by (auto_tac (claset(), |
1531 by (auto_tac (claset(), |
1532 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1532 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1533 qed "Bolzano_bisect_Suc_le_snd"; |
1533 qed "Bolzano_bisect_Suc_le_snd"; |
1534 |
1534 |
1535 Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)"; |
1535 Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)"; |
1536 by Auto_tac; |
1536 by Auto_tac; |
1537 by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1); |
1537 by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1); |
1538 by Auto_tac; |
1538 by Auto_tac; |
1539 qed "eq_divide_2_times_iff"; |
1539 qed "eq_divide_2_times_iff"; |
1540 |
1540 |
1541 Goal "a \\<le> b ==> \ |
1541 Goal "a \\<le> b ==> \ |
1542 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \ |
1542 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \ |
1543 \ (b-a) / (2 ^ n)"; |
1543 \ (b-a) / (2 ^ n)"; |
1544 by (induct_tac "n" 1); |
1544 by (induct_tac "n" 1); |
1545 by (auto_tac (claset(), |
1545 by (auto_tac (claset(), |
1546 simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib, |
1546 simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib, |
1547 Let_def, split_def])); |
1547 Let_def, split_def])); |
1548 by (auto_tac (claset(), |
1548 by (auto_tac (claset(), |
1549 simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def]))); |
1549 simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def]))); |
1550 qed "Bolzano_bisect_diff"; |
1550 qed "Bolzano_bisect_diff"; |
1551 |
1551 |
1552 val Bolzano_nest_unique = |
1552 val Bolzano_nest_unique = |
1553 [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le] |
1553 [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le] |
1554 MRS lemma_nest_unique; |
1554 MRS lemma_nest_unique; |
1555 |
1555 |
1556 (*P_prem is a looping simprule, so it works better if it isn't an assumption*) |
1556 (*P_prem is a looping simprule, so it works better if it isn't an assumption*) |
1557 val P_prem::notP_prem::rest = |
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); \ |
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 |] ==> \ |
1559 \ ~ P(a,b); a \\<le> b |] ==> \ |
1560 \ ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"; |
1560 \ ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"; |
1561 by (cut_facts_tac rest 1); |
1561 by (cut_facts_tac rest 1); |
1562 by (induct_tac "n" 1); |
1562 by (induct_tac "n" 1); |
1563 by (auto_tac (claset(), |
1563 by (auto_tac (claset(), |
1564 simpset() delsimps [surjective_pairing RS sym] |
1564 simpset() delsimps [surjective_pairing RS sym] |
1565 addsimps [notP_prem, Let_def, split_def])); |
1565 addsimps [notP_prem, Let_def, split_def])); |
1566 by (swap_res_tac [P_prem] 1); |
1566 by (swap_res_tac [P_prem] 1); |
1567 by (assume_tac 1); |
1567 by (assume_tac 1); |
1568 by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le])); |
1568 by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le])); |
1569 qed "not_P_Bolzano_bisect"; |
1569 qed "not_P_Bolzano_bisect"; |
1570 |
1570 |
1571 (*Now we re-package P_prem as a formula*) |
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); \ |
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 |] ==> \ |
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))"; |
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); |
1575 by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1); |
1576 qed "not_P_Bolzano_bisect'"; |
1576 qed "not_P_Bolzano_bisect'"; |
1577 |
1577 |
1578 |
1578 |
1579 Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \ |
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 & \ |
1580 \ \\<forall>x. \\<exists>d::real. 0 < d & \ |
1601 by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1); |
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); |
1602 by (dres_inst_tac [("x","snd(Bolzano_bisect P a b (no + noa))")] spec 1); |
1603 by Safe_tac; |
1603 by Safe_tac; |
1604 by (ALLGOALS Asm_simp_tac); |
1604 by (ALLGOALS Asm_simp_tac); |
1605 by (res_inst_tac [("y","abs(fst(Bolzano_bisect P a b(no + noa)) - l) + \ |
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)")] |
1606 \ abs(snd(Bolzano_bisect P a b(no + noa)) - l)")] |
1607 order_le_less_trans 1); |
1607 order_le_less_trans 1); |
1608 by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1); |
1608 by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1); |
1609 by (rtac (real_sum_of_halves RS subst) 1); |
1609 by (rtac (real_sum_of_halves RS subst) 1); |
1610 by (rtac add_strict_mono 1); |
1610 by (rtac add_strict_mono 1); |
1611 by (ALLGOALS |
1611 by (ALLGOALS |
1612 (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def]))); |
1612 (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def]))); |
1613 qed "lemma_BOLZANO"; |
1613 qed "lemma_BOLZANO"; |
1614 |
1614 |
1615 |
1615 |
1616 Goal "((\\<forall>a b c. (a \\<le> b & b \\<le> c & P(a,b) & P(b,c)) --> P(a,c)) & \ |
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 & \ |
1617 \ (\\<forall>x. \\<exists>d::real. 0 < d & \ |
1618 \ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \ |
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))"; |
1619 \ --> (\\<forall>a b. a \\<le> b --> P(a,b))"; |
1620 by (Clarify_tac 1); |
1620 by (Clarify_tac 1); |
1621 by (blast_tac (claset() addIs [lemma_BOLZANO]) 1); |
1621 by (blast_tac (claset() addIs [lemma_BOLZANO]) 1); |
1622 qed "lemma_BOLZANO2"; |
1622 qed "lemma_BOLZANO2"; |
1623 |
1623 |
1624 |
1624 |
1625 (*----------------------------------------------------------------------------*) |
1625 (*----------------------------------------------------------------------------*) |
1626 (* Intermediate Value Theorem (prove contrapositive by bisection) *) |
1626 (* Intermediate Value Theorem (prove contrapositive by bisection) *) |
1698 by (auto_tac (claset() addIs [abs_eqI1], simpset())); |
1698 by (auto_tac (claset() addIs [abs_eqI1], simpset())); |
1699 qed "abs_real_of_nat_cancel"; |
1699 qed "abs_real_of_nat_cancel"; |
1700 Addsimps [abs_real_of_nat_cancel]; |
1700 Addsimps [abs_real_of_nat_cancel]; |
1701 |
1701 |
1702 Goal "~ abs(x) + (1::real) < x"; |
1702 Goal "~ abs(x) + (1::real) < x"; |
1703 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); |
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())); |
1704 by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset())); |
1705 qed "abs_add_one_not_less_self"; |
1705 qed "abs_add_one_not_less_self"; |
1706 Addsimps [abs_add_one_not_less_self]; |
1706 Addsimps [abs_add_one_not_less_self]; |
1707 |
1707 |
1708 |
1708 |
1709 Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |]\ |
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"; |
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 --> \ |
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)")] |
1712 \ (\\<exists>M. \\<forall>x. u \\<le> x & x \\<le> v --> f x \\<le> M)")] |
1713 lemma_BOLZANO2 1); |
1713 lemma_BOLZANO2 1); |
1714 by Safe_tac; |
1714 by Safe_tac; |
1715 by (ALLGOALS Asm_full_simp_tac); |
1715 by (ALLGOALS Asm_full_simp_tac); |
1716 by (rename_tac "x xa ya M Ma" 1); |
1716 by (rename_tac "x xa ya M Ma" 1); |
1717 by (cut_inst_tac [("x","M"),("y","Ma")] linorder_linear 1); |
1717 by (cut_inst_tac [("x","M"),("y","Ma")] linorder_linear 1); |
1718 by Safe_tac; |
1718 by Safe_tac; |
1719 by (res_inst_tac [("x","Ma")] exI 1); |
1719 by (res_inst_tac [("x","Ma")] exI 1); |
1720 by (Clarify_tac 1); |
1720 by (Clarify_tac 1); |
1721 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
1721 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
1722 by (Force_tac 1); |
1722 by (Force_tac 1); |
1723 by (res_inst_tac [("x","M")] exI 1); |
1723 by (res_inst_tac [("x","M")] exI 1); |
1724 by (Clarify_tac 1); |
1724 by (Clarify_tac 1); |
1725 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
1725 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1); |
1726 by (Force_tac 1); |
1726 by (Force_tac 1); |
1727 by (case_tac "a \\<le> x & x \\<le> b" 1); |
1727 by (case_tac "a \\<le> x & x \\<le> b" 1); |
1728 by (res_inst_tac [("x","1")] exI 2); |
1728 by (res_inst_tac [("x","1")] exI 2); |
1729 by (Force_tac 2); |
1729 by (Force_tac 2); |
1730 by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1); |
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); |
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); |
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); |
1733 by (dres_inst_tac [("x","1")] spec 1); |
1734 by Auto_tac; |
1734 by Auto_tac; |
1735 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1); |
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); |
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); |
1737 by (dres_inst_tac [("x","xa - x")] spec 1); |
1738 by (auto_tac (claset(), simpset() addsimps [abs_ge_self])); |
1738 by (auto_tac (claset(), simpset() addsimps [abs_ge_self])); |
1739 by (REPEAT (arith_tac 1)); |
1739 by (REPEAT (arith_tac 1)); |
1771 \ ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M) & \ |
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)"; |
1772 \ (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = M)"; |
1773 by (ftac isCont_has_Ub 1 THEN assume_tac 1); |
1773 by (ftac isCont_has_Ub 1 THEN assume_tac 1); |
1774 by (Clarify_tac 1); |
1774 by (Clarify_tac 1); |
1775 by (res_inst_tac [("x","M")] exI 1); |
1775 by (res_inst_tac [("x","M")] exI 1); |
1776 by (Asm_full_simp_tac 1); |
1776 by (Asm_full_simp_tac 1); |
1777 by (rtac ccontr 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); |
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); |
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); |
1780 by (dres_inst_tac [("z","M")] real_le_anti_sym 2); |
1781 by (REPEAT(Blast_tac 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); |
1782 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. inverse(M - f x)) x" 1); |
1783 by Safe_tac; |
1783 by Safe_tac; |
1784 by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]); |
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]))); |
1785 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [diff_eq_eq]))); |
1786 by (Blast_tac 2); |
1786 by (Blast_tac 2); |
1787 by (subgoal_tac |
1787 by (subgoal_tac |
1788 "\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1); |
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); |
1789 by (rtac isCont_bounded 2); |
1790 by Safe_tac; |
1790 by Safe_tac; |
1791 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> 0 < inverse(M - f(x))" 1); |
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); |
1792 by (Asm_full_simp_tac 1); |
1793 by Safe_tac; |
1793 by Safe_tac; |
1794 by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2); |
1794 by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2); |
1795 by (subgoal_tac |
1795 by (subgoal_tac |
1796 "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1); |
1796 "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1); |
1797 by Safe_tac; |
1797 by Safe_tac; |
1798 by (res_inst_tac [("y","k")] order_le_less_trans 2); |
1798 by (res_inst_tac [("y","k")] order_le_less_trans 2); |
1799 by (asm_full_simp_tac (simpset() addsimps [zero_less_one]) 3); |
1799 by (asm_full_simp_tac (simpset() addsimps [zero_less_one]) 3); |
1800 by (Asm_full_simp_tac 2); |
1800 by (Asm_full_simp_tac 2); |
1801 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \ |
1801 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \ |
1802 \ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1); |
1802 \ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1); |
1803 by Safe_tac; |
1803 by Safe_tac; |
1804 by (rtac less_imp_inverse_less 2); |
1804 by (rtac less_imp_inverse_less 2); |
1805 by (ALLGOALS Asm_full_simp_tac); |
1805 by (ALLGOALS Asm_full_simp_tac); |
1807 ("x","M - inverse(k + 1)")] spec 1); |
1807 ("x","M - inverse(k + 1)")] spec 1); |
1808 by (Step_tac 1 THEN dtac (linorder_not_less RS iffD1) 1); |
1808 by (Step_tac 1 THEN dtac (linorder_not_less RS iffD1) 1); |
1809 by (dtac (le_diff_eq RS iffD1) 1); |
1809 by (dtac (le_diff_eq RS iffD1) 1); |
1810 by (REPEAT(dres_inst_tac [("x","a")] spec 1)); |
1810 by (REPEAT(dres_inst_tac [("x","a")] spec 1)); |
1811 by (Asm_full_simp_tac 1); |
1811 by (Asm_full_simp_tac 1); |
1812 by (asm_full_simp_tac |
1812 by (asm_full_simp_tac |
1813 (simpset() addsimps [inverse_eq_divide, pos_divide_le_eq]) 1); |
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); |
1814 by (cut_inst_tac [("a","k"),("b","M-f a")] zero_less_mult_iff 1); |
1815 by (Asm_full_simp_tac 1); |
1815 by (Asm_full_simp_tac 1); |
1816 (*last one*) |
1816 (*last one*) |
1817 by (REPEAT(dres_inst_tac [("x","x")] spec 1)); |
1817 by (REPEAT(dres_inst_tac [("x","x")] spec 1)); |
1818 by (Asm_full_simp_tac 1); |
1818 by (Asm_full_simp_tac 1); |
1819 qed "isCont_eq_Ub"; |
1819 qed "isCont_eq_Ub"; |
1820 |
1820 |
1821 |
1821 |
1822 (*----------------------------------------------------------------------------*) |
1822 (*----------------------------------------------------------------------------*) |
1823 (* Same theorem for lower bound *) |
1823 (* Same theorem for lower bound *) |
1861 |
1861 |
1862 (*----------------------------------------------------------------------------*) |
1862 (*----------------------------------------------------------------------------*) |
1863 (* If f'(x) > 0 then x is locally strictly increasing at the right *) |
1863 (* If f'(x) > 0 then x is locally strictly increasing at the right *) |
1864 (*----------------------------------------------------------------------------*) |
1864 (*----------------------------------------------------------------------------*) |
1865 |
1865 |
1866 Goalw [deriv_def,LIM_def] |
1866 Goalw [deriv_def,LIM_def] |
1867 "[| DERIV f x :> l; 0 < l |] \ |
1867 "[| DERIV f x :> l; 0 < l |] \ |
1868 \ ==> \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"; |
1868 \ ==> \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"; |
1869 by (dtac spec 1 THEN Auto_tac); |
1869 by (dtac spec 1 THEN Auto_tac); |
1870 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
1870 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
1871 by (subgoal_tac "0 < l*h" 1); |
1871 by (subgoal_tac "0 < l*h" 1); |
1872 by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2); |
1872 by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2); |
1873 by (dres_inst_tac [("x","h")] spec 1); |
1873 by (dres_inst_tac [("x","h")] spec 1); |
1874 by (asm_full_simp_tac |
1874 by (asm_full_simp_tac |
1875 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1875 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1876 pos_le_divide_eq, pos_less_divide_eq] |
1876 pos_le_divide_eq, pos_less_divide_eq] |
1877 addsplits [split_if_asm]) 1); |
1877 addsplits [split_if_asm]) 1); |
1878 qed "DERIV_left_inc"; |
1878 qed "DERIV_left_inc"; |
1879 |
1879 |
1880 val prems = goalw (the_context()) [deriv_def,LIM_def] |
1880 val prems = goalw (the_context()) [deriv_def,LIM_def] |
1881 "[| DERIV f x :> l; l < 0 |] ==> \ |
1881 "[| DERIV f x :> l; l < 0 |] ==> \ |
1882 \ \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x - h))"; |
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*) |
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); |
1884 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); |
1885 by (res_inst_tac [("x","s")] exI 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); |
1886 by (dres_inst_tac [("x","-h")] spec 1); |
1887 by (asm_full_simp_tac |
1887 by (asm_full_simp_tac |
1888 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1888 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1889 pos_less_divide_eq, |
1889 pos_less_divide_eq, |
1890 symmetric real_diff_def] |
1890 symmetric real_diff_def] |
1891 addsplits [split_if_asm]) 1); |
1891 addsplits [split_if_asm]) 1); |
1892 by (subgoal_tac "0 < (f (x - h) - f x)/h" 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); |
1893 by (asm_full_simp_tac (simpset() addsimps [pos_less_divide_eq]) 1); |
1894 by (cut_facts_tac prems 1); |
1894 by (cut_facts_tac prems 1); |
1895 by (arith_tac 1); |
1895 by (arith_tac 1); |
1896 qed "DERIV_left_dec"; |
1896 qed "DERIV_left_dec"; |
1897 |
1897 |
1898 (*????previous proof, revealing arith problem: |
1898 (*????previous proof, revealing arith problem: |
1899 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); |
1899 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); |
1900 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
1900 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
1901 by (subgoal_tac "l*h < 0" 1); |
1901 by (subgoal_tac "l*h < 0" 1); |
1902 by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2); |
1902 by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2); |
1903 by (dres_inst_tac [("x","-h")] spec 1); |
1903 by (dres_inst_tac [("x","-h")] spec 1); |
1904 by (asm_full_simp_tac |
1904 by (asm_full_simp_tac |
1905 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1905 (simpset() addsimps [real_abs_def, inverse_eq_divide, |
1906 pos_less_divide_eq, |
1906 pos_less_divide_eq, |
1907 symmetric real_diff_def] |
1907 symmetric real_diff_def] |
1908 addsplits [split_if_asm] |
1908 addsplits [split_if_asm] |
1909 delsimprocs [fast_real_arith_simproc]) 1); |
1909 delsimprocs [fast_real_arith_simproc]) 1); |
1910 by (subgoal_tac "0 < (f (x - h) - f x)/h" 1); |
1910 by (subgoal_tac "0 < (f (x - h) - f x)/h" 1); |
1911 by (arith_tac 2); |
1911 by (arith_tac 2); |
1912 by (asm_full_simp_tac |
1912 by (asm_full_simp_tac |
1913 (simpset() addsimps [pos_less_divide_eq]) 1); |
1913 (simpset() addsimps [pos_less_divide_eq]) 1); |
1914 qed "DERIV_left_dec"; |
1914 qed "DERIV_left_dec"; |
1915 *) |
1915 *) |
1916 |
1916 |
1917 |
1917 |
1918 Goal "[| DERIV f x :> l; \ |
1918 Goal "[| DERIV f x :> l; \ |
2067 Rolle 1); |
2067 Rolle 1); |
2068 by (rtac lemma_MVT 1); |
2068 by (rtac lemma_MVT 1); |
2069 by Safe_tac; |
2069 by Safe_tac; |
2070 by (rtac isCont_diff 1 THEN Blast_tac 1); |
2070 by (rtac isCont_diff 1 THEN Blast_tac 1); |
2071 by (rtac (isCont_const RS isCont_mult) 1); |
2071 by (rtac (isCont_const RS isCont_mult) 1); |
2072 by (rtac isCont_Id 1); |
2072 by (rtac isCont_Id 1); |
2073 by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"), |
2073 by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"), |
2074 ("x","x")] spec 1); |
2074 ("x","x")] spec 1); |
2075 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
2075 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); |
2076 by Safe_tac; |
2076 by Safe_tac; |
2077 by (res_inst_tac [("x","xa - ((f(b) - f(a)) / (b - a))")] exI 1); |
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); |
2078 by (rtac DERIV_diff 1 THEN assume_tac 1); |
2079 (*derivative of a linear function is the constant...*) |
2079 (*derivative of a linear function is the constant...*) |
2080 by (subgoal_tac "(%x. (f b - f a) * x / (b - a)) = \ |
2080 by (subgoal_tac "(%x. (f b - f a) * x / (b - a)) = \ |
2081 \ op * ((f b - f a) / (b - a))" 1); |
2081 \ op * ((f b - f a) / (b - a))" 1); |
2082 by (rtac ext 2 THEN Simp_tac 2); |
2082 by (rtac ext 2 THEN Simp_tac 2); |
2083 by (Asm_full_simp_tac 1); |
2083 by (Asm_full_simp_tac 1); |
2084 (*final case*) |
2084 (*final case*) |
2085 by (res_inst_tac [("x","((f(b) - f(a)) / (b - a))")] exI 1); |
2085 by (res_inst_tac [("x","((f(b) - f(a)) / (b - a))")] exI 1); |
2086 by (res_inst_tac [("x","z")] exI 1); |
2086 by (res_inst_tac [("x","z")] exI 1); |
2087 by Safe_tac; |
2087 by Safe_tac; |
2088 by (Asm_full_simp_tac 2); |
2088 by (Asm_full_simp_tac 2); |
2089 by (subgoal_tac "DERIV (%x. ((f(b) - f(a)) / (b - a)) * x) z :> \ |
2089 by (subgoal_tac "DERIV (%x. ((f(b) - f(a)) / (b - a)) * x) z :> \ |
2090 \ ((f(b) - f(a)) / (b - a))" 1); |
2090 \ ((f(b) - f(a)) / (b - a))" 1); |
2091 by (rtac DERIV_cmult_Id 2); |
2091 by (rtac DERIV_cmult_Id 2); |
2092 by (dtac DERIV_add 1 THEN assume_tac 1); |
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); |
2093 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc, real_diff_def]) 1); |
2094 qed "MVT"; |
2094 qed "MVT"; |
2095 |
2095 |
2096 (*----------------------------------------------------------------------------*) |
2096 (*----------------------------------------------------------------------------*) |
2134 |
2134 |
2135 Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k"; |
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); |
2136 by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1); |
2137 by Auto_tac; |
2137 by Auto_tac; |
2138 by (ALLGOALS(dres_inst_tac [("f","f")] MVT)); |
2138 by (ALLGOALS(dres_inst_tac [("f","f")] MVT)); |
2139 by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps |
2139 by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps |
2140 [differentiable_def])); |
2140 [differentiable_def])); |
2141 by (auto_tac (claset() addDs [DERIV_unique], |
2141 by (auto_tac (claset() addDs [DERIV_unique], |
2142 simpset() addsimps [left_distrib, real_diff_def])); |
2142 simpset() addsimps [left_distrib, real_diff_def])); |
2143 qed "DERIV_const_ratio_const"; |
2143 qed "DERIV_const_ratio_const"; |
2144 |
2144 |
2145 Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k"; |
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); |
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], |
2147 by (auto_tac (claset() addSDs [DERIV_const_ratio_const], |
2148 simpset() addsimps [real_mult_assoc])); |
2148 simpset() addsimps [real_mult_assoc])); |
2149 qed "DERIV_const_ratio_const2"; |
2149 qed "DERIV_const_ratio_const2"; |
2150 |
2150 |
2151 Goal "((a + b) /2 - a) = (b - a)/(2::real)"; |
2151 Goal "((a + b) /2 - a) = (b - a)/(2::real)"; |
2152 by Auto_tac; |
2152 by Auto_tac; |
2153 qed "real_average_minus_first"; |
2153 qed "real_average_minus_first"; |
2154 Addsimps [real_average_minus_first]; |
2154 Addsimps [real_average_minus_first]; |
2155 |
2155 |
2156 Goal "((b + a)/2 - a) = (b - a)/(2::real)"; |
2156 Goal "((b + a)/2 - a) = (b - a)/(2::real)"; |
2157 by Auto_tac; |
2157 by Auto_tac; |
2158 qed "real_average_minus_second"; |
2158 qed "real_average_minus_second"; |
2159 Addsimps [real_average_minus_second]; |
2159 Addsimps [real_average_minus_second]; |
2160 |
2160 |
2161 |
2161 |
2162 (* Gallileo's "trick": average velocity = av. of end velocities *) |
2162 (* Gallileo's "trick": average velocity = av. of end velocities *) |
2165 by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1); |
2165 by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1); |
2166 by Safe_tac; |
2166 by Safe_tac; |
2167 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1); |
2167 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1); |
2168 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2); |
2168 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2); |
2169 by (dtac real_less_half_sum 1); |
2169 by (dtac real_less_half_sum 1); |
2170 by (dtac real_gt_half_sum 2); |
2170 by (dtac real_gt_half_sum 2); |
2171 by (ftac (real_not_refl2 RS DERIV_const_ratio_const2) 1 THEN assume_tac 1); |
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 |
2172 by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2 |
2173 THEN assume_tac 2); |
2173 THEN assume_tac 2); |
2174 by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong)); |
2174 by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong)); |
2175 by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide])); |
2175 by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide])); |
2176 by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1); |
2176 by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1); |
2177 qed "DERIV_const_average"; |
2177 qed "DERIV_const_average"; |
2178 |
2178 |
2179 |
2179 |
2180 (* ------------------------------------------------------------------------ *) |
2180 (* ------------------------------------------------------------------------ *) |
2181 (* Dull lemma that an continuous injection on an interval must have a strict*) |
2181 (* Dull lemma that an continuous injection on an interval must have a strict*) |
2242 \ ==> \\<exists>e. 0 < e & \ |
2242 \ ==> \\<exists>e. 0 < e & \ |
2243 \ (\\<forall>y. \ |
2243 \ (\\<forall>y. \ |
2244 \ abs(y - f(x)) \\<le> e --> \ |
2244 \ abs(y - f(x)) \\<le> e --> \ |
2245 \ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))"; |
2245 \ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))"; |
2246 by (ftac order_less_imp_le 1); |
2246 by (ftac order_less_imp_le 1); |
2247 by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate |
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); |
2248 [("f","f"),("a","x - d"),("b","x + d")] isCont_Lb_Ub))) 1); |
2249 by Safe_tac; |
2249 by Safe_tac; |
2250 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
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); |
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); |
2252 by (dres_inst_tac [("P", "%v. ?P v --> ?Q v & ?R v"), ("x","x")] spec 2); |
2253 by (Asm_full_simp_tac 2); |
2253 by (Asm_full_simp_tac 2); |
2254 by (subgoal_tac "L < f x & f x < M" 1); |
2254 by (subgoal_tac "L < f x & f x < M" 1); |
2255 by Safe_tac; |
2255 by Safe_tac; |
2256 by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1); |
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); |
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")] |
2258 by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")] |
2259 (real_lbound_gt_zero) 1); |
2259 (real_lbound_gt_zero) 1); |
2260 by Safe_tac; |
2260 by Safe_tac; |
2261 by (res_inst_tac [("x","e")] exI 1); |
2261 by (res_inst_tac [("x","e")] exI 1); |
2262 by Safe_tac; |
2262 by Safe_tac; |
2263 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |
2263 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1); |