legacy/oldtame/dangtatdatusb/DLWCHEM.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALISATION                                              *)
   3 (*                                                                            *)
   4 (* Proof: DLWCHEM                                                             *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Dang Tat Dat                                                       *)
   7 (* Date:   In progress                                                        *)
   8 (* ========================================================================== *)
   9
  10 needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;
  11
  12 (* ** Load parent files ** *)
  13 flyspeck_needs "nonlinear/ineq.hl";;
  14 flyspeck_needs "packing/pack_defs.hl";;
  15 flyspeck_needs "tame/tame_defs.hl";;
  16 flyspeck_needs "trigonometry/trigonometry.hl";;
  17 flyspeck_needs "fan/Conforming.hl";;
  18 flyspeck_needs "packing/pack_defs.hl";;
  19 flyspeck_needs "fan/HypermapAndFan.hl";;
  20 flyspeck_needs "fan/polyhedron.hl";;
  21
  22 (* ** Proof module type ** *)
  23
  24
  25 (* ** Proof module ** *)
  26
  27 open Sphere;;
  28 open Trigonometry1;;
  29 open Trigonometry2;;
  30 open Vol1;;
  31 open Pack_defs;;
  32 open Tame_defs;;
  33 open Ineq;;
  34 open Fan_defs;;
  35 open Hypermap;;
  36 open Hypermap_and_fan;;
  37 open Fan;;
  38 open Polyhedron;;
  39 (*open Polyhedron_def;;*)
  40 (*--------------Definition---------------------------------------------------*)
  41 let weakly_saturated =
  42     new_definition
  43      `weakly_saturated (V:real^3 ->bool) (r:real) (r':real) <=>
  44         (!(v:real^3).(&2 <= dist(vec 0,v) ) /\ (dist(vec 0, v) <= r') ==>
  45             (?(u:real^3). (u IN V) /\ (~((vec 0) = u)) /\ (dist(u,v) < r)))`;;
  46
  47 let half_spaces =
  48     new_definition
  49     `half_spaces (a:real^3) (b:real) =
  50      {x:real^3| (a dot x) <= b}`;;
  51
  52 let r =
  53     new_definition
  54      `r = &2` ;;
  55
  56 let r' =
  57     new_definition
  58      `r' = &2 * h0` ;;
  59
  60 let g_fun =
  61     new_definition
  62     `(g_fun) (x:real^3) = (acs(dist(vec 0, x)/(&4))) - (pi/(&6))` ;;
  63
  64 let dart2_of_fan = new_definition
  65   `dart2_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  {(v,v) | v IN V /\ set_of_edge (v:A) V E = {} }`;;
  66
  67 (*-------------------------Fan   Definiton-----------------------------------*)
  68
  69 let CASE_FAN_FINITE = new_definition `CASE_FAN_FINITE (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> FINITE V /\ ~(V SUBSET {})`;;
  70
  71 let CASE_FAN_ORIGIN = new_definition `CASE_FAN_ORIGIN (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> ~((vec 0) IN (V))`;;
  72
  73 let CASE_FAN_INDEPENDENCE =
  74   new_definition `CASE_FAN_INDEPENDENCE (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=>
  75   (!e.  e IN E ==> ~collinear ({vec 0} UNION e))`;;
  76
  77 let CASE_FAN_INTERSECTION =
  78   new_definition`CASE_FAN_INTERSECTION(V:real^3 -> bool,E:(real^3 ->bool)->bool)<=>
  79   (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  80   ==> ((aff_ge {vec 0 } e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;
  81
  82 let FANO =
  83   new_definition `FANO(V:real^3 -> bool,E:(real^3 ->bool)->bool) <=>
  84   ((UNIONS E) SUBSET V) /\ graph(E) /\ CASE_FAN_FINITE(V,E) /\ CASE_FAN_ORIGIN(V,E)/\
  85   CASE_FAN_INDEPENDENCE(V,E)/\ CASE_FAN_INTERSECTION(V,E)`;;
  86
  87 let FANO_OF_FAN = prove( `!(V:real^3 -> bool)(E:(real^3 ->bool)->bool). (FAN(vec 0 , V , E) <=> FANO(V,E))`,
  88   REWRITE_TAC[FAN;FANO;CASE_FAN_FINITE;CASE_FAN_ORIGIN;CASE_FAN_INDEPENDENCE;CASE_FAN_INTERSECTION;fan1;fan2;fan6;fan7]);;
  89
  90 (*-------------------------------------------------------------------------*)
  91
  92 let interior_point =
  93     new_definition
  94     `interior_point (p:real^3) (P:real^3->bool)
  95        <=> ?(r:real). (&0 < r) /\ (ball(p,r) SUBSET P)` ;;
  96 let reg =
  97     new_definition
  98      `reg (a:real) (k:real) = (&2)*pi - (&2)*k*(asn(cos(a)*sin(pi/k)))` ;;
  99
 100 let arc_1 =
 101     new_definition
 102     `arc_1 (a:real) (b:real) (c:real) =
 103      pi/(&2) - (atn2( (sqrt (ups_x (a*a) (b*b) (c*c))),(a*a + b*b - c*c)))`;;
 104
 105 let IN_DOUBLE = prove(`!x y z:real^N. x IN {y,z} <=> x = y  \/ x = z`,SET_TAC[]);;
 106
 107 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[]);;
 108
 109 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)`,
 110   GEN_TAC THEN REWRITE_TAC[face_set;node_set;edge_set]
 111 THEN REPEAT STRIP_TAC
 112 THEN MATCH_MP_TAC lemma_partition
 113 THEN REWRITE_TAC[hypermap_lemma]);;
 114
 115
 116 (*-----------------Some new axiom--------------------------------------------*)
 117 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') /\
 118  P = INTERS {half_spaces u (g u)| u IN V} /\ polyhedron P /\ u IN V ==>
 119 (bounded P)`;;
 120
 121 let TARJJUW = new_axiom TARJJUW_concl;;
 122
 123 (*----------------------------------------------------------------------------*)
 124 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}`;;
 125
 126 e (GEN_TAC);;
 127 e (STRIP_TAC);;
 128 e (REWRITE_TAC [edges;EXTENSION]);;
 129 e (GEN_TAC THEN EQ_TAC);;
 130 e (REWRITE_TAC [IN_ELIM_THM]);;
 131 e (STRIP_TAC);;
 132 e (MP_TAC (ISPECL [`V:real^3 -> bool`;`v:real^3`;`w:real^3`]SEGMENT_EDGE_OF));;
 133 e (ASM_REWRITE_TAC[]);;
 134 e (STRIP_TAC);;
 135 e (EXISTS_TAC `v:real^3`);;
 136 e (EXISTS_TAC `w:real^3`);;
 137 e (ASM_REWRITE_TAC[]);;
 138 e (UNDISCH_TAC `segment [v,w] edge_of (V:real^3->bool)`);;
 139 e (REWRITE_TAC [edge_of;face_of;segment;CONVEX_HULL_2_ALT;IN_ELIM_THM]);;
 140 e (STRIP_TAC);;
 141 e (SUBGOAL_THEN `!v:real^3 w:real^3 u:real . v + u % (w - v) = (&1 - u) % v + u % w` ASSUME_TAC);;
 142 e (REPEAT GEN_TAC);;
 143 e (REWRITE_TAC [VECTOR_SUB_LDISTRIB;VECTOR_SUB_RDISTRIB;VECTOR_MUL_LID]);;
 144 e (VECTOR_ARITH_TAC);;
 145 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);;
 146 e (REWRITE_TAC [EXTENSION]);;
 147 e (GEN_TAC);;
 148 e (EQ_TAC);;
 149 e (REWRITE_TAC [IN_ELIM_THM]);;
 150 e (STRIP_TAC);;
 151 e (EXISTS_TAC `u:real`);;
 152 e (ASM_REWRITE_TAC[]);;
 153 e (REWRITE_TAC [IN_ELIM_THM]);;
 154 e (STRIP_TAC);;
 155 e (EXISTS_TAC `u:real`);;
 156 e (ASM_REWRITE_TAC[]);;
 157 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
 158 e (ASM_REWRITE_TAC[]);;
 159 e (SUBGOAL_THEN `!v:real^3 w:real^3 u:real . v + u % (w - v) = (&1 - u) % v + u % w` ASSUME_TAC);;
 160 e (REPEAT GEN_TAC);;
 161 e (REWRITE_TAC [VECTOR_SUB_LDISTRIB;VECTOR_SUB_RDISTRIB;VECTOR_MUL_LID]);;
 162 e (VECTOR_ARITH_TAC);;
 163 e (REWRITE_TAC [IN_ELIM_THM]);;
 164 e (STRIP_TAC);;
 165 e (EXISTS_TAC `v:real^3`);;
 166 e (EXISTS_TAC `w:real^3`);;
 167 e (ASM_REWRITE_TAC[]);;
 168 e (UNDISCH_TAC `convex hull {v, w} face_of (V:real^3->bool)`);;
 169 e (REWRITE_TAC [edge_of;face_of;segment;CONVEX_HULL_2_ALT]);;
 170 e (STRIP_TAC);;
 171 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);;
 172 e (REWRITE_TAC [EXTENSION]);;
 173 e (GEN_TAC);;
 174 e (EQ_TAC);;
 175 e (REWRITE_TAC [IN_ELIM_THM]);;
 176 e (STRIP_TAC);;
 177 e (EXISTS_TAC `u:real`);;
 178 e (ASM_REWRITE_TAC[]);;
 179 e (REWRITE_TAC [IN_ELIM_THM]);;
 180 e (STRIP_TAC);;
 181 e (EXISTS_TAC `u:real`);;
 182 e (ASM_REWRITE_TAC[]);;
 183 e (POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]));;
 184 e (ASM_REWRITE_TAC[]);;
 185 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);;
 186 e (REWRITE_TAC [EXTENSION]);;
 187 e (GEN_TAC);;
 188 e (EQ_TAC);;
 189 e (REWRITE_TAC [IN_ELIM_THM]);;
 190 e (STRIP_TAC);;
 191 e (EXISTS_TAC `u:real`);;
 192 e (ASM_REWRITE_TAC[]);;
 193 e (REWRITE_TAC [IN_ELIM_THM]);;
 194 e (STRIP_TAC);;
 195 e (EXISTS_TAC `u:real`);;
 196 e (ASM_REWRITE_TAC[]);;
 197 e (REWRITE_TAC [GSYM segment]);;
 198 e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]SEGMENT_SUBSET_HALFLINE));;
 199 e (STRIP_TAC);;
 200 e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]HALFLINE_SUBSET_AFFINE_HULL));;
 201 e (STRIP_TAC);;
 202 e (MP_TAC (ISPECL [`{v:real^3,w:real^3}`]AFF_DIM_AFFINE_HULL));;
 203 e (STRIP_TAC);;
 204 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));;
 205 e (ASM_REWRITE_TAC[]);;
 206 e (STRIP_TAC);;
 207 e (MP_TAC (ISPECL [`segment [v:real^3,w:real^3]`;`affine hull {v:real^3, w:real^3}`]AFF_DIM_SUBSET));;
 208 e (ASM_REWRITE_TAC[]);;
 209 e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]AFF_DIM_2));;
 210 e (ASM_REWRITE_TAC[]);;
 211 e (REPEAT STRIP_TAC);;
 212 e (SUBGOAL_THEN `{v:real^3,w:real^3} SUBSET segment [v,w]` ASSUME_TAC);;
 213 e (REWRITE_TAC [segment;SUBSET]);;
 214 e (GEN_TAC);;
 215 e (REWRITE_TAC[IN_DOUBLE;IN_ELIM_THM]);;
 216 e (STRIP_TAC);;
 217 e (EXISTS_TAC `&0`);;
 218 e (REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1`]);;
 219 e (REWRITE_TAC[ARITH_RULE `&1 - &0 = &1`;VECTOR_MUL_LZERO;VECTOR_ADD_RID;VECTOR_MUL_LID]);;
 220 e (ASM_REWRITE_TAC[]);;
 221 e (EXISTS_TAC `&1`);;
 222 e (REWRITE_TAC [ARITH_RULE `&0 <= &1 /\ &1 <= &1`]);;
 223 e (REWRITE_TAC [ARITH_RULE `&1 - &1 = &0`;VECTOR_MUL_LZERO;VECTOR_MUL_LID;VECTOR_ADD_LID]);;
 224 e (ASM_REWRITE_TAC[]);;
 225 e (MP_TAC (ISPECL [`{v:real^3, w:real^3}`;`segment [v:real^3,w:real^3]`]AFF_DIM_SUBSET));;
 226 e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
 227 e (STRIP_TAC);;
 228 e (MP_TAC (ISPECL [`aff_dim (segment [v:real^3,w:real^3])`;`aff_dim {(v:real^3), (w:real^3)}`]INT_LE_ANTISYM));;
 229 e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
 230 e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
 231 e (POP_ASSUM (fun th-> REWRITE_TAC[th]));;
 232
 233 let EDGE_CONVEX_HULL = top_thm();;
 234
 235 g `!(V:real^3 -> bool). (polyhedron V) /\ (bounded V) /\ (interior_point (vec 0) V) ==> FANO (fan_of_polyhedron V)`;;
 236 e (GEN_TAC);;
 237 e (STRIP_TAC);;
 238 e (MP_TAC (ISPECL [`V:real^3->bool`;`(vec 0):real^3`]POLYHEDRON_FAN));;
 239 e (MP_TAC (ISPECL [`V:real^3->bool`;`(vec 0):real^3`]INTERIOR_EQUIVALENT));;
 240 e (ASM_REWRITE_TAC[]);;
 241 e (STRIP_TAC);;
 242 e (ASM_REWRITE_TAC[vertices;edges;fan_of_polyhedron]);;
 243 e (REWRITE_TAC [edge_of]);;
 244 e (MP_TAC (ISPECL [`V:real^3->bool`]EDGE_CONVEX_HULL));;
 245 e (ASM_REWRITE_TAC[]);;
 246 e (STRIP_TAC);;
 247 e (POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));;
 248 e (MP_TAC (ISPECL [`V:real^3 ->bool`;`(vec 0):real^3`]POLYHEDRON_FAN));;
 249 e (ASM_REWRITE_TAC[]);;
 250 e (STRIP_TAC);;
 251 e (STRIP_TAC);;
 252 e (MP_TAC (ISPECL [`vertices (V:real^3->bool)`;`edges (V:real^3->bool)`]FANO_OF_FAN));;
 253 e (ASM_REWRITE_TAC[GSYM vertices]);;
 254
 255 let JLIGZGS = top_thm();;
 256
 257 (*---------------------------------------------------------------------------*)
 258 let WGVWSKE_concl = `!(V:real^3->bool) (E:(real^3->bool)->bool).
 259    FANO (V,E) /\ conforming (V,E)
 260    ==> connected_hypermap (hypermap_of_fan (V,E))`;;
 261
 262 let WGVWSKE = new_axiom WGVWSKE_concl;;
 263
 264
 265 let GGRLKHP_concl = `!(V:real^3->bool) (E:(real^3->bool)->bool).
 266    FANO (V,E) /\ conforming (V,E)
 267    ==> planar_hypermap (hypermap_of_fan (V,E))`;;
 268
 269 let GGRLKHP = new_axiom GGRLKHP_concl;;
 270
 271 let PLAIN_HYPERMAP =prove(`!(V:real^3->bool) (E:(real^3->bool)->bool).
 272    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]);;
 273
 274 (*---------------------------------------------------------------------------*)
 275
 276 (*FACET_OF_POLYHEDRON_EXPLICIT*)
 277 (*Chung minh rang o day ton tai mot song anh*)
 278 (*!s f a b.
 279          FINITE f /\
 280          s = affine hull s INTER INTERS f /\
 281          (!h. h IN f ==> ~(a h = vec 0) /\ h = {x | a h dot x <= b h}) /\
 282          (!f'. f' PSUBSET f ==> s PSUBSET affine hull s INTER INTERS f')
 283          ==> (!c. c facet_of s <=>
 284                   (?h. h IN f /\ c = s INTER {x | a h dot x = b h})) *)
 285 let CZZHBLI_concl_1 =
 286     `!(V:real^3 -> bool) P (u:real^3) b:real F .(FINITE V) /\ packing V
 287    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 288     P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 289   (polyhedron P) /\ (bounded P) /\
 290    F = {f|f facet_of P}
 291   ==> (?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F)`;;
 292
 293 let CZZHBLI_1 = new_axiom CZZHBLI_concl_1;;
 294 (*
 295 g `!(V:real^3 -> bool) P (u:real^3) b:real F .(FINITE V) /\ packing V
 296    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 297     P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 298   (polyhedron P) /\ (bounded P) /\
 299    F = {f|f facet_of P}
 300   ==> (?(h:(real^3) -> (real^3->bool)) (g:((real^3->bool))->(real^3)). h o g = I /\ g o h = I /\ IMAGE h V = F)`;;
 301 e (REPEAT GEN_TAC);;
 302 e (STRIP_TAC);;
 303 e (MP_TAC (ISPECL [`P:real^3->bool`;`f:real^3->bool`]FACET_OF_POLYHEDRON));;
 304 e (ASM_REWRITE_TAC[]);;
 305 e (STRIP_TAC);;
 306
 307 FACET_OF_POLYHEDRON_EXPLICIT;;
 308 FACET_OF_POLYHEDRON;;
 309 FINITE_POLYHEDRON_FACES;;
 310 FINITE_POLYHEDRON_EXTREME_POINT;;
 311 search [`norm v`];;
 312 *)
 313 (*----------------------------------------------------------------------------*)
 314
 315 let RDWKARC_concl = `~kepler_conjecture /\ (!V. cell_cluster_estimate V) /\
 316   marchal_inequality
 317    ==> (?V.  packing V /\ V SUBSET ball_annulus /\ ~(lmfun_ineq_center V))`;;
 318
 319 let RDWKARC = new_axiom  RDWKARC_concl;;
 320
 321
 322 (*---------------------------------------------------------------------------*)
 323
 324 let AMHFNXP_concl =
 325     `!(P:real^3 -> bool) F WF.
 326      (polyhedron P) /\ (bounded P) /\ (interior_point (vec 0) P) /\
 327      (F = {f|f facet_of P}) /\ (WF = topological_component_yfan (vec 0,fan_of_polyhedron P))
 328       ==> (?(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)`;;
 329
 330 let AMHFNXP = new_axiom AMHFNXP_concl;;
 331
 332 (*---------------------------------------------------------------------------*)
 333
 334 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`;;
 335
 336 let BSXAQBQ = new_axiom BSXAQBQ_concl;;
 337 (*---------------------------------------------------------------------------*)
 338
 339 let PIIJBJK_concl =`!(V:real^3 -> bool)(E:(real^3->bool)->bool).
 340     fully_surrounded (V,E) ==>
 341      conforming (V,E)`;;
 342
 343
 344 let PIIJBJK = new_axiom PIIJBJK_concl;;
 345 (*---------------------------------------------------------------------------*)
 346
 347 let UVPFEEP_concl1 =`!(V:real^3 -> bool) (E:(real^3->bool)->bool) F WF.
 348       FANO (V,E) /\ (conforming (V,E)) /\
 349       (WF = topological_component_yfan (vec 0,V,E)) /\
 350       (F = face_set_of_fan (V,E))
 351       ==> (?(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)`;;
 352
 353
 354 let UVPFEEP_1= new_axiom UVPFEEP_concl1;;
 355
 356 (*---------------------------------------------------------------------------*)
 357 let GOTCJAH_concl = `!s f (v:real^3) b WF h k.
 358     polyhedron s /\ bounded s /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET s) /\
 359     f facet_of s /\
 360     f = { p | p dot v = b } INTER s /\
 361     topological_component_yfan (vec 0,fan_of_polyhedron s) WF /\
 362     ~(f INTER WF = {}) /\
 363     rcone_gt (vec 0) v h SUBSET WF /\
 364     (k = CARD {u | u extreme_point_of f })
 365    ==> &2 * pi - &2* &k * asn (h* sin(pi/ &k)) <= sol (vec 0) WF`;;
 366
 367 let GOTCJAH = new_axiom GOTCJAH_concl;;
 368
 369 (*---------------------------------proof--------------------------------------*)
 370
 371 g `!(V:real^3 -> bool) (x:real). (&1 <=x ) ==> (lmfun x <= &1)`;;
 372 e (REWRITE_TAC [lmfun;h0]);;
 373 e (REPEAT STRIP_TAC);;
 374 e (ASM_CASES_TAC `(x:real) <= #1.26`);;
 375 e (ASM_REWRITE_TAC[]);;
 376 e (PURE_REWRITE_TAC [ARITH_RULE `#1.26 - &1 = #0.26`]);;
 377 e (SUBGOAL_THEN `&0 < #0.26` ASSUME_TAC);;
 378 e (ARITH_TAC);;
 379 e (SUBGOAL_THEN `(--x:real <= --(&1) )` ASSUME_TAC);;
 380 e (ASM_REWRITE_TAC [REAL_LE_NEG]);;
 381 e (SUBGOAL_THEN `#1.26 + --(x:real) <= #1.26 + --(&1)` ASSUME_TAC);;
 382 e (ASM_REWRITE_TAC [REAL_LE_LADD]);;
 383 e (POP_ASSUM MP_TAC);;
 384 e (REWRITE_TAC [GSYM real_sub]);;
 385 e (STRIP_TAC);;
 386 e (SUBGOAL_THEN `(#1.26 - (x:real)) / #0.26 <= (#1.26 - &1) / #0.26` ASSUME_TAC);;
 387 e (ASM_MESON_TAC [GSYM REAL_LE_DIV2_EQ]);;
 388 e (SUBGOAL_THEN `(#1.26 - &1) / #0.26 = &1` ASSUME_TAC);;
 389 e (ARITH_TAC);;
 390 e (ASM_MESON_TAC[]);;
 391 e (ASM_REWRITE_TAC[]);;
 392 e (ARITH_TAC);;
 393
 394 let thm1 = top_thm();;
 395
 396 (*----------------------------------------------------------------------------*)
 397
 398
 399 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
 400    (u IN V) ==> ((&1) <= dist(vec 0,u)/(&2)) `;;
 401 e (REWRITE_TAC [ball_annulus]);;
 402 e (REWRITE_TAC [cball;ball]);;
 403 e (REWRITE_TAC [DIFF]);;
 404 e (REWRITE_TAC [SUBSET]);;
 405 e (REPEAT STRIP_TAC);;
 406 e (POP_ASSUM MP_TAC);;
 407 e (POP_ASSUM MP_TAC);;
 408 e (DISCH_THEN (LABEL_TAC "F1"));;
 409 e (STRIP_TAC);;
 410 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
 411 e (STRIP_TAC);;
 412 e (SUBGOAL_THEN `(u:real^3) IN
 413           {x:real^3 | x IN {y:real^3 | dist (vec 0,y) <= &2 * h0} /\
 414                ~(x IN {y | dist (vec 0,y) < &2})} ` ASSUME_TAC);;
 415 e (ASM_MESON_TAC []);;
 416 e (POP_ASSUM MP_TAC);;
 417 e (REWRITE_TAC [IN_ELIM_THM]);;
 418 e (STRIP_TAC);;
 419 e (POP_ASSUM MP_TAC);;
 420 e (REWRITE_TAC [REAL_NOT_LT]);;
 421 e (STRIP_TAC);;
 422 e (SUBGOAL_THEN `(&0) < (&2)` ASSUME_TAC);;
 423 e (ARITH_TAC);;
 424 e (SUBGOAL_THEN `(&2)/(&2) <= dist (vec 0,u:real^3)/(&2)` ASSUME_TAC);;
 425 e (ASM_MESON_TAC [REAL_LE_DIV2_EQ]);;
 426 e (POP_ASSUM MP_TAC);;
 427 e (REWRITE_TAC [ARITH_RULE `(&2)/(&2) = (&1)`]);;
 428
 429 let thm2 = top_thm();;
 430
 431 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
 432    (u IN V) ==> (dist(vec 0,u) <= &2 * h0) `;;
 433 e (REWRITE_TAC [ball_annulus]);;
 434 e (REWRITE_TAC [cball;ball]);;
 435 e (REWRITE_TAC [DIFF]);;
 436 e (REWRITE_TAC [SUBSET]);;
 437 e (REPEAT STRIP_TAC);;
 438 e (POP_ASSUM MP_TAC);;
 439 e (POP_ASSUM MP_TAC);;
 440 e (DISCH_THEN (LABEL_TAC "F1"));;
 441 e (STRIP_TAC);;
 442 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
 443 e (STRIP_TAC);;
 444 e (SUBGOAL_THEN `(u:real^3) IN
 445           {x:real^3 | x IN {y:real^3 | dist (vec 0,y) <= &2 * h0} /\
 446                ~(x IN {y | dist (vec 0,y) < &2})} ` ASSUME_TAC);;
 447 e (ASM_MESON_TAC []);;
 448 e (POP_ASSUM MP_TAC);;
 449 e (REWRITE_TAC [IN_ELIM_THM]);;
 450 e (STRIP_TAC);;
 451
 452 let thm21 = top_thm();;
 453 (*----------------------------------------------------------------------------*)
 454
 455 g `!(V:real^3->bool).(FINITE V) /\ (packing V) /\ (V SUBSET ball_annulus) /\
 456     (&(CARD V) <= (&12)) ==>
 457     sum V (\v. lmfun (dist (vec 0,v) / &2)) <= (&12)`;;
 458 e (REPEAT STRIP_TAC);;
 459 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> (&1) <= dist(vec 0,v)/(&2)` ASSUME_TAC);;
 460 e (REPEAT STRIP_TAC);;
 461 e (ASM_MESON_TAC [thm2]);;
 462 e (POP_ASSUM (LABEL_TAC "F1"));;
 463 e (USE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
 464 e (STRIP_TAC);;
 465 e (SUBGOAL_THEN `!(v:real^3). (&1) <= dist(vec 0,v)/(&2) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_TAC);;
 466 e (STRIP_TAC);;
 467 e (MESON_TAC [thm1]);;
 468 e (POP_ASSUM (LABEL_TAC "F2"));;
 469 e (USE_THEN "F2" (MP_TAC o SPEC `v:real^3`));;
 470 e (STRIP_TAC);;
 471 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_TAC);;
 472 e (STRIP_TAC);;
 473 e (ASM_MESON_TAC[]);;
 474 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (dist (vec 0,v) / &2)) <= (&(CARD V)) * (&1)` ASSUME_TAC);;
 475 e (ASM_MESON_TAC [SUM_BOUND]);;
 476 e (POP_ASSUM MP_TAC);;
 477 e (REWRITE_TAC [ARITH_RULE `&(CARD (V:real^3->bool)) * &1 =  &(CARD V)`]);;
 478 e (STRIP_TAC);;
 479 e (ASM_MESON_TAC[REAL_LE_TRANS]);;
 480
 481 let thm3 = top_thm();;
 482
 483 (*----------------------------------------------------------------------------*)
 484
 485 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)`;;
 486 e (REPEAT GEN_TAC);;
 487 e (REWRITE_TAC [packing;ball_annulus]);;
 488 e (STRIP_TAC);;
 489 e (POP_ASSUM MP_TAC);;
 490 e (POP_ASSUM MP_TAC);;
 491 e (POP_ASSUM MP_TAC);;
 492 e (REWRITE_TAC [cball;ball]);;
 493 e (REWRITE_TAC [SUBSET]);;
 494 e (REWRITE_TAC [DIFF]);;
 495 e (REWRITE_TAC [IN_ELIM_THM]);;
 496 e (DISCH_THEN (LABEL_TAC "F1"));;
 497 e (REPEAT STRIP_TAC);;
 498 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
 499 e (STRIP_TAC);;
 500 e (SUBGOAL_THEN `&0 < &2` ASSUME_TAC);;
 501 e (ARITH_TAC);;
 502 e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= (&2) * h0` ASSUME_TAC);;
 503 e (ASM_MESON_TAC[]);;
 504 e (POP_ASSUM MP_TAC);;I
 505 e (FIRST_X_ASSUM MP_TAC);;
 506 e (ABBREV_TAC `uu = dist (vec 0, (u:real^3)) `);;
 507 e (MESON_TAC[REAL_LE_LDIV_EQ; REAL_MUL_SYM]);;
 508
 509 let thm4 = top_thm();;
 510
 511 g `! (x:real^N) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w))`;;
 512 e (REPEAT GEN_TAC);;
 513 e (EXISTS_TAC ` inv (&2) % ( x + (y:real^N) )  `);;
 514 e (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]);;
 515 e (STRIP_TAC);;
 516 e (EXISTS_TAC `inv (&2)`);;
 517 e (EXISTS_TAC `inv (&2)`);;
 518 e (PURE_REWRITE_TAC[ARITH_RULE `inv (&2) + inv (&2) = &1 `]);;
 519 e (PURE_REWRITE_TAC [VECTOR_ADD_LDISTRIB]);;
 520 e (STRIP_TAC);;
 521 e (ARITH_TAC);;
 522 e (ARITH_TAC);;
 523 e (EXISTS_TAC `dist (x:real^N,y) /(&2)`);;
 524 e (GEN_TAC);;
 525 e (SUBGOAL_THEN `{x:real^N, y} w <=> w IN {x:real^N, y}` ASSUME_TAC);;
 526 e (REWRITE_TAC [IN]);;
 527 e (SUBGOAL_THEN `(w:real^N) IN {x, y} <=> w = x \/ w = y` ASSUME_TAC);;
 528 e (MESON_TAC [IN_DOUBLE]);;
 529 e (ASM_REWRITE_TAC[]);;
 530 e (STRIP_TAC);;
 531 e (ASM_REWRITE_TAC[]);;
 532
 533 e (PURE_REWRITE_TAC [GSYM midpoint]);;
 534 e (REWRITE_TAC [DIST_MIDPOINT]);;
 535 e (ASM_REWRITE_TAC [GSYM midpoint]);;
 536 e (REWRITE_TAC [DIST_MIDPOINT]);;
 537
 538 let thm5 = top_thm();;
 539
 540
 541 let dat_th1 = prove(` segment [v,w:real^3] SUBSET affine hull {v,w} `,
 542
 543 REWRITE_TAC[AFFINE_HULL_2; segment; SUBSET; IN_ELIM_THM] THEN
 544
 545 MESON_TAC[REAL_ARITH` (&1 - x ) + x = &1 `]);;
 546
 547 g `(! (x:real^3) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w)))
 548 ==>
 549 ( !v w:real^3. ~(v = w) ==> circumcenter{v,w} = midpoint(v,w))`;;
 550 e (REPEAT STRIP_TAC);;
 551 e (MP_TAC (MESON[MIDPOINT_IN_SEGMENT]` midpoint (v,w:real^3) IN segment [v,w]`));;
 552 e (SUBGOAL_THEN ` ( affine hull {v,w:real^3} ) (circumcenter {v, w}) /\
 553 (?c. ! x. {v,w} x ==> c = dist ((circumcenter {v, w}),x)) ` ASSUME_TAC);;
 554 e (REWRITE_TAC[Collect_geom.circumcenter]);;
 555 e (CONV_TAC SELECT_CONV);;
 556 e (ASM_REWRITE_TAC[]);;
 557 e (MP_TAC dat_th1);;
 558 e (REWRITE_TAC[SUBSET]);;
 559 e (REPEAT STRIP_TAC);;
 560 e (SUBGOAL_THEN ` midpoint (v,w:real^3) IN affine hull {v,w} ` ASSUME_TAC);;
 561 e (FIRST_X_ASSUM MATCH_MP_TAC);;
 562 e (FIRST_X_ASSUM ACCEPT_TAC);;
 563 e (REPEAT (FIRST_X_ASSUM MP_TAC));;
 564 e (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]);;
 565 e (REPEAT STRIP_TAC);;
 566 e (UNDISCH_TAC ` !x. {v, w} x ==> c = dist (circumcenter {v, w},x:real^3)`);;
 567 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]);;
 568 e (UNDISCH_TAC ` u + v' = &1 `);;
 569 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]);;
 570 e (REPEAT STRIP_TAC);;
 571 e (FIRST_X_ASSUM MP_TAC);;
 572 e (ASM_REWRITE_TAC[REAL_ARITH` a * b = c * b <=> (a - c ) * b = &0`; REAL_ENTIRE]);;
 573 e (STRIP_TAC);;
 574 e (FIRST_X_ASSUM MP_TAC);;
 575 e (REWRITE_TAC[REAL_ARITH ` abs a - abs ( a - &1 ) = &0 <=> a = &1 / &2 `]);;
 576 e (SIMP_TAC[REAL_ARITH` &1 - &1 / &2 = &1 / &2 `]);;
 577 e (UNDISCH_TAC` midpoint (v,w) = u' % v + v'' % (w:real^3) `);;
 578 e (DISCH_THEN (SUBST1_TAC o SYM));;
 579 e (REWRITE_TAC[midpoint; REAL_ARITH` inv (&2) = &1 / &2 `]);;
 580 e (DISCH_TAC THEN VECTOR_ARITH_TAC);;
 581 e (FIRST_X_ASSUM MP_TAC);;
 582 e (REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ]);;
 583 e (ASM_MESON_TAC[]);;
 584
 585 let thm6 = top_thm();;
 586
 587
 588 g `!v w:real^3. ~(v = w) ==> circumcenter{v,w} = midpoint(v,w)`;;
 589 e (SUBGOAL_THEN `! (x:real^3) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w))` ASSUME_TAC);;
 590 e (REWRITE_TAC [thm5]);;
 591 e (POP_ASSUM MP_TAC);;
 592 e (PURE_REWRITE_TAC [thm6]);;
 593
 594 let thm7 = top_thm();;
 595
 596 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
 597    (u IN V) ==> ~(vec 0 = u)`;;
 598 e (REPEAT GEN_TAC);;
 599 e (PURE_REWRITE_TAC [ball_annulus;SUBSET;DIFF;IN_ELIM_THM;cball;ball]);;
 600 e (STRIP_TAC);;
 601 e (POP_ASSUM MP_TAC);;
 602 e (POP_ASSUM MP_TAC);;
 603 e (DISCH_THEN (LABEL_TAC "F1"));;
 604 e (STRIP_TAC);;
 605 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
 606 e (STRIP_TAC);;
 607 e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= &2 * h0 /\ ~(dist (vec 0,u) < &2)` ASSUME_TAC);;
 608 e (ASM_MESON_TAC[]);;
 609 e (ASM_CASES_TAC `(vec 0 = u:real^3)`);;
 610 e (SUBGOAL_THEN `dist(vec 0, u:real^3) = &0` ASSUME_TAC);;
 611 e (ASM_REWRITE_TAC[]);;
 612 e (MESON_TAC[DIST_REFL]);;
 613 e (SUBGOAL_THEN `~(dist (vec 0,u:real^3) < &2)` ASSUME_TAC);;
 614 e (ASM_MESON_TAC[]);;
 615 e (SUBGOAL_THEN `&2 <= dist (vec 0,u:real^3)` ASSUME_TAC);;
 616 e (POP_ASSUM MP_TAC);;
 617 e (MESON_TAC [REAL_NOT_LT]);;
 618 e (ASM_REWRITE_TAC[]);;
 619 e (POP_ASSUM MP_TAC);;
 620 e (ASM_REWRITE_TAC[]);;
 621 e (ARITH_TAC);;
 622 e (ASM_REWRITE_TAC[]);;
 623
 624 let thm8= top_thm();;
 625
 626
 627 g `!u:real^3 . ?d.(!w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w))`;;
 628 e (GEN_TAC);;
 629 e (EXISTS_TAC `dist(vec 0,u:real^3)/(&2)`);;
 630 e (GEN_TAC);;
 631 e (SUBGOAL_THEN `{vec 0, u:real^3} w <=> w IN {vec 0, u}` ASSUME_TAC);;
 632 e (REWRITE_TAC [IN]);;
 633 e (SUBGOAL_THEN `(w:real^3) IN {vec 0, u:real^3} <=> w = vec 0 \/ w = u` ASSUME_TAC);;
 634 e (MESON_TAC [IN_DOUBLE]);;
 635 e (ASM_REWRITE_TAC[]);;
 636 e (STRIP_TAC);;
 637 e (ASM_REWRITE_TAC[]);;
 638 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
 639 e (REWRITE_TAC[]);;
 640 e (ASM_REWRITE_TAC[]);;
 641 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
 642 e (REWRITE_TAC[]);;
 643
 644 let thm9 = top_thm();;
 645
 646 g `!w:real^3 u. ~(vec 0 = u) /\ {vec 0, u} w ==>  dist (vec 0,u)/(&2) = dist (circumcenter {vec 0, u},w)`;;
 647 e (REPEAT GEN_TAC);;
 648 e (STRIP_TAC);;
 649 e (POP_ASSUM MP_TAC);;
 650 e (SUBGOAL_THEN `{vec 0, u:real^3} w <=> w IN {vec 0, u}` ASSUME_TAC);;
 651 e (REWRITE_TAC [IN]);;
 652 e (SUBGOAL_THEN `(w:real^3) IN {vec 0, u:real^3} <=> w = vec 0 \/ w = u` ASSUME_TAC);;
 653 e (MESON_TAC [IN_DOUBLE]);;
 654 e (ASM_REWRITE_TAC[]);;
 655 e (SUBGOAL_THEN `circumcenter {vec 0, u:real^3} = midpoint (vec 0,u)` ASSUME_TAC);;
 656 e (ASM_MESON_TAC [thm7]);;
 657 e (STRIP_TAC);;
 658 e (ASM_REWRITE_TAC[]);;
 659 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
 660 e (ARITH_TAC);;
 661 e (ASM_REWRITE_TAC[]);;
 662 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
 663 e (ARITH_TAC);;
 664
 665 let thm10 = top_thm();;
 666
 667
 668
 669 g `(!u:real^3 . ?d. (!w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w)))
 670 ==> (!v:real^3. ~(vec 0 = v) ==> hl [vec 0;v] = dist (vec 0,v)/(&2))`;;
 671 e (STRIP_TAC);;
 672 e (GEN_TAC);;
 673 e (STRIP_TAC);;
 674 e (SUBGOAL_THEN `circumcenter {vec 0, v:real^3} = midpoint (vec 0,v)` ASSUME_TAC);;
 675 e (ASM_MESON_TAC [thm7]);;
 676 e (SUBGOAL_THEN `!w:real^3. {vec 0, v} w ==> (dist (vec 0,v) / (&2)) = dist (circumcenter {vec 0, v},w)` ASSUME_TAC);;
 677 e (ASM_MESON_TAC [thm10]);;
 678 e (ASM_REWRITE_TAC[]);;
 679 e (REWRITE_TAC [HL;set_of_list;radV]);;
 680 e (POP_ASSUM MP_TAC);;
 681 e (ASM_REWRITE_TAC[]);;
 682 e (SET_TAC[]);;
 683
 684 let thm11 = top_thm();;
 685
 686
 687 g `!v:real^3. ~(vec 0 = v) ==> hl [vec 0; v] = dist (vec 0,v) / &2`;;
 688 e (SUBGOAL_THEN `!u:real^3. ?d. !w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w)` ASSUME_TAC);;
 689 e (REWRITE_TAC [thm9]);;
 690 e (POP_ASSUM MP_TAC);;
 691 e (REWRITE_TAC [thm11]);;
 692
 693 let thm12 = top_thm();;
 694
 695 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
 696    (u IN V) ==> hl [vec 0;u] = dist (vec 0,u)/(&2)  `;;
 697 e (REPEAT GEN_TAC);;
 698 e (STRIP_TAC);;
 699 e (SUBGOAL_THEN `~(vec 0 = u:real^3)` ASSUME_TAC);;
 700 e (ASM_MESON_TAC [thm8]);;
 701 e (ASM_MESON_TAC [thm12]);;
 702
 703 let thm13 = top_thm();;
 704
 705 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
 706    (u IN V) ==> &1 <= hl [vec 0;u] `;;
 707 e (REPEAT GEN_TAC);;
 708 e (STRIP_TAC);;
 709 e (SUBGOAL_THEN `hl [vec 0; u:real^3] = dist (vec 0,u) / (&2)` ASSUME_TAC);;
 710 e (ASM_MESON_TAC [thm13]);;
 711 e (ASM_REWRITE_TAC[]);;
 712 e (ASM_MESON_TAC [thm2]);;
 713
 714 let thm14 = top_thm();;
 715
 716 g `!(V:real^3->bool). FINITE V /\ packing V /\ V SUBSET ball_annulus /\ &(CARD V) <= &12
 717   ==> sum V (\v. lmfun (hl [vec 0;v])) <= &12`;;
 718 e (REPEAT STRIP_TAC);;
 719 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> (&1) <= hl [vec 0;v]` ASSUME_TAC);;
 720 e (REPEAT STRIP_TAC);;
 721 e (ASM_MESON_TAC [thm14]);;
 722 e (POP_ASSUM (LABEL_TAC "F1"));;
 723 e (USE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
 724 e (STRIP_TAC);;
 725 e (SUBGOAL_THEN `!(v:real^3). (&1) <= hl [vec 0;v] ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_TAC);;
 726 e (STRIP_TAC);;
 727 e (MESON_TAC [thm1]);;
 728 e (POP_ASSUM (LABEL_TAC "F2"));;
 729 e (USE_THEN "F2" (MP_TAC o SPEC `v:real^3`));;
 730 e (STRIP_TAC);;
 731 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_TAC);;
 732 e (STRIP_TAC);;
 733 e (ASM_MESON_TAC[]);;
 734 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (hl [vec 0;v])) <= (&(CARD V)) * (&1)` ASSUME_TAC);;
 735 e (ASM_MESON_TAC [SUM_BOUND]);;
 736 e (POP_ASSUM MP_TAC);;
 737 e (REWRITE_TAC [ARITH_RULE `&(CARD (V:real^3->bool)) * &1 =  &(CARD V)`]);;
 738 e (STRIP_TAC);;
 739 e (ASM_MESON_TAC[REAL_LE_TRANS]);;
 740
 741 let thm15 = top_thm();;
 742
 743
 744 g `!(V:real^3->bool). FINITE V /\ packing V /\
 745   V SUBSET ball_annulus /\ ~(lmfun_ineq_center V)
 746   ==> &12 < &(CARD V)`;;
 747 e (GEN_TAC);;
 748 e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
 749 e (STRIP_TAC);;
 750 e (ASM_CASES_TAC `&12 < &(CARD (V:real^3->bool))`);;
 751 e (ASM_REWRITE_TAC[]);;
 752 e (POP_ASSUM MP_TAC);;
 753 e (PURE_REWRITE_TAC[REAL_NOT_LT]);;
 754 e (STRIP_TAC);;
 755 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v])) <= &12` ASSUME_TAC);;
 756 e (ASM_MESON_TAC [thm15]);;
 757 e (UNDISCH_TAC `~(sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v])) <= &12)`);;
 758 e (POP_ASSUM MP_TAC);;
 759 e (ABBREV_TAC `a = sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v]))`);;
 760 e (STRIP_TAC);;
 761 e (ASM_MESON_TAC[]);;
 762
 763 let condition_1 = top_thm();;
 764
 765 (*-------------------------------------------------------------------------*)
 766
 767 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))`;;
 768 e (REPEAT GEN_TAC);;
 769 e (DISCH_THEN (LABEL_TAC "F1"));;
 770 e (GEN_TAC);;
 771 e (STRIP_TAC);;
 772 e (USE_THEN "F1"(MP_TAC o SPEC `u:real^3`));;
 773 e (POP_ASSUM MP_TAC);;
 774 e (SET_TAC[]);;
 775
 776 let thm16 = top_thm();;
 777
 778 g `!(V:real^3->bool) V1. FINITE V /\ packing V /\
 779   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'`;;
 780 e (REPEAT GEN_TAC);;
 781 e (PURE_REWRITE_TAC [packing]);;
 782 e (STRIP_TAC);;
 783 e (PURE_REWRITE_TAC [weakly_saturated]);;
 784 e (PURE_REWRITE_TAC [r;r']);;
 785 e (GEN_TAC);;
 786 e (STRIP_TAC);;
 787 e (ASM_CASES_TAC `p:real^3 IN (V1:real^3->bool)`);;
 788 e (EXISTS_TAC `p:real^3`);;
 789 e (STRIP_TAC);;
 790 e (ASM_REWRITE_TAC[]);;
 791 e (PURE_REWRITE_TAC [DIST_REFL]);;
 792 e (ARITH_TAC);;
 793 e (ASM_CASES_TAC `?u:real^3. u IN V1 /\ dist(u,p) < (&2)` );;
 794 e (ASM_REWRITE_TAC[]);;
 795 e (POP_ASSUM MP_TAC);;
 796 e (PURE_REWRITE_TAC [NOT_EXISTS_THM]);;
 797 e (PURE_REWRITE_TAC [DE_MORGAN_THM]);;
 798 e (PURE_REWRITE_TAC [REAL_NOT_LT]);;
 799 e (STRIP_TAC);;
 800 e (SUBGOAL_THEN `!u:real^3. u IN (V1:real^3->bool) ==> &2 <= dist (u,p:real^3)` ASSUME_TAC);;
 801 e (POP_ASSUM MP_TAC);;
 802 e (REWRITE_TAC [thm16]);;
 803 e (UNDISCH_TAC `!y:real^3. (!x:real^3. x IN (V1:real^3->bool) ==> &2 <= dist (x,y)) ==> y IN V1`);;
 804 e (DISCH_THEN (LABEL_TAC "F1"));;
 805 e (USE_THEN "F1" (MP_TAC o SPEC `p:real^3`));;
 806 e (STRIP_TAC);;
 807 e (SUBGOAL_THEN `p:real^3 IN (V1:real^3->bool)` ASSUME_TAC);;
 808 e (UNDISCH_TAC `!u:real^3. u IN (V1:real^3->bool) ==> &2 <= dist (u,p)`);;
 809 e (POP_ASSUM MP_TAC);;
 810 e (REWRITE_TAC[]);;
 811 e (UNDISCH_TAC `~(p:real^3 IN (V1:real^3->bool))`);;
 812 e (POP_ASSUM MP_TAC);;
 813 e (SET_TAC[]);;
 814
 815 let thm17 = top_thm();;
 816
 817 (*---------------------------------------------------------------------------*)
 818 g `!h1 h2 g1 g2. (h1 o h2) o (g1 o g2) = h1 o (h2 o g1) o g2`;;
 819 e (REPEAT GEN_TAC);;
 820 e (PURE_REWRITE_TAC [o_ASSOC]);;
 821 e (ARITH_TAC);;
 822
 823
 824 let MUL_o_ASSOC = top_thm();;
 825
 826 (*
 827 g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) f b:real F X.(FINITE V) /\ packing V
 828    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 829     P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 830   (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\
 831    f facet_of P /\
 832    F = {f|f facet_of P}
 833    /\ (X = topological_component_yfan (vec 0,fan_of_polyhedron P))
 834    /\ (interior_point (vec 0) P)
 835    ==> (?(h: V -> X) (g: X -> V). (h o g = I /\ g o h = I))`;;
 836 e (REPEAT GEN_TAC);;
 837 e (STRIP_TAC);;
 838 e (SUBGOAL_THEN `(?(h1: V -> F) (g1: F-> V). h1 o g1 = I /\ g1 o h1 = I)` ASSUME_TAC);;
 839 e (ASM_MESON_TAC [CZZHBLI_1]);;
 840 e (SUBGOAL_THEN `(?(h2: F -> WF) (g2: WF -> F). h2 o g2 = I /\ g2 o h2 = I)` ASSUME_TAC);;
 841 e (ASM_MESON_TAC [AMHFNXP]);;
 842 e (POP_ASSUM MP_TAC);;
 843 e (POP_ASSUM MP_TAC);;
 844 e (REPEAT STRIP_TAC);;
 845 e (EXISTS_TAC `(h2:F->WF) o (h1:V->F)`);;
 846 e (EXISTS_TAC `(g1: F-> V) o (g2: WF -> F)`);;
 847 e (STRIP_TAC);;
 848 e (SUBGOAL_THEN `((h2:F->WF) o (h1:V->F)) o ((g1: F-> V) o (g2: WF -> F)) =
 849  (h2 o (h1 o g1) o g2)` ASSUME_TAC);;
 850 e (REWRITE_TAC [MUL_o_ASSOC]);;
 851 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 852 e (UNDISCH_TAC `(h1:V->F) o (g1:F->V) = I`);;
 853 e (STRIP_TAC);;
 854 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 855 e (PURE_REWRITE_TAC [o_ASSOC]);;
 856 e (PURE_REWRITE_TAC [I_O_ID]);;
 857 e (UNDISCH_TAC `(h2: F -> WF)o(g2: WF -> F)= I`);;
 858 e (REWRITE_TAC[]);;
 859 e (SUBGOAL_THEN `((g1: F-> V) o (g2: WF -> F)) o ((h2:F->WF) o (h1:V->F)) =
 860  (g1 o (g2 o h2) o h1)` ASSUME_TAC);;
 861 e (REWRITE_TAC [MUL_o_ASSOC]);;
 862 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 863 e (UNDISCH_TAC `(g2: WF -> F) o (h2: F -> WF) = I`);;
 864 e (STRIP_TAC);;
 865 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 866 e (PURE_REWRITE_TAC [o_ASSOC]);;
 867 e (PURE_REWRITE_TAC [I_O_ID]);;
 868 e (UNDISCH_TAC `(g1: F-> V)o(h1:V->F)= I`);;
 869 e (REWRITE_TAC[]);;
 870
 871 let V_TOPO_BIJ = top_thm();;
 872
 873
 874 g `!(V:real^3 -> bool) (P:real^3->bool) (u:real^3) f b:real F WF F_T.(FINITE V) /\ packing V
 875    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 876     P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 877   (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\
 878    f facet_of P /\
 879    FANO (fan_of_polyhedron P) /\
 880    F = {f|f facet_of P}
 881    /\ (WF = topological_component_yfan (vec 0,fan_of_polyhedron P))
 882    /\ (conforming (fan_of_polyhedron P))
 883    /\ (interior_point (vec 0) P) /\
 884    F_T = face_set_of_fan (fan_of_polyhedron P )
 885    ==> (?(h: V -> F_T) (g: F_T -> V). (h o g = I /\ g o h = I))`;;
 886
 887 e (REPEAT GEN_TAC);;
 888 e (STRIP_TAC);;
 889 e (SUBGOAL_THEN `(?(h1: V -> WF) (g1: WF -> V). h1 o g1 = I /\ g1 o h1 = I)` ASSUME_TAC);;
 890 e (ASM_MESON_TAC[V_TOPO_BIJ]);;
 891 e (SUBGOAL_THEN `(?(h2: WF -> F_T) (g2: F_T -> WF). h2 o g2 = I /\ g2 o h2 = I)`
 892 ASSUME_TAC);;
 893 e (UNDISCH_TAC `F_T = face_set_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
 894 e (UNDISCH_TAC `(WF' = topological_component_yfan (vec 0,fan_of_polyhedron (P:real^3->bool)))`);;
 895 e (UNDISCH_TAC `(conforming (fan_of_polyhedron (P:real^3->bool)))`);;
 896 e (UNDISCH_TAC `FANO (fan_of_polyhedron P)`);;
 897 e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
 898 e (ABBREV_TAC `V1 ={v | v extreme_point_of (P:real^3->bool)}`);;
 899 e (ABBREV_TAC `E1 ={{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
 900 e (MESON_TAC [UVPFEEP_1]);;
 901 e (POP_ASSUM MP_TAC);;
 902 e (POP_ASSUM MP_TAC);;
 903 e (REPEAT STRIP_TAC);;
 904 e (EXISTS_TAC `(h2:WF->F_T) o (h1:V->WF)`);;
 905 e (EXISTS_TAC `(g1: WF-> V) o (g2: F_T -> WF)`);;
 906 e (STRIP_TAC);;
 907 e (SUBGOAL_THEN `((h2:WF->F_T) o (h1:V->WF)) o ((g1: WF-> V) o (g2: F_T -> WF)) =
 908  (h2 o (h1 o g1) o g2)` ASSUME_TAC);;
 909 e (REWRITE_TAC [MUL_o_ASSOC]);;
 910 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 911 e (UNDISCH_TAC `(h1:V->WF) o (g1:WF->V) = I`);;
 912 e (STRIP_TAC);;
 913 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 914 e (PURE_REWRITE_TAC [o_ASSOC]);;
 915 e (PURE_REWRITE_TAC [I_O_ID]);;
 916 e (UNDISCH_TAC `(h2: WF -> F_T)o(g2: F_T -> WF)= I`);;
 917 e (REWRITE_TAC[]);;
 918 e (SUBGOAL_THEN `((g1: WF-> V) o (g2: F_T -> WF)) o ((h2:WF->F_T) o (h1:V->WF)) =
 919  (g1 o (g2 o h2) o h1)` ASSUME_TAC);;
 920 e (REWRITE_TAC [MUL_o_ASSOC]);;
 921 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 922 e (UNDISCH_TAC `(g2: F_T -> WF) o (h2: WF -> F_T) = I`);;
 923 e (STRIP_TAC);;
 924 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 925 e (PURE_REWRITE_TAC [o_ASSOC]);;
 926 e (PURE_REWRITE_TAC [I_O_ID]);;
 927 e (UNDISCH_TAC `(g1: WF-> V)o(h1:V->WF)= I`);;
 928 e (REWRITE_TAC[]);;
 929
 930 let V_FHYPER_BIJ = top_thm();;
 931 *)
 932 (*----------------------------------------------------------------------------*)
 933
 934 g `!(V:real^3 -> bool) (P:real^3->bool) X (f1:(real^3) -> (real^3->bool)) (f2:((real^3->bool))->(real^3)).
 935   (FINITE V) /\ packing V /\
 936   (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 937   P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 938   (polyhedron P) /\ (bounded P) /\
 939   (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
 940   f1 o f2 = I /\ f2 o f1 = I /\
 941   IMAGE f1 V = X
 942  ==> (sum (V) (\v:real^3. sol (vec 0) (f1(v))) = sum (X) (\v. sol (vec 0) v ))`;;
 943
 944 e (REPEAT GEN_TAC);;
 945 e (STRIP_TAC);;
 946 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);;
 947 e (REPEAT GEN_TAC);;
 948 e (STRIP_TAC);;
 949 e (SUBGOAL_THEN `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) (x:real^3)= I x` ASSUME_TAC);;
 950 e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) = I `);;
 951 e (MESON_TAC[]);;
 952 e (SUBGOAL_THEN `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) ->
 953 (real^3->bool))) (y:real^3)= I y` ASSUME_TAC);;
 954 e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) = I `);;
 955 e (MESON_TAC[]);;
 956 e (UNDISCH_TAC `((f2:(real^3->bool)->(real^3)) o (f1:(real^3) -> (real^3->bool))) (x:real^3)= I x`);;
 957 e (PURE_REWRITE_TAC [o_THM]);;
 958 e (ASM_REWRITE_TAC[]);;
 959 e (POP_ASSUM MP_TAC);;
 960 e (PURE_REWRITE_TAC [o_THM]);;
 961 e (REPEAT STRIP_TAC);;
 962 e (SUBGOAL_THEN `I (y:real^3) = I x` ASSUME_TAC);;
 963 e (POP_ASSUM MP_TAC);;
 964 e (POP_ASSUM MP_TAC);;
 965 e (MESON_TAC[]);;
 966 e (POP_ASSUM MP_TAC);;
 967 e (SIMP_TAC[I_THM]);;
 968 e (MP_TAC(ISPECL [`f1:(real^3)->(real^3->bool)`;`(\v:(real^3->bool). sol (vec 0) v)`;`(V:real^3->bool)`] SUM_IMAGE));;
 969 e (STRIP_TAC);;
 970 e (SUBGOAL_THEN `sum (IMAGE (f1:(real^3)->(real^3->bool)) V) (\v:(real^3->bool). sol (vec 0) v) =
 971           sum (V:real^3->bool) ((\v. sol (vec 0) v) o f1)` ASSUME_TAC);;
 972 e (POP_ASSUM MP_TAC);;
 973 e (POP_ASSUM MP_TAC);;
 974 e (MESON_TAC[]);;
 975 e (POP_ASSUM MP_TAC);;
 976 e (UNDISCH_TAC `IMAGE (f1:(real^3)->(real^3->bool)) (V:real^3->bool) = (X:(real^3->bool)->bool)`);;
 977 e (STRIP_TAC);;
 978 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 979 e (STRIP_TAC);;
 980 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
 981 e (SUBGOAL_THEN `(\v:real^3. sol (vec 0) (f1 v)) = ((\t. sol (vec 0) t) o f1)` ASSUME_TAC);;
 982 e (REWRITE_TAC[FUN_EQ_THM]);;
 983 e (GEN_TAC);;
 984 e (PURE_REWRITE_TAC [o_THM]);;
 985 e (REWRITE_TAC[]);;
 986 e (ASM_REWRITE_TAC[]);;
 987
 988 let thm18 = top_thm();;
 989
 990 (*
 991 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)).
 992    (FINITE V) /\ packing V
 993    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
 994    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
 995    (polyhedron P) /\ (bounded P) /\
 996    (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
 997    (interior_point (vec 0) P) /\
 998    F = {f|f facet_of P} /\
 999    f1 o f2 = I /\ f2 o f1 = I /\
1000    f3 o f4 = I /\ f4 o f3 = I /\
1001    IMAGE f1 V = X  /\
1002    IMAGE f3 V = F
1003   ==> 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)))`;;
1004 e (REPEAT GEN_TAC);;
1005 e (STRIP_TAC);;
1006 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);;
1007 e (GEN_TAC);;
1008 e (STRIP_TAC);;
1009
1010
1011
1012 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)})))) <=
1013 (sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v)))`;;
1014
1015
1016 search [`sum s f <= sum s g`];;
1017
1018 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)).
1019    (FINITE V) /\ packing V
1020    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
1021    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
1022    (polyhedron P) /\ (bounded P) /\
1023    (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
1024    (interior_point (vec 0) P) /\
1025    F = {f|f facet_of P} /\
1026    f1 o f2 = I /\ f2 o f1 = I /\
1027    f3 o f4 = I /\ f4 o f3 = I /\
1028    IMAGE f1 V = X  /\
1029    IMAGE f3 V = F`;;
1030 type_of `sum (V) (\v:real^3. sol (vec 0) (f1(v)))`;;
1031 search [`IMAGE`];;
1032
1033 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)).
1034    (FINITE V) /\ packing V
1035    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
1036    P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\
1037    (polyhedron P) /\ (bounded P) /\
1038    (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
1039    (interior_point (vec 0) P)
1040    F_T = face_set_of_fan (fan_of_polyhedron P )
1041    /\ f1 o f2 = I /\ f2 o f1 = I
1042    /\ f3 o f4 = I /\ f4 o f3 = I
1043    /\ IMAGE f1 V = X
1044    /\ IMAGE f3 V = F_T
1045 ==> (!(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 })
1046
1047 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)).
1048    (FINITE V) /\ packing V
1049    /\(weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
1050    P = INTERS {half_spaces g_fun u| (u IN V) /\
1051    (polyhedron P) /\ (bounded P) /\ (f = {p | u dot p = g_fun u } INTER P) /\
1052    (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
1053    (X = topological_component_yfan (vec 0,fan_of_polyhedron P)) /\
1054    F_T = face_set_of_fan (fan_of_polyhedron P ) /\
1055    F = {l | l facet_of P} /\
1056    /\ f1 o f2 = I /\ f2 o f1 = I
1057    /\ IMAGE f1 V = F_T
1058
1059   (~(vec 0 = u))} /\
1060    /\ (interior_point (vec 0) P)
1061
1062     ==>
1063 type_of `face_set_of_fan (fan_of_polyhedron P )`;;
1064 type_of `facet_of`;;
1065
1066 type_of `extreme_point_of`;;
1067 type_of `facet_of`;;
1068 inverse;;
1069 EXTREME_POINT_OF_LINEAR_IMAGE;;
1070
1071 search [`leaner f`];;
1072
1073 search [`extreme_point_of`];;
1074
1075
1076 type_of `f facet_of P`;;
1077 type_of `(?(g1:F -> V). h1 o g1 = I /\ g1 o h1 = I)/\
1078    (?(g2:F_T -> V). h2 o g2 = I /\ g2 o h2 = I) `;;
1079 *)
1080
1081
1082 (*---------------------------------------------------------------------------*)
1083 (*Dart Bound*)
1084
1085 g `!(V:real^3 -> bool).(V SUBSET ball_annulus) ==> (!x:real^3. x IN V ==>  ~(vec 0 = x))`;;
1086 e (GEN_TAC);;
1087 e (PURE_REWRITE_TAC [ball_annulus;cball;ball;DIFF]);;
1088 e (STRIP_TAC);;
1089 e (GEN_TAC);;
1090 e (STRIP_TAC);;
1091 e (SUBGOAL_THEN `x:real^3 IN {x | x IN {y | dist (vec 0,y) <= &2 * h0} /\
1092            ~(x IN {y | dist (vec 0,y) < &2})}` ASSUME_TAC);;
1093 e (ASM_MESON_TAC [SUBSET]);;
1094 e (ASM_CASES_TAC `vec 0 = x:real^3`);;
1095 e (SUBGOAL_THEN `(vec 0):real^3 IN {x | x IN {y | dist (vec 0,y) <= &2 * h0} /\
1096            ~(x IN {y | dist (vec 0,y) < &2})}` ASSUME_TAC);;
1097 e (ASM_MESON_TAC[]);;
1098 e (POP_ASSUM MP_TAC);;
1099 e (REWRITE_TAC [IN_ELIM_THM]);;
1100 e (REWRITE_TAC [DIST_REFL]);;
1101 e (STRIP_TAC);;
1102 e (ASM_MESON_TAC [ARITH_RULE `&0 < &2`]);;
1103 e (ASM_REWRITE_TAC[]);;
1104
1105 let th54 = top_thm();;
1106
1107
1108 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)`;;
1109 e (REPEAT GEN_TAC);;
1110 e (STRIP_TAC);;
1111 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);;
1112 e (ASM_REWRITE_TAC[half_spaces]);;
1113 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);;
1114 e (GEN_TAC);;
1115 e (STRIP_TAC);;
1116 e (REWRITE_TAC [SUBSET]);;
1117 e (GEN_TAC);;
1118 e (REWRITE_TAC [IN_ELIM_THM]);;
1119 e (REWRITE_TAC [REAL_LT_IMP_LE]);;
1120 e (POP_ASSUM (LABEL_TAC "F1"));;
1121 e (SUBGOAL_THEN ` !u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u)
1122           ==> INTERS {{p | u dot p < g_fun u} | u IN V /\ ~(vec 0 = u)} SUBSET {p | u dot p <= g_fun u}` ASSUME_TAC);;
1123 e (GEN_TAC);;
1124 e (STRIP_TAC);;
1125 e (REWRITE_TAC [INTERS;SUBSET;IN_ELIM_THM]);;
1126 e (REPEAT STRIP_TAC);;
1127 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1128 e (ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]);;
1129 e (POP_ASSUM (fun th -> (MP_TAC (SPEC `{p:real^3 | u dot p < g_fun u}` th))));;
1130 e (REWRITE_TAC[]);;
1131 e (SUBGOAL_THEN `?u':real^3. (u' IN V /\ ~(vec 0 = u')) /\
1132         {p | u dot p < g_fun u} = {p | u' dot p < g_fun u'}` ASSUME_TAC);;
1133 e (EXISTS_TAC `u:real^3`);;
1134 e (ASM_REWRITE_TAC[]);;
1135 e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
1136 e (REPEAT STRIP_TAC);;
1137 e (POP_ASSUM (LABEL_TAC "F2"));;
1138 e (USE_THEN "F2" (MP_TAC o SPEC `x:real^3`));;
1139 e (UNDISCH_TAC `u:real^3 dot x < g_fun u`);;
1140 e (MESON_TAC[]);;
1141 e (POP_ASSUM MP_TAC);;
1142 e (ABBREV_TAC `(s:real^3->bool) = INTERS {{p:real^3 | u dot p < g_fun u} | u IN V /\ ~(vec 0 = u)}`);;
1143 e (DISCH_THEN (LABEL_TAC "F3"));;
1144 e (REWRITE_TAC [INTERS;SUBSET;IN_ELIM_THM]);;
1145 e (REPEAT STRIP_TAC);;
1146 e (REMOVE_THEN "F3" (MP_TAC o SPEC `u':real^3`));;
1147 e (ASM_REWRITE_TAC[SUBSET]);;
1148 e (STRIP_TAC);;
1149 e (UNDISCH_TAC `x IN (s:real^3->bool)`);;
1150 e (POP_ASSUM MP_TAC);;
1151 e (MESON_TAC[]);;
1152 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);;
1153 e (GEN_TAC);;
1154 e (REPEAT STRIP_TAC);;
1155 e (PURE_REWRITE_TAC [IN_ELIM_THM]);;
1156 e (PURE_REWRITE_TAC [DOT_RZERO;g_fun]);;
1157 e (SUBGOAL_THEN `&1 <= dist (vec 0,(u:real^3)) / &2` ASSUME_TAC);;
1158 e (ASM_MESON_TAC[thm2]);;
1159 e (SUBGOAL_THEN `&0 < &2` ASSUME_TAC);;
1160 e (ARITH_TAC);;
1161 e (SUBGOAL_THEN `&1 / &2 <= (dist (vec 0,(u:real^3)) / &2) / &2` ASSUME_TAC);;
1162 e (POP_ASSUM MP_TAC);;
1163 e (POP_ASSUM MP_TAC);;
1164 e (MESON_TAC [REAL_LE_DIV2_EQ]);;
1165 e (POP_ASSUM MP_TAC);;
1166 e (REWRITE_TAC [ARITH_RULE `(dist (vec 0,(u:real^3)) / &2) / &2 = dist (vec 0,u) / &4`]);;
1167 e (STRIP_TAC);;
1168 e (SUBGOAL_THEN `dist (vec 0,u:real^3) <= &2 * h0` ASSUME_TAC);;
1169 e (ASM_MESON_TAC [thm21]);;
1170 e (SUBGOAL_THEN `&0 < &4` ASSUME_TAC);;
1171 e (ARITH_TAC);;
1172 e (SUBGOAL_THEN `dist (vec 0,u:real^3) / &4 <= (&2 * h0) / &4` ASSUME_TAC);;
1173 e (POP_ASSUM MP_TAC);;
1174 e (POP_ASSUM MP_TAC);;
1175 e (MESON_TAC [REAL_LE_DIV2_EQ]);;
1176 e (POP_ASSUM MP_TAC);;
1177 e (REWRITE_TAC [ARITH_RULE `(&2 * h0) / &4 = h0 / &2`]);;
1178 e (STRIP_TAC);;
1179 e (SUBGOAL_THEN `(&0 <= (pi / &6)) /\ ((pi / &6) <= pi)` ASSUME_TAC);;
1180 e (MP_TAC PI_POS_LE);;
1181 e (ARITH_TAC);;
1182 e (SUBGOAL_THEN `acs (cos (pi/ &6)) = (pi / &6)` ASSUME_TAC);;
1183 e (POP_ASSUM MP_TAC);;
1184 e (REWRITE_TAC [ACS_COS]);;
1185 e (POP_ASSUM MP_TAC);;
1186 e (PURE_REWRITE_TAC [COS_PI6]);;
1187 e (REPEAT STRIP_TAC);;
1188 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);;
1189 e (STRIP_TAC);;
1190 e (UNDISCH_TAC `&1 / &2 <= dist (vec 0,u:real^3) / &4`);;
1191 e (MP_TAC (ARITH_RULE `-- &1 <= &1 / &2`));;
1192 e (ARITH_TAC);;
1193 e (STRIP_TAC);;
1194 e (UNDISCH_TAC `dist (vec 0,u:real^3) / &4 <= h0 / &2`);;
1195 e (PURE_REWRITE_TAC [h0]);;
1196 e (SUBGOAL_THEN `#1.26 / &2 < sqrt (&3) / &2` ASSUME_TAC);;
1197 e (MP_TAC (ARITH_RULE `&0 < &2`));;
1198 e (SUBGOAL_THEN `#1.26 < sqrt (&3)` ASSUME_TAC);;
1199 e (SUBGOAL_THEN `#1.26 pow 2 < &3` ASSUME_TAC);;
1200 e (ARITH_TAC);;
1201 e (POP_ASSUM MP_TAC);;
1202 e (REWRITE_TAC [REAL_LT_RSQRT]);;
1203 e (POP_ASSUM MP_TAC);;
1204 e (MESON_TAC [REAL_LT_DIV2_EQ]);;
1205 e (POP_ASSUM MP_TAC);;
1206 e (ARITH_TAC);;
1207 e (SUBGOAL_THEN `(&3) <= &2 pow 2` ASSUME_TAC);;
1208 e (ARITH_TAC);;
1209 e (SUBGOAL_THEN `sqrt (&3) <= &2` ASSUME_TAC);;
1210 e (POP_ASSUM MP_TAC);;
1211 e (MP_TAC (ARITH_RULE `&0 <= &3 /\ &0 <= &2`));;
1212 e (MESON_TAC [REAL_LE_LSQRT]);;
1213 e (SUBGOAL_THEN `sqrt (&3) <= &1 * &2` ASSUME_TAC);;
1214 e (POP_ASSUM MP_TAC);;
1215 e (MESON_TAC [ARITH_RULE `&2 = &1 * &2`]);;
1216 e (POP_ASSUM MP_TAC);;
1217 e (MP_TAC (ARITH_RULE `&0 < &2`));;
1218 e (MESON_TAC [REAL_LE_LDIV_EQ]);;
1219 e (SUBGOAL_THEN `acs (sqrt (&3) / &2) < acs (dist (vec 0,u:real^3) / &4)` ASSUME_TAC);;
1220 e (POP_ASSUM MP_TAC);;
1221 e (REWRITE_TAC [ACS_MONO_LT]);;
1222 e (POP_ASSUM MP_TAC);;
1223 e (ASM_REWRITE_TAC[]);;
1224 e (REWRITE_TAC [REAL_SUB_LT]);;
1225 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);;
1226 e (PURE_REWRITE_TAC [IN_INTERS]);;
1227 e (REWRITE_TAC [IN_ELIM_THM]);;
1228 e (POP_ASSUM (LABEL_TAC "F1"));;
1229 e (STRIP_TAC);;
1230 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1231 e (STRIP_TAC);;
1232 e (ASM_REWRITE_TAC []);;
1233 e (ASM_MESON_TAC[]);;
1234 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);;
1235 e (GEN_TAC);;
1236 e (STRIP_TAC);;
1237 e (REWRITE_TAC [OPEN_HALFSPACE_LT]);;
1238 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);;
1239 e (POP_ASSUM (LABEL_TAC "F1"));;
1240 e (GEN_TAC);;
1241 e (STRIP_TAC);;
1242 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1243 e (ASM_REWRITE_TAC[]);;
1244 e (STRIP_TAC);;
1245 e (POP_ASSUM MP_TAC);;
1246 e (REWRITE_TAC [INTERIOR_OPEN]);;
1247 e (SUBGOAL_THEN `!u:real^3. u IN (V:real^3->bool) /\ ~(vec 0 = u) ==>
1248   interior_point (vec 0) ({p:real^3 | u dot p < g_fun u}) ` ASSUME_TAC);;
1249 e (GEN_TAC);;
1250 e (POP_ASSUM (LABEL_TAC "F1"));;
1251 e (STRIP_TAC);;
1252 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1253 e (ASM_REWRITE_TAC[]);;
1254 e (STRIP_TAC);;
1255 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}`);;
1256 e (DISCH_THEN (LABEL_TAC "F1"));;
1257 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1258 e (STRIP_TAC);;
1259 e (SUBGOAL_THEN `vec 0 IN (interior ({p:real^3 | u dot p < g_fun u}))` ASSUME_TAC);;
1260 e (POP_ASSUM MP_TAC);;
1261 e (POP_ASSUM MP_TAC);;
1262 e (ASM_REWRITE_TAC[]);;
1263 e (MESON_TAC[]);;
1264 e (POP_ASSUM MP_TAC);;
1265 e (REWRITE_TAC [IN_INTERIOR_CBALL]);;
1266 e (REWRITE_TAC [interior_point]);;
1267 e (STRIP_TAC);;
1268 e (EXISTS_TAC `e:real`);;
1269 e (ASM_REWRITE_TAC[]);;
1270 e (MP_TAC (ISPECL [`(vec 0):real^3`;`e:real`] BALL_SUBSET_CBALL));;
1271 e (POP_ASSUM MP_TAC);;
1272 e (MESON_TAC [SUBSET_TRANS]);;
1273
1274 e (MP_TAC (ISPECL [`{{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`] OPEN_INTERS));;
1275 e (STRIP_TAC);;
1276 e (SUBGOAL_THEN `FINITE {{p:real^3 | u dot p < g_fun u} | u IN (V:real^3->bool) /\ ~(vec 0 = u)}` ASSUME_TAC);;
1277 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
1278 e (STRIP_TAC);;
1279 e (MP_TAC (ISPECL [`(\u:real^3. {p:real^3 | u dot p < g_fun u})`;`V:real^3->bool`] FINITE_IMAGE));;
1280 e (ASM_REWRITE_TAC [IMAGE]);;
1281 e (STRIP_TAC);;
1282 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);;
1283 e (REWRITE_TAC[EXTENSION]);;
1284 e (GEN_TAC);;
1285 e (EQ_TAC);;
1286 e (REWRITE_TAC [IN_ELIM_THM]);;
1287 e (STRIP_TAC);;
1288 e (EXISTS_TAC `u:real^3`);;
1289 e (ASM_REWRITE_TAC[]);;
1290 e (STRIP_TAC);;
1291 e (REWRITE_TAC [IN_ELIM_THM]);;
1292 e (REWRITE_TAC [IN_ELIM_THM]);;
1293 e (STRIP_TAC);;
1294 e (EXISTS_TAC `x':real^3`);;
1295 e (SUBGOAL_THEN `~(vec 0 = x':real^3)` ASSUME_TAC);;
1296 e (ASM_MESON_TAC [th54]);;
1297 e (ASM_REWRITE_TAC[]);;
1298 e (REWRITE_TAC [EXTENSION]);;
1299 e (REWRITE_TAC [IN_ELIM_THM]);;
1300 e (ASM_MESON_TAC[]);;
1301 e (ASM_REWRITE_TAC[]);;
1302
1303 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);;
1304 e (STRIP_TAC);;
1305 e (REWRITE_TAC [IN_ELIM_THM]);;
1306 e (STRIP_TAC);;
1307 e (ASM_REWRITE_TAC[]);;
1308 e (ASM_MESON_TAC[]);;
1309 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);;
1310 e (POP_ASSUM MP_TAC);;
1311 e (POP_ASSUM MP_TAC);;
1312 e (POP_ASSUM MP_TAC);;
1313 e (MESON_TAC[]);;
1314 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);;
1315 e (ASM_MESON_TAC [INTERIOR_MAXIMAL]);;
1316 e (SUBGOAL_THEN `(vec 0):real^3 IN (interior P)` ASSUME_TAC);;
1317 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)})`);;
1318 e (POP_ASSUM MP_TAC);;
1319 e (REWRITE_TAC [SUBSET]);;
1320 e (MESON_TAC[]);;
1321 e (POP_ASSUM MP_TAC);;
1322 e (REWRITE_TAC [IN_INTERIOR;interior_point]);;
1323
1324 let th51= top_thm();;
1325
1326
1327 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)`;;
1328 e (REPEAT GEN_TAC);;
1329 e (STRIP_TAC);;
1330 e (REWRITE_TAC [fan_of_polyhedron;fully_surrounded]);;
1331 e (STRIP_TAC);;
1332 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1333 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
1334 e (ASM_MESON_TAC[th51]);;
1335 e (POP_ASSUM MP_TAC);;
1336 e (POP_ASSUM MP_TAC);;
1337 e (POP_ASSUM MP_TAC);;
1338 e (MESON_TAC [BSXAQBQ]);;
1339
1340 let th52 = top_thm();;
1341
1342 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)`;;
1343 e (REPEAT GEN_TAC);;
1344 e (STRIP_TAC);;
1345 e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
1346 e (ASM_MESON_TAC[th52]);;
1347 e (POP_ASSUM MP_TAC);;
1348 e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
1349 e (REWRITE_TAC [PIIJBJK]);;
1350
1351 let th53 = top_thm();;
1352
1353 g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V)  /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
1354 ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==>
1355  (dart (hypermap_of_fan (fan_of_polyhedron P))) = dart_of_fan (fan_of_polyhedron P)`;;
1356
1357 e (REPEAT GEN_TAC);;
1358 e (STRIP_TAC);;
1359 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
1360 e (ASM_MESON_TAC [th51]);;
1361 e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
1362 e (ASM_MESON_TAC [JLIGZGS]);;
1363 e (POP_ASSUM MP_TAC);;
1364 e (REWRITE_TAC [fan_of_polyhedron]);;
1365 e (REWRITE_TAC [GSYM FANO_OF_FAN]);;
1366 e (ASM_REWRITE_TAC[]);;
1367 e (STRIP_TAC);;
1368 e (MP_TAC (ISPECL [`FST (fan_of_polyhedron (P:real^3 -> bool))`;`SND (fan_of_polyhedron (P:real^3 -> bool))`] COMPONENTS_HYPERMAP_OF_FAN));;
1369 e (ASM_REWRITE_TAC[fan_of_polyhedron]);;
1370 e (ASM_REWRITE_TAC[]);;
1371 e (STRIP_TAC);;
1372
1373 let DART_OF_HYPERMAP_FAN = top_thm();;
1374
1375
1376 let FULLY_SURROUND_IS_NON_ISOLATED_FAN2 = prove(`!(V:real^3->bool) (E:(real^3->bool)->bool).
1377 FANO(V,E) /\ (!v. v IN V ==> CARD (set_of_edge v V E) >1)
1378 ==> dart2_of_fan (V,E) = {}`,REPEAT STRIP_TAC
1379 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
1380 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);;
1381
1382 g `!(V:real^3->bool) (E:(real^3->bool)->bool).
1383 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)
1384 ==> dart_of_fan (V,E) = dart1_of_fan (V,E)`;;
1385 e (REPEAT GEN_TAC);;
1386 e (STRIP_TAC);;
1387 e (REWRITE_TAC [EXTENSION]);;
1388 e (GEN_TAC);;
1389 e (EQ_TAC);;
1390 e (POP_ASSUM (LABEL_TAC "F1"));;
1391 e (STRIP_TAC);;
1392 e (REMOVE_THEN "F1" (MP_TAC o SPEC `x:real^3#real^3`));;
1393 e (ASM_REWRITE_TAC[]);;
1394 e (POP_ASSUM MP_TAC);;
1395 e (REWRITE_TAC [dart_of_fan;UNION;IN_ELIM_THM]);;
1396 e (STRIP_TAC);;
1397 e (STRIP_TAC);;
1398 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);;
1399 e (ASM_REWRITE_TAC[CARD_CLAUSES]);;
1400 e (POP_ASSUM MP_TAC);;
1401 e (POP_ASSUM MP_TAC);;
1402 e (ARITH_TAC);;
1403 e (STRIP_TAC);;
1404 e (REWRITE_TAC [dart1_of_fan]);;
1405 e (REWRITE_TAC [IN_ELIM_THM]);;
1406 e (EXISTS_TAC `v:real^3`);;
1407 e (EXISTS_TAC `w:real^3`);;
1408 e (ASM_REWRITE_TAC[]);;
1409 e (REWRITE_TAC[dart1_of_fan;dart_of_fan;IN_UNION]);;
1410 e (STRIP_TAC);;
1411 e (ASM_REWRITE_TAC[]);;
1412
1413 let FULLY_SURROUND_IS_NON_ISOLATED_FAN3 = top_thm();;
1414
1415 let DARTSET_FULLY_SURROUNDED_IS_NON_ISOLATED_FAN2 = prove (`!(V:real^3->bool) (E:(real^3->bool)->bool).
1416 FANO(V,E) /\ (!v. v IN V ==>CARD (set_of_edge v V E) >1)
1417 ==> 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[]);;
1418
1419
1420 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[]);;
1421
1422 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[]);;
1423
1424 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`;;
1425 e (REPEAT GEN_TAC);;
1426 e (REWRITE_TAC [fully_surrounded]);;
1427 e (STRIP_TAC);;
1428 e (POP_ASSUM MP_TAC);;
1429 e (POP_ASSUM MP_TAC);;
1430 e (POP_ASSUM(LABEL_TAC "F1"));;
1431 e (REPEAT STRIP_TAC);;
1432 e (ASM_CASES_TAC `CARD (set_of_edge (FST (x:real^3#real^3)) (V:real^3->bool) (E:(real^3->bool)->bool)) > 1`);;
1433 e (ASM_REWRITE_TAC[]);;
1434 e (REMOVE_THEN "F1" (MP_TAC o SPEC `x:real^3#real^3`));;
1435 e (STRIP_TAC);;
1436 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 ));;
1437 e (ASM_REWRITE_TAC[]);;
1438 e (SUBGOAL_THEN `FST (x:real^3#real^3) IN (V:real^3->bool)` ASSUME_TAC);;
1439 e (UNDISCH_TAC `(x:real^3#real^3) IN dart_of_fan ((V:real^3->bool),(E:(real^3->bool)->bool))`);;
1440 e (ONCE_REWRITE_TAC [ARITH_RULE `(x:real^3#real^3) = (FST x, SND x)`]);;
1441 e (PURE_REWRITE_TAC [dart_of_fan]);;
1442 e (REWRITE_TAC [UNION]);;
1443 e (REWRITE_TAC [IN_ELIM_THM]);;
1444 e (STRIP_TAC);;
1445 e (ASM_REWRITE_TAC[]);;
1446 e (ASM_REWRITE_TAC[]);;
1447 e (SUBGOAL_THEN `UNIONS (E:(real^3->bool) -> bool) SUBSET (V:real^3->bool)` ASSUME_TAC);;
1448 e (UNDISCH_TAC `FANO (V:real^3->bool,E:(real^3->bool) -> bool)`);;
1449 e (REWRITE_TAC [FANO]);;
1450 e (MESON_TAC[]);;
1451 e (POP_ASSUM MP_TAC);;
1452 e (REWRITE_TAC [UNIONS;SUBSET]);;
1453 e (DISCH_THEN (LABEL_TAC "F1"));;
1454 e (REMOVE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
1455 e (REWRITE_TAC [IN_ELIM_THM]);;
1456 e (STRIP_TAC);;
1457 e (SUBGOAL_THEN `v:real^3 IN {v:real^3,w:real^3}` ASSUME_TAC);;
1458 e (SET_TAC[]);;
1459 e (ASM_MESON_TAC[]);;
1460 e (ASM_REWRITE_TAC[]);;
1461 e (STRIP_TAC);;
1462 e (SUBGOAL_THEN `azim_dart (V:real^3->bool,E:(real^3->bool) -> bool) (x:real^3#real^3) < pi` ASSUME_TAC);;
1463 e (ASM_MESON_TAC[]);;
1464 e (POP_ASSUM MP_TAC);;
1465 e (POP_ASSUM SUBST1_TAC);;
1466 e (MP_TAC PI_POS);;
1467 e (ARITH_TAC);;
1468
1469 let FULLY_EDGE  = top_thm();;
1470
1471 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)`;;
1472 e (REPEAT GEN_TAC);;
1473 e (REPEAT STRIP_TAC);;
1474 e (ASM_MESON_TAC [FULLY_EDGE]);;
1475
1476 let FULLY_EDGE1 = top_thm();;
1477
1478 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)`;;
1479 e (REPEAT GEN_TAC);;
1480 e (STRIP_TAC);;
1481 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);;
1482 e (ASM_MESON_TAC [FULLY_EDGE1]);;
1483 e (ASM_MESON_TAC [FULLY_SURROUND_IS_NON_ISOLATED_FAN3]);;
1484
1485 let FULLY_SURROUNDED_IMP_DART = top_thm();;
1486
1487
1488 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))) <=
1489    (6*(CARD (face_set_of_fan (fan_of_polyhedron P)))-12)`;;
1490 e (REPEAT GEN_TAC);;
1491 e (STRIP_TAC);;
1492 e (SUBGOAL_THEN `conforming (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
1493 e (ASM_MESON_TAC [th53]);;
1494 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
1495 e (ASM_MESON_TAC [th51]);;
1496 e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
1497 e (ASM_MESON_TAC [JLIGZGS]);;
1498 e (SUBGOAL_THEN `connected_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
1499 e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
1500 e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
1501 e (REWRITE_TAC [fan_of_polyhedron]);;
1502 e (ASM_MESON_TAC [WGVWSKE]);;
1503 e (SUBGOAL_THEN `planar_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
1504 e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
1505 e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
1506 e (REWRITE_TAC [fan_of_polyhedron]);;
1507 e (ASM_MESON_TAC [GGRLKHP]);;
1508 e (SUBGOAL_THEN `plain_hypermap (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
1509 e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3 -> bool))`);;
1510 e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3 -> bool))`);;
1511 e (REWRITE_TAC [fan_of_polyhedron]);;
1512 e (ASM_MESON_TAC [PLAIN_HYPERMAP]);;
1513 e (SUBGOAL_THEN `dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))) =
1514              dart_of_fan (fan_of_polyhedron P)` ASSUME_TAC);;
1515 e (ASM_MESON_TAC [DART_OF_HYPERMAP_FAN]);;
1516 e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
1517 e (UNDISCH_TAC `conforming (fan_of_polyhedron (P:real^3->bool))`);;
1518 e (REWRITE_TAC [fan_of_polyhedron;conforming]);;
1519 e (MESON_TAC[]);;
1520 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);;
1521 e (GEN_TAC);;
1522 e (STRIP_TAC);;
1523 e (SUBGOAL_THEN `x IN dart_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
1524 e (ASM_MESON_TAC[]);;
1525 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));;
1526 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1527 e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`FANO (fan_of_polyhedron (P:real^3->bool))`);;
1528 e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`fully_surrounded (fan_of_polyhedron (P:real^3->bool))`);;
1529 e (STRIP_TAC);;
1530 e (SUBGOAL_THEN `x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
1531 e (ASM_MESON_TAC[]);;
1532 e (SUBGOAL_THEN `FAN (vec 0,fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
1533 e (UNDISCH_TAC `FANO (fan_of_polyhedron (P:real^3->bool))`);;
1534 e (REWRITE_TAC [fan_of_polyhedron]);;
1535 e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
1536 e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
1537 e (MESON_TAC [FANO_OF_FAN]);;
1538 e (STRIP_TAC);;
1539 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);;
1540 e (POP_ASSUM MP_TAC);;
1541 e (REWRITE_TAC [fan_of_polyhedron]);;
1542 e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
1543 e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
1544 e (MESON_TAC [COMPONENTS_HYPERMAP_OF_FAN]);;
1545 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1546 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);;
1547 e (UNDISCH_TAC `x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
1548 e (REWRITE_TAC [fan_of_polyhedron]);;
1549 e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
1550 e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
1551 e (REWRITE_TAC [e_fan_pair_ext]);;
1552 e (ARITH_TAC);;
1553 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1554 e (POP_ASSUM MP_TAC);;
1555 e (POP_ASSUM MP_TAC);;
1556 e (REWRITE_TAC [fan_of_polyhedron]);;
1557 e (ABBREV_TAC `V_P = {v | v extreme_point_of (P:real^3->bool)}`);;
1558 e (ABBREV_TAC `E_P = {{v, w} | ~(v = w) /\ convex hull {v, w} face_of (P:real^3->bool)}`);;
1559 e (MESON_TAC [E_HAS_NO_FIXED_POINTS_IN_D1]);;
1560 e (SUBGOAL_THEN `surrounded_node (fan_of_polyhedron (P:real^3->bool)) (FST (x:real^3#real^3))` ASSUME_TAC);;
1561 e (REWRITE_TAC [fan_of_polyhedron;surrounded_node]);;
1562 e (GEN_TAC);;
1563 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1564 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);;
1565 e (UNDISCH_TAC `fully_surrounded (fan_of_polyhedron (P:real^3->bool))`);;
1566 e (REWRITE_TAC [fan_of_polyhedron;fully_surrounded]);;
1567 e (POP_ASSUM (LABEL_TAC "F1"));;
1568 e (REMOVE_THEN "F1" (MP_TAC o SPEC `x':real^3#real^3`));;
1569 e (MESON_TAC[]);;
1570 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));;
1571 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1572 e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`FAN (vec 0,fan_of_polyhedron (P:real^3->bool))`);;
1573 e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`x IN dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
1574 e (FIND_ASSUM (fun th -> REWRITE_TAC[th])`surrounded_node (fan_of_polyhedron (P:real^3->bool)) (FST (x:real^3#real^3))`);;
1575 e (REWRITE_TAC [GE]);;
1576
1577 e (REWRITE_TAC [fan_of_polyhedron;face_set_of_fan]);;
1578 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1579
1580 e (MP_TAC (ISPECL [`hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))`]lemmaTGJISOK));;
1581 e (REWRITE_TAC [number_of_faces]);;
1582 e (ASM_REWRITE_TAC[]);;
1583
1584
1585 let th5 = top_thm();;
1586
1587 (*----------------------------------------------------------------------------*)
1588 (* proof CARD V = CARD {f|f facet_of V}*)
1589
1590 g `!(V:real^3 -> bool) (P:real^3 -> bool) F.(FINITE V) /\ packing V /\ (V SUBSET ball_annulus) /\
1591 (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)`;;
1592 e (REPEAT GEN_TAC);;
1593 e (STRIP_TAC);;
1594 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);;
1595 e (ASM_MESON_TAC [CZZHBLI_1]);;
1596 e (POP_ASSUM MP_TAC);;
1597 e (STRIP_TAC);;
1598 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);;
1599 e (REPEAT GEN_TAC);;
1600 e (STRIP_TAC);;
1601 e (SUBGOAL_THEN `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) x:real^3 = I x` ASSUME_TAC);;
1602 e (UNDISCH_TAC `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) = I`);;
1603 e (MESON_TAC[]);;
1604 e (POP_ASSUM MP_TAC);;
1605 e (PURE_REWRITE_TAC [o_THM]);;
1606 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1607 e (SUBGOAL_THEN `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) y:real^3 = I y` ASSUME_TAC);;
1608 e (UNDISCH_TAC `((g:((real^3->bool))->(real^3))o(h:(real^3) -> (real^3->bool))) = I`);;
1609 e (MESON_TAC[]);;
1610 e (POP_ASSUM MP_TAC);;
1611 e (PURE_REWRITE_TAC [o_THM]);;
1612 e (REPEAT STRIP_TAC);;
1613 e (SUBGOAL_THEN `I (y:real^3) = I x` ASSUME_TAC);;
1614 e (POP_ASSUM MP_TAC);;
1615 e (POP_ASSUM MP_TAC);;
1616 e (MESON_TAC[]);;
1617 e (POP_ASSUM MP_TAC);;
1618 e (SIMP_TAC[I_THM]);;
1619 e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3) -> (real^3->bool)) (V:real^3->bool)) = CARD V ` ASSUME_TAC);;
1620 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
1621 e (POP_ASSUM MP_TAC);;
1622 e (MESON_TAC [CARD_IMAGE_INJ]);;
1623 e (POP_ASSUM MP_TAC);;
1624 e (ASM_REWRITE_TAC[]);;
1625 e (ARITH_TAC);;
1626
1627 let CARD_1 = top_thm();;
1628
1629 (*---------------------------------------------------------------------------*)
1630
1631 (*Proof CARD {f|f facet_of V} = CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) *)
1632
1633 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} /\
1634 (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`;;
1635 e (REPEAT GEN_TAC);;
1636 e (STRIP_TAC);;
1637 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);;
1638 e (ASM_MESON_TAC [CZZHBLI_1]);;
1639 e (POP_ASSUM MP_TAC);;
1640 e (STRIP_TAC);;
1641 e (MP_TAC (ISPECL [`(h:(real^3) -> (real^3->bool))`;`V:real^3->bool`]FINITE_IMAGE));;
1642 e (ASM_REWRITE_TAC[]);;
1643
1644 let FINITE_FACE_SET = top_thm();;
1645
1646 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} /\
1647 (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 `;;
1648 e (REPEAT GEN_TAC);;
1649 e (STRIP_TAC);;
1650 e (SUBGOAL_THEN `interior_point (vec 0) (P:real^3 -> bool)` ASSUME_TAC);;
1651 e (ASM_MESON_TAC [th51]);;
1652 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);;
1653 e (ASM_MESON_TAC [AMHFNXP]);;
1654 e (POP_ASSUM MP_TAC);;
1655 e (STRIP_TAC);;
1656 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);;
1657 e (REPEAT GEN_TAC);;
1658 e (STRIP_TAC);;
1659
1660 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);;
1661 e (UNDISCH_TAC `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) = I`);;
1662 e (MESON_TAC[]);;
1663 e (POP_ASSUM MP_TAC);;
1664 e (PURE_REWRITE_TAC [o_THM]);;
1665 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1666 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);;
1667 e (UNDISCH_TAC `((g:(real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3->bool))) = I`);;
1668 e (MESON_TAC[]);;
1669 e (POP_ASSUM MP_TAC);;
1670 e (PURE_REWRITE_TAC [o_THM]);;
1671 e (REPEAT STRIP_TAC);;
1672 e (SUBGOAL_THEN `I (y:real^3->bool) = I x` ASSUME_TAC);;
1673 e (POP_ASSUM MP_TAC);;
1674 e (POP_ASSUM MP_TAC);;
1675 e (MESON_TAC[]);;
1676 e (POP_ASSUM MP_TAC);;
1677 e (SIMP_TAC[I_THM]);;
1678 e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3->bool) -> (real^3->bool)) (F':(real^3->bool)->bool)) = CARD F' ` ASSUME_TAC);;
1679 e (SUBGOAL_THEN `FINITE (F':(real^3->bool) -> bool)` ASSUME_TAC);;
1680 e (ASM_MESON_TAC [FINITE_FACE_SET]);;
1681 e (POP_ASSUM MP_TAC);;
1682 e (POP_ASSUM MP_TAC);;
1683 e (MESON_TAC [CARD_IMAGE_INJ]);;
1684 e (POP_ASSUM MP_TAC);;
1685 e (ASM_REWRITE_TAC[]);;
1686 e (ARITH_TAC);;
1687
1688 let CARD_2 = top_thm();;
1689
1690
1691 (*----------------------------------------------------------------------------*)
1692
1693 (*Proof CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) =
1694    CARD (face_set_of_fan (fan_of_polyhedron V))  *)
1695
1696 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} /\
1697 (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))
1698 ==> FINITE WF`;;
1699
1700 e (REPEAT GEN_TAC);;
1701 e (STRIP_TAC);;
1702 e (SUBGOAL_THEN `FINITE (F':(real^3->bool)->bool)` ASSUME_TAC);;
1703 e (ASM_MESON_TAC [FINITE_FACE_SET]);;
1704 e (SUBGOAL_THEN `interior_point (vec 0) (P:real^3 -> bool)` ASSUME_TAC);;
1705 e (ASM_MESON_TAC [th51]);;
1706
1707 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);;
1708 e (ASM_MESON_TAC [AMHFNXP]);;
1709 e (POP_ASSUM MP_TAC);;
1710 e (STRIP_TAC);;
1711 e (MP_TAC (ISPECL [`(h:(real^3->bool) -> (real^3->bool))`;`F':(real^3->bool)->bool`]FINITE_IMAGE));;
1712 e (ASM_REWRITE_TAC[]);;
1713
1714 let FINITE_TOPO_SET = top_thm();;
1715
1716
1717 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} /\
1718 (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`;;
1719 e (REPEAT GEN_TAC);;
1720 e (STRIP_TAC);;
1721 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3 -> bool))` ASSUME_TAC);;
1722 e (ASM_MESON_TAC [th51]);;
1723 e (SUBGOAL_THEN ` FANO (fan_of_polyhedron (P:real^3 -> bool))` ASSUME_TAC);;
1724 e (ASM_MESON_TAC [JLIGZGS]);;
1725 e (SUBGOAL_THEN `(conforming (fan_of_polyhedron (P:real^3 -> bool)))` ASSUME_TAC);;
1726 e (ASM_MESON_TAC [th53]);;
1727 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);;
1728 e (REPEAT (POP_ASSUM MP_TAC));;
1729 e (PURE_REWRITE_TAC [fan_of_polyhedron]);;
1730 e (REPEAT STRIP_TAC);;
1731 e (ASM_MESON_TAC [UVPFEEP_1]);;
1732
1733 e (POP_ASSUM MP_TAC);;
1734 e (STRIP_TAC);;
1735 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);;
1736 e (REPEAT GEN_TAC);;
1737 e (STRIP_TAC);;
1738
1739 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);;
1740 e (UNDISCH_TAC `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) = I`);;
1741 e (MESON_TAC[]);;
1742 e (POP_ASSUM MP_TAC);;
1743 e (PURE_REWRITE_TAC [o_THM]);;
1744 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1745 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);;
1746 e (UNDISCH_TAC `((g:(real^3#real^3->bool) -> (real^3->bool))o(h:(real^3->bool) -> (real^3#real^3->bool))) = I`);;
1747 e (MESON_TAC[]);;
1748 e (POP_ASSUM MP_TAC);;
1749 e (PURE_REWRITE_TAC [o_THM]);;
1750 e (REPEAT STRIP_TAC);;
1751 e (SUBGOAL_THEN `I (y:real^3->bool) = I x` ASSUME_TAC);;
1752 e (POP_ASSUM MP_TAC);;
1753 e (POP_ASSUM MP_TAC);;
1754 e (MESON_TAC[]);;
1755 e (POP_ASSUM MP_TAC);;
1756 e (SIMP_TAC[I_THM]);;
1757 e (SUBGOAL_THEN `CARD (IMAGE (h:(real^3->bool) -> (real^3#real^3->bool)) (WF':(real^3->bool)->bool)) = CARD WF' ` ASSUME_TAC);;
1758 e (SUBGOAL_THEN `FINITE (WF':(real^3->bool) -> bool)` ASSUME_TAC);;
1759 e (ASM_MESON_TAC [FINITE_TOPO_SET]);;
1760 e (POP_ASSUM MP_TAC);;
1761 e (POP_ASSUM MP_TAC);;
1762 e (MESON_TAC [CARD_IMAGE_INJ]);;
1763 e (POP_ASSUM MP_TAC);;
1764 e (ASM_REWRITE_TAC[]);;
1765 e (ARITH_TAC);;
1766
1767 let CARD_3 = top_thm();;
1768
1769
1770 (*----------------------------------------------------------------------------*)
1771
1772 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} /\
1773 (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`;;
1774 e (REPEAT GEN_TAC);;
1775 e (STRIP_TAC);;
1776 e (SUBGOAL_THEN `(CARD (V:real^3 -> bool)) = (CARD (F':(real^3->bool)->bool))` ASSUME_TAC);;
1777 e (ASM_MESON_TAC [CARD_1]);;
1778 e (SUBGOAL_THEN `(CARD (F':(real^3->bool)->bool)) = CARD (WF':(real^3->bool)->bool)` ASSUME_TAC);;
1779 e (ASM_MESON_TAC [CARD_2]);;
1780 e (SUBGOAL_THEN `CARD (WF':(real^3->bool)->bool) =  CARD (F_T:(real^3#real^3->bool)->bool) ` ASSUME_TAC);;
1781 e (ASM_MESON_TAC [CARD_3]);;
1782 e (ASM_MESON_TAC[]);;
1783
1784 let CARD_4 = top_thm();;
1785
1786
1787 (*---------------------------------------------------------------------------*)
1788 g `!(V:real^3 -> bool) (P:real^3 -> bool).(FINITE V)  /\ packing V /\ (weakly_saturated V r r') /\ (V SUBSET ball_annulus) /\
1789 ~(lmfun_ineq_center V) /\ P = INTERS {half_spaces g_fun u| (u IN V) /\ (~(vec 0 = u))} /\ (polyhedron P) /\ (bounded P) ==>
1790 nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))
1791  = CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))`;;
1792 e (REPEAT GEN_TAC);;
1793 e (STRIP_TAC);;
1794 e (MP_TAC (ISPECL [`(dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))`]card_partition_formula));;
1795 e (DISCH_THEN (LABEL_TAC "F1"));;
1796 e (REMOVE_THEN "F1" (MP_TAC o SPEC `face_map (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))`));;
1797 e (REWRITE_TAC [face_map_and_darts]);;
1798 e (STRIP_TAC);;
1799 e (REWRITE_TAC [fan_of_polyhedron;face_set_of_fan]);;
1800 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
1801 e (REWRITE_TAC [face_set]);;
1802 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
1803
1804 let CARD_5 = top_thm();;
1805
1806 (*--------------------------------------------------------------------------*)
1807
1808 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} /\
1809 (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))   ==>
1810 nsum (face_set_of_fan (fan_of_polyhedron P)) (\u:real^3#real^3->bool. (CARD u))
1811  <= (6*(CARD V)-12)`;;
1812 e (REPEAT GEN_TAC);;
1813 e (STRIP_TAC);;
1814
1815 (*SUBGOAL 1*)
1816 e (SUBGOAL_THEN `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3 -> bool))) (\u:real^3#real^3->bool. (CARD u))
1817  = CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))` ASSUME_TAC);;
1818 e (ASM_MESON_TAC[CARD_5]);;
1819
1820 (*SUBGOAL 2*)
1821 e (SUBGOAL_THEN `CARD (V:real^3 -> bool) =  CARD (F_T:(real^3#real^3->bool)->bool)` ASSUME_TAC);;
1822 e (ASM_MESON_TAC [CARD_4]);;
1823 (*SUBGOAL 3*)
1824 e (SUBGOAL_THEN `conforming (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
1825 e (ASM_MESON_TAC [th53]);;
1826 e (SUBGOAL_THEN `CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3 -> bool)))) <=
1827    (6*(CARD (face_set_of_fan (fan_of_polyhedron P)))-12)` ASSUME_TAC);;
1828 e (ASM_MESON_TAC[th5]);;
1829 e (UNDISCH_TAC `CARD (V:real^3->bool) = CARD (F_T:(real^3#real^3->bool)->bool)`);;
1830 e (STRIP_TAC);;
1831 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1832 e (UNDISCH_TAC `F_T = face_set_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
1833 e (STRIP_TAC);;
1834 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1835 e (UNDISCH_TAC `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u) =
1836       CARD (dart (hypermap_of_fan (fan_of_polyhedron P)))`);;
1837 e (STRIP_TAC);;
1838 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1839 e (ASM_REWRITE_TAC[]);;
1840
1841 let th6 = top_thm();;
1842
1843 (*--------------------------------------------------------------------------*)
1844 let th7_concl = `!V X.FINITE V /\ packing V /\
1845     V SUBSET ball_annulus /\
1846     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
1847     (polyhedron P) /\ (bounded P) /\
1848    X = topological_component_yfan (vec 0,fan_of_polyhedron P)
1849
1850 ==> &4 * pi = sum X (\v. sol (vec 0) (v))`;;
1851
1852 let th7 = new_axiom th7_concl;;
1853
1854
1855 (*----------------------------------------------------------------------------*)
1856 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)).
1857     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
1858     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
1859     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
1860     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
1861     F = {l | l facet_of P} /\
1862     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
1863     f1 o f2 = I /\ f2 o f1 = I /\
1864     IMAGE f1 V = X /\
1865     f3 o f4 = I /\ f3 o f4 = I /\
1866     IMAGE f3 V = F
1867   ==>
1868   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))))`;;
1869
1870 let th8 = new_axiom th8_concl;;
1871
1872 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)}`;;
1873 e (REPEAT GEN_TAC);;
1874 e (STRIP_TAC);;
1875 e (REWRITE_TAC [half_spaces]);;
1876 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
1877 e (STRIP_TAC);;
1878 e (MP_TAC (ISPECL [`(\u:real^3. {p:real^3 | u dot p <= g_fun u})`;`V:real^3->bool`] FINITE_IMAGE));;
1879 e (ASM_REWRITE_TAC [IMAGE]);;
1880 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);;
1881 e (REWRITE_TAC[EXTENSION]);;
1882 e (GEN_TAC);;
1883 e (EQ_TAC);;
1884 e (REWRITE_TAC [IN_ELIM_THM]);;
1885 e (STRIP_TAC);;
1886 e (EXISTS_TAC `u:real^3`);;
1887 e (ASM_REWRITE_TAC[]);;
1888 e (GEN_TAC);;
1889 e (REWRITE_TAC [IN_ELIM_THM]);;
1890 e (REWRITE_TAC [IN_ELIM_THM]);;
1891 e (STRIP_TAC);;
1892 e (EXISTS_TAC `x':real^3`);;
1893 e (SUBGOAL_THEN `~(vec 0 = x':real^3)` ASSUME_TAC);;
1894 e (ASM_MESON_TAC [th54]);;
1895 e (ASM_REWRITE_TAC[]);;
1896 e (REWRITE_TAC [EXTENSION]);;
1897 e (REWRITE_TAC [IN_ELIM_THM]);;
1898 e (ASM_MESON_TAC[]);;
1899 e (ASM_REWRITE_TAC[]);;
1900
1901 let FINITE_HALF_SPACES = top_thm();;
1902
1903 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)).
1904     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
1905     ~(lmfun_ineq_center V) /\ (weakly_saturated V r r') /\
1906     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
1907     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
1908     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
1909     F = {l | l facet_of P} /\
1910     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
1911     f1 o f2 = I /\ f2 o f1 = I /\
1912     IMAGE f1 V = X /\
1913     f3 o f4 = I /\ f3 o f4 = I /\
1914     IMAGE f3 V = F
1915 ==> (!u. u IN V ==> f3 u = {p | p dot u = g_fun u} INTER P)`;;
1916
1917
1918 e (REPEAT GEN_TAC);;
1919 e (STRIP_TAC);;
1920 e (MP_TAC (ISPECL [`P:real^3->bool`] POLYHEDRON_INTER_AFFINE_MINIMAL));;
1921 e (UNDISCH_TAC `polyhedron (P:real^3->bool)`);;
1922 e (STRIP_TAC);;
1923 e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
1924 e (STRIP_TAC);;
1925 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));;
1926
1927 e (DISCH_THEN (LABEL_TAC "F1"));;
1928
1929
1930 e (REMOVE_THEN "F1" (MP_TAC o SPECL `{half_spaces g_fun u | (u:real^3) IN (V:real^3->bool) /\ ~(vec 0 = u)}`));;
1931
1932
1933 e (SUBGOAL_THEN `FINITE {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}` ASSUME_TAC);;
1934 e (ASM_MESON_TAC [FINITE_HALF_SPACES]);;
1935
1936 e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
1937 e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`);;
1938 e (STRIP_TAC);;
1939 e (FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th]));;
1940 search [`affine hull P INTER P`];;
1941 ARITH_RULE `affine hull P INTER P`;;
1942 e (ASM_REWRITE_TAC[INTER]);;
1943
1944 search [`FINITE P`];;
1945
1946
1947 type_of `{half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`;;
1948 type_of `g_fun(f4:((real^3->bool))->(real^3))`;;
1949 type_of `g_fun`;;
1950
1951 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)).
1952     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
1953     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
1954     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
1955     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
1956     F = {l | l facet_of P} /\
1957     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
1958     f1 o f2 = I /\ f2 o f1 = I /\
1959     IMAGE f1 V = X /\
1960     f3 o f4 = I /\ f3 o f4 = I /\
1961     IMAGE f3 V = F
1962   ==>
1963   (!v:real^3. v IN V ==> reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})) <=  sol (vec 0) (f1(v)))`;;
1964
1965
1966 OPEN_RCONE_GT;;
1967 e (REPEAT GEN_TAC);;
1968 e (STRIP_TAC);;
1969 e (GEN_TAC);;
1970 e (STRIP_TAC);;
1971 e (SUBGOAL_THEN `(?r:real. r > &0 /\ ball (vec 0,r) SUBSET (P:real^3->bool))` ASSUME_TAC);;
1972 e (EXISTS_TAC `r'':real`);;
1973 e (ASM_REWRITE_TAC[]);;
1974 e (MP_TAC (ISPECL [`(f3:(real^3) -> (real^3->bool))`;`V:real^3->bool`;`v:real^3`] FUN_IN_IMAGE));;
1975 e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
1976 e (STRIP_TAC);;
1977 e (MP_TAC (ISPECL [`(f1:(real^3) -> (real^3->bool))`;`V:real^3->bool`;`v:real^3`] FUN_IN_IMAGE));;
1978 e (ONCE_ASM_REWRITE_TAC[IN]);;
1979 e (ONCE_ASM_REWRITE_TAC[IN]);;
1980 e (ONCE_ASM_REWRITE_TAC[IN]);;
1981 e (ONCE_ASM_REWRITE_TAC[IN]);;
1982 e (STRIP_TAC);;
1983
1984
1985 FACET_OF_POLYHEDRON_EXPLICIT;;
1986
1987 e (MP_TAC (ISPECL [`P:real^3->bool`;`(f3:(real^3) -> (real^3->bool))(v:real^3)`]
1988 FACET_OF_POLYHEDRON));;
1989 e (ASM_REWRITE_TAC[]);;
1990 e (MP_TAC (ISPECL [`P:real^3->bool`;`(f3:(real^3) -> (real^3->bool))(v:real^3)`;
1991 `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));;
1992 e (ASM_REWRITE_TAC []);;
1993 e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u | u IN (V:real^3->bool) /\ ~(vec 0 = u)}`);;
1994 e (STRIP_TAC);;
1995 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]));;
1996 e (STRIP_TAC);;
1997 e (REWRITE_TAC [reg]);;
1998
1999
2000
2001 FACET_OF_POLYHEDRON_EXPLICIT;;
2002 e (DISCH_THEN (CHOOSE_TAC [`v:real^3`]));;
2003 e (POP_ASSUM (X_CHOOSE_TAC `g_fun (u:real^3)`));;
2004 help "X_CHOOSE_TAC";;
2005
2006 search [`rcone`];;
2007
2008 e (SUBGOAL_THEN `(f3:(real^3) -> (real^3->bool))(v:real^3) IN F'` ASSUME_TAC);;
2009
2010 search [`f (v) IN V`];;
2011
2012 FUN_IN_IMAGE;;
2013 e (GEN_TAC);;
2014
2015
2016 search [`x IN V /\ f x`];;
2017 type_of `extreme_point_of`;;
2018 search [`f o g = I`];;
2019
2020
2021 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)).
2022     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
2023     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2024     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2025     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2026     F = {l | l facet_of P} /\
2027     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
2028     f1 o f2 = I /\ f2 o f1 = I /\
2029     IMAGE f1 V = X /\
2030     f3 o f4 = I /\ f4 o f3 = I /\
2031     IMAGE f3 V = F
2032   ==>
2033   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))))`;;
2034
2035 e (REPEAT GEN_TAC);;
2036 e (STRIP_TAC);;
2037
2038 GOTCJAH;;
2039 facet_of;;
2040
2041 (*----------------------------------------------------------------------------*)
2042
2043 g `!a b c e f:real. a = b + c /\ b = e - f ==> a = e - f + c`;;
2044 e (REPEAT GEN_TAC);;
2045 e (STRIP_TAC);;
2046 e (ASM_REWRITE_TAC[]);;
2047
2048 let th91 = top_thm();;
2049
2050 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)).
2051     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
2052     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2053     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2054     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2055     F = {l | l facet_of P} /\
2056     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
2057     f1 o f2 = I /\ f2 o f1 = I /\
2058     IMAGE f1 V = X /\
2059     f3 o f4 = I /\ f3 o f4 = I /\
2060     IMAGE f3 V = F
2061     ==> 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))))`;;
2062
2063 let th92 =new_axiom th92_T;;
2064
2065 g `!(P:real^3->bool) v b. (polyhedron P) /\ (bounded P) ==> (!f.(f facet_of P) /\ f = { p | p dot v = b } INTER P ==>
2066    (CARD {u | u extreme_point_of f}) = (CARD (edges f)))`;;
2067 e (REPEAT GEN_TAC);;
2068 e (STRIP_TAC);;
2069 e (GEN_TAC);;
2070 e (STRIP_TAC);;
2071 e (REWRITE_TAC [edges]);;
2072 dart1_of_fan;;
2073 e (REWRITE_TAC [
2074
2075
2076
2077 g `!(V:real^3->bool) X P F F_T.
2078     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
2079     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2080     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2081     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2082     F = {l | l facet_of P} /\
2083     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
2084     ~(lmfun_ineq_center V) /\
2085     (weakly_saturated V r r')
2086     ==> 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)))`;;
2087
2088
2089 e (REPEAT GEN_TAC);;
2090 e (STRIP_TAC);;
2091 e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
2092 e (ASM_MESON_TAC [th52]);;
2093 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3->bool))` ASSUME_TAC);;
2094 e (ASM_MESON_TAC [th51]);;
2095 e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
2096 e (ASM_MESON_TAC [JLIGZGS]);;
2097 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);;
2098 e (POP_ASSUM MP_TAC);;
2099 e (POP_ASSUM MP_TAC);;
2100 e (POP_ASSUM MP_TAC);;
2101 e (REWRITE_TAC [fan_of_polyhedron]);;
2102 e (MESON_TAC [FULLY_SURROUNDED_IMP_DART]);;
2103 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);;
2104 e (ASM_MESON_TAC[DART_OF_HYPERMAP_FAN]);;
2105 e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;
2106 e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;
2107
2108
2109 e (REWRITE_TAC [fan_of_polyhedron;dart1_of_fan]);;
2110 e (SUBGOAL_THEN `nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u) =
2111              CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` ASSUME_TAC);;
2112 e (ASM_MESON_TAC [CARD_5]);;
2113
2114
2115
2116 CARD_5;;
2117 e (REWRITE_TAC [IN_ELIM_THM]);;
2118
2119 e (REWRITE_TAC [dart]);;
2120 KREIN_MILMAN_POLYTOPE;;
2121 verticesface_of;;
2122 EXTREME_POINT_OF_FACE;;
2123 DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET;;
2124 search [`vertices`];;
2125
2126 card_partition_formula;;
2127 CARD_5;;
2128 th8;;
2129 edge_map_and_darts;;
2130
2131 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`,
2132   REPEAT GEN_TAC THEN
2133   DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "F1") (LABEL_TAC "F2")) THEN
2134   USE_THEN "F1" (MP_TAC o MATCH_MP lemma_edge_representation) THEN
2135   DISCH_THEN (X_CHOOSE_THEN `y:A` (SUBST_ALL_TAC o CONJUNCT2)) THEN
2136   USE_THEN "F2" (fun th -> REWRITE_TAC [MATCH_MP lemma_edge_identity th]));;
2137
2138 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`,
2139   REPEAT GEN_TAC THEN
2140   DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "F1") (LABEL_TAC "F2")) THEN
2141   USE_THEN "F1" (MP_TAC o MATCH_MP lemma_face_representation) THEN
2142   DISCH_THEN (X_CHOOSE_THEN `y:A` (SUBST_ALL_TAC o CONJUNCT2)) THEN
2143   USE_THEN "F2" (fun th -> REWRITE_TAC [MATCH_MP lemma_face_identity th]));;
2144
2145 g `!(V:real^3->bool) X P F F_T.
2146     FINITE V /\ packing V /\ weakly_saturated V r r' /\ V SUBSET ball_annulus /\
2147     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2148     ~(lmfun_ineq_center V) /\
2149     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2150     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2151     F = {l | l facet_of P} /\
2152     F_T = face_set_of_fan (fan_of_polyhedron P )
2153 ==> nsum F (\v.((CARD (edges v)))) = (CARD (dart (hypermap_of_fan(fan_of_polyhedron P))))`;;
2154
2155 e (REPEAT GEN_TAC);;
2156 e (STRIP_TAC);;
2157 e (MP_TAC (ISPECL [`hypermap_of_fan(fan_of_polyhedron (P:real^3->bool))`]DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET));;
2158 e (STRIP_TAC);;
2159 e (SUBGOAL_THEN `CARD (dart (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool)))) =
2160      CARD (UNIONS (face_set (hypermap_of_fan (fan_of_polyhedron P))))` ASSUME_TAC);;
2161 e (ASM_MESON_TAC[]);;
2162 e (SUBGOAL_THEN `FINITE (face_set (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` ASSUME_TAC);;
2163 e (MP_TAC (ISPECL [`hypermap_of_fan(fan_of_polyhedron (P:real^3->bool))`]FINITE_HYPERMAP_ORBITS));;
2164 e (SIMP_TAC[]);;
2165 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);;
2166 e (REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM face;FACE_FINITE]);;
2167 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);;
2168 e (REPEAT GEN_TAC);;
2169 e (DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "G1") (CONJUNCTS_THEN2 (LABEL_TAC "G2") (MP_TAC))));;
2170 e (ONCE_REWRITE_TAC [GSYM CONTRAPOS_THM]);;
2171 e (REWRITE_TAC[]);;
2172 e (REWRITE_TAC [GSYM MEMBER_NOT_EMPTY;IN_INTER]);;
2173 e (STRIP_TAC);;
2174 e (POP_ASSUM (fun th -> USE_THEN "G2" (fun th1 -> REWRITE_TAC [MATCH_MP lemma_face_from_dart (CONJ th1 th)])));;
2175 e (POP_ASSUM (fun th -> USE_THEN "G1" (fun th1 -> REWRITE_TAC [MATCH_MP lemma_face_from_dart (CONJ th1 th)])));;
2176 e (MP_TAC (MATCH_MP card_partition_formula (ISPEC `( (hypermap_of_fan (fan_of_polyhedron (P:real^3->bool))))` face_map_and_darts)));;
2177 e (REWRITE_TAC [GSYM face_set]);;
2178 CARD_5;;
2179 e (STRIP_TAC);;
2180
2181 e (POP_ASSUM MP_TAC);;
2182 e (ASM_REWRITE_TAC[]);;
2183
2184 g `!(V:real^3->bool) X P F F_T.
2185     FINITE V /\ packing V /\ weakly_saturated V r r' /\ V SUBSET ball_annulus /\
2186     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2187     ~(lmfun_ineq_center V) /\
2188     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2189     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2190     F = {l | l facet_of P} /\
2191     F_T = face_set_of_fan (fan_of_polyhedron P )
2192 ==> nsum F (\v.((CARD (edges v)))) = (CARD (dart (hypermap_of_fan(fan_of_polyhedron P))))`;;
2193
2194 e (REPEAT GEN_TAC);;
2195 e (STRIP_TAC);;
2196 e (REWRITE_TAC [edges]);;
2197 e (SUBGOAL_THEN `fully_surrounded (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
2198 e (ASM_MESON_TAC [th52]);;
2199 e (SUBGOAL_THEN `(interior_point (vec 0) (P:real^3->bool))` ASSUME_TAC);;
2200 e (ASM_MESON_TAC [th51]);;
2201 e (SUBGOAL_THEN `FANO (fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
2202 e (ASM_MESON_TAC [JLIGZGS]);;
2203 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);;
2204 e (POP_ASSUM MP_TAC);;
2205 e (POP_ASSUM MP_TAC);;
2206 e (POP_ASSUM MP_TAC);;
2207 e (REWRITE_TAC [fan_of_polyhedron]);;
2208 e (MESON_TAC [FULLY_SURROUNDED_IMP_DART]);;
2209 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);;
2210 e (ASM_MESON_TAC[DART_OF_HYPERMAP_FAN]);;
2211 e (POP_ASSUM (fun th -> REWRITE_TAC [th]));;
2212 e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
2213 e (UNDISCH_TAC `F' = {l | l facet_of (P:real^3->bool)}`);;
2214 e (DISCH_TAC);;
2215 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
2216 e (MP_TAC (ISPECL [`(dart1_of_fan ((fan_of_polyhedron (P:real^3->bool))))`]card_partition_formula));;
2217 e (DISCH_THEN (LABEL_TAC "F1"));;
2218 e (REMOVE_THEN "F1" (MP_TAC o SPEC `e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool))`));;
2219 e (SUBGOAL_THEN `FAN(vec 0,fan_of_polyhedron (P:real^3->bool))` ASSUME_TAC);;
2220 e (UNDISCH_TAC `FANO (fan_of_polyhedron  (P:real^3->bool))`);;
2221 e (REWRITE_TAC [fan_of_polyhedron]);;
2222 e (MESON_TAC [FANO_OF_FAN]);;
2223 e (SUBGOAL_THEN `FINITE (dart_of_fan (fan_of_polyhedron (P:real^3->bool)))` ASSUME_TAC);;
2224 e (POP_ASSUM MP_TAC THEN REWRITE_TAC [fan_of_polyhedron]);;
2225 e (REWRITE_TAC [FINITE_DART_OF_FAN]);;
2226 e (SUBGOAL_THEN `FINITE (dart1_of_fan (fan_of_polyhedron (P:real^3->bool)))` ASSUME_TAC);;
2227 e (ASM_MESON_TAC[]);;
2228 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
2229 e (SUBGOAL_THEN `e_fan_pair_ext (fan_of_polyhedron (P:real^3->bool)) permutes dart1_of_fan (fan_of_polyhedron P)` ASSUME_TAC);;
2230 e (REWRITE_TAC [fan_of_polyhedron;E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
2231 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
2232 e (REWRITE_TAC [set_of_orbits;fan_of_polyhedron;e_fan_pair_ext]);;
2233
2234 e (STRIP_TAC);;
2235 e (POP_ASSUM (fun th -> REWRITE_TAC[th]));;
2236 e (UNDISCH_TAC `dart_of_fan (fan_of_polyhedron (P:real^3->bool)) = dart1_of_fan (fan_of_polyhedron (P:real^3->bool))`);;
2237 E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN;;
2238 e (REWRITE_TAC [IN_ELIM_THM]);;
2239 e (REWRITE_TAC [fan_of_polyhedron;dart1_of_fan]);;
2240 e (REWRITE_TAC [edge_of]);;
2241
2242 search [`convex hull {v', w'} face_of P`];;
2243 e (REWRITE_TAC [IN_ELIM_THM]);;
2244
2245 e (REWRITE_TAC weakly_saturated V r r'
2246 e (REWRITE_TAC [dart]);;
2247
2248
2249 search [`CARD (UNIONS s)`];;
2250
2251
2252 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)).
2253     FINITE V /\ packing V /\ V SUBSET ball_annulus /\
2254     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2255     (polyhedron P) /\ (bounded P) /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2256     X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2257     F = {l | l facet_of P} /\
2258     F_T = face_set_of_fan (fan_of_polyhedron P ) /\
2259     f1 o f2 = I /\ f2 o f1 = I /\
2260     IMAGE f1 V = X /\
2261     f3 o f4 = I /\ f3 o f4 = I /\
2262     IMAGE f3 V = F
2263     /\ (!v. v IN V ==>  #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of f3(v)})) +  #0.506 * lmfun (hl [vec 0; v])
2264        <= reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})))
2265 ==>
2266
2267 #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)})))`;;
2268
2269 e (REPEAT GEN_TAC);;
2270 e (STRIP_TAC);;
2271 e (POP_ASSUM (LABEL_TAC "F1"));;
2272 e (SUBGOAL_THEN `!v:real^3. v IN (V:real^3->bool)
2273           ==> (\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);;
2274 e (GEN_TAC);;
2275 e (STRIP_TAC);;
2276 e (REMOVE_THEN "F1" (MP_TAC o SPEC `v:real^3`));;
2277 e (ASM_MESON_TAC[]);;
2278 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);;
2279 e (POP_ASSUM MP_TAC);;
2280 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
2281 e (MESON_TAC [SUM_LE]);;
2282 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);;
2283 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
2284 e (REWRITE_TAC [SUM_ADD]);;
2285 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)}))) =
2286 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);;
2287 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
2288 e (REWRITE_TAC [SUM_SUB]);;
2289 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)})) +
2290        #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)})))
2291    + sum V (\v. #0.506 * lmfun (hl [vec 0; v]))` ASSUME_TAC);;
2292 e (POP_ASSUM MP_TAC);;
2293 e (POP_ASSUM MP_TAC);;
2294 e (MESON_TAC[th91]);;
2295 e (SUBGOAL_THEN  `sum (V:real^3->bool) (\v. #0.591) =  #0.591 * &(CARD V) ` ASSUME_TAC);;
2296 e (ONCE_REWRITE_TAC [ARITH_RULE `#0.591 = #0.591 * &1`]);;
2297 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.591 * &1)  = #0.591 * (sum V (\v. &1))` ASSUME_TAC);;
2298 e (REWRITE_TAC[SUM_LMUL]);;
2299 e (ASM_REWRITE_TAC[]);;
2300 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
2301 e (SIMP_TAC[GSYM CARD_EQ_SUM]);;
2302 e (STRIP_TAC);;
2303 e (REAL_ARITH_TAC);;
2304 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v. #0.506 * lmfun (hl [vec 0; v])) =
2305 #0.506 * sum V (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
2306 e (SIMP_TAC [SUM_LMUL]);;
2307 e (SUBGOAL_THEN `sum (V:real^3->bool)
2308       (\v. #0.0331 *
2309            &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) = #0.0331 * sum (V)
2310       (\v.
2311            &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))  ` ASSUME_TAC);;
2312
2313 e (SIMP_TAC [SUM_LMUL]);;
2314 e (SUBGOAL_THEN `sum (V:real^3->bool) (\v.
2315            &(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);;
2316 e (ASM_MESON_TAC [th92]);;
2317 e (UNDISCH_TAC `sum (V:real^3->bool)
2318       (\v. #0.0331 *
2319            &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) =
2320       #0.0331 *
2321       sum V
2322       (\v. &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))`);;
2323 e (POP_ASSUM(fun th ->REWRITE_TAC[th]  ));;
2324 e (STRIP_TAC);;
2325 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
2326 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
2327 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
2328 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]  ));;
2329 e (ASM_REWRITE_TAC[]);;
2330
2331 let th9 = top_thm();;
2332
2333
2334 g `!(V:real^3->bool) (P:real^3->bool).
2335 FINITE V /\ packing V /\ V SUBSET ball_annulus /\
2336     weakly_saturated V r r' /\
2337      ~lmfun_ineq_center V /\
2338     P = INTERS {half_spaces g_fun u | u IN V /\ ~(vec 0 = u)} /\
2339     (polyhedron P) /\ (bounded P)
2340     ==> #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])))`;;
2341
2342 e (REPEAT GEN_TAC);;
2343 e (STRIP_TAC);;
2344 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);;
2345 e (ASM_MESON_TAC [th6]);;
2346 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);;
2347 e (POP_ASSUM MP_TAC);;
2348 e (REWRITE_TAC [REAL_OF_NUM_LE]);;
2349 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);;
2350 e (POP_ASSUM MP_TAC);;
2351 e (MP_TAC (ARITH_RULE `&0 <= #0.0331`));;
2352 e (MESON_TAC [REAL_LE_LMUL]);;
2353 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);;
2354 e (POP_ASSUM MP_TAC);;
2355 e (REWRITE_TAC [REAL_LE_NEG]);;
2356 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);;
2357 e (POP_ASSUM MP_TAC);;
2358 e (REWRITE_TAC [REAL_LE_LADD_IMP]);;
2359 e (POP_ASSUM MP_TAC);;
2360 e (PURE_REWRITE_TAC [GSYM real_sub]);;
2361 e (STRIP_TAC);;
2362 e (UNDISCH_TAC `~lmfun_ineq_center (V:real^3->bool)`);;
2363 e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
2364 e (STRIP_TAC);;
2365 e (SUBGOAL_THEN `&12 < sum (V:real^3 -> bool) (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
2366 e (POP_ASSUM MP_TAC);;
2367 e (REWRITE_TAC [REAL_NOT_LE]);;
2368 e (SUBGOAL_THEN `#0.506 * &12 < #0.506 * sum (V:real^3->bool) (\v. lmfun (hl [vec 0; v]))` ASSUME_TAC);;
2369 e (POP_ASSUM MP_TAC);;
2370 e (MP_TAC (ARITH_RULE `&0 < #0.506`));;
2371 e (MESON_TAC [REAL_LT_LMUL]);;
2372 e (POP_ASSUM MP_TAC);;
2373 e (UNDISCH_TAC `#0.591 * &(CARD (V:real^3->bool)) - #0.0331 * &(6 * CARD V - 12) <=
2374       #0.591 * &(CARD V) -
2375       #0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u))`);;
2376 e (ABBREV_TAC `a:real = #0.591 * &(CARD (V:real^3->bool)) - #0.0331 * &(6 * CARD V - 12)`);;
2377 e (ABBREV_TAC `b:real = #0.591 * &(CARD (V:real^3->bool)) -
2378  #0.0331 * &(nsum (face_set_of_fan (fan_of_polyhedron (P:real^3->bool))) (\u. CARD u))`);;
2379 e (MESON_TAC [REAL_LET_ADD2]);;
2380
2381 let th10 = top_thm();;
2382
2383 (*--------------------------------------------------------------------------*)
2384 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]]);;
2385
2386 let REAL_ADD2_ADD2 = prove (`!x y z:real. x + (y + z) = x + y + z`,SET_TAC[]);;
2387
2388 g `(pi < #3.15) ==> (&4 * pi - #6.4692) / #0.3924 < &16`;;
2389 e (STRIP_TAC);;
2390 e (SUBGOAL_THEN `&0 < &4` ASSUME_TAC);;
2391 e (ARITH_TAC);;
2392 e (SUBGOAL_THEN `&4*pi < &4 * #3.15` ASSUME_TAC);;
2393 e (ASM_MESON_TAC[REAL_LT_LMUL_EQ]);;
2394 e (POP_ASSUM MP_TAC);;
2395 e (PURE_REWRITE_TAC [ARITH_RULE `&4 * #3.15= #12.6`]);;
2396 e (STRIP_TAC);;
2397 e (SUBGOAL_THEN `&4*pi + (--(#6.4692)) < #12.6 + (--(#6.4692))` ASSUME_TAC);;
2398 e (ASM_REWRITE_TAC[REAL_LT_RADD]);;
2399 e (POP_ASSUM MP_TAC);;
2400 e (PURE_REWRITE_TAC [GSYM real_sub]);;
2401 e (PURE_REWRITE_TAC [ARITH_RULE `#12.6 - #6.4692 = #6.1308`]);;
2402 e (SUBGOAL_THEN `&0 < #0.3924` ASSUME_TAC);;
2403 e (ARITH_TAC);;
2404 e (STRIP_TAC);;
2405 e (SUBGOAL_THEN `(&4 * pi - #6.4692)/( #0.3924) < #6.1308 / #0.3924` ASSUME_TAC);;
2406 e (ASM_MESON_TAC[GSYM REAL_LT_DIV2_EQ]);;
2407 e (SUBGOAL_THEN `#6.1308 / #0.3924 < &16` ASSUME_TAC);;
2408 e (ARITH_TAC);;
2409 e (ASM_MESON_TAC[REAL_LT_TRANS]);;
2410
2411 let th11 = top_thm();;
2412
2413 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`;;
2414 e (GEN_TAC);;
2415 e (STRIP_TAC);;
2416 e (SUBGOAL_THEN `12 < CARD (V:real^3->bool)` ASSUME_TAC);;
2417 e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
2418 e (SUBGOAL_THEN ` 12 < 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
2419 e (SUBGOAL_THEN `6 * 12 < 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
2420 e (SUBGOAL_THEN `~(6 = 0)` ASSUME_TAC);;
2421 e (ARITH_TAC);;
2422 e (ASM_MESON_TAC[LT_LMULT]);;
2423 e (POP_ASSUM MP_TAC);;
2424 e (PURE_REWRITE_TAC [ARITH_RULE `6 * 12 = 72`]);;
2425 e (STRIP_TAC);;
2426 e (SUBGOAL_THEN ` 12 < 72 ` ASSUME_TAC);;
2427 e (ARITH_TAC);;
2428 e (ASM_MESON_TAC[LT_TRANS]);;
2429 e (SUBGOAL_THEN ` 12 <= 6 * (CARD (V:real^3->bool))` ASSUME_TAC);;
2430 e (ASM_MESON_TAC[LT_IMP_LE]);;
2431 e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))-12) = &(6 *(CARD V)) - &12` ASSUME_TAC);;
2432 e (ASM_MESON_TAC[REAL_OF_NUM_SUB]);;
2433 e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))) = &(6) * &(CARD V)` ASSUME_TAC);;
2434 e (MESON_TAC[REAL_OF_NUM_MUL]);;
2435 e (SUBGOAL_THEN `&(6*(CARD (V:real^3->bool))-12) = &(6) * &(CARD V) - &12` ASSUME_TAC);;
2436 e (ASM_MESON_TAC[]);;
2437 e (SUBGOAL_THEN `#0.591 * (&(CARD (V:real^3 -> bool))) - #0.0331 * (&(6) * &(CARD V) - &12) + #0.506 * (&12)< &4 * pi` ASSUME_TAC);;
2438 e (ASM_MESON_TAC[]);;
2439 e (SUBGOAL_THEN `#0.0331 * (&(6) * &(CARD (V:real^3->bool)) - &12) = #0.0331 * &(6) * &(CARD (V)) -  #0.0331 * &12` ASSUME_TAC);;
2440 e (MESON_TAC[REAL_SUB_LDISTRIB]);;
2441 e (POP_ASSUM MP_TAC);;
2442 e (PURE_REWRITE_TAC [ARITH_RULE `#0.0331 * &12 = #0.3972`]);;
2443 e (STRIP_TAC);;
2444 e (SUBGOAL_THEN `#0.591 * (&(CARD (V:real^3 -> bool))) - (#0.0331 * &6 * &(CARD V) - #0.3972) + #0.506 * (&12)< &4 * pi` ASSUME_TAC);;
2445 e (ASM_MESON_TAC[]);;
2446 e (POP_ASSUM MP_TAC);;
2447 e (PURE_REWRITE_TAC [ARITH_RULE `#0.506 * &12 = #6.072`]);;
2448 e (PURE_REWRITE_TAC [REAL_SUB2_SUB2 ]);;
2449 e (SUBGOAL_THEN `#0.0331 * &6 * &(CARD (V:real^3->bool)) = (#0.0331 * &6) * &(CARD V) ` ASSUME_TAC);;
2450 e (REWRITE_TAC[REAL_MUL_ASSOC]);;
2451 e (POP_ASSUM MP_TAC);;
2452 e (PURE_REWRITE_TAC [ARITH_RULE `#0.0331 * &6 = #0.1986`]);;
2453 e (STRIP_TAC);;
2454 e (ASM_REWRITE_TAC[]);;
2455 e (SUBGOAL_THEN `#0.591 * &(CARD (V:real^3->bool)) - #0.1986 * &(CARD V)
2456 = (#0.591 - #0.1986) * &(CARD V)` ASSUME_TAC);;
2457 e (MESON_TAC[REAL_SUB_RDISTRIB]);;
2458 e (POP_ASSUM MP_TAC);;
2459 e (PURE_REWRITE_TAC [ARITH_RULE `(#0.591 - #0.1986) = #0.3924`]);;
2460 e (STRIP_TAC);;
2461 e (SUBGOAL_THEN `#0.591 * &(CARD (V:real^3->bool)) - #0.1986 * &(CARD V) + #0.3972 = #0.3924 * &(CARD V) + #0.3972` ASSUME_TAC);;
2462 e (ASM_MESON_TAC[]);;
2463 e (ASM_REWRITE_TAC[]);;
2464 e (SUBGOAL_THEN `(#0.3924 * &(CARD (V:real^3->bool)) + #0.3972) + #6.072 =
2465 #0.3924 * &(CARD (V:real^3->bool)) + (#0.3972 + #6.072)` ASSUME_TAC);;
2466 e (MESON_TAC[REAL_ADD_AC]);;
2467 e (ASM_REWRITE_TAC[]);;
2468 e (SUBGOAL_THEN `#0.3972 + #6.072 = #6.4692` ASSUME_TAC);;
2469 e (ARITH_TAC);;
2470 e (ASM_REWRITE_TAC[]);;
2471 e (STRIP_TAC);;
2472 e (SUBGOAL_THEN `(#0.3924 * &(CARD (V:real^3->bool)) + #6.4692) + (--(#6.4692)) <  &4 * pi + (--(#6.4692))` ASSUME_TAC);;
2473 e (ASM_REWRITE_TAC [REAL_LT_RADD]);;
2474 e (POP_ASSUM MP_TAC);;
2475 e (ONCE_REWRITE_TAC [REAL_ADD_AC]);;
2476 e (PURE_REWRITE_TAC [GSYM real_sub]);;
2477 e (PURE_REWRITE_TAC [ARITH_RULE `#6.4692 - #6.4692 = &0`]);;
2478 e (PURE_REWRITE_TAC [REAL_ADD_RID]);;
2479 e (ONCE_REWRITE_TAC [REAL_ADD_AC]);;
2480 e (PURE_REWRITE_TAC [GSYM real_sub]);;
2481 e (SUBGOAL_THEN `&0 < (#0.3924)` ASSUME_TAC);;
2482 e (ARITH_TAC);;
2483 e (STRIP_TAC);;
2484 e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) < (&4 * pi - #6.4692)/(#0.3924)` ASSUME_TAC);;
2485 e (POP_ASSUM MP_TAC);;
2486 e (PURE_REWRITE_TAC [ARITH_RULE `#0.3924 * &(CARD (V:real^3->bool)) = &(CARD V)*(#0.3924)`]);;
2487 e (ASM_MESON_TAC [GSYM REAL_LT_RDIV_EQ]);;
2488 e (SUBGOAL_THEN `(&4 * pi - #6.4692) / #0.3924 < &16` ASSUME_TAC);;
2489 e (ASM_MESON_TAC[th11]);;
2490 e (ASM_MESON_TAC[REAL_LT_TRANS]);;
2491
2492
2493 let th12 = top_thm();;
2494
2495 (*---------------------------------------------------------------------------*)
2496 g `!(V:real^3->bool). &(CARD V) < &16 /\ &12 < &(CARD V) ==> CARD V = 13 \/
2497 CARD V = 14 \/ CARD V = 15`;;
2498 e (GEN_TAC);;
2499 e (STRIP_TAC);;
2500 e (SUBGOAL_THEN `CARD (V:real^3->bool) < 16` ASSUME_TAC);;
2501 e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
2502 e (SUBGOAL_THEN `12 < CARD (V:real^3->bool)` ASSUME_TAC);;
2503 e (ASM_MESON_TAC [REAL_OF_NUM_LT]);;
2504 e (ASM_MESON_TAC [ARITH_RULE `!a:num.a = 13 \/ a = 14 \/ a = 15 <=> a < 16 /\ 12 < a` ]);;
2505
2506 let NUM_REAL = top_thm();;
2507
2508 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)).
2509          FINITE V /\ FINITE V1 /\
2510          packing V  /\
2511          V SUBSET ball_annulus /\ V SUBSET V1 /\
2512          V1 SUBSET ball_annulus /\
2513          packing V1 /\
2514          (!y. (!x. x IN V1 ==> &2 <= dist (x,y)) ==> y IN V1) /\
2515          P = INTERS {half_spaces g_fun u|(u IN V1) /\ (~(vec 0 = u))} /\
2516          polyhedron P /\
2517          pi < #3.15 /\
2518          ~(lmfun_ineq_center V) /\
2519          ~(lmfun_ineq_center V1) /\
2520          (?r. r> &0 /\ ball(vec 0,r) SUBSET P) /\
2521          X = topological_component_yfan (vec 0,fan_of_polyhedron P) /\
2522          F = {l | l facet_of P} /\
2523          F_T = face_set_of_fan (fan_of_polyhedron P ) /\
2524          f1 o f2 = I /\ f2 o f1 = I /\
2525         IMAGE f1 V1 = X /\
2526         f3 o f4 = I /\ f3 o f4 = I /\
2527        IMAGE f3 V1 = F /\
2528        (!v. v IN V1 ==>  #0.591 - #0.0331 * (&(CARD {u | u extreme_point_of f3(v)})) +  #0.506 * lmfun (hl [vec 0; v])
2529        <= reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})))
2530     ==>
2531    (CARD V = 13 \/ CARD V = 14 \/ CARD V = 15)`;;
2532
2533 e (REPEAT GEN_TAC);;
2534 e (STRIP_TAC);;
2535 e (SUBGOAL_THEN `&12 < &(CARD (V:real^3->bool))` ASSUME_TAC);;
2536 e (ASM_MESON_TAC [condition_1]);;
2537 e (SUBGOAL_THEN `weakly_saturated (V1:real^3->bool) r r'` ASSUME_TAC);;
2538 e (ASM_MESON_TAC [thm17]);;
2539 e (SUBGOAL_THEN `&2 <= r:real` ASSUME_TAC);;
2540 e (PURE_REWRITE_TAC[r]);;
2541 e (ARITH_TAC);;
2542 e (SUBGOAL_THEN `r:real <= r'` ASSUME_TAC);;
2543 e (PURE_REWRITE_TAC [r;r';h0]);;
2544 e (ARITH_TAC);;
2545 e (SUBGOAL_THEN `bounded (P:real^3->bool)` ASSUME_TAC);;
2546 e (UNDISCH_TAC `polyhedron (P:real^3->bool)`);;
2547 e (UNDISCH_TAC `P = INTERS {half_spaces g_fun u|(u IN V1:real^3->bool) /\ (~(vec 0 = u))} `);;
2548 e (UNDISCH_TAC `weakly_saturated (V1:real^3->bool) r r'`);;
2549 e (UNDISCH_TAC `packing (V1:real^3->bool)`);;
2550 e (UNDISCH_TAC `FINITE (V1:real^3->bool)`);;
2551 e (POP_ASSUM MP_TAC);;
2552 e (POP_ASSUM MP_TAC);;
2553 e (SUBGOAL_THEN `!(V:real^3 -> bool) (g:real^3->real) (r:real) (r':real) P.(&2 <= r) /\ (r <= r') /\ (FINITE V) /\ packing V /\
2554 (weakly_saturated V r r') /\
2555  P = INTERS {half_spaces g u|(u IN V) /\ (~(vec 0 = u))} /\ polyhedron P ==>
2556 (bounded P)` ASSUME_TAC);;
2557 e (REWRITE_TAC [TARJJUW]);;
2558 e (POP_ASSUM (LABEL_TAC "F1"));;
2559 e (USE_THEN "F1" (MP_TAC o SPECL [`V1:real^3->bool`;`g_fun`;`r`;`r'`;`P:real^3->bool`]));;
2560 e (SET_TAC[]);;
2561 e (SUBGOAL_THEN `(?r:real. r> &0 /\ ball(vec 0,r) SUBSET (P:real^3->bool))` ASSUME_TAC);;
2562 e (EXISTS_TAC `r'':real`);;
2563 e (ASM_MESON_TAC[]);;
2564 e (SUBGOAL_THEN `sum (V1:real^3->bool)
2565              (\v:real^3. reg (g_fun v)
2566                   (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))) <=
2567              (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))` ASSUME_TAC);;
2568 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));;
2569 e (ASM_REWRITE_TAC[]);;
2570 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);;
2571 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));;
2572 e (ASM_REWRITE_TAC[]);;
2573 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);;
2574 e (ASM_MESON_TAC [th10]);;
2575 e (SUBGOAL_THEN `#0.591 * (&(CARD (V1:real^3->bool))) - #0.0331 * &(6*(CARD V1) - 12) + #0.506 * (&12) < sum V1
2576       (\v. reg (g_fun v)
2577            (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})))` ASSUME_TAC);;
2578 e (POP_ASSUM MP_TAC);;
2579 e (POP_ASSUM MP_TAC);;
2580 e (MESON_TAC[REAL_LTE_TRANS]);;
2581 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);;
2582 e (UNDISCH_TAC `sum (V1:real^3->bool)
2583              (\v. reg (g_fun v)
2584                   (&(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)}))) <=
2585              (sum (V1:real^3->bool) (\v:real^3. sol (vec 0) ((f1:(real^3) -> (real^3->bool))(v))))`);;
2586 e (POP_ASSUM MP_TAC);;
2587 e (MESON_TAC[REAL_LTE_TRANS]);;
2588 e (POP_ASSUM MP_TAC);;
2589 e (SUBGOAL_THEN `&4 * pi = (sum (X:(real^3->bool)->bool) (\v:real^3->bool. sol (vec 0) (v)))` ASSUME_TAC);;
2590 e (ASM_MESON_TAC [th7]);;
2591 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);;
2592 e (ASM_MESON_TAC [thm18]);;
2593 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);;
2594 e (POP_ASSUM MP_TAC);;
2595 e (POP_ASSUM MP_TAC);;
2596 e (ARITH_TAC);;
2597 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]));;
2598 e (SUBGOAL_THEN `CARD (V:real^3->bool) <= CARD (V1:real^3->bool)` ASSUME_TAC);;
2599 e (UNDISCH_TAC `FINITE (V1:real^3->bool)`);;
2600 e (UNDISCH_TAC `(V:real^3->bool) SUBSET V1`);;
2601 e (REPEAT STRIP_TAC);;
2602 e (SUBGOAL_THEN `(V:real^3->bool) SUBSET V1 /\ FINITE (V1:real^3->bool)` ASSUME_TAC);;
2603 e (ASM_MESON_TAC[]);;
2604 e (POP_ASSUM MP_TAC);;
2605 e (MESON_TAC[CARD_SUBSET]);;
2606 e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) <= &(CARD (V1:real^3->bool))` ASSUME_TAC);;
2607 e (POP_ASSUM MP_TAC);;
2608 e (MESON_TAC [REAL_OF_NUM_LE]);;
2609 e (SUBGOAL_THEN `&12 < &(CARD (V1:real^3->bool))` ASSUME_TAC);;
2610 e (UNDISCH_TAC `&12 < &(CARD (V:real^3->bool))`);;
2611 e (POP_ASSUM MP_TAC);;
2612 e (REAL_ARITH_TAC);;
2613 e (STRIP_TAC);;
2614 e (SUBGOAL_THEN `&(CARD (V1:real^3->bool)) < &16` ASSUME_TAC);;
2615 e (POP_ASSUM MP_TAC);;
2616 e (UNDISCH_TAC `pi < #3.15`);;
2617 e (POP_ASSUM MP_TAC);;
2618 e (MESON_TAC [th12]);;
2619 e (SUBGOAL_THEN `&(CARD (V:real^3->bool)) < &16` ASSUME_TAC);;
2620 e (POP_ASSUM MP_TAC);;
2621 e (UNDISCH_TAC `&(CARD (V:real^3->bool)) <= &(CARD (V1:real^3->bool))`);;
2622 e (MESON_TAC [REAL_LET_TRANS]);;
2623 e (UNDISCH_TAC `&12 < &(CARD (V:real^3->bool))`);;
2624 e (POP_ASSUM MP_TAC);;
2625 e (MESON_TAC [NUM_REAL]);;
2626
2627
2628 let DLWCHEM = top_thm();;