|
1 (* Title : Integration.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2000 University of Edinburgh |
|
4 Description : Theory of integration (c.f. Harison's HOL development) |
|
5 *) |
|
6 |
|
7 Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0"; |
|
8 by Auto_tac; |
|
9 qed "partition_zero"; |
|
10 Addsimps [partition_zero]; |
|
11 |
|
12 Goalw [psize_def] "a < b ==> psize (%n. if n = 0 then a else b) = 1"; |
|
13 by Auto_tac; |
|
14 by (rtac some_equality 1); |
|
15 by Auto_tac; |
|
16 by (dres_inst_tac [("x","1")] spec 1); |
|
17 by Auto_tac; |
|
18 qed "partition_one"; |
|
19 Addsimps [partition_one]; |
|
20 |
|
21 Goalw [partition_def] |
|
22 "a <= b ==> partition(a,b)(%n. if n = 0 then a else b)"; |
|
23 by (auto_tac (claset(),simpset() addsimps [real_le_less])); |
|
24 qed "partition_single"; |
|
25 Addsimps [partition_single]; |
|
26 |
|
27 Goalw [partition_def] "partition(a,b) D ==> (D(0) = a)"; |
|
28 by Auto_tac; |
|
29 qed "partition_lhs"; |
|
30 |
|
31 Goalw [partition_def] |
|
32 "(partition(a,b) D) = \ |
|
33 \ ((D 0 = a) & \ |
|
34 \ (ALL n. n < (psize D) --> D n < D(Suc n)) & \ |
|
35 \ (ALL n. (psize D) <= n --> (D n = b)))"; |
|
36 by Auto_tac; |
|
37 by (ALLGOALS(subgoal_tac "psize D = N")); |
|
38 by Auto_tac; |
|
39 by (ALLGOALS(simp_tac (simpset() addsimps [psize_def]))); |
|
40 by (ALLGOALS(rtac some_equality)); |
|
41 by (Blast_tac 1 THEN Blast_tac 2); |
|
42 by (ALLGOALS(rtac ccontr)); |
|
43 by (ALLGOALS(dtac (ARITH_PROVE "n ~= (N::nat) ==> n < N | N < n"))); |
|
44 by (Step_tac 1); |
|
45 by (dres_inst_tac [("x","Na")] spec 1); |
|
46 by (rotate_tac 3 1); |
|
47 by (dres_inst_tac [("x","Suc Na")] spec 1); |
|
48 by (Asm_full_simp_tac 1); |
|
49 by (rotate_tac 2 1); |
|
50 by (dres_inst_tac [("x","N")] spec 1); |
|
51 by (Asm_full_simp_tac 1); |
|
52 by (dres_inst_tac [("x","Na")] spec 1); |
|
53 by (rotate_tac 3 1); |
|
54 by (dres_inst_tac [("x","Suc Na")] spec 1); |
|
55 by (Asm_full_simp_tac 1); |
|
56 by (rotate_tac 2 1); |
|
57 by (dres_inst_tac [("x","N")] spec 1); |
|
58 by (Asm_full_simp_tac 1); |
|
59 qed "partition"; |
|
60 |
|
61 Goal "partition(a,b) D ==> (D(psize D) = b)"; |
|
62 by (dtac (partition RS subst) 1); |
|
63 by (Step_tac 1); |
|
64 by (REPEAT(dres_inst_tac [("x","psize D")] spec 1)); |
|
65 by Auto_tac; |
|
66 qed "partition_rhs"; |
|
67 |
|
68 Goal "[|partition(a,b) D; psize D <= n |] ==> (D n = b)"; |
|
69 by (dtac (partition RS subst) 1); |
|
70 by (Blast_tac 1); |
|
71 qed "partition_rhs2"; |
|
72 |
|
73 Goal |
|
74 "partition(a,b) D & m + Suc d <= n & n <= (psize D) --> D(m) < D(m + Suc d)"; |
|
75 by (induct_tac "d" 1); |
|
76 by Auto_tac; |
|
77 by (ALLGOALS(dtac (partition RS subst))); |
|
78 by (Step_tac 1); |
|
79 by (ALLGOALS(dtac (ARITH_PROVE "Suc m <= n ==> m < n"))); |
|
80 by (ALLGOALS(dtac less_le_trans)); |
|
81 by (assume_tac 1 THEN assume_tac 2); |
|
82 by (ALLGOALS(blast_tac (claset() addIs [real_less_trans]))); |
|
83 qed_spec_mp "lemma_partition_lt_gen"; |
|
84 |
|
85 Goal "m < n ==> EX d. n = m + Suc d"; |
|
86 by (auto_tac (claset(),simpset() addsimps [less_iff_Suc_add])); |
|
87 qed "less_eq_add_Suc"; |
|
88 |
|
89 Goal "[|partition(a,b) D; m < n; n <= (psize D)|] ==> D(m) < D(n)"; |
|
90 by (auto_tac (claset() addDs [less_eq_add_Suc] addIs [lemma_partition_lt_gen], |
|
91 simpset())); |
|
92 qed "partition_lt_gen"; |
|
93 |
|
94 Goal "partition(a,b) D ==> (n < (psize D) --> D(0) < D(Suc n))"; |
|
95 by (dtac (partition RS subst) 1); |
|
96 by (induct_tac "n" 1); |
|
97 by (Blast_tac 1); |
|
98 by (blast_tac (claset() addSDs [leI] addDs |
|
99 [(ARITH_PROVE "m <= n ==> m <= Suc n"), |
|
100 le_less_trans,real_less_trans]) 1); |
|
101 qed_spec_mp "partition_lt"; |
|
102 |
|
103 Goal "partition(a,b) D ==> a <= b"; |
|
104 by (ftac (partition RS subst) 1); |
|
105 by (Step_tac 1); |
|
106 by (rotate_tac 2 1); |
|
107 by (dres_inst_tac [("x","psize D")] spec 1); |
|
108 by (Step_tac 1); |
|
109 by (rtac ccontr 1); |
|
110 by (case_tac "psize D = 0" 1); |
|
111 by (Step_tac 1); |
|
112 by (dres_inst_tac [("n","psize D - 1")] partition_lt 2); |
|
113 by Auto_tac; |
|
114 qed "partition_le"; |
|
115 |
|
116 Goal "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"; |
|
117 by (auto_tac (claset() addIs [partition_lt_gen],simpset())); |
|
118 qed "partition_gt"; |
|
119 |
|
120 Goal "partition(a,b) D ==> ((a = b) = (psize D = 0))"; |
|
121 by (ftac (partition RS subst) 1); |
|
122 by (Step_tac 1); |
|
123 by (rotate_tac 2 1); |
|
124 by (dres_inst_tac [("x","psize D")] spec 1); |
|
125 by (rtac ccontr 1); |
|
126 by (dres_inst_tac [("n","psize D - 1")] partition_lt 1); |
|
127 by (Blast_tac 3 THEN Auto_tac); |
|
128 qed "partition_eq"; |
|
129 |
|
130 Goal "partition(a,b) D ==> a <= D(r)"; |
|
131 by (ftac (partition RS subst) 1); |
|
132 by (Step_tac 1); |
|
133 by (induct_tac "r" 1); |
|
134 by (cut_inst_tac [("m","Suc n"),("n","psize D")] |
|
135 (ARITH_PROVE "m < n | n <= (m::nat)") 2); |
|
136 by (Step_tac 1); |
|
137 by (eres_inst_tac [("j","D n")] real_le_trans 1); |
|
138 by (dres_inst_tac [("x","n")] spec 1); |
|
139 by (blast_tac (claset() addIs [less_trans,order_less_imp_le]) 1); |
|
140 by (res_inst_tac [("j","b")] real_le_trans 1); |
|
141 by (etac partition_le 1); |
|
142 by (Blast_tac 1); |
|
143 qed "partition_lb"; |
|
144 |
|
145 Goal "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"; |
|
146 by (res_inst_tac [("t","a")] (partition_lhs RS subst) 1); |
|
147 by (assume_tac 1); |
|
148 by (cut_inst_tac [("m","psize D"),("n","Suc n")] |
|
149 (ARITH_PROVE "m < n | n <= (m::nat)") 1); |
|
150 by (ftac (partition RS subst) 1); |
|
151 by (Step_tac 1); |
|
152 by (rotate_tac 3 1); |
|
153 by (dres_inst_tac [("x","Suc n")] spec 1); |
|
154 by (etac impE 1); |
|
155 by (etac less_imp_le 1); |
|
156 by (ftac partition_rhs 1); |
|
157 by (dtac partition_gt 1 THEN assume_tac 1); |
|
158 by (Asm_simp_tac 1); |
|
159 by (blast_tac (claset() addIs [partition_lt,less_le_trans]) 1); |
|
160 qed "partition_lb_lt"; |
|
161 |
|
162 Goal "partition(a,b) D ==> D(r) <= b"; |
|
163 by (ftac (partition RS subst) 1); |
|
164 by (cut_inst_tac [("m","r"),("n","psize D")] |
|
165 (ARITH_PROVE "m < n | n <= (m::nat)") 1); |
|
166 by (Step_tac 1); |
|
167 by (Blast_tac 2); |
|
168 by (subgoal_tac "ALL x. D((psize D) - x) <= b" 1); |
|
169 by (rotate_tac 4 1); |
|
170 by (dres_inst_tac [("x","psize D - r")] spec 1); |
|
171 by (dtac (ARITH_PROVE "p < m ==> m - (m - p) = (p::nat)") 1); |
|
172 by (thin_tac "ALL n. psize D <= n --> D n = b" 1); |
|
173 by (Asm_full_simp_tac 1); |
|
174 by (Step_tac 1); |
|
175 by (induct_tac "x" 1); |
|
176 by (Simp_tac 1 THEN Blast_tac 1); |
|
177 by (case_tac "psize D - Suc n = 0" 1); |
|
178 by (thin_tac "ALL n. psize D <= n --> D n = b" 1); |
|
179 by (asm_simp_tac (simpset() addsimps [partition_le]) 1); |
|
180 by (rtac real_le_trans 1 THEN assume_tac 2); |
|
181 by (rtac (ARITH_PROVE "0 < m - Suc n ==> (m - n) = Suc(m - Suc n)" |
|
182 RS ssubst) 1); |
|
183 by (dres_inst_tac [("x","psize D - Suc n")] spec 2); |
|
184 by (thin_tac "ALL n. psize D <= n --> D n = b" 2); |
|
185 by (Asm_full_simp_tac 2); |
|
186 by (Blast_tac 1); |
|
187 qed "partition_ub"; |
|
188 |
|
189 Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b"; |
|
190 by (blast_tac (claset() addIs [partition_rhs RS subst] addIs |
|
191 [partition_gt]) 1); |
|
192 qed "partition_ub_lt"; |
|
193 |
|
194 Goal "[| partition (a, b) D1; partition (b, c) D2 |] \ |
|
195 \ ==> (ALL n. \ |
|
196 \ n < psize D1 + psize D2 --> \ |
|
197 \ (if n < psize D1 then D1 n else D2 (n - psize D1)) \ |
|
198 \ < (if Suc n < psize D1 then D1 (Suc n) \ |
|
199 \ else D2 (Suc n - psize D1))) & \ |
|
200 \ (ALL n. \ |
|
201 \ psize D1 + psize D2 <= n --> \ |
|
202 \ (if n < psize D1 then D1 n else D2 (n - psize D1)) = \ |
|
203 \ (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) \ |
|
204 \ else D2 (psize D1 + psize D2 - psize D1)))"; |
|
205 by (Step_tac 1); |
|
206 by (auto_tac (claset() addIs [partition_lt_gen],simpset())); |
|
207 by (dres_inst_tac [("m","psize D1")] |
|
208 (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 1); |
|
209 by (assume_tac 1); |
|
210 by (auto_tac (claset() addSIs [partition_lt_gen], |
|
211 simpset() addsimps [partition_lhs,partition_ub_lt])); |
|
212 by (blast_tac (claset() addIs [ARITH_PROVE "~n < m ==> n - m < Suc n - m"]) 1); |
|
213 by (auto_tac (claset(),simpset() addsimps [ |
|
214 ARITH_PROVE "~ n < m ==> (Suc n - m <= p) = (Suc n <= m + p)"])); |
|
215 by (dtac (ARITH_PROVE "p + q <= (n::nat) ==> q <= n - p") 1); |
|
216 by (auto_tac (claset() addSIs [partition_rhs2], simpset() addsimps |
|
217 [partition_rhs])); |
|
218 qed "lemma_partition_append1"; |
|
219 |
|
220 Goal "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] \ |
|
221 \ ==> D1(N) < D2 (psize D2)"; |
|
222 by (res_inst_tac [("y","D1(psize D1)")] order_less_le_trans 1); |
|
223 by (etac partition_gt 1 THEN assume_tac 1); |
|
224 by (auto_tac (claset(),simpset() addsimps [partition_rhs,partition_le])); |
|
225 qed "lemma_psize1"; |
|
226 |
|
227 Goal "[| partition (a, b) D1; partition (b, c) D2 |] \ |
|
228 \ ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = \ |
|
229 \ psize D1 + psize D2"; |
|
230 by (res_inst_tac |
|
231 [("D2","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] |
|
232 ((psize_def RS meta_eq_to_obj_eq) RS ssubst) 1); |
|
233 by (rtac some1_equality 1); |
|
234 by (blast_tac (claset() addSIs [lemma_partition_append1]) 2); |
|
235 by (rtac ex1I 1 THEN rtac lemma_partition_append1 1); |
|
236 by Auto_tac; |
|
237 by (rtac ccontr 1); |
|
238 by (dtac (ARITH_PROVE "m ~= n ==> m < n | n < (m::nat)") 1); |
|
239 by (Step_tac 1); |
|
240 by (rotate_tac 3 1); |
|
241 by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1); |
|
242 by Auto_tac; |
|
243 by (case_tac "N < psize D1" 1); |
|
244 by (auto_tac (claset() addDs [lemma_psize1],simpset())); |
|
245 by (dtac leI 1); |
|
246 by (dtac (ARITH_PROVE "[|p <= n; n < p + m|] ==> n - p < (m::nat)") 1); |
|
247 by (assume_tac 1); |
|
248 by (dres_inst_tac [("a","b"),("b","c")] partition_gt 1); |
|
249 by Auto_tac; |
|
250 by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1); |
|
251 by (auto_tac (claset(),simpset() addsimps [partition_rhs2])); |
|
252 qed "lemma_partition_append2"; |
|
253 |
|
254 Goalw [tpart_def] |
|
255 "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"; |
|
256 by (auto_tac (claset(),simpset() addsimps [partition_eq])); |
|
257 qed "tpart_eq_lhs_rhs"; |
|
258 |
|
259 Goalw [tpart_def] "tpart(a,b) (D,p) ==> partition(a,b) D"; |
|
260 by Auto_tac; |
|
261 qed "tpart_partition"; |
|
262 |
|
263 Goal "[| tpart(a,b) (D1,p1); fine(g) (D1,p1); \ |
|
264 \ tpart(b,c) (D2,p2); fine(g) (D2,p2) |] \ |
|
265 \ ==> EX D p. tpart(a,c) (D,p) & fine(g) (D,p)"; |
|
266 by (res_inst_tac |
|
267 [("x","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] exI 1); |
|
268 by (res_inst_tac |
|
269 [("x","%n. if n < psize D1 then p1 n else p2 (n - psize D1)")] exI 1); |
|
270 by (cut_inst_tac [("m","psize D1")] (ARITH_PROVE "0 < (m::nat) | m = 0") 1); |
|
271 by (auto_tac (claset() addDs [tpart_eq_lhs_rhs],simpset())); |
|
272 by (asm_full_simp_tac (simpset() addsimps [fine_def, |
|
273 [tpart_partition,tpart_partition] MRS lemma_partition_append2]) 2); |
|
274 by Auto_tac; |
|
275 by (dres_inst_tac [("m","psize D1"),("n","n")] |
|
276 (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2); |
|
277 by Auto_tac; |
|
278 by (dtac (tpart_partition RS partition_rhs) 2); |
|
279 by (dtac (tpart_partition RS partition_lhs) 2); |
|
280 by Auto_tac; |
|
281 by (rotate_tac 3 2); |
|
282 by (dres_inst_tac [("x","n - psize D1")] spec 2); |
|
283 by (auto_tac (claset(),simpset() addsimps |
|
284 [ARITH_PROVE "[| (0::nat) < p; p <= n |] ==> (n - p < m) = (n < p + m)", |
|
285 ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"])); |
|
286 by (auto_tac (claset(),simpset() addsimps [tpart_def, |
|
287 ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"])); |
|
288 by (dres_inst_tac [("m","psize D1"),("n","n")] |
|
289 (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2); |
|
290 by Auto_tac; |
|
291 by (dtac partition_rhs 2); |
|
292 by (dtac partition_lhs 2); |
|
293 by Auto_tac; |
|
294 by (rtac (partition RS ssubst) 1); |
|
295 by (rtac (lemma_partition_append2 RS ssubst) 1); |
|
296 by (rtac conjI 3); |
|
297 by (dtac lemma_partition_append1 4); |
|
298 by (auto_tac (claset(),simpset() addsimps [partition_lhs,partition_rhs])); |
|
299 qed "partition_append"; |
|
300 |
|
301 (* ------------------------------------------------------------------------ *) |
|
302 (* We can always find a division which is fine wrt any gauge *) |
|
303 (* ------------------------------------------------------------------------ *) |
|
304 |
|
305 Goal "[| a <= b; gauge(%x. a <= x & x <= b) g |] \ |
|
306 \ ==> EX D p. tpart(a,b) (D,p) & fine g (D,p)"; |
|
307 by (cut_inst_tac |
|
308 [("P","%(u,v). a <= u & v <= b --> (EX D p. tpart(u,v) (D,p) & fine(g) (D,p))")] |
|
309 lemma_BOLZANO2 1); |
|
310 by (Step_tac 1); |
|
311 by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 1)); |
|
312 by (auto_tac (claset() addIs [partition_append],simpset())); |
|
313 by (case_tac "a <= x & x <= b" 1); |
|
314 by (res_inst_tac [("x","1")] exI 2); |
|
315 by Auto_tac; |
|
316 by (res_inst_tac [("x","g x")] exI 1); |
|
317 by (auto_tac (claset(),simpset() addsimps [gauge_def])); |
|
318 by (res_inst_tac [("x","%n. if n = 0 then aa else ba")] exI 1); |
|
319 by (res_inst_tac [("x","%n. if n = 0 then x else ba")] exI 1); |
|
320 by (auto_tac (claset(),simpset() addsimps [tpart_def,fine_def])); |
|
321 qed "partition_exists"; |
|
322 |
|
323 (* ------------------------------------------------------------------------ *) |
|
324 (* Lemmas about combining gauges *) |
|
325 (* ------------------------------------------------------------------------ *) |
|
326 |
|
327 Goalw [gauge_def] |
|
328 "[| gauge(E) g1; gauge(E) g2 |] \ |
|
329 \ ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))"; |
|
330 by Auto_tac; |
|
331 qed "gauge_min"; |
|
332 |
|
333 Goalw [fine_def] |
|
334 "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) \ |
|
335 \ ==> fine(g1) (D,p) & fine(g2) (D,p)"; |
|
336 by (auto_tac (claset(),simpset() addsimps [split_if])); |
|
337 qed "fine_min"; |
|
338 |
|
339 |
|
340 (* ------------------------------------------------------------------------ *) |
|
341 (* The integral is unique if it exists *) |
|
342 (* ------------------------------------------------------------------------ *) |
|
343 |
|
344 Goalw [Integral_def] |
|
345 "[| a <= b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"; |
|
346 by Auto_tac; |
|
347 by (REPEAT(dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1)); |
|
348 by (Auto_tac THEN TRYALL(arith_tac)); |
|
349 by (dtac gauge_min 1 THEN assume_tac 1); |
|
350 by (dres_inst_tac [("g","%x. if g x < ga x then g x else ga x")] |
|
351 partition_exists 1 THEN assume_tac 1); |
|
352 by Auto_tac; |
|
353 by (dtac fine_min 1); |
|
354 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
355 by (subgoal_tac |
|
356 "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1); |
|
357 by (arith_tac 1); |
|
358 by (dtac real_add_less_mono 1 THEN assume_tac 1); |
|
359 by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, |
|
360 real_mult_2_right RS sym,real_mult_less_cancel2])); |
|
361 by (ALLGOALS(arith_tac)); |
|
362 qed "Integral_unique"; |
|
363 |
|
364 Goalw [Integral_def] "Integral(a,a) f 0"; |
|
365 by Auto_tac; |
|
366 by (res_inst_tac [("x","%x. 1")] exI 1); |
|
367 by (auto_tac (claset() addDs [partition_eq],simpset() addsimps [gauge_def, |
|
368 tpart_def,rsum_def])); |
|
369 qed "Integral_zero"; |
|
370 Addsimps [Integral_zero]; |
|
371 |
|
372 Goal "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"; |
|
373 by (induct_tac "m" 1); |
|
374 by Auto_tac; |
|
375 qed "sumr_partition_eq_diff_bounds"; |
|
376 Addsimps [sumr_partition_eq_diff_bounds]; |
|
377 |
|
378 Goal "a <= b ==> Integral(a,b) (%x. 1) (b - a)"; |
|
379 by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac); |
|
380 by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def])); |
|
381 by (res_inst_tac [("x","%x. b - a")] exI 1); |
|
382 by (auto_tac (claset(),simpset() addsimps [gauge_def, |
|
383 abs_interval_iff,tpart_def,partition])); |
|
384 qed "Integral_eq_diff_bounds"; |
|
385 |
|
386 Goal "a <= b ==> Integral(a,b) (%x. c) (c*(b - a))"; |
|
387 by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac); |
|
388 by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def])); |
|
389 by (res_inst_tac [("x","%x. b - a")] exI 1); |
|
390 by (auto_tac (claset(),simpset() addsimps |
|
391 [sumr_mult RS sym,gauge_def,abs_interval_iff, |
|
392 real_diff_mult_distrib2 RS sym,partition,tpart_def])); |
|
393 qed "Integral_mult_const"; |
|
394 |
|
395 Goal "[| a <= b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"; |
|
396 by (dtac real_le_imp_less_or_eq 1); |
|
397 by (auto_tac (claset() addDs [[real_le_refl,Integral_zero] MRS Integral_unique], |
|
398 simpset())); |
|
399 by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def, |
|
400 sumr_mult RS sym,real_mult_assoc])); |
|
401 by (res_inst_tac [("x2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq) |
|
402 RS disjE) 1); |
|
403 by (dtac sym 2); |
|
404 by (Asm_full_simp_tac 2 THEN Blast_tac 2); |
|
405 by (dres_inst_tac [("x","e/abs c")] spec 1 THEN Auto_tac); |
|
406 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff, |
|
407 real_divide_def]) 1); |
|
408 by (rtac exI 1 THEN Auto_tac); |
|
409 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
410 by (res_inst_tac [("z1","inverse(abs c)")] (real_mult_less_iff1 RS iffD1) 1); |
|
411 by (fold_tac [real_divide_def]); |
|
412 by (auto_tac (claset(),simpset() addsimps [real_diff_mult_distrib2 |
|
413 RS sym,abs_mult,real_mult_assoc RS sym, |
|
414 ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0",real_inverse_gt_0])); |
|
415 qed "Integral_mult"; |
|
416 |
|
417 (* ------------------------------------------------------------------------ *) |
|
418 (* Fundamental theorem of calculus (Part I) *) |
|
419 (* ------------------------------------------------------------------------ *) |
|
420 |
|
421 (* "Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *) |
|
422 |
|
423 Goal "ALL x. P(x) --> (EX y. Q x y) ==> EX f. (ALL x. P(x) --> Q x (f x))"; |
|
424 by (cut_inst_tac [("S","Collect (%x. P x)"),("Q","Q")] (CLAIM_SIMP |
|
425 "(ALL x:S. (EX y. Q x y)) --> (EX f. (ALL x:S. Q x (f x)))" [bchoice]) 1); |
|
426 by Auto_tac; |
|
427 qed "choiceP"; |
|
428 |
|
429 Goal "ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z)) ==> \ |
|
430 \ EX f fa. (ALL x. P(x) --> R(f x) & Q x (f x) (fa x))"; |
|
431 by (dtac (CLAIM "(ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z))) = \ |
|
432 \ (ALL x. P(x) --> (EX y z. R(y) & Q x y z))" RS iffD1) 1);; |
|
433 by (dtac choiceP 1 THEN Step_tac 1); |
|
434 by (dtac choiceP 1 THEN Auto_tac); |
|
435 qed "choiceP2"; |
|
436 |
|
437 Goal "ALL x. (EX y. R(y) & (EX z. Q x y z)) ==> \ |
|
438 \ EX f fa. (ALL x. R(f x) & Q x (f x) (fa x))"; |
|
439 by (dtac (CLAIM "(ALL x. (EX y. R(y) & (EX z. Q x y z))) = \ |
|
440 \ (ALL x. (EX y z. R(y) & Q x y z))" RS iffD1) 1);; |
|
441 by (dtac choice 1 THEN Step_tac 1); |
|
442 by (dtac choice 1 THEN Auto_tac); |
|
443 qed "choice2"; |
|
444 |
|
445 (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance |
|
446 they break the original proofs and make new proofs longer! *) |
|
447 Goalw [gauge_def] |
|
448 "[| ALL x. a <= x & x <= b --> DERIV f x :> f'(x); 0 < e |]\ |
|
449 \ ==> EX g. gauge(%x. a <= x & x <= b) g & \ |
|
450 \ (ALL x u v. a <= u & u <= x & x <= v & v <= b & (v - u) < g(x) \ |
|
451 \ --> abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u))"; |
|
452 by (subgoal_tac "ALL x. a <= x & x <= b --> \ |
|
453 \ (EX d. 0 < d & \ |
|
454 \ (ALL u v. u <= x & x <= v & (v - u) < d --> \ |
|
455 \ abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u)))" 1); |
|
456 by (dtac choiceP 1); |
|
457 by Auto_tac; |
|
458 by (dtac spec 1 THEN Auto_tac); |
|
459 by (auto_tac (claset(),simpset() addsimps [DERIV_iff2,LIM_def])); |
|
460 by (dres_inst_tac [("x","e/2")] spec 1); |
|
461 by Auto_tac; |
|
462 by (subgoal_tac "ALL z. abs(z - x) < s --> \ |
|
463 \ abs((f(z) - f(x)) - (f'(x) * (z - x))) <= (e / 2) * abs(z - x)" 1); |
|
464 by Auto_tac; |
|
465 by (case_tac "0 < abs(z - x)" 2); |
|
466 by (dtac (ARITH_PROVE "~ 0 < abs z ==> z = (0::real)") 3); |
|
467 by (asm_full_simp_tac (simpset() addsimps |
|
468 [ARITH_PROVE "(z - x = 0) = (z = (x::real))"]) 3); |
|
469 by (dres_inst_tac [("x","z")] spec 2); |
|
470 by (res_inst_tac [("z1","abs(inverse(z - x))")] |
|
471 (real_mult_le_cancel_iff2 RS iffD1) 2); |
|
472 by (Asm_full_simp_tac 2); |
|
473 by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym, |
|
474 real_mult_assoc RS sym]) 2); |
|
475 by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \ |
|
476 \ (f z - f x)/(z - x) - f' x" 2); |
|
477 by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ real_mult_ac) 2); |
|
478 by (asm_full_simp_tac (simpset() addsimps [real_diff_def]) 2); |
|
479 by (rtac (real_mult_commute RS subst) 2); |
|
480 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib, |
|
481 real_diff_def]) 2); |
|
482 by (dtac (CLAIM "z ~= x ==> z + -x ~= (0::real)") 2); |
|
483 by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc, |
|
484 real_divide_def]) 2); |
|
485 by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 2); |
|
486 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); |
|
487 by (res_inst_tac [("u1","u"),("v1","v")] (ARITH_PROVE "u < v | v <= (u::real)" |
|
488 RS disjE) 1); |
|
489 by (dres_inst_tac [("x","v")] real_le_imp_less_or_eq 2); |
|
490 by Auto_tac; |
|
491 (*29*) |
|
492 by (res_inst_tac [("j","abs((f(v) - f(x)) - (f'(x) * (v - x))) + \ |
|
493 \ abs((f(x) - f(u)) - (f'(x) * (x - u)))")] real_le_trans 1); |
|
494 by (rtac (abs_triangle_ineq RSN (2,real_le_trans)) 1); |
|
495 by (asm_full_simp_tac (simpset() addsimps [real_diff_mult_distrib2]) 1); |
|
496 by (arith_tac 1); |
|
497 by (res_inst_tac [("t","e*(v - u)")] (real_sum_of_halves RS subst) 1); |
|
498 by (rtac real_add_le_mono 1); |
|
499 by (res_inst_tac [("j","(e / 2) * abs(v - x)")] real_le_trans 1); |
|
500 |
|
501 by (Asm_full_simp_tac 2 THEN arith_tac 2); |
|
502 by (ALLGOALS (thin_tac "ALL xa. \ |
|
503 \ xa ~= x & abs (xa + - x) < s --> \ |
|
504 \ abs ((f xa + - f x) / (xa + - x) + - f' x) * 2 < e")); |
|
505 by (dres_inst_tac [("x","v")] spec 1 THEN Auto_tac); |
|
506 by (arith_tac 1); |
|
507 by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac); |
|
508 by (arith_tac 1); |
|
509 by (subgoal_tac "abs (f u - f x - f' x * (u - x)) = \ |
|
510 \ abs (f x - f u - f' x * (x - u))" 1); |
|
511 by (Asm_full_simp_tac 1); |
|
512 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
|
513 real_diff_def]) 2); |
|
514 by (arith_tac 2); |
|
515 by(rtac real_le_trans 1); |
|
516 by Auto_tac; |
|
517 by (arith_tac 1); |
|
518 qed "lemma_straddle"; |
|
519 |
|
520 Goal "((number_of c - 1) * x <= 0) =((number_of c ::real) * x <= x)"; |
|
521 by (rtac ((ARITH_PROVE "(x <= y) = (x - y <= (0::real))") RS ssubst) 1); |
|
522 by (simp_tac (simpset() addsimps [real_diff_mult_distrib, |
|
523 CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [real_diff_mult_distrib]]) 1); |
|
524 qed "lemma_number_of_mult_le"; |
|
525 |
|
526 |
|
527 Goal "[|a <= b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \ |
|
528 \ ==> Integral(a,b) f' (f(b) - f(a))"; |
|
529 by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac); |
|
530 by (auto_tac (claset(),simpset() addsimps [Integral_def])); |
|
531 by (rtac ccontr 1); |
|
532 by (subgoal_tac "ALL e. 0 < e --> \ |
|
533 \ (EX g. gauge (%x. a <= x & x <= b) g & \ |
|
534 \ (ALL D p. \ |
|
535 \ tpart (a, b) (D, p) & fine g (D, p) --> \ |
|
536 \ abs (rsum (D, p) f' - (f b - f a)) <= e))" 1); |
|
537 by (rotate_tac 3 1); |
|
538 by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac); |
|
539 by (dtac spec 1 THEN Auto_tac); |
|
540 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
541 by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1); |
|
542 by (auto_tac (claset(),simpset() addsimps [real_0_less_divide_iff])); |
|
543 by (rtac exI 1); |
|
544 by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def])); |
|
545 by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \ |
|
546 \ f b - f a" 1); |
|
547 by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")] |
|
548 sumr_partition_eq_diff_bounds 2); |
|
549 by (asm_full_simp_tac (simpset() addsimps [partition_lhs,partition_rhs]) 2); |
|
550 by (dtac sym 1 THEN Asm_full_simp_tac 1); |
|
551 by (simp_tac (simpset() addsimps [sumr_diff]) 1); |
|
552 by (rtac (sumr_rabs RS real_le_trans) 1); |
|
553 by (subgoal_tac |
|
554 "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D(Suc n) - (D n)))" 1); |
|
555 by (asm_full_simp_tac (simpset() addsimps |
|
556 [ARITH_PROVE "abs(y - (x::real)) = abs(x - y)"]) 1); |
|
557 by (res_inst_tac [("t","ea")] ssubst 1 THEN assume_tac 1); |
|
558 by (rtac sumr_le2 1); |
|
559 by (rtac (sumr_mult RS subst) 2); |
|
560 by (auto_tac (claset(),simpset() addsimps [partition_rhs, |
|
561 partition_lhs,partition_lb,partition_ub,fine_def])); |
|
562 qed "FTC1"; |
|
563 |
|
564 |
|
565 Goal "[| Integral(a,b) f k1; k2 = k1 |] ==> Integral(a,b) f k2"; |
|
566 by (Asm_simp_tac 1); |
|
567 qed "Integral_subst"; |
|
568 |
|
569 Goal "[| a <= b; b <= c; Integral(a,b) f' k1; Integral(b,c) f' k2; \ |
|
570 \ ALL x. a <= x & x <= c --> DERIV f x :> f' x |] \ |
|
571 \ ==> Integral(a,c) f' (k1 + k2)"; |
|
572 by (rtac (FTC1 RS Integral_subst) 1); |
|
573 by Auto_tac; |
|
574 by (ftac FTC1 1 THEN Auto_tac); |
|
575 by (forw_inst_tac [("a","b")] FTC1 1 THEN Auto_tac); |
|
576 by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac); |
|
577 by (dres_inst_tac [("k2.0","f b - f a")] Integral_unique 1); |
|
578 by (dres_inst_tac [("k2.0","f c - f b")] Integral_unique 3); |
|
579 by Auto_tac; |
|
580 qed "Integral_add"; |
|
581 |
|
582 Goal "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"; |
|
583 by (auto_tac (claset() addSIs [Least_equality RS sym,partition_rhs],simpset())); |
|
584 by (rtac ccontr 1); |
|
585 by (dtac partition_ub_lt 1); |
|
586 by Auto_tac; |
|
587 qed "partition_psize_Least"; |
|
588 |
|
589 Goal "partition (a, c) D ==> ~ (EX n. c < D(n))"; |
|
590 by (Step_tac 1); |
|
591 by (dres_inst_tac [("r","n")] partition_ub 1); |
|
592 by Auto_tac; |
|
593 qed "lemma_partition_bounded"; |
|
594 |
|
595 Goal "partition (a, c) D ==> D = (%n. if D n < c then D n else c)"; |
|
596 by (rtac ext 1 THEN Auto_tac); |
|
597 by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset())); |
|
598 by (dres_inst_tac [("x","n")] spec 1); |
|
599 by Auto_tac; |
|
600 qed "lemma_partition_eq"; |
|
601 |
|
602 Goal "partition (a, c) D ==> D = (%n. if D n <= c then D n else c)"; |
|
603 by (rtac ext 1 THEN Auto_tac); |
|
604 by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset())); |
|
605 by (dres_inst_tac [("x","n")] spec 1); |
|
606 by Auto_tac; |
|
607 qed "lemma_partition_eq2"; |
|
608 |
|
609 Goal "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)"; |
|
610 by (auto_tac (claset(),simpset() addsimps [partition])); |
|
611 qed "partition_lt_Suc"; |
|
612 |
|
613 Goal "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"; |
|
614 by (rtac ext 1); |
|
615 by (auto_tac (claset(),simpset() addsimps [tpart_def])); |
|
616 by (dtac real_leI 1); |
|
617 by (dres_inst_tac [("r","Suc n")] partition_ub 1); |
|
618 by (dres_inst_tac [("x","n")] spec 1); |
|
619 by Auto_tac; |
|
620 qed "tpart_tag_eq"; |
|
621 |
|
622 (*----------------------------------------------------------------------------*) |
|
623 (* Lemmas for Additivity Theorem of gauge integral *) |
|
624 (*----------------------------------------------------------------------------*) |
|
625 |
|
626 Goal "[| a <= D n; D n < b; partition(a,b) D |] ==> n < psize D"; |
|
627 by (dtac (partition RS iffD1) 1 THEN Step_tac 1); |
|
628 by (rtac ccontr 1 THEN dtac leI 1); |
|
629 by Auto_tac; |
|
630 val lemma_additivity1 = result(); |
|
631 |
|
632 Goal "[| a <= D n; partition(a,D n) D |] ==> psize D <= n"; |
|
633 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
634 by (ftac (partition RS iffD1) 1 THEN Step_tac 1); |
|
635 by (forw_inst_tac [("r","Suc n")] partition_ub 1); |
|
636 by (auto_tac (claset() addSDs [spec],simpset())); |
|
637 val lemma_additivity2 = result(); |
|
638 |
|
639 Goal "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)"; |
|
640 by (auto_tac (claset(),simpset() addsimps [partition])); |
|
641 qed "partition_eq_bound"; |
|
642 |
|
643 Goal "[| partition(a,b) D; psize D < m |] ==> D(r) <= D(m)"; |
|
644 by (ftac (partition RS iffD1) 1 THEN Auto_tac); |
|
645 by (etac partition_ub 1); |
|
646 qed "partition_ub2"; |
|
647 |
|
648 Goalw [tpart_def] |
|
649 "[| tpart(a,b) (D,p); psize D <= m |] ==> p(m) = D(m)"; |
|
650 by Auto_tac; |
|
651 by (dres_inst_tac [("x","m")] spec 1); |
|
652 by (auto_tac (claset(),simpset() addsimps [partition_rhs2])); |
|
653 qed "tag_point_eq_partition_point"; |
|
654 |
|
655 Goal "[| partition(a,b) D; D m < D n |] ==> m < n"; |
|
656 by (cut_inst_tac [("m","n"),("n","psize D")] less_linear 1); |
|
657 by Auto_tac; |
|
658 by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1); |
|
659 by (cut_inst_tac [("m","m"),("n","psize D")] less_linear 1); |
|
660 by (auto_tac (claset() addDs [partition_gt],simpset())); |
|
661 by (dres_inst_tac [("n","m")] partition_lt_gen 1 THEN Auto_tac); |
|
662 by (ftac partition_eq_bound 1); |
|
663 by (dtac partition_gt 2); |
|
664 by Auto_tac; |
|
665 by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1); |
|
666 by (auto_tac (claset() addDs [partition_eq_bound],simpset())); |
|
667 by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1); |
|
668 by (ftac partition_eq_bound 1 THEN assume_tac 1); |
|
669 by (dres_inst_tac [("m","m")] partition_eq_bound 1); |
|
670 by Auto_tac; |
|
671 qed "partition_lt_cancel"; |
|
672 |
|
673 Goalw [psize_def] |
|
674 "[| a <= D n; D n < b; partition (a, b) D |] \ |
|
675 \ ==> psize (%x. if D x < D n then D(x) else D n) = n"; |
|
676 by (ftac lemma_additivity1 1); |
|
677 by (assume_tac 1 THEN assume_tac 1); |
|
678 by (rtac some_equality 1); |
|
679 by (auto_tac (claset() addIs [partition_lt_Suc],simpset())); |
|
680 by (dres_inst_tac [("n","n")] partition_lt_gen 1); |
|
681 by (assume_tac 1 THEN arith_tac 1 THEN arith_tac 1); |
|
682 by (cut_inst_tac [("m","na"),("n","psize D")] less_linear 1); |
|
683 by (auto_tac (claset() addDs [partition_lt_cancel],simpset())); |
|
684 by (rtac ccontr 1); |
|
685 by (dtac (ARITH_PROVE "m ~= (n::nat) ==> m < n | n < m") 1); |
|
686 by (etac disjE 1); |
|
687 by (rotate_tac 5 1); |
|
688 by (dres_inst_tac [("x","n")] spec 1); |
|
689 by Auto_tac; |
|
690 by (dres_inst_tac [("n","n")] partition_lt_gen 1); |
|
691 by Auto_tac; |
|
692 by (arith_tac 1); |
|
693 by (dres_inst_tac [("x","n")] spec 1); |
|
694 by (asm_full_simp_tac (simpset() addsimps [split_if]) 1); |
|
695 qed "lemma_additivity4_psize_eq"; |
|
696 |
|
697 Goal "partition (a, b) D \ |
|
698 \ ==> psize (%x. if D x < D n then D(x) else D n) <= psize D"; |
|
699 by (forw_inst_tac [("r","n")] partition_ub 1); |
|
700 by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1); |
|
701 by (auto_tac (claset(),simpset() addsimps |
|
702 [lemma_partition_eq RS sym])); |
|
703 by (forw_inst_tac [("r","n")] partition_lb 1); |
|
704 by (dtac lemma_additivity4_psize_eq 1); |
|
705 by (rtac ccontr 3 THEN Auto_tac); |
|
706 by (ftac (not_leE RSN (2,partition_eq_bound)) 1); |
|
707 by (auto_tac (claset(),simpset() addsimps [partition_rhs])); |
|
708 qed "lemma_psize_left_less_psize"; |
|
709 |
|
710 Goal "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |] \ |
|
711 \ ==> na < psize D"; |
|
712 by (etac (lemma_psize_left_less_psize RSN (2,less_le_trans)) 1); |
|
713 by (assume_tac 1); |
|
714 qed "lemma_psize_left_less_psize2"; |
|
715 |
|
716 |
|
717 Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \ |
|
718 \ n < psize D |] \ |
|
719 \ ==> False"; |
|
720 by (cut_inst_tac [("m","n"),("n","Suc na")] less_linear 1); |
|
721 by Auto_tac; |
|
722 by (dres_inst_tac [("n","n")] partition_lt_gen 2); |
|
723 by Auto_tac; |
|
724 by (cut_inst_tac [("m","psize D"),("n","na")] less_linear 1); |
|
725 by (auto_tac (claset(),simpset() addsimps [partition_rhs2])); |
|
726 by (dtac (ARITH_PROVE "n < Suc na ==> n < na | n = na") 1); |
|
727 by Auto_tac; |
|
728 by (dres_inst_tac [("n","na")] partition_lt_gen 1); |
|
729 by Auto_tac; |
|
730 val lemma_additivity3 = result(); |
|
731 |
|
732 Goalw [psize_def] "psize (%x. k) = 0"; |
|
733 by Auto_tac; |
|
734 qed "psize_const"; |
|
735 Addsimps [psize_const]; |
|
736 |
|
737 Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \ |
|
738 \ na < psize D |] \ |
|
739 \ ==> False"; |
|
740 by (forw_inst_tac [("m","n")] partition_lt_cancel 1); |
|
741 by (auto_tac (claset() addIs [lemma_additivity3],simpset())); |
|
742 val lemma_additivity3a = result(); |
|
743 |
|
744 Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D - n"; |
|
745 by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS |
|
746 meta_eq_to_obj_eq RS ssubst) 1); |
|
747 by (res_inst_tac [("a","psize D - n")] someI2 1); |
|
748 by Auto_tac; |
|
749 by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1); |
|
750 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
751 by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1); |
|
752 by (case_tac "psize D <= n" 1); |
|
753 by (dtac not_leE 2); |
|
754 by (asm_simp_tac (simpset() addsimps |
|
755 [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1); |
|
756 by (blast_tac (claset() addDs [partition_rhs2]) 1); |
|
757 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
758 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
759 by (dres_inst_tac [("x","psize D - n")] spec 1); |
|
760 by Auto_tac; |
|
761 by (ftac partition_rhs 1 THEN Step_tac 1); |
|
762 by (ftac partition_lt_cancel 1 THEN assume_tac 1); |
|
763 by (dtac (partition RS iffD1) 1 THEN Step_tac 1); |
|
764 by (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))" 1); |
|
765 by (Blast_tac 1); |
|
766 by (rotate_tac 6 1 THEN dres_inst_tac [("x","Suc (psize D)")] spec 1); |
|
767 by (Asm_simp_tac 1); |
|
768 qed "better_lemma_psize_right_eq1"; |
|
769 |
|
770 Goal "partition (a, D n) D ==> psize D <= n"; |
|
771 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
772 by (ftac partition_lt_Suc 1 THEN assume_tac 1); |
|
773 by (forw_inst_tac [("r","Suc n")] partition_ub 1); |
|
774 by Auto_tac; |
|
775 qed "psize_le_n"; |
|
776 |
|
777 Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D - n"; |
|
778 by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS |
|
779 meta_eq_to_obj_eq RS ssubst) 1); |
|
780 by (res_inst_tac [("a","psize D - n")] someI2 1); |
|
781 by Auto_tac; |
|
782 by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1); |
|
783 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
784 by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1); |
|
785 by (case_tac "psize D <= n" 1); |
|
786 by (dtac not_leE 2); |
|
787 by (asm_simp_tac (simpset() addsimps |
|
788 [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1); |
|
789 by (blast_tac (claset() addDs [partition_rhs2]) 1); |
|
790 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
791 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
792 by (ftac psize_le_n 1); |
|
793 by (dres_inst_tac [("x","psize D - n")] spec 1); |
|
794 by (asm_full_simp_tac (simpset() addsimps |
|
795 [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1); |
|
796 by (dtac (partition RS iffD1) 1 THEN Step_tac 1); |
|
797 by (rotate_tac 5 1 THEN dres_inst_tac [("x","Suc n")] spec 1); |
|
798 by Auto_tac; |
|
799 qed "better_lemma_psize_right_eq1a"; |
|
800 |
|
801 Goal "partition(a,b) D ==> psize (%x. D (x + n)) <= psize D - n"; |
|
802 by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1); |
|
803 by (blast_tac (claset() addIs [better_lemma_psize_right_eq1a, |
|
804 better_lemma_psize_right_eq1]) 1); |
|
805 qed "better_lemma_psize_right_eq"; |
|
806 |
|
807 Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D"; |
|
808 by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS |
|
809 meta_eq_to_obj_eq RS ssubst) 1); |
|
810 by (res_inst_tac [("a","psize D - n")] someI2 1); |
|
811 by Auto_tac; |
|
812 by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1); |
|
813 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
814 by (subgoal_tac "n <= psize D" 1); |
|
815 by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1); |
|
816 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
817 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
818 by (dtac (less_imp_le RSN (2,partition_rhs2)) 1); |
|
819 by Auto_tac; |
|
820 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
821 by (dres_inst_tac [("x","psize D")] spec 1); |
|
822 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
823 qed "lemma_psize_right_eq1"; |
|
824 |
|
825 (* should be combined with previous theorem; also proof has redundancy *) |
|
826 Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D"; |
|
827 by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS |
|
828 meta_eq_to_obj_eq RS ssubst) 1); |
|
829 by (res_inst_tac [("a","psize D - n")] someI2 1); |
|
830 by Auto_tac; |
|
831 by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1); |
|
832 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
833 by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1); |
|
834 by (case_tac "psize D <= n" 1); |
|
835 by (dtac not_leE 2); |
|
836 by (asm_simp_tac (simpset() addsimps |
|
837 [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1); |
|
838 by (blast_tac (claset() addDs [partition_rhs2]) 1); |
|
839 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
840 by (rtac ccontr 1 THEN dtac not_leE 1); |
|
841 by (dres_inst_tac [("x","psize D")] spec 1); |
|
842 by (asm_full_simp_tac (simpset() addsimps [partition]) 1); |
|
843 qed "lemma_psize_right_eq1a"; |
|
844 |
|
845 Goal "[| partition(a,b) D |] ==> psize (%x. D (x + n)) <= psize D"; |
|
846 by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1); |
|
847 by (blast_tac (claset() addIs [lemma_psize_right_eq1a,lemma_psize_right_eq1]) 1); |
|
848 qed "lemma_psize_right_eq"; |
|
849 |
|
850 Goal "[| a <= D n; tpart (a, b) (D, p) |] \ |
|
851 \ ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, \ |
|
852 \ %x. if D x < D n then p(x) else D n)"; |
|
853 by (forw_inst_tac [("r","n")] (tpart_partition RS partition_ub) 1); |
|
854 by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1); |
|
855 by (auto_tac (claset(),simpset() addsimps |
|
856 [tpart_partition RS lemma_partition_eq RS sym, |
|
857 tpart_tag_eq RS sym])); |
|
858 by (ftac (tpart_partition RSN (3,lemma_additivity1)) 1); |
|
859 by (auto_tac (claset(),simpset() addsimps [tpart_def])); |
|
860 by (dtac (real_leI RS real_le_imp_less_or_eq) 2); |
|
861 by (Auto_tac); |
|
862 by (blast_tac (claset() addDs [lemma_additivity3]) 2); |
|
863 by (dtac real_leI 2 THEN dres_inst_tac [("x","na")] spec 2); |
|
864 by (arith_tac 2); |
|
865 by (ftac lemma_additivity4_psize_eq 1); |
|
866 by (REPEAT(assume_tac 1)); |
|
867 by (rtac (partition RS iffD2) 1); |
|
868 by (ftac (partition RS iffD1) 1); |
|
869 by (auto_tac (claset() addIs [partition_lt_gen],simpset() addsimps [])); |
|
870 by (dres_inst_tac [("n","n")] partition_lt_gen 1); |
|
871 by (assume_tac 1 THEN arith_tac 1); |
|
872 by (Blast_tac 1); |
|
873 by (dtac partition_lt_cancel 1 THEN Auto_tac); |
|
874 qed "tpart_left1"; |
|
875 |
|
876 Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. a <= x & x <= D n) g;\ |
|
877 \ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \ |
|
878 \ else if x = D n then min (g (D n)) (ga (D n)) \ |
|
879 \ else min (ga x) ((x - D n)/ 2)) (D, p) |] \ |
|
880 \ ==> fine g \ |
|
881 \ (%x. if D x < D n then D(x) else D n, \ |
|
882 \ %x. if D x < D n then p(x) else D n)"; |
|
883 by (auto_tac (claset(),simpset() addsimps [fine_def,tpart_def,gauge_def])); |
|
884 by (ALLGOALS (ftac lemma_psize_left_less_psize2)); |
|
885 by (TRYALL(assume_tac)); |
|
886 by (ALLGOALS (dres_inst_tac [("x","na")] spec) THEN Auto_tac); |
|
887 by (ALLGOALS(dres_inst_tac [("x","na")] spec)); |
|
888 by Auto_tac; |
|
889 by (asm_full_simp_tac (simpset() addsimps [split_if]) 1); |
|
890 by (dtac (real_leI RS real_le_imp_less_or_eq) 1); |
|
891 by (Step_tac 1); |
|
892 by (blast_tac (claset() addDs [lemma_additivity3a]) 1); |
|
893 by (dtac sym 1 THEN Auto_tac); |
|
894 qed "fine_left1"; |
|
895 |
|
896 Goal "[| a <= D n; tpart (a, b) (D, p) |] \ |
|
897 \ ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"; |
|
898 by (asm_full_simp_tac (simpset() addsimps [tpart_def,partition_def]) 1); |
|
899 by (Step_tac 1); |
|
900 by (res_inst_tac [("x","N - n")] exI 1 THEN Auto_tac); |
|
901 by (rotate_tac 2 1); |
|
902 by (dres_inst_tac [("x","na + n")] spec 1); |
|
903 by (rotate_tac 3 2); |
|
904 by (dres_inst_tac [("x","na + n")] spec 2); |
|
905 by (ALLGOALS(arith_tac)); |
|
906 qed "tpart_right1"; |
|
907 |
|
908 Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. D n <= x & x <= b) ga;\ |
|
909 \ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \ |
|
910 \ else if x = D n then min (g (D n)) (ga (D n)) \ |
|
911 \ else min (ga x) ((x - D n)/ 2)) (D, p) |] \ |
|
912 \ ==> fine ga (%x. D(x + n),%x. p(x + n))"; |
|
913 by (auto_tac (claset(),simpset() addsimps [fine_def,gauge_def])); |
|
914 by (dres_inst_tac [("x","na + n")] spec 1); |
|
915 by (forw_inst_tac [("n","n")] (tpart_partition RS better_lemma_psize_right_eq) 1); |
|
916 by Auto_tac; |
|
917 by (arith_tac 1); |
|
918 by (asm_full_simp_tac (simpset() addsimps [tpart_def]) 1 THEN Step_tac 1); |
|
919 by (subgoal_tac "D n <= p (na + n)" 1); |
|
920 by (dres_inst_tac [("y","p (na + n)")] real_le_imp_less_or_eq 1); |
|
921 by (Step_tac 1); |
|
922 by (asm_full_simp_tac (simpset() addsimps [split_if]) 1); |
|
923 by (Asm_full_simp_tac 1); |
|
924 by (dtac less_le_trans 1 THEN assume_tac 1); |
|
925 by (rotate_tac 5 1); |
|
926 by (dres_inst_tac [("x","na + n")] spec 1 THEN Step_tac 1); |
|
927 by (rtac real_le_trans 1 THEN assume_tac 2); |
|
928 by (case_tac "na = 0" 1 THEN Auto_tac); |
|
929 by (rtac (partition_lt_gen RS order_less_imp_le) 1); |
|
930 by Auto_tac; |
|
931 by (arith_tac 1); |
|
932 qed "fine_right1"; |
|
933 |
|
934 Goalw [rsum_def] |
|
935 "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g"; |
|
936 by (auto_tac (claset(),simpset() addsimps [sumr_add,real_add_mult_distrib])); |
|
937 qed "rsum_add"; |
|
938 |
|
939 (* Bartle/Sherbert: Theorem 10.1.5 p. 278 *) |
|
940 Goalw [Integral_def] |
|
941 "[| a <= b; Integral(a,b) f k1; Integral(a,b) g k2 |] \ |
|
942 \ ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"; |
|
943 by Auto_tac; |
|
944 by (REPEAT(dres_inst_tac [("x","e/2")] spec 1)); |
|
945 by Auto_tac; |
|
946 by (dtac gauge_min 1 THEN assume_tac 1); |
|
947 by (res_inst_tac [("x","(%x. if ga x < gaa x then ga x else gaa x)")] exI 1); |
|
948 by Auto_tac; |
|
949 by (dtac fine_min 1); |
|
950 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
951 by (dres_inst_tac [("R1.0","abs (rsum (D, p) f - k1)* 2"), |
|
952 ("R2.0","abs (rsum (D, p) g - k2) * 2")] |
|
953 real_add_less_mono 1 THEN assume_tac 1); |
|
954 by (auto_tac (claset(),HOL_ss addsimps [rsum_add,real_add_mult_distrib RS sym, |
|
955 real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); |
|
956 by (arith_tac 1); |
|
957 qed "Integral_add_fun"; |
|
958 |
|
959 Goal "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r"; |
|
960 by (auto_tac (claset(),simpset() addsimps [partition])); |
|
961 qed "partition_lt_gen2"; |
|
962 |
|
963 Goalw [tpart_def] |
|
964 "[| ALL x. a <= x & x <= b --> f x <= g x; \ |
|
965 \ tpart(a,b) (D,p) \ |
|
966 \ |] ==> ALL n. n <= psize D --> f (p n) <= g (p n)"; |
|
967 by (Auto_tac THEN ftac (partition RS iffD1) 1); |
|
968 by Auto_tac; |
|
969 by (dres_inst_tac [("x","p n")] spec 1); |
|
970 by Auto_tac; |
|
971 by (case_tac "n = 0" 1); |
|
972 by (rtac (partition_lt_gen RS order_less_le_trans RS order_less_imp_le) 2); |
|
973 by Auto_tac; |
|
974 by (dtac le_imp_less_or_eq 1 THEN Auto_tac); |
|
975 by (dres_inst_tac [("x","psize D")] spec 2 THEN Auto_tac); |
|
976 by (dres_inst_tac [("r","Suc n")] partition_ub 1); |
|
977 by (dres_inst_tac [("x","n")] spec 1); |
|
978 by Auto_tac; |
|
979 qed "lemma_Integral_le"; |
|
980 |
|
981 Goalw [rsum_def] |
|
982 "[| ALL x. a <= x & x <= b --> f x <= g x; \ |
|
983 \ tpart(a,b) (D,p) \ |
|
984 \ |] ==> rsum(D,p) f <= rsum(D,p) g"; |
|
985 by (auto_tac (claset() addSIs [sumr_le2] addDs |
|
986 [tpart_partition RS partition_lt_gen2] addSDs |
|
987 [lemma_Integral_le],simpset())); |
|
988 qed "lemma_Integral_rsum_le"; |
|
989 |
|
990 Goalw [Integral_def] |
|
991 "[| a <= b; \ |
|
992 \ ALL x. a <= x & x <= b --> f(x) <= g(x); \ |
|
993 \ Integral(a,b) f k1; Integral(a,b) g k2 \ |
|
994 \ |] ==> k1 <= k2"; |
|
995 by Auto_tac; |
|
996 by (rotate_tac 2 1); |
|
997 by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1); |
|
998 by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1); |
|
999 by Auto_tac; |
|
1000 by (dtac gauge_min 1 THEN assume_tac 1); |
|
1001 by (dres_inst_tac [("g","%x. if ga x < gaa x then ga x else gaa x")] |
|
1002 partition_exists 1 THEN assume_tac 1); |
|
1003 by Auto_tac; |
|
1004 by (dtac fine_min 1); |
|
1005 by (dres_inst_tac [("x","D")] spec 1 THEN dres_inst_tac [("x","D")] spec 1); |
|
1006 by (dres_inst_tac [("x","p")] spec 1 THEN dres_inst_tac [("x","p")] spec 1); |
|
1007 by Auto_tac; |
|
1008 by (ftac lemma_Integral_rsum_le 1 THEN assume_tac 1); |
|
1009 by (subgoal_tac |
|
1010 "abs((rsum(D,p) f - k1) - (rsum(D,p) g - k2)) < abs(k1 - k2)" 1); |
|
1011 by (arith_tac 1); |
|
1012 by (dtac real_add_less_mono 1 THEN assume_tac 1); |
|
1013 by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, |
|
1014 real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); |
|
1015 by (arith_tac 1); |
|
1016 qed "Integral_le"; |
|
1017 |
|
1018 Goalw [Integral_def] |
|
1019 "(EX k. Integral(a,b) f k) ==> \ |
|
1020 \ (ALL e. 0 < e --> \ |
|
1021 \ (EX g. gauge (%x. a <= x & x <= b) g & \ |
|
1022 \ (ALL D1 D2 p1 p2. \ |
|
1023 \ tpart(a,b) (D1, p1) & fine g (D1,p1) & \ |
|
1024 \ tpart(a,b) (D2, p2) & fine g (D2,p2) --> \ |
|
1025 \ abs(rsum(D1,p1) f - rsum(D2,p2) f) < e)))"; |
|
1026 by Auto_tac; |
|
1027 by (dres_inst_tac [("x","e/2")] spec 1); |
|
1028 by Auto_tac; |
|
1029 by (rtac exI 1 THEN Auto_tac); |
|
1030 by (forw_inst_tac [("x","D1")] spec 1); |
|
1031 by (forw_inst_tac [("x","D2")] spec 1); |
|
1032 by (REPEAT(dtac spec 1) THEN Auto_tac); |
|
1033 by (thin_tac "0 < e" 1); |
|
1034 by (dtac real_add_less_mono 1 THEN assume_tac 1); |
|
1035 by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, |
|
1036 real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); |
|
1037 by (arith_tac 1); |
|
1038 qed "Integral_imp_Cauchy"; |
|
1039 |
|
1040 Goalw [Cauchy_def] |
|
1041 "Cauchy X = \ |
|
1042 \ (ALL j. (EX M. ALL m n. M <= m & M <= n --> \ |
|
1043 \ abs (X m + - X n) < inverse(real (Suc j))))"; |
|
1044 by Auto_tac; |
|
1045 by (dtac reals_Archimedean 1); |
|
1046 by (Step_tac 1); |
|
1047 by (dres_inst_tac [("x","n")] spec 1); |
|
1048 by Auto_tac; |
|
1049 by (res_inst_tac [("x","M")] exI 1); |
|
1050 by Auto_tac; |
|
1051 by (dres_inst_tac [("x","m")] spec 1); |
|
1052 by (dres_inst_tac [("x","na")] spec 1); |
|
1053 by Auto_tac; |
|
1054 qed "Cauchy_iff2"; |
|
1055 |
|
1056 Goal "[| a <= b; ALL n. gauge (%x. a <= x & x <= b) (fa n) |] \ |
|
1057 \ ==> ALL n. EX D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"; |
|
1058 by (Step_tac 1); |
|
1059 by (rtac partition_exists 1 THEN Auto_tac); |
|
1060 qed "partition_exists2"; |
|
1061 |
|
1062 Goal "[| a <= b; ALL c. a <= c & c <= b --> f' c <= g' c; \ |
|
1063 \ ALL x. DERIV f x :> f' x; ALL x. DERIV g x :> g' x \ |
|
1064 \ |] ==> f b - f a <= g b - g a"; |
|
1065 by (rtac Integral_le 1); |
|
1066 by (assume_tac 1); |
|
1067 by (rtac FTC1 2); |
|
1068 by (rtac FTC1 4); |
|
1069 by Auto_tac; |
|
1070 qed "monotonic_anti_derivative"; |