(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: RHWVGNP                                                             *)
(* Chapter: Packing                                                           *)
(* Author: Thomas C. Hales                                                    *)
(* Date: Feb 14, 2010                                                         *)
(* ========================================================================== *)




(*
There are two main separate conclusions
(1) The boundedness of the Voronoi cell
(2) The polyhedron.
The statement of the lemma has been broken into substatements.
All statements need a proof.  

Closely related theorems for `voronoi_open` have been proved by  Thang. It might be possible
to adapt his proofs.

Deprecated Dec 28, 2011.  Content moved to pack_concl.hl
*)



module type Rhwvgnp_type = sig
  val RHWVGNP_concl  : term
  val VORONOI_BALL2_concl  : term
  val VORONOI_INTER_BIS_LE_concl : term
  val VORONOI_POLYHEDRON_concl : term
end;;



module Rhwvgnp : Rhwvgnp_type = struct

 let VORONOI_BALL2_concl = `!V (v:real^3).  packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;

 let VORONOI_INTER_BIS_LE_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> 
   (voronoi_closed V v =INTERS { bis_le v u | u IN V /\ u IN ball(v, &4) /\  ~(u=v) })`;;

 let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
   polyhedron (voronoi_closed V v)`;;
  
  let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;

end;;