1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Alexey Solovyev *)
7 (* Proofs of: KIUMVTC, TIWWFYQ, DRUQUFE *)
8 (* ========================================================================== *)
11 flyspeck_needs "general/sphere.hl";;
12 flyspeck_needs "packing/pack_defs.hl";;
13 flyspeck_needs "packing/pack2.hl";;
16 module Packing3 = struct
23 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
26 (* Alternative definition of the packing *)
27 let packing_lt = prove(`packing (V:real^3 -> bool) =
28 (!u:real^3 v:real^3. (u IN V) /\ (v IN V) /\ (dist( u, v) < &2) ==>
30 REWRITE_TAC[packing;IN;REAL_ARITH `x<y <=> ~(y<= x)`]
34 let BIS_SYM = prove(`!p (q:real^N). bis p q = bis q p`,
35 REWRITE_TAC[bis] THEN SET_TAC[]);;
40 (***********************************************************************************)
41 (***********************************************************************************)
42 (***********************************************************************************)
45 (*********************************)
46 (* Auxiliary general definitions *)
47 (*********************************)
49 let discrete = new_definition `discrete S <=> ?e. &0 < e /\ (!x y. x IN S /\ y IN S /\ dist(x, y) < e ==> x = y)`;;
52 (****************************)
53 (* Auxiliary general lemmas *)
54 (****************************)
56 let IMAGE_LEMMA = prove(`!s f. IMAGE f s = {f x | x IN s}`, SET_TAC[IMAGE]);;
59 let CHOICE_LEMMA = MESON[] `!y (P:A->bool). ((?x. P x) /\ (!x. P x ==> (x = y))) ==> (@x. P x) = y`;;
62 let SING_GSPEC_APP = prove(`!(f:A->B) a. {f x | x = a} = {f a}`,
63 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN
65 EQ_TAC THEN REPEAT STRIP_TAC THENL [ ASM_REWRITE_TAC[]; ALL_TAC ] THEN
66 EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]);;
69 let SING_UNION_EQ_INSERT = prove(`!s x:A. {x} UNION s = x INSERT s`, SET_TAC[]);;
72 let IN_TRANS = prove(`!(x:A) s t. x IN t /\ t SUBSET s ==> x IN s`, SIMP_TAC[SUBSET]);;
75 let PROJECTION_ORTHOGONAL = prove(`!d v:real^N. projection d v dot d = &0`,
76 REWRITE_TAC[DOT_SYM; projection; VECTOR_SUB_PROJECT_ORTHOGONAL]);;
80 let LENGTH_IMP_CONS = prove(`!l:(A)list. 1 <= LENGTH l ==> ?h t. l = CONS h t`,
82 MP_TAC (ISPECL [`l:(A)list`; `PRE (LENGTH (l:(A)list))`] LENGTH_EQ_CONS) THEN
83 ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> SUC (PRE n) = n`] THEN
85 MAP_EVERY EXISTS_TAC [`h:A`; `t:(A)list`] THEN
90 let LENGTH_1_LEMMA = prove(`!ul:(A)list. LENGTH ul = 1 ==> ul = [HD ul]`,
92 MP_TAC (SPEC `ul:(A)list` LENGTH_IMP_CONS) THEN
93 ASM_REWRITE_TAC[LE_REFL] THEN
95 ASM_REWRITE_TAC[HD] THEN
96 SUBGOAL_THEN `t:(A)list = []` (fun th -> REWRITE_TAC[th]) THEN
97 MP_TAC (ISPEC `ul:(A)list` LENGTH_TL) THEN
98 ASM_REWRITE_TAC[NOT_CONS_NIL; TL; SUB_REFL; LENGTH_EQ_NIL]);;
103 let PERMUTES_TRIVIAL = prove(`!p. p permutes 0..0 <=> p = I`,
104 GEN_TAC THEN EQ_TAC THENL
106 REWRITE_TAC[permutes; FUN_EQ_THM; I_THM; IN_NUMSEG; DE_MORGAN_THM; LE_0; NOT_LE] THEN
107 REPEAT STRIP_TAC THEN
108 ASM_CASES_TAC `x = 0` THENL
110 FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
111 REWRITE_TAC[EXISTS_UNIQUE] THEN
112 STRIP_TAC THEN REMOVE_ASSUM THEN
113 SUBGOAL_THEN `x' = 0` ASSUME_TAC THENL
115 ASM_CASES_TAC `x' = 0` THEN ASM_REWRITE_TAC[] THEN
116 FIRST_X_ASSUM (MP_TAC o SPEC `x':num`) THEN
117 ASM_REWRITE_TAC[ARITH_RULE `0 < x' <=> ~(x' = 0)`];
121 UNDISCH_TAC `(p:num->num) x' = 0` THEN ASM_REWRITE_TAC[];
124 FIRST_X_ASSUM MATCH_MP_TAC THEN
125 POP_ASSUM MP_TAC THEN ARITH_TAC;
128 SIMP_TAC[PERMUTES_I]);;
131 let CONTAINS_BALL_AFFINE_HULL = prove(`!s (x:real^N) r. &0 < r /\ ball (x,r) SUBSET s ==> affine hull s = UNIV`,
132 REPEAT STRIP_TAC THEN
133 MATCH_MP_TAC SUBSET_ANTISYM THEN
134 REWRITE_TAC[SUBSET_UNIV] THEN
135 MATCH_MP_TAC SUBSET_TRANS THEN
136 EXISTS_TAC `affine hull (ball (x:real^N,r))` THEN
137 ASM_SIMP_TAC[HULL_MONO] THEN
138 SUBGOAL_THEN `affine hull ball (x:real^N,r) = UNIV` (fun th -> REWRITE_TAC[th; SUBSET_REFL]) THEN
139 MATCH_MP_TAC AFFINE_HULL_OPEN THEN
140 ASM_REWRITE_TAC[OPEN_BALL; BALL_EQ_EMPTY; REAL_NOT_LE]);;
143 (* conv (A UNION B) = conv(A UNION conv B) *)
144 let CONV_UNION_lemma = prove(`!A B:real^N->bool. convex hull (A UNION B) = convex hull (A UNION convex hull B)`,
146 MATCH_MP_TAC CONVEX_HULLS_EQ THEN
149 MATCH_MP_TAC SUBSET_TRANS THEN
150 EXISTS_TAC `convex hull (A UNION B:real^N->bool)` THEN
151 REWRITE_TAC[HULL_SUBSET] THEN
152 MATCH_MP_TAC HULL_MONO THEN
153 REWRITE_TAC[SUBSET; IN_UNION] THEN
155 DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
157 POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
158 REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
162 MATCH_MP_TAC SUBSET_TRANS THEN
163 EXISTS_TAC `convex hull (A:real^N->bool) UNION convex hull (B:real^N->bool)` THEN
166 REWRITE_TAC[SUBSET; IN_UNION] THEN
167 GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
169 POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
170 REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
174 REWRITE_TAC[HULL_UNION_SUBSET]);;
177 let CONVEX_HULL_EQ_EQ_SET_EQ = prove(`!s t:real^N->bool. ~affine_dependent s /\ ~affine_dependent t ==>
178 (convex hull s = convex hull t <=> s = t)`,
179 REPEAT STRIP_TAC THEN
180 SUBGOAL_THEN `FINITE (s:real^N->bool) /\ FINITE (t:real^N->bool)` ASSUME_TAC THENL
182 ASM_SIMP_TAC[AFFINE_INDEPENDENT_IMP_FINITE];
186 EQ_TAC THEN SIMP_TAC[] THEN
189 SUBGOAL_THEN `s = {x | x extreme_point_of convex hull s}:real^N->bool` ASSUME_TAC THENL
191 MP_TAC (ISPEC `s:real^N->bool` EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
192 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; EQ_SYM_EQ];
195 SUBGOAL_THEN `t = {x | x extreme_point_of convex hull t}:real^N->bool` ASSUME_TAC THENL
197 MP_TAC (ISPEC `t:real^N->bool` EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
198 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; EQ_SYM_EQ];
201 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
202 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
206 (* Lemmas about intersections *)
208 let HULL_INTER_SUBSET_INTER_HULL = prove(`!P s (t:A->bool). P hull (s INTER t) SUBSET P hull s INTER P hull t`,
209 REWRITE_TAC[SUBSET_INTER] THEN
210 REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_MONO THEN REWRITE_TAC[INTER_SUBSET]);;
213 let HULL_INTER_EQ_INTER = prove(`!P s (t:A->bool). P s /\ P t ==> P hull (s INTER t) = s INTER t`,
214 REPEAT STRIP_TAC THEN
215 MATCH_MP_TAC SUBSET_ANTISYM THEN
216 REWRITE_TAC[HULL_SUBSET] THEN
217 MP_TAC (SPEC_ALL HULL_INTER_SUBSET_INTER_HULL) THEN
218 ASM_SIMP_TAC[HULL_P]);;
221 let SUBSET_INTERS = prove(`!(s:A->bool) f. s SUBSET INTERS f <=> (!t. t IN f ==> s SUBSET t)`, SET_TAC[]);;
224 let HULL_INTERS_SUBSET_INTERS_HULL = prove(`!P:((A->bool)->bool) s. P hull (INTERS s) SUBSET INTERS {P hull t | t IN s}`,
226 REWRITE_TAC[SUBSET_INTERS; IN_ELIM_THM] THEN
227 REPEAT STRIP_TAC THEN
228 ASM_REWRITE_TAC[] THEN
229 MATCH_MP_TAC HULL_MONO THEN
230 REWRITE_TAC[SUBSET; IN_INTERS; IN_ELIM_THM] THEN
231 GEN_TAC THEN DISCH_THEN (MP_TAC o SPEC `t':A->bool`) THEN
235 let HULL_INTERS_EQ_INTERS = prove(`!P:((A->bool)->bool) s. (!t. t IN s ==> P t) ==> P hull (INTERS s) = INTERS s`,
236 REPEAT STRIP_TAC THEN
237 MATCH_MP_TAC SUBSET_ANTISYM THEN
238 REWRITE_TAC[HULL_SUBSET] THEN
239 MP_TAC (SPEC_ALL HULL_INTERS_SUBSET_INTERS_HULL) THEN
240 SUBGOAL_THEN `{P hull t | t IN s} = s:(A->bool)->bool` (fun th -> SIMP_TAC[th]) THEN
241 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN GEN_TAC THEN
244 REWRITE_TAC[GSYM EXTENSION] THEN
246 ASM_SIMP_TAC[HULL_P];
249 REWRITE_TAC[GSYM EXTENSION] THEN
250 DISCH_TAC THEN EXISTS_TAC `x:A->bool` THEN
251 ASM_SIMP_TAC[HULL_P]);;
260 let INTERS_2_LEMMA = prove(`!a b f. INTERS {f x | x IN {a, b}} = f a INTER f b`, SET_TAC[INTERS]);;
263 let INTER_INTERS = prove(`!(s:A->bool) (f:(B->bool)) (P:B->(A->bool)). ~(f = {}) ==> s INTER INTERS {P t | t IN f} = INTERS {s INTER P t | t IN f}`,
264 REPEAT STRIP_TAC THEN
265 REWRITE_TAC[EXTENSION; IN_INTER; IN_INTERS; IN_ELIM_THM] THEN
266 GEN_TAC THEN EQ_TAC THENL
268 REPEAT STRIP_TAC THEN
273 REPEAT STRIP_TAC THENL
275 SUBGOAL_THEN `?t':B. t' IN (f:B->bool)` MP_TAC THENL
277 FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
278 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
279 REWRITE_TAC[NOT_FORALL_THM];
283 FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
286 EXISTS_TAC `t':B` THEN
287 ASM_REWRITE_TAC[IN_INTER];
294 ASM_REWRITE_TAC[] THEN
295 FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
298 EXISTS_TAC `t':B` THEN
299 ASM_REWRITE_TAC[IN_INTER];
302 SIMP_TAC[IN_INTER]);;
306 let INTERS_UNIV = prove(`!f:(A->bool)->bool. INTERS f = INTERS (f DELETE UNIV)`,
307 GEN_TAC THEN REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM; IN_DELETE; IN_UNIV] THEN
312 let INTERS_INTER_INTERS = prove(`!f g. INTERS f INTER INTERS g = INTERS (f UNION g)`, SET_TAC[]);;
316 let INTERS_INTER_INTERS_ALT = prove(`!(f:B->bool) g (P:B->(A->bool)). INTERS {P x | x IN f} INTER INTERS {P y | y IN g} = INTERS {P u | u IN (f UNION g)}`,
321 let REAL_DIV_LE_1 = prove(`!a b. &0 < b ==> (a / b <= &1 <=> a <= b)`,
322 MESON_TAC[REAL_LE_LDIV_EQ; REAL_MUL_LID]);;
326 (* Union of finite sets is finite *)
327 let UNIONS_FINITE_LEMMA = prove(`!(g:(A->bool)->bool) (P:(A->bool)->(A->bool)). FINITE g /\ (!t. t IN g ==> FINITE (P t)) ==> FINITE (UNIONS {P t | t IN g})`,
328 REPEAT STRIP_TAC THEN
329 MP_TAC (ISPEC `{(P:(A->bool)->(A->bool)) t | t IN g}` FINITE_FINITE_UNIONS) THEN
330 SUBGOAL_THEN `FINITE {(P:(A->bool)->(A->bool)) t | t IN (g:(A->bool)->bool)}` (fun th -> REWRITE_TAC[th]) THENL
332 REWRITE_TAC[SIMPLE_IMAGE] THEN
333 ASM_SIMP_TAC[FINITE_IMAGE];
336 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
337 REWRITE_TAC[IN_ELIM_THM] THEN
338 REPEAT STRIP_TAC THEN
343 (* Lemmas about min and max for finite sets of real numbers *)
344 let REAL_FINITE_MIN_EXISTS = prove(`!S:real->bool. FINITE S /\ ~(S = {}) ==> ?m. m IN S /\ (!x. x IN S ==> m <= x)`,
345 MESON_TAC[INF_FINITE]);;
348 let REAL_FINITE_MAX_EXISTS = prove(`!S:real->bool. FINITE S /\ ~(S = {}) ==> ?m. m IN S /\ (!x. x IN S ==> x <= m)`,
349 MESON_TAC[SUP_FINITE]);;
352 let REAL_FINITE_ARGMIN = prove(`!(f:A->real) (S:A->bool). FINITE S /\ ~(S = {}) ==> ?a. a IN S /\ (!x. x IN S ==> f a <= f x)`,
353 REPEAT STRIP_TAC THEN
354 SUBGOAL_THEN `?m. m IN IMAGE (f:A->real) S /\ !y. y IN IMAGE f S ==> m <= y` MP_TAC THENL
356 MATCH_MP_TAC REAL_FINITE_MIN_EXISTS THEN
357 ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];
362 REWRITE_TAC[IN_IMAGE] THEN
366 let REAL_FINITE_ARGMAX = prove(`!(f:A->real) (S:A->bool). FINITE S /\ ~(S = {}) ==> ?a. a IN S /\ (!x. x IN S ==> f x <= f a)`,
367 REPEAT STRIP_TAC THEN
368 SUBGOAL_THEN `?m. m IN IMAGE (f:A->real) S /\ !y. y IN IMAGE f S ==> y <= m` MP_TAC THENL
370 MATCH_MP_TAC REAL_FINITE_MAX_EXISTS THEN
371 ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];
376 REWRITE_TAC[IN_IMAGE] THEN
381 (***************************)
382 (* Properties of bisectors *)
383 (***************************)
385 let BIS_EQ_HYPERPLANE = prove(`!u v. bis u v = {x | &2 % (v - u) dot x = v dot v - u dot u}`,
386 REWRITE_TAC[bis; EXTENSION; IN_ELIM_THM; dist; NORM_EQ] THEN
387 REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_RMUL; DOT_SYM] THEN
391 let BIS_LE_EQ_HALFSPACE = prove(`!u v. bis_le u v = {x | &2 % (v - u) dot x <= v dot v - u dot u}`,
392 REWRITE_TAC[bis_le; EXTENSION; IN_ELIM_THM; dist; NORM_LE] THEN
393 REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_RMUL; DOT_SYM] THEN
397 let CONVEX_BIS_LE = prove(`!u v:real^N. convex (bis_le u v)`,
398 REWRITE_TAC[BIS_LE_EQ_HALFSPACE; CONVEX_HALFSPACE_LE]);;
402 let CLOSED_BIS_LE = prove(`!u v:real^N. closed (bis_le u v)`,
403 REWRITE_TAC[BIS_LE_EQ_HALFSPACE; CLOSED_HALFSPACE_LE]);;
406 let CONVEX_BIS = prove(`!u v:real^N. convex(bis u v)`,
407 REWRITE_TAC[BIS_EQ_HYPERPLANE; CONVEX_HYPERPLANE]);;
410 let POLYHEDRON_BIS = prove(`!u v:real^N. polyhedron (bis u v)`,
411 ASM_REWRITE_TAC[BIS_EQ_HYPERPLANE; POLYHEDRON_HYPERPLANE]);;
415 let AFFINE_BIS = prove(`!a b:real^N. affine (bis a b)`,
416 REWRITE_TAC[BIS_EQ_HYPERPLANE; AFFINE_HYPERPLANE]);;
419 let AFFINE_HULL_INTERS_BIS = prove(`!(p:real^N) s. affine hull INTERS {bis p u | u IN s} = INTERS {bis p u | u IN s}`,
421 MATCH_MP_TAC HULL_INTERS_EQ_INTERS THEN
422 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
423 ASM_REWRITE_TAC[AFFINE_BIS]);;
427 (* Auxiliary lemma for distances and points inside an interval *)
428 let MID_POINT_EXISTS = prove(`!(v:real^N) w (d:real). &0 <= d /\ d <= dist(v, w) ==> ?x. between x (v,w) /\ dist(v,x) = d`,
430 DISJ_CASES_TAC (TAUT `dist(v:real^N, w) = &0 \/ ~(dist(v, w) = &0)`) THENL
432 ASM_SIMP_TAC[REAL_LE_ANTISYM] THEN DISCH_TAC THEN
433 EXISTS_TAC `v:real^N` THEN
434 ASM_SIMP_TAC[BETWEEN_IN_SEGMENT; ENDS_IN_SEGMENT; DIST_REFL];
438 SUBGOAL_TAC "A" `&0 < dist(v:real^N, w)` [ ASM_MESON_TAC[REAL_ARITH `&0 <= a /\ ~(a = &0) ==> &0 < a`; DIST_POS_LE] ] THEN
439 REPEAT STRIP_TAC THEN
440 EXISTS_TAC `(v:real^N) + (d:real / dist(v, w)) % (w - v)` THEN
443 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN
444 EXISTS_TAC `d / dist(v:real^N, w)` THEN
445 ASM_SIMP_TAC [REAL_LT_IMP_LE; REAL_LE_DIV; REAL_DIV_LE_1];
447 ASM_REWRITE_TAC[dist; NORM_EQ_SQUARE] THEN
448 REWRITE_TAC[VECTOR_ARITH `v - (v + a % (b - c)) = a % (c - b)`] THEN
449 REWRITE_TAC[DOT_RMUL; DOT_LMUL] THEN
450 REWRITE_TAC[GSYM NORM_POW_2; GSYM dist; REAL_POW_2] THEN
451 REMOVE_THEN "A" MP_TAC THEN
457 (********************************************************)
458 (* Proof that V(v,r) is finite begins here *)
459 (********************************************************)
461 (* General properties of discrete sets *)
463 (* Any discrete set is closed *)
464 let CLOSED_DISCRETE = prove(`!A. discrete A ==> closed A`,
465 REWRITE_TAC[discrete] THEN REPEAT STRIP_TAC THEN
466 MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN
467 EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[GSYM dist; DIST_SYM] THEN
471 (* Any subset of a discrete set is discrete *)
472 let DISCRETE_SUBSET = prove(`!A B:real^N -> bool. discrete A /\ B SUBSET A ==> discrete B`,
473 REWRITE_TAC[discrete; SUBSET] THEN REPEAT STRIP_TAC THEN
474 EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN
478 (* A discrete and bounded set is compact *)
479 let DISCRETE_IMP_BOUNDED_EQ_COMPACT = prove(`!S. discrete S ==> (bounded S <=> compact S)`,
480 MESON_TAC[CLOSED_DISCRETE; BOUNDED_CLOSED_IMP_COMPACT; COMPACT_IMP_BOUNDED]);;
484 (* If S is discrete, then there is an open cover by balls b such that |b INTER S| = 1 *)
485 let DISCRETE_OPEN_COVER = prove(`!S:real^N->bool. discrete S ==> ?f. (!b. b IN f ==> open b /\ (b INTER S) HAS_SIZE 1) /\ S SUBSET UNIONS f`,
486 REWRITE_TAC[discrete] THEN REPEAT STRIP_TAC THEN
487 EXISTS_TAC `{ball(x, e) | x IN (S:real^N->bool)}` THEN
488 REWRITE_TAC[IN_ELIM_THM; SUBSET; UNIONS] THEN
489 CONJ_TAC THEN REPEAT STRIP_TAC THENL
491 ASM_SIMP_TAC[OPEN_BALL];
492 CONV_TAC HAS_SIZE_CONV THEN
493 EXISTS_TAC `x:real^N` THEN
494 ASM_REWRITE_TAC[INTER; ball; IN_ELIM_THM; EXTENSION; IN_SING] THEN
495 ASM_MESON_TAC[DIST_EQ_0];
496 EXISTS_TAC `ball(x:real^N, e)` THEN
497 ASM_REWRITE_TAC[CENTRE_IN_BALL] THEN
498 EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]
502 (* Discrete and bounded S is finite *)
503 let DISCRETE_BOUNDED_IMP_FINITE = prove(`!S:real^N->bool. discrete S /\ bounded S ==> FINITE S`,
504 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
505 MP_TAC (ISPEC `S:real^N->bool` DISCRETE_IMP_BOUNDED_EQ_COMPACT) THEN
506 ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
508 REWRITE_TAC[COMPACT_EQ_HEINE_BOREL] THEN
509 REPEAT STRIP_TAC THEN
510 MP_TAC (SPEC `S:real^N -> bool` DISCRETE_OPEN_COVER) THEN
511 ASM_REWRITE_TAC[] THEN
512 DISCH_THEN (X_CHOOSE_THEN `f:(real^N->bool)->bool` MP_TAC) THEN
513 FIRST_X_ASSUM ((LABEL_TAC "A") o (SPEC `f:(real^N->bool)->bool`)) THEN
514 DISCH_THEN (LABEL_TAC "B") THEN
515 REMOVE_THEN "A" MP_TAC THEN ASM_SIMP_TAC[] THEN
516 DISCH_THEN (X_CHOOSE_THEN `g:(real^N->bool)->bool` MP_TAC) THEN
518 SUBGOAL_THEN `FINITE (S INTER UNIONS (g:(real^N->bool)->bool))` ASSUME_TAC THENL
520 REWRITE_TAC[INTER_UNIONS] THEN
521 MATCH_MP_TAC UNIONS_FINITE_LEMMA THEN
522 ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
523 REMOVE_THEN "B" (MP_TAC o (SPEC `x:real^N -> bool`) o CONJUNCT1) THEN
524 MP_TAC (SET_RULE `x:(real^N->bool) IN g /\ g SUBSET f ==> x IN f`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
525 SIMP_TAC[INTER_COMM; HAS_SIZE];
528 ASM_MESON_TAC[SET_RULE `S SUBSET A ==> S INTER A = S`]);;
533 (* Proof of the main lemma begins here *)
535 (* A packing is a discrete set *)
536 let PACKING_IMP_DISCRETE = prove(`!V. packing V ==> discrete V`,
537 REWRITE_TAC[packing_lt; discrete] THEN REPEAT STRIP_TAC THEN
538 EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[REAL_ARITH `&0 < &2`]);;
540 (* Main lemma: if V is a packing then (V INTER ball) is finite *)
541 let KIUMVTC = prove(`!(p:real^3) r V. packing V ==> FINITE (V INTER ball(p, r))`,
542 REPEAT STRIP_TAC THEN MATCH_MP_TAC DISCRETE_BOUNDED_IMP_FINITE THEN CONJ_TAC THENL
545 ASM_SIMP_TAC[BOUNDED_INTER; BOUNDED_BALL]
547 MATCH_MP_TAC DISCRETE_SUBSET THEN
548 EXISTS_TAC `V:real^3->bool` THEN
549 ASM_SIMP_TAC[PACKING_IMP_DISCRETE] THEN
556 (****************************************************)
558 (* If a packing is saturated, then every point of *)
559 (* the space is inside some Voronoi (closed) cell *)
560 (****************************************************)
563 (* AS: real^N <== pacling:real^N *)
564 let TIWWFYQ = prove(`!V (p:real^3). packing V /\ saturated V ==> (?v. v IN V /\ p IN voronoi_closed V v)`,
565 REWRITE_TAC[saturated] THEN REPEAT STRIP_TAC THEN
566 ABBREV_TAC `S = V INTER ball(p:real^3, &2)` THEN
567 SUBGOAL_THEN `?v:real^3. v IN S /\ !w. w IN S ==> dist(v, p) <= dist(w, p)` MP_TAC THENL
569 MATCH_MP_TAC REAL_FINITE_ARGMIN THEN
571 ASM_SIMP_TAC[KIUMVTC] THEN
572 REWRITE_TAC[SET_RULE `~(S = {}) <=> ?a. a IN S`] THEN
573 EXPAND_TAC "S" THEN REWRITE_TAC[ball; INTER; IN_ELIM_THM] THEN
579 EXISTS_TAC `v:real^3` THEN
580 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN EXPAND_TAC "S" THEN POP_ASSUM (fun th -> ALL_TAC) THEN
581 ASM_SIMP_TAC[IN_INTER] THEN
582 DISCH_THEN (LABEL_TAC "A") THEN
583 DISCH_THEN (LABEL_TAC "B") THEN
584 REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN GEN_TAC THEN
585 GEN_REWRITE_TAC LAND_CONV [GSYM IN] THEN
586 DISJ_CASES_TAC (TAUT `w:real^3 IN ball(p, &2) \/ ~(w IN ball(p, &2))`) THENL
588 ASM_MESON_TAC[DIST_SYM];
589 SUBGOAL_THEN `&2 <= dist(p:real^3, w)` MP_TAC THENL
591 POP_ASSUM MP_TAC THEN REWRITE_TAC[ball; IN_ELIM_THM; REAL_NOT_LT];
595 SUBGOAL_THEN `dist(p:real^3, v) < &2` MP_TAC THENL
597 REMOVE_THEN "A" MP_TAC THEN SIMP_TAC[ball; IN_ELIM_THM];
608 (*******************************)
609 (* Porperties of Voronoi cells *)
610 (*******************************)
612 (* v IN voronoi_closed V v *)
613 let CENTER_IN_VORONOI_CELL = prove(`!V (v:real^3). v IN voronoi_closed V v /\ v IN voronoi_open V v`,
615 SUBGOAL_THEN `v IN voronoi_open V (v:real^3)` ASSUME_TAC THENL
617 REWRITE_TAC[voronoi_open; IN_ELIM_THM; DIST_REFL] THEN
618 SIMP_TAC[DIST_POS_LT];
621 ASM_REWRITE_TAC[] THEN
622 MATCH_MP_TAC IN_TRANS THEN
623 EXISTS_TAC `voronoi_open V (v:real^3)` THEN
624 ASM_REWRITE_TAC[Pack2.VORONOI_OPEN_SUBSET_CLOSED]);;
628 (* voronoi_closed V v contains a ball *)
629 let VORONOI_CLOSED_CONTAINS_BALL = prove(`!V (v:real^3). packing V ==> ?r. &0 < r /\ ball (v, r) SUBSET voronoi_closed V v`,
630 REWRITE_TAC[packing; voronoi_closed] THEN
631 REPEAT STRIP_TAC THEN
632 ASM_CASES_TAC `v:real^3 IN V` THENL
634 POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN DISCH_TAC THEN
636 REWRITE_TAC[REAL_LT_01; ball; SUBSET; IN_ELIM_THM] THEN
637 REPEAT STRIP_TAC THEN
638 ASM_CASES_TAC `w = v:real^3` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
639 FIRST_X_ASSUM (MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
640 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
641 SUBGOAL_THEN `&2 - dist(x,v:real^3) <= dist(x,w:real^3)` MP_TAC THENL
643 REWRITE_TAC[REAL_ARITH `a - b <= c <=> a <= b + c:real`] THEN
644 MATCH_MP_TAC REAL_LE_TRANS THEN
645 EXISTS_TAC `dist (v,w:real^3)` THEN
646 ASM_REWRITE_TAC[] THEN
647 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
648 REWRITE_TAC[DIST_SYM];
652 UNDISCH_TAC `dist (v,x:real^3) < &1` THEN
653 REWRITE_TAC[DIST_SYM] THEN
658 SUBGOAL_THEN `?s. &0 < s /\ ball (v:real^3, s) INTER V = {}` STRIP_ASSUME_TAC THENL
660 SUBGOAL_THEN `~(ball (v:real^3, &1) INTER V = {}) ==> ?x. ball (v:real^3, &1) INTER V = {x}` MP_TAC THENL
662 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; EXTENSION; IN_SING; ball; IN_ELIM_THM] THEN
664 EXISTS_TAC `x:real^3` THEN
665 GEN_TAC THEN EQ_TAC THENL
668 SUBGOAL_THEN `dist (x:real^3, x') < &2` MP_TAC THENL
670 MATCH_MP_TAC REAL_LET_TRANS THEN
671 EXISTS_TAC `dist (x,v) + dist(v:real^3,x')` THEN
672 REWRITE_TAC[DIST_TRIANGLE; REAL_ARITH `&2 = &1 + &1`] THEN
673 MATCH_MP_TAC REAL_LT_ADD2 THEN
674 ASM_REWRITE_TAC[DIST_SYM];
678 FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `x':real^3`]) THEN
679 POP_ASSUM MP_TAC THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN SIMP_TAC[IN] THEN
680 DISCH_TAC THEN DISCH_TAC THEN
681 ASM_CASES_TAC `x' = x:real^3` THEN ASM_REWRITE_TAC[REAL_NOT_LT];
689 ASM_CASES_TAC `ball (v:real^3, &1) INTER V = {}` THEN ASM_REWRITE_TAC[] THENL
692 ASM_REWRITE_TAC[REAL_LT_01];
697 EXISTS_TAC `dist (v:real^3, x)` THEN
700 MATCH_MP_TAC DIST_POS_LT THEN
701 DISCH_THEN (ASSUME_TAC o SYM) THEN
702 UNDISCH_TAC `ball (v:real^3, &1) INTER V = {x}` THEN
703 ASM_REWRITE_TAC[EXTENSION; IN_INTER; IN_SING; NOT_FORALL_THM] THEN
704 EXISTS_TAC `x:real^3` THEN
709 POP_ASSUM MP_TAC THEN
710 REWRITE_TAC[EXTENSION; IN_INTER; ball; IN_ELIM_THM; NOT_IN_EMPTY; IN_SING] THEN
711 REPEAT STRIP_TAC THEN
712 FIRST_ASSUM (MP_TAC o SPEC `x:real^3`) THEN
713 REWRITE_TAC[] THEN DISCH_TAC THEN
714 FIRST_X_ASSUM (MP_TAC o SPEC `x':real^3`) THEN
715 SUBGOAL_THEN `dist (v,x':real^3) < &1` ASSUME_TAC THENL
717 MATCH_MP_TAC REAL_LT_TRANS THEN
718 EXISTS_TAC `dist (v, x:real^3)` THEN
722 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
723 UNDISCH_TAC `dist (v,x':real^3) < dist (v,x)` THEN
724 ASM_REWRITE_TAC[REAL_LT_REFL];
728 EXISTS_TAC `s / &2` THEN
729 POP_ASSUM MP_TAC THEN
730 ASM_REWRITE_TAC[REAL_ARITH `&0 < s / &2 <=> &0 < s`; ball; SUBSET; IN_ELIM_THM; EXTENSION; IN_INTER; NOT_IN_EMPTY; DE_MORGAN_THM; REAL_NOT_LT] THEN
731 REPEAT STRIP_TAC THEN
732 FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`) THEN
733 ASM_REWRITE_TAC[IN] THEN DISCH_TAC THEN
734 SUBGOAL_THEN `s - dist(x,v:real^3) <= dist(x,w:real^3)` MP_TAC THENL
736 REWRITE_TAC[REAL_ARITH `a - b <= c <=> a <= b + c:real`] THEN
737 MATCH_MP_TAC REAL_LE_TRANS THEN
738 EXISTS_TAC `dist (v,w:real^3)` THEN
739 ASM_REWRITE_TAC[] THEN
740 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
741 REWRITE_TAC[DIST_SYM];
745 UNDISCH_TAC `dist (v, x:real^3) < s / &2` THEN
746 UNDISCH_TAC `&0 < s` THEN
747 REWRITE_TAC[DIST_SYM] THEN
752 (* aff_dim voronoi_closed V v = 3 *)
753 let AFF_DIM_VORONOI_CLOSED = prove(`!V v. packing V ==> aff_dim (voronoi_closed V v) = &3`,
754 REWRITE_TAC[GSYM DIMINDEX_3; AFF_DIM_EQ_FULL] THEN
755 REPEAT STRIP_TAC THEN
756 MATCH_MP_TAC CONTAINS_BALL_AFFINE_HULL THEN
757 MP_TAC (SPEC_ALL VORONOI_CLOSED_CONTAINS_BALL) THEN
758 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
759 MAP_EVERY EXISTS_TAC [`v:real^3`; `r:real`] THEN
766 (* For a saturated packing each Voronoi cell is inside a ball of radius 2 *)
767 let VORONOI_BALL2 = prove(`!V (v:real^N). saturated V ==> voronoi_closed V v SUBSET ball(v, &2)`,
768 REWRITE_TAC[saturated; voronoi_closed] THEN REPEAT STRIP_TAC THEN
769 REWRITE_TAC[SUBSET; ball; IN_ELIM_THM] THEN
770 X_GEN_TAC `y:real^N` THEN
771 ONCE_REWRITE_TAC[TAUT `(A ==> B) <=> (~B ==> ~A)`] THEN
772 REWRITE_TAC[REAL_NOT_LT; NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
773 FIRST_X_ASSUM ((X_CHOOSE_THEN `w:real^N` MP_TAC) o SPEC `y:real^N`) THEN
774 REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
775 EXISTS_TAC `w:real^N` THEN
776 ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN
777 REWRITE_TAC[DIST_SYM] THEN
781 (* A Voronoi cell is bounded (for a saturated packing) *)
782 let BOUNDED_VORONOI_CLOSED = prove(`!V (v:real^N). saturated V ==> bounded (voronoi_closed V v)`,
783 REPEAT STRIP_TAC THEN
784 MATCH_MP_TAC BOUNDED_SUBSET THEN
785 ASM_MESON_TAC[VORONOI_BALL2; BOUNDED_BALL]);;
788 (* A closed Voronoi cell is an intersection of bisector half-spaces *)
789 let VORONOI_CLOSED_EQ_INTERS_BIS_LE = prove(`!S v:real^N. voronoi_closed S v = INTERS {bis_le v w | w IN S}`,
791 REWRITE_TAC[voronoi_closed; bis_le; INTERS; IN_ELIM_THM] THEN
792 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN] THEN GEN_TAC THEN
793 EQ_TAC THEN REPEAT STRIP_TAC THENL
796 FIRST_X_ASSUM (MP_TAC o (SPEC `bis_le v (w:real^N)`) o check (is_forall o concl)) THEN
797 ANTS_TAC THEN REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
798 EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[]
802 (* The same result with excluded point v *)
803 let VORONOI_CLOSED_EQ_INTERS_BIS_LE_ALT = prove(`!S v:real^N. voronoi_closed S v = INTERS {bis_le v w | w | w IN S /\ ~(w = v)}`,
805 REWRITE_TAC[voronoi_closed; bis_le] THEN
806 REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM; IN] THEN GEN_TAC THEN
807 EQ_TAC THEN REPEAT STRIP_TAC THENL
810 DISJ_CASES_TAC (TAUT `w:real^N = v \/ ~(w = v)`) THENL
812 ASM_REWRITE_TAC[REAL_LE_REFL];
815 FIRST_X_ASSUM (MP_TAC o (SPEC `bis_le v (w:real^N)`) o check (is_forall o concl)) THEN
816 ANTS_TAC THEN REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
817 EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[]
822 (* A closed Voronoi cell is an intersection of bisectors for w IN ball(v, 4) *)
823 let VORONOI_INTER_BIS_LE = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
824 (voronoi_closed V v =INTERS { bis_le v u | u | u IN V /\ u IN ball(v, &4) /\ ~(u=v) })`,
825 REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE_ALT; saturated] THEN REPEAT STRIP_TAC THEN
826 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "A") THEN DISCH_TAC THEN
827 REWRITE_TAC[EXTENSION; IN_INTERS] THEN GEN_TAC THEN EQ_TAC THENL
833 REWRITE_TAC[IN_ELIM_THM] THEN
834 DISCH_THEN (LABEL_TAC "B") THEN REPEAT STRIP_TAC THEN
836 DISJ_CASES_TAC (TAUT `(w:real^3) IN ball(v:real^3, &4) \/ ~(w IN ball(v, &4))`) THENL
838 REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN SET_TAC[];
842 SUBGOAL_THEN `x:real^3 IN ball(v, &2)` (LABEL_TAC "C") THENL
844 POP_ASSUM MP_TAC THEN REWRITE_TAC[ball; IN_ELIM_THM] THEN
845 ONCE_REWRITE_TAC[TAUT `~A ==> B <=> ~B ==> A`] THEN
846 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
847 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `&2`] MID_POINT_EXISTS) THEN
848 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`] THEN
849 DISCH_THEN (X_CHOOSE_THEN `q:real^3` MP_TAC) THEN
850 REWRITE_TAC[between] THEN STRIP_TAC THEN
851 REMOVE_THEN "A" ((X_CHOOSE_THEN `p:real^3` MP_TAC) o SPEC `q:real^3`) THEN STRIP_TAC THEN
852 REMOVE_THEN "B" (MP_TAC o SPEC `bis_le v (p:real^3)`) THEN
855 EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[ball; IN_ELIM_THM] THEN
858 MP_TAC (ISPECL [`v:real^3`; `q:real^3`; `p:real^3`] DIST_TRIANGLE) THEN
859 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
862 REWRITE_TAC[DIST_NZ] THEN
863 MP_TAC (ISPECL [`v:real^3`; `p:real^3`; `q:real^3`] DIST_TRIANGLE) THEN
864 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN
870 REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
871 SUBGOAL_TAC "A" `dist(x:real^3, v) = &2 + dist(q, x)` [ASM_SIMP_TAC[DIST_SYM]] THEN
872 MP_TAC (ISPECL [`x:real^3`; `q:real^3`; `p:real^3`] DIST_TRIANGLE) THEN
873 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC;
878 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
879 ASM_REWRITE_TAC[bis_le; ball; IN_ELIM_THM; REAL_NOT_LT] THEN
880 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
881 REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC);;
885 (* A closed Voronoi cell is an intersection of finitely many closed half-spaces *)
886 let VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
887 ?W. W SUBSET V /\ ~(v IN W) /\ FINITE W /\
888 voronoi_closed V v = INTERS { bis_le v u | u | u IN W }`,
891 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP VORONOI_INTER_BIS_LE th)) THEN
893 EXISTS_TAC `(V:real^3->bool) INTER ball(v,&4) DELETE v` THEN
894 REPEAT STRIP_TAC THENL
898 MATCH_MP_TAC FINITE_SUBSET THEN
899 EXISTS_TAC `V INTER ball(v:real^3,&4)` THEN
902 ASM_MESON_TAC[KIUMVTC];
907 ASM_REWRITE_TAC[] THEN
913 (* A closed Voronoi cell is a polyhedron *)
915 (* AS: real^N (requires packing:real^N) *)
916 let VORONOI_POLYHEDRON = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
917 polyhedron (voronoi_closed V v)`,
919 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE th)) THEN
921 REWRITE_TAC[polyhedron] THEN
922 EXISTS_TAC `{bis_le v (u:real^3) | u IN W}` THEN
923 ASM_REWRITE_TAC[] THEN
926 REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
927 MATCH_MP_TAC FINITE_IMAGE THEN
931 REWRITE_TAC[IN_ELIM_THM; BIS_LE_EQ_HALFSPACE] THEN
932 REPEAT STRIP_TAC THEN
933 EXISTS_TAC `&2 % (u - v:real^3)` THEN
934 EXISTS_TAC `(u:real^3) dot u - (v:real^3) dot v` THEN
935 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; REAL_ARITH `~(&2 = &0)`; VECTOR_SUB_EQ] THEN
939 (* A closed Voronoi cell is convex *)
940 let CONVEX_VORONOI_CLOSED = prove(`!S v:real^N. convex(voronoi_closed S v)`,
942 REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE] THEN
943 MATCH_MP_TAC CONVEX_INTERS THEN
944 REWRITE_TAC[IN_ELIM_THM] THEN
945 MESON_TAC[CONVEX_BIS_LE]);;
948 (* A closed Voronoi cell is closed *)
949 let CLOSED_VORONOI_CLOSED = prove(`!S v:real^N. closed(voronoi_closed S v)`,
951 REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE] THEN
952 MATCH_MP_TAC CLOSED_INTERS THEN
953 REWRITE_TAC[IN_ELIM_THM] THEN
954 MESON_TAC[CLOSED_BIS_LE]);;
956 (* A closed Voronoi cell is compact if a packing is saturated (for boundness) *)
957 let COMPACT_VORONOI_CLOSED = prove(`!S v. saturated S ==> compact (voronoi_closed S v)`,
958 REPEAT STRIP_TAC THEN
959 MATCH_MP_TAC BOUNDED_CLOSED_IMP_COMPACT THEN
960 ASM_SIMP_TAC[CLOSED_VORONOI_CLOSED; BOUNDED_VORONOI_CLOSED]);;
963 (****************************************************************)
965 (* For a saturated packing, each closed Voronoi closed cell is *)
966 (* compact, convex, and measurable *)
967 (****************************************************************)
969 (* AS: real^N, remove `packing` *)
970 let DRUQUFE = prove(`!V (v:real^3). packing V /\ saturated V ==>
971 compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`,
972 REPEAT STRIP_TAC THENL
974 ASM_SIMP_TAC[COMPACT_VORONOI_CLOSED];
975 REWRITE_TAC[CONVEX_VORONOI_CLOSED];
976 MATCH_MP_TAC MEASURABLE_CONVEX THEN
977 ASM_SIMP_TAC[CONVEX_VORONOI_CLOSED; BOUNDED_VORONOI_CLOSED]
985 (*************************************************************)
988 (*******************************************)
989 (* Some results for initial sublists *)
990 (*******************************************)
992 let INITIAL_SUBLIST_APPEND = prove(`!ul vl. initial_sublist ul (APPEND ul vl)`,
993 REWRITE_TAC[INITIAL_SUBLIST] THEN
997 let INITIAL_SUBLIST_HEAD_EQ = prove(`!xl zl hx tx hz tz. xl = CONS hx tx /\ zl = CONS hz tz /\ initial_sublist xl zl ==> hx = hz`,
999 REWRITE_TAC[INITIAL_SUBLIST] THEN
1001 POP_ASSUM MP_TAC THEN
1002 ASM_REWRITE_TAC[APPEND] THEN
1003 MESON_TAC[injectivity "list"]);;
1006 let INITIAL_SUBLIST_HEAD_EQ_2 = prove(`!xl yl zl hx tx hy ty. xl = CONS hx tx /\ yl = CONS hy ty /\ initial_sublist xl zl /\ initial_sublist yl zl ==> hx = hy`,
1007 MESON_TAC[INITIAL_SUBLIST_HEAD_EQ; INITIAL_SUBLIST; APPEND]);;
1011 let INITIAL_SUBLIST_TAIL = prove(`!xl zl hx tx. xl = CONS hx tx /\ initial_sublist xl zl ==> initial_sublist tx (TL zl)`,
1012 REWRITE_TAC[INITIAL_SUBLIST] THEN
1013 REPEAT STRIP_TAC THEN
1014 POP_ASSUM MP_TAC THEN
1015 ASM_REWRITE_TAC[APPEND] THEN
1017 ASM_REWRITE_TAC[TL] THEN
1021 (* Two initial sublists of the same list and of the same size are equal *)
1022 let INITIAL_SUBLIST_UNIQUE = prove(`!n (xl:(A)list) yl zl. initial_sublist xl zl /\ initial_sublist yl zl /\ LENGTH xl = n /\ LENGTH yl = n ==> xl = yl`,
1023 INDUCT_TAC THEN REPEAT STRIP_TAC THENL
1025 ASM_MESON_TAC[LENGTH_EQ_NIL];
1029 MP_TAC (ISPECL [`xl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
1030 MP_TAC (ISPECL [`yl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
1031 ASM_REWRITE_TAC[] THEN
1032 REPEAT STRIP_TAC THEN
1033 ASM_REWRITE_TAC[injectivity "list"] THEN
1036 ASM_MESON_TAC[INITIAL_SUBLIST_HEAD_EQ_2];
1040 ASM_MESON_TAC[INITIAL_SUBLIST_TAIL]);;
1043 (* Transitivity for initial sublists *)
1044 let INITIAL_SUBLIST_TRANS = prove(`!(xl:(A)list) yl zl. initial_sublist xl yl /\ initial_sublist yl zl ==> initial_sublist xl zl`,
1045 REWRITE_TAC[INITIAL_SUBLIST] THEN
1046 REPEAT STRIP_TAC THEN
1047 ASM_MESON_TAC[APPEND_ASSOC]);;
1050 (* initial_sublist is reflexive *)
1051 let INITIAL_SUBLIST_REFL = prove(`!ul. initial_sublist ul ul`, MESON_TAC[INITIAL_SUBLIST; APPEND_NIL]);;
1054 (* An empty list is an initial sublist of any list *)
1055 let INITIAL_SUBLIST_NIL = prove(`!zl. initial_sublist [] zl`,
1056 REWRITE_TAC[INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]);;
1059 (* There exists initial sublists of all acceptable lengths *)
1060 let INITIAL_SUBLIST_EXISTS_ALT = prove(`!n (zl:(A)list) k. LENGTH zl = n /\ k <= n ==> ?xl. initial_sublist xl zl /\ LENGTH xl = k`,
1061 INDUCT_TAC THEN REPEAT STRIP_TAC THENL
1063 EXISTS_TAC `[]:(A)list` THEN
1064 REWRITE_TAC[INITIAL_SUBLIST_NIL] THEN
1065 POP_ASSUM MP_TAC THEN
1066 SIMP_TAC[LE; LENGTH];
1071 MP_TAC (ISPECL [`zl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
1072 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1073 SUBGOAL_THEN `?yl:(A)list. initial_sublist yl t /\ LENGTH yl = k - 1` MP_TAC THENL
1075 FIRST_X_ASSUM (MP_TAC o SPECL [`t:(A)list`; `k - 1`]) THEN
1076 ASM_SIMP_TAC[ARITH_RULE `k <= SUC n ==> k - 1 <= n`];
1081 DISJ_CASES_TAC (ARITH_RULE `k = 0 \/ 0 < k`) THENL
1083 EXISTS_TAC `[]:(A)list` THEN
1084 ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL; LENGTH];
1088 EXISTS_TAC `CONS (h:A) yl` THEN
1089 ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND; LENGTH] THEN
1092 REPLICATE_TAC 2 (POP_ASSUM (fun th -> ALL_TAC)) THEN
1093 POP_ASSUM MP_TAC THEN
1094 REWRITE_TAC[INITIAL_SUBLIST] THEN
1097 POP_ASSUM MP_TAC THEN
1103 let INITIAL_SUBLIST_EXISTS = prove(`!zl k. k <= LENGTH zl ==> (?xl. initial_sublist xl zl /\ LENGTH xl = k)`,
1104 MESON_TAC[INITIAL_SUBLIST_EXISTS_ALT]);;
1107 (* The length of an initial sublist does not exceed the length of the list itself *)
1108 let INITIAL_SUBLIST_LENGTH_LE = prove(`!xl zl. initial_sublist xl zl ==> LENGTH xl <= LENGTH zl`,
1109 REWRITE_TAC[INITIAL_SUBLIST] THEN REPEAT STRIP_TAC THEN
1110 ASM_REWRITE_TAC[LENGTH_APPEND] THEN
1114 (* Structure of initial sublists of APPEND ul vl *)
1115 let INITIAL_SUBLIST_APPEND_2 = prove(`!(xl:(A)list) ul vl. initial_sublist xl (APPEND ul vl) <=> initial_sublist xl ul \/ (?yl. initial_sublist yl vl /\ xl = APPEND ul yl)`,
1116 REPEAT STRIP_TAC THEN EQ_TAC THENL
1118 ABBREV_TAC `k = LENGTH (xl:(A)list)` THEN
1119 DISJ_CASES_TAC (ARITH_RULE `k:num <= LENGTH (ul:(A)list) \/ LENGTH ul < k`) THENL
1123 MP_TAC (ISPECL [`ul:(A)list`; `k:num`] INITIAL_SUBLIST_EXISTS) THEN
1124 ASM_REWRITE_TAC[] THEN
1126 MP_TAC (ISPECL [`xl':(A)list`; `ul:(A)list`; `APPEND (ul:(A)list) vl`] INITIAL_SUBLIST_TRANS) THEN
1127 ASM_REWRITE_TAC[INITIAL_SUBLIST_APPEND] THEN
1128 ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];
1135 SUBGOAL_THEN `?yl:(A)list. initial_sublist yl vl /\ LENGTH yl = k - LENGTH (ul:(A)list)` MP_TAC THENL
1137 MP_TAC (ISPECL [`vl:(A)list`; `k - LENGTH (ul:(A)list)`] INITIAL_SUBLIST_EXISTS) THEN
1140 POP_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_LENGTH_LE th)) THEN
1141 ASM_REWRITE_TAC[LENGTH_APPEND] THEN
1142 POP_ASSUM MP_TAC THEN
1152 EXISTS_TAC `yl:(A)list` THEN
1153 ASM_REWRITE_TAC[] THEN
1154 SUBGOAL_THEN `initial_sublist (APPEND (ul:(A)list) yl) (APPEND ul vl) /\ LENGTH (APPEND ul yl) = k` MP_TAC THENL
1158 POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM MP_TAC THEN
1159 REWRITE_TAC[INITIAL_SUBLIST] THEN
1160 MESON_TAC[APPEND_ASSOC];
1161 REWRITE_TAC[LENGTH_APPEND] THEN
1162 POP_ASSUM MP_TAC THEN
1163 POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1164 POP_ASSUM MP_TAC THEN
1171 ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];
1176 REPEAT STRIP_TAC THENL
1178 ASM_MESON_TAC[INITIAL_SUBLIST_TRANS; INITIAL_SUBLIST_APPEND];
1179 ASM_MESON_TAC[INITIAL_SUBLIST; APPEND_ASSOC]
1184 (* Initial sublists of an one-element list *)
1185 let INITIAL_SUBLIST_SING = prove(`!(v:A) xl. initial_sublist xl [v] <=> xl = [] \/ xl = [v]`,
1186 REPEAT GEN_TAC THEN EQ_TAC THENL
1189 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_LENGTH_LE th)) THEN
1190 REWRITE_TAC[LENGTH; SYM ONE] THEN
1192 DISJ_CASES_TAC (ARITH_RULE `LENGTH (xl:(A)list) = 0 \/ 1 <= LENGTH xl`) THENL
1194 ASM_MESON_TAC[LENGTH_EQ_NIL];
1198 MP_TAC (ISPECL [`1`; `LENGTH (xl:(A)list)`] LE_ANTISYM) THEN
1199 ASM_REWRITE_TAC[] THEN
1200 SUBGOAL_THEN `initial_sublist [v:A] [v] /\ LENGTH [v] = 1` ASSUME_TAC THENL
1202 REWRITE_TAC[INITIAL_SUBLIST; LENGTH; SYM ONE; APPEND] THEN MESON_TAC[];
1205 ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];
1212 ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL];
1213 ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]
1217 (* Initial sublists of APPEND ul [v] *)
1218 let INITIAL_SUBLIST_APPEND_SING = prove(`!xl ul (v:A). initial_sublist xl (APPEND ul [v]) <=> initial_sublist xl ul \/ xl = APPEND ul [v]`,
1220 REWRITE_TAC[INITIAL_SUBLIST_APPEND_2; INITIAL_SUBLIST_SING] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
1223 DISJ1_TAC THEN POP_ASSUM MP_TAC THEN
1224 ASM_REWRITE_TAC[APPEND_NIL] THEN
1225 SIMP_TAC[INITIAL_SUBLIST_REFL];
1229 EXISTS_TAC `[v:A]` THEN
1234 (* (HD ul) is an initial sublist of ul *)
1235 let INITIAL_SUBLIST_HD = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist [HD ul] ul`,
1236 REPEAT STRIP_TAC THEN
1237 MP_TAC (SPEC `ul:(A)list` LENGTH_IMP_CONS) THEN
1238 ASM_REWRITE_TAC[] THEN
1240 ASM_REWRITE_TAC[HD; INITIAL_SUBLIST; APPEND] THEN
1241 EXISTS_TAC `t:(A)list` THEN
1244 (* (BUTLAST ul) is an initial sublist of ul *)
1245 let BUTLAST_INITIAL_SUBLIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist (BUTLAST ul) ul`,
1246 REPEAT STRIP_TAC THEN
1247 MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
1248 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
1249 ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
1250 REWRITE_TAC[INITIAL_SUBLIST] THEN
1252 EXISTS_TAC `[LAST ul:A]` THEN
1253 ASM_REWRITE_TAC[]);;
1256 (**********************************************************)
1258 (**********************************)
1259 (* Additional properties of lists *)
1260 (**********************************)
1262 let LENGTH_BUTLAST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> LENGTH (BUTLAST ul) = LENGTH ul - 1`,
1263 REPEAT STRIP_TAC THEN
1264 MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
1265 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
1266 ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
1267 DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM th]) THEN
1268 REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
1274 let HD_IN_SET_OF_LIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> HD ul IN set_of_list ul`,
1275 REPEAT STRIP_TAC THEN
1276 REWRITE_TAC[IN_SET_OF_LIST] THEN
1277 ONCE_REWRITE_TAC[GSYM EL] THEN
1278 MATCH_MP_TAC MEM_EL THEN
1279 POP_ASSUM MP_TAC THEN
1283 let HD_INITIAL_SUBLIST = prove(`!xl yl:(A)list. 1 <= LENGTH yl /\ initial_sublist yl xl ==> HD yl = HD xl`,
1284 REPEAT STRIP_TAC THEN
1285 MP_TAC (SPEC `yl:(A)list` LENGTH_IMP_CONS) THEN
1286 ASM_REWRITE_TAC[] THEN
1287 MP_TAC (SPEC `xl:(A)list` LENGTH_IMP_CONS) THEN
1288 SUBGOAL_THEN `1 <= LENGTH (xl:(A)list)` (fun th -> REWRITE_TAC[th]) THENL
1290 MATCH_MP_TAC LE_TRANS THEN
1291 EXISTS_TAC `LENGTH (yl:(A)list)` THEN
1292 ASM_REWRITE_TAC[] THEN
1293 MATCH_MP_TAC INITIAL_SUBLIST_LENGTH_LE THEN
1297 REPEAT STRIP_TAC THEN
1298 MATCH_MP_TAC INITIAL_SUBLIST_HEAD_EQ THEN
1299 MAP_EVERY EXISTS_TAC [`yl:(A)list`; `xl:(A)list`; `t':(A)list`; `t:(A)list`] THEN
1300 ASM_REWRITE_TAC[HD]);;
1303 let SET_OF_LIST_INITIAL_SUBLIST_SUBSET = prove(`!vl ul:(A)list. initial_sublist vl ul ==> set_of_list vl SUBSET set_of_list ul`,
1304 REWRITE_TAC[INITIAL_SUBLIST] THEN
1305 REPEAT STRIP_TAC THEN
1306 ASM_REWRITE_TAC[SET_OF_LIST_APPEND; SUBSET_UNION]);;
1309 let LENGTH_REVERSE = prove(`!ul:(A)list. LENGTH (REVERSE ul) = LENGTH ul`,
1310 LIST_INDUCT_TAC THEN REWRITE_TAC[REVERSE; LENGTH] THEN
1311 ASM_REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
1315 let EL_REVERSE = prove(`!(ul:(A)list) i. i < LENGTH ul ==> EL i (REVERSE ul) = EL (LENGTH ul - 1 - i) ul`,
1316 LIST_INDUCT_TAC THENL
1318 REWRITE_TAC[LENGTH] THEN ARITH_TAC;
1321 REWRITE_TAC[LENGTH; REVERSE; EL_APPEND; LENGTH_REVERSE] THEN
1322 REPEAT STRIP_TAC THEN
1323 COND_CASES_TAC THENL
1325 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN
1326 ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1327 SUBGOAL_THEN `SUC (LENGTH t) - 1 - i = SUC (LENGTH (t:(A)list) - 1 - i)` (fun th -> REWRITE_TAC[th]) THENL
1329 POP_ASSUM MP_TAC THEN
1334 REWRITE_TAC[EL; TL];
1338 SUBGOAL_THEN `LENGTH (t:(A)list) = i` (fun th -> REWRITE_TAC[th]) THENL
1340 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1345 REWRITE_TAC[ARITH_RULE `i - i = 0`; ARITH_RULE `SUC i - 1 - i = 0`] THEN
1346 REWRITE_TAC[EL; HD]);;
1350 let LENGTH_TABLE = prove(`!(f:num->A) n. LENGTH (TABLE f n) = n`,
1351 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE] THENL
1353 REWRITE_TAC[LENGTH];
1356 ASM_REWRITE_TAC[GSYM TABLE; LENGTH_APPEND; LENGTH] THEN
1360 let EL_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,
1361 REPEAT GEN_TAC THEN SPEC_TAC (`n:num`, `n:num`) THEN
1362 INDUCT_TAC THENL [ ARITH_TAC; ALL_TAC ] THEN
1363 REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE; EL_APPEND] THEN
1364 REWRITE_TAC[GSYM TABLE; LENGTH_TABLE] THEN
1365 DISCH_TAC THEN COND_CASES_TAC THENL
1367 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1370 SUBGOAL_THEN `i = n:num` (fun th -> REWRITE_TAC[th]) THENL
1372 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1376 REWRITE_TAC[ARITH_RULE `n - n = 0`; EL; HD]);;
1380 let LENGTH_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p. LENGTH (left_action_list p ul) = LENGTH ul`,
1381 REWRITE_TAC[left_action_list; LENGTH_TABLE]);;
1385 let EL_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p i. p permutes (0..LENGTH ul - 1) /\ i < LENGTH ul
1386 ==> EL i ul = EL (p i) (left_action_list p ul)`,
1387 REPEAT STRIP_TAC THEN
1388 REWRITE_TAC[left_action_list] THEN
1389 ABBREV_TAC `n = LENGTH (ul:(A)list)` THEN
1390 SUBGOAL_THEN `(p:num->num) i < n` ASSUME_TAC THENL
1392 MP_TAC (ISPECL [`p:num->num`; `0..n - 1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
1393 ASM_REWRITE_TAC[IN_NUMSEG] THEN
1394 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
1395 ASM_REWRITE_TAC[ARITH_RULE `0 <= i`] THEN
1396 ASM_SIMP_TAC[ARITH_RULE `i < n ==> i <= n - 1`] THEN
1397 UNDISCH_TAC `i < n:num` THEN
1401 ASM_SIMP_TAC[EL_TABLE] THEN
1402 AP_THM_TAC THEN AP_TERM_TAC THEN
1403 MP_TAC (ISPECL [`p:num->num`; `0..n-1`] PERMUTES_INVERSES) THEN
1404 ASM_REWRITE_TAC[] THEN
1408 let MEM_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p x. p permutes (0..LENGTH ul - 1)
1409 ==> (MEM x (left_action_list p ul) <=> MEM x ul)`,
1410 REPEAT STRIP_TAC THEN
1411 ABBREV_TAC `n = LENGTH (ul:(A)list)` THEN
1412 ASM_REWRITE_TAC[MEM_EXISTS_EL; LENGTH_LEFT_ACTION_LIST] THEN
1416 POP_ASSUM MP_TAC THEN
1417 ASM_SIMP_TAC[left_action_list; EL_TABLE] THEN
1419 EXISTS_TAC `inverse (p:num->num) i` THEN
1421 MP_TAC (ISPECL [`p:num->num`; `0..n-1`] PERMUTES_INVERSE) THEN
1422 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1423 MP_TAC (ISPECL [`inverse (p:num->num)`; `0..n-1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
1424 ASM_REWRITE_TAC[] THEN
1425 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
1426 ASM_SIMP_TAC[IN_NUMSEG; ARITH_RULE `i < n ==> i <= n - 1`; LE_0] THEN
1427 UNDISCH_TAC `i < n:num` THEN ARITH_TAC;
1431 EXISTS_TAC `(p:num->num) i` THEN
1432 MP_TAC (SPEC_ALL EL_LEFT_ACTION_LIST) THEN
1433 ASM_SIMP_TAC[] THEN DISCH_TAC THEN
1434 MP_TAC (ISPECL [`p:num->num`; `0..n-1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
1435 ASM_REWRITE_TAC[IN_NUMSEG] THEN DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
1436 UNDISCH_TAC `i < n:num` THEN
1440 let SET_OF_LIST_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p. p permutes 0..LENGTH ul - 1
1441 ==> set_of_list (left_action_list p ul) = set_of_list ul`,
1442 REPEAT STRIP_TAC THEN
1443 REWRITE_TAC[EXTENSION; IN_SET_OF_LIST] THEN
1444 ASM_SIMP_TAC[MEM_LEFT_ACTION_LIST]);;
1448 let CARD_SET_OF_LIST_EQ_LENGTH_IMP_ALL_DISTINCT = prove(`!ul:(A)list. CARD (set_of_list ul) = LENGTH ul
1449 ==> (!i j. i < LENGTH ul /\ j < LENGTH ul /\ ~(i = j) ==> ~(EL i ul = EL j ul))`,
1450 LIST_INDUCT_TAC THEN REWRITE_TAC[set_of_list; LENGTH; CARD_CLAUSES; ARITH_RULE `~(j < 0)`] THEN
1451 SIMP_TAC[CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
1452 COND_CASES_TAC THENL
1454 MP_TAC (ISPEC `t:(A)list` CARD_SET_OF_LIST_LE) THEN
1459 REWRITE_TAC[ARITH_RULE `SUC n = SUC m <=> n = m`] THEN
1460 DISCH_THEN (fun th -> FIRST_X_ASSUM (ASSUME_TAC o (fun th2 -> MATCH_MP th2 th))) THEN
1461 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
1463 MP_TAC (SPEC `i:num` num_CASES) THEN STRIP_TAC THENL
1465 ASM_REWRITE_TAC[EL; HD] THEN
1466 MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
1468 UNDISCH_TAC `~(i = j:num)` THEN ASM_REWRITE_TAC[];
1472 ASM_REWRITE_TAC[EL; TL] THEN
1473 DISCH_TAC THEN UNDISCH_TAC `~(h:A IN set_of_list t)` THEN
1474 ASM_REWRITE_TAC[IN_SET_OF_LIST] THEN
1475 MATCH_MP_TAC (ISPECL [`t:(A)list`; `n:num`] MEM_EL) THEN
1476 UNDISCH_TAC `j = SUC n` THEN UNDISCH_TAC `j < SUC (LENGTH (t:(A)list))` THEN
1481 ASM_REWRITE_TAC[EL; TL] THEN
1482 MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
1484 ASM_REWRITE_TAC[EL; HD] THEN
1485 DISCH_THEN (ASSUME_TAC o SYM) THEN UNDISCH_TAC `~(h:A IN set_of_list t)` THEN
1486 ASM_REWRITE_TAC[IN_SET_OF_LIST] THEN
1487 MATCH_MP_TAC (ISPECL [`t:(A)list`; `n:num`] MEM_EL) THEN
1488 UNDISCH_TAC `i = SUC n` THEN UNDISCH_TAC `i < SUC (LENGTH (t:(A)list))` THEN
1493 ASM_REWRITE_TAC[EL; TL] THEN
1494 FIRST_X_ASSUM MATCH_MP_TAC THEN
1495 REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN
1499 let LENGTH_DROP = prove(`!i ul:(A)list. i < LENGTH ul ==> LENGTH (DROP ul i) = LENGTH ul - 1`,
1503 REWRITE_TAC[DROP] THEN DISCH_TAC THEN
1504 MATCH_MP_TAC LENGTH_TL THEN
1505 ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1509 REPEAT STRIP_TAC THEN
1510 REWRITE_TAC[DROP; LENGTH] THEN
1511 FIRST_X_ASSUM (MP_TAC o SPEC `TL ul:(A)list`) THEN
1512 SUBGOAL_THEN `LENGTH (TL ul) = LENGTH (ul:(A)list) - 1` ASSUME_TAC THENL
1514 MATCH_MP_TAC LENGTH_TL THEN
1515 ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1521 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1525 ASM_REWRITE_TAC[] THEN
1526 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1527 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1532 let EL_DROP = prove(`!i j ul:(A)list. i < LENGTH ul /\ j < LENGTH ul - 1 ==>
1533 EL j (DROP ul i) = if (j < i) then EL j ul else EL (j + 1) ul`,
1534 INDUCT_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THEN REWRITE_TAC[DROP; EL; LT_REFL; ARITH_RULE `0 + 1 = SUC 0`] THENL
1536 REWRITE_TAC[ARITH_RULE `~(x < 0)`; ARITH_RULE `SUC j + 1 = SUC (SUC j)`; EL];
1537 REWRITE_TAC[ARITH_RULE `0 < SUC i`; HD];
1541 REWRITE_TAC[ARITH_RULE `SUC j + 1 = SUC (SUC j)`; ARITH_RULE `SUC j < SUC i <=> j < i`; TL; EL] THEN
1542 FIRST_X_ASSUM (MP_TAC o SPECL [`j:num`; `TL ul:(A)list`]) THEN
1543 SUBGOAL_THEN `LENGTH (TL ul:(A)list) = LENGTH ul - 1` ASSUME_TAC THENL
1545 MATCH_MP_TAC LENGTH_TL THEN
1546 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1550 ASM_REWRITE_TAC[ARITH_RULE `j + 1 = SUC j`; EL] THEN
1551 DISCH_THEN MATCH_MP_TAC THEN
1552 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1556 let LIST_EL_EQ = prove(`!ul vl:(A)list. ul = vl <=>
1557 (LENGTH ul = LENGTH vl /\ (!j. j < LENGTH ul ==> EL j ul = EL j vl))`,
1558 REPEAT STRIP_TAC THEN
1559 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1560 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1561 SPEC_TAC (`vl:(A)list`, `vl:(A)list`) THEN SPEC_TAC (`ul:(A)list`, `ul:(A)list`) THEN
1562 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN SIMP_TAC[LENGTH_EQ_NIL; EQ_SYM_EQ; LENGTH; ARITH_RULE `~(0 = SUC a)`] THEN
1564 REWRITE_TAC[ARITH_RULE `SUC a = SUC b <=> a = b`] THEN
1565 REPEAT STRIP_TAC THEN
1566 FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN
1567 ASM_REWRITE_TAC[] THEN
1570 REPEAT STRIP_TAC THEN
1571 FIRST_X_ASSUM (MP_TAC o SPEC `SUC j`) THEN
1572 ASM_REWRITE_TAC[ARITH_RULE `SUC a < SUC b <=> a < b`; EL; TL];
1576 FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
1577 ASM_SIMP_TAC[ARITH_RULE `0 < SUC a`; EL; HD]);;
1580 let LEFT_ACTION_LIST_I = prove(`!ul:(A)list. left_action_list I ul = ul`,
1581 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1582 GEN_TAC THEN REWRITE_TAC[LIST_EL_EQ] THEN
1583 ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
1584 ASM_REWRITE_TAC[LENGTH_LEFT_ACTION_LIST] THEN
1585 REPEAT STRIP_TAC THEN
1586 ASM_SIMP_TAC[left_action_list; EL_TABLE; INVERSE_I; I_THM]);;
1591 let SET_OF_LIST_DELETE_SUBSET_DROP = prove(`!j ul:(A)list. j < LENGTH ul ==>
1592 set_of_list ul DELETE (EL j ul) SUBSET set_of_list (DROP ul j)`,
1593 REPEAT STRIP_TAC THEN
1594 ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
1595 ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_DELETE; MEM_EXISTS_EL] THEN
1596 REPEAT STRIP_TAC THEN
1597 MP_TAC (ISPECL [`j:num`; `ul:(A)list`] LENGTH_DROP) THEN
1598 ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1599 ASM_CASES_TAC `i:num < j` THENL
1601 EXISTS_TAC `i:num` THEN
1602 MP_TAC (ARITH_RULE `i < j /\ j < k ==> i < k - 1`) THEN
1603 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1604 ASM_REWRITE_TAC[] THEN
1605 MP_TAC (ISPECL [`j:num`; `i:num`; `ul:(A)list`] EL_DROP) THEN
1610 EXISTS_TAC `i - 1` THEN
1611 POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LT; LE_LT] THEN
1614 MP_TAC (ARITH_RULE `j < k /\ i < k /\ j < i ==> i - 1 < k - 1`) THEN
1615 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1616 ASM_REWRITE_TAC[] THEN
1617 MP_TAC (ISPECL [`j:num`; `i - 1`; `ul:(A)list`] EL_DROP) THEN
1618 ASM_SIMP_TAC[ARITH_RULE `j < i ==> ~(i - 1 < j)`] THEN
1619 MP_TAC (ARITH_RULE `j < i ==> i - 1 + 1 = i`) THEN
1624 UNDISCH_TAC `x:A = EL i ul` THEN
1625 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
1630 let SET_OF_LIST_DELETE_EQ_DROP = prove(`!j ul:(A)list. CARD (set_of_list ul) = LENGTH ul /\ j < LENGTH ul
1631 ==> set_of_list ul DELETE (EL j ul) = set_of_list (DROP ul j)`,
1632 REPEAT STRIP_TAC THEN
1633 MATCH_MP_TAC SUBSET_ANTISYM THEN
1634 ASM_SIMP_TAC[SET_OF_LIST_DELETE_SUBSET_DROP] THEN
1635 ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
1636 MP_TAC (SPECL [`j:num`; `ul:(A)list`] LENGTH_DROP) THEN
1637 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1638 ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_DELETE; MEM_EXISTS_EL] THEN
1639 GEN_TAC THEN STRIP_TAC THEN
1640 POP_ASSUM (ASSUME_TAC o SYM) THEN
1641 MP_TAC (SPECL [`j:num`; `i:num`; `ul:(A)list`] EL_DROP) THEN
1642 ASM_REWRITE_TAC[] THEN
1643 MP_TAC (ARITH_RULE `i < k - 1 ==> i < k`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1645 MP_TAC (SPEC `ul:(A)list` CARD_SET_OF_LIST_EQ_LENGTH_IMP_ALL_DISTINCT) THEN
1646 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1648 COND_CASES_TAC THENL
1653 EXISTS_TAC `i:num` THEN
1657 ASM_REWRITE_TAC[] THEN
1658 FIRST_X_ASSUM MATCH_MP_TAC THEN
1659 ASM_SIMP_TAC[ARITH_RULE `i < j ==> ~(i = j:num)`];
1666 EXISTS_TAC `i + 1` THEN
1667 ASM_SIMP_TAC[ARITH_RULE `i < k - 1 ==> i + 1 < k`];
1670 ASM_REWRITE_TAC[] THEN
1671 FIRST_X_ASSUM MATCH_MP_TAC THEN
1672 ASM_SIMP_TAC[ARITH_RULE `i < k - 1 ==> i + 1 < k`] THEN
1673 UNDISCH_TAC `~(i < j:num)` THEN ARITH_TAC);;
1679 (**********************************************************)
1681 (*****************************************)
1682 (* Properties of barV *)
1683 (*****************************************)
1685 (* barV(k) SUBSET V *)
1686 let BARV_SUBSET = prove(`!V k ul. barV V k ul ==> set_of_list ul SUBSET V`,
1688 REWRITE_TAC[BARV; VORONOI_NONDG; INITIAL_SUBLIST] THEN
1690 POP_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
1693 ASM_REWRITE_TAC[ARITH_RULE `0 < k + 1`] THEN
1694 EXISTS_TAC `[]:(real^3)list` THEN
1695 REWRITE_TAC[APPEND_NIL];
1701 (* barV(k) = (h:t) for some h, t *)
1702 let BARV_CONS = prove(`!V k ul. barV V k ul ==> ?h t. ul = CONS h t /\ h = HD ul`,
1704 REWRITE_TAC[BARV] THEN
1705 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
1706 REWRITE_TAC[GSYM ADD1; LENGTH_EQ_CONS] THEN
1707 ASM_MESON_TAC[HD]);;
1711 (* An initial sublist of barV(k) is barV(length - 1) *)
1712 let BARV_INITIAL_SUBLIST = prove(`!V k ul vl. barV V k ul /\ initial_sublist vl ul /\ 0 < LENGTH vl ==> barV V ((LENGTH vl) - 1) vl`,
1713 REWRITE_TAC[BARV] THEN
1714 REPEAT STRIP_TAC THENL
1716 ASM_SIMP_TAC[ARITH_RULE `0 < a ==> a - 1 + 1 = a`];
1720 MP_TAC (ISPECL [`vl':(real^3)list`; `vl:(real^3)list`; `ul:(real^3)list`] INITIAL_SUBLIST_TRANS) THEN
1721 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1722 FIRST_X_ASSUM (MP_TAC o SPEC `vl':(real^3)list`) THEN
1726 (* barV V 0 [v] (if v IN V) *)
1727 let BARV_0 = prove(`!V v. packing V /\ v IN V ==> barV V 0 [v]`,
1728 REPEAT STRIP_TAC THEN
1729 REWRITE_TAC[BARV; VORONOI_NONDG; LENGTH; ARITH] THEN
1730 REWRITE_TAC[INITIAL_SUBLIST_SING] THEN
1732 STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
1733 ASM_SIMP_TAC[set_of_list; SUBSET; IN_SING] THEN
1734 ASM_REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET; IN_SING; SING_GSPEC_APP; INTERS_1] THEN
1735 ASM_SIMP_TAC[AFF_DIM_VORONOI_CLOSED] THEN
1739 (* ul IN barV V k ==> k <= 3 *)
1740 let BARV_IMP_K_LE_3 = prove(`!V ul k. barV V k ul ==> k <= 3`,
1741 REWRITE_TAC[BARV; VORONOI_NONDG] THEN
1742 REPEAT STRIP_TAC THEN
1743 FIRST_X_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
1744 ASM_REWRITE_TAC[INITIAL_SUBLIST_REFL; ARITH_RULE `0 < k + 1`] THEN
1748 (* ul IN barV V k ul ==> HD ul IN set_of_list ul *)
1749 let BARV_IMP_HD_IN_SET_OF_LIST = prove(`!V k ul. barV V k ul ==> HD ul IN set_of_list ul`,
1750 REPEAT STRIP_TAC THEN
1751 MATCH_MP_TAC HD_IN_SET_OF_LIST THEN
1752 POP_ASSUM MP_TAC THEN
1753 REWRITE_TAC[BARV] THEN
1759 (* Lemma for truncate_simplex operation *)
1760 let TRUNCATE_SIMPLEX_INITIAL_SUBLIST = prove(`!k xl (zl:(A)list). truncate_simplex k zl = xl /\ k + 1 <= LENGTH zl <=> initial_sublist xl zl /\ LENGTH xl = k + 1`,
1761 REPEAT GEN_TAC THEN EQ_TAC THENL
1763 REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
1765 POP_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_EXISTS th)) THEN
1768 MP_TAC (ISPECL [`xl:(A)list`; `zl:(A)list`] INITIAL_SUBLIST_LENGTH_LE) THEN
1771 REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
1772 ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE]
1777 let TRUNCATE_SIMPLEX_BARV = prove(`!V r k zl. barV V k zl /\ r <= k ==> barV V r (truncate_simplex r zl)`,
1778 REPEAT STRIP_TAC THEN
1779 SUBGOAL_TAC "A" `LENGTH (zl:(real^3)list) = k + 1` [ ASM_MESON_TAC[BARV] ] THEN
1780 ABBREV_TAC `xl:(real^3)list = truncate_simplex r zl` THEN
1781 SUBGOAL_THEN `initial_sublist xl (zl:(real^3)list) /\ LENGTH xl = r + 1` STRIP_ASSUME_TAC THENL
1783 REWRITE_TAC[GSYM TRUNCATE_SIMPLEX_INITIAL_SUBLIST] THEN
1784 ASM_SIMP_TAC[ARITH_RULE `r <= k ==> r + 1 <= k + 1`];
1787 MP_TAC (ISPECL [`V:real^3->bool`; `k:num`; `zl:(real^3)list`; `xl:(real^3)list`] BARV_INITIAL_SUBLIST) THEN
1788 ASM_SIMP_TAC[ARITH_RULE `0 < r + 1`; ARITH_RULE `(r + 1) - 1 = r`]);;
1792 let TRUNCATE_SIMPLEX_REFL = prove(`!k ul:(A)list. LENGTH ul = k + 1 ==> truncate_simplex k ul = ul`,
1793 REPEAT STRIP_TAC THEN
1794 MP_TAC (SPECL [`k:num`; `ul:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1795 ASM_REWRITE_TAC[LE_REFL; INITIAL_SUBLIST_REFL]);;
1799 let TRUNCATE_0_EQ_HEAD = prove(`!ul:(A)list. 1 <= LENGTH ul ==> truncate_simplex 0 ul = [HD ul]`,
1800 REPEAT STRIP_TAC THEN
1801 MP_TAC (SPECL [`0`; `[HD ul]:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1802 ASM_REWRITE_TAC[ARITH] THEN
1803 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1804 ASM_SIMP_TAC[INITIAL_SUBLIST_HD; LENGTH; ARITH]);;
1807 let LENGTH_TRUNCATE_SIMPLEX = prove(`!k ul:(A)list. k + 1 <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = k + 1`,
1808 REPEAT STRIP_TAC THEN
1809 MP_TAC (SPECL [`k:num`; `truncate_simplex k ul:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1814 let TRUNCATE_SIMPLEX_EQ_BUTLAST = prove(`!ul:(A)list. 2 <= LENGTH ul ==> truncate_simplex (LENGTH ul - 2) ul = BUTLAST ul`,
1815 REPEAT STRIP_TAC THEN
1816 MP_TAC (SPECL [`LENGTH (ul:(A)list) - 2`; `BUTLAST (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1817 ASM_SIMP_TAC[ARITH_RULE `2 <= a ==> a - 2 + 1 = a - 1 /\ a - 1 <= a`] THEN
1818 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1819 ASM_SIMP_TAC[ARITH_RULE `2 <= a ==> 1 <= a`; BUTLAST_INITIAL_SUBLIST; LENGTH_BUTLAST]);;
1822 let HD_TRUNCATE_SIMPLEX = prove(`!(ul:(A)list) j. j + 1 <= LENGTH ul ==> HD (truncate_simplex j ul) = HD ul`,
1823 REPEAT STRIP_TAC THEN
1824 MP_TAC (SPECL [`j:num`; `truncate_simplex j (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1825 ASM_REWRITE_TAC[] THEN
1827 MATCH_MP_TAC HD_INITIAL_SUBLIST THEN
1828 ASM_REWRITE_TAC[ARITH_RULE `1 <= j + 1`]);;
1831 let TRUNCATE_TRUNCATE_SIMPLEX = prove(`!(ul:(A)list) i j. i <= j /\ j + 1 <= LENGTH ul ==>
1832 truncate_simplex i (truncate_simplex j ul) = truncate_simplex i ul`,
1833 REPEAT STRIP_TAC THEN
1834 ABBREV_TAC `xl = truncate_simplex j (ul:(A)list)` THEN
1835 SUBGOAL_THEN `i + 1 <= LENGTH (xl:(A)list) /\ i + 1 <= LENGTH (ul:(A)list) /\ initial_sublist (xl:(A)list) ul` STRIP_ASSUME_TAC THENL
1837 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1838 MP_TAC (SPECL [`j:num`; `truncate_simplex j (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1840 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1844 MP_TAC (SPECL [`i:num`; `truncate_simplex i (xl:(A)list)`; `xl:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1845 MP_TAC (SPECL [`i:num`; `truncate_simplex i (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1846 ASM_REWRITE_TAC[] THEN
1847 REPEAT STRIP_TAC THEN
1848 MATCH_MP_TAC INITIAL_SUBLIST_UNIQUE THEN
1849 MAP_EVERY EXISTS_TAC [`i + 1`; `ul:(A)list`] THEN
1850 ASM_REWRITE_TAC[] THEN
1851 MATCH_MP_TAC INITIAL_SUBLIST_TRANS THEN
1852 EXISTS_TAC `xl:(A)list` THEN
1853 ASM_REWRITE_TAC[]);;
1856 let INITIAL_SUBLIST_IMP_TRUNCATE_SIMPLEX = prove(`!xl yl:(A)list. initial_sublist yl xl /\ 1 <= LENGTH yl ==>
1857 yl = truncate_simplex (LENGTH yl - 1) xl /\ LENGTH yl <= LENGTH xl`,
1858 REPEAT STRIP_TAC THENL
1860 MP_TAC (SPECL [`LENGTH (yl:(A)list) - 1`; `yl:(A)list`; `xl:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1861 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1862 SUBGOAL_THEN `LENGTH yl = LENGTH (yl:(A)list) - 1 + 1` MP_TAC THENL
1864 UNDISCH_TAC `1 <= LENGTH (yl:(A)list)` THEN ARITH_TAC;
1867 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1871 ASM_SIMP_TAC[INITIAL_SUBLIST_LENGTH_LE]);;
1874 let LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST = prove(`!ul:(A)list. 2 <= LENGTH ul ==>
1875 ul = APPEND (truncate_simplex (LENGTH ul - 2) ul) [LAST ul]`,
1876 ASM_SIMP_TAC[TRUNCATE_SIMPLEX_EQ_BUTLAST] THEN
1877 REPEAT STRIP_TAC THEN
1878 MATCH_MP_TAC (GSYM APPEND_BUTLAST_LAST) THEN
1879 REWRITE_TAC[EQ_SYM_EQ; GSYM LENGTH_EQ_NIL] THEN
1880 POP_ASSUM MP_TAC THEN ARITH_TAC);;
1883 let TRUNCATE_SIMPLEX_ADD1 = prove(`!(ul:(A)list) k. k + 2 <= LENGTH ul ==>
1884 truncate_simplex (k + 1) ul = APPEND (truncate_simplex k ul) [LAST (truncate_simplex (k + 1) ul)]`,
1885 REPEAT STRIP_TAC THEN
1886 ABBREV_TAC `xl:(A)list = truncate_simplex (k + 1) ul` THEN
1887 SUBGOAL_THEN `truncate_simplex k ul = truncate_simplex k xl:(A)list` (fun th -> REWRITE_TAC[th]) THENL
1889 EXPAND_TAC "xl" THEN
1890 MATCH_MP_TAC (GSYM TRUNCATE_TRUNCATE_SIMPLEX) THEN
1891 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1894 SUBGOAL_THEN `LENGTH (xl:(A)list) = k + 2` ASSUME_TAC THENL
1896 EXPAND_TAC "xl" THEN
1897 REWRITE_TAC[ARITH_RULE `k + 2 = (k + 1) + 1`] THEN
1898 MATCH_MP_TAC LENGTH_TRUNCATE_SIMPLEX THEN
1899 ASM_REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 2`];
1902 SUBGOAL_THEN `k = LENGTH (xl:(A)list) - 2` (fun th -> REWRITE_TAC[th]) THENL
1904 POP_ASSUM MP_TAC THEN ARITH_TAC;
1908 MATCH_MP_TAC LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST THEN
1909 POP_ASSUM MP_TAC THEN ARITH_TAC);;
1913 let EL_TRUNCATE_SIMPLEX = prove(`!ul:(A)list k j. k + 1 <= LENGTH ul /\ j <= k ==> EL j (truncate_simplex k ul) = EL j ul`,
1914 REPEAT STRIP_TAC THEN
1915 ABBREV_TAC `vl:(A)list = truncate_simplex k ul` THEN
1916 SUBGOAL_THEN `?yl:(A)list. ul = APPEND vl yl /\ LENGTH vl = k + 1` CHOOSE_TAC THENL
1918 MP_TAC (SPECL [`k:num`; `vl:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1919 ASM_REWRITE_TAC[INITIAL_SUBLIST] THEN
1921 EXISTS_TAC `yl:(A)list` THEN ASM_REWRITE_TAC[];
1924 ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `j < k + 1 <=> j <= k`]);;
1928 let TRUNCATE_SIMPLEX_ADD1_ALT = prove(`!ul:(A)list k. k + 2 <= LENGTH ul
1929 ==> truncate_simplex (k + 1) ul = APPEND (truncate_simplex k ul) [EL (k + 1) ul]`,
1930 REPEAT STRIP_TAC THEN
1931 MP_TAC (SPEC_ALL TRUNCATE_SIMPLEX_ADD1) THEN
1932 ASM_REWRITE_TAC[] THEN
1933 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
1936 MP_TAC (SPECL [`k + 1`; `ul:(A)list`] LENGTH_TRUNCATE_SIMPLEX) THEN
1937 ASM_SIMP_TAC[ARITH_RULE `k + 2 <= a ==> (k + 1) + 1 <= a`] THEN
1940 MP_TAC (ISPEC `(truncate_simplex (k + 1) ul:(A)list)` LAST_EL) THEN
1941 ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL; ARITH_RULE `~(a + 1 = 0)`; ARITH_RULE `(a + 1) - 1 = a`] THEN
1942 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1943 MP_TAC (SPECL [`ul:(A)list`; `k + 1`; `k + 1`] EL_TRUNCATE_SIMPLEX) THEN
1944 ASM_SIMP_TAC[ARITH_RULE `k + 2 <= a ==> (k + 1) + 1 <= a`; LE_REFL]);;
1948 (****************************************************)
1950 (***************************************************************************)
1951 (* Properties of voronoi_set (Omega(V, W)) and voronoi_list (Omega(V, vl)) *)
1952 (***************************************************************************)
1955 (* Equivalent definitions for intersections of one and two Voronoi cells *)
1956 let VORONOI_SET_SING = prove(`!V (u:real^3). voronoi_set V {u} = voronoi_closed V u`,
1957 REWRITE_TAC[VORONOI_SET; IN_SING; EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
1961 let VORONOI_LIST_SING = prove(`!V (u:real^3). voronoi_list V [u] = voronoi_closed V u`,
1962 REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET_SING]);;
1965 (* Omega(V, v) INTER Omega(V, u) *)
1966 let VORONOI_SET_2 = prove(`!V (u:real^3) v. voronoi_set V {u, v} = voronoi_closed V v INTER voronoi_closed V u`,
1967 REWRITE_TAC[VORONOI_SET; INTERS_2_LEMMA; INTER_COMM]);;
1970 (* Omega(V, v) INTER A(u, v) *)
1971 let VORONOI_SET_2_BIS = prove(`!V (u:real^3) v. u IN V /\ v IN V ==> voronoi_set V {u, v} = voronoi_closed V v INTER bis u v`,
1972 REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
1973 REWRITE_TAC[VORONOI_SET_2; bis; voronoi_closed; EXTENSION; IN_INTER; IN_ELIM_THM] THEN
1974 REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
1975 ASM_MESON_TAC[REAL_ARITH `a <= b /\ b <= a ==> a = b`]);;
1978 (* Omega(V, v) INTER A+(u, v) *)
1979 let VORONOI_SET_2_BIS_LE = prove(`!V (u:real^3) v. u IN V /\ v IN V ==> voronoi_set V {u, v} = voronoi_closed V v INTER bis_le u v`,
1980 REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
1981 REWRITE_TAC[VORONOI_SET_2; bis_le; voronoi_closed; EXTENSION; IN_INTER; IN_ELIM_THM] THEN
1982 REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
1983 ASM_MESON_TAC[REAL_LE_TRANS]);;
1986 (* The result for lists of arbitrary length *)
1987 let VORONOI_LIST_BIS = prove(`!V ul (h:real^3) t. set_of_list ul SUBSET V /\ ul = CONS h t ==> voronoi_list V ul = voronoi_closed V h INTER (INTERS {bis h u | u | u IN set_of_list t})`,
1988 REPEAT STRIP_TAC THEN
1989 SUBGOAL_THEN `V (h:real^3) /\ (!u. u IN set_of_list t ==> V u)` ASSUME_TAC THENL
1991 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1992 DISCH_THEN (LABEL_TAC "A") THEN DISCH_TAC THEN
1993 REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[] THEN
1994 REWRITE_TAC[set_of_list] THEN
1999 REWRITE_TAC[VORONOI_LIST; VORONOI_SET; bis; EXTENSION; IN_INTER; IN_INTERS; IN_ELIM_THM] THEN
2000 X_GEN_TAC `y:real^3` THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
2002 FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V (h:real^3)`) THEN
2003 ASM_REWRITE_TAC[set_of_list] THEN
2004 ANTS_TAC THEN REWRITE_TAC[] THEN
2005 EXISTS_TAC `h:real^3` THEN
2006 REWRITE_TAC[COMPONENT];
2008 ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> ALL_TAC) THEN
2009 SUBGOAL_THEN `y:real^3 IN voronoi_closed V h` ASSUME_TAC THENL
2011 POP_ASSUM (fun th -> ALL_TAC) THEN
2012 POP_ASSUM (MP_TAC o SPEC `voronoi_closed V (h:real^3)`) THEN
2013 ANTS_TAC THEN REWRITE_TAC[] THEN
2014 EXISTS_TAC `h:real^3` THEN
2015 ASM_REWRITE_TAC[set_of_list; COMPONENT];
2019 SUBGOAL_THEN `y:real^3 IN voronoi_closed V u` ASSUME_TAC THENL
2021 FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V (u:real^3)` o check (is_forall o concl)) THEN
2022 ANTS_TAC THEN REWRITE_TAC[] THEN
2023 EXISTS_TAC `u:real^3` THEN
2024 ASM_REWRITE_TAC[set_of_list; IN_INSERT];
2028 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
2029 REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN
2030 DISCH_THEN (ASSUME_TAC o SPEC `u:real^3`) THEN
2031 DISCH_THEN (ASSUME_TAC o SPEC `h:real^3`) THEN
2032 ASM_MESON_TAC[REAL_ARITH `a <= b /\ b <= a ==> a = b`];
2035 ASM_REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN GEN_TAC THEN
2036 POP_ASSUM (fun th -> ALL_TAC) THEN
2037 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_list; IN_INSERT] THEN
2038 POP_ASSUM (MP_TAC o SPEC `bis h (v:real^3)`) THEN
2039 POP_ASSUM MP_TAC THEN REWRITE_TAC[bis; voronoi_closed; IN_ELIM_THM] THEN
2040 REPEAT STRIP_TAC THENL
2046 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
2049 EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[];
2060 let VORONOI_INTER_BIS_EQ_INTER_BIS_LE = prove(`!V v u. v IN V /\ u IN V ==> voronoi_closed V v INTER bis u v = voronoi_closed V v INTER bis_le u v`,
2061 REWRITE_TAC[voronoi_closed; bis; bis_le; IN] THEN
2062 REPEAT STRIP_TAC THEN
2063 REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN
2064 ASM_MESON_TAC[REAL_EQ_IMP_LE; REAL_LE_ANTISYM]);;
2068 let LIST_SUBSET = prove(`!V ul (h:A) t. ((set_of_list ul) SUBSET V /\ ul = CONS h t) ==> h IN V /\ (!u. u IN set_of_list t ==> u IN V)`,
2071 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
2072 DISCH_THEN (LABEL_TAC "A") THEN
2073 DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN
2074 ASM_REWRITE_TAC[set_of_list; INSERT_SUBSET] THEN
2079 (* Omega(V,h:t) = Omega(V,h) INTER INTERS {A+(u, h) | u IN t} *)
2080 let VORONOI_LIST_BIS_LE = prove(`!V ul (h:real^3) t. set_of_list ul SUBSET V /\ ul = CONS h t ==> voronoi_list V ul = voronoi_closed V h INTER (INTERS {bis_le u h| u | u IN set_of_list t})`,
2083 MP_TAC (ISPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] LIST_SUBSET) THEN
2084 FIRST_ASSUM ((fun th -> REWRITE_TAC[th]) o (fun th -> MATCH_MP VORONOI_LIST_BIS th)) THEN
2085 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2086 DISJ_CASES_TAC (TAUT `set_of_list (t:(real^3)list) = {} \/ ~(set_of_list t = {})`) THENL
2088 ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN SET_TAC[];
2091 ASM_SIMP_TAC[INTER_INTERS] THEN
2092 REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
2093 ASM_MESON_TAC[BIS_SYM; VORONOI_INTER_BIS_EQ_INTER_BIS_LE]);;
2098 (* Voronoi list is bounded *)
2099 let BOUNDED_VORONOI_LIST = prove(`!V k ul. saturated V /\ barV V k ul ==> bounded (voronoi_list V ul)`,
2100 REPEAT STRIP_TAC THEN
2101 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP BARV_SUBSET th)) THEN
2102 FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP BARV_CONS th)) THEN
2103 STRIP_TAC THEN POP_ASSUM (fun th -> ALL_TAC) THEN
2105 MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS_LE) THEN
2106 ASM_REWRITE_TAC[] THEN
2107 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2108 MATCH_MP_TAC BOUNDED_INTER THEN
2110 ASM_SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;
2114 (* Omega(V, h:t) INTER A(h, v) = Omega(V, (h:t) ++ [v]) *)
2115 let VORONOI_LIST_INTER_BIS = prove(`!V ul v h t. set_of_list ul SUBSET V /\ v IN V /\ ul = CONS h t ==>
2116 (voronoi_list V ul) INTER (bis h v) = voronoi_list V (APPEND ul [v])`,
2117 REPEAT STRIP_TAC THEN
2118 MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS) THEN
2119 ASM_REWRITE_TAC[] THEN
2120 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2121 REWRITE_TAC[APPEND] THEN
2122 MP_TAC (SPECL [`V:real^3->bool`; `CONS (h:real^3) (APPEND t [v])`; `h:real^3`; `APPEND t [v:real^3]`] VORONOI_LIST_BIS) THEN
2123 SUBGOAL_THEN `set_of_list (CONS (h:real^3) (APPEND t [v])) SUBSET V` (fun th -> REWRITE_TAC[th]) THENL
2125 REWRITE_TAC[GSYM APPEND] THEN
2126 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2127 REWRITE_TAC[SUBSET; IN_SET_OF_LIST; MEM_APPEND; MEM] THEN
2128 REPEAT STRIP_TAC THENL
2130 ASM_MESON_TAC[SUBSET; IN_SET_OF_LIST];
2136 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2137 REWRITE_TAC[IN_SET_OF_LIST; MEM_APPEND; MEM] THEN
2142 (* Canonical representations of Omega(V, vl) as a polyhedron *)
2145 let SUPSET_INTER = prove(`!s t u. s SUBSET t /\ s = u ==> s = t INTER u`, SET_TAC[]);;
2148 let INTER_AFFINE_HULL = prove(`!(s:real^N->bool). s = affine hull s INTER s`,
2149 GEN_TAC THEN MATCH_MP_TAC SUPSET_INTER THEN
2150 MESON_TAC[CLOSURE_SUBSET; CLOSURE_SUBSET_AFFINE_HULL; SUBSET_TRANS]);;
2154 (* "Almost canonical" polyhedron representation for Omega(V, ul) *)
2156 let VORONOI_LIST_ALMOST_CANONICAL_0 = prove(`!V ul (h:real^3) t. packing V /\ saturated V /\ set_of_list ul SUBSET V /\ ul = CONS h t
2157 ==> ?K. FINITE K /\ voronoi_list V ul = INTERS K /\
2158 (!a. a IN K ==> (?v. v IN V /\ (a = bis_le v h \/ a = bis_le h v)))`,
2161 MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS_LE) THEN
2162 ASM_REWRITE_TAC[] THEN
2163 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2164 MP_TAC (ISPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] LIST_SUBSET) THEN
2165 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2166 MP_TAC (SPECL [`V:real^3->bool`; `h:real^3`] VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE) THEN
2167 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2168 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
2169 EXISTS_TAC `{bis_le h u | u IN (W:real^3->bool)} UNION {bis_le u (h:real^3) | u IN set_of_list t}` THEN
2170 REPEAT STRIP_TAC THENL
2172 REWRITE_TAC[FINITE_UNION] THEN
2173 REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
2174 CONJ_TAC THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[FINITE_SET_OF_LIST];
2176 REWRITE_TAC[INTERS_INTER_INTERS];
2183 let VORONOI_LIST_ALMOST_CANONICAL = prove(`!V ul (h:real^3) t. packing V /\ saturated V /\ set_of_list ul SUBSET V /\ ul = CONS h t
2184 ==> ?K. FINITE K /\ voronoi_list V ul = affine hull (voronoi_list V ul) INTER INTERS K /\
2185 (!a. a IN K ==> (?v. v IN V /\ ~(v = h) /\ (a = bis_le v h \/ a = bis_le h v)))`,
2187 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL_0 th)) THEN
2189 EXISTS_TAC `K DELETE (:real^3)` THEN
2190 ASM_REWRITE_TAC[FINITE_DELETE; GSYM INTERS_UNIV; IN_DELETE] THEN
2191 REWRITE_TAC[INTER_AFFINE_HULL] THEN
2192 REPEAT STRIP_TAC THEN
2193 FIRST_X_ASSUM (MP_TAC o SPEC `a:real^3->bool`) THEN
2194 ASM_REWRITE_TAC[] THEN
2195 DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN
2196 EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[] THEN
2197 DISJ_CASES_TAC (TAUT `~(v:real^3 = h) \/ (v = h)`) THEN ASM_REWRITE_TAC[] THEN
2198 FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
2199 ASM_REWRITE_TAC[bis_le; REAL_LE_REFL] THEN
2206 (* For a canonical polyhedron representation we need to find a minimal intersection *)
2207 let lemma1 = prove(`!f P. FINITE f /\ P f ==> (?n g. g SUBSET f /\ g HAS_SIZE n /\ P g)`, MESON_TAC[FINITE_HAS_SIZE; SUBSET_REFL]);;
2209 (* Lemma about minimal intersection *)
2210 (* The proof is a modification of the proof of POLYHEDRON_INTER_AFFINE_MINIMAL *)
2211 let MINIMAL_INTERS_EXISTS = prove(`!(s:A->bool) f. FINITE f /\ s = INTERS f ==> (?g. g SUBSET f /\ s = INTERS g /\ (!g'. g' PSUBSET g ==> s PSUBSET INTERS g'))`,
2213 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP lemma1 th)) THEN
2214 GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
2215 DISCH_THEN(X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
2216 MATCH_MP_TAC MONO_EXISTS THEN
2217 SIMP_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
2218 X_GEN_TAC `g:(A->bool)->bool` THEN STRIP_TAC THEN
2219 X_GEN_TAC `g':(A->bool)->bool` THEN DISCH_TAC THEN
2220 FIRST_X_ASSUM(MP_TAC o SPEC `CARD(g':(A->bool)->bool)`) THEN
2221 ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET]; ALL_TAC] THEN
2222 REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN
2223 DISCH_THEN(MP_TAC o SPEC `g':(A->bool)->bool`) THEN
2224 MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
2225 CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; SUBSET_TRANS]; ALL_TAC] THEN
2226 CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET]; ALL_TAC] THEN
2227 ASM_REWRITE_TAC[] THEN
2228 MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN
2229 FIRST_X_ASSUM MP_TAC THEN
2234 (* Variation of the previous lemma: the proof is exactly the same *)
2235 let MINIMAL_INTER_INTERS_EXISTS = prove(`!(s:A->bool) t f. FINITE f /\ s = t INTER INTERS f ==> (?g. g SUBSET f /\ s = t INTER INTERS g /\ (!g'. g' PSUBSET g ==> s PSUBSET t INTER INTERS g'))`,
2237 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP lemma1 th)) THEN
2238 GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
2239 DISCH_THEN(X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
2240 MATCH_MP_TAC MONO_EXISTS THEN
2241 SIMP_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
2242 X_GEN_TAC `g:(A->bool)->bool` THEN STRIP_TAC THEN
2243 X_GEN_TAC `g':(A->bool)->bool` THEN DISCH_TAC THEN
2244 FIRST_X_ASSUM(MP_TAC o SPEC `CARD(g':(A->bool)->bool)`) THEN
2245 ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET]; ALL_TAC] THEN
2246 REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN
2247 DISCH_THEN(MP_TAC o SPEC `g':(A->bool)->bool`) THEN
2248 MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
2249 CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; SUBSET_TRANS]; ALL_TAC] THEN
2250 CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET]; ALL_TAC] THEN
2251 ASM_REWRITE_TAC[] THEN
2252 MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN
2253 FIRST_X_ASSUM MP_TAC THEN
2259 (* Canonical polyhedron representation for Omega(V, ul) *)
2260 let VORONOI_LIST_CANONICAL = prove(`!V ul (h:real^3) t. packing V /\ saturated V /\ set_of_list ul SUBSET V /\ ul = CONS h t
2261 ==> ?K. FINITE K /\ voronoi_list V ul = affine hull (voronoi_list V ul) INTER INTERS K /\
2262 (!a. a IN K ==> (?v. v IN V /\ ~(v = h) /\ (a = bis_le v h \/ a = bis_le h v))) /\
2263 (!K'. K' PSUBSET K ==> voronoi_list V ul PSUBSET affine hull (voronoi_list V ul) INTER INTERS K')`,
2265 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL th)) THEN
2268 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
2269 DISCH_THEN (LABEL_TAC "A") THEN
2270 DISCH_THEN (LABEL_TAC "B") THEN
2271 DISCH_THEN (LABEL_TAC "C") THEN
2273 MP_TAC (ISPECL [`voronoi_list (V:real^3->bool) ul`; `affine hull (voronoi_list (V:real^3->bool) ul)`; `K:(real^3->bool)->bool`] MINIMAL_INTER_INTERS_EXISTS) THEN
2275 USE_THEN "A" (fun th -> REWRITE_TAC[th]) THEN
2283 EXISTS_TAC `g:(real^3->bool)->bool` THEN
2284 ASM_REWRITE_TAC[] THEN
2285 REPEAT STRIP_TAC THENL
2287 ASM_MESON_TAC[FINITE_SUBSET];
2289 POP_ASSUM MP_TAC THEN
2290 REPLICATE_TAC 2 (POP_ASSUM (fun th -> ALL_TAC)) THEN
2291 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN
2292 REWRITE_TAC[SUBSET] THEN MESON_TAC[]
2296 (* voronoi_list is a polyhedron *)
2297 let POLYHEDRON_VORONOI_LIST = prove(`!V ul. packing V /\ saturated V /\ set_of_list ul SUBSET V
2298 ==> polyhedron (voronoi_list V ul)`,
2299 REPEAT STRIP_TAC THEN
2300 DISJ_CASES_TAC (ISPEC `ul:(real^3)list` list_CASES) THENL
2302 ASM_REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET; NOT_IN_EMPTY] THEN
2303 SUBGOAL_THEN `{voronoi_closed V (v:real^3) | v | F} = {}` (fun th -> REWRITE_TAC[th]) THENL
2305 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM];
2308 REWRITE_TAC[INTERS_0; POLYHEDRON_UNIV];
2312 POP_ASSUM STRIP_ASSUME_TAC THEN
2313 ASM_SIMP_TAC[VORONOI_LIST_BIS] THEN
2315 MATCH_MP_TAC POLYHEDRON_INTER THEN
2318 MATCH_MP_TAC VORONOI_POLYHEDRON THEN
2319 ASM_REWRITE_TAC[] THEN
2320 MATCH_MP_TAC IN_TRANS THEN
2321 EXISTS_TAC `set_of_list ul:real^3->bool` THEN
2322 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
2326 MATCH_MP_TAC POLYHEDRON_INTERS THEN
2329 ONCE_REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
2330 MATCH_MP_TAC FINITE_IMAGE THEN
2331 REWRITE_TAC[FINITE_SET_OF_LIST];
2335 REWRITE_TAC[IN_ELIM_THM] THEN
2336 REPEAT STRIP_TAC THEN
2337 ASM_REWRITE_TAC[POLYHEDRON_BIS]);;
2340 (* voronoi_list is a polytope *)
2341 let POLYTOPE_VORONOI_LIST = prove(`!V ul. packing V /\ saturated V /\ set_of_list ul SUBSET V /\ ~(ul = [])
2342 ==> polytope (voronoi_list V ul)`,
2343 REPEAT STRIP_TAC THEN
2344 REWRITE_TAC[POLYTOPE_EQ_BOUNDED_POLYHEDRON] THEN
2345 ASM_SIMP_TAC[POLYHEDRON_VORONOI_LIST] THEN
2346 MP_TAC (ISPEC `ul:(real^3)list` list_CASES) THEN
2347 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2348 ASM_SIMP_TAC[VORONOI_LIST_BIS] THEN
2349 MATCH_MP_TAC BOUNDED_SUBSET THEN
2350 EXISTS_TAC `voronoi_closed V (h:real^3)` THEN
2351 REWRITE_TAC[INTER_SUBSET] THEN
2352 ASM_SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;
2355 let POLYTOPE_VORONOI_LIST_BARV = prove(`!V ul k. packing V /\ saturated V /\ barV V k ul ==> polytope (voronoi_list V ul)`,
2356 REPEAT STRIP_TAC THEN
2357 MATCH_MP_TAC POLYTOPE_VORONOI_LIST THEN
2358 ASM_REWRITE_TAC[] THEN
2361 MATCH_MP_TAC BARV_SUBSET THEN
2362 EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[];
2365 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
2366 POP_ASSUM MP_TAC THEN SIMP_TAC[BARV; ARITH_RULE `~(k + 1 = 0)`]);;
2369 (* closed (voronoi_list V ul) *)
2370 let CLOSED_VORONOI_LIST = prove(`!V ul. closed (voronoi_list V ul)`,
2371 REPEAT STRIP_TAC THEN
2372 REWRITE_TAC[VORONOI_LIST; VORONOI_SET] THEN
2373 MATCH_MP_TAC CLOSED_INTERS THEN
2374 REWRITE_TAC[IN_ELIM_THM] THEN
2375 REPEAT STRIP_TAC THEN
2376 ASM_REWRITE_TAC[CLOSED_VORONOI_CLOSED]);;
2379 (* convex (voronoi_list V ul) *)
2380 let CONVEX_VORONOI_LIST = prove(`!V ul. convex (voronoi_list V ul)`,
2381 REPEAT STRIP_TAC THEN
2382 REWRITE_TAC[VORONOI_LIST; VORONOI_SET] THEN
2383 MATCH_MP_TAC CONVEX_INTERS THEN
2384 REWRITE_TAC[IN_ELIM_THM] THEN
2385 REPEAT STRIP_TAC THEN
2386 ASM_REWRITE_TAC[CONVEX_VORONOI_CLOSED]);;
2390 (* aff_dim voronoi_list *)
2391 let AFF_DIM_VORONOI_LIST = prove(`!V ul k. barV V k ul ==> aff_dim (voronoi_list V ul) = &3 - &k`,
2392 REWRITE_TAC[BARV; VORONOI_NONDG] THEN REPEAT STRIP_TAC THEN
2393 POP_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
2394 ASM_REWRITE_TAC[ARITH_RULE `0 < k + 1`; INITIAL_SUBLIST_REFL] THEN
2395 REWRITE_TAC[GSYM INT_OF_NUM_ADD] THEN INT_ARITH_TAC);;
2398 (* voronoi_list V vl SUBSET voronoi_closed V (HD vl) *)
2399 let VORONOI_LIST_SUBSET_VORONOI_CLOSED = prove(`!V vl. 1 <= LENGTH vl ==> voronoi_list V vl SUBSET voronoi_closed V (HD vl)`,
2400 REPEAT STRIP_TAC THEN
2401 REWRITE_TAC[SUBSET; VORONOI_LIST; VORONOI_SET; IN_INTERS; IN_ELIM_THM] THEN
2402 REPEAT STRIP_TAC THEN
2403 FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V ((HD vl):real^3)`) THEN
2406 EXISTS_TAC `HD vl:real^3` THEN
2408 MATCH_MP_TAC HD_IN_SET_OF_LIST THEN
2416 (************************************************************)
2418 (*****************************************************)
2419 (* General properties of omega_list_n and omega_list *)
2420 (*****************************************************)
2422 (* omega_k(u) = omega_k (d_(k+i) u) *)
2423 let OMEGA_LIST_N_LEMMA = prove(`!V ul k i. k + i + 1 <= LENGTH ul ==> omega_list_n V ul k = omega_list_n V (truncate_simplex (k + i) ul) k`,
2424 GEN_TAC THEN GEN_TAC THEN
2425 INDUCT_TAC THEN REWRITE_TAC[OMEGA_LIST_N] THEN REPEAT STRIP_TAC THENL
2427 MATCH_MP_TAC (GSYM HD_TRUNCATE_SIMPLEX) THEN
2428 POP_ASSUM MP_TAC THEN ARITH_TAC;
2431 MP_TAC (ISPECL [`ul:(real^3)list`; `SUC k`; `SUC k + i`] TRUNCATE_TRUNCATE_SIMPLEX) THEN
2432 ASM_REWRITE_TAC[ARITH_RULE `a:num <= a + i`; ARITH_RULE `(a + b) + 1 = a + b + 1`] THEN
2433 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2435 FIRST_X_ASSUM (MP_TAC o SPEC `i + 1`) THEN
2436 ASM_REWRITE_TAC[ARITH_RULE `k + (i + 1) + 1 = SUC k + i + 1`] THEN
2437 SIMP_TAC[ARITH_RULE `k + i + 1 = SUC k + i`]);;
2440 (* omega(d_k u) = omega_k (u) *)
2441 let OMEGA_LIST_LEMMA = prove(`!V ul k. k + 1 <= LENGTH ul ==> omega_list V (truncate_simplex k ul) = omega_list_n V ul k`,
2442 REPEAT STRIP_TAC THEN REWRITE_TAC[OMEGA_LIST] THEN
2443 MP_TAC (ISPECL [`k:num`; `truncate_simplex k (ul:(real^3)list)`; `ul:(real^3)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
2444 ASM_SIMP_TAC[ARITH_RULE `(k + 1) - 1 = k`] THEN
2446 MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `k:num`; `0`] OMEGA_LIST_N_LEMMA) THEN
2447 ASM_SIMP_TAC[ADD_CLAUSES]);;
2451 let BARV_IMP_VORONOI_LIST_NOT_EMPTY = prove(`!V ul k. barV V k ul ==> ~(voronoi_list V ul = {})`,
2452 REPEAT STRIP_TAC THEN
2453 UNDISCH_TAC `barV V k ul` THEN DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
2454 REWRITE_TAC[BARV; VORONOI_NONDG] THEN
2455 REPEAT STRIP_TAC THEN
2456 FIRST_X_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
2457 ASM_REWRITE_TAC[INITIAL_SUBLIST_REFL; ARITH_RULE `0 < k + 1`; DE_MORGAN_THM] THEN
2458 DISJ2_TAC THEN DISJ2_TAC THEN
2459 REWRITE_TAC[AFF_DIM_EMPTY; GSYM INT_OF_NUM_ADD] THEN
2460 SUBGOAL_THEN `&k <= int_of_num 3` MP_TAC THENL
2462 REWRITE_TAC[INT_OF_NUM_LE] THEN
2463 MATCH_MP_TAC BARV_IMP_K_LE_3 THEN
2464 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `ul:(real^3)list`] THEN
2471 (* omega_i IN voronoi_list V (d_i ul) *)
2472 let OMEGA_LIST_N_IN_VORONOI_LIST = prove(`!V ul k i. barV V k ul /\ i <= k
2473 ==> omega_list_n V ul i IN voronoi_list V (truncate_simplex i ul)`,
2474 REPEAT STRIP_TAC THEN
2475 SUBGOAL_THEN `LENGTH (ul:(real^3)list) = k + 1` ASSUME_TAC THENL
2477 UNDISCH_TAC `barV V k ul` THEN
2481 DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
2483 ASM_REWRITE_TAC[OMEGA_LIST_N] THEN
2484 MP_TAC (ISPEC `ul:(real^3)list` TRUNCATE_0_EQ_HEAD) THEN
2485 ASM_REWRITE_TAC[ARITH_RULE `1 <= k + 1`] THEN
2486 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2487 REWRITE_TAC[VORONOI_LIST_SING; CENTER_IN_VORONOI_CELL];
2490 POP_ASSUM CHOOSE_TAC THEN
2491 ASM_REWRITE_TAC[OMEGA_LIST_N] THEN
2492 MP_TAC (ISPECL [`voronoi_list V (truncate_simplex i ul):real^3->bool`; `omega_list_n V ul n`] CLOSEST_POINT_EXISTS) THEN
2495 REWRITE_TAC[CLOSED_VORONOI_LIST] THEN
2496 MATCH_MP_TAC BARV_IMP_VORONOI_LIST_NOT_EMPTY THEN
2497 EXISTS_TAC `i:num` THEN
2498 MATCH_MP_TAC TRUNCATE_SIMPLEX_BARV THEN
2499 EXISTS_TAC `k:num` THEN
2506 (* omega ul IN voronoi_list V ul *)
2507 let OMEGA_LIST_IN_VORONOI_LIST = prove(`!V ul k. barV V k ul ==> omega_list V ul IN voronoi_list V ul`,
2508 REPEAT STRIP_TAC THEN
2509 REWRITE_TAC[OMEGA_LIST] THEN
2510 MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `k:num`; `k:num`] OMEGA_LIST_N_IN_VORONOI_LIST) THEN
2511 ASM_REWRITE_TAC[LE_REFL] THEN
2512 SUBGOAL_THEN `LENGTH (ul:(real^3)list) = k + 1` ASSUME_TAC THENL
2514 POP_ASSUM MP_TAC THEN SIMP_TAC[BARV];
2518 SUBGOAL_THEN `truncate_simplex k ul = ul:(real^3)list` (fun th -> REWRITE_TAC[th]) THENL
2520 MP_TAC (ISPECL [`k:num`; `ul:(real^3)list`; `ul:(real^3)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
2521 ASM_REWRITE_TAC[LE_REFL; INITIAL_SUBLIST_REFL];
2525 ASM_REWRITE_TAC[ARITH_RULE `(k + 1) - 1 = k`]);;