1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Chapter: Tame Hypermap *)
\r
5 (* Author: Alexey Solovyev *)
\r
6 (* Date: 2010-06-17 *)
\r
7 (* ========================================================================== *)
\r
9 (* General properties of a contravening packing *)
\r
12 flyspeck_needs "leg/collect_geom.hl";;
\r
13 flyspeck_needs "trigonometry/trigonometry.hl";;
\r
14 flyspeck_needs "nonlinear/ineq.hl";;
\r
16 flyspeck_needs "fan/HypermapAndFan.hl";;
\r
17 flyspeck_needs "tame/CKQOWSA.hl";;
\r
18 flyspeck_needs "tame/tame_defs.hl";;
\r
21 module Tame_general = struct
\r
24 open Hypermap_and_fan;;
\r
29 (* Non-linear inequalities *)
\r
30 (* let tame_hypermap_calcs_concl = new_definition Tame_defs.tame_hypermap_calcs;; *)
\r
33 (* tame ==> restricted *)
\r
34 let RUNOQPQ = prove(`!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`,
\r
35 GEN_TAC THEN REWRITE_TAC[tame_hypermap; restricted_hypermap] THEN
\r
36 SIMP_TAC[tame_1; tame_2; tame_3; tame_5a; tame_9a] THEN
\r
37 REPEAT STRIP_TAC THENL
\r
39 FIRST_X_ASSUM (MP_TAC o check (fun th -> (concl th) = `tame_8 (H:(A)hypermap)`)) THEN
\r
40 REWRITE_TAC[tame_8; Hypermap.number_of_faces; Hypermap.face_set; Hypermap.set_of_orbits] THEN
\r
41 SUBGOAL_THEN `{orbit_map (face_map (H:(A)hypermap)) x | x | x IN dart H} = {}` (fun th -> REWRITE_TAC[th]) THENL
\r
43 ASM_REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
\r
44 X_GEN_TAC `ff:A->bool` THEN
\r
45 REWRITE_TAC[IN_ELIM_THM];
\r
48 REWRITE_TAC[CARD_CLAUSES; ARITH_RULE `~(0 >= 3)`];
\r
50 MP_TAC (SPEC `H:(A)hypermap` Hypermap.lemmaZHQCZLX) THEN
\r
51 ASM_SIMP_TAC[is_node_nondegenerate; GSYM GE];
\r
53 POP_ASSUM MP_TAC THEN
\r
54 REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits] THEN
\r
55 ONCE_REWRITE_TAC[GSYM Hypermap.face] THEN
\r
56 REWRITE_TAC[IN_ELIM_THM] THEN
\r
62 (* UBHDEUU1 = CKQOWSA *)
\r
63 let UBHDEUU1 = Ckqowsa.CKQOWSA;;
\r
66 (* (V,ECTC V) is a fan *)
\r
67 let UBHDEUU2 = prove(`!V. packing V /\ V SUBSET ball_annulus /\ ~(V = {}) ==> FAN(vec 0, V, ECTC V)`,
\r
68 REPEAT STRIP_TAC THEN
\r
69 MATCH_MP_TAC Topology.CTVTAQA THEN
\r
70 EXISTS_TAC `ESTD V` THEN
\r
71 ASM_SIMP_TAC[UBHDEUU1] THEN
\r
72 REWRITE_TAC[ECTC; ESTD; SUBSET; IN_ELIM_THM] THEN
\r
73 REPEAT STRIP_TAC THEN
\r
74 MAP_EVERY EXISTS_TAC [`v:real^3`; `w:real^3`] THEN
\r
75 ASM_SIMP_TAC[Sphere.h0; REAL_ARITH `a = &2 ==> a <= &2 * #1.26`]);;
\r
79 (*********************)
\r
80 (* Numerical results *)
\r
81 (*********************)
\r
83 let COS_PI3 = prove(`cos (pi / &3) = &1 / &2`,
\r
84 REWRITE_TAC[COS_SIN] THEN
\r
85 REWRITE_TAC[REAL_ARITH `pi / &2 - pi / &3 = pi / &6`] THEN
\r
86 REWRITE_TAC[SIN_PI6]);;
\r
89 let ACS_2 = prove(`acs (&1 / &2) = pi / &3`,
\r
90 REWRITE_TAC[SYM COS_PI3] THEN
\r
91 MATCH_MP_TAC ACS_COS THEN
\r
92 REWRITE_TAC[REAL_ARITH `(&0 <= a / &3 <=> &0 <= a) /\ (a / &3 <= a <=> &0 <= a)`] THEN
\r
93 MATCH_MP_TAC REAL_LT_IMP_LE THEN
\r
94 REWRITE_TAC[PI_POS]);;
\r
97 let sol0_POS = prove(`&0 < sol0`,
\r
98 REWRITE_TAC[Pack_defs.sol0] THEN
\r
99 REWRITE_TAC[REAL_ARITH `&0 < &3 * a - pi <=> pi / &3 < a`] THEN
\r
100 REWRITE_TAC[SYM ACS_2] THEN
\r
101 MATCH_MP_TAC ACS_MONO_LT THEN
\r
105 (****************************************)
\r
109 (*******************************************************************************************)
\r
110 (* Connections between algebraic definitions in Sphere and geometric definitions elsewhere *)
\r
111 (*******************************************************************************************)
\r
114 let ly_EQ_lmfun = prove(`!x:real^3#real^3. norm (FST x) <= &2 * h0 ==> lmfun (h_dart x) = ly (norm (FST x))`,
\r
115 REWRITE_TAC[Pack_defs.lmfun; Sphere.ly; Sphere.interp; h_dart; Pack_defs.h0] THEN
\r
120 (* sol0 = const1 * pi *)
\r
121 let sol0_EQ_sol_y = prove(`sol0 = sol_y (&2) (&2) (&2) (&2) (&2) (&2)`,
\r
122 REWRITE_TAC[Pack_defs.sol0; Sphere.sol_y; Sphere.dih_y; Sphere.dih_x; Sphere.delta_x4; Sphere.delta_x] THEN
\r
123 CONV_TAC (DEPTH_CONV let_CONV) THEN
\r
124 CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
\r
125 MP_TAC (SPEC `&1 / &3` Trigonometry2.acs_atn2) THEN
\r
126 CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
\r
127 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
128 REWRITE_TAC [REAL_ARITH `&3 * (a - b) - c = (a + d) + (a + d) + (a + d) - c <=> --b = d`] THEN
\r
129 MP_TAC (SPECL [`sqrt (&8 / &9)`; `&1 / &3`] Trigonometry1.ATN2_RNEG) THEN
\r
130 CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
\r
131 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
\r
132 SUBGOAL_THEN `sqrt (&2048) = &48 * sqrt (&8 / &9) /\ -- &16 = &48 * (-- &1 / &3)` ASSUME_TAC THENL
\r
134 MP_TAC (SPECL [`&48`; `&8 / &9`] Vol1.SQRT_MUL_POW_2) THEN
\r
135 CONV_TAC (REAL_RAT_REDUCE_CONV);
\r
138 ASM_REWRITE_TAC[] THEN
\r
139 MATCH_MP_TAC (GSYM Trigonometry1.ATN2_LMUL_EQ) THEN
\r
143 (* sol0 = const1 *)
\r
144 let sol0_over_pi_EQ_const1 = prove(`sol0 / pi = const1`,
\r
145 REWRITE_TAC[sol0_EQ_sol_y; Sphere.const1]);;
\r
149 (* Alternative form for ineq *)
\r
150 let INEQ_ALT = prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,
\r
152 MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL
\r
154 REWRITE_TAC[Sphere.ineq; ALL];
\r
157 MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN
\r
158 DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN
\r
159 DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
\r
160 MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN
\r
161 DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN
\r
162 DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN
\r
163 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
164 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
165 ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;
\r
168 (* delta = delta_x *)
\r
169 let DELTA_EQ_DELTA_X = prove(`!x1 x2 x3 x4 x5 x6.
\r
170 delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,
\r
171 REPEAT GEN_TAC THEN
\r
172 REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN
\r
176 (* Connection between delta_x and delta_x4 *)
\r
177 let DELTA_X_AND_DELTA_X4 = prove(`!x1 x2 x3 x4 x5 x6.
\r
178 (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
\r
179 let d = delta_x x1 x2 x3 x4 x5 x6 in
\r
180 let v1 = ups_x x1 x2 x6 in
\r
181 let v2 = ups_x x1 x3 x5 in
\r
182 &4 * x1 * d = v1 * v2 - d4 * d4)`,
\r
183 REPEAT GEN_TAC THEN
\r
184 REPEAT (CONV_TAC let_CONV) THEN
\r
185 REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN
\r
192 let DIHV_EQ_DIH_Y = prove(`!v0:real^3 v1 v2 v3. ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3}
\r
193 ==> (let v01 = dist (v0, v1) in
\r
194 let v02 = dist (v0, v2) in
\r
195 let v03 = dist (v0, v3) in
\r
196 let v12 = dist (v1, v2) in
\r
197 let v13 = dist (v1, v3) in
\r
198 let v23 = dist (v2, v3) in
\r
199 dihV v0 v1 v2 v3 = dih_y v01 v02 v03 v23 v13 v12)`,
\r
200 REPEAT GEN_TAC THEN
\r
202 FIRST_ASSUM (MP_TAC o (fun th -> CONJUNCT2 (MATCH_MP (let_RULE Trigonometry.OJEKOJF) th))) THEN
\r
203 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
204 REPEAT (CONV_TAC let_CONV) THEN
\r
205 MAP_EVERY ABBREV_TAC [`v01 = dist(v0:real^3,v1)`; `v02 = dist(v0:real^3,v2)`;
\r
206 `v03 = dist(v0:real^3,v3)`; `v12 = dist(v1:real^3,v2)`;
\r
207 `v13 = dist(v1:real^3,v3)`; `v23 = dist(v2:real^3,v3)`;
\r
208 `d = delta_x (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`;
\r
209 `d4 = delta_x4 (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`] THEN
\r
210 REWRITE_TAC[let_RULE Sphere.dih_y; let_RULE Sphere.dih_x; GSYM REAL_POW_2] THEN
\r
211 ASM_REWRITE_TAC[REAL_ARITH `a - b = a + c <=> c = --b`] THEN
\r
213 MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN
\r
214 DISJ_CASES_TAC (TAUT `~(d4 = &0) \/ d4 = &0`) THEN ASM_REWRITE_TAC[] THEN
\r
215 MATCH_MP_TAC SQRT_POS_LT THEN
\r
217 MP_TAC (let_RULE (SPECL [`v01 pow 2`; `v02 pow 2`; `v03 pow 2`; `v23 pow 2`; `v13 pow 2`; `v12 pow 2`] DELTA_X_AND_DELTA_X4)) THEN
\r
218 ASM_REWRITE_TAC[] THEN
\r
219 DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a - &0 * &0 = a`]) THEN
\r
221 MP_TAC (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT) THEN
\r
222 ASM_REWRITE_TAC[] THEN
\r
223 MP_TAC (INST [`v3:real^3`,`v2:real^3`] (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)) THEN
\r
224 ASM_REWRITE_TAC[] THEN
\r
225 REPEAT DISCH_TAC THEN
\r
226 MATCH_MP_TAC REAL_LT_MUL THEN
\r
227 ASM_REWRITE_TAC[]);;
\r
233 (************************************************************************************)
\r
236 (* Properties of a contravening packing *)
\r
239 let DIFF_LEMMA = prove(`!A B. A SUBSET B ==> (A = B DIFF (B DIFF A))`,
\r
240 REWRITE_TAC[SUBSET; EXTENSION; IN_DIFF; DE_MORGAN_THM] THEN
\r
241 REWRITE_TAC[TAUT `P /\ (~P \/ Q) <=> P /\ Q`] THEN
\r
242 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[]);;
\r
246 (* (V,ESTD V) is a fan for a contravening packing V *)
\r
247 let CONTRAVENING_FAN = prove(`!V. contravening V ==> FAN (vec 0,V,ESTD V)`,
\r
248 REWRITE_TAC[contravening] THEN
\r
249 GEN_TAC THEN REWRITE_TAC[GSYM IMP_IMP] THEN
\r
250 REPLICATE_TAC 5 DISCH_TAC THEN
\r
251 REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
\r
252 MATCH_MP_TAC Ckqowsa.CKQOWSA THEN
\r
253 ASM_REWRITE_TAC[] THEN
\r
254 POP_ASSUM (LABEL_TAC "A") THEN DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN
\r
255 ASM_REWRITE_TAC[CARD_CLAUSES] THEN
\r
262 let CONTRAVENING_IMP_SURROUNDED = prove(`!V v. contravening V /\ v IN V ==> surrounded_node (V,ESTD V) v`,
\r
263 ASM_SIMP_TAC[contravening]);;
\r
266 let CONTRAVENING_IMP_FULLY_SURROUNDED = prove(`!V. FAN (vec 0,V,ESTD V) /\ contravening V
\r
267 ==> fully_surrounded (V,ESTD V)`,
\r
268 REPEAT STRIP_TAC THEN
\r
269 ASM_SIMP_TAC[FULLY_SURROUNDED] THEN
\r
270 REPEAT STRIP_TAC THEN
\r
271 ASM_SIMP_TAC[CONTRAVENING_IMP_SURROUNDED]);;
\r
275 (* LEMMA: general *)
\r
276 let CONTRAVENING_IMP_IN_DART1_OF_FAN = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
\r
277 ==> x IN dart1_of_fan (V,ESTD V)`,
\r
278 REPEAT GEN_TAC THEN
\r
279 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
\r
280 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
281 REPEAT STRIP_TAC THEN
\r
282 ASSUME_TAC (SPEC `V:real^3->bool` CONTRAVENING_FAN) THEN
\r
283 MATCH_MP_TAC SURROUNDED_IMP_IN_DART1_OF_FAN THEN
\r
284 ASM_SIMP_TAC[] THEN
\r
285 MATCH_MP_TAC CONTRAVENING_IMP_SURROUNDED THEN
\r
286 ASM_REWRITE_TAC[] THEN
\r
287 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x':real^3`; `y:real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
291 (* LEMMA: general *)
\r
292 let CONTRAVENING_IMP_DART_FST_NEQ_SND = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
\r
293 ==> ~(FST x = SND x)`,
\r
294 REPEAT STRIP_TAC THEN
\r
295 POP_ASSUM MP_TAC THEN
\r
296 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
297 MP_TAC (SPEC_ALL CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN
\r
298 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
299 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART1_OF_FAN) THEN
\r
300 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
\r
301 ASM_REWRITE_TAC[] THEN
\r
302 MATCH_MP_TAC PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ THEN
\r
303 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `ESTD V`] THEN
\r
304 ASM_REWRITE_TAC[]);;
\r
309 (* LEMMA: general *)
\r
310 let CONTRAVENING_DIST = prove(`!V v. contravening V /\ v IN V
\r
311 ==> #2.0 <= dist(vec 0, v) /\ dist(vec 0,v) <= #2.52
\r
312 /\ (!w. w IN V /\ ~(v = w) ==> #2.0 <= dist(v, w))`,
\r
313 REPEAT GEN_TAC THEN
\r
314 REWRITE_TAC[contravening] THEN
\r
315 DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
\r
316 DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (MP_TAC o CONJUNCT1)) THEN
\r
317 REWRITE_TAC[Pack_defs.ball_annulus; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
\r
318 REWRITE_TAC[SUBSET; IN_DIFF; cball; ball; IN_ELIM_THM; REAL_NOT_LT] THEN
\r
319 DISCH_THEN (MP_TAC o SPEC `v:real^3`) THEN
\r
320 ASM_SIMP_TAC[REAL_ARITH `&2 = #2.0`] THEN
\r
321 DISCH_THEN (fun th -> ALL_TAC) THEN
\r
322 REWRITE_TAC[Sphere.packing; REAL_ARITH `#2.0 = &2`] THEN
\r
327 let IN_ESTD = prove(`!V v w. {v,w} IN ESTD V <=> v IN V /\ w IN V /\ ~(v = w) /\ dist(v,w) <= #2.52`,
\r
328 REPEAT GEN_TAC THEN
\r
329 REWRITE_TAC[ESTD; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
\r
332 REWRITE_TAC[IN_ELIM_THM] THEN
\r
334 SUBGOAL_THEN `(v:real^3 = v' /\ w:real^3 = w') \/ (v = w' /\ w = v')` MP_TAC THENL
\r
336 POP_ASSUM MP_TAC THEN SET_TAC[];
\r
339 ASM_MESON_TAC[DIST_SYM];
\r
344 (* LEMMA: general *)
\r
345 let CONTRAVENING_ESTD_DIST = prove(`!V v w. contravening V /\ v IN V /\ w IN V /\ {v,w} IN ESTD V
\r
346 ==> #2.0 <= dist(v,w) /\ dist(v,w) <= #2.52`,
\r
347 REPEAT GEN_TAC THEN
\r
348 REWRITE_TAC[contravening; IN_ESTD; Sphere.packing] THEN
\r
349 DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
\r
350 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
\r
351 ASM_REWRITE_TAC[REAL_ARITH `#2.0 = &2`] THEN
\r
356 (* LEMMA: general *)
\r
357 let CONTRAVENING_DART_DIST = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
\r
358 ==> #2.0 <= dist x /\ dist x <= #2.52`,
\r
359 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
360 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
361 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN
\r
362 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
363 MATCH_MP_TAC CONTRAVENING_ESTD_DIST THEN
\r
364 EXISTS_TAC `V:real^3->bool` THEN
\r
365 ASM_REWRITE_TAC[] THEN
\r
366 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN
\r
367 MP_TAC (SPEC_ALL CONTRAVENING_IMP_SURROUNDED) THEN
\r
368 ASM_REWRITE_TAC[] THEN
\r
369 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
370 REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
\r
372 ASM_REWRITE_TAC[]);;
\r
377 (* LEMMA: general *)
\r
378 let CONTRAVENING_LMFUN_BOUND = prove(`!V v. contravening V /\ v IN V
\r
379 ==> lmfun (norm v / &2) <= &1`,
\r
380 REPEAT GEN_TAC THEN
\r
381 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP CONTRAVENING_DIST th)) THEN
\r
382 REWRITE_TAC[DIST_SYM] THEN
\r
383 REWRITE_TAC[dist; VECTOR_SUB_RZERO; Pack_defs.lmfun; Pack_defs.h0] THEN
\r
391 let CONTRAVENING_IMP_AZIM_DART_EQ_AZIM = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
\r
392 ==> azim_dart (V,ESTD V) (v,w) = azim (vec 0) v w (sigma_fan (vec 0) V (ESTD V) v w)`,
\r
393 REPEAT STRIP_TAC THEN
\r
394 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
395 MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_DART_FST_NEQ_SND) THEN
\r
396 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`] SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3) THEN
\r
397 MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_IMP_SURROUNDED) THEN
\r
398 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
399 ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
\r
400 ASM_SIMP_TAC[azim_dart; azim_fan; ARITH_RULE `a >= 3 ==> a > 1`]);;
\r
405 (* 0, v, w, and sigma(v)(w) are not coplanar *)
\r
406 let CONTRAVENING_IMP_NOT_COPLANAR = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
\r
407 ==> ~coplanar {vec 0, v, w, sigma_fan (vec 0) V (ESTD V) v w}`,
\r
408 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
409 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
410 MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN
\r
411 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
412 MP_TAC (SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `sigma_fan (vec 0) V (ESTD V) v w`] AZIM_EQ_0_PI_EQ_COPLANAR) THEN
\r
415 MATCH_MP_TAC DART1_NOT_COLLINEAR_2 THEN
\r
419 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
\r
420 REWRITE_TAC[DE_MORGAN_THM] THEN
\r
421 ASM_SIMP_TAC[GSYM CONTRAVENING_IMP_AZIM_DART_EQ_AZIM] THEN
\r
424 MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
\r
425 MATCH_MP_TAC AZIM_DART_POS THEN
\r
427 MATCH_MP_TAC (REAL_ARITH `a < pi ==> ~(a = pi)`) THEN
\r
428 MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
\r
429 ASM_REWRITE_TAC[fully_surrounded] THEN
\r
430 DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
\r
438 (* azim_dart = dih_y *)
\r
439 let CONTRAVENING_AZIM_DART_EQ_DIH_Y = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
\r
440 ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
\r
443 let y3 = norm w' in
\r
444 let y4 = dist (w,w') in
\r
445 let y5 = dist (v,w') in
\r
446 let y6 = dist (v,w) in
\r
447 azim_dart (V,ESTD V) (v,w) = dih_y y1 y2 y3 y4 y5 y6`,
\r
448 REPEAT STRIP_TAC THEN REPEAT (CONV_TAC let_CONV) THEN
\r
449 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
450 ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
\r
451 MP_TAC (SPEC_ALL CONTRAVENING_IMP_AZIM_DART_EQ_AZIM) THEN
\r
452 MP_TAC (SPEC_ALL CONTRAVENING_IMP_NOT_COPLANAR) THEN
\r
453 ASM_REWRITE_TAC[] THEN
\r
454 REPEAT STRIP_TAC THEN
\r
456 SUBGOAL_THEN `~collinear {vec 0, v, w:real^3} /\ ~collinear {vec 0, v, w'}` ASSUME_TAC THENL
\r
458 CONJ_TAC THEN MATCH_MP_TAC NOT_COPLANAR_NOT_COLLINEAR THENL
\r
460 EXISTS_TAC `w':real^3` THEN ASM_REWRITE_TAC[];
\r
461 EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[SET_RULE `{a:real^3,b,c,d} = {a,b,d,c}`]
\r
466 MP_TAC ((let_RULE o SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `w':real^3`]) DIHV_EQ_DIH_Y) THEN
\r
467 ASM_REWRITE_TAC[DIST_0] THEN
\r
468 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
\r
469 MATCH_MP_TAC AZIM_DIHV_SAME THEN
\r
470 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
\r
471 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
472 MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
\r
473 ASM_REWRITE_TAC[fully_surrounded] THEN
\r
474 DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
\r
480 (* Lower bound for CARD(face) in a contravening packing *)
\r
481 let CONTRAVENING_IMP_CARD_FACE_GE_3 = prove(`!V. contravening V
\r
482 ==> (!x. x IN dart_of_fan (V,ESTD V) ==> CARD (face (hypermap_of_fan (V,ESTD V)) x) >= 3)`,
\r
483 MESON_TAC[CONTRAVENING_FAN; FULLY_SURROUNDED_IMP_CARD_FACE_GE_3; CONTRAVENING_IMP_FULLY_SURROUNDED]);;
\r
487 (* Alternative form for type_of_node H x *)
\r
488 let NODE_TYPE_lemma = prove(`!H (x:A). simple_hypermap H /\ x IN dart H
\r
489 ==> type_of_node H x = CARD {y | y IN node H x /\ CARD (face H y) = 3},
\r
490 CARD {y | y IN node H x /\ CARD (face H y) = 4},
\r
491 CARD {y | y IN node H x /\ CARD (face H y) >= 5}`,
\r
492 REPEAT GEN_TAC THEN
\r
493 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP SIMPLE_HYPERMAP_lemma th)) THEN
\r
494 REWRITE_TAC[type_of_node] THEN
\r
495 REWRITE_TAC[set_of_triangles_meeting_node; set_of_quadrilaterals_meeting_node; set_of_exceptional_meeting_node] THEN
\r
496 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
\r
499 (* CARD (node) = p + q + r *)
\r
500 let FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE =
\r
501 prove(`!V E x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
502 fully_surrounded (V,E) /\ x IN dart_of_fan (V,E)
\r
503 ==> (let p,q,r = type_of_node (hypermap_of_fan (V,E)) x in
\r
504 CARD (node (hypermap_of_fan (V,E)) x) = p + q + r)`,
\r
505 REPEAT STRIP_TAC THEN
\r
506 MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN
\r
507 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
\r
508 DISCH_THEN (fun th -> ALL_TAC) THEN
\r
509 CONV_TAC let_CONV THEN
\r
510 ABBREV_TAC `H = hypermap_of_fan (V:real^3->bool,E)` THEN
\r
511 ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
\r
512 ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN
\r
513 ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN
\r
514 MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN
\r
515 ASM_REWRITE_TAC[] THEN
\r
516 DISCH_THEN (MP_TAC o let_RULE) THEN
\r
517 ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
\r
518 ASM_REWRITE_TAC[] THEN
\r
521 SUBGOAL_THEN `CARD (B:real^3#real^3->bool) + CARD (C:real^3#real^3->bool) = CARD (D:real^3#real^3->bool)` MP_TAC THENL
\r
523 MATCH_MP_TAC CARD_UNION_EQ THEN
\r
524 ASM_SIMP_TAC[GSYM DISJOINT];
\r
528 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
529 MATCH_MP_TAC EQ_SYM THEN
\r
530 MATCH_MP_TAC CARD_UNION_EQ THEN
\r
531 ASM_SIMP_TAC[Hypermap.NODE_FINITE; GSYM DISJOINT]);;
\r
535 (******************************************************************************)
\r
538 (* tauVEF = taum for a triangular face *)
\r
539 let tauVEF_EQ_taum = prove(`!V f. contravening V /\
\r
540 f IN face_set_of_fan (V,ESTD V) /\
\r
542 ==> (!v w. (v,w) IN f ==>
\r
543 let w' = sigma_fan (vec 0) V (ESTD V) v w in
\r
546 let y3 = norm w' in
\r
547 let y4 = dist(w,w') in
\r
548 let y5 = dist(v,w') in
\r
549 let y6 = dist(v,w) in
\r
550 tauVEF (V,ESTD V,f) = taum y1 y2 y3 y4 y5 y6)`,
\r
551 REPEAT STRIP_TAC THEN
\r
552 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
553 UNDISCH_TAC `f IN face_set_of_fan (V,ESTD V)` THEN
\r
554 REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN
\r
555 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
\r
557 SUBGOAL_THEN `face (hypermap_of_fan (V,ESTD V)) (v,w) = f` MP_TAC THENL
\r
559 ASM_REWRITE_TAC[] THEN
\r
560 MATCH_MP_TAC (GSYM Hypermap.lemma_face_identity) THEN
\r
561 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
\r
564 SUBGOAL_THEN `(v,w) IN dart1_of_fan (V,ESTD V)` MP_TAC THENL
\r
566 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
567 EXISTS_TAC `f:real^3#real^3->bool` THEN
\r
568 ASM_REWRITE_TAC[] THEN
\r
569 MATCH_MP_TAC FACE_SUBSET_DART1_OF_FAN THEN
\r
570 ASM_SIMP_TAC[CONTRAVENING_IMP_IN_DART1_OF_FAN];
\r
573 REMOVE_ASSUM THEN REMOVE_ASSUM THEN
\r
574 REPEAT DISCH_TAC THEN
\r
575 REPEAT (CONV_TAC let_CONV) THEN
\r
576 ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
\r
577 REWRITE_TAC[tauVEF] THEN
\r
578 MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE)) THEN
\r
579 ASM_REWRITE_TAC[] THEN
\r
581 SUBGOAL_THEN `(w,w') IN dart1_of_fan (V,ESTD V) /\ w',v IN dart1_of_fan (V,ESTD V)` ASSUME_TAC THENL
\r
583 CONJ_TAC THEN MATCH_MP_TAC IN_FACE_IMP_IN_DART1_OF_FAN THEN EXISTS_TAC `v:real^3,w:real^3` THEN ASM_REWRITE_TAC[IN_INSERT];
\r
587 ASM_REWRITE_TAC[] THEN
\r
588 ASM_SIMP_TAC[Hypermap.FINITE_TWO_ELEMENTS; Hypermap.FINITE_SINGLETON; SUM_CLAUSES; SUM_SING] THEN
\r
589 SUBGOAL_THEN `~(v,w IN {(w,w'), (w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL
\r
591 REWRITE_TAC[IN_INSERT; PAIR_EQ; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
\r
592 MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
\r
596 SUBGOAL_THEN `~(w,w' IN {(w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL
\r
598 REWRITE_TAC[IN_SING; PAIR_EQ] THEN
\r
599 MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
\r
603 REWRITE_TAC[sol0_over_pi_EQ_const1] THEN
\r
604 ABBREV_TAC `a1 = azim_dart (V,ESTD V) (v,w)` THEN
\r
605 ABBREV_TAC `a2 = azim_dart (V,ESTD V) (w,w')` THEN
\r
606 ABBREV_TAC `a3 = azim_dart (V,ESTD V) (w',v)` THEN
\r
607 ABBREV_TAC `l1 = lmfun (h_dart (v:real^3,w:real^3))` THEN
\r
608 ABBREV_TAC `l2 = lmfun (h_dart (w:real^3,w':real^3))` THEN
\r
609 ABBREV_TAC `l3 = lmfun (h_dart (w':real^3,v:real^3))` THEN
\r
610 SUBGOAL_THEN `(pi + sol0) = pi * (&1 + const1)` (fun th -> REWRITE_TAC[th]) THENL
\r
612 MP_TAC sol0_over_pi_EQ_const1 THEN
\r
614 CONV_TAC REAL_FIELD;
\r
618 REWRITE_TAC[Sphere.taum; Sphere.sol_y; Sphere.lnazim] THEN
\r
619 SUBGOAL_THEN `v,w IN dart_of_fan (V,ESTD V) /\ w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
\r
621 REPEAT CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN EXISTS_TAC `dart1_of_fan (V,ESTD V)` THEN ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
\r
625 MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `v:real^3`; `w:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
\r
626 MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w:real^3`; `w':real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
\r
627 MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w':real^3`; `v:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
\r
628 ASM_REWRITE_TAC[DIST_SYM] THEN
\r
629 REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[SYM th])) THEN
\r
631 MP_TAC (SPEC `v:real^3,w:real^3` ly_EQ_lmfun) THEN
\r
632 MP_TAC (SPEC `w:real^3,w':real^3` ly_EQ_lmfun) THEN
\r
633 MP_TAC (SPEC `w':real^3,v:real^3` ly_EQ_lmfun) THEN
\r
635 MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN
\r
636 MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN
\r
637 MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN
\r
639 ASM_REWRITE_TAC[] THEN
\r
640 SUBGOAL_THEN `w' IN V /\ w IN V /\ v IN (V:real^3->bool)` (fun th -> REWRITE_TAC[th]) THENL
\r
642 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
643 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
644 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w':real^3`; `v:real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
648 SIMP_TAC[DIST_0; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
\r
649 REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
\r
653 let CONTRAVENING_TAUVEF_EQ_TAUM = prove(`!V v w. contravening V /\
\r
654 (v,w) IN dart_of_fan (V,ESTD V) /\
\r
655 CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3
\r
656 ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
\r
659 let y3 = norm w' in
\r
660 let y4 = dist(w,w') in
\r
661 let y5 = dist(v,w') in
\r
662 let y6 = dist(v,w) in
\r
663 tauVEF (V,ESTD V,face (hypermap_of_fan (V,ESTD V)) (v,w)) = taum y1 y2 y3 y4 y5 y6`,
\r
664 REPEAT STRIP_TAC THEN
\r
665 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
666 MP_TAC (SPECL [`V:real^3->bool`; `face (hypermap_of_fan (V,ESTD V)) (v,w)`] tauVEF_EQ_taum) THEN
\r
669 ASM_REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
\r
670 REWRITE_TAC[IN_ELIM_THM] THEN
\r
671 EXISTS_TAC `v:real^3,w:real^3` THEN
\r
672 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN];
\r
675 DISCH_THEN MATCH_MP_TAC THEN
\r
676 REWRITE_TAC[Hypermap.face_refl]);;
\r
679 (* Bounds for distances in a triangular face *)
\r
681 let CONTRAVENING_TRIANGULAR_FACE_DIST = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V) /\
\r
682 CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3
\r
683 ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
\r
686 let y3 = norm w' in
\r
687 let y4 = dist(w,w') in
\r
688 let y5 = dist(v,w') in
\r
689 let y6 = dist(v,w) in
\r
690 (&2 <= y1 /\ y1 <= #2.52) /\
\r
691 (&2 <= y2 /\ y2 <= #2.52) /\
\r
692 (&2 <= y3 /\ y3 <= #2.52) /\
\r
693 (&2 <= y4 /\ y4 <= #2.52) /\
\r
694 (&2 <= y5 /\ y5 <= #2.52) /\
\r
695 (&2 <= y6 /\ y6 <= #2.52)`,
\r
696 REPEAT STRIP_TAC THEN CONV_TAC (DEPTH_CONV let_CONV) THEN
\r
697 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
698 ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
\r
699 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE) THEN
\r
700 ASM_REWRITE_TAC[] THEN
\r
703 MATCH_MP_TAC CONTRAVENING_IMP_IN_DART1_OF_FAN THEN
\r
707 CONV_TAC (DEPTH_CONV let_CONV) THEN
\r
708 DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
\r
709 SUBGOAL_THEN `w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
\r
711 CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
712 EXISTS_TAC `face (hypermap_of_fan (V,ESTD V)) (v,w)` THEN
\r
713 ASM_SIMP_TAC[FACE_SUBSET_DART_OF_FAN; IN_INSERT];
\r
716 SUBGOAL_THEN `v IN V /\ w IN V /\ w' IN (V:real^3->bool)` ASSUME_TAC THENL
\r
718 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
719 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN
\r
723 REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN
\r
724 MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN
\r
725 MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN
\r
726 MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN
\r
727 ASM_REWRITE_TAC[DIST_0] THEN
\r
728 REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[th])) THEN
\r
729 MAP_EVERY (fun tm -> MP_TAC (SPECL [`V:real^3->bool`; tm] CONTRAVENING_DART_DIST)) [`v:real^3,w:real^3`; `w:real^3,w':real^3`; `w':real^3,v:real^3`] THEN
\r
730 ASM_SIMP_TAC[DIST_SYM]);;
\r
733 (* Bounds for azim_dart in a triangular face *)
\r
735 let azim_dart_bounds_3_list = map (fun id -> (hd (Ineq.getexact id)).ineq) ["5735387903"; "5490182221"];;
\r
737 let azim_dart_bounds_3 = list_mk_conj azim_dart_bounds_3_list;;
\r
739 let TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl = mk_imp (azim_dart_bounds_3,
\r
740 `!V x. contravening V /\
\r
741 x IN dart_of_fan (V,ESTD V) /\
\r
742 CARD (face (hypermap_of_fan (V,ESTD V)) x) = 3
\r
743 ==> #0.852 < azim_dart (V,ESTD V) x /\ azim_dart (V,ESTD V) x < #1.893`);;
\r
745 (* g(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl);; *)
\r
746 let TRIANGULAR_FACE_AZIM_DART_BOUNDS = prove(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl,
\r
747 REWRITE_TAC[Ineq.dart_std3; INEQ_ALT; ALL; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
\r
750 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
751 POP_ASSUM MP_TAC THEN
\r
752 MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
754 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN
\r
755 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
756 MP_TAC (SPEC_ALL CONTRAVENING_AZIM_DART_EQ_DIH_Y) THEN
\r
757 ASM_REWRITE_TAC[] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN
\r
758 ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
\r
759 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
761 MP_TAC (SPEC_ALL CONTRAVENING_TRIANGULAR_FACE_DIST) THEN
\r
762 ASM_REWRITE_TAC[] THEN
\r
763 CONV_TAC (DEPTH_CONV let_CONV) THEN
\r
764 REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN
\r
769 REWRITE_TAC[GSYM real_gt] THEN
\r
770 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
772 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
778 (******************************************************************************)
\r
780 (* Properties of rho_node (might be useful) *)
\r
782 let RHO_NODE_lemma = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
783 f IN face_set (hypermap_of_fan (V,E)) /\ x IN f
\r
784 ==> ?!w. (FST x,w) IN f`,
\r
785 REPEAT STRIP_TAC THEN
\r
786 REWRITE_TAC[EXISTS_UNIQUE] THEN
\r
787 EXISTS_TAC `SND (x:real^3#real^3)` THEN
\r
788 ASM_REWRITE_TAC[PAIR] THEN
\r
789 REPEAT STRIP_TAC THEN
\r
790 MP_TAC (INST [`FST (x:real^3#real^3),y:real^3`, `y:real^3#real^3`] (SPEC_ALL HYPERMAP_OF_FAN_FACE_NODE_INJ)) THEN
\r
791 ASM_REWRITE_TAC[] THEN
\r
792 ONCE_REWRITE_TAC[GSYM PAIR] THEN
\r
793 REWRITE_TAC[PAIR_EQ; EQ_SYM_EQ]);;
\r
798 let RHO_NODE_LEMMA = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
799 f IN face_set (hypermap_of_fan (V,E)) /\ x IN f
\r
800 ==> rho_node (V,E,f) (FST x) = SND x`,
\r
801 REPEAT GEN_TAC THEN
\r
803 MP_TAC (SPEC_ALL RHO_NODE_lemma) THEN ASM_REWRITE_TAC[EXISTS_UNIQUE] THEN
\r
805 SUBGOAL_THEN `w = SND (x:real^3#real^3)` ASSUME_TAC THENL
\r
807 MATCH_MP_TAC EQ_SYM THEN
\r
808 POP_ASSUM (fun th -> MATCH_MP_TAC th) THEN
\r
809 ASM_REWRITE_TAC[PAIR];
\r
812 REWRITE_TAC[rho_node] THEN
\r
813 MATCH_MP_TAC SELECT_UNIQUE THEN
\r
814 GEN_TAC THEN BETA_TAC THEN
\r
818 FIRST_X_ASSUM (MP_TAC o SPEC `y:real^3`) THEN
\r
820 DISCH_THEN (fun th -> ASM_REWRITE_TAC[th])
\r
826 let RHO_NODE_EQ_FACE_MAP = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
827 x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
\r
828 ==> f_fan_pair_ext (V,E) x = (rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x))`,
\r
829 REPEAT STRIP_TAC THEN
\r
830 REWRITE_TAC[Hypermap.POWER_2; o_THM] THEN
\r
831 ABBREV_TAC `w = rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST (x:real^3#real^3))` THEN
\r
832 MATCH_MP_TAC HYPERMAP_OF_FAN_FACE_NODE_INJ THEN
\r
833 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`; `f:real^3#real^3->bool`] THEN
\r
834 ASM_REWRITE_TAC[] THEN
\r
836 SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
\r
838 ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
\r
839 REWRITE_TAC[IN_ELIM_THM] THEN
\r
840 EXISTS_TAC `x:real^3#real^3` THEN
\r
842 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
843 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
\r
844 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
\r
845 REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
\r
848 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
850 SUBGOAL_THEN `f_fan_pair_ext (V,E) x IN f` MP_TAC THENL
\r
852 ASM_REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
\r
853 ASM_SIMP_TAC[HYPERMAP_OF_FAN; Hypermap.in_orbit_map1];
\r
856 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
860 REWRITE_TAC[rho_node] THEN
\r
861 MATCH_MP_TAC (BETA_RULE (ISPECL [`(\w':real^3. (w:real^3,w') IN face (hypermap_of_fan (V,E)) x)`] SELECT_AX)) THEN
\r
862 POP_ASSUM MP_TAC THEN
\r
863 MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
\r
864 ASM_REWRITE_TAC[Hypermap.face_refl] THEN
\r
865 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
\r
866 STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair] THEN
\r
867 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
869 EXISTS_TAC `inverse_sigma_fan (vec 0) V E y x'` THEN
\r
874 MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
\r
875 ASM_REWRITE_TAC[Hypermap.face_refl] THEN
\r
876 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
877 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
\r
878 STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair]);;
\r
882 let RHO_NODE_POWER_EQ_FACE_MAP_POWER = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
883 x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
\r
884 ==> !i. (f_fan_pair_ext (V,E) POWER i) x =
\r
885 ((\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) POWER i) x`,
\r
886 REPEAT STRIP_TAC THEN
\r
887 ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN
\r
888 SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
\r
890 ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
\r
891 REWRITE_TAC[IN_ELIM_THM] THEN
\r
892 EXISTS_TAC `x:real^3#real^3` THEN
\r
894 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
895 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
\r
896 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
\r
897 REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
\r
900 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
902 SPEC_TAC (`i:num`,`i:num`) THEN
\r
905 REWRITE_TAC[Hypermap.POWER];
\r
909 REWRITE_TAC[ARITH_RULE `SUC i = 1 + i`; Hypermap.addition_exponents; Hypermap.POWER_1; o_THM] THEN
\r
910 ABBREV_TAC `y = (f_fan_pair_ext (V,E) POWER i) x` THEN
\r
911 MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `y:real^3#real^3`; `f:real^3#real^3->bool`] RHO_NODE_EQ_FACE_MAP) THEN
\r
912 FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (rator (concl th)) = `y:real^3#real^3`)) THEN
\r
913 ASM_REWRITE_TAC[] THEN
\r
915 SUBGOAL_THEN `y IN face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL
\r
917 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
918 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
\r
919 REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN
\r
920 EXISTS_TAC `i:num` THEN
\r
921 REWRITE_TAC[GE; LE_0];
\r
925 SUBGOAL_THEN `face (hypermap_of_fan (V,E)) x = face (hypermap_of_fan (V,E)) y` ASSUME_TAC THENL
\r
927 MATCH_MP_TAC Hypermap.lemma_face_identity THEN
\r
932 SUBGOAL_THEN `y IN dart1_of_fan (V:real^3->bool,E)` (fun th -> REWRITE_TAC[th]) THENL
\r
934 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
935 EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN
\r
936 ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];
\r
940 ASM_REWRITE_TAC[] THEN
\r
941 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
\r
942 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
943 EXPAND_TAC "g" THEN BETA_TAC THEN
\r
944 ASM_REWRITE_TAC[]);;
\r
950 let ORBIT_MAP_FUN_EQ_lemma = prove(`!(f:A->A) g x. (!y. y IN orbit_map f x ==> g y = f y)
\r
951 ==> orbit_map g x = orbit_map f x`,
\r
952 REPEAT STRIP_TAC THEN
\r
953 MATCH_MP_TAC Hypermap.lemma_orbit_eq THEN
\r
954 INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER] THEN
\r
955 REWRITE_TAC[GSYM Hypermap.POWER] THEN
\r
956 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
\r
957 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
958 REWRITE_TAC[Hypermap.lemma_in_orbit]);;
\r
963 let RHO_NODE_face = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
964 x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
\r
965 ==> f = orbit_map (\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) x`,
\r
966 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
967 SUBGOAL_THEN `orbit_map (f_fan_pair_ext (V,E)) x = face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL
\r
969 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN];
\r
972 FIRST_ASSUM (fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
\r
973 MATCH_MP_TAC EQ_SYM THEN
\r
974 MATCH_MP_TAC ORBIT_MAP_FUN_EQ_lemma THEN
\r
975 ASM_REWRITE_TAC[] THEN
\r
976 REPEAT STRIP_TAC THEN
\r
977 MATCH_MP_TAC EQ_SYM THEN BETA_TAC THEN
\r
978 MATCH_MP_TAC RHO_NODE_EQ_FACE_MAP THEN
\r
979 ASM_REWRITE_TAC[] THEN
\r
982 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
983 EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN
\r
984 ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];
\r
987 MATCH_MP_TAC Hypermap.lemma_face_identity THEN
\r
988 ASM_REWRITE_TAC[]);;
\r
992 let RHO_NODE_POWER = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
993 x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
\r
994 ==> !i. ((\x. rho_node (V,E,f) (FST x),(rho_node (V,E,f) POWER 2) (FST x)) POWER i) x
\r
995 = (\x. (rho_node (V,E,f) POWER i) (FST x), (rho_node (V,E,f) POWER (i + 1)) (FST x)) x`,
\r
996 REPEAT STRIP_TAC THEN
\r
997 SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
\r
999 ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
\r
1000 REWRITE_TAC[IN_ELIM_THM] THEN
\r
1001 EXISTS_TAC `x:real^3#real^3` THEN
\r
1002 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
\r
1003 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
\r
1004 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
\r
1005 ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
\r
1008 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
\r
1010 SPEC_TAC (`i:num`, `i:num`) THEN
\r
1011 INDUCT_TAC THEN BETA_TAC THENL
\r
1013 REWRITE_TAC[Hypermap.POWER; ARITH_RULE `0 + 1 = 1`; Hypermap.POWER_1; I_THM] THEN
\r
1014 MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
\r
1015 ASM_REWRITE_TAC[Hypermap.face_refl] THEN
\r
1016 DISCH_THEN (fun th -> REWRITE_TAC[th]);
\r
1020 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM; PAIR_EQ] THEN
\r
1021 REWRITE_TAC[ARITH_RULE `SUC i + 1 = 2 + i`] THEN
\r
1022 REWRITE_TAC[Hypermap.addition_exponents; o_THM]);;
\r
1026 (* Alternative definition of the perimeter of a face *)
\r
1028 let PERIMETER_lemma = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
\r
1029 x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
\r
1030 ==> per (V,E,f) (FST x) (CARD f) = sum f (\(v,w). arcV (vec 0) v w)`,
\r
1031 REPEAT STRIP_TAC THEN
\r
1032 REWRITE_TAC[per] THEN
\r
1033 ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN
\r
1034 ABBREV_TAC `orbit = orbit_map (f_fan_pair_ext (V,E)) x` THEN
\r
1036 SUBGOAL_THEN `0 < CARD (orbit:real^3#real^3->bool)` ASSUME_TAC THENL
\r
1038 SUBGOAL_THEN `FINITE (orbit:real^3#real^3->bool)` ASSUME_TAC THENL
\r
1040 EXPAND_TAC "orbit" THEN
\r
1041 MATCH_MP_TAC Hypermap.lemma_orbit_finite THEN
\r
1042 EXISTS_TAC `dart_of_fan (V,E)` THEN
\r
1043 ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN];
\r
1046 DISJ_CASES_TAC (ARITH_RULE `0 < CARD (orbit:real^3#real^3->bool) \/ CARD orbit = 0`) THEN ASM_REWRITE_TAC[] THEN
\r
1047 POP_ASSUM MP_TAC THEN
\r
1048 POP_ASSUM (MP_TAC o (MATCH_MP CARD_EQ_0)) THEN
\r
1049 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
1051 MP_TAC (ISPECL [`f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.orbit_reflect) THEN
\r
1052 ASM_REWRITE_TAC[NOT_IN_EMPTY];
\r
1056 SUBGOAL_THEN `!i. arcV (vec 0:real^3) ((rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) POWER i) (FST (x:real^3#real^3))) ((rho_node (V,E,f) POWER (i + 1)) (FST x)) = ((\(v,w). arcV (vec 0) v w) o (\i. (g POWER i) x)) i` MP_TAC THENL
\r
1058 REWRITE_TAC[LAMBDA_PAIR; o_THM] THEN BETA_TAC THEN
\r
1059 MP_TAC (SPEC_ALL RHO_NODE_POWER) THEN
\r
1060 ASM_REWRITE_TAC[] THEN
\r
1061 DISCH_THEN (fun th -> REWRITE_TAC[th]);
\r
1065 ASM_REWRITE_TAC[] THEN
\r
1066 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
1068 SUBGOAL_THEN `f:real^3#real^3->bool = IMAGE (\i. (g:real^3#real^3->real^3#real^3 POWER i) x) (0..CARD f - 1)` MP_TAC THENL
\r
1070 ASM_REWRITE_TAC[GSYM IMAGE_LEMMA; IN_NUMSEG; LE_0] THEN
\r
1071 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
\r
1072 MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`; `CARD (orbit_map (f_fan_pair_ext (V,E)) x)`] FINITE_ORBIT_MAP) THEN
\r
1073 ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
\r
1074 DISCH_THEN (fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
\r
1075 MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN
\r
1076 ASM_REWRITE_TAC[] THEN
\r
1077 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
1078 POP_ASSUM MP_TAC THEN
\r
1079 SIMP_TAC[ARITH_RULE `0 < c ==> !i. i < c <=> i <= c - 1`];
\r
1082 ASM_REWRITE_TAC[] THEN
\r
1083 DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
\r
1084 REWRITE_TAC[ETA_AX] THEN
\r
1086 MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
\r
1088 X_GEN_TAC `n:num` THEN X_GEN_TAC `m:num` THEN
\r
1089 REWRITE_TAC[IN_NUMSEG; LE_0] THEN
\r
1090 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
\r
1091 MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN
\r
1092 ASM_REWRITE_TAC[] THEN
\r
1093 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
\r
1096 SUBGOAL_THEN `inj_orbit (f_fan_pair_ext (V,E)) x (CARD (f:real^3#real^3->bool) - 1)` MP_TAC THENL
\r
1098 MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.lemma_segment_orbit) THEN
\r
1099 ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
\r
1100 DISCH_THEN (MP_TAC o SPEC `CARD (f:real^3#real^3->bool) - 1`) THEN
\r
1101 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
\r
1104 REPLICATE_TAC 3 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
\r
1111 REWRITE_TAC[Hypermap.lemma_inj_orbit] THEN
\r
1112 DISCH_THEN MATCH_MP_TAC THEN
\r
1113 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN]);;
\r