HOL html


(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-03-15                                                           *)
(* Proofs of: KIUMVTC, TIWWFYQ, DRUQUFE                                       *)
(* ========================================================================== *)


flyspeck_needs "general/sphere.hl";;
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "packing/pack2.hl";;


module Packing3 = struct


open Sphere;;
open Pack_defs;;


let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;


(* Alternative definition of the packing *)
let packing_lt = prove(`packing (V:real^3 -> bool) = 
      (!u:real^3 v:real^3. (u IN V) /\ (v IN V) /\ (dist( u, v) < &2) ==>
      (u = v))`,
     REWRITE_TAC[packing;IN;REAL_ARITH `x<y <=> ~(y<= x)`]
       THEN MESON_TAC[]);;

let BIS_SYM = prove(`!p (q:real^N). bis p q = bis q p`,
   REWRITE_TAC[bis] THEN SET_TAC[]);;



(***********************************************************************************)
(***********************************************************************************)
(***********************************************************************************)


(*********************************)
(* Auxiliary general definitions *)
(*********************************)

let discrete = new_definition `discrete S <=> ?e. &0 < e /\ (!x y. x IN S /\ y IN S /\ dist(x, y) < e ==> x = y)`;;

(****************************)
(* Auxiliary general lemmas *)
(****************************)

let IMAGE_LEMMA = prove(`!s f. IMAGE f s = {f x | x IN s}`, SET_TAC[IMAGE]);;

let CHOICE_LEMMA = MESON[] `!y (P:A->bool). ((?x. P x) /\ (!x. P x ==> (x = y))) ==> (@x. P x) = y`;;


let SING_GSPEC_APP = prove(`!(f:A->B) a. {f x | x = a} = {f a}`,
   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN
     REPEAT STRIP_TAC THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL [ ASM_REWRITE_TAC[]; ALL_TAC ] THEN
     EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]);;	 

let SING_UNION_EQ_INSERT = prove(`!s x:A. {x} UNION s = x INSERT s`, SET_TAC[]);;

let IN_TRANS = prove(`!(x:A) s t. x IN t /\ t SUBSET s ==> x IN s`, SIMP_TAC[SUBSET]);;

let PROJECTION_ORTHOGONAL = prove(`!d v:real^N. projection d v dot d = &0`,
   REWRITE_TAC[DOT_SYM; projection; VECTOR_SUB_PROJECT_ORTHOGONAL]);;


let LENGTH_IMP_CONS = prove(`!l:(A)list. 1 <= LENGTH l ==> ?h t. l = CONS h t`,
   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`l:(A)list`; `PRE (LENGTH (l:(A)list))`] LENGTH_EQ_CONS) THEN
     ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> SUC (PRE n) = n`] THEN
     STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`h:A`; `t:(A)list`] THEN
     ASM_REWRITE_TAC[]);;
   
   
let LENGTH_1_LEMMA = prove(`!ul:(A)list. LENGTH ul = 1 ==> ul = [HD ul]`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `ul:(A)list` LENGTH_IMP_CONS) THEN
     ASM_REWRITE_TAC[LE_REFL] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[HD] THEN
     SUBGOAL_THEN `t:(A)list = []` (fun th -> REWRITE_TAC[th]) THEN
     MP_TAC (ISPEC `ul:(A)list` LENGTH_TL) THEN
     ASM_REWRITE_TAC[NOT_CONS_NIL; TL; SUB_REFL; LENGTH_EQ_NIL]);;

	 
	
let PERMUTES_TRIVIAL = prove(`!p. p permutes 0..0 <=> p = I`,
   GEN_TAC THEN EQ_TAC THENL
     [
       REWRITE_TAC[permutes; FUN_EQ_THM; I_THM; IN_NUMSEG; DE_MORGAN_THM; LE_0; NOT_LE] THEN
	 REPEAT STRIP_TAC THEN
	 ASM_CASES_TAC `x = 0` THENL
	 [
	   FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
	     REWRITE_TAC[EXISTS_UNIQUE] THEN
	     STRIP_TAC THEN REMOVE_ASSUM THEN
	     SUBGOAL_THEN `x' = 0` ASSUME_TAC THENL
	     [
	       ASM_CASES_TAC `x' = 0` THEN ASM_REWRITE_TAC[] THEN
		 FIRST_X_ASSUM (MP_TAC o SPEC `x':num`) THEN
		 ASM_REWRITE_TAC[ARITH_RULE `0 < x' <=> ~(x' = 0)`];
	       ALL_TAC
	     ] THEN

	     UNDISCH_TAC `(p:num->num) x' = 0` THEN ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN
	 FIRST_X_ASSUM MATCH_MP_TAC THEN
	 POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     SIMP_TAC[PERMUTES_I]);;	 
	 
let CONTAINS_BALL_AFFINE_HULL = prove(`!s (x:real^N) r. &0 < r /\ ball (x,r) SUBSET s ==> affine hull s = UNIV`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUBSET_ANTISYM THEN
     REWRITE_TAC[SUBSET_UNIV] THEN
     MATCH_MP_TAC SUBSET_TRANS THEN
     EXISTS_TAC `affine hull (ball (x:real^N,r))` THEN
     ASM_SIMP_TAC[HULL_MONO] THEN
     SUBGOAL_THEN `affine hull ball (x:real^N,r) = UNIV` (fun th -> REWRITE_TAC[th; SUBSET_REFL]) THEN
     MATCH_MP_TAC AFFINE_HULL_OPEN THEN
     ASM_REWRITE_TAC[OPEN_BALL; BALL_EQ_EMPTY; REAL_NOT_LE]);;
	 
(* conv (A UNION B) = conv(A UNION conv B) *)
let CONV_UNION_lemma = prove(`!A B:real^N->bool. convex hull (A UNION B) = convex hull (A UNION convex hull B)`,
   REPEAT GEN_TAC THEN
     MATCH_MP_TAC CONVEX_HULLS_EQ THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC SUBSET_TRANS THEN
	 EXISTS_TAC `convex hull (A UNION B:real^N->bool)` THEN
	 REWRITE_TAC[HULL_SUBSET] THEN
	 MATCH_MP_TAC HULL_MONO THEN
	 REWRITE_TAC[SUBSET; IN_UNION] THEN
	 GEN_TAC THEN
	 DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
	 DISJ2_TAC THEN
	 POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
	 REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
       ALL_TAC
     ] THEN

     MATCH_MP_TAC SUBSET_TRANS THEN
     EXISTS_TAC `convex hull (A:real^N->bool) UNION convex hull (B:real^N->bool)` THEN
     CONJ_TAC THENL
     [
       REWRITE_TAC[SUBSET; IN_UNION] THEN
	 GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
	 DISJ1_TAC THEN
	 POP_ASSUM MP_TAC THEN SPEC_TAC (`x:real^N`, `x:real^N`) THEN
	 REWRITE_TAC[GSYM SUBSET; HULL_SUBSET];
       ALL_TAC
     ] THEN

     REWRITE_TAC[HULL_UNION_SUBSET]);;	 
	 
let CONVEX_HULL_EQ_EQ_SET_EQ = prove(`!s t:real^N->bool. ~affine_dependent s /\ ~affine_dependent t ==> 
				      (convex hull s = convex hull t <=> s = t)`,
   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `FINITE (s:real^N->bool) /\ FINITE (t:real^N->bool)` ASSUME_TAC THENL
     [
       ASM_SIMP_TAC[AFFINE_INDEPENDENT_IMP_FINITE];
       ALL_TAC
     ] THEN
     
     EQ_TAC THEN SIMP_TAC[] THEN
     DISCH_TAC THEN

     SUBGOAL_THEN `s = {x | x extreme_point_of convex hull s}:real^N->bool` ASSUME_TAC THENL
     [
       MP_TAC (ISPEC `s:real^N->bool` EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
	 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; EQ_SYM_EQ];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `t = {x | x extreme_point_of convex hull t}:real^N->bool` ASSUME_TAC THENL
     [
       MP_TAC (ISPEC `t:real^N->bool` EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
	 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; EQ_SYM_EQ];
       ALL_TAC
     ] THEN
     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
     ASM_REWRITE_TAC[]);;	 
	 
(* Lemmas about intersections *)

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`,
   REWRITE_TAC[SUBSET_INTER] THEN
     REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_MONO THEN REWRITE_TAC[INTER_SUBSET]);;

let HULL_INTER_EQ_INTER = prove(`!P s (t:A->bool). P s /\ P t ==> P hull (s INTER t) = s INTER t`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUBSET_ANTISYM THEN
     REWRITE_TAC[HULL_SUBSET] THEN
     MP_TAC (SPEC_ALL HULL_INTER_SUBSET_INTER_HULL) THEN
     ASM_SIMP_TAC[HULL_P]);;

let SUBSET_INTERS = prove(`!(s:A->bool) f. s SUBSET INTERS f <=> (!t. t IN f ==> s SUBSET t)`, SET_TAC[]);;

let HULL_INTERS_SUBSET_INTERS_HULL = prove(`!P:((A->bool)->bool) s. P hull (INTERS s) SUBSET INTERS {P hull t | t IN s}`,
   REPEAT GEN_TAC THEN
     REWRITE_TAC[SUBSET_INTERS; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC HULL_MONO THEN
     REWRITE_TAC[SUBSET; IN_INTERS; IN_ELIM_THM] THEN
     GEN_TAC THEN DISCH_THEN (MP_TAC o SPEC `t':A->bool`) THEN
     ASM_REWRITE_TAC[]);;
	 
let HULL_INTERS_EQ_INTERS = prove(`!P:((A->bool)->bool) s. (!t. t IN s ==> P t) ==> P hull (INTERS s) = INTERS s`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUBSET_ANTISYM THEN
     REWRITE_TAC[HULL_SUBSET] THEN
     MP_TAC (SPEC_ALL HULL_INTERS_SUBSET_INTERS_HULL) THEN
     SUBGOAL_THEN `{P hull t | t IN s} = s:(A->bool)->bool` (fun th -> SIMP_TAC[th]) THEN
     REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN GEN_TAC THEN
     EQ_TAC THENL
     [
       REWRITE_TAC[GSYM EXTENSION] THEN
	 STRIP_TAC THEN
	 ASM_SIMP_TAC[HULL_P];
       ALL_TAC
     ] THEN
     REWRITE_TAC[GSYM EXTENSION] THEN
     DISCH_TAC THEN EXISTS_TAC `x:A->bool` THEN
     ASM_SIMP_TAC[HULL_P]);;	 
	 
	 





let INTERS_2_LEMMA = prove(`!a b f. INTERS {f x | x IN {a, b}} = f a INTER f b`, SET_TAC[INTERS]);;

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}`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[EXTENSION; IN_INTER; IN_INTERS; IN_ELIM_THM] THEN
     GEN_TAC THEN EQ_TAC THENL
     [
       REPEAT STRIP_TAC THEN
	 ASM SET_TAC[];

       ALL_TAC
     ] THEN
     REPEAT STRIP_TAC THENL
     [
       SUBGOAL_THEN `?t':B. t' IN (f:B->bool)` MP_TAC THENL
       [
	 FIRST_X_ASSUM (MP_TAC o check (is_neg o concl)) THEN
	   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
	   REWRITE_TAC[NOT_FORALL_THM];
	 ALL_TAC
       ] THEN
       STRIP_TAC THEN
       FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
       ANTS_TAC THENL
       [
	 EXISTS_TAC `t':B` THEN
	 ASM_REWRITE_TAC[IN_INTER];
	 ALL_TAC
       ] THEN
       SIMP_TAC[IN_INTER];

       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `(s:A->bool) INTER (P (t':B))`) THEN
     ANTS_TAC THENL
     [
       EXISTS_TAC `t':B` THEN
       ASM_REWRITE_TAC[IN_INTER];
       ALL_TAC
     ] THEN
     SIMP_TAC[IN_INTER]);;


let INTERS_UNIV = prove(`!f:(A->bool)->bool. INTERS f = INTERS (f DELETE UNIV)`,
   GEN_TAC THEN REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM; IN_DELETE; IN_UNIV] THEN
     MESON_TAC[]);; 
     

let INTERS_INTER_INTERS = prove(`!f g. INTERS f INTER INTERS g = INTERS (f UNION g)`, SET_TAC[]);;


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)}`,
  SET_TAC[]);;


let REAL_DIV_LE_1 = prove(`!a b. &0 < b ==> (a / b <= &1 <=> a <= b)`,
			  MESON_TAC[REAL_LE_LDIV_EQ; REAL_MUL_LID]);;


(* Union of finite sets is finite *)
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})`,
			 REPEAT STRIP_TAC THEN
			   MP_TAC (ISPEC `{(P:(A->bool)->(A->bool)) t | t IN g}` FINITE_FINITE_UNIONS) THEN
			   SUBGOAL_THEN `FINITE {(P:(A->bool)->(A->bool)) t | t IN (g:(A->bool)->bool)}` (fun th -> REWRITE_TAC[th]) THENL
			   [
			     REWRITE_TAC[SIMPLE_IMAGE] THEN
			       ASM_SIMP_TAC[FINITE_IMAGE];
			     ALL_TAC
			   ] THEN
			   DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
			   REWRITE_TAC[IN_ELIM_THM] THEN
			   REPEAT STRIP_TAC THEN
			   ASM_MESON_TAC[]);;


(* Lemmas about min and max for finite sets of real numbers *)
let REAL_FINITE_MIN_EXISTS = prove(`!S:real->bool. FINITE S /\ ~(S = {}) ==> ?m. m IN S /\ (!x. x IN S ==> m <= x)`,
		MESON_TAC[INF_FINITE]);;

let REAL_FINITE_MAX_EXISTS = prove(`!S:real->bool. FINITE S /\ ~(S = {}) ==> ?m. m IN S /\ (!x. x IN S ==> x <= m)`,
		MESON_TAC[SUP_FINITE]);;

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)`,
	REPEAT STRIP_TAC THEN
	  SUBGOAL_THEN `?m. m IN IMAGE (f:A->real) S /\ !y. y IN IMAGE f S ==> m <= y` MP_TAC THENL
	  [
	    MATCH_MP_TAC REAL_FINITE_MIN_EXISTS THEN
	      ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];

	    ALL_TAC
	  ] THEN

	  REWRITE_TAC[IN_IMAGE] THEN
	  MESON_TAC[]);;

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)`,
	REPEAT STRIP_TAC THEN
	  SUBGOAL_THEN `?m. m IN IMAGE (f:A->real) S /\ !y. y IN IMAGE f S ==> y <= m` MP_TAC THENL
	  [
	    MATCH_MP_TAC REAL_FINITE_MAX_EXISTS THEN
	      ASM_MESON_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE];

	    ALL_TAC
	  ] THEN

	  REWRITE_TAC[IN_IMAGE] THEN
	  MESON_TAC[]);;

	  
(***************************)
(* Properties of bisectors *)
(***************************)

let BIS_EQ_HYPERPLANE = prove(`!u v. bis u v = {x | &2 % (v - u) dot x = v dot v - u dot u}`,
							REWRITE_TAC[bis; EXTENSION; IN_ELIM_THM; dist; NORM_EQ] THEN
							REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_RMUL; DOT_SYM] THEN
							REAL_ARITH_TAC);;

let BIS_LE_EQ_HALFSPACE = prove(`!u v. bis_le u v = {x | &2 % (v - u) dot x <= v dot v - u dot u}`,
								REWRITE_TAC[bis_le; EXTENSION; IN_ELIM_THM; dist; NORM_LE] THEN
								REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_RMUL; DOT_SYM] THEN
								REAL_ARITH_TAC);;

let CONVEX_BIS_LE = prove(`!u v:real^N. convex (bis_le u v)`,
						REWRITE_TAC[BIS_LE_EQ_HALFSPACE; CONVEX_HALFSPACE_LE]);;


let CLOSED_BIS_LE = prove(`!u v:real^N. closed (bis_le u v)`,
						REWRITE_TAC[BIS_LE_EQ_HALFSPACE; CLOSED_HALFSPACE_LE]);;

let CONVEX_BIS = prove(`!u v:real^N. convex(bis u v)`,
						REWRITE_TAC[BIS_EQ_HYPERPLANE; CONVEX_HYPERPLANE]);;						
						
let POLYHEDRON_BIS = prove(`!u v:real^N. polyhedron (bis u v)`,
     ASM_REWRITE_TAC[BIS_EQ_HYPERPLANE; POLYHEDRON_HYPERPLANE]);;	 
	 

let AFFINE_BIS = prove(`!a b:real^N. affine (bis a b)`,
   REWRITE_TAC[BIS_EQ_HYPERPLANE; AFFINE_HYPERPLANE]);;     

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}`,
   REPEAT GEN_TAC THEN
     MATCH_MP_TAC HULL_INTERS_EQ_INTERS THEN
     REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[AFFINE_BIS]);;


(* Auxiliary lemma for distances and points inside an interval *)
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`,
        REPEAT GEN_TAC THEN
	  DISJ_CASES_TAC (TAUT `dist(v:real^N, w) = &0 \/ ~(dist(v, w) = &0)`) THENL
	  [
	    ASM_SIMP_TAC[REAL_LE_ANTISYM] THEN DISCH_TAC THEN
	      EXISTS_TAC `v:real^N` THEN
	      ASM_SIMP_TAC[BETWEEN_IN_SEGMENT; ENDS_IN_SEGMENT; DIST_REFL];

	    ALL_TAC
	  ] THEN
	  SUBGOAL_TAC "A" `&0 < dist(v:real^N, w)` [ ASM_MESON_TAC[REAL_ARITH `&0 <= a /\ ~(a = &0) ==> &0 < a`; DIST_POS_LE] ] THEN
	  REPEAT STRIP_TAC THEN
	  EXISTS_TAC `(v:real^N) + (d:real / dist(v, w)) % (w - v)` THEN
	  CONJ_TAC THENL
	  [
	    REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN
	      EXISTS_TAC `d / dist(v:real^N, w)` THEN
	      ASM_SIMP_TAC [REAL_LT_IMP_LE; REAL_LE_DIV; REAL_DIV_LE_1];
	      
	    ASM_REWRITE_TAC[dist; NORM_EQ_SQUARE] THEN
	      REWRITE_TAC[VECTOR_ARITH `v - (v + a % (b - c)) = a % (c - b)`] THEN
	      REWRITE_TAC[DOT_RMUL; DOT_LMUL] THEN
	      REWRITE_TAC[GSYM NORM_POW_2; GSYM dist; REAL_POW_2] THEN
	      REMOVE_THEN "A" MP_TAC THEN
	      CONV_TAC REAL_FIELD
 	  ]);;
			  
	  
(********************************************************)
(* Proof that V(v,r) is finite begins here              *)
(********************************************************)

(* General properties of discrete sets *)
	  
(* Any discrete set is closed *)
let CLOSED_DISCRETE = prove(`!A. discrete A ==> closed A`,
							REWRITE_TAC[discrete] THEN REPEAT STRIP_TAC THEN
								MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN
								EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[GSYM dist; DIST_SYM] THEN
								ASM_MESON_TAC[]);;			      

(* Any subset of a discrete set is discrete *)
let DISCRETE_SUBSET = prove(`!A B:real^N -> bool. discrete A /\ B SUBSET A ==> discrete B`,
						REWRITE_TAC[discrete; SUBSET] THEN REPEAT STRIP_TAC THEN
							EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN
							ASM_MESON_TAC[]);;

(* A discrete and bounded set is compact *)
let DISCRETE_IMP_BOUNDED_EQ_COMPACT = prove(`!S. discrete S ==> (bounded S <=> compact S)`,
		     MESON_TAC[CLOSED_DISCRETE; BOUNDED_CLOSED_IMP_COMPACT; COMPACT_IMP_BOUNDED]);;
				       

(* If S is discrete, then there is an open cover by balls b such that |b INTER S| = 1 *)
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`,
			     REWRITE_TAC[discrete] THEN REPEAT STRIP_TAC THEN
			       EXISTS_TAC `{ball(x, e) | x IN (S:real^N->bool)}` THEN
			       REWRITE_TAC[IN_ELIM_THM; SUBSET; UNIONS] THEN
			       CONJ_TAC THEN REPEAT STRIP_TAC THENL
			       [
				 ASM_SIMP_TAC[OPEN_BALL];
				 CONV_TAC HAS_SIZE_CONV THEN
				   EXISTS_TAC `x:real^N` THEN
				   ASM_REWRITE_TAC[INTER; ball; IN_ELIM_THM; EXTENSION; IN_SING] THEN
				   ASM_MESON_TAC[DIST_EQ_0];
				 EXISTS_TAC `ball(x:real^N, e)` THEN
				   ASM_REWRITE_TAC[CENTRE_IN_BALL] THEN
				   EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]
			       ]);;
				   
(* Discrete and bounded S is finite *)
let DISCRETE_BOUNDED_IMP_FINITE = prove(`!S:real^N->bool. discrete S /\ bounded S ==> FINITE S`,
			REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
			  MP_TAC (ISPEC `S:real^N->bool` DISCRETE_IMP_BOUNDED_EQ_COMPACT) THEN
			  ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
							      
			  REWRITE_TAC[COMPACT_EQ_HEINE_BOREL] THEN
			  REPEAT STRIP_TAC THEN
			  MP_TAC (SPEC `S:real^N -> bool` DISCRETE_OPEN_COVER) THEN
			  ASM_REWRITE_TAC[] THEN
			  DISCH_THEN (X_CHOOSE_THEN `f:(real^N->bool)->bool` MP_TAC) THEN
			  FIRST_X_ASSUM ((LABEL_TAC "A") o (SPEC `f:(real^N->bool)->bool`)) THEN
			  DISCH_THEN (LABEL_TAC "B") THEN
			  REMOVE_THEN "A" MP_TAC THEN ASM_SIMP_TAC[] THEN
			  DISCH_THEN (X_CHOOSE_THEN `g:(real^N->bool)->bool` MP_TAC) THEN
			  STRIP_TAC THEN
			  SUBGOAL_THEN `FINITE (S INTER UNIONS (g:(real^N->bool)->bool))` ASSUME_TAC THENL
			  [
	 		    REWRITE_TAC[INTER_UNIONS] THEN
			      MATCH_MP_TAC UNIONS_FINITE_LEMMA THEN
			      ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
			      REMOVE_THEN "B" (MP_TAC o (SPEC `x:real^N -> bool`) o CONJUNCT1) THEN
			      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
			      SIMP_TAC[INTER_COMM; HAS_SIZE];
			    ALL_TAC
			  ] THEN
			  ASM_MESON_TAC[SET_RULE `S SUBSET A ==> S INTER A = S`]);;				      


				     
			       
(* Proof of the main lemma begins here *)

(* A packing is a discrete set *)
let PACKING_IMP_DISCRETE = prove(`!V. packing V ==> discrete V`,
			     REWRITE_TAC[packing_lt; discrete] THEN REPEAT STRIP_TAC THEN
			       EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[REAL_ARITH `&0 < &2`]);;
(* Main lemma: if V is a packing then (V INTER ball) is finite *)
let KIUMVTC = prove(`!(p:real^3) r V. packing V ==> FINITE (V INTER ball(p, r))`,
		  REPEAT STRIP_TAC THEN MATCH_MP_TAC DISCRETE_BOUNDED_IMP_FINITE THEN CONJ_TAC THENL
		    [
		      ALL_TAC;
		      ASM_SIMP_TAC[BOUNDED_INTER; BOUNDED_BALL]
		    ] THEN
		    MATCH_MP_TAC DISCRETE_SUBSET THEN
		    EXISTS_TAC `V:real^3->bool` THEN
		    ASM_SIMP_TAC[PACKING_IMP_DISCRETE] THEN
		    SET_TAC[]);;


			
			
(****************************************************)			
(* TIWWFYQ                                          *)
(* If a packing is saturated, then every point of   *)
(* the space is inside some Voronoi (closed) cell   *)
(****************************************************)


(* AS: real^N <== pacling:real^N *)
let TIWWFYQ = prove(`!V (p:real^3). packing V /\ saturated V ==> (?v.  v IN V /\ p IN voronoi_closed V v)`,
    REWRITE_TAC[saturated] THEN REPEAT STRIP_TAC THEN
      ABBREV_TAC `S = V INTER ball(p:real^3, &2)` THEN
      SUBGOAL_THEN `?v:real^3. v IN S /\ !w. w IN S ==> dist(v, p) <= dist(w, p)` MP_TAC THENL
      [
	  MATCH_MP_TAC REAL_FINITE_ARGMIN THEN
	    EXPAND_TAC "S" THEN
	    ASM_SIMP_TAC[KIUMVTC] THEN
	    REWRITE_TAC[SET_RULE `~(S = {}) <=> ?a. a IN S`] THEN
	    EXPAND_TAC "S" THEN REWRITE_TAC[ball; INTER; IN_ELIM_THM] THEN
	    ASM_MESON_TAC[];

	ALL_TAC
      ] THEN
      STRIP_TAC THEN
      EXISTS_TAC `v:real^3` THEN
      REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN EXPAND_TAC "S" THEN POP_ASSUM (fun th -> ALL_TAC) THEN
      ASM_SIMP_TAC[IN_INTER] THEN
      DISCH_THEN (LABEL_TAC "A") THEN
      DISCH_THEN (LABEL_TAC "B") THEN
      REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN GEN_TAC THEN
      GEN_REWRITE_TAC LAND_CONV [GSYM IN] THEN
      DISJ_CASES_TAC (TAUT `w:real^3 IN ball(p, &2) \/ ~(w IN ball(p, &2))`) THENL
      [
	ASM_MESON_TAC[DIST_SYM];
	SUBGOAL_THEN `&2 <= dist(p:real^3, w)` MP_TAC THENL
	  [
	    POP_ASSUM MP_TAC THEN REWRITE_TAC[ball; IN_ELIM_THM; REAL_NOT_LT];
	    ALL_TAC
	  ] THEN
	  
	  SUBGOAL_THEN `dist(p:real^3, v) < &2` MP_TAC THENL
	  [
	    REMOVE_THEN "A" MP_TAC THEN SIMP_TAC[ball; IN_ELIM_THM];
	    ALL_TAC
	  ] THEN

	  REAL_ARITH_TAC
      ]);;

	  
	  
	  
(*******************************)
(* Porperties of Voronoi cells *)
(*******************************)

(* v IN voronoi_closed V v *)
let CENTER_IN_VORONOI_CELL = prove(`!V (v:real^3). v IN voronoi_closed V v /\ v IN voronoi_open V v`,
   REPEAT GEN_TAC THEN
     SUBGOAL_THEN `v IN voronoi_open V (v:real^3)` ASSUME_TAC THENL
     [
       REWRITE_TAC[voronoi_open; IN_ELIM_THM; DIST_REFL] THEN
	 SIMP_TAC[DIST_POS_LT];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC IN_TRANS THEN
     EXISTS_TAC `voronoi_open V (v:real^3)` THEN
     ASM_REWRITE_TAC[Pack2.VORONOI_OPEN_SUBSET_CLOSED]);;	 
	 

(* voronoi_closed V v contains a ball *)
let VORONOI_CLOSED_CONTAINS_BALL = prove(`!V (v:real^3). packing V ==> ?r. &0 < r /\ ball (v, r) SUBSET voronoi_closed V v`,
   REWRITE_TAC[packing; voronoi_closed] THEN
     REPEAT STRIP_TAC THEN
     ASM_CASES_TAC `v:real^3 IN V` THENL
     [
       POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN DISCH_TAC THEN
	 EXISTS_TAC `&1` THEN
	 REWRITE_TAC[REAL_LT_01; ball; SUBSET; IN_ELIM_THM] THEN
	 REPEAT STRIP_TAC THEN
	 ASM_CASES_TAC `w = v:real^3` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
	 FIRST_X_ASSUM (MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 SUBGOAL_THEN `&2 - dist(x,v:real^3) <= dist(x,w:real^3)` MP_TAC THENL
	 [
	   REWRITE_TAC[REAL_ARITH `a - b <= c <=> a <= b + c:real`] THEN
	     MATCH_MP_TAC REAL_LE_TRANS THEN
	     EXISTS_TAC `dist (v,w:real^3)` THEN
	     ASM_REWRITE_TAC[] THEN
	     MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
	     REWRITE_TAC[DIST_SYM];
	   ALL_TAC
	 ] THEN

	 UNDISCH_TAC `dist (v,x:real^3) < &1` THEN
	 REWRITE_TAC[DIST_SYM] THEN
	 REAL_ARITH_TAC;
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `?s. &0 < s /\ ball (v:real^3, s) INTER V = {}` STRIP_ASSUME_TAC THENL
     [
       SUBGOAL_THEN `~(ball (v:real^3, &1) INTER V = {}) ==> ?x. ball (v:real^3, &1) INTER V = {x}` MP_TAC THENL
         [
	   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; EXTENSION; IN_SING; ball; IN_ELIM_THM] THEN
	     STRIP_TAC THEN
	     EXISTS_TAC `x:real^3` THEN
	     GEN_TAC THEN EQ_TAC THENL
	     [
	       STRIP_TAC THEN
		 SUBGOAL_THEN `dist (x:real^3, x') < &2` MP_TAC THENL
		 [
		   MATCH_MP_TAC REAL_LET_TRANS THEN
		     EXISTS_TAC `dist (x,v) + dist(v:real^3,x')` THEN
		     REWRITE_TAC[DIST_TRIANGLE; REAL_ARITH `&2 = &1 + &1`] THEN
		     MATCH_MP_TAC REAL_LT_ADD2 THEN
		     ASM_REWRITE_TAC[DIST_SYM];
		   ALL_TAC
		 ] THEN

		 FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `x':real^3`]) THEN
		 POP_ASSUM MP_TAC THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN SIMP_TAC[IN] THEN
		 DISCH_TAC THEN DISCH_TAC THEN
		 ASM_CASES_TAC `x' = x:real^3` THEN ASM_REWRITE_TAC[REAL_NOT_LT];
	       ALL_TAC
	     ] THEN

	     ASM_SIMP_TAC[];
	   ALL_TAC
	 ] THEN

	 ASM_CASES_TAC `ball (v:real^3, &1) INTER V = {}` THEN ASM_REWRITE_TAC[] THENL
         [
	   EXISTS_TAC `&1` THEN
	     ASM_REWRITE_TAC[REAL_LT_01];
	   ALL_TAC
	 ] THEN

	 STRIP_TAC THEN
	 EXISTS_TAC `dist (v:real^3, x)` THEN
	 CONJ_TAC THENL
	 [
	   MATCH_MP_TAC DIST_POS_LT THEN
	     DISCH_THEN (ASSUME_TAC o SYM) THEN
	     UNDISCH_TAC `ball (v:real^3, &1) INTER V = {x}` THEN
	     ASM_REWRITE_TAC[EXTENSION; IN_INTER; IN_SING; NOT_FORALL_THM] THEN
	     EXISTS_TAC `x:real^3` THEN
	     ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN

	 POP_ASSUM MP_TAC THEN
	 REWRITE_TAC[EXTENSION; IN_INTER; ball; IN_ELIM_THM; NOT_IN_EMPTY; IN_SING] THEN
	 REPEAT STRIP_TAC THEN
	 FIRST_ASSUM (MP_TAC o SPEC `x:real^3`) THEN
	 REWRITE_TAC[] THEN DISCH_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o SPEC `x':real^3`) THEN
	 SUBGOAL_THEN `dist (v,x':real^3) < &1` ASSUME_TAC THENL
	 [
	   MATCH_MP_TAC REAL_LT_TRANS THEN
	     EXISTS_TAC `dist (v, x:real^3)` THEN
	     ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 UNDISCH_TAC `dist (v,x':real^3) < dist (v,x)` THEN
	 ASM_REWRITE_TAC[REAL_LT_REFL];
       ALL_TAC
     ] THEN

     EXISTS_TAC `s / &2` THEN
     POP_ASSUM MP_TAC THEN
     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
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`) THEN
     ASM_REWRITE_TAC[IN] THEN DISCH_TAC THEN
     SUBGOAL_THEN `s - dist(x,v:real^3) <= dist(x,w:real^3)` MP_TAC THENL
     [
       REWRITE_TAC[REAL_ARITH `a - b <= c <=> a <= b + c:real`] THEN
	 MATCH_MP_TAC REAL_LE_TRANS THEN
	 EXISTS_TAC `dist (v,w:real^3)` THEN
	 ASM_REWRITE_TAC[] THEN
	 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
	 REWRITE_TAC[DIST_SYM];
       ALL_TAC
     ] THEN

     UNDISCH_TAC `dist (v, x:real^3) < s / &2` THEN
     UNDISCH_TAC `&0 < s` THEN
     REWRITE_TAC[DIST_SYM] THEN
     REAL_ARITH_TAC);;


(* aff_dim voronoi_closed V v = 3 *)  
let AFF_DIM_VORONOI_CLOSED = prove(`!V v. packing V ==> aff_dim (voronoi_closed V v) = &3`,
   REWRITE_TAC[GSYM DIMINDEX_3; AFF_DIM_EQ_FULL] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CONTAINS_BALL_AFFINE_HULL THEN
     MP_TAC (SPEC_ALL VORONOI_CLOSED_CONTAINS_BALL) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`v:real^3`; `r:real`] THEN
     ASM_REWRITE_TAC[]);;
	
     


(* For a saturated packing each Voronoi cell is inside a ball of radius 2 *)
let VORONOI_BALL2 = prove(`!V (v:real^N). saturated V ==> voronoi_closed V v SUBSET ball(v, &2)`,
			  REWRITE_TAC[saturated; voronoi_closed] THEN REPEAT STRIP_TAC THEN
			     REWRITE_TAC[SUBSET; ball; IN_ELIM_THM] THEN
			     X_GEN_TAC `y:real^N` THEN
			     ONCE_REWRITE_TAC[TAUT `(A ==> B) <=> (~B ==> ~A)`] THEN
			     REWRITE_TAC[REAL_NOT_LT; NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
			     FIRST_X_ASSUM ((X_CHOOSE_THEN `w:real^N` MP_TAC) o SPEC `y:real^N`) THEN
			     REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
			     EXISTS_TAC `w:real^N` THEN
			     ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN
			     REWRITE_TAC[DIST_SYM] THEN
			     REAL_ARITH_TAC);;

(* A Voronoi cell is bounded (for a saturated packing) *)
let BOUNDED_VORONOI_CLOSED = prove(`!V (v:real^N). saturated V ==> bounded (voronoi_closed V v)`,
				   REPEAT STRIP_TAC THEN
				     MATCH_MP_TAC BOUNDED_SUBSET THEN
				     ASM_MESON_TAC[VORONOI_BALL2; BOUNDED_BALL]);;				     

(* A closed Voronoi cell is an intersection of bisector half-spaces *)
let VORONOI_CLOSED_EQ_INTERS_BIS_LE = prove(`!S v:real^N. voronoi_closed S v = INTERS {bis_le v w | w IN S}`,
	 REPEAT GEN_TAC THEN
	   REWRITE_TAC[voronoi_closed; bis_le; INTERS; IN_ELIM_THM] THEN
	   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN] THEN GEN_TAC THEN
	   EQ_TAC THEN REPEAT STRIP_TAC THENL
	   [
	     ASM_MESON_TAC[];
	     FIRST_X_ASSUM (MP_TAC o (SPEC `bis_le v (w:real^N)`) o check (is_forall o concl)) THEN
	       ANTS_TAC THEN REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
	       EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[]
	   ]);;

(* The same result with excluded point v *)
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)}`,
	 REPEAT GEN_TAC THEN
	   REWRITE_TAC[voronoi_closed; bis_le] THEN
	   REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM; IN] THEN GEN_TAC THEN
	   EQ_TAC THEN REPEAT STRIP_TAC THENL
	   [
	     ASM_MESON_TAC[];
	     DISJ_CASES_TAC (TAUT `w:real^N = v \/ ~(w = v)`) THENL
	       [
		 ASM_REWRITE_TAC[REAL_LE_REFL];
		 ALL_TAC
	       ] THEN
	     FIRST_X_ASSUM (MP_TAC o (SPEC `bis_le v (w:real^N)`) o check (is_forall o concl)) THEN
	       ANTS_TAC THEN REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
	       EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[]
	   ]);;


(* A closed Voronoi cell is an intersection of bisectors for w IN ball(v, 4) *)
let VORONOI_INTER_BIS_LE = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> 
		(voronoi_closed V v =INTERS { bis_le v u | u | u IN V /\ u IN ball(v, &4) /\  ~(u=v) })`,
   REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE_ALT; saturated] THEN REPEAT STRIP_TAC THEN
     REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "A") THEN DISCH_TAC THEN
     REWRITE_TAC[EXTENSION; IN_INTERS] THEN GEN_TAC THEN EQ_TAC THENL
     [
       SET_TAC[];
       ALL_TAC
     ] THEN

     REWRITE_TAC[IN_ELIM_THM] THEN
     DISCH_THEN (LABEL_TAC "B") THEN REPEAT STRIP_TAC THEN
  
     DISJ_CASES_TAC (TAUT `(w:real^3) IN ball(v:real^3, &4) \/ ~(w IN ball(v, &4))`) THENL
     [
       REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN SET_TAC[];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `x:real^3 IN ball(v, &2)` (LABEL_TAC "C") THENL
     [
       POP_ASSUM MP_TAC THEN REWRITE_TAC[ball; IN_ELIM_THM] THEN
	 ONCE_REWRITE_TAC[TAUT `~A ==> B <=> ~B ==> A`] THEN
	 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
	 MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `&2`] MID_POINT_EXISTS) THEN
	 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`] THEN
	 DISCH_THEN (X_CHOOSE_THEN `q:real^3` MP_TAC) THEN
	 REWRITE_TAC[between] THEN STRIP_TAC THEN
	 REMOVE_THEN "A" ((X_CHOOSE_THEN `p:real^3` MP_TAC) o SPEC `q:real^3`) THEN STRIP_TAC THEN
	 REMOVE_THEN "B" (MP_TAC o SPEC `bis_le v (p:real^3)`) THEN
	 ANTS_TAC THENL
	 [
	   EXISTS_TAC `p:real^3` THEN ASM_REWRITE_TAC[ball; IN_ELIM_THM] THEN
	     CONJ_TAC THENL
	     [
	       MP_TAC (ISPECL [`v:real^3`; `q:real^3`; `p:real^3`] DIST_TRIANGLE) THEN
		 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
	       ALL_TAC
	     ] THEN
	     REWRITE_TAC[DIST_NZ] THEN
	     MP_TAC (ISPECL [`v:real^3`; `p:real^3`; `q:real^3`] DIST_TRIANGLE) THEN
	     REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN
	     REAL_ARITH_TAC;

	   ALL_TAC
	 ] THEN

	 REWRITE_TAC[bis_le; IN_ELIM_THM] THEN
	 SUBGOAL_TAC "A" `dist(x:real^3, v) = &2 + dist(q, x)` [ASM_SIMP_TAC[DIST_SYM]] THEN
	 MP_TAC (ISPECL [`x:real^3`; `q:real^3`; `p:real^3`] DIST_TRIANGLE) THEN
	 REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC;

       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     ASM_REWRITE_TAC[bis_le; ball; IN_ELIM_THM; REAL_NOT_LT] THEN
     MP_TAC (ISPECL [`v:real^3`; `x:real^3`; `w:real^3`] DIST_TRIANGLE) THEN
     REWRITE_TAC[DIST_SYM] THEN REAL_ARITH_TAC);;


(* A closed Voronoi cell is an intersection of finitely many closed half-spaces *)
let VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> 
		?W. W SUBSET V /\ ~(v IN W) /\ FINITE W /\ 
		voronoi_closed V v = INTERS { bis_le v u | u | u IN W }`,
  REPEAT GEN_TAC THEN
    DISCH_TAC THEN
    FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP VORONOI_INTER_BIS_LE th)) THEN
    DISCH_TAC THEN
    EXISTS_TAC `(V:real^3->bool) INTER ball(v,&4) DELETE v` THEN
    REPEAT STRIP_TAC THENL
    [
      SET_TAC[];
      ASM SET_TAC[];
      MATCH_MP_TAC FINITE_SUBSET THEN
	EXISTS_TAC `V INTER ball(v:real^3,&4)` THEN
	CONJ_TAC THENL
	[
	  ASM_MESON_TAC[KIUMVTC];
	  ALL_TAC
	] THEN
	SET_TAC[];

    ASM_REWRITE_TAC[] THEN
		SET_TAC[]
    ]);;


(* A closed Voronoi cell is a polyhedron *)

(* AS: real^N (requires packing:real^N) *)
let VORONOI_POLYHEDRON = prove(`!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
   polyhedron (voronoi_closed V v)`,
	REPEAT GEN_TAC THEN
	  DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE th)) THEN
	  STRIP_TAC THEN
	  REWRITE_TAC[polyhedron] THEN
	  EXISTS_TAC `{bis_le v (u:real^3) | u IN W}` THEN
	  ASM_REWRITE_TAC[] THEN
	  CONJ_TAC THENL
	  [
	    REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
	      MATCH_MP_TAC FINITE_IMAGE THEN
	      ASM_REWRITE_TAC[];
	    ALL_TAC
	  ] THEN
	  REWRITE_TAC[IN_ELIM_THM; BIS_LE_EQ_HALFSPACE] THEN
	  REPEAT STRIP_TAC THEN
	  EXISTS_TAC `&2 % (u - v:real^3)` THEN
	  EXISTS_TAC `(u:real^3) dot u - (v:real^3) dot v` THEN
	  ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; REAL_ARITH `~(&2 = &0)`; VECTOR_SUB_EQ] THEN
	  ASM SET_TAC[]);;

(* A closed Voronoi cell is convex *)
let CONVEX_VORONOI_CLOSED = prove(`!S v:real^N. convex(voronoi_closed S v)`,
				  REPEAT GEN_TAC THEN
				    REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE] THEN
				    MATCH_MP_TAC CONVEX_INTERS THEN
				    REWRITE_TAC[IN_ELIM_THM] THEN
				    MESON_TAC[CONVEX_BIS_LE]);;

(* A closed Voronoi cell is closed *)
let CLOSED_VORONOI_CLOSED = prove(`!S v:real^N. closed(voronoi_closed S v)`,
				  REPEAT GEN_TAC THEN
				    REWRITE_TAC[VORONOI_CLOSED_EQ_INTERS_BIS_LE] THEN
				    MATCH_MP_TAC CLOSED_INTERS THEN
				    REWRITE_TAC[IN_ELIM_THM] THEN
				    MESON_TAC[CLOSED_BIS_LE]);;
(* A closed Voronoi cell is compact if a packing is saturated (for boundness) *)
let COMPACT_VORONOI_CLOSED = prove(`!S v. saturated S ==> compact (voronoi_closed S v)`,
			    REPEAT STRIP_TAC THEN
			      MATCH_MP_TAC BOUNDED_CLOSED_IMP_COMPACT THEN
			      ASM_SIMP_TAC[CLOSED_VORONOI_CLOSED; BOUNDED_VORONOI_CLOSED]);;

(****************************************************************)
(* DRUQUFE:											  			*)
(* For a saturated packing, each closed Voronoi closed cell is  *)
(* compact, convex, and measurable 								*)
(****************************************************************)

(* AS: real^N, remove `packing` *)
let DRUQUFE = prove(`!V (v:real^3). packing V /\ saturated V  ==>
     compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`,
		     REPEAT STRIP_TAC THENL
		       [
			 ASM_SIMP_TAC[COMPACT_VORONOI_CLOSED];
			 REWRITE_TAC[CONVEX_VORONOI_CLOSED];
			 MATCH_MP_TAC MEASURABLE_CONVEX THEN
			   ASM_SIMP_TAC[CONVEX_VORONOI_CLOSED; BOUNDED_VORONOI_CLOSED]
		       ]);;





(*************************************************************)			   


(*******************************************)
(* Some results for initial sublists       *)
(*******************************************)

let INITIAL_SUBLIST_APPEND = prove(`!ul vl. initial_sublist ul (APPEND ul vl)`,
				   REWRITE_TAC[INITIAL_SUBLIST] THEN
				     MESON_TAC[]);;

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`,
   REPEAT GEN_TAC THEN
     REWRITE_TAC[INITIAL_SUBLIST] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     ASM_REWRITE_TAC[APPEND] THEN
     MESON_TAC[injectivity "list"]);;

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`,
   MESON_TAC[INITIAL_SUBLIST_HEAD_EQ; INITIAL_SUBLIST; APPEND]);;

   
let INITIAL_SUBLIST_TAIL = prove(`!xl zl hx tx. xl = CONS hx tx /\ initial_sublist xl zl ==> initial_sublist tx (TL zl)`,
   REWRITE_TAC[INITIAL_SUBLIST] THEN
     REPEAT STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     ASM_REWRITE_TAC[APPEND] THEN
     DISCH_TAC THEN
     ASM_REWRITE_TAC[TL] THEN
     MESON_TAC[]);;
   
(* Two initial sublists of the same list and of the same size are equal *)
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`,
     INDUCT_TAC THEN REPEAT STRIP_TAC THENL
     [
       ASM_MESON_TAC[LENGTH_EQ_NIL];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`xl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
     MP_TAC (ISPECL [`yl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[injectivity "list"] THEN
     CONJ_TAC THENL
     [
       ASM_MESON_TAC[INITIAL_SUBLIST_HEAD_EQ_2];
       ALL_TAC
     ] THEN

     ASM_MESON_TAC[INITIAL_SUBLIST_TAIL]);;

(* Transitivity for initial sublists *)
let INITIAL_SUBLIST_TRANS = prove(`!(xl:(A)list) yl zl. initial_sublist xl yl /\ initial_sublist yl zl ==> initial_sublist xl zl`,
   REWRITE_TAC[INITIAL_SUBLIST] THEN
     REPEAT STRIP_TAC THEN
     ASM_MESON_TAC[APPEND_ASSOC]);;

(* initial_sublist is reflexive *)	 
let INITIAL_SUBLIST_REFL = prove(`!ul. initial_sublist ul ul`, MESON_TAC[INITIAL_SUBLIST; APPEND_NIL]);;

(* An empty list is an initial sublist of any list *)
let INITIAL_SUBLIST_NIL = prove(`!zl. initial_sublist [] zl`,
   REWRITE_TAC[INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]);;

(* There exists initial sublists of all acceptable lengths *)
let INITIAL_SUBLIST_EXISTS_ALT = prove(`!n (zl:(A)list) k. LENGTH zl = n /\ k <= n ==> ?xl. initial_sublist xl zl /\ LENGTH xl = k`,
   INDUCT_TAC THEN REPEAT STRIP_TAC THENL
     [
       EXISTS_TAC `[]:(A)list` THEN
	 REWRITE_TAC[INITIAL_SUBLIST_NIL] THEN
	 POP_ASSUM MP_TAC THEN
	 SIMP_TAC[LE; LENGTH];

       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`zl:(A)list`; `n:num`] LENGTH_EQ_CONS) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     SUBGOAL_THEN `?yl:(A)list. initial_sublist yl t /\ LENGTH yl = k - 1` MP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPECL [`t:(A)list`; `k - 1`]) THEN
	 ASM_SIMP_TAC[ARITH_RULE `k <= SUC n ==> k - 1 <= n`];
       ALL_TAC
     ] THEN

     STRIP_TAC THEN
     DISJ_CASES_TAC (ARITH_RULE `k = 0 \/ 0 < k`) THENL
     [
       EXISTS_TAC `[]:(A)list` THEN
	 ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL; LENGTH];
       ALL_TAC
     ] THEN

     EXISTS_TAC `CONS (h:A) yl` THEN
     ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND; LENGTH] THEN
     CONJ_TAC THENL
     [
       REPLICATE_TAC 2 (POP_ASSUM (fun th -> ALL_TAC)) THEN
	 POP_ASSUM MP_TAC THEN
	 REWRITE_TAC[INITIAL_SUBLIST] THEN
	 MESON_TAC[];

       POP_ASSUM MP_TAC THEN
	 ARITH_TAC
     ]);;

	 
let INITIAL_SUBLIST_EXISTS = prove(`!zl k. k <= LENGTH zl ==> (?xl. initial_sublist xl zl /\ LENGTH xl = k)`,
   MESON_TAC[INITIAL_SUBLIST_EXISTS_ALT]);;

(* The length of an initial sublist does not exceed the length of the list itself *)
let INITIAL_SUBLIST_LENGTH_LE = prove(`!xl zl. initial_sublist xl zl ==> LENGTH xl <= LENGTH zl`,
   REWRITE_TAC[INITIAL_SUBLIST] THEN REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[LENGTH_APPEND] THEN
     ARITH_TAC);;

(* Structure of initial sublists of APPEND ul vl *)
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)`,
  REPEAT STRIP_TAC THEN EQ_TAC THENL
    [
      ABBREV_TAC `k = LENGTH (xl:(A)list)` THEN
	DISJ_CASES_TAC (ARITH_RULE `k:num <= LENGTH (ul:(A)list) \/ LENGTH ul < k`) THENL
	[
	  DISCH_TAC THEN
	    DISJ1_TAC THEN
	    MP_TAC (ISPECL [`ul:(A)list`; `k:num`] INITIAL_SUBLIST_EXISTS) THEN
	    ASM_REWRITE_TAC[] THEN
	    STRIP_TAC THEN
	    MP_TAC (ISPECL [`xl':(A)list`; `ul:(A)list`; `APPEND (ul:(A)list) vl`] INITIAL_SUBLIST_TRANS) THEN
	    ASM_REWRITE_TAC[INITIAL_SUBLIST_APPEND] THEN
	    ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];

	  ALL_TAC
	] THEN

	DISCH_TAC THEN
	DISJ2_TAC THEN
	SUBGOAL_THEN `?yl:(A)list. initial_sublist yl vl /\ LENGTH yl = k - LENGTH (ul:(A)list)` MP_TAC THENL
	[
	  MP_TAC (ISPECL [`vl:(A)list`; `k - LENGTH (ul:(A)list)`] INITIAL_SUBLIST_EXISTS) THEN
	    ANTS_TAC THENL
	    [
	      POP_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_LENGTH_LE th)) THEN
		ASM_REWRITE_TAC[LENGTH_APPEND] THEN
		POP_ASSUM MP_TAC THEN
		ARITH_TAC;

	      MESON_TAC[]
	    ];
	  
	  ALL_TAC
	] THEN

	STRIP_TAC THEN
	EXISTS_TAC `yl:(A)list` THEN
	ASM_REWRITE_TAC[] THEN
	SUBGOAL_THEN `initial_sublist (APPEND (ul:(A)list) yl) (APPEND ul vl) /\ LENGTH (APPEND ul yl) = k` MP_TAC THENL
	[
	  CONJ_TAC THENL
	    [
	      POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM MP_TAC THEN
		REWRITE_TAC[INITIAL_SUBLIST] THEN
		MESON_TAC[APPEND_ASSOC];
	      REWRITE_TAC[LENGTH_APPEND] THEN
		POP_ASSUM MP_TAC THEN
		POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
		POP_ASSUM MP_TAC THEN
		ARITH_TAC
	    ];

	  ALL_TAC
	] THEN

	ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];

      ALL_TAC
    ] THEN

    REPEAT STRIP_TAC THENL
    [
      ASM_MESON_TAC[INITIAL_SUBLIST_TRANS; INITIAL_SUBLIST_APPEND];
      ASM_MESON_TAC[INITIAL_SUBLIST; APPEND_ASSOC]
    ]);;   


(* Initial sublists of an one-element list *)
let INITIAL_SUBLIST_SING = prove(`!(v:A) xl. initial_sublist xl [v] <=> xl = [] \/ xl = [v]`,
  REPEAT GEN_TAC THEN EQ_TAC THENL
    [
      DISCH_TAC THEN
	FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_LENGTH_LE th)) THEN
	REWRITE_TAC[LENGTH; SYM ONE] THEN
	DISCH_TAC THEN
	DISJ_CASES_TAC (ARITH_RULE `LENGTH (xl:(A)list) = 0 \/ 1 <= LENGTH xl`) THENL
	[
	  ASM_MESON_TAC[LENGTH_EQ_NIL];
	  ALL_TAC
	] THEN
	DISJ2_TAC THEN
	MP_TAC (ISPECL [`1`; `LENGTH (xl:(A)list)`] LE_ANTISYM) THEN
	ASM_REWRITE_TAC[] THEN
	SUBGOAL_THEN `initial_sublist [v:A] [v] /\ LENGTH [v] = 1` ASSUME_TAC THENL
	[
	  REWRITE_TAC[INITIAL_SUBLIST; LENGTH; SYM ONE; APPEND] THEN MESON_TAC[];
	  ALL_TAC
	] THEN
	ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE];

      ALL_TAC
    ] THEN
    
    STRIP_TAC THENL
    [
      ASM_REWRITE_TAC[INITIAL_SUBLIST_NIL];
      ASM_REWRITE_TAC[INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]
    ]);;    

(* Initial sublists of APPEND ul [v] *)
let INITIAL_SUBLIST_APPEND_SING = prove(`!xl ul (v:A). initial_sublist xl (APPEND ul [v]) <=> initial_sublist xl ul \/ xl = APPEND ul [v]`,
   REPEAT GEN_TAC THEN
     REWRITE_TAC[INITIAL_SUBLIST_APPEND_2; INITIAL_SUBLIST_SING] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       ASM_REWRITE_TAC[];
       DISJ1_TAC THEN POP_ASSUM MP_TAC THEN
	 ASM_REWRITE_TAC[APPEND_NIL] THEN
	 SIMP_TAC[INITIAL_SUBLIST_REFL];
       ASM_REWRITE_TAC[];
       ASM_REWRITE_TAC[];
       DISJ2_TAC THEN
	 EXISTS_TAC `[v:A]` THEN
	 ASM_REWRITE_TAC[]
     ]);;	 
	 
(* (HD ul) is an initial sublist of ul *)
let INITIAL_SUBLIST_HD = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist [HD ul] ul`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `ul:(A)list` LENGTH_IMP_CONS) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[HD; INITIAL_SUBLIST; APPEND] THEN
     EXISTS_TAC `t:(A)list` THEN
     REWRITE_TAC[]);;
(* (BUTLAST ul) is an initial sublist of ul *)
let BUTLAST_INITIAL_SUBLIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist (BUTLAST ul) ul`,
   REPEAT STRIP_TAC THEN
     MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
     REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
     ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
     REWRITE_TAC[INITIAL_SUBLIST] THEN
     DISCH_TAC THEN
     EXISTS_TAC `[LAST ul:A]` THEN
     ASM_REWRITE_TAC[]);;

(**********************************************************)

(**********************************)
(* Additional properties of lists *)
(**********************************)

let LENGTH_BUTLAST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> LENGTH (BUTLAST ul) = LENGTH ul - 1`,
   REPEAT STRIP_TAC THEN
     MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
     REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
     ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM th]) THEN
     REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
     ARITH_TAC);;	 
	 
	 

let HD_IN_SET_OF_LIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> HD ul IN set_of_list ul`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[IN_SET_OF_LIST] THEN
     ONCE_REWRITE_TAC[GSYM EL] THEN
     MATCH_MP_TAC MEM_EL THEN
     POP_ASSUM MP_TAC THEN
     ARITH_TAC);;	 
	 
let HD_INITIAL_SUBLIST = prove(`!xl yl:(A)list. 1 <= LENGTH yl /\ initial_sublist yl xl ==> HD yl = HD xl`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `yl:(A)list` LENGTH_IMP_CONS) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPEC `xl:(A)list` LENGTH_IMP_CONS) THEN
     SUBGOAL_THEN `1 <= LENGTH (xl:(A)list)` (fun th -> REWRITE_TAC[th]) THENL
     [
       MATCH_MP_TAC LE_TRANS THEN
	 EXISTS_TAC `LENGTH (yl:(A)list)` THEN
	 ASM_REWRITE_TAC[] THEN
	 MATCH_MP_TAC INITIAL_SUBLIST_LENGTH_LE THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC INITIAL_SUBLIST_HEAD_EQ THEN
     MAP_EVERY EXISTS_TAC [`yl:(A)list`; `xl:(A)list`; `t':(A)list`; `t:(A)list`] THEN
     ASM_REWRITE_TAC[HD]);;	 
	 
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`,
   REWRITE_TAC[INITIAL_SUBLIST] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[SET_OF_LIST_APPEND; SUBSET_UNION]);;	 
	 
let LENGTH_REVERSE = prove(`!ul:(A)list. LENGTH (REVERSE ul) = LENGTH ul`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[REVERSE; LENGTH] THEN
     ASM_REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
     ARITH_TAC);;     

let EL_REVERSE = prove(`!(ul:(A)list) i. i < LENGTH ul ==> EL i (REVERSE ul) = EL (LENGTH ul - 1 - i) ul`,
   LIST_INDUCT_TAC THENL
     [
       REWRITE_TAC[LENGTH] THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[LENGTH; REVERSE; EL_APPEND; LENGTH_REVERSE] THEN
     REPEAT STRIP_TAC THEN
     COND_CASES_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 SUBGOAL_THEN `SUC (LENGTH t) - 1 - i = SUC (LENGTH (t:(A)list) - 1 - i)` (fun th -> REWRITE_TAC[th]) THENL
	 [
	   POP_ASSUM MP_TAC THEN 
	     ARITH_TAC;
	   ALL_TAC
	 ] THEN

	 REWRITE_TAC[EL; TL];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `LENGTH (t:(A)list) = i` (fun th -> REWRITE_TAC[th]) THENL
     [
       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN

     REWRITE_TAC[ARITH_RULE `i - i = 0`; ARITH_RULE `SUC i - 1 - i = 0`] THEN
     REWRITE_TAC[EL; HD]);;


let LENGTH_TABLE = prove(`!(f:num->A) n. LENGTH (TABLE f n) = n`,
   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE] THENL
     [
       REWRITE_TAC[LENGTH];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[GSYM TABLE; LENGTH_APPEND; LENGTH] THEN
     ARITH_TAC);;

let EL_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,
   REPEAT GEN_TAC THEN SPEC_TAC (`n:num`, `n:num`) THEN
     INDUCT_TAC THENL [ ARITH_TAC; ALL_TAC ] THEN
     REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE; EL_APPEND] THEN
     REWRITE_TAC[GSYM TABLE; LENGTH_TABLE] THEN
     DISCH_TAC THEN COND_CASES_TAC THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `i = n:num` (fun th -> REWRITE_TAC[th]) THENL
     [
       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[ARITH_RULE `n - n = 0`; EL; HD]);;   


let LENGTH_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p. LENGTH (left_action_list p ul) = LENGTH ul`,
   REWRITE_TAC[left_action_list; LENGTH_TABLE]);;


let EL_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p i. p permutes (0..LENGTH ul - 1) /\ i < LENGTH ul
				  ==> EL i ul = EL (p i) (left_action_list p ul)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[left_action_list] THEN
     ABBREV_TAC `n = LENGTH (ul:(A)list)` THEN
     SUBGOAL_THEN `(p:num->num) i < n` ASSUME_TAC THENL
     [
       MP_TAC (ISPECL [`p:num->num`; `0..n - 1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
	 ASM_REWRITE_TAC[IN_NUMSEG] THEN
	 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
	 ASM_REWRITE_TAC[ARITH_RULE `0 <= i`] THEN
	 ASM_SIMP_TAC[ARITH_RULE `i < n ==> i <= n - 1`] THEN
	 UNDISCH_TAC `i < n:num` THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[EL_TABLE] THEN
     AP_THM_TAC THEN AP_TERM_TAC THEN
     MP_TAC (ISPECL [`p:num->num`; `0..n-1`] PERMUTES_INVERSES) THEN
     ASM_REWRITE_TAC[] THEN
     SIMP_TAC[]);;	 
	 
let MEM_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p x. p permutes (0..LENGTH ul - 1) 
				   ==> (MEM x (left_action_list p ul) <=> MEM x ul)`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `n = LENGTH (ul:(A)list)` THEN
     ASM_REWRITE_TAC[MEM_EXISTS_EL; LENGTH_LEFT_ACTION_LIST] THEN
     EQ_TAC THENL
     [
       STRIP_TAC THEN
	 POP_ASSUM MP_TAC THEN
	 ASM_SIMP_TAC[left_action_list; EL_TABLE] THEN
	 DISCH_TAC THEN
	 EXISTS_TAC `inverse (p:num->num) i` THEN
	 REWRITE_TAC[] THEN
	 MP_TAC (ISPECL [`p:num->num`; `0..n-1`] PERMUTES_INVERSE) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 MP_TAC (ISPECL [`inverse (p:num->num)`; `0..n-1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
	 ASM_REWRITE_TAC[] THEN
	 DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
	 ASM_SIMP_TAC[IN_NUMSEG; ARITH_RULE `i < n ==> i <= n - 1`; LE_0] THEN
	 UNDISCH_TAC `i < n:num` THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     EXISTS_TAC `(p:num->num) i` THEN
     MP_TAC (SPEC_ALL EL_LEFT_ACTION_LIST) THEN
     ASM_SIMP_TAC[] THEN DISCH_TAC THEN
     MP_TAC (ISPECL [`p:num->num`; `0..n-1`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
     ASM_REWRITE_TAC[IN_NUMSEG] THEN DISCH_THEN (MP_TAC o SPEC `i:num`) THEN
     UNDISCH_TAC `i < n:num` THEN
     ARITH_TAC);;	 
	 
let SET_OF_LIST_LEFT_ACTION_LIST = prove(`!(ul:(A)list) p. p permutes 0..LENGTH ul - 1
					   ==> set_of_list (left_action_list p ul) = set_of_list ul`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[EXTENSION; IN_SET_OF_LIST] THEN
     ASM_SIMP_TAC[MEM_LEFT_ACTION_LIST]);;	 
	 

let CARD_SET_OF_LIST_EQ_LENGTH_IMP_ALL_DISTINCT = prove(`!ul:(A)list. CARD (set_of_list ul) = LENGTH ul
                               ==> (!i j. i < LENGTH ul /\ j < LENGTH ul /\ ~(i = j) ==> ~(EL i ul = EL j ul))`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[set_of_list; LENGTH; CARD_CLAUSES; ARITH_RULE `~(j < 0)`] THEN
     SIMP_TAC[CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
     COND_CASES_TAC THENL
     [
       MP_TAC (ISPEC `t:(A)list` CARD_SET_OF_LIST_LE) THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN

     REWRITE_TAC[ARITH_RULE `SUC n = SUC m <=> n = m`] THEN
     DISCH_THEN (fun th -> FIRST_X_ASSUM (ASSUME_TAC o (fun th2 -> MATCH_MP th2 th))) THEN
     REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN

     MP_TAC (SPEC `i:num` num_CASES) THEN STRIP_TAC THENL
     [
       ASM_REWRITE_TAC[EL; HD] THEN
	 MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
	 [
	   UNDISCH_TAC `~(i = j:num)` THEN ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN

	 ASM_REWRITE_TAC[EL; TL] THEN
	 DISCH_TAC THEN UNDISCH_TAC `~(h:A IN set_of_list t)` THEN
	 ASM_REWRITE_TAC[IN_SET_OF_LIST] THEN
	 MATCH_MP_TAC (ISPECL [`t:(A)list`; `n:num`] MEM_EL) THEN
	 UNDISCH_TAC `j = SUC n` THEN UNDISCH_TAC `j < SUC (LENGTH (t:(A)list))` THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[EL; TL] THEN
     MP_TAC (SPEC `j:num` num_CASES) THEN STRIP_TAC THENL
     [
       ASM_REWRITE_TAC[EL; HD] THEN
	 DISCH_THEN (ASSUME_TAC o SYM) THEN UNDISCH_TAC `~(h:A IN set_of_list t)` THEN
	 ASM_REWRITE_TAC[IN_SET_OF_LIST] THEN
	 MATCH_MP_TAC (ISPECL [`t:(A)list`; `n:num`] MEM_EL) THEN
	 UNDISCH_TAC `i = SUC n` THEN UNDISCH_TAC `i < SUC (LENGTH (t:(A)list))` THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[EL; TL] THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN
     ARITH_TAC);;	 
	 
let LENGTH_DROP = prove(`!i ul:(A)list. i < LENGTH ul ==> LENGTH (DROP ul i) = LENGTH ul - 1`,
   INDUCT_TAC THENL
     [
       GEN_TAC THEN
	 REWRITE_TAC[DROP] THEN DISCH_TAC THEN
	 MATCH_MP_TAC LENGTH_TL THEN
	 ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN

     REPEAT STRIP_TAC THEN
     REWRITE_TAC[DROP; LENGTH] THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `TL ul:(A)list`) THEN
     SUBGOAL_THEN `LENGTH (TL ul) = LENGTH (ul:(A)list) - 1` ASSUME_TAC THENL
     [
       MATCH_MP_TAC LENGTH_TL THEN
	 ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN

     ANTS_TAC THENL
     [
       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
     ARITH_TAC);;


let EL_DROP = prove(`!i j ul:(A)list. i < LENGTH ul /\ j < LENGTH ul - 1 ==> 
		      EL j (DROP ul i) = if (j < i) then EL j ul else EL (j + 1) ul`,
   INDUCT_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THEN REWRITE_TAC[DROP; EL; LT_REFL; ARITH_RULE `0 + 1 = SUC 0`] THENL
     [
       REWRITE_TAC[ARITH_RULE `~(x < 0)`; ARITH_RULE `SUC j + 1 = SUC (SUC j)`; EL];
       REWRITE_TAC[ARITH_RULE `0 < SUC i`; HD];
       ALL_TAC
     ] THEN

     REWRITE_TAC[ARITH_RULE `SUC j + 1 = SUC (SUC j)`; ARITH_RULE `SUC j < SUC i <=> j < i`; TL; EL] THEN
     FIRST_X_ASSUM (MP_TAC o SPECL [`j:num`; `TL ul:(A)list`]) THEN
     SUBGOAL_THEN `LENGTH (TL ul:(A)list) = LENGTH ul - 1` ASSUME_TAC THENL
     [
       MATCH_MP_TAC LENGTH_TL THEN
	 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[ARITH_RULE `j + 1 = SUC j`; EL] THEN
     DISCH_THEN MATCH_MP_TAC THEN
     REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     ARITH_TAC);;	 
	 
let LIST_EL_EQ = prove(`!ul vl:(A)list. ul = vl <=> 
               (LENGTH ul = LENGTH vl /\ (!j. j < LENGTH ul ==> EL j ul = EL j vl))`,
   REPEAT STRIP_TAC THEN
     EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     SPEC_TAC (`vl:(A)list`, `vl:(A)list`) THEN SPEC_TAC (`ul:(A)list`, `ul:(A)list`) THEN
     LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN SIMP_TAC[LENGTH_EQ_NIL; EQ_SYM_EQ; LENGTH; ARITH_RULE `~(0 = SUC a)`] THEN
     REMOVE_ASSUM THEN
     REWRITE_TAC[ARITH_RULE `SUC a = SUC b <=> a = b`] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     ANTS_TAC THENL
     [
       REPEAT STRIP_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o SPEC `SUC j`) THEN
	 ASM_REWRITE_TAC[ARITH_RULE `SUC a < SUC b <=> a < b`; EL; TL];
       ALL_TAC
     ] THEN
     DISCH_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
     ASM_SIMP_TAC[ARITH_RULE `0 < SUC a`; EL; HD]);;	 
	 
let LEFT_ACTION_LIST_I = prove(`!ul:(A)list. left_action_list I ul = ul`,
   ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN   
     GEN_TAC THEN REWRITE_TAC[LIST_EL_EQ] THEN
     ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
     ASM_REWRITE_TAC[LENGTH_LEFT_ACTION_LIST] THEN
     REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[left_action_list; EL_TABLE; INVERSE_I; I_THM]);;

	 
	 
let SET_OF_LIST_DELETE_SUBSET_DROP = prove(`!j ul:(A)list. j < LENGTH ul ==>
					     set_of_list ul DELETE (EL j ul) SUBSET set_of_list (DROP ul j)`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
     ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_DELETE; MEM_EXISTS_EL] THEN
     REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`j:num`; `ul:(A)list`] LENGTH_DROP) THEN
     ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     ASM_CASES_TAC `i:num < j` THENL
     [
       EXISTS_TAC `i:num` THEN
	 MP_TAC (ARITH_RULE `i < j /\ j < k ==> i < k - 1`) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 ASM_REWRITE_TAC[] THEN
	 MP_TAC (ISPECL [`j:num`; `i:num`; `ul:(A)list`] EL_DROP) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     EXISTS_TAC `i - 1` THEN
     POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LT; LE_LT] THEN
     STRIP_TAC THENL
     [
       MP_TAC (ARITH_RULE `j < k /\ i < k /\ j < i ==> i - 1 < k - 1`) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 ASM_REWRITE_TAC[] THEN
	 MP_TAC (ISPECL [`j:num`; `i - 1`; `ul:(A)list`] EL_DROP) THEN
	 ASM_SIMP_TAC[ARITH_RULE `j < i ==> ~(i - 1 < j)`] THEN
	 MP_TAC (ARITH_RULE `j < i ==> i - 1 + 1 = i`) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN

     UNDISCH_TAC `x:A = EL i ul` THEN
     POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;     



let SET_OF_LIST_DELETE_EQ_DROP = prove(`!j ul:(A)list. CARD (set_of_list ul) = LENGTH ul /\ j < LENGTH ul
    ==> set_of_list ul DELETE (EL j ul) = set_of_list (DROP ul j)`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUBSET_ANTISYM THEN
     ASM_SIMP_TAC[SET_OF_LIST_DELETE_SUBSET_DROP] THEN
     ABBREV_TAC `k = LENGTH (ul:(A)list)` THEN
     MP_TAC (SPECL [`j:num`; `ul:(A)list`] LENGTH_DROP) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_DELETE; MEM_EXISTS_EL] THEN
     GEN_TAC THEN STRIP_TAC THEN
     POP_ASSUM (ASSUME_TAC o SYM) THEN
     MP_TAC (SPECL [`j:num`; `i:num`; `ul:(A)list`] EL_DROP) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (ARITH_RULE `i < k - 1 ==> i < k`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN

     MP_TAC (SPEC `ul:(A)list` CARD_SET_OF_LIST_EQ_LENGTH_IMP_ALL_DISTINCT) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN

     COND_CASES_TAC THENL
     [
       DISCH_TAC THEN
	 CONJ_TAC THENL
	 [
	   EXISTS_TAC `i:num` THEN
	     ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN
	 ASM_REWRITE_TAC[] THEN
	 FIRST_X_ASSUM MATCH_MP_TAC THEN
	 ASM_SIMP_TAC[ARITH_RULE `i < j ==> ~(i = j:num)`];
       ALL_TAC
     ] THEN

     DISCH_TAC THEN
     CONJ_TAC THENL
     [
       EXISTS_TAC `i + 1` THEN
	 ASM_SIMP_TAC[ARITH_RULE `i < k - 1 ==> i + 1 < k`];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     ASM_SIMP_TAC[ARITH_RULE `i < k - 1 ==> i + 1 < k`] THEN
     UNDISCH_TAC `~(i < j:num)` THEN ARITH_TAC);;

	 
	 

(**********************************************************)

(*****************************************)
(* Properties of barV                    *)
(*****************************************)

(* barV(k) SUBSET V *)
let BARV_SUBSET = prove(`!V k ul. barV V k ul ==> set_of_list ul SUBSET V`,
			REPEAT GEN_TAC THEN
			  REWRITE_TAC[BARV; VORONOI_NONDG; INITIAL_SUBLIST] THEN
			  STRIP_TAC THEN
			  POP_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
			  ANTS_TAC THENL
			  [
			    ASM_REWRITE_TAC[ARITH_RULE `0 < k + 1`] THEN
			      EXISTS_TAC `[]:(real^3)list` THEN
			      REWRITE_TAC[APPEND_NIL];
			    SIMP_TAC[]
			  ]);;


(* barV(k) = (h:t) for some h, t *)
let BARV_CONS = prove(`!V k ul. barV V k ul ==> ?h t. ul = CONS h t /\ h = HD ul`,
		      REPEAT GEN_TAC THEN
			REWRITE_TAC[BARV] THEN
			DISCH_THEN (MP_TAC o CONJUNCT1) THEN
			REWRITE_TAC[GSYM ADD1; LENGTH_EQ_CONS] THEN
			ASM_MESON_TAC[HD]);;


(* An initial sublist of barV(k) is barV(length - 1) *)
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`,
   REWRITE_TAC[BARV] THEN
     REPEAT STRIP_TAC THENL
     [
       ASM_SIMP_TAC[ARITH_RULE `0 < a ==> a - 1 + 1 = a`];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`vl':(real^3)list`; `vl:(real^3)list`; `ul:(real^3)list`] INITIAL_SUBLIST_TRANS) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `vl':(real^3)list`) THEN
     ASM_SIMP_TAC[]);;	 

(* barV V 0 [v] (if v IN V) *)
let BARV_0 = prove(`!V v. packing V /\ v IN V ==> barV V 0 [v]`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[BARV; VORONOI_NONDG; LENGTH; ARITH] THEN
     REWRITE_TAC[INITIAL_SUBLIST_SING] THEN
     GEN_TAC THEN
     STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
     ASM_SIMP_TAC[set_of_list; SUBSET; IN_SING] THEN
     ASM_REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET; IN_SING; SING_GSPEC_APP; INTERS_1] THEN
     ASM_SIMP_TAC[AFF_DIM_VORONOI_CLOSED] THEN
     INT_ARITH_TAC);;	 
	 
(* ul IN barV V k ==> k <= 3 *)
let BARV_IMP_K_LE_3 = prove(`!V ul k. barV V k ul ==> k <= 3`,
   REWRITE_TAC[BARV; VORONOI_NONDG] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
     ASM_REWRITE_TAC[INITIAL_SUBLIST_REFL; ARITH_RULE `0 < k + 1`] THEN
     ARITH_TAC);;	 

(* ul IN barV V k ul ==> HD ul IN set_of_list ul *)
let BARV_IMP_HD_IN_SET_OF_LIST = prove(`!V k ul. barV V k ul ==> HD ul IN set_of_list ul`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC HD_IN_SET_OF_LIST THEN
     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[BARV] THEN
     ARITH_TAC);;	 



(* Lemma for truncate_simplex operation *)
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`,
  REPEAT GEN_TAC THEN EQ_TAC THENL
    [
      REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
	STRIP_TAC THEN
	POP_ASSUM (MP_TAC o (fun th -> MATCH_MP INITIAL_SUBLIST_EXISTS th)) THEN
	ASM_MESON_TAC[];
      STRIP_TAC THEN
	MP_TAC (ISPECL [`xl:(A)list`; `zl:(A)list`] INITIAL_SUBLIST_LENGTH_LE) THEN
	ASM_SIMP_TAC[] THEN
	DISCH_TAC THEN
	REWRITE_TAC[TRUNCATE_SIMPLEX] THEN
	ASM_MESON_TAC[INITIAL_SUBLIST_UNIQUE]
    ]);;


let TRUNCATE_SIMPLEX_BARV = prove(`!V r k zl. barV V k zl /\ r <= k ==> barV V r (truncate_simplex r zl)`,
   REPEAT STRIP_TAC THEN
     SUBGOAL_TAC "A" `LENGTH (zl:(real^3)list) = k + 1` [ ASM_MESON_TAC[BARV] ] THEN
     ABBREV_TAC `xl:(real^3)list = truncate_simplex r zl` THEN
     SUBGOAL_THEN `initial_sublist xl (zl:(real^3)list) /\ LENGTH xl = r + 1` STRIP_ASSUME_TAC THENL
     [
       REWRITE_TAC[GSYM TRUNCATE_SIMPLEX_INITIAL_SUBLIST] THEN
	 ASM_SIMP_TAC[ARITH_RULE `r <= k ==> r + 1 <= k + 1`];
       ALL_TAC
     ] THEN
     MP_TAC (ISPECL [`V:real^3->bool`; `k:num`; `zl:(real^3)list`; `xl:(real^3)list`] BARV_INITIAL_SUBLIST) THEN
     ASM_SIMP_TAC[ARITH_RULE `0 < r + 1`; ARITH_RULE `(r + 1) - 1 = r`]);;	 
	 
	 
let TRUNCATE_SIMPLEX_REFL = prove(`!k ul:(A)list. LENGTH ul = k + 1 ==> truncate_simplex k ul = ul`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`k:num`; `ul:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_REWRITE_TAC[LE_REFL; INITIAL_SUBLIST_REFL]);;	 
	 

let TRUNCATE_0_EQ_HEAD = prove(`!ul:(A)list. 1 <= LENGTH ul ==> truncate_simplex 0 ul = [HD ul]`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`0`; `[HD ul]:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_REWRITE_TAC[ARITH] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     ASM_SIMP_TAC[INITIAL_SUBLIST_HD; LENGTH; ARITH]);;	 

let LENGTH_TRUNCATE_SIMPLEX = prove(`!k ul:(A)list. k + 1 <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = k + 1`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`k:num`; `truncate_simplex k ul:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_SIMP_TAC[]);;
	 
	 
let TRUNCATE_SIMPLEX_EQ_BUTLAST = prove(`!ul:(A)list. 2 <= LENGTH ul ==> truncate_simplex (LENGTH ul - 2) ul = BUTLAST ul`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`LENGTH (ul:(A)list) - 2`; `BUTLAST (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_SIMP_TAC[ARITH_RULE `2 <= a ==> a - 2 + 1 = a - 1 /\ a - 1 <= a`] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     ASM_SIMP_TAC[ARITH_RULE `2 <= a ==> 1 <= a`; BUTLAST_INITIAL_SUBLIST; LENGTH_BUTLAST]);;	 
	 
let HD_TRUNCATE_SIMPLEX = prove(`!(ul:(A)list) j. j + 1 <= LENGTH ul ==> HD (truncate_simplex j ul) = HD ul`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`j:num`; `truncate_simplex j (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     MATCH_MP_TAC HD_INITIAL_SUBLIST THEN
     ASM_REWRITE_TAC[ARITH_RULE `1 <= j + 1`]);;	 
	 
let TRUNCATE_TRUNCATE_SIMPLEX = prove(`!(ul:(A)list) i j. i <= j /\ j + 1 <= LENGTH ul ==> 
					truncate_simplex i (truncate_simplex j ul) = truncate_simplex i ul`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `xl = truncate_simplex j (ul:(A)list)` THEN
     SUBGOAL_THEN `i + 1 <= LENGTH (xl:(A)list) /\ i + 1 <= LENGTH (ul:(A)list) /\ initial_sublist (xl:(A)list) ul` STRIP_ASSUME_TAC THENL
     [
       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
	 MP_TAC (SPECL [`j:num`; `truncate_simplex j (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
	 ASM_SIMP_TAC[] THEN
	 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN
     MP_TAC (SPECL [`i:num`; `truncate_simplex i (xl:(A)list)`; `xl:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     MP_TAC (SPECL [`i:num`; `truncate_simplex i (ul:(A)list)`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC INITIAL_SUBLIST_UNIQUE THEN
     MAP_EVERY EXISTS_TAC [`i + 1`; `ul:(A)list`] THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC INITIAL_SUBLIST_TRANS THEN
     EXISTS_TAC `xl:(A)list` THEN
     ASM_REWRITE_TAC[]);;	 
	 
let INITIAL_SUBLIST_IMP_TRUNCATE_SIMPLEX = prove(`!xl yl:(A)list. initial_sublist yl xl /\ 1 <= LENGTH yl ==>
						                 yl = truncate_simplex (LENGTH yl - 1) xl /\ LENGTH yl <= LENGTH xl`,
   REPEAT STRIP_TAC THENL
     [
       MP_TAC (SPECL [`LENGTH (yl:(A)list) - 1`; `yl:(A)list`; `xl:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
	 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
	 SUBGOAL_THEN `LENGTH yl = LENGTH (yl:(A)list) - 1 + 1` MP_TAC THENL
	 [
	   UNDISCH_TAC `1 <= LENGTH (yl:(A)list)` THEN ARITH_TAC;
	   ALL_TAC
	 ] THEN
	 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
	 SIMP_TAC[];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[INITIAL_SUBLIST_LENGTH_LE]);;	 
	 
let LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST = prove(`!ul:(A)list. 2 <= LENGTH ul ==>
						   ul = APPEND (truncate_simplex (LENGTH ul - 2) ul) [LAST ul]`,
   ASM_SIMP_TAC[TRUNCATE_SIMPLEX_EQ_BUTLAST] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC (GSYM APPEND_BUTLAST_LAST) THEN
     REWRITE_TAC[EQ_SYM_EQ; GSYM LENGTH_EQ_NIL] THEN
     POP_ASSUM MP_TAC THEN ARITH_TAC);;	 
	 
let TRUNCATE_SIMPLEX_ADD1 = prove(`!(ul:(A)list) k. k + 2 <= LENGTH ul ==> 
				    truncate_simplex (k + 1) ul = APPEND (truncate_simplex k ul) [LAST (truncate_simplex (k + 1) ul)]`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `xl:(A)list = truncate_simplex (k + 1) ul` THEN
     SUBGOAL_THEN `truncate_simplex k ul = truncate_simplex k xl:(A)list` (fun th -> REWRITE_TAC[th]) THENL
     [
       EXPAND_TAC "xl" THEN
	 MATCH_MP_TAC (GSYM TRUNCATE_TRUNCATE_SIMPLEX) THEN
	 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `LENGTH (xl:(A)list) = k + 2` ASSUME_TAC THENL
     [
       EXPAND_TAC "xl" THEN
	 REWRITE_TAC[ARITH_RULE `k + 2 = (k + 1) + 1`] THEN
	 MATCH_MP_TAC LENGTH_TRUNCATE_SIMPLEX THEN
	 ASM_REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 2`];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `k = LENGTH (xl:(A)list) - 2` (fun th -> REWRITE_TAC[th]) THENL
     [
       POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN

     MATCH_MP_TAC LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST THEN
     POP_ASSUM MP_TAC THEN ARITH_TAC);;	 
	 

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`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `vl:(A)list = truncate_simplex k ul` THEN
     SUBGOAL_THEN `?yl:(A)list. ul = APPEND vl yl /\ LENGTH vl = k + 1` CHOOSE_TAC THENL
     [
       MP_TAC (SPECL [`k:num`; `vl:(A)list`; `ul:(A)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
	 ASM_REWRITE_TAC[INITIAL_SUBLIST] THEN
	 STRIP_TAC THEN
	 EXISTS_TAC `yl:(A)list` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `j < k + 1 <=> j <= k`]);;	 
	 

let TRUNCATE_SIMPLEX_ADD1_ALT = prove(`!ul:(A)list k. k + 2 <= LENGTH ul
					==> truncate_simplex (k + 1) ul = APPEND (truncate_simplex k ul) [EL (k + 1) ul]`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL TRUNCATE_SIMPLEX_ADD1) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     AP_TERM_TAC THEN

     MP_TAC (SPECL [`k + 1`; `ul:(A)list`] LENGTH_TRUNCATE_SIMPLEX) THEN
     ASM_SIMP_TAC[ARITH_RULE `k + 2 <= a ==> (k + 1) + 1 <= a`] THEN
     DISCH_TAC THEN
					   
     MP_TAC (ISPEC `(truncate_simplex (k + 1) ul:(A)list)` LAST_EL) THEN
     ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL; ARITH_RULE `~(a + 1 = 0)`; ARITH_RULE `(a + 1) - 1 = a`] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     MP_TAC (SPECL [`ul:(A)list`; `k + 1`; `k + 1`] EL_TRUNCATE_SIMPLEX) THEN
     ASM_SIMP_TAC[ARITH_RULE `k + 2 <= a ==> (k + 1) + 1 <= a`; LE_REFL]);;


(****************************************************)
	 
(***************************************************************************)
(* Properties of voronoi_set (Omega(V, W)) and voronoi_list (Omega(V, vl)) *)
(***************************************************************************)


(* Equivalent definitions for intersections of one and two Voronoi cells *)
let VORONOI_SET_SING = prove(`!V (u:real^3). voronoi_set V {u} = voronoi_closed V u`,
			     REWRITE_TAC[VORONOI_SET; IN_SING; EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
			       MESON_TAC[]);;

let VORONOI_LIST_SING = prove(`!V (u:real^3). voronoi_list V [u] = voronoi_closed V u`,
			      REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET_SING]);;

(* Omega(V, v) INTER Omega(V, u) *)
let VORONOI_SET_2 = prove(`!V (u:real^3) v. voronoi_set V {u, v} = voronoi_closed V v INTER voronoi_closed V u`,
		       REWRITE_TAC[VORONOI_SET; INTERS_2_LEMMA; INTER_COMM]);;

(* Omega(V, v) INTER A(u, v) *)
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`,
   REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
     REWRITE_TAC[VORONOI_SET_2; bis; voronoi_closed; EXTENSION; IN_INTER; IN_ELIM_THM] THEN
     REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
     ASM_MESON_TAC[REAL_ARITH `a <= b /\ b <= a ==> a = b`]);;
     
(* Omega(V, v) INTER A+(u, v) *)
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`,
   REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
     REWRITE_TAC[VORONOI_SET_2; bis_le; voronoi_closed; EXTENSION; IN_INTER; IN_ELIM_THM] THEN
     REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
     ASM_MESON_TAC[REAL_LE_TRANS]);;

(* The result for lists of arbitrary length *)
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})`,
   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `V (h:real^3) /\ (!u. u IN set_of_list t ==> V u)` ASSUME_TAC THENL
     [
       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 DISCH_THEN (LABEL_TAC "A") THEN DISCH_TAC THEN
	 REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[] THEN
	 REWRITE_TAC[set_of_list] THEN
	 SET_TAC[];
       ALL_TAC
     ] THEN

     REWRITE_TAC[VORONOI_LIST; VORONOI_SET; bis; EXTENSION; IN_INTER; IN_INTERS; IN_ELIM_THM] THEN
     X_GEN_TAC `y:real^3` THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V (h:real^3)`) THEN
	 ASM_REWRITE_TAC[set_of_list] THEN
	 ANTS_TAC THEN REWRITE_TAC[] THEN
	 EXISTS_TAC `h:real^3` THEN
	 REWRITE_TAC[COMPONENT];

       ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> ALL_TAC) THEN
	 SUBGOAL_THEN `y:real^3 IN voronoi_closed V h` ASSUME_TAC THENL
	 [
	   POP_ASSUM (fun th -> ALL_TAC) THEN
	     POP_ASSUM (MP_TAC o SPEC `voronoi_closed V (h:real^3)`) THEN
	     ANTS_TAC THEN REWRITE_TAC[] THEN
	     EXISTS_TAC `h:real^3` THEN
	     ASM_REWRITE_TAC[set_of_list; COMPONENT];
	   ALL_TAC
	 ] THEN

	 SUBGOAL_THEN `y:real^3 IN voronoi_closed V u` ASSUME_TAC THENL
	 [
	   FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V (u:real^3)` o check (is_forall o concl)) THEN
	     ANTS_TAC THEN REWRITE_TAC[] THEN
	     EXISTS_TAC `u:real^3` THEN
	     ASM_REWRITE_TAC[set_of_list; IN_INSERT];
	   ALL_TAC
	 ] THEN

	 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN
	 DISCH_THEN (ASSUME_TAC o SPEC `u:real^3`) THEN
	 DISCH_THEN (ASSUME_TAC o SPEC `h:real^3`) THEN
	 ASM_MESON_TAC[REAL_ARITH `a <= b /\ b <= a ==> a = b`];


       ASM_REWRITE_TAC[voronoi_closed; IN_ELIM_THM] THEN GEN_TAC THEN
	 POP_ASSUM (fun th -> ALL_TAC) THEN
	 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_list; IN_INSERT] THEN
	 POP_ASSUM (MP_TAC o SPEC `bis h (v:real^3)`) THEN
	 POP_ASSUM MP_TAC THEN REWRITE_TAC[bis; voronoi_closed; IN_ELIM_THM] THEN
	 REPEAT STRIP_TAC THENL
	 [
	   ASM_MESON_TAC[];
	   ALL_TAC
	 ] THEN

	 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
	 ANTS_TAC THENL
	 [
	   EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[];
	   ALL_TAC
	 ] THEN

	 ASM_MESON_TAC[]
     ]);;     



(* Used below *)
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`,
 REWRITE_TAC[voronoi_closed; bis; bis_le; IN] THEN
   REPEAT STRIP_TAC THEN
   REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN
   ASM_MESON_TAC[REAL_EQ_IMP_LE; REAL_LE_ANTISYM]);;


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)`,
 REPEAT GEN_TAC THEN
   STRIP_TAC THEN
   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
   DISCH_THEN (LABEL_TAC "A") THEN
   DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN
   ASM_REWRITE_TAC[set_of_list; INSERT_SUBSET] THEN
   SET_TAC[]);;


(* Omega(V,h:t) = Omega(V,h) INTER INTERS {A+(u, h) | u IN t} *)
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})`,
 REPEAT GEN_TAC THEN
   DISCH_TAC THEN
   MP_TAC (ISPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] LIST_SUBSET) THEN
   FIRST_ASSUM ((fun th -> REWRITE_TAC[th]) o (fun th -> MATCH_MP VORONOI_LIST_BIS th)) THEN
   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
   DISJ_CASES_TAC (TAUT `set_of_list (t:(real^3)list) = {} \/ ~(set_of_list t = {})`) THENL
   [
     ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN SET_TAC[];
     ALL_TAC
   ] THEN
   ASM_SIMP_TAC[INTER_INTERS] THEN
   REWRITE_TAC[EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
   ASM_MESON_TAC[BIS_SYM; VORONOI_INTER_BIS_EQ_INTER_BIS_LE]);;



(* Voronoi list is bounded *)
let BOUNDED_VORONOI_LIST = prove(`!V k ul. saturated V /\ barV V k ul ==> bounded (voronoi_list V ul)`,
  REPEAT STRIP_TAC THEN
    FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP BARV_SUBSET th)) THEN
    FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP BARV_CONS th)) THEN
    STRIP_TAC THEN POP_ASSUM (fun th -> ALL_TAC) THEN
    DISCH_TAC THEN
    MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS_LE) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    MATCH_MP_TAC BOUNDED_INTER THEN
    DISJ1_TAC THEN
    ASM_SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;


(* Omega(V, h:t) INTER A(h, v) = Omega(V, (h:t) ++ [v]) *)   
let VORONOI_LIST_INTER_BIS = prove(`!V ul v h t. set_of_list ul SUBSET V /\ v IN V /\ ul = CONS h t ==>
    (voronoi_list V ul) INTER (bis h v) = voronoi_list V (APPEND ul [v])`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     REWRITE_TAC[APPEND] THEN
     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
     SUBGOAL_THEN `set_of_list (CONS (h:real^3) (APPEND t [v])) SUBSET V` (fun th -> REWRITE_TAC[th]) THENL
     [
       REWRITE_TAC[GSYM APPEND] THEN
	 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
	 REWRITE_TAC[SUBSET; IN_SET_OF_LIST; MEM_APPEND; MEM] THEN
	 REPEAT STRIP_TAC THENL
	 [
	   ASM_MESON_TAC[SUBSET; IN_SET_OF_LIST];
	   ASM_MESON_TAC[]
	 ];

       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     REWRITE_TAC[IN_SET_OF_LIST; MEM_APPEND; MEM] THEN
     SET_TAC[]);;
   
   
(* Canonical representations of Omega(V, vl) as a polyhedron *)


let SUPSET_INTER = prove(`!s t u. s SUBSET t /\ s = u ==> s = t INTER u`, SET_TAC[]);;

let INTER_AFFINE_HULL = prove(`!(s:real^N->bool). s = affine hull s INTER s`,
			      GEN_TAC THEN MATCH_MP_TAC SUPSET_INTER THEN
				MESON_TAC[CLOSURE_SUBSET; CLOSURE_SUBSET_AFFINE_HULL; SUBSET_TRANS]);;			      


(* "Almost canonical" polyhedron representation for Omega(V, ul) *)

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 
    ==> ?K. FINITE K /\ voronoi_list V ul = INTERS K /\ 
	(!a. a IN K ==> (?v. v IN V /\ (a = bis_le v h \/ a = bis_le h v)))`,
  REPEAT GEN_TAC THEN
    DISCH_TAC THEN
    MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] VORONOI_LIST_BIS_LE) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    MP_TAC (ISPECL [`V:real^3->bool`; `ul:(real^3)list`; `h:real^3`; `t:(real^3)list`] LIST_SUBSET) THEN
    ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
    MP_TAC (SPECL [`V:real^3->bool`; `h:real^3`] VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE) THEN
    ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
    POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
    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
    REPEAT STRIP_TAC THENL
    [
      REWRITE_TAC[FINITE_UNION] THEN
	REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
	CONJ_TAC THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[FINITE_SET_OF_LIST];
      
      REWRITE_TAC[INTERS_INTER_INTERS];

      ASM SET_TAC[]
    ]);;


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 
    ==> ?K. FINITE K /\ voronoi_list V ul = affine hull (voronoi_list V ul) INTER INTERS K /\ 
	(!a. a IN K ==> (?v. v IN V /\ ~(v = h) /\ (a = bis_le v h \/ a = bis_le h v)))`,
  REPEAT GEN_TAC THEN
    DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL_0 th)) THEN
    STRIP_TAC THEN
    EXISTS_TAC `K DELETE (:real^3)` THEN
    ASM_REWRITE_TAC[FINITE_DELETE; GSYM INTERS_UNIV; IN_DELETE] THEN
    REWRITE_TAC[INTER_AFFINE_HULL] THEN
    REPEAT STRIP_TAC THEN
    FIRST_X_ASSUM (MP_TAC o SPEC `a:real^3->bool`) THEN 
    ASM_REWRITE_TAC[] THEN 
    DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN
    EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[] THEN
    DISJ_CASES_TAC (TAUT `~(v:real^3 = h) \/ (v = h)`) THEN ASM_REWRITE_TAC[] THEN
    FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
    ASM_REWRITE_TAC[bis_le; REAL_LE_REFL] THEN
    ASM SET_TAC[]);;    
    
    


(* For a canonical polyhedron representation we need to find a minimal intersection *)    
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]);;
(* Lemma about minimal intersection *)
(* The proof is a modification of the proof of POLYHEDRON_INTER_AFFINE_MINIMAL *)
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'))`,
 REPEAT GEN_TAC THEN
   DISCH_THEN (MP_TAC o (fun th -> MATCH_MP lemma1 th)) THEN
   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
   DISCH_THEN(X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
   MATCH_MP_TAC MONO_EXISTS THEN 
   SIMP_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
   X_GEN_TAC `g:(A->bool)->bool` THEN STRIP_TAC THEN
   X_GEN_TAC `g':(A->bool)->bool` THEN DISCH_TAC THEN
   FIRST_X_ASSUM(MP_TAC o SPEC `CARD(g':(A->bool)->bool)`) THEN
   ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET]; ALL_TAC] THEN
   REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN
   DISCH_THEN(MP_TAC o SPEC `g':(A->bool)->bool`) THEN
   MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
   CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; SUBSET_TRANS]; ALL_TAC] THEN
   CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET]; ALL_TAC] THEN
   ASM_REWRITE_TAC[] THEN
   MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN
   FIRST_X_ASSUM MP_TAC THEN
   SET_TAC[]);;


(* Variation of the previous lemma: the proof is exactly the same *)
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'))`,
 REPEAT GEN_TAC THEN
   DISCH_THEN (MP_TAC o (fun th -> MATCH_MP lemma1 th)) THEN
   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
   DISCH_THEN(X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
   MATCH_MP_TAC MONO_EXISTS THEN 
   SIMP_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
   X_GEN_TAC `g:(A->bool)->bool` THEN STRIP_TAC THEN
   X_GEN_TAC `g':(A->bool)->bool` THEN DISCH_TAC THEN
   FIRST_X_ASSUM(MP_TAC o SPEC `CARD(g':(A->bool)->bool)`) THEN
   ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET]; ALL_TAC] THEN
   REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN
   DISCH_THEN(MP_TAC o SPEC `g':(A->bool)->bool`) THEN
   MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
   CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; SUBSET_TRANS]; ALL_TAC] THEN
   CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET]; ALL_TAC] THEN
   ASM_REWRITE_TAC[] THEN
   MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN
   FIRST_X_ASSUM MP_TAC THEN
   SET_TAC[]);;



(* Canonical polyhedron representation for Omega(V, ul) *)
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 
    ==> ?K. FINITE K /\ voronoi_list V ul = affine hull (voronoi_list V ul) INTER INTERS K /\ 
	(!a. a IN K ==> (?v. v IN V /\ ~(v = h) /\ (a = bis_le v h \/ a = bis_le h v))) /\
	(!K'. K' PSUBSET K ==> voronoi_list V ul PSUBSET affine hull (voronoi_list V ul) INTER INTERS K')`,
  REPEAT GEN_TAC THEN
    DISCH_THEN (MP_TAC o (fun th -> MATCH_MP VORONOI_LIST_ALMOST_CANONICAL th)) THEN
    STRIP_TAC THEN

    REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
    DISCH_THEN (LABEL_TAC "A") THEN
    DISCH_THEN (LABEL_TAC "B") THEN
    DISCH_THEN (LABEL_TAC "C") THEN
    
    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

    USE_THEN "A" (fun th -> REWRITE_TAC[th]) THEN
    ANTS_TAC THENL
    [
      ASM_MESON_TAC[];
      ALL_TAC
    ] THEN

    STRIP_TAC THEN
    EXISTS_TAC `g:(real^3->bool)->bool` THEN
    ASM_REWRITE_TAC[] THEN
    REPEAT STRIP_TAC THENL
    [
      ASM_MESON_TAC[FINITE_SUBSET];
      ASM_MESON_TAC[];
      POP_ASSUM MP_TAC THEN
      REPLICATE_TAC 2 (POP_ASSUM (fun th -> ALL_TAC)) THEN
	REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN
	REWRITE_TAC[SUBSET] THEN MESON_TAC[]
    ]);;

(* voronoi_list is a polyhedron *)
let POLYHEDRON_VORONOI_LIST = prove(`!V ul. packing V /\ saturated V /\ set_of_list ul SUBSET V 
				    ==> polyhedron (voronoi_list V ul)`,
   REPEAT STRIP_TAC THEN
     DISJ_CASES_TAC (ISPEC `ul:(real^3)list` list_CASES) THENL
     [
       ASM_REWRITE_TAC[VORONOI_LIST; set_of_list; VORONOI_SET; NOT_IN_EMPTY] THEN
	 SUBGOAL_THEN `{voronoi_closed V (v:real^3) | v | F} = {}` (fun th -> REWRITE_TAC[th]) THENL
	 [
	   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM];
	   ALL_TAC
	 ] THEN
	 REWRITE_TAC[INTERS_0; POLYHEDRON_UNIV];
       ALL_TAC
     ] THEN

     POP_ASSUM STRIP_ASSUME_TAC THEN
     ASM_SIMP_TAC[VORONOI_LIST_BIS] THEN

     MATCH_MP_TAC POLYHEDRON_INTER THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC VORONOI_POLYHEDRON THEN
	 ASM_REWRITE_TAC[] THEN
	 MATCH_MP_TAC IN_TRANS THEN
	 EXISTS_TAC `set_of_list ul:real^3->bool` THEN
         ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
       ALL_TAC
     ] THEN

     MATCH_MP_TAC POLYHEDRON_INTERS THEN
     CONJ_TAC THENL
     [
       ONCE_REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
	 MATCH_MP_TAC FINITE_IMAGE THEN
	 REWRITE_TAC[FINITE_SET_OF_LIST];
       ALL_TAC
     ] THEN

     REWRITE_TAC[IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[POLYHEDRON_BIS]);;

(* voronoi_list is a polytope *)
let POLYTOPE_VORONOI_LIST = prove(`!V ul. packing V /\ saturated V /\ set_of_list ul SUBSET V /\ ~(ul = [])
				    ==> polytope (voronoi_list V ul)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[POLYTOPE_EQ_BOUNDED_POLYHEDRON] THEN
     ASM_SIMP_TAC[POLYHEDRON_VORONOI_LIST] THEN
     MP_TAC (ISPEC `ul:(real^3)list` list_CASES) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_SIMP_TAC[VORONOI_LIST_BIS] THEN
     MATCH_MP_TAC BOUNDED_SUBSET THEN
     EXISTS_TAC `voronoi_closed V (h:real^3)` THEN
     REWRITE_TAC[INTER_SUBSET] THEN
     ASM_SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;	 
	 
let POLYTOPE_VORONOI_LIST_BARV = prove(`!V ul k. packing V /\ saturated V /\ barV V k ul ==> polytope (voronoi_list V ul)`,
   REPEAT STRIP_TAC THEN
   MATCH_MP_TAC POLYTOPE_VORONOI_LIST THEN
   ASM_REWRITE_TAC[] THEN
   CONJ_TAC THENL 
   [ 
     MATCH_MP_TAC BARV_SUBSET THEN
       EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[];
     ALL_TAC
   ] THEN
   REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
   POP_ASSUM MP_TAC THEN SIMP_TAC[BARV; ARITH_RULE `~(k + 1 = 0)`]);;   

(* closed (voronoi_list V ul) *)   
let CLOSED_VORONOI_LIST = prove(`!V ul. closed (voronoi_list V ul)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[VORONOI_LIST; VORONOI_SET] THEN
     MATCH_MP_TAC CLOSED_INTERS THEN
     REWRITE_TAC[IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[CLOSED_VORONOI_CLOSED]);;

(* convex (voronoi_list V ul) *)
let CONVEX_VORONOI_LIST = prove(`!V ul. convex (voronoi_list V ul)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[VORONOI_LIST; VORONOI_SET] THEN
     MATCH_MP_TAC CONVEX_INTERS THEN
     REWRITE_TAC[IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[CONVEX_VORONOI_CLOSED]);;


(* aff_dim voronoi_list *)
let AFF_DIM_VORONOI_LIST = prove(`!V ul k. barV V k ul ==> aff_dim (voronoi_list V ul) = &3 - &k`,
   REWRITE_TAC[BARV; VORONOI_NONDG] THEN REPEAT STRIP_TAC THEN
     POP_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
     ASM_REWRITE_TAC[ARITH_RULE `0 < k + 1`; INITIAL_SUBLIST_REFL] THEN
     REWRITE_TAC[GSYM INT_OF_NUM_ADD] THEN INT_ARITH_TAC);;	 
	 
(* voronoi_list V vl SUBSET voronoi_closed V (HD vl) *)
let VORONOI_LIST_SUBSET_VORONOI_CLOSED = prove(`!V vl. 1 <= LENGTH vl ==> voronoi_list V vl SUBSET voronoi_closed V (HD vl)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[SUBSET; VORONOI_LIST; VORONOI_SET; IN_INTERS; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `voronoi_closed V ((HD vl):real^3)`) THEN
     ANTS_TAC THENL
     [
       EXISTS_TAC `HD vl:real^3` THEN
	 REWRITE_TAC[] THEN
	 MATCH_MP_TAC HD_IN_SET_OF_LIST THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REWRITE_TAC[]);;  


(************************************************************)

(*****************************************************)
(* General properties of omega_list_n and omega_list *)
(*****************************************************)

(* omega_k(u) = omega_k (d_(k+i) u) *)
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`,
   GEN_TAC THEN GEN_TAC THEN
     INDUCT_TAC THEN REWRITE_TAC[OMEGA_LIST_N] THEN REPEAT STRIP_TAC THENL
     [
       MATCH_MP_TAC (GSYM HD_TRUNCATE_SIMPLEX) THEN
	 POP_ASSUM MP_TAC THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     MP_TAC (ISPECL [`ul:(real^3)list`; `SUC k`; `SUC k + i`] TRUNCATE_TRUNCATE_SIMPLEX) THEN
     ASM_REWRITE_TAC[ARITH_RULE `a:num <= a + i`; ARITH_RULE `(a + b) + 1 = a + b + 1`] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     AP_TERM_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `i + 1`) THEN
     ASM_REWRITE_TAC[ARITH_RULE `k + (i + 1) + 1 = SUC k + i + 1`] THEN
     SIMP_TAC[ARITH_RULE `k + i + 1 = SUC k + i`]);;

(* omega(d_k u) = omega_k (u) *)
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`,
   REPEAT STRIP_TAC THEN REWRITE_TAC[OMEGA_LIST] THEN
     MP_TAC (ISPECL [`k:num`; `truncate_simplex k (ul:(real^3)list)`; `ul:(real^3)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
     ASM_SIMP_TAC[ARITH_RULE `(k + 1) - 1 = k`] THEN
     DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `k:num`; `0`] OMEGA_LIST_N_LEMMA) THEN
     ASM_SIMP_TAC[ADD_CLAUSES]);;	 

	 
let BARV_IMP_VORONOI_LIST_NOT_EMPTY = prove(`!V ul k. barV V k ul ==> ~(voronoi_list V ul = {})`,
   REPEAT STRIP_TAC THEN
     UNDISCH_TAC `barV V k ul` THEN DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
     REWRITE_TAC[BARV; VORONOI_NONDG] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `ul:(real^3)list`) THEN
     ASM_REWRITE_TAC[INITIAL_SUBLIST_REFL; ARITH_RULE `0 < k + 1`; DE_MORGAN_THM] THEN
     DISJ2_TAC THEN DISJ2_TAC THEN
     REWRITE_TAC[AFF_DIM_EMPTY; GSYM INT_OF_NUM_ADD] THEN
     SUBGOAL_THEN `&k <= int_of_num 3` MP_TAC THENL
     [
       REWRITE_TAC[INT_OF_NUM_LE] THEN
	 MATCH_MP_TAC BARV_IMP_K_LE_3 THEN
	 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `ul:(real^3)list`] THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     INT_ARITH_TAC);;     
     
(* omega_i IN voronoi_list V (d_i ul) *)
let OMEGA_LIST_N_IN_VORONOI_LIST = prove(`!V ul k i. barV V k ul /\ i <= k
					   ==> omega_list_n V ul i IN voronoi_list V (truncate_simplex i ul)`,
   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `LENGTH (ul:(real^3)list) = k + 1` ASSUME_TAC THENL
     [
       UNDISCH_TAC `barV V k ul` THEN
	 SIMP_TAC[BARV];
       ALL_TAC
     ] THEN
     DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
     [
       ASM_REWRITE_TAC[OMEGA_LIST_N] THEN
	 MP_TAC (ISPEC `ul:(real^3)list` TRUNCATE_0_EQ_HEAD) THEN
	 ASM_REWRITE_TAC[ARITH_RULE `1 <= k + 1`] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 REWRITE_TAC[VORONOI_LIST_SING; CENTER_IN_VORONOI_CELL];
       ALL_TAC
     ] THEN
     POP_ASSUM CHOOSE_TAC THEN
     ASM_REWRITE_TAC[OMEGA_LIST_N] THEN
     MP_TAC (ISPECL [`voronoi_list V (truncate_simplex i ul):real^3->bool`; `omega_list_n V ul n`] CLOSEST_POINT_EXISTS) THEN
     ANTS_TAC THENL
     [
       REWRITE_TAC[CLOSED_VORONOI_LIST] THEN
	 MATCH_MP_TAC BARV_IMP_VORONOI_LIST_NOT_EMPTY THEN
	 EXISTS_TAC `i:num` THEN
	 MATCH_MP_TAC TRUNCATE_SIMPLEX_BARV THEN
	 EXISTS_TAC `k:num` THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[]);;

(* omega ul IN voronoi_list V ul *)
let OMEGA_LIST_IN_VORONOI_LIST = prove(`!V ul k. barV V k ul ==> omega_list V ul IN voronoi_list V ul`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[OMEGA_LIST] THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ul:(real^3)list`; `k:num`; `k:num`] OMEGA_LIST_N_IN_VORONOI_LIST) THEN
     ASM_REWRITE_TAC[LE_REFL] THEN
     SUBGOAL_THEN `LENGTH (ul:(real^3)list) = k + 1` ASSUME_TAC THENL
     [
       POP_ASSUM MP_TAC THEN SIMP_TAC[BARV];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `truncate_simplex k ul = ul:(real^3)list` (fun th -> REWRITE_TAC[th]) THENL
     [
       MP_TAC (ISPECL [`k:num`; `ul:(real^3)list`; `ul:(real^3)list`] TRUNCATE_SIMPLEX_INITIAL_SUBLIST) THEN
	 ASM_REWRITE_TAC[LE_REFL; INITIAL_SUBLIST_REFL];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[ARITH_RULE `(k + 1) - 1 = k`]);;


end;;