legacy/oldpacking/RHWVGNP.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: RHWVGNP                                                             *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 There are two main separate conclusions
  15 (1) The boundedness of the Voronoi cell
  16 (2) The polyhedron.
  17 The statement of the lemma has been broken into substatements.
  18 All statements need a proof.
  19
  20 Closely related theorems for `voronoi_open` have been proved by  Thang. It might be possible
  21 to adapt his proofs.
  22
  23 Deprecated Dec 28, 2011.  Content moved to pack_concl.hl
  24 *)
  25
  26
  27
  28 module type Rhwvgnp_type = sig
  29   val RHWVGNP_concl  : term
  30   val VORONOI_BALL2_concl  : term
  31   val VORONOI_INTER_BIS_LE_concl : term
  32   val VORONOI_POLYHEDRON_concl : term
  33 end;;
  34
  35
  36
  37 module Rhwvgnp : Rhwvgnp_type = struct
  38
  39  let VORONOI_BALL2_concl = `!V (v:real^3).  packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;
  40
  41  let VORONOI_INTER_BIS_LE_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
  42    (voronoi_closed V v =INTERS { bis_le v u | u IN V /\ u IN ball(v, &4) /\  ~(u=v) })`;;
  43
  44  let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
  45    polyhedron (voronoi_closed V v)`;;
  46
  47   let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;
  48
  49 end;;