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