1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: QZYZMJC *)
6 (* Chaper : Packing (Marchal cells) *)
8 (* ========================================================================= *)
11 (* ========================================================================= *)
12 (* The lemma statement has been corrected *)
14 module Qzyzmjc = struct
18 open Vukhacky_tactics;;
25 open Marchal_cells_2_new;;
38 saturated V /\ packing V /\ v IN V
39 ==> sum {X | mcell_set V X /\ v IN VX V X} (\t. sol v t) = &4 * pi`;;
41 (* ========================================================================= *)
43 let mcell_set_2 = prove_by_refinement (
44 `!V:real^3->bool. mcell_set V =
45 {X | ?i ul. X = mcell i V ul /\ ul IN barV V 3 /\ i <= 4}`,
47 [(REWRITE_TAC[mcell_set] THEN GEN_TAC);
48 (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> B = A`));
51 (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
52 (ASM_CASES_TAC `i <= 4`);
53 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
55 (EXISTS_TAC `4:num` THEN EXISTS_TAC `ul:(real^3)list`);
56 (ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
57 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(i <= 4) ==> (i >= 4)`;
58 ARITH_RULE `4 >= 4`])]);;
60 (* ========================================================================= *)
62 let BARV_3_IMP_FINITE_lemma1 = prove_by_refinement(
64 packing V /\ saturated V /\ barV V 3 ul /\ {u, v} SUBSET set_of_list ul
68 (NEW_GOAL `?a. voronoi_list V ul = {a} /\
69 a = circumcenter (set_of_list ul) /\
70 hl ul = dist (HD ul,a)`);
71 (MATCH_MP_TAC VORONOI_LIST_3_SINGLETON_EXPLICIT);
73 (UP_ASM_TAC THEN STRIP_TAC);
74 (NEW_GOAL `!s. s IN set_of_list ul ==> dist (a, s:real^3) < &2`);
76 (NEW_GOAL `?y. y IN V /\ dist (a,y:real^3) < &2`);
77 (ASM_MESON_TAC[saturated]);
78 (UP_ASM_TAC THEN STRIP_TAC);
79 (SUBGOAL_THEN `a IN voronoi_list V ul` MP_TAC);
81 (REWRITE_TAC[VORONOI_LIST; VORONOI_SET; voronoi_closed; IN_INTERS]);
83 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,s:real^3) <= dist (x,w)}`);
84 (FIRST_ASSUM MATCH_MP_TAC);
86 (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
87 (NEW_GOAL `dist (a,s) <= dist (a, y:real^3)`);
88 (FIRST_ASSUM MATCH_MP_TAC);
91 (NEW_GOAL `dist (u, v:real^3) <= dist (u,a) + dist (a,v)`);
92 (REWRITE_TAC[DIST_TRIANGLE]);
93 (NEW_GOAL `dist (u,a:real^3) < &2`);
94 (ONCE_REWRITE_TAC[DIST_SYM]);
95 (FIRST_ASSUM MATCH_MP_TAC);
97 (NEW_GOAL `dist (a,v:real^3) < &2`);
98 (FIRST_ASSUM MATCH_MP_TAC);
100 (ASM_REAL_ARITH_TAC)]);;
102 (* ========================================================================= *)
104 let BARV_3_IMP_FINITE_lemma2 = prove_by_refinement (
105 `!V ul v k. packing V /\ saturated V /\ barV V 3 ul /\ v IN set_of_list ul
106 ==> set_of_list ul SUBSET ball (v, &4)`,
107 [(REWRITE_TAC[SUBSET; ball; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
108 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma1);
109 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `ul:(real^3)list`);
110 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[])]);;
111 (* ========================================================================= *)
114 let lemma_r_r'_fix2 = prove_by_refinement (
116 measurable C /\ radial_norm r x C /\ s > &0 /\ s <= r
117 ==> measurable (C INTER normball x s) /\
118 vol (C INTER normball x s) = vol C * (s / r) pow 3 `,
120 (ASM_CASES_TAC `s < r`);
121 (ASM_MESON_TAC[Vol1.lemma_r_r'_fix]);
123 (NEW_GOAL `s = r:real`);
124 (ASM_REAL_ARITH_TAC);
126 (REWRITE_WITH `C INTER normball x r = C:real^3->bool`);
127 (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> A INTER B = A`));
128 (UNDISCH_TAC `radial_norm r (x:real^3) C`);
129 (REWRITE_TAC[GSYM RADIAL_VS_RADIAL_NORM; radial; NORMBALL_BALL] THEN SET_TAC[]);
131 (REWRITE_WITH `r / r = &1`);
132 (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC);
135 (* ========================================================================= *)
137 let MCELL_SET_NOT_EMPTY = prove_by_refinement (
139 saturated V /\ packing V /\ v IN V
140 ==> ~({X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X} = {})`,
142 [(REWRITE_TAC[mcell_set; SET_RULE `~(s = {}) <=> (?x. x IN s)`; IN;
146 (ASM_CASES_TAC `!i ul. 1 <= i /\ i <= 4 /\ barV V 3 ul /\
147 truncate_simplex 0 ul = [v] ==>
148 negligible (mcell i V ul)`);
149 (NEW_GOAL `!vl. barV V 3 vl /\
150 truncate_simplex 0 vl = [v] ==>
151 negligible (rogers V vl INTER ball (v, sqrt (&2)))`);
154 (NEW_GOAL `vol (rogers V vl) <=
155 vol (UNIONS {x | ?i. i <= 4 /\ x = mcell i V vl})`);
156 (MATCH_MP_TAC MEASURE_SUBSET);
158 (MATCH_MP_TAC MEASURABLE_ROGERS);
161 (MATCH_MP_TAC MEASURABLE_UNIONS);
163 (REWRITE_TAC[GSYM IN_NUMSEG_0]);
164 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
165 (REWRITE_TAC[FINITE_NUMSEG]);
166 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
167 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
170 (REWRITE_TAC[SUBSET]);
172 (REWRITE_TAC[IN_UNIONS; IN;IN_ELIM_THM]);
174 (NEW_GOAL `?i. i <= 4 /\ x IN mcell i V vl`);
175 (MATCH_MP_TAC SLTSTLO1);
177 (UP_ASM_TAC THEN STRIP_TAC);
178 (EXISTS_TAC `mcell i V vl`);
180 (EXISTS_TAC `i:num`);
182 (UP_ASM_TAC THEN REWRITE_TAC[IN]);
185 (UP_ASM_TAC THEN REWRITE_WITH
186 `UNIONS {x | ?i. i <= 4 /\ x = mcell i V vl} =
187 UNIONS {x | ?i. 1 <= i /\ i <= 4 /\ x = mcell i V vl} UNION (mcell 0 V vl)`);
188 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_UNIONS; IN_UNION]);
190 (ASM_CASES_TAC `i = 0`);
194 (EXISTS_TAC `t:real^3->bool`);
196 (EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]);
198 (EXISTS_TAC `t:real^3->bool`);
200 (EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]);
201 (EXISTS_TAC `mcell 0 V vl`);
203 (EXISTS_TAC `0` THEN ASM_REWRITE_TAC[]);
206 (ABBREV_TAC `S1 = UNIONS {x | ?i. 1 <= i /\ i <= 4 /\ x = mcell i V vl}`);
207 (REWRITE_WITH `vol (S1 UNION mcell 0 V vl) =
208 vol (S1) + vol (mcell 0 V vl) - vol (S1 INTER mcell 0 V vl)`);
209 (MATCH_MP_TAC MEASURE_UNION);
211 (EXPAND_TAC "S1" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
213 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
214 (REWRITE_TAC[GSYM IN_NUMSEG]);
215 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
216 (REWRITE_TAC[FINITE_NUMSEG]);
217 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
218 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
220 (MATCH_MP_TAC MEASURABLE_MCELL);
222 (NEW_GOAL `vol S1 = &0`);
224 (MATCH_MP_TAC MEASURE_EQ_0);
225 (EXPAND_TAC "S1" THEN MATCH_MP_TAC NEGLIGIBLE_UNIONS);
227 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
228 (REWRITE_TAC[GSYM IN_NUMSEG]);
229 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
230 (REWRITE_TAC[FINITE_NUMSEG]);
231 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
233 (FIRST_ASSUM MATCH_MP_TAC);
236 (NEW_GOAL `vol (S1 INTER mcell 0 V vl) = &0`);
237 (MATCH_MP_TAC MEASURE_EQ_0);
238 (MATCH_MP_TAC NEGLIGIBLE_INTER);
240 (REWRITE_WITH `NULLSET S1 <=> vol S1 = &0`);
241 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
242 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
244 (EXPAND_TAC "S1" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
246 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
247 (REWRITE_TAC[GSYM IN_NUMSEG]);
248 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
249 (REWRITE_TAC[FINITE_NUMSEG]);
250 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
251 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
255 (ASM_REWRITE_TAC[REAL_ARITH `&0 + a - &0 = a`]);
257 (ABBREV_TAC `S2 = rogers V vl INTER ball (v,sqrt (&2))`);
258 (ABBREV_TAC `S3 = rogers V vl DIFF ball (v,sqrt (&2))`);
259 (REWRITE_WITH `mcell 0 V vl = S3`);
260 (REWRITE_TAC[mcell0; MCELL_EXPLICIT]);
262 (REWRITE_WITH `HD vl = v:real^3`);
263 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 0 vl)`);
264 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
265 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
266 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
267 (MATCH_MP_TAC BARV_3_EXPLICIT);
268 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
269 (UP_ASM_TAC THEN STRIP_TAC);
270 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
271 (ASM_REWRITE_TAC[HD]);
272 (REWRITE_WITH `rogers V vl = S2 UNION S3`);
274 (REWRITE_WITH `vol (S2 UNION S3) = vol (S2) + vol (S3) - vol (S2 INTER S3)`);
275 (MATCH_MP_TAC MEASURE_UNION);
276 (EXPAND_TAC "S2" THEN EXPAND_TAC "S3");
278 (MATCH_MP_TAC MEASURABLE_INTER);
279 (REWRITE_TAC[MEASURABLE_BALL]);
280 (MATCH_MP_TAC MEASURABLE_ROGERS);
282 (MATCH_MP_TAC MEASURABLE_DIFF);
283 (REWRITE_TAC[MEASURABLE_BALL]);
284 (MATCH_MP_TAC MEASURABLE_ROGERS);
287 (REWRITE_WITH `S2 INTER S3 = {}:real^3->bool`);
289 (REWRITE_TAC[MEASURE_EMPTY; REAL_ARITH `a + b - &0 <= b <=> a <= &0`]);
290 (NEW_GOAL `&0 <= vol S2`);
291 (MATCH_MP_TAC MEASURE_POS_LE);
293 (EXPAND_TAC "S2" THEN MATCH_MP_TAC MEASURABLE_INTER);
294 (REWRITE_TAC[MEASURABLE_BALL]);
295 (MATCH_MP_TAC MEASURABLE_ROGERS THEN ASM_REWRITE_TAC[]);
297 (REWRITE_WITH `NULLSET S2 <=> vol S2 = &0`);
298 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
299 (EXPAND_TAC "S2" THEN MATCH_MP_TAC MEASURABLE_INTER);
300 (REWRITE_TAC[MEASURABLE_BALL]);
301 (MATCH_MP_TAC MEASURABLE_ROGERS THEN ASM_REWRITE_TAC[]);
302 (ASM_REAL_ARITH_TAC);
304 (NEW_GOAL `voronoi_closed V v =
305 UNIONS {y| ?vl. vl IN barV V 3 /\
307 truncate_simplex 0 vl = [v:real^3]}`);
308 (ONCE_REWRITE_TAC[SET_RULE `s = t <=> (!x. x IN s <=> x IN t)`]);
310 (REWRITE_WITH `!x. x IN voronoi_closed V v <=>
311 (?vl. vl IN barV V 3 /\
313 truncate_simplex 0 vl = [v])`);
314 (GEN_TAC THEN MATCH_MP_TAC GLTVHUM);
317 (REWRITE_TAC[IN_UNIONS; IN; IN_ELIM_THM]);
321 (EXISTS_TAC `rogers V vl` THEN ASM_REWRITE_TAC[]);
322 (EXISTS_TAC `vl:(real^3)list` THEN ASM_REWRITE_TAC[]);
324 (EXISTS_TAC `vl:(real^3)list` THEN ASM_REWRITE_TAC[]);
327 (NEW_GOAL `voronoi_closed V v INTER ball (v,sqrt (&2)) =
329 {y | ?vl. vl IN barV V 3 /\
330 y = rogers V vl INTER ball (v,sqrt (&2)) /\
331 truncate_simplex 0 vl = [v]}`);
333 (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
334 (REWRITE_TAC[IN_INTER; IN_UNIONS]);
335 (ONCE_REWRITE_TAC[IN]);
336 (REWRITE_TAC[IN_ELIM_THM]);
339 (EXISTS_TAC `rogers V vl INTER ball (v,sqrt (&2))`);
341 (EXISTS_TAC `vl:(real^3)list`);
343 (REWRITE_TAC[MESON[IN] `(a INTER b) x <=> x IN (a INTER b)`]);
344 (ASM_SIMP_TAC[IN_INTER]);
347 (EXISTS_TAC `rogers V vl`);
349 (EXISTS_TAC `vl:(real^3)list`);
354 (NEW_GOAL `NULLSET (voronoi_closed V v INTER ball (v,sqrt (&2)))`);
356 (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
357 (REWRITE_TAC[IN; IN_ELIM_THM]);
361 (ABBREV_TAC `s2 = V INTER ball (v:real^3, &4)`);
362 (ABBREV_TAC `s3 = {ul | ?u0 u1 u2 u3.
367 ul = [u0; u1; u2; u3:real^3]}`);
368 (ABBREV_TAC `f = (\t. rogers V t INTER ball (v:real^3,sqrt (&2)))`);
369 (MATCH_MP_TAC FINITE_SUBSET);
371 (EXISTS_TAC `{y | ?vl. vl IN s3 /\y = (f:((real^3)list)->real^3->bool) vl}`);
373 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
375 (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
377 (MATCH_MP_TAC Pack1.KIUMVTC);
378 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
380 (EXPAND_TAC "f" THEN EXPAND_TAC "s3");
381 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC);
382 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
383 (MATCH_MP_TAC BARV_3_EXPLICIT);
384 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
385 (UP_ASM_TAC THEN STRIP_TAC);
386 (EXISTS_TAC `vl:(real^3)list`);
388 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
389 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
392 (NEW_GOAL `!s:real^3. s IN set_of_list vl ==> s IN s2`);
393 (REPEAT STRIP_TAC THEN EXPAND_TAC "s2");
395 (NEW_GOAL `set_of_list vl SUBSET (V INTER ball (v:real^3, &4))`);
396 (REWRITE_TAC[SUBSET_INTER]);
398 (MATCH_MP_TAC Packing3.BARV_SUBSET);
399 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
401 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma2);
402 (EXISTS_TAC `V:real^3->bool`);
404 (NEW_GOAL `v = HD [v:real^3]`);
406 (ONCE_REWRITE_TAC[ASSUME `v = HD [v:real^3]`]);
407 (REWRITE_TAC[GSYM (ASSUME `truncate_simplex 0 vl = [v:real^3]`)]);
408 (REWRITE_TAC[ASSUME `vl = [u0; u1; u2; u3:real^3]`]);
409 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; HD;set_of_list]);
411 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
413 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
414 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
415 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
416 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
421 (NEW_GOAL `NULLSET (ball (v, &1))`);
422 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
423 (EXISTS_TAC `voronoi_closed V v INTER ball (v:real^3,sqrt (&2))`);
426 (REWRITE_TAC[SUBSET; IN_INTER; IN_BALL; voronoi_closed]);
427 (REWRITE_TAC[IN; IN_ELIM_THM]);
429 (ASM_CASES_TAC `w = v:real^3`);
430 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
431 (NEW_GOAL `dist (v,w) <= dist (v, x) + dist (x, w:real^3)`);
432 (REWRITE_TAC[DIST_TRIANGLE]);
433 (NEW_GOAL `&2 <= dist (v,w:real^3)`);
434 (UNDISCH_TAC `packing (V:real^3->bool)`);
435 (REWRITE_TAC[packing] THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
437 (REWRITE_WITH `dist (x,v) = dist (v,x:real^3)`);
438 (REWRITE_TAC[DIST_SYM]);
439 (ASM_REAL_ARITH_TAC);
440 (NEW_GOAL `&1 < sqrt (&2)`);
441 (REWRITE_WITH `&1 < sqrt (&2) <=> &1 pow 2 < sqrt (&2) pow 2`);
442 (MATCH_MP_TAC Pack1.bp_bdt);
443 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
444 (ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
446 (ASM_REAL_ARITH_TAC);
448 (NEW_GOAL `vol (ball (v, &1)) = &4 / &3 * pi * (&1) pow 3`);
449 (ASM_SIMP_TAC[REAL_ARITH `&0 <= &1`; VOLUME_BALL]);
450 (NEW_GOAL `vol (ball (v, &1)) > &0`);
451 (ASM_REWRITE_TAC[REAL_ARITH `&4 / &3 * pi * &1 pow 3 > &0 <=>
452 &0 < &4 / &3 * pi`]);
453 (MATCH_MP_TAC REAL_LT_MUL);
455 (MATCH_MP_TAC REAL_LT_DIV THEN REAL_ARITH_TAC);
456 (REWRITE_TAC[PI_POS]);
458 (NEW_GOAL `vol (ball (v,&1)) = &0`);
459 (REWRITE_WITH `vol (ball (v,&1)) = &0 <=> NULLSET (ball (v,&1))`);
460 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
461 (REWRITE_TAC[MEASURABLE_BALL]);
463 (ASM_REAL_ARITH_TAC);
466 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE
467 `~(!i ul. 1 <= i /\ i <= 4 /\ barV V 3 ul /\ truncate_simplex 0 ul = [v]
468 ==> NULLSET (mcell i V ul)) <=>
469 (?i ul. 1 <= i /\ i <= 4 /\ barV V 3 ul /\ truncate_simplex 0 ul = [v] /\
470 ~NULLSET (mcell i V ul))`]);
472 (EXISTS_TAC `mcell i V ul`);
474 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
478 (NEW_GOAL `V INTER mcell i V ul =
479 set_of_list (truncate_simplex (i - 1) ul)`);
480 (MATCH_MP_TAC LEPJBDJ);
483 (UNDISCH_TAC `~NULLSET (mcell i V ul) ` THEN
484 ASM_REWRITE_TAC[NEGLIGIBLE_EMPTY]);
487 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
488 (MATCH_MP_TAC BARV_3_EXPLICIT);
489 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
490 (UP_ASM_TAC THEN STRIP_TAC);
491 (NEW_GOAL `set_of_list (truncate_simplex 0 ul) SUBSET
492 set_of_list (truncate_simplex (i-1) (ul:(real^3)list))`);
493 (MATCH_MP_TAC Rogers.TRUNCATE_SIMPLEX_SUBSET);
494 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
495 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
498 (* ======================================================================= *)
500 (* ======================================================================= *)
503 let QZYZMJC = prove_by_refinement ( QZYZMJC1_concl,
507 (* Simplify the set *)
509 `{X | mcell_set V X /\ v IN VX V X} =
510 {X | mcell_set V X /\ ~(negligible X) /\ v IN V INTER X}`);
511 (REWRITE_TAC[SET_EQ_LEMMA]);
513 (REWRITE_TAC[IN; IN_ELIM_THM]);
516 (NEW_GOAL `v IN VX V x`);
519 (ASM_CASES_TAC `negligible (x:real^3->bool)`);
526 (NEW_GOAL `x IN mcell_set V`);
528 (UP_ASM_TAC THEN REWRITE_TAC[mcell_set;IN;IN_ELIM_THM]);
531 (REWRITE_WITH `V INTER x = VX V x`);
532 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
533 (MATCH_MP_TAC HDTFNFZ);
534 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
538 (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
540 (REWRITE_WITH `VX V x = V INTER x`);
541 (MATCH_MP_TAC HDTFNFZ);
542 (NEW_GOAL `x IN mcell_set V`);
544 (UP_ASM_TAC THEN REWRITE_TAC[mcell_set;IN;IN_ELIM_THM]);
546 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
548 (REWRITE_TAC[GSYM (ASSUME `x = mcell i V ul`)] THEN ASM_SET_TAC[]);
549 (REWRITE_TAC[MESON [IN] `(V INTER x) v <=> v IN V INTER x`]);
551 (* finish simplifyng the set *)
553 (* -------------------------------------------------------------------------- *)
554 (* begin to prove the set is finite *)
557 (NEW_GOAL `FINITE {X | mcell_set V X /\ v IN V INTER X}`);
558 (REWRITE_TAC[mcell_set_2; IN_ELIM_THM]);
559 (ABBREV_TAC `s = {(i, ul)| barV V 3 ul /\ v IN V INTER mcell i V ul /\ i <= 4}`);
560 (ABBREV_TAC `f = (\x:num#(real^3)list. mcell (FST x) V (SND x))`);
563 `{X |(?i ul. X = mcell i V ul /\ ul IN barV V 3/\ i <= 4) /\ v IN V INTER X}
564 = {X | ?y:num#(real^3)list. y IN s /\ X = f y}`);
566 (EXPAND_TAC "s" THEN EXPAND_TAC "f");
567 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN]);
568 (REWRITE_TAC[IN_ELIM_THM]);
570 (EXISTS_TAC `(i:num, ul:(real^3)list)`);
571 (ASM_REWRITE_TAC[FST;SND]);
572 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
573 (REWRITE_TAC[GSYM (ASSUME `x = mcell i V ul`)]);
574 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
575 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
576 (ASM_REWRITE_TAC[IN]);
579 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
581 (ABBREV_TAC `s1 = {0,1,2,3,4}`);
582 (ABBREV_TAC `s2 = V INTER ball (v:real^3, &4)`);
583 (ABBREV_TAC `s3 = {ul | ?u0 u1 u2 u3.
588 ul = [u0; u1; u2; u3:real^3]}`);
589 (MATCH_MP_TAC FINITE_SUBSET);
590 (EXISTS_TAC `{(i:num, ul:(real^3)list)| i IN s1 /\ ul IN s3}`);
592 (MATCH_MP_TAC FINITE_PRODUCT);
593 (EXPAND_TAC "s1" THEN EXPAND_TAC "s3");
594 (REWRITE_TAC[Geomdetail.FINITE6]);
595 (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
596 (EXPAND_TAC "s2" THEN MATCH_MP_TAC Pack1.KIUMVTC);
597 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
598 (EXPAND_TAC "s1" THEN EXPAND_TAC "s3" THEN REWRITE_TAC[SUBSET]);
599 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
601 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
603 (REWRITE_TAC[SET_RULE `i IN {0,1,2,3,4} <=> i = 0\/i=1\/i=2\/i=3\/i=4`]);
605 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
606 (MATCH_MP_TAC BARV_3_EXPLICIT);
607 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
608 (UP_ASM_TAC THEN STRIP_TAC);
609 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
610 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
612 (NEW_GOAL `!s:real^3. s IN set_of_list ul ==> s IN s2`);
613 (REPEAT STRIP_TAC THEN EXPAND_TAC "s2");
615 (NEW_GOAL `set_of_list ul SUBSET (V INTER ball (v:real^3, &4))`);
616 (REWRITE_TAC[SUBSET_INTER]);
618 (MATCH_MP_TAC Packing3.BARV_SUBSET);
619 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
620 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma2);
621 (EXISTS_TAC `V:real^3->bool`);
624 (NEW_GOAL `V INTER mcell i V ul = set_of_list(truncate_simplex (i - 1) ul)`);
625 (MATCH_MP_TAC LEPJBDJ);
630 (ASM_CASES_TAC `i = 0`);
631 (UNDISCH_TAC `v IN V INTER mcell i V ul`);
632 (REWRITE_TAC[ASSUME `i = 0`; MCELL_EXPLICIT; mcell0; IN_INTER; IN_DIFF]);
635 (NEW_GOAL `v:real^3 = HD ul`);
636 (MATCH_MP_TAC Marchal_cells_2_new.ROGERS_INTER_V_LEMMA);
637 (EXISTS_TAC `V:real^3->bool`);
638 (REWRITE_TAC[MESON[IN] `rogers V ul v <=> v IN rogers V ul`]);
640 (UNDISCH_TAC `~(v:real^3 IN ball (HD ul,sqrt (&2)))`);
641 (ASM_REWRITE_TAC[IN_BALL; DIST_REFL]);
642 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
648 (NEW_GOAL `set_of_list (truncate_simplex (i - 1) ul) SUBSET
649 set_of_list (ul:(real^3)list)`);
650 (MATCH_MP_TAC Rogers.SET_OF_LIST_TRUNCATE_SIMPLEX_SUBSET);
651 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
652 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
657 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
658 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
659 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
660 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
663 (* finish to prove the set is finite *)
664 (* -------------------------------------------------------------------------- *)
666 (NEW_GOAL `FINITE {X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X}`);
667 (MATCH_MP_TAC FINITE_SUBSET);
668 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
673 (ABBREV_TAC `S = {X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X}`);
675 `P = (\X r. X IN S ==> r > &0 /\ radial r v (X INTER ball (v:real^3,r)))`);
676 (NEW_GOAL `?f:(real^3->bool)->real. (!X:real^3->bool. P X (f X))`);
677 (REWRITE_TAC[GSYM SKOLEM_THM]);
680 (ASM_CASES_TAC `X:real^3 ->bool IN S`);
681 (NEW_GOAL `?c. c > &0 /\ radial c v (X INTER ball (v:real^3,c))`);
682 (REWRITE_TAC[GSYM eventually_radial]);
683 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM;mcell_set]);
685 (ONCE_ASM_REWRITE_TAC[]);
686 (MATCH_MP_TAC URRPHBZ2);
687 (ASM_REWRITE_TAC[] THEN UP_ASM_TAC THEN SET_TAC[]);
688 (UP_ASM_TAC THEN STRIP_TAC);
689 (EXISTS_TAC `c:real`);
690 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
696 (UP_ASM_TAC THEN STRIP_TAC);
697 (UP_ASM_TAC THEN EXPAND_TAC "P" THEN STRIP_TAC);
699 `sum S (\t. sol v t) =
700 sum S (\t. &3 * vol (t INTER normball v (f t)) / (f t) pow 3)`);
701 (MATCH_MP_TAC SUM_EQ);
702 (REWRITE_TAC[BETA_THM]);
706 (ASM_SIMP_TAC[NORMBALL_BALL; GSYM RADIAL_VS_RADIAL_NORM]);
707 (MATCH_MP_TAC MEASURABLE_INTER);
708 (REWRITE_TAC[MEASURABLE_BALL]);
709 (UP_ASM_TAC THEN EXPAND_TAC"S" THEN REWRITE_TAC[IN;IN_ELIM_THM;mcell_set]);
710 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
711 (ASM_SIMP_TAC[MEASURABLE_MCELL]);
713 (NEW_GOAL `~(S:(real^3->bool)->bool = {})`);
715 (MATCH_MP_TAC MCELL_SET_NOT_EMPTY);
718 (NEW_GOAL `?r. r > &0 /\ r < &1 /\ !x:real^3->bool. x IN S ==> r <= f x`);
719 (NEW_GOAL `?r. r > &0 /\ !x:real^3->bool. x IN S ==> r <= f x`);
720 (NEW_GOAL `?r. r IN (IMAGE f (S:(real^3->bool)->bool)) /\
721 (!x. x IN (IMAGE f S) ==> r <= x)`);
722 (MATCH_MP_TAC INF_FINITE_LEMMA);
724 (ASM_SIMP_TAC[FINITE_IMAGE]);
725 (REWRITE_TAC[IMAGE_EQ_EMPTY]);
727 (UP_ASM_TAC THEN STRIP_TAC);
729 (UNDISCH_TAC `r IN IMAGE (f:(real^3->bool)->real) S`);
730 (REWRITE_TAC[IMAGE]);
731 (ONCE_REWRITE_TAC[IN]);
732 (REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
733 (EXISTS_TAC `r:real`);
738 (FIRST_ASSUM MATCH_MP_TAC);
739 (REWRITE_TAC[IMAGE; IN; IN_ELIM_THM]);
740 (EXISTS_TAC `x':real^3->bool` THEN ASM_REWRITE_TAC[]);
741 (UP_ASM_TAC THEN STRIP_TAC);
742 (EXISTS_TAC `min r (inv(&2))`);
743 (NEW_GOAL `inv (&2) > &0 /\ inv (&2) < &1`);
745 (REWRITE_TAC[REAL_ARITH `a > b <=> b < a`]);
746 (ASM_SIMP_TAC[REAL_LT_MIN]);
748 (ASM_REAL_ARITH_TAC);
749 (ASM_SIMP_TAC[REAL_MIN_LT]);
750 (ASM_SIMP_TAC[REAL_MIN_LE]);
751 (UP_ASM_TAC THEN STRIP_TAC);
754 `sum S (\t. &3 * vol (t INTER normball v (f t)) / f t pow 3)
755 = sum S (\t. &3 * vol (t INTER normball (v:real^3) r) / r pow 3)`);
756 (MATCH_MP_TAC SUM_EQ);
757 (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
758 (ABBREV_TAC `C:real^3->bool = x INTER normball v (f x)`);
759 (REWRITE_WITH `x INTER normball v r = C INTER normball (v:real^3) r`);
761 (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> x INTER A = (x INTER B) INTER A`));
762 (REWRITE_TAC[normball; SUBSET;IN;IN_ELIM_THM]);
763 (NEW_GOAL `r <= f (x:real^3->bool)`);
765 (ASM_REAL_ARITH_TAC);
767 (REWRITE_WITH `measurable (C INTER normball v r) /\
768 vol (C INTER normball v r) =
769 vol C * (r / f (x:real^3->bool)) pow 3`);
770 (MATCH_MP_TAC lemma_r_r'_fix2);
771 (EXPAND_TAC "C" THEN REPEAT STRIP_TAC);
772 (MATCH_MP_TAC MEASURABLE_INTER);
773 (REWRITE_TAC[NORMBALL_BALL; MEASURABLE_BALL]);
774 (UNDISCH_TAC `x:real^3->bool IN S` THEN EXPAND_TAC "S");
775 (REWRITE_TAC[mcell_set;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
777 (ASM_SIMP_TAC[MEASURABLE_MCELL]);
778 (REWRITE_TAC[NORMBALL_BALL; GSYM RADIAL_VS_RADIAL_NORM]);
783 (REWRITE_TAC[REAL_POW_DIV]);
784 (REWRITE_TAC[REAL_ARITH `a * (b * c / d) / c = (a * b / d) * (c / c)`]);
785 (REWRITE_WITH `r pow 3 / r pow 3 = &1`);
786 (MATCH_MP_TAC REAL_DIV_REFL);
787 (MATCH_MP_TAC Real_ext.REAL_PROP_NZ_POW);
788 (ASM_REAL_ARITH_TAC);
792 `sum S (\t:real^3->bool. &3 * vol (t INTER normball v r) / r pow 3) =
793 sum S (\t. (&3 / r pow 3) * vol (t INTER normball v r))`);
794 (MATCH_MP_TAC SUM_EQ);
795 (REWRITE_TAC[BETA_THM] THEN REAL_ARITH_TAC);
796 (REWRITE_TAC [SUM_LMUL]);
797 (ABBREV_TAC `g = (\t:real^3->bool. t INTER normball v r)`);
798 (REWRITE_WITH `sum S (\t:real^3->bool.
799 vol (t INTER normball v r)) = sum S (\t. vol (g t))`);
800 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
801 (REWRITE_WITH `sum S (\t:real^3->bool. vol (g t)) = measure (UNIONS (IMAGE g S))`);
802 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
803 (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE);
804 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "g");
806 (MATCH_MP_TAC MEASURABLE_INTER);
807 (REWRITE_TAC[NORMBALL_BALL; MEASURABLE_BALL]);
808 (UNDISCH_TAC `t:real^3->bool IN S` THEN EXPAND_TAC "S");
809 (REWRITE_TAC[mcell_set;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
811 (ASM_SIMP_TAC[MEASURABLE_MCELL]);
813 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
814 (EXISTS_TAC `t INTER y:real^3->bool`);
816 (ASM_CASES_TAC `negligible (t INTER y:real^3->bool)`);
818 (UNDISCH_TAC `t:real^3->bool IN S` THEN UNDISCH_TAC `y:real^3->bool IN S`
819 THEN EXPAND_TAC "S");
820 (REWRITE_TAC[mcell_set_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
822 (UNDISCH_TAC `~(t = y:real^3->bool)`);
824 (REWRITE_WITH `i' = i /\ mcell i' V ul' = mcell i V ul`);
825 (MATCH_MP_TAC AJRIPQN);
826 (REWRITE_TAC[GSYM (ASSUME `t = mcell i' V ul'`);
827 GSYM (ASSUME `y = mcell i V ul`)]);
829 (REWRITE_TAC[SET_RULE `a IN {0,1,2,3,4}<=> a=0\/a=1\/a=2\/a=3\/a=4`]);
833 (EXPAND_TAC "g" THEN EXPAND_TAC "S" THEN REWRITE_TAC[IMAGE]);
835 (NEW_GOAL `!s p:real^3->bool.
836 UNIONS {y| ?x. x IN s /\ y = x INTER p} =
837 UNIONS {y| ?x. x IN s /\ y = x} INTER p`);
838 (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
841 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER; IN_UNIONS]);
843 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
845 (EXISTS_TAC `x' INTER p:real^3->bool`);
847 (EXISTS_TAC `x':real^3->bool`);
849 (REWRITE_TAC[MESON[IN] `(x' INTER p) x <=> x IN x' INTER p`]);
853 `UNIONS {y | ?x:real^3->bool. x IN S /\ y = x INTER normball v r} =
854 UNIONS {y | ?x. x IN S /\ y = x} INTER normball v r`);
855 (UP_ASM_TAC THEN MESON_TAC[]);
857 (* ----------------------------------------------------------------------- *)
861 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
863 UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ ~NULLSET x /\
864 v IN V INTER x) /\ y = x} INTER normball v r`);
866 UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ NULLSET x /\
867 v IN V INTER x) /\ y = x} INTER normball v r`);
869 UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ v IN V INTER x) /\ y = x}
870 INTER normball v r`);
872 (NEW_GOAL `S3 = S2 UNION S1:real^3->bool`);
873 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN EXPAND_TAC "S3");
874 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN REWRITE_TAC[IN_INTER; IN_UNIONS;
875 IN_UNION; IN_ELIM_THM]);
877 (ASM_CASES_TAC `negligible (x':real^3->bool)`);
880 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
881 (EXISTS_TAC `x':real^3->bool`);
887 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
888 (EXISTS_TAC `x':real^3->bool`);
893 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
894 (EXISTS_TAC `x':real^3->bool`);
899 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
900 (EXISTS_TAC `x':real^3->bool`);
905 (NEW_GOAL `measure (S3:real^3->bool) =
906 measure S2 + measure (S1:real^3->bool) - measure (S2 INTER S1)`);
907 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURE_UNION);
908 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN STRIP_TAC);
910 (MATCH_MP_TAC MEASURABLE_INTER);
911 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
912 (MATCH_MP_TAC MEASURABLE_UNIONS);
914 (MATCH_MP_TAC FINITE_SUBSET);
915 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
918 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
922 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
924 (MATCH_MP_TAC MEASURABLE_MCELL);
927 (MATCH_MP_TAC MEASURABLE_INTER);
928 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
929 (MATCH_MP_TAC MEASURABLE_UNIONS);
931 (MATCH_MP_TAC FINITE_SUBSET);
932 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
935 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
939 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
941 (MATCH_MP_TAC MEASURABLE_MCELL);
944 (NEW_GOAL `measure (S2:real^3->bool) = &0`);
946 (MATCH_MP_TAC MEASURE_EQ_0);
947 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
948 (EXISTS_TAC `UNIONS {y | ?x:real^3->bool. (mcell_set V x /\
949 NULLSET x /\ v IN V INTER x) /\ y = x}`);
950 (REWRITE_TAC[SET_RULE `A INTER B SUBSET A`]);
951 (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
953 (MATCH_MP_TAC FINITE_SUBSET);
954 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
957 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
961 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
962 (REWRITE_TAC[ASSUME `t = x:real^3->bool`]);
965 (NEW_GOAL `measure (S2 INTER S1:real^3->bool) = &0`);
966 (MATCH_MP_TAC MEASURE_EQ_0);
967 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
968 (EXISTS_TAC `S2:real^3->bool`);
969 (REWRITE_TAC[SET_RULE `A INTER B SUBSET A`]);
970 (REWRITE_WITH `negligible S2 <=> measure (S2:real^3->bool) = &0`);
971 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
972 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
974 (MATCH_MP_TAC MEASURABLE_INTER);
975 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
976 (MATCH_MP_TAC MEASURABLE_UNIONS);
978 (MATCH_MP_TAC FINITE_SUBSET);
979 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
982 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
986 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
988 (MATCH_MP_TAC MEASURABLE_MCELL);
992 (REWRITE_WITH `vol S1 = vol S3`);
993 (ASM_REAL_ARITH_TAC);
994 (REWRITE_WITH `S3 = normball (v:real^3) r`);
996 (REWRITE_TAC[SET_RULE `A INTER B = B <=> B SUBSET A`]);
998 (NEW_GOAL `normball v r SUBSET voronoi_closed V (v:real^3)`);
999 (REWRITE_TAC[NORMBALL_BALL; SUBSET; IN_BALL; voronoi_closed]);
1000 (REWRITE_TAC[IN; IN_ELIM_THM]);
1003 (ASM_CASES_TAC `w = v:real^3`);
1004 (ASM_REWRITE_TAC[]);
1007 (NEW_GOAL `dist (v, w) <= dist (v, x) + dist (x, w:real^3)`);
1008 (REWRITE_TAC[DIST_TRIANGLE]);
1009 (REWRITE_WITH `dist (x,v:real^3) = dist (v, x)`);
1010 (REWRITE_TAC[DIST_SYM]);
1011 (NEW_GOAL `&2 <= dist (v, w:real^3)`);
1012 (UNDISCH_TAC `packing (V:real^3->bool)` THEN REWRITE_TAC[packing]
1013 THEN REPEAT STRIP_TAC);
1014 (FIRST_ASSUM MATCH_MP_TAC);
1015 (ASM_REWRITE_TAC[]);
1017 (ASM_REAL_ARITH_TAC);
1019 (NEW_GOAL `voronoi_closed V (v:real^3) INTER normball v r SUBSET UNIONS
1020 {y | ?x. (mcell_set V x /\ v IN V INTER x) /\ y = x}`);
1021 (REWRITE_TAC[SUBSET; IN_UNIONS; IN_INTER] THEN GEN_TAC);
1022 (REWRITE_WITH `x IN voronoi_closed V v <=> (?vl. vl IN barV V 3 /\
1024 truncate_simplex 0 vl = [v:real^3])`);
1025 (MATCH_MP_TAC GLTVHUM);
1026 (ASM_REWRITE_TAC[]);
1028 (NEW_GOAL `?i. i <= 4 /\ x IN mcell i V vl`);
1029 (MATCH_MP_TAC SLTSTLO1);
1030 (ASM_REWRITE_TAC[]);
1031 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
1032 (UP_ASM_TAC THEN STRIP_TAC);
1033 (EXISTS_TAC `mcell i V vl`);
1034 (ASM_REWRITE_TAC[mcell_set] THEN ONCE_REWRITE_TAC[IN]);
1035 (REWRITE_TAC[IN_ELIM_THM]);
1036 (EXISTS_TAC `mcell i V vl`);
1039 (EXISTS_TAC `i:num` THEN EXISTS_TAC `vl:(real^3)list`);
1040 (ASM_REWRITE_TAC[]);
1042 (ASM_CASES_TAC `i = 0`);
1043 (UNDISCH_TAC `x IN mcell i V vl` THEN ASM_REWRITE_TAC
1044 [MCELL_EXPLICIT; mcell0; IN_DIFF; IN_BALL]);
1045 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
1046 (MATCH_MP_TAC BARV_3_EXPLICIT);
1047 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1048 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
1049 (UP_ASM_TAC THEN STRIP_TAC);
1050 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 0 vl)`);
1051 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1052 (MATCH_MP_TAC Packing3. HD_TRUNCATE_SIMPLEX);
1053 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
1055 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; HD]);
1058 (UNDISCH_TAC `x:real^3 IN normball v r`);
1059 (REWRITE_TAC[NORMBALL_BALL; IN_BALL]);
1060 (NEW_GOAL `&1 < sqrt (&2)`);
1061 (REWRITE_WITH `&1 < sqrt (&2) <=> &1 pow 2 < sqrt (&2) pow 2`);
1062 (MATCH_MP_TAC Pack1.bp_bdt);
1063 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
1064 (ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
1066 (ASM_REAL_ARITH_TAC);
1069 (NEW_GOAL `V INTER mcell i V vl =
1070 set_of_list (truncate_simplex (i - 1) vl)`);
1071 (MATCH_MP_TAC LEPJBDJ);
1072 (ASM_REWRITE_TAC[]);
1074 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
1077 (SWITCH_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
1079 (NEW_GOAL `v IN V INTER mcell i V vl`);
1080 (ASM_REWRITE_TAC[]);
1081 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
1082 (MATCH_MP_TAC BARV_3_EXPLICIT);
1083 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1084 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
1085 (UP_ASM_TAC THEN STRIP_TAC);
1086 (NEW_GOAL `set_of_list (truncate_simplex 0 vl) SUBSET
1087 set_of_list (truncate_simplex (i-1) (vl:(real^3)list))`);
1088 (MATCH_MP_TAC Rogers.TRUNCATE_SIMPLEX_SUBSET);
1089 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
1090 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
1092 (UP_ASM_TAC THEN SET_TAC[]);
1094 (UP_ASM_TAC THEN REWRITE_WITH
1095 `voronoi_closed V v INTER normball v r = normball (v:real^3) r`);
1098 (REWRITE_TAC[NORMBALL_BALL]);
1099 (REWRITE_WITH `vol (ball (v:real^3,r)) = &4 / &3 * pi * r pow 3`);
1100 (MATCH_MP_TAC VOLUME_BALL);
1101 (ASM_REAL_ARITH_TAC);
1102 (REWRITE_TAC[REAL_ARITH `&3 / r pow 3 * &4 / &3 * pi * r pow 3 =
1103 (&4 * pi) * (r pow 3 / r pow 3)`]);
1104 (REWRITE_WITH `r pow 3 / r pow 3 = &1`);
1105 (MATCH_MP_TAC REAL_DIV_REFL);
1106 (MATCH_MP_TAC REAL_POW_NZ);
1107 (ASM_REAL_ARITH_TAC);
1108 (REAL_ARITH_TAC)]);;