1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALISATION *)
6 (* Author: Dang Tat Dat *)
7 (* Date: In progress *)
8 (* ========================================================================== *)
10 needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;
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";;
22 (* ** Proof module type ** *)
25 (* ** Proof module ** *)
36 open Hypermap_and_fan;;
39 (*open Polyhedron_def;;*)
40 (*--------------Definition---------------------------------------------------*)
41 let weakly_saturated =
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)))`;;
49 `half_spaces (a:real^3) (b:real) =
50 {x:real^3| (a dot x) <= b}`;;
62 `(g_fun) (x:real^3) = (acs(dist(vec 0, x)/(&4))) - (pi/(&6))` ;;
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 = {} }`;;
67 (*-------------------------Fan Definiton-----------------------------------*)
69 let CASE_FAN_FINITE = new_definition `CASE_FAN_FINITE (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> FINITE V /\ ~(V SUBSET {})`;;
71 let CASE_FAN_ORIGIN = new_definition `CASE_FAN_ORIGIN (V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> ~((vec 0) IN (V))`;;
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))`;;
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)))`;;
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)`;;
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]);;
90 (*-------------------------------------------------------------------------*)
94 `interior_point (p:real^3) (P:real^3->bool)
95 <=> ?(r:real). (&0 < r) /\ (ball(p,r) SUBSET P)` ;;
98 `reg (a:real) (k:real) = (&2)*pi - (&2)*k*(asn(cos(a)*sin(pi/k)))` ;;
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)))`;;
105 let IN_DOUBLE = prove(`!x y z:real^N. x IN {y,z} <=> x = y \/ x = z`,SET_TAC[]);;
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[]);;
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]);;
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 ==>
121 let TARJJUW = new_axiom TARJJUW_concl;;
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}`;;
128 e (REWRITE_TAC [edges;EXTENSION]);;
129 e (GEN_TAC THEN EQ_TAC);;
130 e (REWRITE_TAC [IN_ELIM_THM]);;
132 e (MP_TAC (ISPECL [`V:real^3 -> bool`;`v:real^3`;`w:real^3`]SEGMENT_EDGE_OF));;
133 e (ASM_REWRITE_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]);;
141 e (SUBGOAL_THEN `!v:real^3 w:real^3 u:real . v + u % (w - v) = (&1 - u) % v + u % w` ASSUME_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]);;
149 e (REWRITE_TAC [IN_ELIM_THM]);;
151 e (EXISTS_TAC `u:real`);;
152 e (ASM_REWRITE_TAC[]);;
153 e (REWRITE_TAC [IN_ELIM_THM]);;
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);;
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]);;
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]);;
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]);;
175 e (REWRITE_TAC [IN_ELIM_THM]);;
177 e (EXISTS_TAC `u:real`);;
178 e (ASM_REWRITE_TAC[]);;
179 e (REWRITE_TAC [IN_ELIM_THM]);;
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]);;
189 e (REWRITE_TAC [IN_ELIM_THM]);;
191 e (EXISTS_TAC `u:real`);;
192 e (ASM_REWRITE_TAC[]);;
193 e (REWRITE_TAC [IN_ELIM_THM]);;
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));;
200 e (MP_TAC (ISPECL [`v:real^3`;`w:real^3`]HALFLINE_SUBSET_AFFINE_HULL));;
202 e (MP_TAC (ISPECL [`{v:real^3,w:real^3}`]AFF_DIM_AFFINE_HULL));;
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[]);;
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]);;
215 e (REWRITE_TAC[IN_DOUBLE;IN_ELIM_THM]);;
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]));;
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]));;
233 let EDGE_CONVEX_HULL = top_thm();;
235 g `!(V:real^3 -> bool). (polyhedron V) /\ (bounded V) /\ (interior_point (vec 0) V) ==> FANO (fan_of_polyhedron V)`;;
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[]);;
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[]);;
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[]);;
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]);;
255 let JLIGZGS = top_thm();;
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))`;;
262 let WGVWSKE = new_axiom WGVWSKE_concl;;
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))`;;
269 let GGRLKHP = new_axiom GGRLKHP_concl;;
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]);;
274 (*---------------------------------------------------------------------------*)
276 (*FACET_OF_POLYHEDRON_EXPLICIT*)
277 (*Chung minh rang o day ton tai mot song anh*)
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) /\
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)`;;
293 let CZZHBLI_1 = new_axiom CZZHBLI_concl_1;;
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) /\
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)`;;
303 e (MP_TAC (ISPECL [`P:real^3->bool`;`f:real^3->bool`]FACET_OF_POLYHEDRON));;
304 e (ASM_REWRITE_TAC[]);;
307 FACET_OF_POLYHEDRON_EXPLICIT;;
308 FACET_OF_POLYHEDRON;;
309 FINITE_POLYHEDRON_FACES;;
310 FINITE_POLYHEDRON_EXTREME_POINT;;
313 (*----------------------------------------------------------------------------*)
315 let RDWKARC_concl = `~kepler_conjecture /\ (!V. cell_cluster_estimate V) /\
317 ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~(lmfun_ineq_center V))`;;
319 let RDWKARC = new_axiom RDWKARC_concl;;
322 (*---------------------------------------------------------------------------*)
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)`;;
330 let AMHFNXP = new_axiom AMHFNXP_concl;;
332 (*---------------------------------------------------------------------------*)
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`;;
336 let BSXAQBQ = new_axiom BSXAQBQ_concl;;
337 (*---------------------------------------------------------------------------*)
339 let PIIJBJK_concl =`!(V:real^3 -> bool)(E:(real^3->bool)->bool).
340 fully_surrounded (V,E) ==>
344 let PIIJBJK = new_axiom PIIJBJK_concl;;
345 (*---------------------------------------------------------------------------*)
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)`;;
354 let UVPFEEP_1= new_axiom UVPFEEP_concl1;;
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) /\
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`;;
367 let GOTCJAH = new_axiom GOTCJAH_concl;;
369 (*---------------------------------proof--------------------------------------*)
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);;
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]);;
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);;
390 e (ASM_MESON_TAC[]);;
391 e (ASM_REWRITE_TAC[]);;
394 let thm1 = top_thm();;
396 (*----------------------------------------------------------------------------*)
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"));;
410 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
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]);;
419 e (POP_ASSUM MP_TAC);;
420 e (REWRITE_TAC [REAL_NOT_LT]);;
422 e (SUBGOAL_THEN `(&0) < (&2)` ASSUME_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)`]);;
429 let thm2 = top_thm();;
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"));;
442 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
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]);;
452 let thm21 = top_thm();;
453 (*----------------------------------------------------------------------------*)
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`));;
465 e (SUBGOAL_THEN `!(v:real^3). (&1) <= dist(vec 0,v)/(&2) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_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`));;
471 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (dist (vec 0,v) / &2) <= (&1)` ASSUME_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)`]);;
479 e (ASM_MESON_TAC[REAL_LE_TRANS]);;
481 let thm3 = top_thm();;
483 (*----------------------------------------------------------------------------*)
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)`;;
487 e (REWRITE_TAC [packing;ball_annulus]);;
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`));;
500 e (SUBGOAL_THEN `&0 < &2` ASSUME_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]);;
509 let thm4 = top_thm();;
511 g `! (x:real^N) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w))`;;
513 e (EXISTS_TAC ` inv (&2) % ( x + (y:real^N) ) `);;
514 e (REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]);;
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]);;
523 e (EXISTS_TAC `dist (x:real^N,y) /(&2)`);;
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[]);;
531 e (ASM_REWRITE_TAC[]);;
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]);;
538 let thm5 = top_thm();;
541 let dat_th1 = prove(` segment [v,w:real^3] SUBSET affine hull {v,w} `,
543 REWRITE_TAC[AFFINE_HULL_2; segment; SUBSET; IN_ELIM_THM] THEN
545 MESON_TAC[REAL_ARITH` (&1 - x ) + x = &1 `]);;
547 g `(! (x:real^3) y. ?d. (affine hull {x,y}) d /\ (?c. ! w. {x,y} w ==> c = dist (d,w)))
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[]);;
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]);;
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[]);;
585 let thm6 = top_thm();;
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]);;
594 let thm7 = top_thm();;
596 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
597 (u IN V) ==> ~(vec 0 = u)`;;
599 e (PURE_REWRITE_TAC [ball_annulus;SUBSET;DIFF;IN_ELIM_THM;cball;ball]);;
601 e (POP_ASSUM MP_TAC);;
602 e (POP_ASSUM MP_TAC);;
603 e (DISCH_THEN (LABEL_TAC "F1"));;
605 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
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[]);;
622 e (ASM_REWRITE_TAC[]);;
624 let thm8= top_thm();;
627 g `!u:real^3 . ?d.(!w. {vec 0, u} w ==> d = dist (midpoint (vec 0,u),w))`;;
629 e (EXISTS_TAC `dist(vec 0,u:real^3)/(&2)`);;
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[]);;
637 e (ASM_REWRITE_TAC[]);;
638 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
640 e (ASM_REWRITE_TAC[]);;
641 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
644 let thm9 = top_thm();;
646 g `!w:real^3 u. ~(vec 0 = u) /\ {vec 0, u} w ==> dist (vec 0,u)/(&2) = dist (circumcenter {vec 0, u},w)`;;
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]);;
658 e (ASM_REWRITE_TAC[]);;
659 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
661 e (ASM_REWRITE_TAC[]);;
662 e (PURE_REWRITE_TAC [DIST_MIDPOINT]);;
665 let thm10 = top_thm();;
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))`;;
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[]);;
684 let thm11 = top_thm();;
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]);;
693 let thm12 = top_thm();;
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) `;;
699 e (SUBGOAL_THEN `~(vec 0 = u:real^3)` ASSUME_TAC);;
700 e (ASM_MESON_TAC [thm8]);;
701 e (ASM_MESON_TAC [thm12]);;
703 let thm13 = top_thm();;
705 g `!(V:real^3->bool) (u:real^3). (packing V) /\ (V SUBSET ball_annulus) /\
706 (u IN V) ==> &1 <= hl [vec 0;u] `;;
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]);;
714 let thm14 = top_thm();;
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`));;
725 e (SUBGOAL_THEN `!(v:real^3). (&1) <= hl [vec 0;v] ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_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`));;
731 e (SUBGOAL_THEN `!(v:real^3). (v IN (V:real^3->bool)) ==> lmfun (hl [vec 0;v]) <= (&1)` ASSUME_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)`]);;
739 e (ASM_MESON_TAC[REAL_LE_TRANS]);;
741 let thm15 = top_thm();;
744 g `!(V:real^3->bool). FINITE V /\ packing V /\
745 V SUBSET ball_annulus /\ ~(lmfun_ineq_center V)
746 ==> &12 < &(CARD V)`;;
748 e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
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]);;
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]))`);;
761 e (ASM_MESON_TAC[]);;
763 let condition_1 = top_thm();;
765 (*-------------------------------------------------------------------------*)
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))`;;
769 e (DISCH_THEN (LABEL_TAC "F1"));;
772 e (USE_THEN "F1"(MP_TAC o SPEC `u:real^3`));;
773 e (POP_ASSUM MP_TAC);;
776 let thm16 = top_thm();;
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'`;;
781 e (PURE_REWRITE_TAC [packing]);;
783 e (PURE_REWRITE_TAC [weakly_saturated]);;
784 e (PURE_REWRITE_TAC [r;r']);;
787 e (ASM_CASES_TAC `p:real^3 IN (V1:real^3->bool)`);;
788 e (EXISTS_TAC `p:real^3`);;
790 e (ASM_REWRITE_TAC[]);;
791 e (PURE_REWRITE_TAC [DIST_REFL]);;
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]);;
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`));;
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);;
811 e (UNDISCH_TAC `~(p:real^3 IN (V1:real^3->bool))`);;
812 e (POP_ASSUM MP_TAC);;
815 let thm17 = top_thm();;
817 (*---------------------------------------------------------------------------*)
818 g `!h1 h2 g1 g2. (h1 o h2) o (g1 o g2) = h1 o (h2 o g1) o g2`;;
820 e (PURE_REWRITE_TAC [o_ASSOC]);;
824 let MUL_o_ASSOC = top_thm();;
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) /\
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))`;;
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)`);;
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`);;
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`);;
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`);;
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`);;
871 let V_TOPO_BIJ = top_thm();;
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) /\
879 FANO (fan_of_polyhedron 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))`;;
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)`
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)`);;
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`);;
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`);;
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`);;
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`);;
930 let V_FHYPER_BIJ = top_thm();;
932 (*----------------------------------------------------------------------------*)
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 /\
942 ==> (sum (V) (\v:real^3. sol (vec 0) (f1(v))) = sum (X) (\v. sol (vec 0) v ))`;;
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);;
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 `);;
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 `);;
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);;
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));;
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);;
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)`);;
978 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
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]);;
984 e (PURE_REWRITE_TAC [o_THM]);;
986 e (ASM_REWRITE_TAC[]);;
988 let thm18 = top_thm();;
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 /\
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);;
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);;
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)))`;;
1016 search [`sum s f <= sum s g`];;
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 /\
1030 type_of `sum (V) (\v:real^3. sol (vec 0) (f1(v)))`;;
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
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 })
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
1060 /\ (interior_point (vec 0) P)
1063 type_of `face_set_of_fan (fan_of_polyhedron P )`;;
1064 type_of `facet_of`;;
1066 type_of `extreme_point_of`;;
1067 type_of `facet_of`;;
1069 EXTREME_POINT_OF_LINEAR_IMAGE;;
1071 search [`leaner f`];;
1073 search [`extreme_point_of`];;
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) `;;
1082 (*---------------------------------------------------------------------------*)
1085 g `!(V:real^3 -> bool).(V SUBSET ball_annulus) ==> (!x:real^3. x IN V ==> ~(vec 0 = x))`;;
1087 e (PURE_REWRITE_TAC [ball_annulus;cball;ball;DIFF]);;
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]);;
1102 e (ASM_MESON_TAC [ARITH_RULE `&0 < &2`]);;
1103 e (ASM_REWRITE_TAC[]);;
1105 let th54 = top_thm();;
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);;
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);;
1116 e (REWRITE_TAC [SUBSET]);;
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);;
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))));;
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`);;
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]);;
1149 e (UNDISCH_TAC `x IN (s:real^3->bool)`);;
1150 e (POP_ASSUM MP_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);;
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);;
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`]);;
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);;
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`]);;
1179 e (SUBGOAL_THEN `(&0 <= (pi / &6)) /\ ((pi / &6) <= pi)` ASSUME_TAC);;
1180 e (MP_TAC PI_POS_LE);;
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);;
1190 e (UNDISCH_TAC `&1 / &2 <= dist (vec 0,u:real^3) / &4`);;
1191 e (MP_TAC (ARITH_RULE `-- &1 <= &1 / &2`));;
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);;
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);;
1207 e (SUBGOAL_THEN `(&3) <= &2 pow 2` ASSUME_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"));;
1230 e (USE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
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);;
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"));;
1242 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1243 e (ASM_REWRITE_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);;
1250 e (POP_ASSUM (LABEL_TAC "F1"));;
1252 e (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));;
1253 e (ASM_REWRITE_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`));;
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[]);;
1264 e (POP_ASSUM MP_TAC);;
1265 e (REWRITE_TAC [IN_INTERIOR_CBALL]);;
1266 e (REWRITE_TAC [interior_point]);;
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]);;
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));;
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)`);;
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]);;
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]);;
1286 e (REWRITE_TAC [IN_ELIM_THM]);;
1288 e (EXISTS_TAC `u:real^3`);;
1289 e (ASM_REWRITE_TAC[]);;
1291 e (REWRITE_TAC [IN_ELIM_THM]);;
1292 e (REWRITE_TAC [IN_ELIM_THM]);;
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[]);;
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);;
1305 e (REWRITE_TAC [IN_ELIM_THM]);;
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);;
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]);;
1321 e (POP_ASSUM MP_TAC);;
1322 e (REWRITE_TAC [IN_INTERIOR;interior_point]);;
1324 let th51= top_thm();;
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);;
1330 e (REWRITE_TAC [fan_of_polyhedron;fully_surrounded]);;
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]);;
1340 let th52 = top_thm();;
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);;
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]);;
1351 let th53 = top_thm();;
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)`;;
1357 e (REPEAT GEN_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[]);;
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[]);;
1373 let DART_OF_HYPERMAP_FAN = top_thm();;
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);;
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);;
1387 e (REWRITE_TAC [EXTENSION]);;
1390 e (POP_ASSUM (LABEL_TAC "F1"));;
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]);;
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);;
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]);;
1411 e (ASM_REWRITE_TAC[]);;
1413 let FULLY_SURROUND_IS_NON_ISOLATED_FAN3 = top_thm();;
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[]);;
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[]);;
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[]);;
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]);;
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`));;
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]);;
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]);;
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]);;
1457 e (SUBGOAL_THEN `v:real^3 IN {v:real^3,w:real^3}` ASSUME_TAC);;
1459 e (ASM_MESON_TAC[]);;
1460 e (ASM_REWRITE_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);;
1469 let FULLY_EDGE = top_thm();;
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]);;
1476 let FULLY_EDGE1 = top_thm();;
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);;
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]);;
1485 let FULLY_SURROUNDED_IMP_DART = top_thm();;
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);;
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]);;
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);;
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))`);;
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]);;
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]);;
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]);;
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`));;
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]);;
1577 e (REWRITE_TAC [fan_of_polyhedron;face_set_of_fan]);;
1578 e (REWRITE_TAC [GSYM fan_of_polyhedron]);;
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[]);;
1585 let th5 = top_thm();;
1587 (*----------------------------------------------------------------------------*)
1588 (* proof CARD V = CARD {f|f facet_of V}*)
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);;
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);;
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);;
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`);;
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`);;
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);;
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[]);;
1627 let CARD_1 = top_thm();;
1629 (*---------------------------------------------------------------------------*)
1631 (*Proof CARD {f|f facet_of V} = CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) *)
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);;
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);;
1641 e (MP_TAC (ISPECL [`(h:(real^3) -> (real^3->bool))`;`V:real^3->bool`]FINITE_IMAGE));;
1642 e (ASM_REWRITE_TAC[]);;
1644 let FINITE_FACE_SET = top_thm();;
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);;
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);;
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);;
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`);;
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`);;
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);;
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[]);;
1688 let CARD_2 = top_thm();;
1691 (*----------------------------------------------------------------------------*)
1693 (*Proof CARD (topological_component_yfan (vec 0,fan_of_polyhedron V)) =
1694 CARD (face_set_of_fan (fan_of_polyhedron V)) *)
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))
1700 e (REPEAT GEN_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]);;
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);;
1711 e (MP_TAC (ISPECL [`(h:(real^3->bool) -> (real^3->bool))`;`F':(real^3->bool)->bool`]FINITE_IMAGE));;
1712 e (ASM_REWRITE_TAC[]);;
1714 let FINITE_TOPO_SET = top_thm();;
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);;
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]);;
1733 e (POP_ASSUM MP_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);;
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`);;
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`);;
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);;
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[]);;
1767 let CARD_3 = top_thm();;
1770 (*----------------------------------------------------------------------------*)
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);;
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[]);;
1784 let CARD_4 = top_thm();;
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);;
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]);;
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]));;
1804 let CARD_5 = top_thm();;
1806 (*--------------------------------------------------------------------------*)
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);;
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]);;
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]);;
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)`);;
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))`);;
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)))`);;
1838 e (POP_ASSUM(fun th ->REWRITE_TAC[th]));;
1839 e (ASM_REWRITE_TAC[]);;
1841 let th6 = top_thm();;
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)
1850 ==> &4 * pi = sum X (\v. sol (vec 0) (v))`;;
1852 let th7 = new_axiom th7_concl;;
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 /\
1865 f3 o f4 = I /\ f3 o f4 = I /\
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))))`;;
1870 let th8 = new_axiom th8_concl;;
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);;
1875 e (REWRITE_TAC [half_spaces]);;
1876 e (UNDISCH_TAC `FINITE (V:real^3->bool)`);;
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]);;
1884 e (REWRITE_TAC [IN_ELIM_THM]);;
1886 e (EXISTS_TAC `u:real^3`);;
1887 e (ASM_REWRITE_TAC[]);;
1889 e (REWRITE_TAC [IN_ELIM_THM]);;
1890 e (REWRITE_TAC [IN_ELIM_THM]);;
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[]);;
1901 let FINITE_HALF_SPACES = top_thm();;
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 /\
1913 f3 o f4 = I /\ f3 o f4 = I /\
1915 ==> (!u. u IN V ==> f3 u = {p | p dot u = g_fun u} INTER P)`;;
1918 e (REPEAT GEN_TAC);;
1920 e (MP_TAC (ISPECL [`P:real^3->bool`] POLYHEDRON_INTER_AFFINE_MINIMAL));;
1921 e (UNDISCH_TAC `polyhedron (P:real^3->bool)`);;
1923 e (FIRST_ASSUM (fun th -> REWRITE_TAC [th]));;
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));;
1927 e (DISCH_THEN (LABEL_TAC "F1"));;
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)}`));;
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]);;
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)}`);;
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]);;
1944 search [`FINITE P`];;
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))`;;
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 /\
1960 f3 o f4 = I /\ f3 o f4 = I /\
1963 (!v:real^3. v IN V ==> reg (g_fun v) (&(CARD {u | u extreme_point_of f3(v)})) <= sol (vec 0) (f1(v)))`;;
1967 e (REPEAT GEN_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]);;
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]);;
1985 FACET_OF_POLYHEDRON_EXPLICIT;;
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)}`);;
1995 e (POP_ASSUM(fun th ->REWRITE_TAC[GSYM th]));;
1997 e (REWRITE_TAC [reg]);;
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";;
2008 e (SUBGOAL_THEN `(f3:(real^3) -> (real^3->bool))(v:real^3) IN F'` ASSUME_TAC);;
2010 search [`f (v) IN V`];;
2016 search [`x IN V /\ f x`];;
2017 type_of `extreme_point_of`;;
2018 search [`f o g = I`];;
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 /\
2030 f3 o f4 = I /\ f4 o f3 = I /\
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))))`;;
2035 e (REPEAT GEN_TAC);;
2041 (*----------------------------------------------------------------------------*)
2043 g `!a b c e f:real. a = b + c /\ b = e - f ==> a = e - f + c`;;
2044 e (REPEAT GEN_TAC);;
2046 e (ASM_REWRITE_TAC[]);;
2048 let th91 = top_thm();;
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 /\
2059 f3 o f4 = I /\ f3 o f4 = I /\
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))))`;;
2063 let th92 =new_axiom th92_T;;
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);;
2071 e (REWRITE_TAC [edges]);;
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)))`;;
2089 e (REPEAT GEN_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]));;
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]);;
2117 e (REWRITE_TAC [IN_ELIM_THM]);;
2119 e (REWRITE_TAC [dart]);;
2120 KREIN_MILMAN_POLYTOPE;;
2122 EXTREME_POINT_OF_FACE;;
2123 DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET;;
2124 search [`vertices`];;
2126 card_partition_formula;;
2129 edge_map_and_darts;;
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`,
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]));;
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`,
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]));;
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))))`;;
2155 e (REPEAT GEN_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));;
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));;
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]);;
2172 e (REWRITE_TAC [GSYM MEMBER_NOT_EMPTY;IN_INTER]);;
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]);;
2181 e (POP_ASSUM MP_TAC);;
2182 e (ASM_REWRITE_TAC[]);;
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))))`;;
2194 e (REPEAT GEN_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)}`);;
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]);;
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]);;
2242 search [`convex hull {v', w'} face_of P`];;
2243 e (REWRITE_TAC [IN_ELIM_THM]);;
2245 e (REWRITE_TAC weakly_saturated V r r'
2246 e (REWRITE_TAC [dart]);;
2249 search [`CARD (UNIONS s)`];;
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 /\
2261 f3 o f4 = I /\ f3 o f4 = I /\
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)})))
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)})))`;;
2269 e (REPEAT GEN_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);;
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]);;
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)
2309 &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) = #0.0331 * sum (V)
2311 &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(v)})) ` ASSUME_TAC);;
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)
2319 &(CARD {u | u extreme_point_of (f3:(real^3) -> (real^3->bool))(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] ));;
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[]);;
2331 let th9 = top_thm();;
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])))`;;
2342 e (REPEAT GEN_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]);;
2362 e (UNDISCH_TAC `~lmfun_ineq_center (V:real^3->bool)`);;
2363 e (PURE_REWRITE_TAC [lmfun_ineq_center]);;
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]);;
2381 let th10 = top_thm();;
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]]);;
2386 let REAL_ADD2_ADD2 = prove (`!x y z:real. x + (y + z) = x + y + z`,SET_TAC[]);;
2388 g `(pi < #3.15) ==> (&4 * pi - #6.4692) / #0.3924 < &16`;;
2390 e (SUBGOAL_THEN `&0 < &4` ASSUME_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`]);;
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);;
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);;
2409 e (ASM_MESON_TAC[REAL_LT_TRANS]);;
2411 let th11 = top_thm();;
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`;;
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);;
2422 e (ASM_MESON_TAC[LT_LMULT]);;
2423 e (POP_ASSUM MP_TAC);;
2424 e (PURE_REWRITE_TAC [ARITH_RULE `6 * 12 = 72`]);;
2426 e (SUBGOAL_THEN ` 12 < 72 ` ASSUME_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`]);;
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`]);;
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`]);;
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);;
2470 e (ASM_REWRITE_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);;
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]);;
2493 let th12 = top_thm();;
2495 (*---------------------------------------------------------------------------*)
2496 g `!(V:real^3->bool). &(CARD V) < &16 /\ &12 < &(CARD V) ==> CARD V = 13 \/
2497 CARD V = 14 \/ CARD V = 15`;;
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` ]);;
2506 let NUM_REAL = top_thm();;
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 /\
2511 V SUBSET ball_annulus /\ V SUBSET V1 /\
2512 V1 SUBSET ball_annulus /\
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))} /\
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 /\
2526 f3 o f4 = I /\ f3 o f4 = I /\
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)})))
2531 (CARD V = 13 \/ CARD V = 14 \/ CARD V = 15)`;;
2533 e (REPEAT GEN_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]);;
2542 e (SUBGOAL_THEN `r:real <= r'` ASSUME_TAC);;
2543 e (PURE_REWRITE_TAC [r;r';h0]);;
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`]));;
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
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)
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);;
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);;
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]);;
2628 let DLWCHEM = top_thm();;