text_formalization/packing/pack3.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Author: Alexey Solovyev                                                    *)
   6 (* Date: 2010-03-15                                                           *)
   7 (* Proofs of: KIUMVTC, TIWWFYQ, DRUQUFE                                       *)
   8 (* ========================================================================== *)
   9
  10
  11 flyspeck_needs "general/sphere.hl";;
  12 flyspeck_needs "packing/pack_defs.hl";;
  13 flyspeck_needs "packing/pack2.hl";;
  14
  15
  16 module Packing3 = struct
  17
  18
  19 open Sphere;;
  20 open Pack_defs;;
  21
  22
  23 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
  24
  25
  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) ==>
  29       (u = v))`,
  30      REWRITE_TAC[packing;IN;REAL_ARITH `x<y <=> ~(y<= x)`]
  31        THEN MESON_TAC[]);;
  32
  33
  34 let BIS_SYM = prove(`!p (q:real^N). bis p q = bis q p`,
  35    REWRITE_TAC[bis] THEN SET_TAC[]);;
  36
  37
  38
  39
  40 (***********************************************************************************)
  41 (***********************************************************************************)
  42 (***********************************************************************************)
  43
  44
  45 (*********************************)
  46 (* Auxiliary general definitions *)
  47 (*********************************)
  48
  49 let discrete = new_definition `discrete S <=> ?e. &0 < e /\ (!x y. x IN S /\ y IN S /\ dist(x, y) < e ==> x = y)`;;
  50
  51
  52 (****************************)
  53 (* Auxiliary general lemmas *)
  54 (****************************)
  55
  56 let IMAGE_LEMMA = prove(`!s f. IMAGE f s = {f x | x IN s}`, SET_TAC[IMAGE]);;
  57
  58
  59 let CHOICE_LEMMA = MESON[] `!y (P:A->bool). ((?x. P x) /\ (!x. P x ==> (x = y))) ==> (@x. P x) = y`;;
  60
  61
  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
  64      REPEAT STRIP_TAC THEN
  65      EQ_TAC THEN REPEAT STRIP_TAC THENL [ ASM_REWRITE_TAC[]; ALL_TAC ] THEN
  66      EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]);;
  67
  68
  69 let SING_UNION_EQ_INSERT = prove(`!s x:A. {x} UNION s = x INSERT s`, SET_TAC[]);;
  70
  71
  72 let IN_TRANS = prove(`!(x:A) s t. x IN t /\ t SUBSET s ==> x IN s`, SIMP_TAC[SUBSET]);;
  73
  74
  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]);;
  77
  78
  79
  80 let LENGTH_IMP_CONS = prove(`!l:(A)list. 1 <= LENGTH l ==> ?h t. l = CONS h t`,
  81    REPEAT STRIP_TAC THEN
  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
  84      STRIP_TAC THEN
  85      MAP_EVERY EXISTS_TAC [`h:A`; `t:(A)list`] THEN
  86      ASM_REWRITE_TAC[]);;
  87
  88
  89
  90 let LENGTH_1_LEMMA = prove(`!ul:(A)list. LENGTH ul = 1 ==> ul = [HD ul]`,
  91    REPEAT STRIP_TAC THEN
  92      MP_TAC (SPEC `ul:(A)list` LENGTH_IMP_CONS) THEN
  93      ASM_REWRITE_TAC[LE_REFL] THEN
  94      STRIP_TAC 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]);;
  99
 100
 101
 102
 103 let PERMUTES_TRIVIAL = prove(`!p. p permutes 0..0 <=> p = I`,
 104    GEN_TAC THEN EQ_TAC THENL
 105      [
 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
 109          [
 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
 114              [
 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)`];
 118                ALL_TAC
 119              ] THEN
 120
 121              UNDISCH_TAC `(p:num->num) x' = 0` THEN ASM_REWRITE_TAC[];
 122            ALL_TAC
 123          ] THEN
 124          FIRST_X_ASSUM MATCH_MP_TAC THEN
 125          POP_ASSUM MP_TAC THEN ARITH_TAC;
 126        ALL_TAC
 127      ] THEN
 128      SIMP_TAC[PERMUTES_I]);;
 129
 130
 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]);;
 141
 142
 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)`,
 145    REPEAT GEN_TAC THEN
 146      MATCH_MP_TAC CONVEX_HULLS_EQ THEN
 147      CONJ_TAC THENL
 148      [
 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
 154          GEN_TAC THEN
 155          DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 156          DISJ2_TAC THEN
 157          POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
 158          REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
 159        ALL_TAC
 160      ] THEN
 161
 162      MATCH_MP_TAC SUBSET_TRANS THEN
 163      EXISTS_TAC `convex hull (A:real^N->bool) UNION convex hull (B:real^N->bool)` THEN
 164      CONJ_TAC THENL
 165      [
 166        REWRITE_TAC[SUBSET; IN_UNION] THEN
 167          GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 168          DISJ1_TAC THEN
 169          POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
 170          REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
 171        ALL_TAC
 172      ] THEN
 173
 174      REWRITE_TAC[HULL_UNION_SUBSET]);;
 175
 176
 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
 181      [
 182        ASM_SIMP_TAC[AFFINE_INDEPENDENT_IMP_FINITE];
 183        ALL_TAC
 184      ] THEN
 185
 186      EQ_TAC THEN SIMP_TAC[] THEN
 187      DISCH_TAC THEN
 188
 189      SUBGOAL_THEN `s = {x | x extreme_point_of convex hull s}:real^N->bool` ASSUME_TAC THENL
 190      [
 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];
 193        ALL_TAC
 194      ] THEN
 195      SUBGOAL_THEN `t = {x | x extreme_point_of convex hull t}:real^N->bool` ASSUME_TAC THENL
 196      [
 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];
 199        ALL_TAC
 200      ] THEN
 201      POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 202      POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 203      ASM_REWRITE_TAC[]);;
 204
 205
 206 (* Lemmas about intersections *)
 207
 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]);;
 211
 212
 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]);;
 219
 220
 221 let SUBSET_INTERS = prove(`!(s:A->bool) f. s SUBSET INTERS f <=> (!t. t IN f ==> s SUBSET t)`, SET_TAC[]);;
 222
 223
 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}`,
 225    REPEAT GEN_TAC THEN
 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
 232      ASM_REWRITE_TAC[]);;
 233
 234
 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
 242      EQ_TAC THENL
 243      [
 244        REWRITE_TAC[GSYM EXTENSION] THEN
 245          STRIP_TAC THEN
 246          ASM_SIMP_TAC[HULL_P];
 247        ALL_TAC
 248      ] THEN
 249      REWRITE_TAC[GSYM EXTENSION] THEN
 250      DISCH_TAC THEN EXISTS_TAC `x:A->bool` THEN
 251      ASM_SIMP_TAC[HULL_P]);;
 252
 253
 254
 255
 256
 257
 258
 259
 260 let INTERS_2_LEMMA = prove(`!a b f. INTERS {f x | x IN {a, b}} = f a INTER f b`, SET_TAC[INTERS]);;
 261
 262
 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
 267      [
 268        REPEAT STRIP_TAC THEN
 269          ASM SET_TAC[];
 270
 271        ALL_TAC
 272      ] THEN
 273      REPEAT STRIP_TAC THENL
 274      [
 275        SUBGOAL_THEN `?t':B. t' IN (f:B->bool)` MP_TAC THENL
 276        [
 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];
 280          ALL_TAC
 281        ] THEN
 282        STRIP_TAC THEN
 283        FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
 284        ANTS_TAC THENL
 285        [
 286          EXISTS_TAC `t':B` THEN
 287          ASM_REWRITE_TAC[IN_INTER];
 288          ALL_TAC
 289        ] THEN
 290        SIMP_TAC[IN_INTER];
 291
 292        ALL_TAC
 293      ] THEN
 294      ASM_REWRITE_TAC[] THEN
 295      FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
 296      ANTS_TAC THENL
 297      [
 298        EXISTS_TAC `t':B` THEN
 299        ASM_REWRITE_TAC[IN_INTER];
 300        ALL_TAC
 301      ] THEN
 302      SIMP_TAC[IN_INTER]);;
 303
 304
 305
 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
 308      MESON_TAC[]);;
 309
 310
 311
 312 let INTERS_INTER_INTERS = prove(`!f g. INTERS f INTER INTERS g = INTERS (f UNION g)`, SET_TAC[]);;
 313
 314
 315
 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)}`,
 317   SET_TAC[]);;
 318
 319
 320
 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]);;
 323
 324
 325
 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
 331                            [
 332                              REWRITE_TAC[SIMPLE_IMAGE] THEN
 333                                ASM_SIMP_TAC[FINITE_IMAGE];
 334                              ALL_TAC
 335                            ] THEN
 336                            DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 337                            REWRITE_TAC[IN_ELIM_THM] THEN
 338                            REPEAT STRIP_TAC THEN
 339                            ASM_MESON_TAC[]);;
 340
 341
 342
 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]);;
 346
 347
 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]);;
 350
 351
 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
 355           [
 356             MATCH_MP_TAC REAL_FINITE_MIN_EXISTS THEN
 357               ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];
 358
 359             ALL_TAC
 360           ] THEN
 361
 362           REWRITE_TAC[IN_IMAGE] THEN
 363           MESON_TAC[]);;
 364
 365
 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
 369           [
 370             MATCH_MP_TAC REAL_FINITE_MAX_EXISTS THEN
 371               ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];
 372
 373             ALL_TAC
 374           ] THEN
 375
 376           REWRITE_TAC[IN_IMAGE] THEN
 377           MESON_TAC[]);;
 378
 379
 380
 381 (***************************)
 382 (* Properties of bisectors *)
 383 (***************************)
 384
 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
 388                                                         REAL_ARITH_TAC);;
 389
 390
 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
 394                                                                 REAL_ARITH_TAC);;
 395
 396
 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]);;
 399
 400
 401
 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]);;
 404
 405
 406 let CONVEX_BIS = prove(`!u v:real^N. convex(bis u v)`,
 407                                                 REWRITE_TAC[BIS_EQ_HYPERPLANE; CONVEX_HYPERPLANE]);;
 408
 409
 410 let POLYHEDRON_BIS = prove(`!u v:real^N. polyhedron (bis u v)`,
 411      ASM_REWRITE_TAC[BIS_EQ_HYPERPLANE; POLYHEDRON_HYPERPLANE]);;
 412
 413
 414
 415 let AFFINE_BIS = prove(`!a b:real^N. affine (bis a b)`,
 416    REWRITE_TAC[BIS_EQ_HYPERPLANE; AFFINE_HYPERPLANE]);;
 417
 418
 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}`,
 420    REPEAT GEN_TAC THEN
 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]);;
 424
 425
 426
 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`,
 429         REPEAT GEN_TAC THEN
 430           DISJ_CASES_TAC (TAUT `dist(v:real^N, w) = &0 \/ ~(dist(v, w) = &0)`) THENL
 431           [
 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];
 435
 436             ALL_TAC
 437           ] THEN
 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
 441           CONJ_TAC THENL
 442           [
 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];
 446
 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
 452               CONV_TAC REAL_FIELD
 453           ]);;
 454
 455
 456
 457 (********************************************************)
 458 (* Proof that V(v,r) is finite begins here              *)
 459 (********************************************************)
 460
 461 (* General properties of discrete sets *)
 462
 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
 468                                                                 ASM_MESON_TAC[]);;
 469
 470
 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
 475                                                         ASM_MESON_TAC[]);;
 476
 477
 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]);;
 481
 482
 483
 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
 490                                [
 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[]
 499                                ]);;
 500
 501
 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
 507
 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
 517                           STRIP_TAC THEN
 518                           SUBGOAL_THEN `FINITE (S INTER UNIONS (g:(real^N->bool)->bool))` ASSUME_TAC THENL
 519                           [
 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];
 526                             ALL_TAC
 527                           ] THEN
 528                           ASM_MESON_TAC[SET_RULE `S SUBSET A ==> S INTER A = S`]);;
 529
 530
 531
 532
 533 (* Proof of the main lemma begins here *)
 534
 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`]);;
 539
 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
 543                     [
 544                       ALL_TAC;
 545                       ASM_SIMP_TAC[BOUNDED_INTER; BOUNDED_BALL]
 546                     ] THEN
 547                     MATCH_MP_TAC DISCRETE_SUBSET THEN
 548                     EXISTS_TAC `V:real^3->bool` THEN
 549                     ASM_SIMP_TAC[PACKING_IMP_DISCRETE] THEN
 550                     SET_TAC[]);;
 551
 552
 553
 554
 555
 556 (****************************************************)
 557 (* TIWWFYQ                                          *)
 558 (* If a packing is saturated, then every point of   *)
 559 (* the space is inside some Voronoi (closed) cell   *)
 560 (****************************************************)
 561
 562
 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
 568       [
 569           MATCH_MP_TAC REAL_FINITE_ARGMIN THEN
 570             EXPAND_TAC "S" 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
 574             ASM_MESON_TAC[];
 575
 576         ALL_TAC
 577       ] THEN
 578       STRIP_TAC 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
 587       [
 588         ASM_MESON_TAC[DIST_SYM];
 589         SUBGOAL_THEN `&2 <= dist(p:real^3, w)` MP_TAC THENL
 590           [
 591             POP_ASSUM MP_TAC THEN REWRITE_TAC[ball; IN_ELIM_THM; REAL_NOT_LT];
 592             ALL_TAC
 593           ] THEN
 594
 595           SUBGOAL_THEN `dist(p:real^3, v) < &2` MP_TAC THENL
 596           [
 597             REMOVE_THEN "A" MP_TAC THEN SIMP_TAC[ball; IN_ELIM_THM];
 598             ALL_TAC
 599           ] THEN
 600
 601           REAL_ARITH_TAC
 602       ]);;
 603
 604
 605
 606
 607
 608 (*******************************)
 609 (* Porperties of Voronoi cells *)
 610 (*******************************)
 611
 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`,
 614    REPEAT GEN_TAC THEN
 615      SUBGOAL_THEN `v IN voronoi_open V (v:real^3)` ASSUME_TAC THENL
 616      [
 617        REWRITE_TAC[voronoi_open; IN_ELIM_THM; DIST_REFL] THEN
 618          SIMP_TAC[DIST_POS_LT];
 619        ALL_TAC
 620      ] THEN
 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]);;
 625
 626
 627
 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
 633      [
 634        POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN DISCH_TAC THEN
 635          EXISTS_TAC `&1` 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
 642          [
 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];
 649            ALL_TAC
 650          ] THEN
 651
 652          UNDISCH_TAC `dist (v,x:real^3) < &1` THEN
 653          REWRITE_TAC[DIST_SYM] THEN
 654          REAL_ARITH_TAC;
 655        ALL_TAC
 656      ] THEN
 657
 658      SUBGOAL_THEN `?s. &0 < s /\ ball (v:real^3, s) INTER V = {}` STRIP_ASSUME_TAC THENL
 659      [
 660        SUBGOAL_THEN `~(ball (v:real^3, &1) INTER V = {}) ==> ?x. ball (v:real^3, &1) INTER V = {x}` MP_TAC THENL
 661          [
 662            REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; EXTENSION; IN_SING; ball; IN_ELIM_THM] THEN
 663              STRIP_TAC THEN
 664              EXISTS_TAC `x:real^3` THEN
 665              GEN_TAC THEN EQ_TAC THENL
 666              [
 667                STRIP_TAC THEN
 668                  SUBGOAL_THEN `dist (x:real^3, x') < &2` MP_TAC THENL
 669                  [
 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];
 675                    ALL_TAC
 676                  ] THEN
 677
 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];
 682                ALL_TAC
 683              ] THEN
 684
 685              ASM_SIMP_TAC[];
 686            ALL_TAC
 687          ] THEN
 688
 689          ASM_CASES_TAC `ball (v:real^3, &1) INTER V = {}` THEN ASM_REWRITE_TAC[] THENL
 690          [
 691            EXISTS_TAC `&1` THEN
 692              ASM_REWRITE_TAC[REAL_LT_01];
 693            ALL_TAC
 694          ] THEN
 695
 696          STRIP_TAC THEN
 697          EXISTS_TAC `dist (v:real^3, x)` THEN
 698          CONJ_TAC THENL
 699          [
 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
 705              ASM_REWRITE_TAC[];
 706            ALL_TAC
 707          ] THEN
 708
 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
 716          [
 717            MATCH_MP_TAC REAL_LT_TRANS THEN
 718              EXISTS_TAC `dist (v, x:real^3)` THEN
 719              ASM_REWRITE_TAC[];
 720            ALL_TAC
 721          ] 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];
 725        ALL_TAC
 726      ] THEN
 727
 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
 735      [
 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];
 742        ALL_TAC
 743      ] THEN
 744
 745      UNDISCH_TAC `dist (v, x:real^3) < s / &2` THEN
 746      UNDISCH_TAC `&0 < s` THEN
 747      REWRITE_TAC[DIST_SYM] THEN
 748      REAL_ARITH_TAC);;
 749
 750
 751
 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
 760      ASM_REWRITE_TAC[]);;
 761
 762
 763
 764
 765
 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
 778                              REAL_ARITH_TAC);;
 779
 780
 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]);;
 786
 787
 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}`,
 790          REPEAT GEN_TAC THEN
 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
 794            [
 795              ASM_MESON_TAC[];
 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[]
 799            ]);;
 800
 801
 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)}`,
 804          REPEAT GEN_TAC THEN
 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
 808            [
 809              ASM_MESON_TAC[];
 810              DISJ_CASES_TAC (TAUT `w:real^N = v \/ ~(w = v)`) THENL
 811                [
 812                  ASM_REWRITE_TAC[REAL_LE_REFL];
 813                  ALL_TAC
 814                ] THEN
 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[]
 818            ]);;
 819
 820
 821
 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
 828      [
 829        SET_TAC[];
 830        ALL_TAC
 831      ] THEN
 832
 833      REWRITE_TAC[IN_ELIM_THM] THEN
 834      DISCH_THEN (LABEL_TAC "B") THEN REPEAT STRIP_TAC THEN
 835
 836      DISJ_CASES_TAC (TAUT `(w:real^3) IN ball(v:real^3, &4) \/ ~(w IN ball(v, &4))`) THENL
 837      [
 838        REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN SET_TAC[];
 839        ALL_TAC
 840      ] THEN
 841
 842      SUBGOAL_THEN `x:real^3 IN ball(v, &2)` (LABEL_TAC "C") THENL
 843      [
 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
 853          ANTS_TAC THENL
 854          [
 855            EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[ball; IN_ELIM_THM] THEN
 856              CONJ_TAC THENL
 857              [
 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;
 860                ALL_TAC
 861              ] THEN
 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
 865              REAL_ARITH_TAC;
 866
 867            ALL_TAC
 868          ] THEN
 869
 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;
 874
 875        ALL_TAC
 876      ] THEN
 877
 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);;
 882
 883
 884
 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 }`,
 889   REPEAT GEN_TAC THEN
 890     DISCH_TAC THEN
 891     FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP VORONOI_INTER_BIS_LE th)) THEN
 892     DISCH_TAC THEN
 893     EXISTS_TAC `(V:real^3->bool) INTER ball(v,&4) DELETE v` THEN
 894     REPEAT STRIP_TAC THENL
 895     [
 896       SET_TAC[];
 897       ASM SET_TAC[];
 898       MATCH_MP_TAC FINITE_SUBSET THEN
 899         EXISTS_TAC `V INTER ball(v:real^3,&4)` THEN
 900         CONJ_TAC THENL
 901         [
 902           ASM_MESON_TAC[KIUMVTC];
 903           ALL_TAC
 904         ] THEN
 905         SET_TAC[];
 906
 907     ASM_REWRITE_TAC[] THEN
 908                 SET_TAC[]
 909     ]);;
 910
 911
 912
 913 (* A closed Voronoi cell is a polyhedron *)
 914
 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)`,
 918         REPEAT GEN_TAC THEN
 919           DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE th)) THEN
 920           STRIP_TAC THEN
 921           REWRITE_TAC[polyhedron] THEN
 922           EXISTS_TAC `{bis_le v (u:real^3) | u IN W}` THEN
 923           ASM_REWRITE_TAC[] THEN
 924           CONJ_TAC THENL
 925           [
 926             REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
 927               MATCH_MP_TAC FINITE_IMAGE THEN
 928               ASM_REWRITE_TAC[];
 929             ALL_TAC
 930           ] 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
 936           ASM SET_TAC[]);;
 937
 938
 939 (* A closed Voronoi cell is convex *)
 940 let CONVEX_VORONOI_CLOSED = prove(`!S v:real^N. convex(voronoi_closed S v)`,
 941                                   REPEAT GEN_TAC THEN
 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]);;
 946
 947
 948 (* A closed Voronoi cell is closed *)
 949 let CLOSED_VORONOI_CLOSED = prove(`!S v:real^N. closed(voronoi_closed S v)`,
 950                                   REPEAT GEN_TAC THEN
 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]);;
 955
 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]);;
 961
 962
 963 (****************************************************************)
 964 (* DRUQUFE:                                                                                                             *)
 965 (* For a saturated packing, each closed Voronoi closed cell is  *)
 966 (* compact, convex, and measurable                                                              *)
 967 (****************************************************************)
 968
 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
 973                        [
 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]
 978                        ]);;
 979
 980
 981
 982
 983
 984
 985 (*************************************************************)
 986
 987
 988 (*******************************************)
 989 (* Some results for initial sublists       *)
 990 (*******************************************)
 991
 992 let INITIAL_SUBLIST_APPEND = prove(`!ul vl. initial_sublist ul (APPEND ul vl)`,
 993                                    REWRITE_TAC[INITIAL_SUBLIST] THEN
 994                                      MESON_TAC[]);;
 995
 996
 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`,
 998    REPEAT GEN_TAC THEN
 999      REWRITE_TAC[INITIAL_SUBLIST] THEN
1000      STRIP_TAC THEN
1001      POP_ASSUM MP_TAC THEN
1002      ASM_REWRITE_TAC[APPEND] THEN
1003      MESON_TAC[injectivity "list"]);;
1004
1005
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]);;
1008
1009
1010
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
1016      DISCH_TAC THEN
1017      ASM_REWRITE_TAC[TL] THEN
1018      MESON_TAC[]);;
1019
1020
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
1024      [
1025        ASM_MESON_TAC[LENGTH_EQ_NIL];
1026        ALL_TAC
1027      ] THEN
1028
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
1034      CONJ_TAC THENL
1035      [
1036        ASM_MESON_TAC[INITIAL_SUBLIST_HEAD_EQ_2];
1037        ALL_TAC
1038      ] THEN
1039
1040      ASM_MESON_TAC[INITIAL_SUBLIST_TAIL]);;
1041
1042
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]);;
1048
1049
1050 (* initial_sublist is reflexive *)
1051 let INITIAL_SUBLIST_REFL = prove(`!ul. initial_sublist ul ul`, MESON_TAC[INITIAL_SUBLIST; APPEND_NIL]);;
1052
1053
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[]);;
1057
1058
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
1062      [
1063        EXISTS_TAC `[]:(A)list` THEN
1064          REWRITE_TAC[INITIAL_SUBLIST_NIL] THEN
1065          POP_ASSUM MP_TAC THEN
1066          SIMP_TAC[LE; LENGTH];
1067
1068        ALL_TAC
1069      ] THEN
1070
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
1074      [
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`];
1077        ALL_TAC
1078      ] THEN
1079
1080      STRIP_TAC THEN
1081      DISJ_CASES_TAC (ARITH_RULE `k = 0 \/ 0 < k`) THENL
1082      [
1083        EXISTS_TAC `[]:(A)list` THEN
1084          ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL; LENGTH];
1085        ALL_TAC
1086      ] THEN
1087
1088      EXISTS_TAC `CONS (h:A) yl` THEN
1089      ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND; LENGTH] THEN
1090      CONJ_TAC THENL
1091      [
1092        REPLICATE_TAC 2 (POP_ASSUM (fun th -> ALL_TAC)) THEN
1093          POP_ASSUM MP_TAC THEN
1094          REWRITE_TAC[INITIAL_SUBLIST] THEN
1095          MESON_TAC[];
1096
1097        POP_ASSUM MP_TAC THEN
1098          ARITH_TAC
1099      ]);;
1100
1101
1102
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]);;
1105
1106
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
1111      ARITH_TAC);;
1112
1113
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
1117     [
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
1120         [
1121           DISCH_TAC THEN
1122             DISJ1_TAC THEN
1123             MP_TAC (ISPECL [`ul:(A)list`; `k:num`] INITIAL_SUBLIST_EXISTS) THEN
1124             ASM_REWRITE_TAC[] THEN
1125             STRIP_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];
1129
1130           ALL_TAC
1131         ] THEN
1132
1133         DISCH_TAC THEN
1134         DISJ2_TAC THEN
1135         SUBGOAL_THEN `?yl:(A)list. initial_sublist yl vl /\ LENGTH yl = k - LENGTH (ul:(A)list)` MP_TAC THENL
1136         [
1137           MP_TAC (ISPECL [`vl:(A)list`; `k - LENGTH (ul:(A)list)`] INITIAL_SUBLIST_EXISTS) THEN
1138             ANTS_TAC THENL
1139             [
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
1143                 ARITH_TAC;
1144
1145               MESON_TAC[]
1146             ];
1147
1148           ALL_TAC
1149         ] THEN
1150
1151         STRIP_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
1155         [
1156           CONJ_TAC THENL
1157             [
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
1165                 ARITH_TAC
1166             ];
1167
1168           ALL_TAC
1169         ] THEN
1170
1171         ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];
1172
1173       ALL_TAC
1174     ] THEN
1175
1176     REPEAT STRIP_TAC THENL
1177     [
1178       ASM_MESON_TAC[INITIAL_SUBLIST_TRANS; INITIAL_SUBLIST_APPEND];
1179       ASM_MESON_TAC[INITIAL_SUBLIST; APPEND_ASSOC]
1180     ]);;
1181
1182
1183
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
1187     [
1188       DISCH_TAC THEN
1189         FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_LENGTH_LE th)) THEN
1190         REWRITE_TAC[LENGTH; SYM ONE] THEN
1191         DISCH_TAC THEN
1192         DISJ_CASES_TAC (ARITH_RULE `LENGTH (xl:(A)list) = 0 \/ 1 <= LENGTH xl`) THENL
1193         [
1194           ASM_MESON_TAC[LENGTH_EQ_NIL];
1195           ALL_TAC
1196         ] THEN
1197         DISJ2_TAC THEN
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
1201         [
1202           REWRITE_TAC[INITIAL_SUBLIST; LENGTH; SYM ONE; APPEND] THEN MESON_TAC[];
1203           ALL_TAC
1204         ] THEN
1205         ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];
1206
1207       ALL_TAC
1208     ] THEN
1209
1210     STRIP_TAC THENL
1211     [
1212       ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL];
1213       ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]
1214     ]);;
1215
1216
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]`,
1219    REPEAT GEN_TAC THEN
1220      REWRITE_TAC[INITIAL_SUBLIST_APPEND_2; INITIAL_SUBLIST_SING] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
1221      [
1222        ASM_REWRITE_TAC[];
1223        DISJ1_TAC THEN POP_ASSUM MP_TAC THEN
1224          ASM_REWRITE_TAC[APPEND_NIL] THEN
1225          SIMP_TAC[INITIAL_SUBLIST_REFL];
1226        ASM_REWRITE_TAC[];
1227        ASM_REWRITE_TAC[];
1228        DISJ2_TAC THEN
1229          EXISTS_TAC `[v:A]` THEN
1230          ASM_REWRITE_TAC[]
1231      ]);;
1232
1233
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
1239      STRIP_TAC THEN
1240      ASM_REWRITE_TAC[HD; INITIAL_SUBLIST; APPEND] THEN
1241      EXISTS_TAC `t:(A)list` THEN
1242      REWRITE_TAC[]);;
1243
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
1251      DISCH_TAC THEN
1252      EXISTS_TAC `[LAST ul:A]` THEN
1253      ASM_REWRITE_TAC[]);;
1254
1255
1256 (**********************************************************)
1257
1258 (**********************************)
1259 (* Additional properties of lists *)
1260 (**********************************)
1261
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
1269      ARITH_TAC);;
1270
1271
1272
1273
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
1280      ARITH_TAC);;
1281
1282
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
1289      [
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
1294          ASM_REWRITE_TAC[];
1295        ALL_TAC
1296      ] 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]);;
1301
1302
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]);;
1307
1308
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
1312      ARITH_TAC);;
1313
1314
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
1317      [
1318        REWRITE_TAC[LENGTH] THEN ARITH_TAC;
1319        ALL_TAC
1320      ] THEN
1321      REWRITE_TAC[LENGTH; REVERSE; EL_APPEND; LENGTH_REVERSE] THEN
1322      REPEAT STRIP_TAC THEN
1323      COND_CASES_TAC THENL
1324      [
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
1328          [
1329            POP_ASSUM MP_TAC THEN
1330              ARITH_TAC;
1331            ALL_TAC
1332          ] THEN
1333
1334          REWRITE_TAC[EL; TL];
1335        ALL_TAC
1336      ] THEN
1337
1338      SUBGOAL_THEN `LENGTH (t:(A)list) = i` (fun th -> REWRITE_TAC[th]) THENL
1339      [
1340        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1341          ARITH_TAC;
1342        ALL_TAC
1343      ] THEN
1344
1345      REWRITE_TAC[ARITH_RULE `i - i = 0`; ARITH_RULE `SUC i - 1 - i = 0`] THEN
1346      REWRITE_TAC[EL; HD]);;
1347
1348
1349
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
1352      [
1353        REWRITE_TAC[LENGTH];
1354        ALL_TAC
1355      ] THEN
1356      ASM_REWRITE_TAC[GSYM TABLE; LENGTH_APPEND; LENGTH] THEN
1357      ARITH_TAC);;
1358
1359
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
1366      [
1367        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1368        ALL_TAC
1369      ] THEN
1370      SUBGOAL_THEN `i = n:num` (fun th -> REWRITE_TAC[th]) THENL
1371      [
1372        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1373          ARITH_TAC;
1374        ALL_TAC
1375      ] THEN
1376      REWRITE_TAC[ARITH_RULE `n - n = 0`; EL; HD]);;
1377
1378
1379
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]);;
1382
1383
1384
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
1391      [
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
1398          ARITH_TAC;
1399        ALL_TAC
1400      ] 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
1405      SIMP_TAC[]);;
1406
1407
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
1413      EQ_TAC THENL
1414      [
1415        STRIP_TAC THEN
1416          POP_ASSUM MP_TAC THEN
1417          ASM_SIMP_TAC[left_action_list; EL_TABLE] THEN
1418          DISCH_TAC THEN
1419          EXISTS_TAC `inverse (p:num->num) i` THEN
1420          REWRITE_TAC[] 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;
1428        ALL_TAC
1429      ] THEN
1430      STRIP_TAC THEN
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
1437      ARITH_TAC);;
1438
1439
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]);;
1445
1446
1447
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
1453      [
1454        MP_TAC (ISPEC `t:(A)list` CARD_SET_OF_LIST_LE) THEN
1455          ARITH_TAC;
1456        ALL_TAC
1457      ] THEN
1458
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
1462
1463      MP_TAC (SPEC `i:num` num_CASES) THEN STRIP_TAC THENL
1464      [
1465        ASM_REWRITE_TAC[EL; HD] THEN
1466          MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
1467          [
1468            UNDISCH_TAC `~(i = j:num)` THEN ASM_REWRITE_TAC[];
1469            ALL_TAC
1470          ] THEN
1471
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
1477          ARITH_TAC;
1478        ALL_TAC
1479      ] THEN
1480
1481      ASM_REWRITE_TAC[EL; TL] THEN
1482      MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
1483      [
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
1489          ARITH_TAC;
1490        ALL_TAC
1491      ] THEN
1492
1493      ASM_REWRITE_TAC[EL; TL] THEN
1494      FIRST_X_ASSUM MATCH_MP_TAC THEN
1495      REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN
1496      ARITH_TAC);;
1497
1498
1499 let LENGTH_DROP = prove(`!i ul:(A)list. i < LENGTH ul ==> LENGTH (DROP ul i) = LENGTH ul - 1`,
1500    INDUCT_TAC THENL
1501      [
1502        GEN_TAC THEN
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;
1506        ALL_TAC
1507      ] THEN
1508
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
1513      [
1514        MATCH_MP_TAC LENGTH_TL THEN
1515          ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1516        ALL_TAC
1517      ] THEN
1518
1519      ANTS_TAC THENL
1520      [
1521        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1522        ALL_TAC
1523      ] THEN
1524
1525      ASM_REWRITE_TAC[] THEN
1526      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1527      REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1528      ARITH_TAC);;
1529
1530
1531
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
1535      [
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];
1538        ALL_TAC
1539      ] THEN
1540
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
1544      [
1545        MATCH_MP_TAC LENGTH_TL THEN
1546          REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1547        ALL_TAC
1548      ] THEN
1549
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
1553      ARITH_TAC);;
1554
1555
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
1563      REMOVE_ASSUM 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
1568      ANTS_TAC THENL
1569      [
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];
1573        ALL_TAC
1574      ] THEN
1575      DISCH_TAC THEN
1576      FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
1577      ASM_SIMP_TAC[ARITH_RULE `0 < SUC a`; EL; HD]);;
1578
1579
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]);;
1587
1588
1589
1590
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
1600      [
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
1606          ASM_SIMP_TAC[];
1607        ALL_TAC
1608      ] THEN
1609
1610      EXISTS_TAC `i - 1` THEN
1611      POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LT; LE_LT] THEN
1612      STRIP_TAC THENL
1613      [
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
1620          ASM_SIMP_TAC[];
1621        ALL_TAC
1622      ] THEN
1623
1624      UNDISCH_TAC `x:A = EL i ul` THEN
1625      POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
1626
1627
1628
1629
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
1644
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
1647
1648      COND_CASES_TAC THENL
1649      [
1650        DISCH_TAC THEN
1651          CONJ_TAC THENL
1652          [
1653            EXISTS_TAC `i:num` THEN
1654              ASM_REWRITE_TAC[];
1655            ALL_TAC
1656          ] 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)`];
1660        ALL_TAC
1661      ] THEN
1662
1663      DISCH_TAC THEN
1664      CONJ_TAC THENL
1665      [
1666        EXISTS_TAC `i + 1` THEN
1667          ASM_SIMP_TAC[ARITH_RULE `i < k - 1 ==> i + 1 < k`];
1668        ALL_TAC
1669      ] THEN
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);;
1674
1675
1676
1677
1678
1679 (**********************************************************)
1680
1681 (*****************************************)
1682 (* Properties of barV                    *)
1683 (*****************************************)
1684
1685 (* barV(k) SUBSET V *)
1686 let BARV_SUBSET = prove(`!V k ul. barV V k ul ==> set_of_list ul SUBSET V`,
1687                         REPEAT GEN_TAC THEN
1688                           REWRITE_TAC[BARV; VORONOI_NONDG; INITIAL_SUBLIST] THEN
1689                           STRIP_TAC THEN
1690                           POP_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
1691                           ANTS_TAC THENL
1692                           [
1693                             ASM_REWRITE_TAC[ARITH_RULE `0 < k + 1`] THEN
1694                               EXISTS_TAC `[]:(real^3)list` THEN
1695                               REWRITE_TAC[APPEND_NIL];
1696                             SIMP_TAC[]
1697                           ]);;
1698
1699
1700
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`,
1703                       REPEAT GEN_TAC THEN
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]);;
1708
1709
1710
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
1715      [
1716        ASM_SIMP_TAC[ARITH_RULE `0 < a ==> a - 1 + 1 = a`];
1717        ALL_TAC
1718      ] THEN
1719
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
1723      ASM_SIMP_TAC[]);;
1724
1725
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
1731      GEN_TAC 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
1736      INT_ARITH_TAC);;
1737
1738
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
1745      ARITH_TAC);;
1746
1747
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
1754      ARITH_TAC);;
1755
1756
1757
1758
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
1762     [
1763       REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
1764         STRIP_TAC THEN
1765         POP_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_EXISTS th)) THEN
1766         ASM_MESON_TAC[];
1767       STRIP_TAC THEN
1768         MP_TAC (ISPECL [`xl:(A)list`; `zl:(A)list`] INITIAL_SUBLIST_LENGTH_LE) THEN
1769         ASM_SIMP_TAC[] THEN
1770         DISCH_TAC THEN
1771         REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
1772         ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE]
1773     ]);;
1774
1775
1776
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
1782      [
1783        REWRITE_TAC[GSYM TRUNCATE_SIMPLEX_INITIAL_SUBLIST] THEN
1784          ASM_SIMP_TAC[ARITH_RULE `r <= k ==> r + 1 <= k + 1`];
1785        ALL_TAC
1786      ] THEN
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`]);;
1789
1790
1791
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]);;
1796
1797
1798
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]);;
1805
1806
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
1810      ASM_SIMP_TAC[]);;
1811
1812
1813
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]);;
1820
1821
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
1826      STRIP_TAC THEN
1827      MATCH_MP_TAC HD_INITIAL_SUBLIST THEN
1828      ASM_REWRITE_TAC[ARITH_RULE `1 <= j + 1`]);;
1829
1830
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
1836      [
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
1839          ASM_SIMP_TAC[] THEN
1840          POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1841          ARITH_TAC;
1842        ALL_TAC
1843      ] 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[]);;
1854
1855
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
1859      [
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
1863          [
1864            UNDISCH_TAC `1 <= LENGTH (yl:(A)list)` THEN ARITH_TAC;
1865            ALL_TAC
1866          ] THEN
1867          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1868          SIMP_TAC[];
1869        ALL_TAC
1870      ] THEN
1871      ASM_SIMP_TAC[INITIAL_SUBLIST_LENGTH_LE]);;
1872
1873
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);;
1881
1882
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
1888      [
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;
1892        ALL_TAC
1893      ] THEN
1894      SUBGOAL_THEN `LENGTH (xl:(A)list) = k + 2` ASSUME_TAC THENL
1895      [
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`];
1900        ALL_TAC
1901      ] THEN
1902      SUBGOAL_THEN `k = LENGTH (xl:(A)list) - 2` (fun th -> REWRITE_TAC[th]) THENL
1903      [
1904        POP_ASSUM MP_TAC THEN ARITH_TAC;
1905        ALL_TAC
1906      ] THEN
1907
1908      MATCH_MP_TAC LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST THEN
1909      POP_ASSUM MP_TAC THEN ARITH_TAC);;
1910
1911
1912
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
1917      [
1918        MP_TAC (SPECL [`k:num`; `vl:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
1919          ASM_REWRITE_TAC[INITIAL_SUBLIST] THEN
1920          STRIP_TAC THEN
1921          EXISTS_TAC `yl:(A)list` THEN ASM_REWRITE_TAC[];
1922        ALL_TAC
1923      ] THEN
1924      ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `j < k + 1 <=> j <= k`]);;
1925
1926
1927
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
1934      AP_TERM_TAC THEN
1935
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
1938      DISCH_TAC THEN
1939
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]);;
1945
1946
1947
1948 (****************************************************)
1949
1950 (***************************************************************************)
1951 (* Properties of voronoi_set (Omega(V, W)) and voronoi_list (Omega(V, vl)) *)
1952 (***************************************************************************)
1953
1954
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
1958                                MESON_TAC[]);;
1959
1960
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]);;
1963
1964
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]);;
1968
1969
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`]);;
1976
1977
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]);;
1984
1985
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
1990      [
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
1995          SET_TAC[];
1996        ALL_TAC
1997      ] THEN
1998
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
2001      [
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];
2007
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
2010          [
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];
2016            ALL_TAC
2017          ] THEN
2018
2019          SUBGOAL_THEN `y:real^3 IN voronoi_closed V u` ASSUME_TAC THENL
2020          [
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];
2025            ALL_TAC
2026          ] THEN
2027
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`];
2033
2034
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
2041          [
2042            ASM_MESON_TAC[];
2043            ALL_TAC
2044          ] THEN
2045
2046          FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
2047          ANTS_TAC THENL
2048          [
2049            EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[];
2050            ALL_TAC
2051          ] THEN
2052
2053          ASM_MESON_TAC[]
2054      ]);;
2055
2056
2057
2058
2059 (* Used below *)
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]);;
2065
2066
2067
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)`,
2069  REPEAT GEN_TAC THEN
2070    STRIP_TAC THEN
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
2075    SET_TAC[]);;
2076
2077
2078
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})`,
2081  REPEAT GEN_TAC THEN
2082    DISCH_TAC THEN
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
2087    [
2088      ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN SET_TAC[];
2089      ALL_TAC
2090    ] THEN
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]);;
2094
2095
2096
2097
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
2104     DISCH_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
2109     DISJ1_TAC THEN
2110     ASM_SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;
2111
2112
2113
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
2124      [
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
2129          [
2130            ASM_MESON_TAC[SUBSET; IN_SET_OF_LIST];
2131            ASM_MESON_TAC[]
2132          ];
2133
2134        ALL_TAC
2135      ] THEN
2136      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2137      REWRITE_TAC[IN_SET_OF_LIST; MEM_APPEND; MEM] THEN
2138      SET_TAC[]);;
2139
2140
2141
2142 (* Canonical representations of Omega(V, vl) as a polyhedron *)
2143
2144
2145 let SUPSET_INTER = prove(`!s t u. s SUBSET t /\ s = u ==> s = t INTER u`, SET_TAC[]);;
2146
2147
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]);;
2151
2152
2153
2154 (* "Almost canonical" polyhedron representation for Omega(V, ul) *)
2155
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)))`,
2159   REPEAT GEN_TAC THEN
2160     DISCH_TAC THEN
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
2171     [
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];
2175
2176       REWRITE_TAC[INTERS_INTER_INTERS];
2177
2178       ASM SET_TAC[]
2179     ]);;
2180
2181
2182
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)))`,
2186   REPEAT GEN_TAC THEN
2187     DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL_0 th)) THEN
2188     STRIP_TAC 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
2200     ASM SET_TAC[]);;
2201
2202
2203
2204
2205
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]);;
2208
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'))`,
2212  REPEAT GEN_TAC THEN
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
2230    SET_TAC[]);;
2231
2232
2233
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'))`,
2236  REPEAT GEN_TAC THEN
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
2254    SET_TAC[]);;
2255
2256
2257
2258
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')`,
2264   REPEAT GEN_TAC THEN
2265     DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL th)) THEN
2266     STRIP_TAC THEN
2267
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
2272
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
2274
2275     USE_THEN "A" (fun th -> REWRITE_TAC[th]) THEN
2276     ANTS_TAC THENL
2277     [
2278       ASM_MESON_TAC[];
2279       ALL_TAC
2280     ] THEN
2281
2282     STRIP_TAC THEN
2283     EXISTS_TAC `g:(real^3->bool)->bool` THEN
2284     ASM_REWRITE_TAC[] THEN
2285     REPEAT STRIP_TAC THENL
2286     [
2287       ASM_MESON_TAC[FINITE_SUBSET];
2288       ASM_MESON_TAC[];
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[]
2293     ]);;
2294
2295
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
2301      [
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
2304          [
2305            REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM];
2306            ALL_TAC
2307          ] THEN
2308          REWRITE_TAC[INTERS_0; POLYHEDRON_UNIV];
2309        ALL_TAC
2310      ] THEN
2311
2312      POP_ASSUM STRIP_ASSUME_TAC THEN
2313      ASM_SIMP_TAC[VORONOI_LIST_BIS] THEN
2314
2315      MATCH_MP_TAC POLYHEDRON_INTER THEN
2316      CONJ_TAC THENL
2317      [
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];
2323        ALL_TAC
2324      ] THEN
2325
2326      MATCH_MP_TAC POLYHEDRON_INTERS THEN
2327      CONJ_TAC THENL
2328      [
2329        ONCE_REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
2330          MATCH_MP_TAC FINITE_IMAGE THEN
2331          REWRITE_TAC[FINITE_SET_OF_LIST];
2332        ALL_TAC
2333      ] THEN
2334
2335      REWRITE_TAC[IN_ELIM_THM] THEN
2336      REPEAT STRIP_TAC THEN
2337      ASM_REWRITE_TAC[POLYHEDRON_BIS]);;
2338
2339
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]);;
2353
2354
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
2359    CONJ_TAC THENL
2360    [
2361      MATCH_MP_TAC BARV_SUBSET THEN
2362        EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[];
2363      ALL_TAC
2364    ] THEN
2365    REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
2366    POP_ASSUM MP_TAC THEN SIMP_TAC[BARV; ARITH_RULE `~(k + 1 = 0)`]);;
2367
2368
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]);;
2377
2378
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]);;
2387
2388
2389
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);;
2396
2397
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
2404      ANTS_TAC THENL
2405      [
2406        EXISTS_TAC `HD vl:real^3` THEN
2407          REWRITE_TAC[] THEN
2408          MATCH_MP_TAC HD_IN_SET_OF_LIST THEN
2409          ASM_REWRITE_TAC[];
2410        ALL_TAC
2411      ] THEN
2412      REWRITE_TAC[]);;
2413
2414
2415
2416 (************************************************************)
2417
2418 (*****************************************************)
2419 (* General properties of omega_list_n and omega_list *)
2420 (*****************************************************)
2421
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
2426      [
2427        MATCH_MP_TAC (GSYM HD_TRUNCATE_SIMPLEX) THEN
2428          POP_ASSUM MP_TAC THEN ARITH_TAC;
2429        ALL_TAC
2430      ] THEN
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
2434      AP_TERM_TAC 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`]);;
2438
2439
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
2445      DISCH_TAC 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]);;
2448
2449
2450
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
2461      [
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
2465          ASM_REWRITE_TAC[];
2466        ALL_TAC
2467      ] THEN
2468      INT_ARITH_TAC);;
2469
2470
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
2476      [
2477        UNDISCH_TAC `barV V k ul` THEN
2478          SIMP_TAC[BARV];
2479        ALL_TAC
2480      ] THEN
2481      DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
2482      [
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];
2488        ALL_TAC
2489      ] THEN
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
2493      ANTS_TAC THENL
2494      [
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
2500          ASM_REWRITE_TAC[];
2501        ALL_TAC
2502      ] THEN
2503      ASM_SIMP_TAC[]);;
2504
2505
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
2513      [
2514        POP_ASSUM MP_TAC THEN SIMP_TAC[BARV];
2515        ALL_TAC
2516      ] THEN
2517
2518      SUBGOAL_THEN `truncate_simplex k ul = ul:(real^3)list` (fun th -> REWRITE_TAC[th]) THENL
2519      [
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];
2522        ALL_TAC
2523      ] THEN
2524
2525      ASM_REWRITE_TAC[ARITH_RULE `(k + 1) - 1 = k`]);;
2526
2527
2528
2529 end;;