(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALISATION                                              *)
(*                                                                            *)
(* Proof: DLWCHEM                                                             *)
(* Chapter: Packing                                                           *)
(* Author: Dang Tat Dat                                                       *)
(* Date:   In progress                                                        *)
(* ========================================================================== *)

needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;

(* ** Load parent files ** *)
flyspeck_needs "nonlinear/ineq.hl";;
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "tame/tame_defs.hl";;
flyspeck_needs "trigonometry/trigonometry.hl";;
flyspeck_needs "fan/Conforming.hl";;
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "fan/HypermapAndFan.hl";;
flyspeck_needs "fan/polyhedron.hl";;

(* ** Proof module type ** *)


(* ** Proof module ** *)

open Sphere;;
open Trigonometry1;;
open Trigonometry2;;
open Vol1;;
open Pack_defs;;
open Tame_defs;;
open Ineq;;
open Fan_defs;;
open Hypermap;;
open Hypermap_and_fan;;
open Fan;;
open Polyhedron;;
(*open Polyhedron_def;;*)
(*--------------Definition---------------------------------------------------*)
let weakly_saturated = 
    new_definition 
     `weakly_saturated (V:real^3 ->bool) (r:real) (r':real) <=>
        (!(v:real^3).(&2 <= dist(vec 0,v) ) /\ (dist(vec 0, v) <= r') ==>
            (?(u:real^3). (u IN V) /\ (~((vec 0) = u)) /\ (dist(u,v) < r)))`;;

let half_spaces =
    new_definition 
    `half_spaces (a:real^3) (b:real) =
     {x:real^3| (a dot x) <= b}`;;

let r = 
    new_definition
     `r = &2` ;;

let r' = 
    new_definition
     `r' = &2 * h0` ;;

let g_fun =
    new_definition 
    `(g_fun) (x:real^3) = (acs(dist(vec 0, x)/(&4))) - (pi/(&6))` ;; 

let dart2_of_fan = new_definition
  `dart2_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  {(v,v) | v IN V /\ set_of_edge (v:A) V E = {} }`;;

(*-------------------------Fan   Definiton-----------------------------------*)

let CASE_FAN_FINITE = new_definition `CASE_FAN_FINITE (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> FINITE V /\ ~(V SUBSET {})`;;

let CASE_FAN_ORIGIN = new_definition `CASE_FAN_ORIGIN (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> ~((vec 0) IN (V))`;;

let CASE_FAN_INDEPENDENCE = 
  new_definition `CASE_FAN_INDEPENDENCE (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> 
  (!e.  e IN E ==> ~collinear ({vec 0} UNION e))`;;
 
let CASE_FAN_INTERSECTION =  
  new_definition`CASE_FAN_INTERSECTION(V:real^3 -> bool,E:(real^3 ->bool)->bool)<=> 
  (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  ==> ((aff_ge {vec 0 } e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;

let FANO =
  new_definition `FANO(V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> 
  ((UNIONS E) SUBSET V) /\ graph(E) /\ CASE_FAN_FINITE(V,E) /\ CASE_FAN_ORIGIN(V,E)/\
  CASE_FAN_INDEPENDENCE(V,E)/\ CASE_FAN_INTERSECTION(V,E)`;;

let FANO_OF_FAN = prove( `!(V:real^3 -> bool)(E:(real^3 ->bool)->bool). (FAN(vec 0 , V , E) <=> FANO(V,E))`, 
  REWRITE_TAC[FAN;FANO;CASE_FAN_FINITE;CASE_FAN_ORIGIN;CASE_FAN_INDEPENDENCE;CASE_FAN_INTERSECTION;fan1;fan2;fan6;fan7]);;

(*-------------------------------------------------------------------------*)

let interior_point =
    new_definition 
    `interior_point (p:real^3) (P:real^3->bool) 
       <=> ?(r:real). (&0 < r) /\ (ball(p,r) SUBSET P)` ;;
let reg =
    new_definition 
     `reg (a:real) (k:real) = (&2)*pi - (&2)*k*(asn(cos(a)*sin(pi/k)))` ;;

let arc_1 =
    new_definition 
    `arc_1 (a:real) (b:real) (c:real) = 
     pi/(&2) - (atn2( (sqrt (ups_x (a*a) (b*b) (c*c))),(a*a + b*b - c*c)))`;;

let IN_DOUBLE = prove(`!x y z:real^N. x IN {y,z} <=> x = y  \/ x = z`,SET_TAC[]);;

let INTERIOR_EQUIVALENT = prove (`!(V:real^3->bool) x:real^3. interior_point x V <=> x IN interior V`,REPEAT GEN_TAC THEN PURE_REWRITE_TAC [interior_point;IN_INTERIOR] THEN MESON_TAC[]);;

let DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET=prove(`!(H:(A)hypermap). dart H = UNIONS (face_set H)/\ dart H = UNIONS (node_set H)/\ dart H = UNIONS (edge_set H)`,
  GEN_TAC THEN REWRITE_TAC[face_set;node_set;edge_set]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC lemma_partition
THEN REWRITE_TAC[hypermap_lemma]);;


(*-----------------Some new axiom--------------------------------------------*)
let TARJJUW_concl = `!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) r r':real u:real^3. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V/\ ~(V = {}) /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} /\ polyhedron P /\ u IN V ==>
(bounded P)`;;

let TARJJUW = new_axiom TARJJUW_concl;;

(*----------------------------------------------------------------------------*)
g `!(V: real^3 -> bool). (polyhedron V) /\ (bounded V) /\ (interior_point (vec 0) V)  ==> edges V  = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of V}`;;

e (GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [edges;EXTENSION]);;
e (GEN_TAC THEN EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`V:real^3 -> bool`;`v:real^3`;`w:real^3`]SEGMENT_EDGE_OF));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (EXISTS_TAC `v:real^3`);;
e (EXISTS_TAC `w:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `segment [v,w] edge_of (V:real^3->bool)`);;
e (REWRITE_TAC [edge_of;face_of;segment;CONVEX_HULL_2_ALT;IN_ELIM_THM]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!v:real^3 w:real^3 u:real . v + u % (w - v) = (&1 - u) % v + u % w` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [VECTOR_SUB_LDISTRIB;VECTOR_SUB_RDISTRIB;VECTOR_MUL_LID]);;
e (VECTOR_ARITH_TAC);;
e (SUBGOAL_THEN `{(v:real^3) + (u:real) % ((w:real^3) - v)| &0 <= u /\ u <= &1} ={(&1 - u) % v + u % w | &0 <= u /\ u <= &1}` ASSUME_TAC);;
e (REWRITE_TAC [EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `!v:real^3 w:real^3 u:real . v + u % (w - v) = (&1 - u) % v + u % w` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [VECTOR_SUB_LDISTRIB;VECTOR_SUB_RDISTRIB;VECTOR_MUL_LID]);;
e (VECTOR_ARITH_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `v:real^3`);;
e (EXISTS_TAC `w:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `convex hull {v, w} face_of (V:real^3->bool)`);;
e (REWRITE_TAC [edge_of;face_of;segment;CONVEX_HULL_2_ALT]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `{(v:real^3) + (u:real) % ((w:real^3) - v)| &0 <= u /\ u <= &1} ={(&1 - u) % v + u % w | &0 <= u /\ u <= &1}` ASSUME_TAC);;
e (REWRITE_TAC [EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]));;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `{(v:real^3) + (u:real) % ((w:real^3) - v)| &0 <= u /\ u <= &1} ={(&1 - u) % v + u % w | &0 <= u /\ u <= &1}` ASSUME_TAC);;
e (REWRITE_TAC [EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real`);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [GSYM segment]);;
e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]SEGMENT_SUBSET_HALFLINE));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]HALFLINE_SUBSET_AFFINE_HULL));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`{v:real^3,w:real^3}`]AFF_DIM_AFFINE_HULL));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`segment [v:real^3,w:real^3]`;`aff_ge {v:real^3} {w:real^3}`;`affine hull {v:real^3, w:real^3}`]SUBSET_TRANS));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`segment [v:real^3,w:real^3]`;`affine hull {v:real^3, w:real^3}`]AFF_DIM_SUBSET));;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]AFF_DIM_2));;
e (ASM_REWRITE_TAC[]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `{v:real^3,w:real^3} SUBSET segment [v,w]` ASSUME_TAC);;
e (REWRITE_TAC [segment;SUBSET]);;
e (GEN_TAC);; 
e (REWRITE_TAC[IN_DOUBLE;IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `&0`);;
e (REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1`]);;
e (REWRITE_TAC[ARITH_RULE `&1 - &0 = &1`;VECTOR_MUL_LZERO;VECTOR_ADD_RID;VECTOR_MUL_LID]);;
e (ASM_REWRITE_TAC[]);;
e (EXISTS_TAC `&1`);;
e (REWRITE_TAC [ARITH_RULE `&0 <= &1 /\ &1 <= &1`]);;
e (REWRITE_TAC [ARITH_RULE `&1 - &1 = &0`;VECTOR_MUL_LZERO;VECTOR_MUL_LID;VECTOR_ADD_LID]);;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC (ISPECL [`{v:real^3, w:real^3}`;`segment [v:real^3,w:real^3]`]AFF_DIM_SUBSET));;
e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`aff_dim (segment [v:real^3,w:real^3])`;`aff_dim {(v:real^3), (w:real^3)}`]INT_LE_ANTISYM));;
e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;

let EDGE_CONVEX_HULL = top_thm();;

g `!(V:real^3 -> bool). (polyhedron V) /\ (bounded V) /\ (interior_point (vec 0) V) ==> FANO (fan_of_polyhedron V)`;;
e (GEN_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`V:real^3->bool`;`(vec 0):real^3`]POLYHEDRON_FAN));;
e (MP_TAC (ISPECL [`V:real^3->bool`;`(vec 0):real^3`]INTERIOR_EQUIVALENT));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[vertices;edges;fan_of_polyhedron]);;
e (REWRITE_TAC [edge_of]);;
e (MP_TAC (ISPECL [`V:real^3->bool`]EDGE_CONVEX_HULL));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));;
e (MP_TAC (ISPECL [`V:real^3 ->bool`;`(vec 0):real^3`]POLYHEDRON_FAN));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`vertices (V:real^3->bool)`;`edges (V:real^3->bool)`]FANO_OF_FAN));;
e (ASM_REWRITE_TAC[GSYM vertices]);;

let JLIGZGS = top_thm();;

(*---------------------------------------------------------------------------*)
let WGVWSKE_concl = `!(V:real^3->bool) (E:(real^3->bool)->bool).
   FANO (V,E) /\ conforming (V,E) 
   ==> connected_hypermap (hypermap_of_fan (V,E))`;;

let WGVWSKE = new_axiom WGVWSKE_concl;;


let GGRLKHP_concl = `!(V:real^3->bool) (E:(real^3->bool)->bool).
   FANO (V,E) /\ conforming (V,E) 
   ==> planar_hypermap (hypermap_of_fan (V,E))`;;

let GGRLKHP = new_axiom GGRLKHP_concl;;

let PLAIN_HYPERMAP =prove(`!(V:real^3->bool) (E:(real^3->bool)->bool).
   FANO (V,E) ==> plain_hypermap (hypermap_of_fan (V,E))`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `FAN (vec 0,(V:real^3->bool),(E:(real^3->bool)->bool))` ASSUME_TAC THEN ASM_REWRITE_TAC [FANO_OF_FAN] THEN ASM_MESON_TAC [PLAIN_HYPERMAP_OF_FAN]);;

(*---------------------------------------------------------------------------*)

(*FACET_OF_POLYHEDRON_EXPLICIT*) 
(*Chung minh rang o day ton tai mot song anh*)
(*!s f a b.
         FINITE f /\
         s = affine hull s INTER INTERS f /\
         (!h. h IN f ==> ~(a h = vec 0) /\ h = {x | a h dot x <= b h}) /\
         (!f'. f' PSUBSET f ==> s PSUBSET affine hull s INTER INTERS f')
         ==> (!c. c facet_of s <=>
                  (?h. h IN f /\ c = s INTER {x | a h dot x = b h})) *)
let CZZHBLI_concl_1 = 
    `!(V:real^3 -> bool) P (u:real^3) b:real F .(FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
  (polyhedron P) /\ (bounded P) /\ 
   F = {f|f facet_of P} 
  ==> (?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F)`;;

let CZZHBLI_1 = new_axiom CZZHBLI_concl_1;;
(*
g `!(V:real^3 -> bool) P (u:real^3) b:real F .(FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
  (polyhedron P) /\ (bounded P) /\ 
   F = {f|f facet_of P} 
  ==> (?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`P:real^3->bool`;`f:real^3->bool`]FACET_OF_POLYHEDRON));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;

FACET_OF_POLYHEDRON_EXPLICIT;;
FACET_OF_POLYHEDRON;;
FINITE_POLYHEDRON_FACES;;
FINITE_POLYHEDRON_EXTREME_POINT;;
search [`norm v`];;
*)
(*----------------------------------------------------------------------------*)

let RDWKARC_concl = `~kepler_conjecture /\ (!V. cell_cluster_estimate V) /\
  marchal_inequality
   ==> (?V.  packing V /\ V SUBSET ball_annulus /\ ~(lmfun_ineq_center V))`;;

let RDWKARC = new_axiom  RDWKARC_concl;;


(*---------------------------------------------------------------------------*)

let AMHFNXP_concl =
    `!(P:real^3 -> bool) F WF. 
     (polyhedron P) /\ (bounded P) /\ (interior_point (vec 0) P) /\
     (F = {f|f facet_of P}) /\ (WF = topological_component_yfan (vec 0,fan_of_polyhedron P))   
      ==> (?(h:(real^3->bool) -> (real^3->bool)) (g: (real^3->bool) -> (real^3->bool)). h o g = I /\ g o h = I /\ IMAGE h F = WF)`;;

let AMHFNXP = new_axiom AMHFNXP_concl;;

(*---------------------------------------------------------------------------*)

let BSXAQBQ_concl = `!(P:real^3 -> bool)(x:real^3#real^3).(polyhedron P) /\ (bounded P) /\(interior_point (vec 0) P) /\ (x IN (dart_of_fan (fan_of_polyhedron P))) ==> azim_dart (fan_of_polyhedron P) x < pi`;;

let BSXAQBQ = new_axiom BSXAQBQ_concl;;
(*---------------------------------------------------------------------------*)

let PIIJBJK_concl =`!(V:real^3 -> bool)(E:(real^3->bool)->bool). 
    fully_surrounded (V,E) ==>
     conforming (V,E)`;;


let PIIJBJK = new_axiom PIIJBJK_concl;;
(*---------------------------------------------------------------------------*)

let UVPFEEP_concl1 =`!(V:real^3 -> bool) (E:(real^3->bool)->bool) F WF.
      FANO (V,E) /\ (conforming (V,E)) /\ 
      (WF = topological_component_yfan (vec 0,V,E)) /\ 
      (F = face_set_of_fan (V,E))
      ==> (?(f: (real^3->bool) -> (real^3#real^3->bool)) (g: (real^3#real^3->bool) ->  (real^3->bool)). f o g = I /\ g o f = I /\ IMAGE f WF = F)`;;


let UVPFEEP_1= new_axiom UVPFEEP_concl1;;      
                                
(*---------------------------------------------------------------------------*)
let GOTCJAH_concl = `!s f (v:real^3) b WF h k. 
    polyhedron s /\ bounded s /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET s) /\
    f facet_of s /\ 
    f = { p | p dot v = b } INTER s /\ 
    topological_component_yfan (vec 0,fan_of_polyhedron s) WF /\
    ~(f INTER WF = {}) /\
    rcone_gt (vec 0) v h SUBSET WF /\
    (k = CARD {u | u extreme_point_of f }) 
   ==> &2 * pi - &2* &k * asn (h* sin(pi/ &k)) <= sol (vec 0) WF`;;

let GOTCJAH = new_axiom GOTCJAH_concl;;

(*---------------------------------proof--------------------------------------*)

g `!(V:real^3 -> bool) (x:real). (&1 <=x ) ==> (lmfun x <= &1)`;;
e (REWRITE_TAC [lmfun;h0]);;
e (REPEAT STRIP_TAC);;
e (ASM_CASES_TAC `(x:real) <= #1.26`);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [ARITH_RULE `#1.26 - &1 = #0.26`]);;
e (SUBGOAL_THEN `&0 < #0.26` ASSUME_TAC);; 
e (ARITH_TAC);;
e (SUBGOAL_THEN `(--x:real <= --(&1) )` ASSUME_TAC);;
e (ASM_REWRITE_TAC [REAL_LE_NEG]);;
e (SUBGOAL_THEN `#1.26 + --(x:real) <= #1.26 + --(&1)` ASSUME_TAC);;
e (ASM_REWRITE_TAC [REAL_LE_LADD]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [GSYM real_sub]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(#1.26 - (x:real)) / #0.26 <= (#1.26 - &1) / #0.26` ASSUME_TAC);;
e (ASM_MESON_TAC [GSYM REAL_LE_DIV2_EQ]);;
e (SUBGOAL_THEN `(#1.26 - &1) / #0.26 = &1` ASSUME_TAC);;
e (ARITH_TAC);;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (ARITH_TAC);;

let thm1 = top_thm();;

(*----------------------------------------------------------------------------*)


g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
   (u IN V) ==> ((&1) <= dist(vec 0,u)/(&2)) `;;
e (REWRITE_TAC [ball_annulus]);;
e (REWRITE_TAC [cball;ball]);;
e (REWRITE_TAC [DIFF]);;
e (REWRITE_TAC [SUBSET]);;
e (REPEAT STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(u:real^3) IN
          {x:real^3 | x IN {y:real^3 | dist (vec 0,y) <= &2 * h0} /\
               ~(x IN {y | dist (vec 0,y) < &2})} ` ASSUME_TAC);;
e (ASM_MESON_TAC []);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_NOT_LT]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(&0) < (&2)` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `(&2)/(&2) <= dist (vec 0,u:real^3)/(&2)` ASSUME_TAC);;
e (ASM_MESON_TAC [REAL_LE_DIV2_EQ]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ARITH_RULE `(&2)/(&2) = (&1)`]);;

let thm2 = top_thm();;

g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
   (u IN V) ==> (dist(vec 0,u) <= &2 * h0) `;;
e (REWRITE_TAC [ball_annulus]);;
e (REWRITE_TAC [cball;ball]);;
e (REWRITE_TAC [DIFF]);;
e (REWRITE_TAC [SUBSET]);;
e (REPEAT STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(u:real^3) IN
          {x:real^3 | x IN {y:real^3 | dist (vec 0,y) <= &2 * h0} /\
               ~(x IN {y | dist (vec 0,y) < &2})} ` ASSUME_TAC);;
e (ASM_MESON_TAC []);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;

let thm21 = top_thm();;
(*----------------------------------------------------------------------------*)

g `!(V:real^3->bool).(FINITE V) /\ (packing V) /\ (V SUBSET ball_annulus) /\ 
    (&(CARD V) <= (&12)) ==> 
    sum V (\v. lmfun (dist (vec 0,v) / &2)) <= (&12)`;;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> (&1) <= dist(vec 0,v)/(&2)` ASSUME_TAC);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC [thm2]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (USE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (&1) <= dist(vec 0,v)/(&2) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_TAC);;
e (STRIP_TAC);;
e (MESON_TAC [thm1]);;
e (POP_ASSUM (LABEL_TAC "F2"));;
e (USE_THEN "F2" (MP_TAC o SPEC `v:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_TAC);;
e (STRIP_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (dist (vec 0,v) / &2)) <= (&(CARD V)) * (&1)` ASSUME_TAC);;
e (ASM_MESON_TAC [SUM_BOUND]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ARITH_RULE `&(CARD (V:real^3->bool)) * &1 =  &(CARD V)`]);;
e (STRIP_TAC);;
e (ASM_MESON_TAC[REAL_LE_TRANS]);;

let thm3 = top_thm();;

(*----------------------------------------------------------------------------*)

g `!(V:real^3->bool) (u:real^3).(packing V) /\ (V SUBSET ball_annulus) /\ (weakly_saturated V r r') /\ (u IN V) ==> (dist (vec 0,u) / &2 <= h0)`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [packing;ball_annulus]);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [cball;ball]);;
e (REWRITE_TAC [SUBSET]);;
e (REWRITE_TAC [DIFF]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (REPEAT STRIP_TAC);;
e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&0 < &2` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= (&2) * h0` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;I
e (FIRST_X_ASSUM MP_TAC);;
e (ABBREV_TAC `uu = dist (vec 0, (u:real^3)) `);;
e (MESON_TAC[REAL_LE_LDIV_EQ; REAL_MUL_SYM]);;

let thm4 = top_thm();;

g `! (x:real^N) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w))`;;
e (REPEAT GEN_TAC);;
e (EXISTS_TAC ` inv (&2) % ( x + (y:real^N) )  `);;
e (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `inv (&2)`);;
e (EXISTS_TAC `inv (&2)`);;
e (PURE_REWRITE_TAC[ARITH_RULE `inv (&2) + inv (&2) = &1 `]);;
e (PURE_REWRITE_TAC [VECTOR_ADD_LDISTRIB]);;
e (STRIP_TAC);;
e (ARITH_TAC);;
e (ARITH_TAC);;
e (EXISTS_TAC `dist (x:real^N,y) /(&2)`);;
e (GEN_TAC);;
e (SUBGOAL_THEN `{x:real^N, y} w <=> w IN {x:real^N, y}` ASSUME_TAC);;
e (REWRITE_TAC [IN]);;
e (SUBGOAL_THEN `(w:real^N) IN {x, y} <=> w = x \/ w = y` ASSUME_TAC);;
e (MESON_TAC [IN_DOUBLE]);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;

e (PURE_REWRITE_TAC [GSYM midpoint]);;
e (REWRITE_TAC [DIST_MIDPOINT]);;
e (ASM_REWRITE_TAC [GSYM midpoint]);;
e (REWRITE_TAC [DIST_MIDPOINT]);;

let thm5 = top_thm();;

 
let dat_th1 = prove(` segment [v,w:real^3] SUBSET affine hull {v,w} `,

REWRITE_TAC[AFFINE_HULL_2; segment; SUBSET; IN_ELIM_THM] THEN

MESON_TAC[REAL_ARITH` (&1 - x ) + x = &1 `]);;

g `(! (x:real^3) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w)))
==>
( !v w:real^3. ~(v = w) ==> circumcenter{v,w} = midpoint(v,w))`;;
e (REPEAT STRIP_TAC);;
e (MP_TAC (MESON[MIDPOINT_IN_SEGMENT]` midpoint (v,w:real^3) IN segment [v,w]`));;
e (SUBGOAL_THEN ` ( affine hull {v,w:real^3} ) (circumcenter {v, w}) /\
(?c. ! x. {v,w} x ==> c = dist ((circumcenter {v, w}),x)) ` ASSUME_TAC);;
e (REWRITE_TAC[Collect_geom.circumcenter]);;
e (CONV_TAC SELECT_CONV);;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC dat_th1);;
e (REWRITE_TAC[SUBSET]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN ` midpoint (v,w:real^3) IN affine hull {v,w} ` ASSUME_TAC);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (FIRST_X_ASSUM ACCEPT_TAC);;
e (REPEAT (FIRST_X_ASSUM MP_TAC));;
e (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]);;
e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC ` !x. {v, w} x ==> c = dist (circumcenter {v, w},x:real^3)`);;
e (ASM_REWRITE_TAC[REWRITE_RULE[IN] (SET_RULE `x IN {a,b} <=> x = a \/ x = b`); MESON[] `(! a. a = x \/ a = y ==> P a) <=> P x /\ P y `; dist]);;
e (UNDISCH_TAC ` u + v' = &1 `);;
e (SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `; VECTOR_ARITH` ((&1 - v') % v + v' % w) - v = v' % (w - v )`; VECTOR_ARITH` ((&1 - v') % v + v' % w) - w = ( v' - &1 ) % ( w - v )`; NORM_MUL]);;
e (REPEAT STRIP_TAC);;
e (FIRST_X_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[REAL_ARITH` a * b = c * b <=> (a - c ) * b = &0`; REAL_ENTIRE]);;
e (STRIP_TAC);;
e (FIRST_X_ASSUM MP_TAC);;
e (REWRITE_TAC[REAL_ARITH ` abs a - abs ( a - &1 ) = &0 <=> a = &1 / &2 `]);;
e (SIMP_TAC[REAL_ARITH` &1 - &1 / &2 = &1 / &2 `]);;
e (UNDISCH_TAC` midpoint (v,w) = u' % v + v'' % (w:real^3) `);;
e (DISCH_THEN (SUBST1_TAC o SYM));;
e (REWRITE_TAC[midpoint; REAL_ARITH` inv (&2) = &1 / &2 `]);;
e (DISCH_TAC THEN VECTOR_ARITH_TAC);;
e (FIRST_X_ASSUM MP_TAC);;
e (REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ]);;
e (ASM_MESON_TAC[]);;

let thm6 = top_thm();;


g `!v w:real^3. ~(v = w) ==> circumcenter{v,w} = midpoint(v,w)`;;
e (SUBGOAL_THEN `! (x:real^3) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w))` ASSUME_TAC);;
e (REWRITE_TAC [thm5]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [thm6]);;

let thm7 = top_thm();;

g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
   (u IN V) ==> ~(vec 0 = u)`;;
e (REPEAT GEN_TAC);;
e (PURE_REWRITE_TAC [ball_annulus;SUBSET;DIFF;IN_ELIM_THM;cball;ball]);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= &2 * h0 /\ ~(dist (vec 0,u) < &2)` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (ASM_CASES_TAC `(vec 0 = u:real^3)`);;
e (SUBGOAL_THEN `dist(vec 0, u:real^3) = &0` ASSUME_TAC);;
e (ASM_REWRITE_TAC[]);;
e (MESON_TAC[DIST_REFL]);;
e (SUBGOAL_THEN `~(dist (vec 0,u:real^3) < &2)` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `&2 <= dist (vec 0,u:real^3)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [REAL_NOT_LT]);;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ARITH_TAC);;
e (ASM_REWRITE_TAC[]);;

let thm8= top_thm();;


g `!u:real^3 . ?d.(!w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w))`;;
e (GEN_TAC);;
e (EXISTS_TAC `dist(vec 0,u:real^3)/(&2)`);;
e (GEN_TAC);;
e (SUBGOAL_THEN `{vec 0, u:real^3} w <=> w IN {vec 0, u}` ASSUME_TAC);;
e (REWRITE_TAC [IN]);;
e (SUBGOAL_THEN `(w:real^3) IN {vec 0, u:real^3} <=> w = vec 0 \/ w = u` ASSUME_TAC);;
e (MESON_TAC [IN_DOUBLE]);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
e (REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
e (REWRITE_TAC[]);;

let thm9 = top_thm();;

g `!w:real^3 u. ~(vec 0 = u) /\ {vec 0, u} w ==>  dist (vec 0,u)/(&2) = dist (circumcenter {vec 0, u},w)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (SUBGOAL_THEN `{vec 0, u:real^3} w <=> w IN {vec 0, u}` ASSUME_TAC);;
e (REWRITE_TAC [IN]);;
e (SUBGOAL_THEN `(w:real^3) IN {vec 0, u:real^3} <=> w = vec 0 \/ w = u` ASSUME_TAC);;
e (MESON_TAC [IN_DOUBLE]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `circumcenter {vec 0, u:real^3} = midpoint (vec 0,u)` ASSUME_TAC);;
e (ASM_MESON_TAC [thm7]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
e (ARITH_TAC);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
e (ARITH_TAC);;

let thm10 = top_thm();;



g `(!u:real^3 . ?d. (!w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w)))
==> (!v:real^3. ~(vec 0 = v) ==> hl [vec 0;v] = dist (vec 0,v)/(&2))`;;
e (STRIP_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `circumcenter {vec 0, v:real^3} = midpoint (vec 0,v)` ASSUME_TAC);;
e (ASM_MESON_TAC [thm7]);;
e (SUBGOAL_THEN `!w:real^3. {vec 0, v} w ==> (dist (vec 0,v) / (&2)) = dist (circumcenter {vec 0, v},w)` ASSUME_TAC);;
e (ASM_MESON_TAC [thm10]);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [HL;set_of_list;radV]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (SET_TAC[]);;

let thm11 = top_thm();;


g `!v:real^3. ~(vec 0 = v) ==> hl [vec 0; v] = dist (vec 0,v) / &2`;;
e (SUBGOAL_THEN `!u:real^3. ?d. !w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w)` ASSUME_TAC);;
e (REWRITE_TAC [thm9]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [thm11]);;

let thm12 = top_thm();;

g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
   (u IN V) ==> hl [vec 0;u] = dist (vec 0,u)/(&2)  `;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `~(vec 0 = u:real^3)` ASSUME_TAC);;
e (ASM_MESON_TAC [thm8]);;
e (ASM_MESON_TAC [thm12]);;

let thm13 = top_thm();;

g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
   (u IN V) ==> &1 <= hl [vec 0;u] `;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `hl [vec 0; u:real^3] = dist (vec 0,u) / (&2)` ASSUME_TAC);;
e (ASM_MESON_TAC [thm13]);;
e (ASM_REWRITE_TAC[]);;
e (ASM_MESON_TAC [thm2]);;

let thm14 = top_thm();;

g `!(V:real^3->bool). FINITE V /\ packing V /\ V SUBSET ball_annulus /\ &(CARD V) <= &12
  ==> sum V (\v. lmfun (hl [vec 0;v])) <= &12`;;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> (&1) <= hl [vec 0;v]` ASSUME_TAC);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC [thm14]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (USE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (&1) <= hl [vec 0;v] ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_TAC);;
e (STRIP_TAC);;
e (MESON_TAC [thm1]);;
e (POP_ASSUM (LABEL_TAC "F2"));;
e (USE_THEN "F2" (MP_TAC o SPEC `v:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_TAC);;
e (STRIP_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (hl [vec 0;v])) <= (&(CARD V)) * (&1)` ASSUME_TAC);;
e (ASM_MESON_TAC [SUM_BOUND]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ARITH_RULE `&(CARD (V:real^3->bool)) * &1 =  &(CARD V)`]);;
e (STRIP_TAC);;
e (ASM_MESON_TAC[REAL_LE_TRANS]);;

let thm15 = top_thm();;


g `!(V:real^3->bool). FINITE V /\ packing V /\ 
  V SUBSET ball_annulus /\ ~(lmfun_ineq_center V) 
  ==> &12 < &(CARD V)`;;
e (GEN_TAC);;
e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
e (STRIP_TAC);;
e (ASM_CASES_TAC `&12 < &(CARD (V:real^3->bool))`);;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC[REAL_NOT_LT]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v])) <= &12` ASSUME_TAC);;
e (ASM_MESON_TAC [thm15]);;
e (UNDISCH_TAC `~(sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v])) <= &12)`);;
e (POP_ASSUM MP_TAC);;
e (ABBREV_TAC `a = sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v]))`);;
e (STRIP_TAC);;
e (ASM_MESON_TAC[]);;

let condition_1 = top_thm();;

(*-------------------------------------------------------------------------*)

g `!(V:real^3->bool) p. (!u:real^3. ~(u IN V1) \/ &2 <= dist (u,p)) ==> (!u:real^3. u IN V1 ==> &2 <= dist (u,p))`;;
e (REPEAT GEN_TAC);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (GEN_TAC);;
e (STRIP_TAC);;
e (USE_THEN "F1"(MP_TAC o SPEC `u:real^3`));;
e (POP_ASSUM MP_TAC);;
e (SET_TAC[]);;

let thm16 = top_thm();;

g `!(V:real^3->bool) V1. FINITE V /\ packing V /\ 
  V SUBSET ball_annulus /\ V SUBSET V1 /\ V1 SUBSET ball_annulus /\ (packing V1) /\ (!y:real^3. (!x:real^3. (x IN V1) ==> &2 <= dist(x,y)) ==> y IN V1)  ==> weakly_saturated V1 r r'`;;  
e (REPEAT GEN_TAC);;
e (PURE_REWRITE_TAC [packing]);;
e (STRIP_TAC);;
e (PURE_REWRITE_TAC [weakly_saturated]);;
e (PURE_REWRITE_TAC [r;r']);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (ASM_CASES_TAC `p:real^3 IN (V1:real^3->bool)`);;
e (EXISTS_TAC `p:real^3`);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (PURE_REWRITE_TAC [DIST_REFL]);;
e (ARITH_TAC);;
e (ASM_CASES_TAC `?u:real^3. u IN V1 /\ dist(u,p) < (&2)` );;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [NOT_EXISTS_THM]);;
e (PURE_REWRITE_TAC [DE_MORGAN_THM]);;
e (PURE_REWRITE_TAC [REAL_NOT_LT]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!u:real^3. u IN (V1:real^3->bool) ==> &2 <= dist (u,p:real^3)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [thm16]);;
e (UNDISCH_TAC `!y:real^3. (!x:real^3. x IN (V1:real^3->bool) ==> &2 <= dist (x,y)) ==> y IN V1`);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (USE_THEN "F1" (MP_TAC o SPEC `p:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `p:real^3 IN (V1:real^3->bool)` ASSUME_TAC);;
e (UNDISCH_TAC `!u:real^3. u IN (V1:real^3->bool) ==> &2 <= dist (u,p)`);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC[]);;
e (UNDISCH_TAC `~(p:real^3 IN (V1:real^3->bool))`);;
e (POP_ASSUM MP_TAC);;
e (SET_TAC[]);;

let thm17 = top_thm();;

(*---------------------------------------------------------------------------*)
g `!h1 h2 g1 g2. (h1 o h2) o (g1 o g2) = h1 o (h2 o g1) o g2`;;
e (REPEAT GEN_TAC);;
e (PURE_REWRITE_TAC [o_ASSOC]);;
e (ARITH_TAC);;


let MUL_o_ASSOC = top_thm();;

(*
g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) f b:real F X.(FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
  (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\ 
   f facet_of P /\
   F = {f|f facet_of P} 
   /\ (X = topological_component_yfan (vec 0,fan_of_polyhedron P))
   /\ (interior_point (vec 0) P)
   ==> (?(h: V -> X) (g: X -> V). (h o g = I /\ g o h = I))`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(?(h1: V -> F) (g1: F-> V). h1 o g1 = I /\ g1 o h1 = I)` ASSUME_TAC);;
e (ASM_MESON_TAC [CZZHBLI_1]);;
e (SUBGOAL_THEN `(?(h2: F -> WF) (g2: WF -> F). h2 o g2 = I /\ g2 o h2 = I)` ASSUME_TAC);;
e (ASM_MESON_TAC [AMHFNXP]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `(h2:F->WF) o (h1:V->F)`);;
e (EXISTS_TAC `(g1: F-> V) o (g2: WF -> F)`);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `((h2:F->WF) o (h1:V->F)) o ((g1: F-> V) o (g2: WF -> F)) =
 (h2 o (h1 o g1) o g2)` ASSUME_TAC);;
e (REWRITE_TAC [MUL_o_ASSOC]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `(h1:V->F) o (g1:F->V) = I`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (PURE_REWRITE_TAC [o_ASSOC]);;
e (PURE_REWRITE_TAC [I_O_ID]);;
e (UNDISCH_TAC `(h2: F -> WF)o(g2: WF -> F)= I`);;
e (REWRITE_TAC[]);;
e (SUBGOAL_THEN `((g1: F-> V) o (g2: WF -> F)) o ((h2:F->WF) o (h1:V->F)) =
 (g1 o (g2 o h2) o h1)` ASSUME_TAC);;
e (REWRITE_TAC [MUL_o_ASSOC]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `(g2: WF -> F) o (h2: F -> WF) = I`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (PURE_REWRITE_TAC [o_ASSOC]);;
e (PURE_REWRITE_TAC [I_O_ID]);;
e (UNDISCH_TAC `(g1: F-> V)o(h1:V->F)= I`);;
e (REWRITE_TAC[]);;

let V_TOPO_BIJ = top_thm();;


g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) f b:real F WF F_T.(FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
  (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\ 
   f facet_of P /\
   FANO (fan_of_polyhedron P) /\
   F = {f|f facet_of P} 
   /\ (WF = topological_component_yfan (vec 0,fan_of_polyhedron P))
   /\ (conforming (fan_of_polyhedron P))
   /\ (interior_point (vec 0) P) /\
   F_T = face_set_of_fan (fan_of_polyhedron P )
   ==> (?(h: V -> F_T) (g: F_T -> V). (h o g = I /\ g o h = I))`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(?(h1: V -> WF) (g1: WF -> V). h1 o g1 = I /\ g1 o h1 = I)` ASSUME_TAC);;
e (ASM_MESON_TAC[V_TOPO_BIJ]);;
e (SUBGOAL_THEN `(?(h2: WF -> F_T) (g2: F_T -> WF). h2 o g2 = I /\ g2 o h2 = I)`
ASSUME_TAC);;
e (UNDISCH_TAC `F_T = face_set_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
e (UNDISCH_TAC `(WF' = topological_component_yfan (vec 0,fan_of_polyhedron (P:real^3->bool)))`);;
e (UNDISCH_TAC `(conforming (fan_of_polyhedron (P:real^3->bool)))`);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron P)`);;
e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
e (ABBREV_TAC `V1 ={v | v extreme_point_of (P:real^3->bool)}`);;
e (ABBREV_TAC `E1 ={{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
e (MESON_TAC [UVPFEEP_1]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `(h2:WF->F_T) o (h1:V->WF)`);;
e (EXISTS_TAC `(g1: WF-> V) o (g2: F_T -> WF)`);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `((h2:WF->F_T) o (h1:V->WF)) o ((g1: WF-> V) o (g2: F_T -> WF)) =
 (h2 o (h1 o g1) o g2)` ASSUME_TAC);;
e (REWRITE_TAC [MUL_o_ASSOC]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `(h1:V->WF) o (g1:WF->V) = I`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (PURE_REWRITE_TAC [o_ASSOC]);;
e (PURE_REWRITE_TAC [I_O_ID]);;
e (UNDISCH_TAC `(h2: WF -> F_T)o(g2: F_T -> WF)= I`);;
e (REWRITE_TAC[]);;
e (SUBGOAL_THEN `((g1: WF-> V) o (g2: F_T -> WF)) o ((h2:WF->F_T) o (h1:V->WF)) =
 (g1 o (g2 o h2) o h1)` ASSUME_TAC);;
e (REWRITE_TAC [MUL_o_ASSOC]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `(g2: F_T -> WF) o (h2: WF -> F_T) = I`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (PURE_REWRITE_TAC [o_ASSOC]);;
e (PURE_REWRITE_TAC [I_O_ID]);;
e (UNDISCH_TAC `(g1: WF-> V)o(h1:V->WF)= I`);;
e (REWRITE_TAC[]);;

let V_FHYPER_BIJ = top_thm();;
*)
(*----------------------------------------------------------------------------*)

g `!(V:real^3 -> bool) (P:real^3->bool) X (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)).
  (FINITE V) /\ packing V /\       
  (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
  P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
  (polyhedron P) /\ (bounded P) /\  
  (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
  f1 o f2 = I /\ f2 o f1 = I /\ 
  IMAGE f1 V = X
 ==> (sum (V) (\v:real^3. sol (vec 0) (f1(v))) = sum (X) (\v. sol (vec 0) v ))`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(!x:real^3 y. x IN (V:real^3->bool) /\ y IN V /\  (f1:(real^3) -> (real^3->bool))  x = f1 y ==> x = y)` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) (x:real^3)= I x` ASSUME_TAC);;
e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) = I `);;
e (MESON_TAC[]);;
e (SUBGOAL_THEN `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> 
(real^3->bool))) (y:real^3)= I y` ASSUME_TAC);;
e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) = I `);;
e (MESON_TAC[]);;
e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) (x:real^3)= I x`);;
e (PURE_REWRITE_TAC [o_THM]);;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `I (y:real^3) = I x` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC[I_THM]);;
e (MP_TAC(ISPECL [`f1:(real^3)->(real^3->bool)`;`(\v:(real^3->bool). sol (vec 0) v)`;`(V:real^3->bool)`] SUM_IMAGE));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `sum (IMAGE (f1:(real^3)->(real^3->bool)) V) (\v:(real^3->bool). sol (vec 0) v) =
          sum (V:real^3->bool) ((\v. sol (vec 0) v) o f1)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `IMAGE (f1:(real^3)->(real^3->bool)) (V:real^3->bool) = (X:(real^3->bool)->bool)`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (SUBGOAL_THEN `(\v:real^3. sol (vec 0) (f1 v)) = ((\t. sol (vec 0) t) o f1)` ASSUME_TAC);;
e (REWRITE_TAC[FUN_EQ_THM]);;
e (GEN_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[]);;

let thm18 = top_thm();;

(*
g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) X F WF1 (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
   (FINITE V) /\ packing V      
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
   P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
   (polyhedron P) /\ (bounded P) /\ 
   (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
   (interior_point (vec 0) P) /\
   F = {f|f facet_of P} /\
   f1 o f2 = I /\ f2 o f1 = I /\
   f3 o f4 = I /\ f4 o f3 = I /\
   IMAGE f1 V = X  /\
   IMAGE f3 V = F
  ==> sum V (\v. &2 * pi - &2* &(CARD {u| u extreme_point_of (f3(v))}) * asn (cos (g_gun v))* sin(pi/ (&(CARD {u| u extreme_point_of f3(v)}))))  <= sum (V) (\v:real^3. sol (vec 0) (f1(v)))`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `!v:real^3. v IN V ==> (&2 * pi - &2* &(CARD {u| u extreme_point_of (f3(v))}) * asn (cos (g_gun v))* sin(pi/ (&(CARD {u| u extreme_point_of f3(v)}))))  <= (sol (vec 0) (f1(v)))` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;



type_of `!v:real^3. &2 * pi - &2* &(CARD {u| u extreme_point_of ((f3:(real^3) -> (real^3->bool))(v))}) * asn (cos (g_gun v))* sin(pi/ (&(CARD {u| u extreme_point_of f3(v)})))) <= 
(sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v)))`;;


search [`sum s f <= sum s g`];;

type_of `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) X F WF1 (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
   (FINITE V) /\ packing V      
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
   P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
   (polyhedron P) /\ (bounded P) /\ 
   (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
   (interior_point (vec 0) P) /\
   F = {f|f facet_of P} /\
   f1 o f2 = I /\ f2 o f1 = I /\
   f3 o f4 = I /\ f4 o f3 = I /\
   IMAGE f1 V = X  /\
   IMAGE f3 V = F`;;
type_of `sum (V) (\v:real^3. sol (vec 0) (f1(v)))`;;
search [`IMAGE`];;

g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) X WF1 (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
   (FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
   P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ 
   (polyhedron P) /\ (bounded P) /\ 
   (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
   (interior_point (vec 0) P)
   F_T = face_set_of_fan (fan_of_polyhedron P )
   /\ f1 o f2 = I /\ f2 o f1 = I
   /\ f3 o f4 = I /\ f4 o f3 = I
   /\ IMAGE f1 V = X
   /\ IMAGE f3 V = F_T
==> (!(v:real^3) f WF1 k. f facet_of s /\ f = { p | p dot v = g_fun v } INTER P /\ WF1 IN X /\ rcone_gt (vec 0) v (cos(g_fun v)) SUBSET WF1 /\ (k = CARD {u | u extreme_point_of f })  

g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) f b:real X F_T (f1:(real^3) -> (real^3#real^3->bool)) (f2:((real^3#real^3->bool))->(real^3)).
   (FINITE V) /\ packing V       
   /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
   P = INTERS {half_spaces g_fun u| (u IN V) /\
   (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\ 
   (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
   (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\ 
   F_T = face_set_of_fan (fan_of_polyhedron P ) /\
   F = {l | l facet_of P} /\
   /\ f1 o f2 = I /\ f2 o f1 = I 
   /\ IMAGE f1 V = F_T

  (~(vec 0 = u))} /\ 
   /\ (interior_point (vec 0) P)
   
    ==>
type_of `face_set_of_fan (fan_of_polyhedron P )`;;
type_of `facet_of`;;

type_of `extreme_point_of`;;
type_of `facet_of`;;
inverse;;
EXTREME_POINT_OF_LINEAR_IMAGE;;

search [`leaner f`];;

search [`extreme_point_of`];;


type_of `f facet_of P`;;
type_of `(?(g1:F -> V). h1 o g1 = I /\ g1 o h1 = I)/\
   (?(g2:F_T -> V). h2 o g2 = I /\ g2 o h2 = I) `;;
*)


(*---------------------------------------------------------------------------*)
(*Dart Bound*)

g `!(V:real^3 -> bool).(V SUBSET ball_annulus) ==> (!x:real^3. x IN V ==>  ~(vec 0 = x))`;;
e (GEN_TAC);;
e (PURE_REWRITE_TAC [ball_annulus;cball;ball;DIFF]);;
e (STRIP_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `x:real^3 IN {x | x IN {y | dist (vec 0,y) <= &2 * h0} /\
           ~(x IN {y | dist (vec 0,y) < &2})}` ASSUME_TAC);;
e (ASM_MESON_TAC [SUBSET]);;
e (ASM_CASES_TAC `vec 0 = x:real^3`);;
e (SUBGOAL_THEN `(vec 0):real^3 IN {x | x IN {y | dist (vec 0,y) <= &2 * h0} /\
           ~(x IN {y | dist (vec 0,y) < &2})}` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (REWRITE_TAC [DIST_REFL]);;
e (STRIP_TAC);;
e (ASM_MESON_TAC [ARITH_RULE `&0 < &2`]);;
e (ASM_REWRITE_TAC[]);;

let th54 = top_thm();;


g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V) /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\  ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> (interior_point (vec 0) P)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `INTERS {{p | u dot p < g_fun u}|(u IN (V:real^3->bool)) /\ (~(vec 0 = u))} SUBSET (P:real^3->bool)` ASSUME_TAC);;
e (ASM_REWRITE_TAC[half_spaces]);;
e (SUBGOAL_THEN `!u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u) ==> {p | u dot p < g_fun u} SUBSET {p | u dot p <= g_fun u}` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [SUBSET]);;
e (GEN_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (REWRITE_TAC [REAL_LT_IMP_LE]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (SUBGOAL_THEN ` !u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u)
          ==> INTERS {{p | u dot p < g_fun u} | u IN V /\ ~(vec 0 = u)} SUBSET {p | u dot p <= g_fun u}` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [INTERS;SUBSET;IN_ELIM_THM]);;
e (REPEAT STRIP_TAC);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]);;
e (POP_ASSUM (fun th -> (MP_TAC (SPEC `{p:real^3 | u dot p < g_fun u}` th))));;
e (REWRITE_TAC[]);;
e (SUBGOAL_THEN `?u':real^3. (u' IN V /\ ~(vec 0 = u')) /\
        {p | u dot p < g_fun u} = {p | u' dot p < g_fun u'}` ASSUME_TAC);;
e (EXISTS_TAC `u:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
e (REPEAT STRIP_TAC);;
e (POP_ASSUM (LABEL_TAC "F2"));; 
e (USE_THEN "F2" (MP_TAC o SPEC `x:real^3`));;
e (UNDISCH_TAC `u:real^3 dot x < g_fun u`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (ABBREV_TAC `(s:real^3->bool) = INTERS {{p:real^3 | u dot p < g_fun u} | u IN V /\ ~(vec 0 = u)}`);;
e (DISCH_THEN (LABEL_TAC "F3"));;
e (REWRITE_TAC [INTERS;SUBSET;IN_ELIM_THM]);;
e (REPEAT STRIP_TAC);;
e (REMOVE_THEN "F3" (MP_TAC o SPEC `u':real^3`));;
e (ASM_REWRITE_TAC[SUBSET]);;
e (STRIP_TAC);;
e (UNDISCH_TAC `x IN (s:real^3->bool)`);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (SUBGOAL_THEN `!u:real^3. u IN V /\ ~(vec 0 = u) ==> vec 0 IN ({p:real^3 | u dot p < g_fun u})` ASSUME_TAC);;
e (GEN_TAC);;
e (REPEAT STRIP_TAC);;
e (PURE_REWRITE_TAC [IN_ELIM_THM]);;
e (PURE_REWRITE_TAC [DOT_RZERO;g_fun]);;
e (SUBGOAL_THEN `&1 <= dist (vec 0,(u:real^3)) / &2` ASSUME_TAC);;
e (ASM_MESON_TAC[thm2]);;
e (SUBGOAL_THEN `&0 < &2` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `&1 / &2 <= (dist (vec 0,(u:real^3)) / &2) / &2` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [REAL_LE_DIV2_EQ]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ARITH_RULE `(dist (vec 0,(u:real^3)) / &2) / &2 = dist (vec 0,u) / &4`]);; 
e (STRIP_TAC);;
e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= &2 * h0` ASSUME_TAC);;
e (ASM_MESON_TAC [thm21]);;
e (SUBGOAL_THEN `&0 < &4` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `dist (vec 0,u:real^3) / &4 <= (&2 * h0) / &4` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [REAL_LE_DIV2_EQ]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ARITH_RULE `(&2 * h0) / &4 = h0 / &2`]);; 
e (STRIP_TAC);;
e (SUBGOAL_THEN `(&0 <= (pi / &6)) /\ ((pi / &6) <= pi)` ASSUME_TAC);;
e (MP_TAC PI_POS_LE);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `acs (cos (pi/ &6)) = (pi / &6)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ACS_COS]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [COS_PI6]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `-- &1 <= (dist (vec 0,u:real^3) / &4) /\ (dist (vec 0,u:real^3) / &4) < (sqrt (&3) / &2) /\ (sqrt (&3) / &2) <= &1` ASSUME_TAC);;
e (STRIP_TAC);;
e (UNDISCH_TAC `&1 / &2 <= dist (vec 0,u:real^3) / &4`);;
e (MP_TAC (ARITH_RULE `-- &1 <= &1 / &2`));;
e (ARITH_TAC);;
e (STRIP_TAC);;
e (UNDISCH_TAC `dist (vec 0,u:real^3) / &4 <= h0 / &2`);;
e (PURE_REWRITE_TAC [h0]);;
e (SUBGOAL_THEN `#1.26 / &2 < sqrt (&3) / &2` ASSUME_TAC);;
e (MP_TAC (ARITH_RULE `&0 < &2`));;
e (SUBGOAL_THEN `#1.26 < sqrt (&3)` ASSUME_TAC);;
e (SUBGOAL_THEN `#1.26 pow 2 < &3` ASSUME_TAC);;
e (ARITH_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_LT_RSQRT]);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [REAL_LT_DIV2_EQ]);;
e (POP_ASSUM MP_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `(&3) <= &2 pow 2` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `sqrt (&3) <= &2` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MP_TAC (ARITH_RULE `&0 <= &3 /\ &0 <= &2`));;
e (MESON_TAC [REAL_LE_LSQRT]);;
e (SUBGOAL_THEN `sqrt (&3) <= &1 * &2` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [ARITH_RULE `&2 = &1 * &2`]);;
e (POP_ASSUM MP_TAC);;
e (MP_TAC (ARITH_RULE `&0 < &2`));;
e (MESON_TAC [REAL_LE_LDIV_EQ]);;
e (SUBGOAL_THEN `acs (sqrt (&3) / &2) < acs (dist (vec 0,u:real^3) / &4)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [ACS_MONO_LT]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [REAL_SUB_LT]);;
e (SUBGOAL_THEN `vec 0 IN (INTERS {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)})` ASSUME_TAC);;
e (PURE_REWRITE_TAC [IN_INTERS]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC []);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `!u:real^3.  u IN (V:real^3->bool) /\ ~(vec 0 = u) ==> open {p:real^3 | u dot p < g_fun u}` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [OPEN_HALFSPACE_LT]);;
e (SUBGOAL_THEN `!u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u) ==> interior ({p:real^3 | u dot p < g_fun u}) = ({p:real^3 | u dot p < g_fun u}) ` ASSUME_TAC);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [INTERIOR_OPEN]);;
e (SUBGOAL_THEN `!u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u) ==>
  interior_point (vec 0) ({p:real^3 | u dot p < g_fun u}) ` ASSUME_TAC);;
e (GEN_TAC);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (UNDISCH_TAC `!u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u) ==> vec 0 IN {p | u dot p < g_fun u}`);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `vec 0 IN (interior ({p:real^3 | u dot p < g_fun u}))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_INTERIOR_CBALL]);;
e (REWRITE_TAC [interior_point]);;
e (STRIP_TAC);;
e (EXISTS_TAC `e:real`);;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC (ISPECL [`(vec 0):real^3`;`e:real`] BALL_SUBSET_CBALL));;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [SUBSET_TRANS]);;

e (MP_TAC (ISPECL [`{{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`] OPEN_INTERS));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `FINITE {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)}` ASSUME_TAC);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(\u:real^3. {p:real^3 | u dot p < g_fun u})`;`V:real^3->bool`] FINITE_IMAGE));;
e (ASM_REWRITE_TAC [IMAGE]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `{{p:real^3 | u dot p < g_fun u} | (u:real^3) IN (V:real^3->bool) /\ ~(vec 0 = u)} = ({y:real^3->bool | ?x:real^3. x IN V /\ y = {p | x dot p < g_fun x}})` ASSUME_TAC);;
e (REWRITE_TAC[EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `x':real^3`);;
e (SUBGOAL_THEN `~(vec 0 = x':real^3)` ASSUME_TAC);;
e (ASM_MESON_TAC [th54]);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [EXTENSION]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;

e (SUBGOAL_THEN `(!t:real^3->bool. t IN {{p | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)} ==> open t)` ASSUME_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `open (INTERS {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)})` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (SUBGOAL_THEN `(INTERS {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)}) SUBSET interior (P:real^3->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [INTERIOR_MAXIMAL]);;
e (SUBGOAL_THEN `(vec 0):real^3 IN (interior P)` ASSUME_TAC);;
e (UNDISCH_TAC `(vec 0):real^3 IN (INTERS {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)})`);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [SUBSET]);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_INTERIOR;interior_point]);;

let th51= top_thm();;


g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V) /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\  ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> fully_surrounded (fan_of_polyhedron P)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron;fully_surrounded]);;
e (STRIP_TAC);;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[th51]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [BSXAQBQ]);;

let th52 = top_thm();;

g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V) /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\  ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> conforming (fan_of_polyhedron P)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[th52]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
e (REWRITE_TAC [PIIJBJK]);;

let th53 = top_thm();;

g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V)  /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\ 
~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> 
 (dart (hypermap_of_fan (fan_of_polyhedron P))) = dart_of_fan (fan_of_polyhedron P)`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [JLIGZGS]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (REWRITE_TAC [GSYM FANO_OF_FAN]);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`FST (fan_of_polyhedron (P:real^3 -> bool))`;`SND (fan_of_polyhedron (P:real^3 -> bool))`] COMPONENTS_HYPERMAP_OF_FAN));;
e (ASM_REWRITE_TAC[fan_of_polyhedron]);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;

let DART_OF_HYPERMAP_FAN = top_thm();;


let FULLY_SURROUND_IS_NON_ISOLATED_FAN2 = prove(`!(V:real^3->bool) (E:(real^3->bool)->bool).
FANO(V,E) /\ (!v. v IN V ==> CARD (set_of_edge v V E) >1)
==> dart2_of_fan (V,E) = {}`,REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`]THEN REWRITE_TAC[dart2_of_fan;IN_ELIM_THM] THEN STRIP_TAC THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES]) THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;

g `!(V:real^3->bool) (E:(real^3->bool)->bool).
FANO(V,E) /\ (!x:real^3#real^3. x IN dart_of_fan (V,E) ==> CARD (set_of_edge (FST x) V (E:(real^3->bool)->bool)) > 1)
==> dart_of_fan (V,E) = dart1_of_fan (V,E)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (STRIP_TAC);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `x:real^3#real^3`));;
e (ASM_REWRITE_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [dart_of_fan;UNION;IN_ELIM_THM]);;
e (STRIP_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `CARD (set_of_edge (FST (x:real^3#real^3)) (V:real^3->bool) (E:(real^3->bool)->bool)) = 0` ASSUME_TAC);;
e (ASM_REWRITE_TAC[CARD_CLAUSES]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (ARITH_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [dart1_of_fan]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (EXISTS_TAC `v:real^3`);;
e (EXISTS_TAC `w:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[dart1_of_fan;dart_of_fan;IN_UNION]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;

let FULLY_SURROUND_IS_NON_ISOLATED_FAN3 = top_thm();;

let DARTSET_FULLY_SURROUNDED_IS_NON_ISOLATED_FAN2 = prove (`!(V:real^3->bool) (E:(real^3->bool)->bool).
FANO(V,E) /\ (!v. v IN V ==>CARD (set_of_edge v V E) >1)
==> dart_of_fan (V,E) = dart1_of_fan (V,E)`,REPEAT STRIP_TAC THEN MRESA_TAC FULLY_SURROUND_IS_NON_ISOLATED_FAN2[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC [dart2_of_fan] THEN STRIP_TAC THEN ASM_REWRITE_TAC[dart_of_fan;dart1_of_fan] THEN SET_TAC[]);;


let AZIM_PI = prove(`!(V:real^3 -> bool) (E:(real^3->bool)->bool) v:real^3 w . v IN V /\ (~(CARD (set_of_edge v V E) > 1)) ==> azim_dart (V,E) (v,w) = &2 * pi`,REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN REWRITE_TAC [azim_dart;azim_fan] THEN ASM_CASES_TAC `v:real^3 = w` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[]);;

let AZIM_PI1 = prove(`!(V:real^3 -> bool) (E:(real^3->bool)->bool) (x:real^3#real^3) . (FST x) IN V /\ (~(CARD (set_of_edge (FST x) V E) > 1)) ==> azim_dart (V,E) ((FST x),(SND x)) = &2 * pi`,REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN REWRITE_TAC [azim_dart;azim_fan] THEN ASM_CASES_TAC `(FST (x:real^3#real^3)) = (SND x)` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[]);;

g `!(V:real^3 -> bool) (E:(real^3->bool)->bool) (x:real^3#real^3).fully_surrounded (V,E) /\ FANO (V,E) /\ x IN dart_of_fan (V,E) ==> CARD (set_of_edge (FST x) V (E:(real^3->bool)->bool)) > 1`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [fully_surrounded]);;
e (STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM(LABEL_TAC "F1"));;
e (REPEAT STRIP_TAC);;
e (ASM_CASES_TAC `CARD (set_of_edge (FST (x:real^3#real^3)) (V:real^3->bool) (E:(real^3->bool)->bool)) > 1`);;
e (ASM_REWRITE_TAC[]);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `x:real^3#real^3`));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FST(x:real^3#real^3)`;`SND (x:real^3#real^3)`]AZIM_PI ));;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `FST (x:real^3#real^3) IN (V:real^3->bool)` ASSUME_TAC);;
e (UNDISCH_TAC `(x:real^3#real^3) IN dart_of_fan ((V:real^3->bool),(E:(real^3->bool)->bool))`);;
e (ONCE_REWRITE_TAC [ARITH_RULE `(x:real^3#real^3) = (FST x, SND x)`]);;
e (PURE_REWRITE_TAC [dart_of_fan]);;
e (REWRITE_TAC [UNION]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `UNIONS (E:(real^3->bool) -> bool) SUBSET (V:real^3->bool)` ASSUME_TAC);;
e (UNDISCH_TAC `FANO (V:real^3->bool,E:(real^3->bool) -> bool)`);;
e (REWRITE_TAC [FANO]);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [UNIONS;SUBSET]);;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `v:real^3 IN {v:real^3,w:real^3}` ASSUME_TAC);;
e (SET_TAC[]);;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `azim_dart (V:real^3->bool,E:(real^3->bool) -> bool) (x:real^3#real^3) < pi` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM SUBST1_TAC);;
e (MP_TAC PI_POS);;
e (ARITH_TAC);;

let FULLY_EDGE  = top_thm();;

g `!(V:real^3 -> bool) (E:(real^3->bool)->bool).fully_surrounded (V,E) /\ FANO(V,E) ==> (!x. x IN dart_of_fan (V,E) ==> CARD (set_of_edge (FST x) V E) > 1)`;;
e (REPEAT GEN_TAC);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC [FULLY_EDGE]);;

let FULLY_EDGE1 = top_thm();;

g `!(V:real^3 -> bool) (E:(real^3->bool)->bool).fully_surrounded (V,E) /\ FANO(V,E) ==> dart_of_fan (V,E) = dart1_of_fan (V,E)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(!x. x IN dart_of_fan ((V:real^3 -> bool),(E:(real^3->bool)->bool)) ==> CARD (set_of_edge (FST x) V E) > 1)` ASSUME_TAC);;
e (ASM_MESON_TAC [FULLY_EDGE1]);;
e (ASM_MESON_TAC [FULLY_SURROUND_IS_NON_ISOLATED_FAN3]);;

let FULLY_SURROUNDED_IMP_DART = top_thm();;


g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V) /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\  ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> CARD (dart (hypermap_of_fan (fan_of_polyhedron P))) <= 
   (6*(CARD (face_set_of_fan (fan_of_polyhedron P)))-12)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `conforming (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th53]);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [JLIGZGS]);;
e (SUBGOAL_THEN `connected_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ASM_MESON_TAC [WGVWSKE]);;
e (SUBGOAL_THEN `planar_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ASM_MESON_TAC [GGRLKHP]);;
e (SUBGOAL_THEN `plain_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ASM_MESON_TAC [PLAIN_HYPERMAP]);;
e (SUBGOAL_THEN `dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))) =
             dart_of_fan (fan_of_polyhedron P)` ASSUME_TAC);;
e (ASM_MESON_TAC [DART_OF_HYPERMAP_FAN]);;
e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3->bool))`);;
e (REWRITE_TAC [fan_of_polyhedron;conforming]);;
e (MESON_TAC[]);;
e (SUBGOAL_THEN `!x:real^3#real^3. x IN dart (hypermap_of_fan (fan_of_polyhedron P)) ==> ~(edge_map (hypermap_of_fan (fan_of_polyhedron P)) x = x) /\ 3 <= CARD (node (hypermap_of_fan (fan_of_polyhedron P)) x)` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `x IN dart_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (MP_TAC (ISPECL [`{v | v extreme_point_of (P:real^3->bool)}`;`{{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`] FULLY_SURROUNDED_IMP_DART));;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`FANO (fan_of_polyhedron (P:real^3->bool))`);;
e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`fully_surrounded (fan_of_polyhedron (P:real^3->bool))`);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `FAN (vec 0,fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3->bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
e (MESON_TAC [FANO_OF_FAN]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `edge_map (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))) = e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
e (MESON_TAC [COMPONENTS_HYPERMAP_OF_FAN]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (SUBGOAL_THEN `e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool)) x  = e_fan_pair (fan_of_polyhedron P) x` ASSUME_TAC);;
e (UNDISCH_TAC `x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
e (REWRITE_TAC [e_fan_pair_ext]);;
e (ARITH_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
e (MESON_TAC [E_HAS_NO_FIXED_POINTS_IN_D1]);;
e (SUBGOAL_THEN `surrounded_node (fan_of_polyhedron (P:real^3->bool)) (FST (x:real^3#real^3))` ASSUME_TAC);;
e (REWRITE_TAC [fan_of_polyhedron;surrounded_node]);;
e (GEN_TAC);;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
e (SUBGOAL_THEN `(!x. x IN dart_of_fan (fan_of_polyhedron (P:real^3->bool)) ==> azim_dart (fan_of_polyhedron (P:real^3->bool)) x < pi)` ASSUME_TAC);;
e (UNDISCH_TAC `fully_surrounded (fan_of_polyhedron (P:real^3->bool))`);;
e (REWRITE_TAC [fan_of_polyhedron;fully_surrounded]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `x':real^3#real^3`));;
e (MESON_TAC[]);;
e (MP_TAC (ISPECL [`{v | v extreme_point_of (P:real^3->bool)}`;`{{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`]SURROUNDED_IMP_CARD_NODE_GE_3));;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`FAN (vec 0,fan_of_polyhedron (P:real^3->bool))`);;
e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`surrounded_node (fan_of_polyhedron (P:real^3->bool)) (FST (x:real^3#real^3))`);;
e (REWRITE_TAC [GE]);;

e (REWRITE_TAC [fan_of_polyhedron;face_set_of_fan]);;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;

e (MP_TAC (ISPECL [`hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))`]lemmaTGJISOK));;
e (REWRITE_TAC [number_of_faces]);;
e (ASM_REWRITE_TAC[]);;


let th5 = top_thm();;

(*----------------------------------------------------------------------------*)
(* proof CARD V = CARD {f|f facet_of V}*)

g `!(V:real^3 -> bool) (P:real^3 -> bool) F.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus) /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ F = {f|f facet_of P}  ==> (CARD V) = (CARD F)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F')` ASSUME_TAC);;
e (ASM_MESON_TAC [CZZHBLI_1]);;
e (POP_ASSUM MP_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(!(x:real^3) y. x IN (V:real^3->bool) /\ y IN V /\ (h:(real^3) -> (real^3->bool)) x = h y ==> x = y)` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) x:real^3 = I x` ASSUME_TAC);;
e (UNDISCH_TAC `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (SUBGOAL_THEN `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) y:real^3 = I y` ASSUME_TAC);;
e (UNDISCH_TAC `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `I (y:real^3) = I x` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC[I_THM]);;
e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3) -> (real^3->bool)) (V:real^3->bool)) = CARD V ` ASSUME_TAC);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [CARD_IMAGE_INJ]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ARITH_TAC);;

let CARD_1 = top_thm();;

(*---------------------------------------------------------------------------*)

(*Proof CARD {f|f facet_of V} = CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) *)

g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P)) ==> FINITE F`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F')` ASSUME_TAC);;
e (ASM_MESON_TAC [CZZHBLI_1]);;
e (POP_ASSUM MP_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(h:(real^3) -> (real^3->bool))`;`V:real^3->bool`]FINITE_IMAGE));;
e (ASM_REWRITE_TAC[]);;

let FINITE_FACE_SET = top_thm();;

g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P))  ==> CARD F = CARD WF `;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `interior_point (vec 0) (P:real^3 -> bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN `(?(h:(real^3->bool) -> (real^3->bool)) (g: (real^3->bool) -> (real^3->bool)). h o g = I /\ g o h = I /\ IMAGE h F' = WF')` ASSUME_TAC);;
e (ASM_MESON_TAC [AMHFNXP]);;
e (POP_ASSUM MP_TAC);;
e (STRIP_TAC);; 
e (SUBGOAL_THEN `(!(x:real^3->bool) y. x IN (F':(real^3->bool)->bool) /\ y IN F' /\ (h:(real^3->bool) -> (real^3->bool)) x = h y ==> x = y)` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;

e (SUBGOAL_THEN `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) x:real^3->bool = I x` ASSUME_TAC);;
e (UNDISCH_TAC `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (SUBGOAL_THEN `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) y:real^3->bool = I y` ASSUME_TAC);;
e (UNDISCH_TAC `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `I (y:real^3->bool) = I x` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC[I_THM]);;
e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3->bool) -> (real^3->bool)) (F':(real^3->bool)->bool)) = CARD F' ` ASSUME_TAC);;
e (SUBGOAL_THEN `FINITE (F':(real^3->bool) -> bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [FINITE_FACE_SET]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [CARD_IMAGE_INJ]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ARITH_TAC);;

let CARD_2 = top_thm();;


(*----------------------------------------------------------------------------*)

(*Proof CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) =
   CARD (face_set_of_fan (fan_of_polyhedron V))  *)

g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P)) /\ (F_T = face_set_of_fan (fan_of_polyhedron P)) 
==> FINITE WF`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `FINITE (F':(real^3->bool)->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [FINITE_FACE_SET]);;
e (SUBGOAL_THEN `interior_point (vec 0) (P:real^3 -> bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;

e (SUBGOAL_THEN `(?(h:(real^3->bool) -> (real^3->bool)) (g: (real^3->bool) -> (real^3->bool)). h o g = I /\ g o h = I /\ IMAGE h F' = WF')` ASSUME_TAC);;
e (ASM_MESON_TAC [AMHFNXP]);;
e (POP_ASSUM MP_TAC);;
e (STRIP_TAC);; 
e (MP_TAC (ISPECL [`(h:(real^3->bool) -> (real^3->bool))`;`F':(real^3->bool)->bool`]FINITE_IMAGE));;
e (ASM_REWRITE_TAC[]);;

let FINITE_TOPO_SET = top_thm();;


g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P)) /\ (F_T = face_set_of_fan (fan_of_polyhedron P)) ==> CARD WF = CARD F_T`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN ` FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [JLIGZGS]);;
e (SUBGOAL_THEN `(conforming (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
e (ASM_MESON_TAC [th53]);;
e (SUBGOAL_THEN `(?(h: (real^3->bool) -> (real^3#real^3->bool)) (g: (real^3#real^3->bool) -> (real^3->bool)). h o g = I /\ g o h = I /\ IMAGE h (WF':(real^3->bool)->bool) = (F_T:(real^3#real^3->bool)->bool))` ASSUME_TAC);;
e (REPEAT (POP_ASSUM MP_TAC));;
e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC [UVPFEEP_1]);;

e (POP_ASSUM MP_TAC);;
e (STRIP_TAC);; 
e (SUBGOAL_THEN `(!(x:real^3->bool) y. x IN (WF':(real^3->bool)->bool) /\ y IN WF' /\ (h:(real^3->bool) -> (real^3#real^3->bool)) x = h y ==> x = y)` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;

e (SUBGOAL_THEN `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) x:real^3->bool = I x` ASSUME_TAC);;
e (UNDISCH_TAC `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (SUBGOAL_THEN `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) y:real^3->bool = I y` ASSUME_TAC);;
e (UNDISCH_TAC `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) = I`);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [o_THM]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `I (y:real^3->bool) = I x` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC[I_THM]);;
e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3->bool) -> (real^3#real^3->bool)) (WF':(real^3->bool)->bool)) = CARD WF' ` ASSUME_TAC);;
e (SUBGOAL_THEN `FINITE (WF':(real^3->bool) -> bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [FINITE_TOPO_SET]);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [CARD_IMAGE_INJ]);;
e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ARITH_TAC);;

let CARD_3 = top_thm();;


(*----------------------------------------------------------------------------*)

g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P)) /\ (F_T = face_set_of_fan (fan_of_polyhedron P))   ==> CARD V =  CARD F_T`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(CARD (V:real^3 -> bool)) = (CARD (F':(real^3->bool)->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [CARD_1]);;
e (SUBGOAL_THEN `(CARD (F':(real^3->bool)->bool)) = CARD (WF':(real^3->bool)->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [CARD_2]);;
e (SUBGOAL_THEN `CARD (WF':(real^3->bool)->bool) =  CARD (F_T:(real^3#real^3->bool)->bool) ` ASSUME_TAC);;
e (ASM_MESON_TAC [CARD_3]);;
e (ASM_MESON_TAC[]);;

let CARD_4 = top_thm();;

  
(*---------------------------------------------------------------------------*)
g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V)  /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\ 
~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==>
nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))
 = CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))`]card_partition_formula));;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `face_map (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))`));;
e (REWRITE_TAC [face_map_and_darts]);;
e (STRIP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron;face_set_of_fan]);;
e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
e (REWRITE_TAC [face_set]);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;

let CARD_5 = top_thm();;

(*--------------------------------------------------------------------------*)

g `!(V:real^3 -> bool) (P:real^3 -> bool) F WF.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus)/\ (~(lmfun_ineq_center V)) /\ F = {f|f facet_of P} /\
(weakly_saturated V r r') /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) /\ WF = (topological_component_yfan (vec 0,fan_of_polyhedron P)) /\ (F_T = face_set_of_fan (fan_of_polyhedron P))   ==> 
nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))
 <= (6*(CARD V)-12)`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;

(*SUBGOAL 1*)
e (SUBGOAL_THEN `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3 -> bool))) (\u:real^3#real^3->bool. (CARD u))
 = CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))` ASSUME_TAC);; 
e (ASM_MESON_TAC[CARD_5]);;

(*SUBGOAL 2*)
e (SUBGOAL_THEN `CARD (V:real^3 -> bool) =  CARD (F_T:(real^3#real^3->bool)->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [CARD_4]);;
(*SUBGOAL 3*)
e (SUBGOAL_THEN `conforming (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th53]);;
e (SUBGOAL_THEN `CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))) <= 
   (6*(CARD (face_set_of_fan (fan_of_polyhedron P)))-12)` ASSUME_TAC);;
e (ASM_MESON_TAC[th5]);;
e (UNDISCH_TAC `CARD (V:real^3->bool) = CARD (F_T:(real^3#real^3->bool)->bool)`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `F_T = face_set_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (UNDISCH_TAC `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u) =
      CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
e (ASM_REWRITE_TAC[]);;

let th6 = top_thm();;

(*--------------------------------------------------------------------------*)
let th7_concl = `!V X.FINITE V /\ packing V /\
    V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\
   X = topological_component_yfan (vec 0,fan_of_polyhedron P)

==> &4 * pi = sum X (\v. sol (vec 0) (v))`;;

let th7 = new_axiom th7_concl;;


(*----------------------------------------------------------------------------*)
let th8_concl = `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f3 o f4 = I /\ 
    IMAGE f3 V = F
  ==> 
  sum V (\v. reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)}))) <= (sum (V) (\v:real^3. sol (vec 0) (f1(v))))`;;

let th8 = new_axiom th8_concl;;

g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V) /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\  ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==> FINITE {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [half_spaces]);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(\u:real^3. {p:real^3 | u dot p <= g_fun u})`;`V:real^3->bool`] FINITE_IMAGE));;
e (ASM_REWRITE_TAC [IMAGE]);;
e (SUBGOAL_THEN `{{p:real^3 | u dot p <= g_fun u} | (u:real^3) IN (V:real^3->bool) /\ ~(vec 0 = u)} = ({y:real^3->bool | ?x:real^3. x IN V /\ y = {p | x dot p <= g_fun x}})` ASSUME_TAC);;
e (REWRITE_TAC[EXTENSION]);;
e (GEN_TAC);;
e (EQ_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `u:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (GEN_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `x':real^3`);;
e (SUBGOAL_THEN `~(vec 0 = x':real^3)` ASSUME_TAC);;
e (ASM_MESON_TAC [th54]);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC [EXTENSION]);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;

let FINITE_HALF_SPACES = top_thm();;

g `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    ~(lmfun_ineq_center V) /\ (weakly_saturated V r r') /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f3 o f4 = I /\ 
    IMAGE f3 V = F
==> (!u. u IN V ==> f3 u = {p | p dot u = g_fun u} INTER P)`;;


e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`P:real^3->bool`] POLYHEDRON_INTER_AFFINE_MINIMAL));;
e (UNDISCH_TAC `polyhedron (P:real^3->bool)`);;
e (STRIP_TAC);;
e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`P:real^3->bool`;`{half_spaces g_fun u | (u:real^3) IN (V:real^3->bool) /\ ~(vec 0 = u)}`;`(f4:((real^3->bool))->(real^3))`;`g_fun o (f4:((real^3->bool))->(real^3))`]FACET_OF_POLYHEDRON_EXPLICIT));;

e (DISCH_THEN (LABEL_TAC "F1"));;


e (REMOVE_THEN "F1" (MP_TAC o SPECL `{half_spaces g_fun u | (u:real^3) IN (V:real^3->bool) /\ ~(vec 0 = u)}`));;


e (SUBGOAL_THEN `FINITE {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}` ASSUME_TAC);;
e (ASM_MESON_TAC [FINITE_HALF_SPACES]);;

e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`);;
e (STRIP_TAC);;
e (FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th]));;
search [`affine hull P INTER P`];;
ARITH_RULE `affine hull P INTER P`;;
e (ASM_REWRITE_TAC[INTER]);;

search [`FINITE P`];;


type_of `{half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`;;
type_of `g_fun(f4:((real^3->bool))->(real^3))`;;
type_of `g_fun`;;

g `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f3 o f4 = I /\ 
    IMAGE f3 V = F
  ==>
  (!v:real^3. v IN V ==> reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})) <=  sol (vec 0) (f1(v)))`;;


OPEN_RCONE_GT;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(?r:real. r > &0 /\ ball (vec 0,r) SUBSET (P:real^3->bool))` ASSUME_TAC);;
e (EXISTS_TAC `r'':real`);;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC (ISPECL [`(f3:(real^3) -> (real^3->bool))`;`V:real^3->bool`;`v:real^3`] FUN_IN_IMAGE));;
e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`(f1:(real^3) -> (real^3->bool))`;`V:real^3->bool`;`v:real^3`] FUN_IN_IMAGE));;
e (ONCE_ASM_REWRITE_TAC[IN]);;
e (ONCE_ASM_REWRITE_TAC[IN]);;
e (ONCE_ASM_REWRITE_TAC[IN]);;
e (ONCE_ASM_REWRITE_TAC[IN]);;
e (STRIP_TAC);;


FACET_OF_POLYHEDRON_EXPLICIT;;

e (MP_TAC (ISPECL [`P:real^3->bool`;`(f3:(real^3) -> (real^3->bool))(v:real^3)`]
FACET_OF_POLYHEDRON));;
e (ASM_REWRITE_TAC[]);;
e (MP_TAC (ISPECL [`P:real^3->bool`;`(f3:(real^3) -> (real^3->bool))(v:real^3)`;
`v:real^3`;`g_fun (v:real^3)`;`(f1:(real^3) -> (real^3->bool)) (v:real^3)`;`cos (g_fun (v:real^3))`;`(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v:real^3)})`] GOTCJAH));;
e (ASM_REWRITE_TAC []);;
e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`);;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]));;
e (STRIP_TAC);;
e (REWRITE_TAC [reg]);;



FACET_OF_POLYHEDRON_EXPLICIT;;
e (DISCH_THEN (CHOOSE_TAC [`v:real^3`]));;
e (POP_ASSUM (X_CHOOSE_TAC `g_fun (u:real^3)`));;
help "X_CHOOSE_TAC";;

search [`rcone`];;

e (SUBGOAL_THEN `(f3:(real^3) -> (real^3->bool))(v:real^3) IN F'` ASSUME_TAC);;

search [`f (v) IN V`];;

FUN_IN_IMAGE;;
e (GEN_TAC);;


search [`x IN V /\ f x`];;
type_of `extreme_point_of`;;
search [`f o g = I`];;


g `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f4 o f3 = I /\ 
    IMAGE f3 V = F
  ==> 
  sum V (\v. reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)}))) <= (sum (V) (\v:real^3. sol (vec 0) (f1(v))))`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;

GOTCJAH;;
facet_of;;

(*----------------------------------------------------------------------------*)

g `!a b c e f:real. a = b + c /\ b = e - f ==> a = e - f + c`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;

let th91 = top_thm();;

let th92_T = `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f3 o f4 = I /\ 
    IMAGE f3 V = F 
    ==> sum V (\v.(&(CARD {u | u extreme_point_of f3(v)}))) = (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))`;;

let th92 =new_axiom th92_T;;

g `!(P:real^3->bool) v b. (polyhedron P) /\ (bounded P) ==> (!f.(f facet_of P) /\ f = { p | p dot v = b } INTER P ==>
   (CARD {u | u extreme_point_of f}) = (CARD (edges f)))`;;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [edges]);;
dart1_of_fan;;
e (REWRITE_TAC [



g `!(V:real^3->bool) X P F F_T.
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\ 
    ~(lmfun_ineq_center V) /\ 
    (weakly_saturated V r r')
    ==> nsum F (\v.((CARD {u | u extreme_point_of v}))) = (nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u)))`;;


e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th52]);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [JLIGZGS]);;
e (SUBGOAL_THEN `dart_of_fan (fan_of_polyhedron (P:real^3->bool)) = dart1_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (MESON_TAC [FULLY_SURROUNDED_IMP_DART]);;
e (SUBGOAL_THEN `(dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) = dart_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[DART_OF_HYPERMAP_FAN]);;
e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;
e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;


e (REWRITE_TAC [fan_of_polyhedron;dart1_of_fan]);;
e (SUBGOAL_THEN `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u) =
             CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` ASSUME_TAC);;
e (ASM_MESON_TAC [CARD_5]);;



CARD_5;;
e (REWRITE_TAC [IN_ELIM_THM]);;

e (REWRITE_TAC [dart]);;
KREIN_MILMAN_POLYTOPE;;
verticesface_of;;
EXTREME_POINT_OF_FACE;;
DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET;;
search [`vertices`];;
       
card_partition_formula;;
CARD_5;;
th8;;
edge_map_and_darts;;

let lemma_edge_from_dart = prove( `!H:(A)hypermap x:A u:A->bool. u IN edge_set H /\ x IN u ==> u = edge H x`, 
  REPEAT GEN_TAC THEN 
  DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "F1") (LABEL_TAC "F2")) THEN 
  USE_THEN "F1" (MP_TAC o MATCH_MP lemma_edge_representation) THEN 
  DISCH_THEN (X_CHOOSE_THEN `y:A` (SUBST_ALL_TAC o CONJUNCT2)) THEN 
  USE_THEN "F2" (fun th -> REWRITE_TAC [MATCH_MP lemma_edge_identity th]));;

let lemma_face_from_dart = prove( `!H:(A)hypermap x:A u:A->bool. u IN face_set H /\ x IN u ==> u = face H x`, 
  REPEAT GEN_TAC THEN 
  DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "F1") (LABEL_TAC "F2")) THEN 
  USE_THEN "F1" (MP_TAC o MATCH_MP lemma_face_representation) THEN 
  DISCH_THEN (X_CHOOSE_THEN `y:A` (SUBST_ALL_TAC o CONJUNCT2)) THEN 
  USE_THEN "F2" (fun th -> REWRITE_TAC [MATCH_MP lemma_face_identity th]));;

g `!(V:real^3->bool) X P F F_T.
    FINITE V /\ packing V /\ weakly_saturated V r r' /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\         
    ~(lmfun_ineq_center V) /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P )
==> nsum F (\v.((CARD (edges v)))) = (CARD (dart (hypermap_of_fan(fan_of_polyhedron P))))`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (MP_TAC (ISPECL [`hypermap_of_fan(fan_of_polyhedron (P:real^3->bool))`]DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET));;
e (STRIP_TAC);;
e (SUBGOAL_THEN `CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) =
     CARD (UNIONS (face_set (hypermap_of_fan (fan_of_polyhedron P))))` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `FINITE (face_set (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` ASSUME_TAC);;
e (MP_TAC (ISPECL [`hypermap_of_fan(fan_of_polyhedron (P:real^3->bool))`]FINITE_HYPERMAP_ORBITS));; 
e (SIMP_TAC[]);;
e (SUBGOAL_THEN `(!t:real^3#real^3->bool. t IN (face_set (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) ==> FINITE t)` ASSUME_TAC);;
e (REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM face;FACE_FINITE]);;
e (SUBGOAL_THEN `(!t u. t IN (face_set (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) /\ u IN (face_set (hypermap_of_fan (fan_of_polyhedron (P)))) /\ ~(t = u) ==> t INTER u = {})` ASSUME_TAC);;
e (REPEAT GEN_TAC);;
e (DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "G1") (CONJUNCTS_THEN2 (LABEL_TAC "G2") (MP_TAC))));;
e (ONCE_REWRITE_TAC [GSYM CONTRAPOS_THM]);;
e (REWRITE_TAC[]);;
e (REWRITE_TAC [GSYM MEMBER_NOT_EMPTY;IN_INTER]);;
e (STRIP_TAC);;
e (POP_ASSUM (fun th -> USE_THEN "G2" (fun th1 -> REWRITE_TAC [MATCH_MP lemma_face_from_dart (CONJ th1 th)])));;
e (POP_ASSUM (fun th -> USE_THEN "G1" (fun th1 -> REWRITE_TAC [MATCH_MP lemma_face_from_dart (CONJ th1 th)])));;
e (MP_TAC (MATCH_MP card_partition_formula (ISPEC `( (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` face_map_and_darts)));;
e (REWRITE_TAC [GSYM face_set]);;
CARD_5;;
e (STRIP_TAC);;

e (POP_ASSUM MP_TAC);;
e (ASM_REWRITE_TAC[]);;

g `!(V:real^3->bool) X P F F_T.
    FINITE V /\ packing V /\ weakly_saturated V r r' /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\         
    ~(lmfun_ineq_center V) /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P )
==> nsum F (\v.((CARD (edges v)))) = (CARD (dart (hypermap_of_fan(fan_of_polyhedron P))))`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (REWRITE_TAC [edges]);;
e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th52]);;
e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [th51]);;
e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC [JLIGZGS]);;
e (SUBGOAL_THEN `dart_of_fan (fan_of_polyhedron (P:real^3->bool)) = dart1_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (MESON_TAC [FULLY_SURROUNDED_IMP_DART]);;
e (SUBGOAL_THEN `(dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) = dart_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[DART_OF_HYPERMAP_FAN]);;
e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;
e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
e (UNDISCH_TAC `F' = {l | l facet_of (P:real^3->bool)}`);;
e (DISCH_TAC);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
e (MP_TAC (ISPECL [`(dart1_of_fan ((fan_of_polyhedron (P:real^3->bool))))`]card_partition_formula));;
e (DISCH_THEN (LABEL_TAC "F1"));;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool))`));;
e (SUBGOAL_THEN `FAN(vec 0,fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
e (UNDISCH_TAC `FANO (fan_of_polyhedron  (P:real^3->bool))`);;
e (REWRITE_TAC [fan_of_polyhedron]);;
e (MESON_TAC [FANO_OF_FAN]);;
e (SUBGOAL_THEN `FINITE (dart_of_fan (fan_of_polyhedron (P:real^3->bool)))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC THEN REWRITE_TAC [fan_of_polyhedron]);;
e (REWRITE_TAC [FINITE_DART_OF_FAN]);;
e (SUBGOAL_THEN `FINITE (dart1_of_fan (fan_of_polyhedron (P:real^3->bool)))` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
e (SUBGOAL_THEN `e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool)) permutes dart1_of_fan (fan_of_polyhedron P)` ASSUME_TAC);;
e (REWRITE_TAC [fan_of_polyhedron;E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
e (REWRITE_TAC [set_of_orbits;fan_of_polyhedron;e_fan_pair_ext]);;

e (STRIP_TAC);;
e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
e (UNDISCH_TAC `dart_of_fan (fan_of_polyhedron (P:real^3->bool)) = dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN;;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (REWRITE_TAC [fan_of_polyhedron;dart1_of_fan]);;
e (REWRITE_TAC [edge_of]);;

search [`convex hull {v', w'} face_of P`];;
e (REWRITE_TAC [IN_ELIM_THM]);;

e (REWRITE_TAC weakly_saturated V r r'
e (REWRITE_TAC [dart]);;


search [`CARD (UNIONS s)`];;


g `!(V:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
    FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
    X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
    F = {l | l facet_of P} /\
    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
    f1 o f2 = I /\ f2 o f1 = I /\ 
    IMAGE f1 V = X /\
    f3 o f4 = I /\ f3 o f4 = I /\ 
    IMAGE f3 V = F
    /\ (!v. v IN V ==>  #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of f3(v)})) +  #0.506 * lmfun (hl [vec 0; v])
       <= reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})))
==>

#0.591* (&(CARD V)) - #0.0331 * (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))  + #0.506 * (sum V (\v. lmfun (hl [vec 0; v]))) <=  sum V (\v. reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})))`;; 

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (SUBGOAL_THEN `!v:real^3. v IN (V:real^3->bool)
          ==> (\v:real^3. #0.591 - #0.0331 * &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}) + #0.506 * lmfun (hl [vec 0; v])) v <= (\v:real^3. reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)}))) v` ASSUME_TAC);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (REMOVE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) + #0.506 * lmfun (hl [vec 0; v])) <= sum V (\v. reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)}))) ` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (MESON_TAC [SUM_LE]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) + #0.506 * lmfun (hl [vec 0; v])) = sum V (\v. #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of f3(v)}))) + sum V (\v. #0.506 * lmfun (hl [vec 0; v]))` ASSUME_TAC);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (REWRITE_TAC [SUM_ADD]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))) = 
sum (V:real^3->bool) (\v. #0.591) - sum V (\v. #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})))` ASSUME_TAC);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (REWRITE_TAC [SUM_SUB]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) + 
       #0.506 * lmfun (hl [vec 0; v]))  = sum (V) (\v. #0.591) - sum V (\v. #0.0331 * (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})))
   + sum V (\v. #0.506 * lmfun (hl [vec 0; v]))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;       
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[th91]);;
e (SUBGOAL_THEN  `sum (V:real^3->bool) (\v. #0.591) =  #0.591 * &(CARD V) ` ASSUME_TAC);;
e (ONCE_REWRITE_TAC [ARITH_RULE `#0.591 = #0.591 * &1`]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 * &1)  = #0.591 * (sum V (\v. &1))` ASSUME_TAC);; 
e (REWRITE_TAC[SUM_LMUL]);;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
e (SIMP_TAC[GSYM CARD_EQ_SUM]);;
e (STRIP_TAC);;
e (REAL_ARITH_TAC);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.506 * lmfun (hl [vec 0; v])) = 
#0.506 * sum V (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
e (SIMP_TAC [SUM_LMUL]);;
e (SUBGOAL_THEN `sum (V:real^3->bool)
      (\v. #0.0331 *
           &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) = #0.0331 * sum (V)
      (\v. 
           &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))  ` ASSUME_TAC);;

e (SIMP_TAC [SUM_LMUL]);;
e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. 
           &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) = (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))` ASSUME_TAC);;
e (ASM_MESON_TAC [th92]);;
e (UNDISCH_TAC `sum (V:real^3->bool)
      (\v. #0.0331 *
           &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) =
      #0.0331 *
      sum V
      (\v. &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))`);;
e (POP_ASSUM(fun th ->REWRITE_TAC[th]  ));;
e (STRIP_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
e (ASM_REWRITE_TAC[]);;

let th9 = top_thm();;


g `!(V:real^3->bool) (P:real^3->bool).
FINITE V /\ packing V /\ V SUBSET ball_annulus /\
    weakly_saturated V r r' /\
     ~lmfun_ineq_center V /\
    P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
    (polyhedron P) /\ (bounded P)
    ==> #0.591 * (&(CARD V)) - #0.0331 * &(6*(CARD V) - 12) + #0.506 * (&12) < #0.591* (&(CARD V)) - #0.0331 * (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))  + #0.506 * (sum V (\v. lmfun (hl [vec 0; v])))`;; 

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u)) <= (6 * CARD (V:real^3->bool) - 12)` ASSUME_TAC);;
e (ASM_MESON_TAC [th6]);;
e (SUBGOAL_THEN `&(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u)) <= &(6 * CARD (V:real^3->bool) - 12)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_OF_NUM_LE]);;
e (SUBGOAL_THEN `#0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u)) <= #0.0331 * &(6 * CARD (V:real^3->bool) - 12)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MP_TAC (ARITH_RULE `&0 <= #0.0331`));;
e (MESON_TAC [REAL_LE_LMUL]);;
e (SUBGOAL_THEN `-- (#0.0331 * &(6 * CARD (V:real^3->bool) - 12)) <= -- (#0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u)))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_LE_NEG]);;
e (SUBGOAL_THEN `#0.591 * &(CARD V) + -- (#0.0331 * &(6 * CARD (V:real^3->bool) - 12)) <= #0.591 * &(CARD V) + -- (#0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u)))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_LE_LADD_IMP]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [GSYM real_sub]);;
e (STRIP_TAC);;
e (UNDISCH_TAC `~lmfun_ineq_center (V:real^3->bool)`);;
e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&12 < sum (V:real^3 -> bool) (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [REAL_NOT_LE]);;
e (SUBGOAL_THEN `#0.506 * &12 < #0.506 * sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MP_TAC (ARITH_RULE `&0 < #0.506`));;
e (MESON_TAC [REAL_LT_LMUL]);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `#0.591 * &(CARD (V:real^3->bool)) - #0.0331 * &(6 * CARD V - 12) <=
      #0.591 * &(CARD V) -
      #0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u))`);;
e (ABBREV_TAC `a:real = #0.591 * &(CARD (V:real^3->bool)) - #0.0331 * &(6 * CARD V - 12)`);;
e (ABBREV_TAC `b:real = #0.591 * &(CARD (V:real^3->bool)) -
 #0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u))`);;
e (MESON_TAC [REAL_LET_ADD2]);;

let th10 = top_thm();;

(*--------------------------------------------------------------------------*)
let REAL_SUB2_SUB2 = prove(`!x y z:real. x - (y - z) = x - y + z`,REPEAT GEN_TAC THEN SUBGOAL_THEN `--(y:real - z) = z - y` ASSUME_TAC THENL [REWRITE_TAC [REAL_NEG_SUB];POP_ASSUM MP_TAC THEN PURE_REWRITE_TAC [real_sub] THEN STRIP_TAC THEN PURE_REWRITE_TAC [REAL_NEG_ADD;REAL_NEGNEG] THEN REWRITE_TAC[REAL_ADD_ASSOC]]);;

let REAL_ADD2_ADD2 = prove (`!x y z:real. x + (y + z) = x + y + z`,SET_TAC[]);;

g `(pi < #3.15) ==> (&4 * pi - #6.4692) / #0.3924 < &16`;;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&0 < &4` ASSUME_TAC);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `&4*pi < &4 * #3.15` ASSUME_TAC);;
e (ASM_MESON_TAC[REAL_LT_LMUL_EQ]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `&4 * #3.15= #12.6`]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&4*pi + (--(#6.4692)) < #12.6 + (--(#6.4692))` ASSUME_TAC);;
e (ASM_REWRITE_TAC[REAL_LT_RADD]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [GSYM real_sub]);;
e (PURE_REWRITE_TAC [ARITH_RULE `#12.6 - #6.4692 = #6.1308`]);;
e (SUBGOAL_THEN `&0 < #0.3924` ASSUME_TAC);;
e (ARITH_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(&4 * pi - #6.4692)/( #0.3924) < #6.1308 / #0.3924` ASSUME_TAC);;
e (ASM_MESON_TAC[GSYM REAL_LT_DIV2_EQ]);;
e (SUBGOAL_THEN `#6.1308 / #0.3924 < &16` ASSUME_TAC);;
e (ARITH_TAC);;
e (ASM_MESON_TAC[REAL_LT_TRANS]);;

let th11 = top_thm();;

g `!(V:real^3->bool).(pi < #3.15) /\ ( &12 < &(CARD V)) /\ #0.591 * (&(CARD V)) - #0.0331 * &(6*(CARD V)-12) + #0.506 * (&12) < &4 * pi ==> &(CARD V) < &16`;;
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `12 < CARD (V:real^3->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
e (SUBGOAL_THEN ` 12 < 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
e (SUBGOAL_THEN `6 * 12 < 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
e (SUBGOAL_THEN `~(6 = 0)` ASSUME_TAC);;
e (ARITH_TAC);;
e (ASM_MESON_TAC[LT_LMULT]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `6 * 12 = 72`]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN ` 12 < 72 ` ASSUME_TAC);;
e (ARITH_TAC);;
e (ASM_MESON_TAC[LT_TRANS]);;
e (SUBGOAL_THEN ` 12 <= 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
e (ASM_MESON_TAC[LT_IMP_LE]);;
e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))-12) = &(6 *(CARD V)) - &12` ASSUME_TAC);; 
e (ASM_MESON_TAC[REAL_OF_NUM_SUB]);;
e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))) = &(6) * &(CARD V)` ASSUME_TAC);; 
e (MESON_TAC[REAL_OF_NUM_MUL]);;
e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))-12) = &(6) * &(CARD V) - &12` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `#0.591 * (&(CARD (V:real^3 -> bool))) - #0.0331 * (&(6) * &(CARD V) - &12) + #0.506 * (&12)< &4 * pi` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `#0.0331 * (&(6) * &(CARD (V:real^3->bool)) - &12) = #0.0331 * &(6) * &(CARD (V)) -  #0.0331 * &12` ASSUME_TAC);;
e (MESON_TAC[REAL_SUB_LDISTRIB]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `#0.0331 * &12 = #0.3972`]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `#0.591 * (&(CARD (V:real^3 -> bool))) - (#0.0331 * &6 * &(CARD V) - #0.3972) + #0.506 * (&12)< &4 * pi` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `#0.506 * &12 = #6.072`]);;
e (PURE_REWRITE_TAC [REAL_SUB2_SUB2 ]);;
e (SUBGOAL_THEN `#0.0331 * &6 * &(CARD (V:real^3->bool)) = (#0.0331 * &6) * &(CARD V) ` ASSUME_TAC);;
e (REWRITE_TAC[REAL_MUL_ASSOC]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `#0.0331 * &6 = #0.1986`]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `#0.591 * &(CARD (V:real^3->bool)) - #0.1986 * &(CARD V)
= (#0.591 - #0.1986) * &(CARD V)` ASSUME_TAC);;
e (MESON_TAC[REAL_SUB_RDISTRIB]);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `(#0.591 - #0.1986) = #0.3924`]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `#0.591 * &(CARD (V:real^3->bool)) - #0.1986 * &(CARD V) + #0.3972 = #0.3924 * &(CARD V) + #0.3972` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `(#0.3924 * &(CARD (V:real^3->bool)) + #0.3972) + #6.072 = 
#0.3924 * &(CARD (V:real^3->bool)) + (#0.3972 + #6.072)` ASSUME_TAC);;
e (MESON_TAC[REAL_ADD_AC]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `#0.3972 + #6.072 = #6.4692` ASSUME_TAC);;
e (ARITH_TAC);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `(#0.3924 * &(CARD (V:real^3->bool)) + #6.4692) + (--(#6.4692)) <  &4 * pi + (--(#6.4692))` ASSUME_TAC);;
e (ASM_REWRITE_TAC [REAL_LT_RADD]);;
e (POP_ASSUM MP_TAC);;
e (ONCE_REWRITE_TAC [REAL_ADD_AC]);;
e (PURE_REWRITE_TAC [GSYM real_sub]);;
e (PURE_REWRITE_TAC [ARITH_RULE `#6.4692 - #6.4692 = &0`]);;
e (PURE_REWRITE_TAC [REAL_ADD_RID]);;
e (ONCE_REWRITE_TAC [REAL_ADD_AC]);;
e (PURE_REWRITE_TAC [GSYM real_sub]);;
e (SUBGOAL_THEN `&0 < (#0.3924)` ASSUME_TAC);;
e (ARITH_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) < (&4 * pi - #6.4692)/(#0.3924)` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (PURE_REWRITE_TAC [ARITH_RULE `#0.3924 * &(CARD (V:real^3->bool)) = &(CARD V)*(#0.3924)`]);;
e (ASM_MESON_TAC [GSYM REAL_LT_RDIV_EQ]);;
e (SUBGOAL_THEN `(&4 * pi - #6.4692) / #0.3924 < &16` ASSUME_TAC);;
e (ASM_MESON_TAC[th11]);;
e (ASM_MESON_TAC[REAL_LT_TRANS]);;


let th12 = top_thm();;

(*---------------------------------------------------------------------------*)
g `!(V:real^3->bool). &(CARD V) < &16 /\ &12 < &(CARD V) ==> CARD V = 13 \/ 
CARD V = 14 \/ CARD V = 15`;; 
e (GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `CARD (V:real^3->bool) < 16` ASSUME_TAC);;
e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
e (SUBGOAL_THEN `12 < CARD (V:real^3->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
e (ASM_MESON_TAC [ARITH_RULE `!a:num.a = 13 \/ a = 14 \/ a = 15 <=> a < 16 /\ 12 < a` ]);;

let NUM_REAL = top_thm();;

g `!(V:real^3->bool) (V1:real^3->bool) X P F F_T (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)) (f3:(real^3) -> (real^3->bool)) (f4:((real^3->bool))->(real^3)).
         FINITE V /\ FINITE V1 /\ 
         packing V  /\
         V SUBSET ball_annulus /\ V SUBSET V1 /\
         V1 SUBSET ball_annulus /\
         packing V1 /\
         (!y. (!x. x IN V1 ==> &2 <= dist (x,y)) ==> y IN V1) /\
         P = INTERS {half_spaces g_fun u|(u IN V1) /\ (~(vec 0 = u))} /\
         polyhedron P /\ 
         pi < #3.15 /\
         ~(lmfun_ineq_center V) /\
         ~(lmfun_ineq_center V1) /\
         (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\ 
         X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
         F = {l | l facet_of P} /\
         F_T = face_set_of_fan (fan_of_polyhedron P ) /\
         f1 o f2 = I /\ f2 o f1 = I /\ 
        IMAGE f1 V1 = X /\
        f3 o f4 = I /\ f3 o f4 = I /\ 
       IMAGE f3 V1 = F /\
       (!v. v IN V1 ==>  #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of f3(v)})) +  #0.506 * lmfun (hl [vec 0; v])
       <= reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})))
    ==>
   (CARD V = 13 \/ CARD V = 14 \/ CARD V = 15)`;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&12 < &(CARD (V:real^3->bool))` ASSUME_TAC);; 
e (ASM_MESON_TAC [condition_1]);;
e (SUBGOAL_THEN `weakly_saturated (V1:real^3->bool) r r'` ASSUME_TAC);;
e (ASM_MESON_TAC [thm17]);;
e (SUBGOAL_THEN `&2 <= r:real` ASSUME_TAC);;
e (PURE_REWRITE_TAC[r]);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `r:real <= r'` ASSUME_TAC);;
e (PURE_REWRITE_TAC [r;r';h0]);;
e (ARITH_TAC);;
e (SUBGOAL_THEN `bounded (P:real^3->bool)` ASSUME_TAC);;
e (UNDISCH_TAC `polyhedron (P:real^3->bool)`);;
e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u|(u IN V1:real^3->bool) /\ (~(vec 0 = u))} `);;
e (UNDISCH_TAC `weakly_saturated (V1:real^3->bool) r r'`);;
e (UNDISCH_TAC `packing (V1:real^3->bool)`);;
e (UNDISCH_TAC `FINITE (V1:real^3->bool)`);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (SUBGOAL_THEN `!(V:real^3 -> bool) (g:real^3->real) (r:real) (r':real) P.(&2 <= r) /\ (r <= r') /\ (FINITE V) /\ packing V /\ 
(weakly_saturated V r r') /\
 P = INTERS {half_spaces g u|(u IN V) /\ (~(vec 0 = u))} /\ polyhedron P ==>
(bounded P)` ASSUME_TAC);;
e (REWRITE_TAC [TARJJUW]);;
e (POP_ASSUM (LABEL_TAC "F1"));;
e (USE_THEN "F1" (MP_TAC o SPECL [`V1:real^3->bool`;`g_fun`;`r`;`r'`;`P:real^3->bool`]));;
e (SET_TAC[]);;
e (SUBGOAL_THEN `(?r:real. r> &0 /\ ball(vec 0,r) SUBSET (P:real^3->bool))` ASSUME_TAC);;
e (EXISTS_TAC `r'':real`);;
e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `sum (V1:real^3->bool)
             (\v:real^3. reg (g_fun v)
                  (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))) <=
             (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))` ASSUME_TAC);;
e (MP_TAC (ISPECL [`(V1:real^3->bool)`;`X:(real^3->bool)->bool`;`P:real^3->bool`;`F':(real^3->bool)->bool`;`F_T:(real^3#real^3->bool)->bool`;`(f1:(real^3) -> (real^3->bool))`;`(f2:((real^3->bool))->(real^3))`;`(f3:(real^3) -> (real^3->bool))`;`(f4:((real^3->bool))->(real^3))`]th8));;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `#0.591* (&(CARD (V1:real^3->bool))) - #0.0331 * (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))  + #0.506 * (sum V1 (\v. lmfun (hl [vec 0; v]))) <=  sum V1 (\v. reg (g_fun v) (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})))` ASSUME_TAC);;
e (MP_TAC (ISPECL [`(V1:real^3->bool)`;`X:(real^3->bool)->bool`;`P:real^3->bool`;`F':(real^3->bool)->bool`;`F_T:(real^3#real^3->bool)->bool`;`(f1:(real^3) -> (real^3->bool))`;`(f2:((real^3->bool))->(real^3))`;`(f3:(real^3) -> (real^3->bool))`;`(f4:((real^3->bool))->(real^3))`]th9));;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `#0.591 * (&(CARD (V1:real^3->bool))) - #0.0331 * &(6*(CARD V1) - 12) + #0.506 * (&12) < #0.591* (&(CARD V1)) - #0.0331 * (&(nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))))  + #0.506 * (sum V1 (\v. lmfun (hl [vec 0; v])))` ASSUME_TAC);;
e (ASM_MESON_TAC [th10]);;
e (SUBGOAL_THEN `#0.591 * (&(CARD (V1:real^3->bool))) - #0.0331 * &(6*(CARD V1) - 12) + #0.506 * (&12) < sum V1
      (\v. reg (g_fun v)
           (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[REAL_LTE_TRANS]);;
e (SUBGOAL_THEN `#0.591 * (&(CARD (V1:real^3->bool))) - #0.0331 * &(6*(CARD V1) - 12) + #0.506 * (&12) < (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))` ASSUME_TAC);;
e (UNDISCH_TAC `sum (V1:real^3->bool)
             (\v. reg (g_fun v)
                  (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))) <=
             (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))`);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[REAL_LTE_TRANS]);;
e (POP_ASSUM MP_TAC);;
e (SUBGOAL_THEN `&4 * pi = (sum (X:(real^3->bool)->bool) (\v:real^3->bool. sol (vec 0) (v)))` ASSUME_TAC);;
e (ASM_MESON_TAC [th7]);;
e (SUBGOAL_THEN `(sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v)))) = (sum (X:(real^3->bool)->bool) (\v:real^3->bool. sol (vec 0) (v)))` ASSUME_TAC);;
e (ASM_MESON_TAC [thm18]);;
e (SUBGOAL_THEN `&4 * pi = (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (ARITH_TAC);;
e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]));;
e (SUBGOAL_THEN `CARD (V:real^3->bool) <= CARD (V1:real^3->bool)` ASSUME_TAC);;
e (UNDISCH_TAC `FINITE (V1:real^3->bool)`);;
e (UNDISCH_TAC `(V:real^3->bool) SUBSET V1`);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `(V:real^3->bool) SUBSET V1 /\ FINITE (V1:real^3->bool)` ASSUME_TAC);;
e (ASM_MESON_TAC[]);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC[CARD_SUBSET]);;
e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) <= &(CARD (V1:real^3->bool))` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [REAL_OF_NUM_LE]);;
e (SUBGOAL_THEN `&12 < &(CARD (V1:real^3->bool))` ASSUME_TAC);;
e (UNDISCH_TAC `&12 < &(CARD (V:real^3->bool))`);;
e (POP_ASSUM MP_TAC);;
e (REAL_ARITH_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `&(CARD (V1:real^3->bool)) < &16` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `pi < #3.15`);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [th12]);;
e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) < &16` ASSUME_TAC);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `&(CARD (V:real^3->bool)) <= &(CARD (V1:real^3->bool))`);;
e (MESON_TAC [REAL_LET_TRANS]);;
e (UNDISCH_TAC `&12 < &(CARD (V:real^3->bool))`);;
e (POP_ASSUM MP_TAC);;
e (MESON_TAC [NUM_REAL]);;


let DLWCHEM = top_thm();;