1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Chapter: Local Fan *)
\r
5 (* Author: Nguyen Quang Truong *)
\r
6 (* Date: 2010-05-09 *)
\r
7 (* ========================================================================== *)
\r
9 (* needs "/home/user1/flyspeck/working/flyspeck_needs.hl";; *)
\r
10 (* =========== snapshot 1631 ===================== *)
\r
12 flyspeck_needs "fan/planarity.hl";;
\r
13 flyspeck_needs "local/WRGCVDR_CIZMRRH.hl";;
\r
16 module type Lvducxu_type = sig
\r
21 module Lvducxu = struct
\r
23 parse_as_infix("has_orders",(12,"right"));;
\r
28 open Trigonometry1;;
\r
29 open Trigonometry2;;
\r
33 open Prove_by_refinement;;
\r
34 open Wrgcvdr_cizmrrh;;
\r
36 let PROPERTIES_OF_IVS_AZIM_CYCLE2 = IVS_AZIM_PROPERTIES;;
\r
40 let IN_FF_IMP_FST_SND_IN_V = prove_by_refinement
\r
41 (` UNIONS E SUBSET (V:A -> bool) /\ FF SUBSET darts_of_hyp E V
\r
42 /\ x IN FF ==> FST x IN V /\ SND x IN V `,
\r
43 [REWRITE_TAC[darts_of_hyp; SUBSET];
\r
47 REWRITE_TAC[ord_pairs; IN_UNION; self_pairs; IN_ELIM_THM];
\r
50 SUBGOAL_THEN` (a:A) IN UNIONS E /\ b IN UNIONS E ` ASSUME_TAC;
\r
51 REWRITE_TAC[IN_UNIONS];
\r
52 ASM_MESON_TAC[SET_RULE` a IN {a,b} /\ b IN {a,b} `];
\r
65 let W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE =
\r
66 prove_by_refinement(
\r
67 `(!(x:A). x IN W ==> W = orbit_map f x)
\r
68 ==> W = IMAGE f W `,
\r
70 REWRITE_TAC[FUN_EQ_THM];
\r
71 GEN_TAC THEN EQ_TAC;
\r
72 PAT_ONCE_REWRITE_TAC `\x. x ==> x ` [GSYM IN];
\r
74 NHANH CYCLIC_MAP_IMP_CIRCLE_ITSELF;
\r
75 REWRITE_TAC[IMAGE; IN_ELIM_THM];
\r
77 REWRITE_TAC[IMAGE; IN_ELIM_THM];
\r
79 ASSUME_TAC in_orbit_map1;
\r
80 DOWN THEN REWRITE_TAC[IN];
\r
91 let FINITE_AND_LOOP_IMP_BIJ_S_IM_S =
\r
92 prove_by_refinement(
\r
93 `! S:A -> bool. FINITE S /\ (! x. x IN S ==> S = orbit_map f x )
\r
94 ==> BIJ f S (IMAGE f S ) `,
\r
95 [NHANH W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE;
\r
96 REWRITE_TAC[BIJ; INJ; SURJ];
\r
97 REPEAT GEN_TAC THEN STRIP_TAC;
\r
98 REWRITE_TAC[FUN_IN_IMAGE; IN_IMAGE];
\r
99 SIMP_TAC[CONJ_SYM; EQ_SYM_EQ];
\r
100 ASM_MESON_TAC[IMAGE_IMP_INJECTIVE_GEN]]);;
\r
105 let CYCLIC_SET_IMP_SELF_LOPP2 = prove_by_refinement
\r
106 (`FAN (x,V,E) /\ {v, u} IN E
\r
107 ==> (!a. a IN EE v E
\r
108 ==> EE v E = orbit_map (azim_cycle (EE v E) x v) a)`,
\r
109 [NHANH CYCLIC_SET_IMP_STABLE_SET2;
\r
111 FIRST_X_ASSUM NHANH;
\r
113 ABBREV_TAC ` f = azim_cycle (EE v E) x v `;
\r
114 ASM_REWRITE_TAC[orbit_map; FUN_EQ_THM; IN_ELIM_THM; POWER_TO_ITER];
\r
115 REWRITE_TAC[ARITH_RULE` x >= 0 `]]);;
\r
118 let FIN_LOOP_IMP_BIJ_ITSELF = prove_by_refinement(
\r
119 `! S: A -> bool. FINITE S /\ (! x. x IN S ==> S = orbit_map f x )
\r
121 [NHANH FINITE_AND_LOOP_IMP_BIJ_S_IM_S;
\r
122 NHANH W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE;
\r
129 (* +++++++++++++++++++++++++++
\r
130 let CYCLIC_SET_IMP_BIJ_AZIM_CYCLE =
\r
131 prove_by_refinement(` cyclic_set W v w ==>
\r
132 BIJ (azim_cycle W v w) W W `,
\r
133 [NHANH CYCLIC_SET_IMP_SELF_LOPP;
\r
134 REWRITE_TAC[cyclic_set];
\r
137 UNDISCH_TAC `FINITE (W:real^3 -> bool) `;
\r
139 NHANH FIN_LOOP_IMP_BIJ_ITSELF;
\r
142 +++++++++++++++++++++++++++++++ *)
\r
144 (* a very important lemma for proving
\r
145 second lemma in local fan chapter *)
\r
146 (* ================================== *)
\r
151 let IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME = prove_by_refinement
\r
152 (` (x:A#A) IN darts_of_hyp E V /\ x IN FF ==>
\r
153 x IN darts_of_hyp (e_prime E FF) (v_prime V FF) `,
\r
154 [REWRITE_TAC[IN_ELIM_THM; darts_of_hyp; IN_UNION; ord_pairs; self_pairs];
\r
155 REWRITE_TAC[e_prime; v_prime; IN_ELIM_THM];
\r
164 DOWN_TAC THEN REWRITE_TAC[EE];
\r
171 let PROPERTIES_OF_IVS_AZIM_CYCLE2 =
\r
172 prove_by_refinement(` FAN (x,V,E) /\ w IN EE v E ==>
\r
173 ivs_azim_cycle (EE v E) x v w IN EE v E /\
\r
174 azim_cycle (EE v E ) x v ( ivs_azim_cycle (EE v E) x v w ) = w `,
\r
176 NHANH FAN_IMP_EE_EQ_SET_OF_EDGE;
\r
178 UNDISCH_TAC` FAN ((x:real^3),V,E) `;
\r
181 NHANH IVS_AZIM_PROPERTIES;
\r
184 UNDISCH_TAC `ivs_azim_cycle (set_of_edge v V E) x v w IN
\r
185 set_of_edge v V E `;
\r
186 UNDISCH_TAC ` FAN (x:real^3,V,E) `;
\r
188 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;
\r
193 let IN_EE_IFF_IN_E = prove(` x IN EE v E <=> {v,x} IN E `,
\r
194 REWRITE_TAC[EE; IN_ELIM_THM]);;
\r
197 let CYCLIC_SET_IMP_SELF_LOPP3 = prove(`FAN (x,V,E)
\r
198 ==> (!a. a IN EE v E
\r
199 ==> EE v E = orbit_map (azim_cycle (EE v E) x v) a)`,
\r
200 MESON_TAC[CYCLIC_SET_IMP_SELF_LOPP2;IN_EE_IFF_IN_E]);;
\r
204 let BIJ_AZIM_CYCLE_EE = prove(
\r
205 ` FAN (x,V,E) ==> BIJ (azim_cycle (EE v E) x v) (EE v E) (EE v E) `,
\r
206 NHANH CYCLIC_SET_IMP_SELF_LOPP3 THEN
\r
207 NHANH FAN_IMP_FINITE_EE THEN
\r
208 MESON_TAC[FIN_LOOP_IMP_BIJ_ITSELF]);;
\r
216 (* ++++++++++++++++++ *)
\r
220 let IN_FF_FACE_MAP_IDE = prove_by_refinement
\r
222 (?x. x IN dart (hypermap (HYP (v,V,E))) /\
\r
223 FF = face (hypermap (HYP (v,V,E))) x)
\r
224 ==> (! x. x IN FF ==> face_map (hypermap (HYP (v,V,E))) x =
\r
225 face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x ) `,
\r
226 [NHANH IMP_FAN_V_PRIME_E_PRIME;
\r
227 NHANH ELMS_OF_HYPERMAP_HYP;
\r
229 STRIP_TAC THEN STRIP_TAC;
\r
230 UNDISCH_TAC`FF = face (hypermap (HYP (v,V,E))) x`;
\r
231 DISCH_THEN (ASSUME_TAC o SYM);
\r
232 ASM_REWRITE_TAC[ff_of_hyp];
\r
233 PAT_ONCE_REWRITE_TAC `\x. P x = Q x ` [GSYM PAIR];
\r
236 SUBGOAL_THEN `x IN dart (hypermap (HYP ((v:real^3),V,E))) ` MP_TAC;
\r
238 NHANH lemma_face_subset;
\r
241 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;
\r
242 DOWN THEN DOWN THEN DOWN THEN SET_TAC[];
\r
243 SUBGOAL_THEN ` x':real^3 # real^3 IN
\r
244 darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;
\r
245 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;
\r
246 DOWN THEN DOWN THEN DOWN THEN SET_TAC[];
\r
247 ASM_SIMP_TAC[IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME];
\r
249 SIMP_TAC[ff_of_hyp2];
\r
250 REMOVE_TAC THEN DOWN THEN REMOVE_TAC;
\r
254 REWRITE_TAC[ff_of_hyp];
\r
255 UNDISCH_TAC `(x': real^3 #real^3 ) IN FF `;
\r
258 NHANH IN_ORBIT_MAP_IMP_F_Y;
\r
259 REWRITE_TAC[GSYM face];
\r
263 IMP_TAC THEN DISCH_TAC;
\r
266 SUBGOAL_THEN `x IN dart (hypermap (HYP ((v:real^3),V,E))) ` MP_TAC;
\r
268 NHANH lemma_face_subset;
\r
271 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;
\r
272 DOWN THEN DOWN THEN SET_TAC[];
\r
273 SIMP_TAC[ff_of_hyp2];
\r
275 DOWN THEN REMOVE_TAC;
\r
279 IMP_TAC THEN DISCH_TAC;
\r
280 PAT_ONCE_REWRITE_TAC `\x. P h x IN FF ==> y `
\r
281 [ISPEC `x': real^3 # real^3 ` (GSYM PAIR)];
\r
284 ABBREV_TAC ` fx = FST (x':real^3 # real^3 ) `;
\r
285 ABBREV_TAC `snx = SND (x':real^3 # real^3 ) `;
\r
286 MP_TAC (ISPEC `x': real^3 # real^3 ` (GSYM PAIR));
\r
290 UNDISCH_TAC `x IN dart (hypermap (HYP (v,V,E))) `;
\r
291 NHANH lemma_face_subset;
\r
293 UNDISCH_TAC` (x':real^3#real^3) IN FF `;
\r
297 NHANH (SET_RULE` a SUBSET b /\ x IN a /\ l ==> x IN b `);
\r
300 REWRITE_TAC[darts_of_hyp; IN_UNION];
\r
301 ONCE_REWRITE_TAC[DISJ_SYM];
\r
303 (* 2 goals araise here *)
\r
306 REWRITE_TAC[self_pairs];
\r
307 UNDISCH_TAC `(x':real^3 # real^3) = FST x',SND x'`;
\r
309 FIRST_X_ASSUM (fun x -> ONCE_REWRITE_TAC[x]);
\r
310 PURE_REWRITE_TAC[IN_ELIM_THM; BETA_THM; PAIR_EQ];
\r
314 ASSUME_TAC (let tm =
\r
315 MATCH_MP (SPECL [`{}:real^3 -> bool `;` v:real^3 `;` v':real^3 `] (GEN_ALL (MESON[W_SUBSET_SINGLETON_IMP_IDE]` W SUBSET {p} ==> azim_cycle W v w p = p`))) (SET_RULE` {} SUBSET {(q:real^3)} `) in
\r
316 GEN `q:real^3 ` tm);
\r
320 ISPECL [`FF:real^3 # real^3 -> bool `] (GEN_ALL E_PRIME_SUBSET_E));
\r
324 GEN_ALL SUBSET_IMP_SO_DO_EE in
\r
325 ISPECL [`W1:(A -> bool ) -> bool`;`v':A `] ge);
\r
326 ASM_SIMP_TAC[SUBSET_EMPTY];
\r
328 REWRITE_TAC[PAIR_EQ];
\r
329 DOWN_TAC THEN NHANH (
\r
330 MESON[FAN]` FAN (x,V,E) ==> UNIONS E SUBSET V `);
\r
333 ISPEC `x': real^3 # real ^3 ` (GEN `x:A#A` IN_FF_IMP_FST_SND_IN_V));
\r
334 DOWN THEN ASM_SIMP_TAC[];
\r
336 SUBGOAL_THEN` snx:real^3 IN v_prime V (FF:real^3 # real^3 -> bool)` ASSUME_TAC;
\r
337 REWRITE_TAC[v_prime; IN_ELIM_THM];
\r
339 EXISTS_TAC `ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;
\r
340 FIRST_ASSUM ACCEPT_TAC;
\r
343 SPECL [`v:real^3 `;`V:real^3 -> bool`;` E:(real^3 -> bool) -> bool`;` snx:real^3`] XOHLED);
\r
344 UNDISCH_TAC`FAN ((v:real^3),v_prime V FF,e_prime E FF)`;
\r
348 ASM_SIMP_TAC[GSYM UNI_E_IMP_EE_EQ_SET_OF_EDGE];
\r
349 SUBGOAL_THEN `{FST (x':real^3 # real^3), SND x'} IN e_prime E FF ` ASSUME_TAC;
\r
350 ASM_REWRITE_TAC[e_prime; IN_ELIM_THM];
\r
351 EXISTS_TAC`(fx:real^3 )`;
\r
352 EXISTS_TAC `snx:real^3 `;
\r
353 REPLICATE_TAC 5 DOWN;
\r
355 REWRITE_TAC[ord_pairs; IN_ELIM_THM];
\r
359 REPLICATE_TAC 6 DOWN;
\r
362 SUBGOAL_THEN ` fx:real^3 IN EE snx E /\ fx IN EE snx (e_prime E FF) ` ASSUME_TAC;
\r
363 REWRITE_TAC[EE; IN_ELIM_THM];
\r
364 REPLICATE_TAC 4 DOWN THEN PHA;
\r
365 ASM_SIMP_TAC[INSERT_COMM; ord_pairs; IN_ELIM_THM];
\r
366 IMP_TAC THEN STRIP_TAC;
\r
373 UNDISCH_TAC ` fx:real^3 IN EE snx E `;
\r
374 UNDISCH_TAC ` cyclic_set (EE snx E) (v:real^3) snx`;
\r
376 IMP_TAC THEN STRIP_TAC;
\r
377 SUBGOAL_THEN ` FAN (v:real^3,V,E)` MP_TAC;
\r
380 NHANH PROPERTIES_OF_IVS_AZIM_CYCLE2;
\r
381 PHA THEN IMP_TAC THEN REMOVE_TAC;
\r
384 UNDISCH_TAC `(fx:real^3) IN EE snx (e_prime E FF)`;
\r
385 UNDISCH_TAC `cyclic_set (EE snx (e_prime E FF)) (v:real^3) snx`;
\r
390 IMP_TAC THEN STRIP_TAC;
\r
391 SUBGOAL_THEN ` FAN (v:real^3,v_prime V FF, e_prime E FF)` MP_TAC;
\r
394 NHANH PROPERTIES_OF_IVS_AZIM_CYCLE2;
\r
395 PHA THEN IMP_TAC THEN REMOVE_TAC;
\r
398 ISPECL [`FF:real^3 # real^3 -> bool`;`snx:real^3 `] (GEN_ALL (MATCH_MP SUBSET_IMP_SO_DO_EE E_PRIME_SUBSET_E)));
\r
400 SUBGOAL_THEN `ivs_azim_cycle (EE snx E) v snx fx IN EE snx (e_prime E FF) ` ASSUME_TAC;
\r
401 PAT_REWRITE_TAC`\x. y IN x ` [EE];
\r
402 REWRITE_TAC[IN_ELIM_THM; e_prime];
\r
403 UNDISCH_TAC` ivs_azim_cycle (EE snx E) (v:real^3) snx fx IN EE snx E`;
\r
404 ABBREV_TAC `t = ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;
\r
405 REWRITE_TAC[EE; IN_ELIM_THM];
\r
407 EXISTS_TAC `snx:real^3 `;
\r
408 EXISTS_TAC `t:real^3 `;
\r
412 ABBREV_TAC `t = ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;
\r
413 ABBREV_TAC `tt = ivs_azim_cycle (EE snx (e_prime E FF)) v snx (fx:real^3)`;
\r
414 ABBREV_TAC `smalset = EE snx (e_prime (E:(real^3 -> bool) -> bool) FF)`;
\r
415 ABBREV_TAC `lset = EE (snx:real^3) E `;
\r
416 ASM_CASES_TAC ` lset SUBSET {t:real^3} `;
\r
418 UNDISCH_TAC` smalset SUBSET (lset:real^3 -> bool) `;
\r
420 NHANH SUBSET_TRANS;
\r
421 UNDISCH_TAC `(tt:real^3) IN smalset `;
\r
424 ASM_CASES_TAC `t = (tt:real^3) `;
\r
425 STRIP_TAC THEN FIRST_ASSUM ACCEPT_TAC;
\r
427 SET_RULE` ~(t = tt) /\ t IN smalset /\ (tt:real^3) IN smalset ==>
\r
428 ~( smalset SUBSET {tt}) `);
\r
429 USE_FIRST ` cyclic_set lset (v:real^3) snx` MP_TAC;
\r
430 USE_FIRST ` cyclic_set smalset (v:real^3) snx` MP_TAC;
\r
431 REWRITE_TAC[cyclic_set];
\r
433 UNDISCH_TAC `FINITE (lset:real^3 -> bool) `;
\r
436 SPECL [`lset:real^3 -> bool `;` t:real^3`;` snx:real^3 `;` v:real^3 ` ] (GEN_ALL AZIM_CYCLE_PROPERTIES));
\r
437 ASSUME_TAC2 (SPECL [`smalset:real^3 -> bool `;` tt:real^3`;` snx:real^3 `;` v:real^3 ` ] (GEN_ALL AZIM_CYCLE_PROPERTIES));
\r
443 SPECL [`smalset:real^3 -> bool`;`v:real^3 `;`snx:real^3`;`t:real^3 `;` fx:real^3 `] (GEN_ALL IDENTIFY_AZIM_CYCLE));
\r
444 SUBGOAL_THEN ` ~(smalset SUBSET {t:real^3}) /\
\r
445 ~collinear {(t:real^3), v, snx} /\
\r
446 cyclic_set smalset v snx /\
\r
447 (~(fx = t) /\ smalset fx) /\
\r
448 (!q. ~(q = t) /\ smalset q
\r
449 ==> azim v snx t fx < azim v snx t q \/
\r
450 azim v snx t fx = azim v snx t q /\
\r
451 norm (projection (snx - v) (fx - v)) <=
\r
452 norm (projection (snx - v) (q - v)))` ASSUME_TAC;
\r
455 UNDISCH_TAC `~( t = (tt:real^3)) `;
\r
456 UNDISCH_TAC ` (tt:real^3) IN smalset`;
\r
459 UNDISCH_TAC` cyclic_set lset (v:real^3) snx `;
\r
460 NHANH CYCLIC_SET_IMP_NOT_COLLINEAR;
\r
462 UNDISCH_TAC ` (t:real^3) IN lset `;
\r
463 FIRST_X_ASSUM NHANH;
\r
465 UNDISCH_TAC ` smalset SUBSET (lset:real^3 -> bool) `;
\r
466 REWRITE_TAC[SUBSET];
\r
470 FIRST_X_ASSUM ACCEPT_TAC;
\r
471 UNDISCH_TAC ` cyclic_set smalset (v:real^3) snx `;
\r
473 SUBGOAL_THEN ` (FAN (v:real^3,v_prime V FF,e_prime E FF)) ` MP_TAC;
\r
474 FIRST_ASSUM ACCEPT_TAC;
\r
475 NHANH (SPEC `snx:real^3 ` (GEN `v:real^3 ` BIJ_AZIM_CYCLE_EE));
\r
476 IMP_TAC THEN REMOVE_TAC;
\r
480 REWRITE_TAC[BIJ; INJ];
\r
483 FIRST_X_ASSUM (MP_TAC o (SPECL [`t:real^3 `;` tt:real^3 `]));
\r
484 REWRITE_TAC[TAUT` ~( a ==> b) <=> a /\ ~ b `];
\r
485 ASM_REWRITE_TAC[]]);;
\r
489 let LOCALIZE_PRESERVE_FACE = prove_by_refinement
\r
491 x IN dart (hypermap (HYP (v,V,E))) /\
\r
492 FF = face (hypermap (HYP (v,V,E))) x
\r
493 ==> FF = face (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x`,
\r
495 MP_TAC IN_FF_FACE_MAP_IDE;
\r
498 EXISTS_TAC`x: real^3 # real^3 `;
\r
501 NHANH (MESON[face_refl]` D = face H x ==> x IN D `);
\r
502 DISCH_TAC THEN DISCH_TAC;
\r
503 ABBREV_TAC ` hy2 = hypermap (HYP (v,v_prime V FF,e_prime E FF)) `;
\r
504 ASM_REWRITE_TAC[face; orbit_map];
\r
506 SET_RULE`(! n. Q n x = P n x ) ==> { Q n x | n >= 0 } = { P n x | n >= 0 } `);
\r
508 ISPECL [`face_map ((hypermap (HYP (v,V,E))) )` ] lemma_in_orbit);
\r
509 DOWN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
510 SIMP_TAC[GSYM face];
\r
516 REWRITE_TAC[POWER];
\r
518 FIRST_X_ASSUM (MP_TAC o (SPEC_ALL));
\r
522 REWRITE_TAC[GSYM COM_POWER_FUNCTION];
\r
533 let FAN_IN_SEFL_PAIRS_IMP_PROGORIOUS_DEGENERATE =
\r
534 prove_by_refinement(` FAN (x,V,E) /\ v IN self_pairs E V
\r
535 ==> edge_map (hypermap (HYP(x,V,E))) v = v /\
\r
536 face_map (hypermap (HYP(x,V,E))) v = v /\
\r
537 node_map (hypermap (HYP(x,V,E))) v = v `,
\r
538 [NHANH ELMS_OF_HYPERMAP_HYP;
\r
542 SIMP_TAC[nn_of_hyp3; ff_of_hyp3];
\r
543 SIMP_TAC[ee_of_hyp2;darts_of_hyp; IN_UNION];
\r
544 REWRITE_TAC[self_pairs; IN_ELIM_THM];
\r
550 let FAN_FACE_IMP_IVS_F_IN_F =
\r
551 prove_by_refinement (` FAN (x,V,E) /\
\r
552 xx IN dart (hypermap (HYP (x,V,E))) /\
\r
553 FF = face (hypermap (HYP (x,V,E))) xx /\ y IN FF
\r
554 ==> inverse ( face_map (hypermap (HYP (x,V,E))) ) y IN FF /\
\r
555 ( face_map (hypermap (HYP (x,V,E))) ) o (inverse ( face_map (hypermap (HYP (x,V,E))) )) = I /\
\r
556 (inverse ( face_map (hypermap (HYP (x,V,E))) )) o ( face_map (hypermap (HYP (x,V,E))) ) = I `,
\r
558 REWRITE_TAC[GSYM hypermap_tybij; HYP];
\r
560 REPLICATE_TAC 3 DOWN THEN PHA;
\r
561 REWRITE_TAC[GSYM HYP];
\r
562 ASSUME_TAC2 ELMS_OF_HYPERMAP_HYP;
\r
563 NHANH lemma_face_subset;
\r
564 ASM_SIMP_TAC[SUBSET];
\r
565 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
568 ASM_REWRITE_TAC[face];
\r
569 UNDISCH_TAC ` ff_of_hyp (x,V,E) permutes darts_of_hyp E V `;
\r
570 UNDISCH_TAC ` FINITE (darts_of_hyp E (V:real^3 -> bool))`;
\r
573 DISCH_TAC THEN CONJ_TAC;
\r
577 MESON_TAC[lemma_orbit_identity; lemma_inverse_in_orbit];
\r
579 NHANH PERMUTES_INVERSES_o;
\r
583 let FAN_FACE_IMP_IVS_F_IN_F =
\r
584 prove_by_refinement
\r
586 FF = face (hypermap (HYP (x,V,E))) xx /\
\r
588 ==> inverse (face_map (hypermap (HYP (x,V,E)))) y IN FF /\
\r
589 face_map (hypermap (HYP (x,V,E))) o
\r
590 inverse (face_map (hypermap (HYP (x,V,E)))) =
\r
592 inverse (face_map (hypermap (HYP (x,V,E)))) o
\r
593 face_map (hypermap (HYP (x,V,E))) =
\r
596 ASM_CASES_TAC` xx IN dart (hypermap (HYP ((x:real^3),V,E)))`;
\r
597 ASSUME_TAC2 FAN_FACE_IMP_IVS_F_IN_F;
\r
598 FIRST_X_ASSUM ACCEPT_TAC;
\r
599 DOWN_TAC THEN NHANH HYP_LEMMA;
\r
600 REWRITE_TAC[GSYM hypermap_tybij; HYP];
\r
601 NHANH ELMS_OF_HYPERMAP_HYP;
\r
603 REWRITE_TAC[GSYM HYP];
\r
605 REPLICATE_TAC 4 DOWN THEN PHA;
\r
606 REWRITE_TAC[GSYM HYP];
\r
607 NHANH lemma_face_exception;
\r
610 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
611 ASM_REWRITE_TAC[SET_RULE` x IN {c} <=> x = c `];
\r
613 USE_FIRST ` ff_of_hyp (x,V,E) permutes darts_of_hyp E V` MP_TAC;
\r
614 REWRITE_TAC[permutes];
\r
615 DOWN THEN DOWN THEN DOWN THEN ASM_REWRITE_TAC[];
\r
616 REWRITE_TAC[GSYM HYP];
\r
618 UNDISCH_TAC `~((xx:real^3 # real^3 ) IN darts_of_hyp E V) `;
\r
619 FIRST_X_ASSUM NHANH;
\r
621 PAT_ONCE_REWRITE_TAC `\x. y = x ` [GSYM I_THM];
\r
622 UNDISCH_TAC `ff_of_hyp (x,V,E) permutes darts_of_hyp E V `;
\r
623 NHANH PERMUTES_INVERSES_o;
\r
625 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
626 REWRITE_TAC[o_THM];
\r
628 UNDISCH_TAC `ff_of_hyp (x,V,E) permutes darts_of_hyp E V`;
\r
629 NHANH PERMUTES_INVERSES_o;
\r
630 ASM_MESON_TAC[]]);;
\r
635 let INVERSE_FACE_EQ_INV_FACE_LOCALLIZED =
\r
636 prove_by_refinement
\r
638 x IN dart (hypermap (HYP (v,V,E))) /\
\r
639 FF = face (hypermap (HYP (v,V,E))) x
\r
641 ==> inverse ( face_map (hypermap (HYP (v,V,E))) ) x =
\r
642 inverse ( face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF)))) x)`,
\r
646 NHANH FAN_FACE_IMP_IVS_F_IN_F;
\r
649 SPECL [` x:real^3 # real^3 `;` x':real^3 # real^3`;` FF:real^3#real^3->bool `;` v:real^3 `;` v_prime (V:real^3 -> bool) (FF:real^3 # real^3 -> bool) ` ;` e_prime E (FF:real^3 # real^3 -> bool)`] (GEN_ALL FAN_FACE_IMP_IVS_F_IN_F));
\r
652 MP_TAC IMP_FAN_V_PRIME_E_PRIME;
\r
655 EXISTS_TAC `x: real^3 # real^3 `;
\r
658 ASSUME_TAC2 LOCALIZE_PRESERVE_FACE;
\r
660 REWRITE_TAC[GSYM HYP];
\r
661 UNDISCH_TAC `FF = face (hypermap (HYP (v,V,E))) x `;
\r
663 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
669 REWRITE_TAC[FUN_EQ_THM];
\r
670 DISCH_THEN (MP_TAC o (SPEC `x': real^3 # real^3` ));
\r
671 ASSUME_TAC2 (SPECL [`x:real^3 # real^3 `;`x':real^3 # real^3 `;` FF: real^3 # real^3 -> bool` ;` v:real^3 `] (GEN_ALL FAN_FACE_IMP_IVS_F_IN_F));
\r
672 REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC));
\r
673 DOWN THEN REMOVE_TAC;
\r
674 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
675 REWRITE_TAC[o_THM];
\r
676 MP_TAC IN_FF_FACE_MAP_IDE;
\r
679 EXISTS_TAC `x:real^3# real^3 `;
\r
682 UNDISCH_TAC ` inverse (face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF)))) x' IN FF `;
\r
683 FIRST_X_ASSUM NHANH;
\r
685 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
686 UNDISCH_TAC ` FAN ((v:real^3),V,E) `;
\r
688 REWRITE_TAC[GSYM hypermap_tybij; HYP];
\r
690 REWRITE_TAC[GSYM HYP];
\r
691 DOWN_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP;
\r
694 UNDISCH_TAC `ff_of_hyp (v,V,E) permutes darts_of_hyp E V `;
\r
695 ASM_REWRITE_TAC[permutes];
\r
704 let ED_MA_O_NO_MA_EQ_INV_FA =
\r
705 prove_by_refinement
\r
706 (`!(H:(A) hypermap ). edge_map H o node_map H = inverse ( face_map H ) `,
\r
708 MP_TAC (SPEC_ALL hypermap_lemma);
\r
709 NHANH (MESON[]` x o y o z = b ==> (x o y o z ) o ( inverse z ) = b o ( inverse z ) `);
\r
710 REWRITE_TAC[GSYM o_ASSOC; I_O_ID];
\r
711 NHANH PERMUTES_INVERSES_o;
\r
714 ASM_REWRITE_TAC[I_O_ID]]);;
\r
722 let IN_FF_IMP_AZIM_CYCLE_EQ =
\r
723 prove_by_refinement (
\r
725 x IN dart (hypermap (HYP (v,V,E))) /\
\r
726 FF = face (hypermap (HYP (v,V,E))) x
\r
727 ==> (!x. x IN FF ==>
\r
728 azim_cycle (EE (FST x ) E ) v (FST x ) (SND x ), FST x =
\r
729 azim_cycle (EE (FST x ) (e_prime E FF ) ) v (FST x ) (SND x ), FST x)`,
\r
731 prove(`FAN (v,V,E) /\
\r
732 x IN dart (hypermap (HYP (v,V,E))) /\
\r
733 FF = face (hypermap (HYP (v,V,E))) x
\r
734 ==> (!x. x IN FF ==>
\r
735 (edge_map (hypermap (HYP (v,V,E))) o node_map (hypermap (HYP (v,V,E))) ) x =
\r
736 (edge_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) o node_map ( hypermap (HYP (v,v_prime V FF,e_prime E FF))) ) x ) `,
\r
737 REWRITE_TAC[ED_MA_O_NO_MA_EQ_INV_FA;
\r
738 INVERSE_FACE_EQ_INV_FACE_LOCALLIZED]));
\r
740 GEN_TAC THEN FIRST_X_ASSUM NHANH;
\r
741 MP_TAC IMP_FAN_V_PRIME_E_PRIME;
\r
744 DOWN_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP;
\r
748 USE_FIRST ` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);
\r
749 REWRITE_TAC[o_THM];
\r
750 PAT_ONCE_REWRITE_TAC `\x. h ( d x ) = h ( i x ) ==> y ` [GSYM PAIR];
\r
751 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;
\r
752 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
754 UNDISCH_TAC ` x IN dart (hypermap (HYP (v,V,E))) `;
\r
755 NHANH lemma_face_subset;
\r
756 DOWN THEN DOWN THEN PHA THEN SET_TAC[];
\r
757 SUBGOAL_THEN ` x' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
\r
758 UNDISCH_TAC ` x IN dart (hypermap (HYP (v,V,E))) `;
\r
759 NHANH lemma_face_subset;
\r
761 DOWN THEN DOWN THEN MESON_TAC[SUBSET];
\r
762 FIRST_X_ASSUM (ASSUME_TAC o SYM);
\r
765 MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]` FAN (v:real^3,V,E) ==> (! y.
\r
766 y IN darts_of_hyp E V ==> nn_of_hyp (v,V,E) y IN darts_of_hyp E V )`);
\r
769 SPECL [`v_prime (V:real^3 -> bool) (FF:real^3 # real^3 -> bool) `;
\r
770 ` e_prime (E:(real^3 -> bool) -> bool) FF`]
\r
771 (MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]`! V E. FAN (v:real^3,V,E) ==> (! y.
\r
772 y IN darts_of_hyp E V ==> nn_of_hyp (v,V,E) y IN darts_of_hyp E V )`));
\r
774 SIMP_TAC[ee_of_hyp2];
\r
775 SIMP_TAC[nn_of_hyp2]]);;
\r
781 let IN_DARTS_IMP_NN_OF_HYP_TOO =
\r
782 MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]`! x V E. FAN (x,V,E) ==>
\r
783 (! y. y IN darts_of_hyp E V
\r
784 ==> nn_of_hyp (x,V,E) y IN darts_of_hyp E V )`;;
\r
793 let CARD_E_GT1_EQ_CARD_E_PRIME = prove_by_refinement
\r
794 (` FAN (x,V,E) /\ v IN dart (hypermap (HYP (x,V,E)) ) /\
\r
795 FF = face (hypermap (HYP (x,V,E))) v /\ y IN FF
\r
796 ==> ( CARD (EE (FST y) E) > 1 <=> CARD (EE (FST y) (e_prime E FF)) > 1 ) `,
\r
797 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c <=> b /\ a /\ c `];
\r
798 NHANH FAN_FACE_IMP_IVS_F_IN_F;
\r
799 ONCE_REWRITE_TAC[TAUT` a /\ ( b /\ c /\ d ) /\ p <=> (b /\ a /\ c ) /\ d /\ p`];
\r
800 NHANH INVERSE_FACE_EQ_INV_FACE_LOCALLIZED;
\r
801 REWRITE_TAC[GSYM ED_MA_O_NO_MA_EQ_INV_FA];
\r
804 FIRST_X_ASSUM (NHANH_PAT`\x. x /\ y ==> k `);
\r
806 MP_TAC (SPEC `x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));
\r
809 UNDISCH_TAC ` FAN ((x:real^3),V,E)`;
\r
810 NHANH ELMS_OF_HYPERMAP_HYP;
\r
811 PHA THEN STRIP_TAC;
\r
812 UNDISCH_TAC ` (edge_map (hypermap (HYP (x,V,E))) o node_map (hypermap (HYP (x,V,E))))
\r
814 (edge_map (hypermap (HYP (x,v_prime V FF,e_prime E FF))) o
\r
815 node_map (hypermap (HYP (x,v_prime V FF,e_prime E FF))))
\r
817 UNDISCH_TAC `(edge_map (hypermap (HYP (x,V,E))) o node_map (hypermap (HYP (x,V,E))))
\r
821 UNDISCH_TAC ` FF = face (hypermap (HYP (x,V,E))) v `;
\r
822 DISCH_THEN (ASSUME_TAC o SYM);
\r
824 PAT_ONCE_REWRITE_TAC `\x. P x IN FF ==> Q x = Y x ==> l ` [GSYM PAIR];
\r
827 PURE_REWRITE_TAC[o_THM];
\r
828 SUBGOAL_THEN ` v IN dart (hypermap (HYP (x,V,E))) ` MP_TAC;
\r
830 NHANH lemma_face_subset;
\r
831 IMP_TAC THEN REMOVE_TAC;
\r
832 SUBGOAL_THEN ` (y:real^3 # real^3) IN FF ` MP_TAC;
\r
833 FIRST_ASSUM ACCEPT_TAC;
\r
837 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];
\r
838 NHANH (SET_RULE` a SUBSET b /\ x IN a ==> x IN b `);
\r
839 IMP_TAC THEN IMP_TAC;
\r
844 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];
\r
845 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
846 ASSUME_TAC2 IN_DARTS_IMP_NN_OF_HYP_TOO;
\r
847 FIRST_X_ASSUM NHANH;
\r
849 SPECL [`x:real^3 `;` v_prime V (FF:real^3 # real^3 -> bool)`;
\r
850 ` e_prime (E:(real^3 -> bool) -> bool) FF `] IN_DARTS_IMP_NN_OF_HYP_TOO);
\r
851 FIRST_X_ASSUM NHANH;
\r
852 SIMP_TAC[ee_of_hyp2];
\r
853 SIMP_TAC[nn_of_hyp2];
\r
856 UNDISCH_TAC ` v IN dart (hypermap (HYP (x,V,E))) `;
\r
857 NHANH lemma_face_subset;
\r
858 ASM_REWRITE_TAC[SUBSET];
\r
860 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF`;
\r
861 FIRST_ASSUM (NHANH_PAT` \x. x ==> y `);
\r
862 REWRITE_TAC[darts_of_hyp; IN_UNION; ord_pairs; self_pairs];
\r
865 REWRITE_TAC[IN_ELIM_THM];
\r
867 FIRST_X_ASSUM SUBST_ALL_TAC;
\r
869 SUBGOAL_THEN ` FINITE (EE (a:real^3) E ) ` ASSUME_TAC;
\r
870 ASM_MESON_TAC[FAN_IMP_FINITE_EE];
\r
875 SUBGOAL_THEN` ~( EE (a:real^3) E SUBSET {b} ) ` ASSUME_TAC;
\r
876 REWRITE_TAC[SET_RULE` a SUBSET {b} <=> a = {} \/ a = {b} `];
\r
878 MESON_TAC[ARITH_RULE` ~( 0 > 1 \/ 1 > 1 )`; CARD_CLAUSES; CARD_SINGLETON];
\r
879 UNDISCH_TAC ` FINITE (EE (a:real^3) E ) `;
\r
884 NHANH (SPECL [`x:real^3 `; `a:real^3 `] (GENL [`v:real^3`;` w:real^3 `] AZIM_CYCLE_PROPERTIES));
\r
886 SUBGOAL_THEN ` b IN EE (a:real^3) (e_prime E FF) /\
\r
887 azim_cycle (EE a E) x a b IN EE (a:real^3) (e_prime E FF) ` ASSUME_TAC;
\r
888 UNDISCH_TAC ` {(a:real^3), b} IN E `;
\r
889 UNDISCH_TAC ` (a:real^3),(b:real^3) IN FF `;
\r
890 UNDISCH_TAC `azim_cycle (EE a E) x a b,a IN FF `;
\r
891 UNDISCH_TAC `EE a E (azim_cycle (EE a E) x a b) `;
\r
893 REWRITE_TAC[EE; e_prime; IN_ELIM_THM];
\r
896 DOWN THEN MESON_TAC[];
\r
897 EXISTS_TAC `azim_cycle {(w:real^3) | {a, w} IN E} x a b`;
\r
898 EXISTS_TAC `a:real^3 `;
\r
899 ASM_SIMP_TAC[INSERT_COMM];
\r
900 UNDISCH_TAC ` FAN ((x:real^3),v_prime V FF,e_prime E FF) `;
\r
901 NHANH (SPEC ` a:real^3` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));
\r
903 REWRITE_TAC[SET_RULE` a IN x /\ b IN x <=> {a,b} SUBSET x `];
\r
904 ONCE_REWRITE_TAC[TAUT` a ==> b /\ c ==> d <=> b /\ a /\ c ==> d `];
\r
906 UNDISCH_TAC ` ~(azim_cycle (EE a E) x a b = b) `;
\r
908 SIMP_TAC[INSERT_COMM];
\r
910 STRIP_TAC THEN DOWN;
\r
913 ISPECL [`FF:real^3 # real^3 -> bool`;` E: (real^3 -> bool) -> bool`] (GEN_ALL E_PRIME_SUBSET_E));
\r
915 ISPECL [`S: (A -> bool) -> bool`;` a:A`] (GEN_ALL SUBSET_IMP_SO_DO_EE));
\r
917 SPEC `a:real^3 ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));
\r
919 ONCE_REWRITE_TAC[TAUT` a ==> b /\ c ==> d <=> b /\ c /\ a ==> d `];
\r
923 REWRITE_TAC[IN_ELIM_THM];
\r
926 REMOVE_TAC THEN REMOVE_TAC;
\r
928 ISPECL [`FF:real^3 # real^3 -> bool`;` E: (real^3 -> bool) -> bool`] (GEN_ALL E_PRIME_SUBSET_E));
\r
930 ISPECL [`S: (A -> bool) -> bool`;` v':A`] (GEN_ALL SUBSET_IMP_SO_DO_EE));
\r
931 ASM_SIMP_TAC[SUBSET_EMPTY]]);;
\r
937 (* OOOOOOOOOOOOOOOOOO *)
\r
947 let AZIM_IN_FAN_EQ_IZIM_E_PRIME = prove_by_refinement
\r
948 (` FAN (vec 0,V,E) /\ v IN dart (hypermap (HYP (vec 0,V,E)) ) /\
\r
949 FF = face (hypermap (HYP (vec 0,V,E))) v /\ y IN FF
\r
950 ==> azim_in_fan y E = azim_in_fan y ( e_prime E FF ) `,
\r
951 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a /\ b /\ c ) /\ d `];
\r
952 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;
\r
954 ONCE_REWRITE_TAC[GSYM PAIR];
\r
955 REWRITE_TAC[azim_in_fan];
\r
959 SPEC` vec 0 : real^3 ` (GEN `x:real^3 ` CARD_E_GT1_EQ_CARD_E_PRIME));
\r
962 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF`;
\r
963 FIRST_X_ASSUM NHANH;
\r
964 ASM_CASES_TAC ` CARD (EE (FST (y:real^3 # real^3)) (E: (real^3->bool)->bool )) > 1 `;
\r
965 ASM_SIMP_TAC[PAIR_EQ];
\r
974 let AZIM_CY_FST_Y_IN_FF =
\r
975 prove_by_refinement(
\r
976 ` xx IN dart (hypermap (HYP (x,V,E))) /\
\r
977 FAN (x,V,E) /\ FF = face (hypermap (HYP (x,V,E))) xx /\ y IN FF
\r
978 ==> azim_cycle (EE (FST y) E) x (FST y) (SND y),FST y IN FF /\
\r
979 (inverse (face_map (hypermap (HYP (x,V,E))))) y =
\r
980 azim_cycle (EE (FST y) E) x (FST y) (SND y),FST y `,
\r
981 [NHANH FAN_FACE_IMP_IVS_F_IN_F;
\r
982 REWRITE_TAC[GSYM ED_MA_O_NO_MA_EQ_INV_FA; o_THM];
\r
983 NHANH ELMS_OF_HYPERMAP_HYP;
\r
984 IMP_TAC THEN IMP_TAC; STRIP_TAC ;
\r
987 PAT_ONCE_REWRITE_TAC ` \x. f ( g x ) IN HH /\ hh ==> l ` [GSYM PAIR];
\r
988 SUBGOAL_THEN ` (y:real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;
\r
989 UNDISCH_TAC ` xx IN dart (hypermap (HYP (x,V,E))) `;
\r
990 NHANH lemma_face_subset;
\r
995 ASSUME_TAC2 IN_DARTS_IMP_NN_OF_HYP_TOO;
\r
996 FIRST_X_ASSUM NHANH;
\r
997 SIMP_TAC[ee_of_hyp2];
\r
998 SIMP_TAC[nn_of_hyp2]]);;
\r
1006 let EE_FST_Y_EQ_SET_SET_SNDY = prove_by_refinement
\r
1008 v IN dart (hypermap (HYP (x,V,E))) /\
\r
1009 FF = face (hypermap (HYP (x,V,E))) v /\
\r
1011 ==> ( EE (FST y) E = {SND y} <=> EE (FST y) (e_prime E FF) = {SND y} ) `,
\r
1012 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a/\b/\c) /\d `];
\r
1013 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;
\r
1015 ONCE_REWRITE_TAC[TAUT`a1/\a2/\a3/\a4/\a5 <=> a2 /\ a4 /\ a1/\a3/\a5 `];
\r
1016 ONCE_REWRITE_TAC[TAUT` a /\ b /\ c <=> b /\ a /\ c `];
\r
1017 NHANH AZIM_CY_FST_Y_IN_FF;
\r
1020 SPEC ` x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));
\r
1024 NHANH (SPEC ` FST (y:real^3#real^3) ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));
\r
1027 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);
\r
1029 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==> azim_cycle W v w p = p`) ));
\r
1031 ASM_REWRITE_TAC[];
\r
1032 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1033 FIRST_ASSUM NHANH;
\r
1034 SIMP_TAC[PAIR_EQ];
\r
1037 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) (e_prime E FF)) `;
\r
1040 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);
\r
1041 UNDISCH_TAC ` EE (FST y) E = {SND (y:real^3 # real^3 )} `;
\r
1042 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);
\r
1046 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) (e_prime E FF) ` ASSUME_TAC;
\r
1048 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1049 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];
\r
1052 ASM_REWRITE_TAC[];
\r
1053 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `];
\r
1056 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);
\r
1058 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==> azim_cycle W v w p = p`)));
\r
1059 ASM_REWRITE_TAC[];
\r
1060 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1061 FIRST_ASSUM NHANH;
\r
1062 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1063 ASM_SIMP_TAC[PAIR_EQ];
\r
1065 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1068 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) E) `;
\r
1069 ASM_REWRITE_TAC[];
\r
1072 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);
\r
1073 UNDISCH_TAC ` EE (FST y) (e_prime E (face (hypermap (HYP (x,V,E))) v)) = {SND (y:real^3 # real^3 )} `;
\r
1074 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);
\r
1078 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) E ` ASSUME_TAC;
\r
1080 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];
\r
1083 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `]]);;
\r
1086 let W_SUBSET_SINGLETON_IMP_IDE =
\r
1087 (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p}
\r
1088 ==> azim_cycle W v w p = p`);;
\r
1091 let EE_FST_Y_EQ_SET_SET_SNDY = prove_by_refinement
\r
1093 v IN dart (hypermap (HYP (x,V,E))) /\
\r
1094 FF = face (hypermap (HYP (x,V,E))) v /\
\r
1096 ==> ( EE (FST y) E = {SND y} <=> EE (FST y) (e_prime E FF) = {SND y} ) `,
\r
1097 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a/\b/\c) /\d `];
\r
1098 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;
\r
1100 ONCE_REWRITE_TAC[TAUT`a1/\a2/\a3/\a4/\a5 <=> a4 /\ a2/\ a1/\a3/\a5 `];
\r
1101 NHANH AZIM_CY_FST_Y_IN_FF;
\r
1104 SPEC ` x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));
\r
1108 NHANH (SPEC ` FST (y:real^3#real^3) ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));
\r
1111 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);
\r
1113 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==> azim_cycle W v w p = p`)));
\r
1114 ASM_REWRITE_TAC[];
\r
1115 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1116 FIRST_ASSUM NHANH;
\r
1117 SIMP_TAC[PAIR_EQ];
\r
1120 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) (e_prime E FF)) `;
\r
1123 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);
\r
1124 UNDISCH_TAC ` EE (FST y) E = {SND (y:real^3 # real^3 )} `;
\r
1125 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);
\r
1129 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) (e_prime E FF) ` ASSUME_TAC;
\r
1131 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1132 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];
\r
1135 ASM_REWRITE_TAC[];
\r
1136 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `];
\r
1139 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);
\r
1141 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] W_SUBSET_SINGLETON_IMP_IDE));
\r
1142 ASM_REWRITE_TAC[];
\r
1143 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;
\r
1144 FIRST_ASSUM NHANH;
\r
1145 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1146 ASM_SIMP_TAC[PAIR_EQ];
\r
1148 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1151 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) E) `;
\r
1152 ASM_REWRITE_TAC[];
\r
1155 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);
\r
1156 UNDISCH_TAC ` EE (FST y) (e_prime E (face (hypermap (HYP (x,V,E))) v)) = {SND (y:real^3 # real^3 )} `;
\r
1157 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);
\r
1161 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) E ` ASSUME_TAC;
\r
1163 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];
\r
1166 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `]]);;
\r
1171 let WEDGE_IN_FAN_EQ_WITH_E_PRIME =
\r
1172 prove_by_refinement (` FAN (vec 0,V,E) /\
\r
1173 v IN dart (hypermap (HYP (vec 0,V,E))) /\
\r
1174 FF = face (hypermap (HYP (vec 0,V,E))) v /\
\r
1176 ==> wedge_in_fan_ge y E = wedge_in_fan_ge y (e_prime E FF ) /\
\r
1177 wedge_in_fan_gt y E = wedge_in_fan_gt y ( e_prime E FF ) `,
\r
1178 [ONCE_REWRITE_TAC[TAUT` a /\ b /\c /\ d <=> (a /\ b /\ c ) /\ d `];
\r
1179 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;
\r
1182 SPEC `vec 0: real^3 ` (GEN `x:real^3 ` CARD_E_GT1_EQ_CARD_E_PRIME));
\r
1184 FIRST_X_ASSUM NHANH;
\r
1185 PAT_ONCE_REWRITE_TAC`\x. a ==> b ==> x ` [GSYM PAIR];
\r
1186 SIMP_TAC[wedge_in_fan_ge; wedge_in_fan_gt];
\r
1189 ASM_CASES_TAC `CARD (EE (FST (y:real^3 # real^3)) E) > 1 `;
\r
1192 ABBREV_TAC ` FD = face (hypermap (HYP (vec 0,V,E))) v `;
\r
1194 REWRITE_TAC[PAIR_EQ];
\r
1200 ABBREV_TAC ` FD = face (hypermap (HYP (vec 0,V,E))) v `;
\r
1201 SUBGOAL_THEN ` EE (FST y) E = {SND (y:real^3 # real^3)} <=>
\r
1202 EE (FST y) ( e_prime E FD ) = {SND y }` ASSUME_TAC;
\r
1203 MATCH_MP_TAC (SPEC ` vec 0:real^3 ` (GEN `x:real^3 ` EE_FST_Y_EQ_SET_SET_SNDY));
\r
1204 ASM_REWRITE_TAC[];
\r
1207 ASM_SIMP_TAC[EQ_SYM_EQ];
\r
1208 DOWN THEN MESON_TAC[]]);;
\r
1214 let FACE_NODE_EDGE_ORBIT_INVERSE = prove(
\r
1215 ` face (H:(A) hypermap) x = orbit_map ( inverse (face_map H )) x /\
\r
1216 node H x = orbit_map (inverse ( node_map H)) x /\
\r
1217 edge H x = orbit_map (inverse ( edge_map H )) x `,
\r
1218 MP_TAC (SPEC_ALL hypermap_lemma) THEN
\r
1219 SIMP_TAC[face;node;edge] THEN
\r
1220 MESON_TAC[lemma_card_inverse_map_eq]);;
\r
1228 let DARTS_E_PRIME_EQ_FF_UNION_SWITCH =
\r
1229 prove_by_refinement(` (! x. x IN FF ==> {FST x, SND x } IN E )
\r
1230 ==> darts_of_hyp (e_prime E FF) (v_prime V FF) =
\r
1231 FF UNION { ((v:A),w) | (w,v) IN FF }`,
\r
1232 [REWRITE_TAC[darts_of_hyp;EXTENSION; IN_UNION];
\r
1233 REWRITE_TAC[ord_pairs; self_pairs; IN_ELIM_THM; e_prime; v_prime];
\r
1234 STRIP_TAC THEN GEN_TAC;
\r
1237 DOWN_TAC THEN REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
\r
1239 DOWN THEN DOWN THEN REWRITE_TAC[EE];
\r
1240 REWRITE_TAC[SET_RULE` x = {} <=> (! a. ~ ( a IN x ))`];
\r
1241 REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM];
\r
1242 ASM_MESON_TAC[FST;SND];
\r
1245 EXISTS_TAC ` FST (x:A#A) `;
\r
1246 EXISTS_TAC ` SND (x:A#A) `;
\r
1248 EXISTS_TAC ` FST (x:A#A) `;
\r
1249 EXISTS_TAC ` SND (x:A#A) `;
\r
1250 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
\r
1252 EXISTS_TAC ` v:A`;
\r
1254 ASM_REWRITE_TAC[];
\r
1256 EXISTS_TAC ` v:A`;
\r
1257 ASM_SIMP_TAC[INSERT_COMM;PAIR; FST; SND];
\r
1258 ASM_MESON_TAC[INSERT_COMM;PAIR; FST; SND]]);;
\r
1266 let CARD_FF_GT1_FF_SUBSET =
\r
1267 prove_by_refinement(` FAN ((v:real^3),V,E) /\
\r
1268 FF = face (hypermap (HYP (v,V,E))) x /\
\r
1270 ==> (! y. y IN FF ==> {FST y, SND y} IN E ) `,
\r
1271 [NHANH ELMS_OF_HYPERMAP_HYP;
\r
1272 ASM_CASES_TAC ` ~( x IN darts_of_hyp E (V:real^3 -> bool) ) \/
\r
1273 x IN self_pairs E V `;
\r
1275 SUBGOAL_THEN ` face_map (hypermap (HYP (v,V,E))) x = x ` MP_TAC;
\r
1276 ASM_SIMP_TAC[ff_of_hyp3];
\r
1277 ABBREV_TAC ` tt = face_map (hypermap (HYP (v,V,E))) `;
\r
1278 ONCE_REWRITE_TAC[orbit_one_point];
\r
1279 REWRITE_TAC[BETA_THM];
\r
1281 REWRITE_TAC[GSYM face];
\r
1282 UNDISCH_TAC ` 1 < CARD (FF: real^3 # real^3 -> bool) `;
\r
1283 ASM_REWRITE_TAC[];
\r
1284 MESON_TAC[CARD_SINGLETON; ARITH_RULE ` ~( 1 < 1 ) `];
\r
1286 REWRITE_TAC[DE_MORGAN_THM];
\r
1287 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1288 STRIP_TAC THEN STRIP_TAC;
\r
1289 UNDISCH_TAC ` x IN darts_of_hyp E (V:real^3 -> bool) `;
\r
1290 ASM_REWRITE_TAC[];
\r
1291 NHANH lemma_face_subset;
\r
1293 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1294 REWRITE_TAC[SUBSET];
\r
1296 ASM_REWRITE_TAC[];
\r
1297 FIRST_X_ASSUM NHANH;
\r
1298 ASM_REWRITE_TAC[darts_of_hyp; IN_UNION];
\r
1301 REWRITE_TAC[IN_ORD_E_EQ_IN_E];
\r
1302 SUBGOAL_THEN ` face_map (hypermap (HYP (v,V,E))) y = y ` MP_TAC;
\r
1303 ASM_REWRITE_TAC[];
\r
1304 ASM_SIMP_TAC[ff_of_hyp3];
\r
1305 ABBREV_TAC ` tt = face_map (hypermap (HYP (v,V,E))) `;
\r
1306 ONCE_REWRITE_TAC[orbit_one_point];
\r
1307 REPLICATE_TAC 3 DOWN;
\r
1308 NHANH lemma_face_identity;
\r
1309 REPEAT STRIP_TAC THEN DOWN;
\r
1310 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
1311 UNDISCH_TAC ` 1 < CARD (FF: real^3 # real^3 -> bool) `;
\r
1312 ASM_REWRITE_TAC[GSYM face];
\r
1313 MESON_TAC[CARD_SINGLETON; ARITH_RULE ` ~( 1 < 1 ) `]]);;
\r
1323 let DARTS_E_PRIME_GT1_SWITCH = prove(
\r
1324 ` FAN (v,V,E) /\ FF = face (hypermap (HYP (v,V,E))) x /\ 1 < CARD FF
\r
1325 ==> darts_of_hyp (e_prime E FF) (v_prime V FF) =
\r
1326 FF UNION {v,w | w,v IN FF}`,
\r
1327 NHANH CARD_FF_GT1_FF_SUBSET THEN
\r
1328 NHANH DARTS_E_PRIME_EQ_FF_UNION_SWITCH THEN SIMP_TAC[]);;
\r
1335 let FAN_FACE_GT1_IMAGE_EE_OF_HYP = prove_by_refinement
\r
1336 (` x IN darts_of_hyp E V /\
\r
1337 FAN (v,V,E) /\ FF = face (hypermap (HYP (v,V,E))) x /\ 1 < CARD FF
\r
1338 ==> darts_of_hyp (e_prime E FF) (v_prime V FF) =
\r
1339 FF UNION IMAGE (ee_of_hyp (v,V,E)) FF `,
\r
1340 [NHANH DARTS_E_PRIME_GT1_SWITCH;
\r
1341 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1343 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1345 UNDISCH_TAC ` x IN darts_of_hyp E (V:real^3 -> bool) `;
\r
1346 ASM_REWRITE_TAC[];
\r
1347 NHANH lemma_face_subset;
\r
1348 ASM_REWRITE_TAC[];
\r
1349 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
1351 MATCH_MP_TAC (MESON[]` x = y ==> f x = f y `);
\r
1352 REWRITE_TAC[IMAGE; EXTENSION; IN_ELIM_THM];
\r
1353 UNDISCH_TAC ` ee_of_hyp (v,V,E) = edge_map (hypermap (HYP (v,V,E))) `;
\r
1354 DISCH_THEN (SUBST1_TAC o SYM);
\r
1356 REWRITE_TAC[SUBSET];
\r
1357 USE_FIRST ` darts_of_hyp E V = dart (hypermap (HYP (v,V,E))) ` (SUBST1_TAC
\r
1359 REWRITE_TAC[ee_of_hyp2];
\r
1360 MESON_TAC[FST; SND; PAIR]]);;
\r
1366 let IN_ORD_PAIRS_E_PRIME = prove(` x IN ord_pairs (e_prime E FF) ==>
\r
1367 x IN ord_pairs E /\ x IN darts_of_hyp E V`,
\r
1368 REWRITE_TAC[darts_of_hyp; IN_UNION; e_prime; ord_pairs; IN_ELIM_THM]
\r
1369 THEN MESON_TAC[]);;
\r
1374 let CARD_GT1_EE_OF_HYP_E_PRIME_EQ = prove_by_refinement
\r
1375 (` FAN (v,V,E) /\ x IN dart (hypermap (HYP (v,V,E))) /\
\r
1376 FF = face (hypermap (HYP (v,V,E))) x /\
\r
1378 ==> (! x. x IN FF ==> ee_of_hyp (v,V,E) x =
\r
1379 ee_of_hyp (v,v_prime V FF,e_prime E FF) x ) `,
\r
1380 [NHANH lemma_face_subset;
\r
1381 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1382 ONCE_REWRITE_TAC[TAUT` (a1/\a2)/\a3/\a4 <=> a2 /\a3/\a1/\a4`];
\r
1383 NHANH DARTS_E_PRIME_GT1_SWITCH;
\r
1385 REWRITE_TAC[ee_of_hyp2];
\r
1386 SUBGOAL_THEN ` x' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
\r
1387 UNDISCH_TAC ` face (hypermap (HYP (v,V,E))) x SUBSET
\r
1388 dart (hypermap (HYP (v,V,E))) `;
\r
1389 ASM_REWRITE_TAC[SUBSET];
\r
1390 DISCH_THEN MATCH_MP_TAC;
\r
1391 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;
\r
1392 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);
\r
1393 FIRST_X_ASSUM ACCEPT_TAC;
\r
1394 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;
\r
1395 REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];
\r
1396 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
1402 let FF_IMAGE_EE_OF_HYP_EQ_E_PRIME = prove_by_refinement
\r
1403 (` FAN (v,V,E) /\ x IN dart (hypermap (HYP (v,V,E))) /\
\r
1404 FF = face (hypermap (HYP (v,V,E))) x /\
\r
1406 ==> IMAGE (ee_of_hyp (v,V,E)) FF =
\r
1407 IMAGE (ee_of_hyp (v,v_prime V FF,e_prime E FF)) FF `,
\r
1408 [NHANH lemma_face_subset;
\r
1409 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1410 ONCE_REWRITE_TAC[TAUT` (a1/\a2)/\a3/\a4 <=> a2 /\a3/\a1/\a4`];
\r
1411 NHANH DARTS_E_PRIME_GT1_SWITCH;
\r
1413 REWRITE_TAC[IMAGE; EXTENSION; IN_ELIM_THM];
\r
1414 GEN_TAC THEN EQ_TAC;
\r
1416 EXISTS_TAC ` x'': real^3 # real^3 `;
\r
1417 ASM_REWRITE_TAC[];
\r
1418 REWRITE_TAC[ee_of_hyp2];
\r
1419 SUBGOAL_THEN ` x'' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
\r
1420 UNDISCH_TAC ` face (hypermap (HYP (v,V,E))) x SUBSET
\r
1421 dart (hypermap (HYP (v,V,E))) `;
\r
1422 ASM_REWRITE_TAC[SUBSET];
\r
1423 DISCH_THEN MATCH_MP_TAC;
\r
1424 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;
\r
1425 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);
\r
1426 FIRST_X_ASSUM ACCEPT_TAC;
\r
1427 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;
\r
1428 REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];
\r
1429 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
1430 USE_FIRST ` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);
\r
1433 SUBGOAL_THEN ` x'' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
\r
1434 UNDISCH_TAC ` face (hypermap (HYP (v,V,E))) x SUBSET
\r
1435 dart (hypermap (HYP (v,V,E))) `;
\r
1436 ASM_REWRITE_TAC[SUBSET];
\r
1437 DISCH_THEN MATCH_MP_TAC;
\r
1438 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;
\r
1439 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);
\r
1440 FIRST_X_ASSUM ACCEPT_TAC;
\r
1441 SUBGOAL_THEN ` x'':real^3 # real^3 IN darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;
\r
1442 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;
\r
1443 ASM_REWRITE_TAC[IN_UNION];
\r
1446 EXISTS_TAC `x'':real^3 # real^3 `;
\r
1447 ASM_REWRITE_TAC[];
\r
1449 SIMP_TAC[ee_of_hyp2];
\r
1450 USE_FIRST` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);
\r
1456 let FIRST_AAUHTVE2 = prove(` FAN (x,V,E) ==>
\r
1457 FINITE (darts_of_hyp E V) /\
\r
1458 ee_of_hyp (x,V,E) permutes darts_of_hyp E V /\
\r
1459 nn_of_hyp (x,V,E) permutes darts_of_hyp E V /\
\r
1460 ff_of_hyp (x,V,E) permutes darts_of_hyp E V /\
\r
1461 ee_of_hyp (x,V,E) o nn_of_hyp (x,V,E) o ff_of_hyp (x,V,E) = I /\
\r
1462 ee_of_hyp (x,V,E) o ee_of_hyp (x,V,E) = I `,
\r
1463 NHANH (SMOOTH_GEN_ALL (REWRITE_RULE[TAUT` a/\b ==> c <=>
\r
1464 a ==> b ==> c `] FIRST_AAUHTVE)) THEN
\r
1465 REWRITE_TAC[HYP; PAIR_EQ] THEN MESON_TAC[]);;
\r
1473 let NOT_IN_DART_IMP_IDE = prove(
\r
1474 ` ~( x IN dart H ) ==>
\r
1475 edge_map H x = x /\
\r
1476 node_map H x = x /\
\r
1477 face_map H x = x:A `,
\r
1478 MP_TAC (SPEC `H:(A) hypermap ` hypermap_lemma)
\r
1479 THEN REWRITE_TAC[permutes] THEN SIMP_TAC[]);;
\r
1485 let SIMPLE_IMP_DISTINCT_FF_NODE_IMAGE =
\r
1486 prove_by_refinement(` simple_hypermap H /\ FF = face H x /\
\r
1487 (! x. (x:A) IN FF ==> ~( node_map H x = x ))
\r
1488 ==> FF INTER IMAGE (node_map H ) FF = {} `,
\r
1489 [REWRITE_TAC[simple_hypermap; INTER; IMAGE];
\r
1491 REWRITE_TAC[ EXTENSION; NOT_IN_EMPTY];
\r
1493 REWRITE_TAC[IN_ELIM_THM];
\r
1495 UNDISCH_TAC ` x'':A IN FF `;
\r
1497 FIRST_X_ASSUM NHANH;
\r
1498 ASM_CASES_TAC ` x'':A IN dart H `;
\r
1500 FIRST_X_ASSUM NHANH;
\r
1501 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SET_RULE` {x} a <=> x = a `];
\r
1503 ASM_REWRITE_TAC[];
\r
1504 NHANH lemma_face_identity;
\r
1506 SUBGOAL_THEN ` x':A IN node H x'' /\ x'' IN node H x'' ` (fun x ->
\r
1507 ASM_MESON_TAC[x]);
\r
1508 ASM_REWRITE_TAC[node_refl; node; in_orbit_map1];
\r
1510 NHANH NOT_IN_DART_IMP_IDE;
\r
1517 let FX_IN_S_IMP_F_POWER_TOO =
\r
1518 prove(` (! (x:A). x IN S ==> f x IN S ) /\ x IN S ==>
\r
1519 (!n. (f POWER n ) x IN S ) `, DISCH_TAC THEN INDUCT_TAC THENL
\r
1520 [ASM_REWRITE_TAC[POWER; I_THM];
\r
1521 REWRITE_TAC[COM_POWER; o_THM] THEN
\r
1522 ASM_MESON_TAC[]]);;
\r
1524 let FX_IN_S_IMP_ORBIT_SUBSET = prove(
\r
1525 ` (!(x:A). x IN S ==> f x IN S) /\ x IN S
\r
1526 ==> orbit_map f x SUBSET S `,
\r
1527 NHANH FX_IN_S_IMP_F_POWER_TOO THEN
\r
1528 REWRITE_TAC[orbit_map; SUBSET; IN_ELIM_THM; ARITH_RULE` n >= 0`]
\r
1529 THEN MESON_TAC[]);;
\r
1535 let FAN_DARTS_OF_IN_D = prove_by_refinement(
\r
1536 ` FAN (v,V,E) /\ x IN darts_of_hyp E V /\
\r
1537 FF = face (hypermap (HYP (v,V,E))) x /\
\r
1538 x' IN FF ==> x' IN darts_of_hyp E V`,
\r
1539 [NHANH ELMS_OF_HYPERMAP_HYP;
\r
1540 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1541 IMP_TAC THEN STRIP_TAC;
\r
1542 ASM_REWRITE_TAC[];
\r
1543 NHANH_PAT `\x. x ==> y ` lemma_face_subset;
\r
1544 REWRITE_TAC[SUBSET]; MESON_TAC[]]);;
\r
1550 let FAN_DART_DARTS = prove(` FAN (x,V,E) ==>
\r
1551 dart (hypermap (HYP (x,V,E))) = darts_of_hyp E V `,
\r
1552 NHANH ELMS_OF_HYPERMAP_HYP THEN SIMP_TAC[]);;
\r
1557 let FACE_SUBSET_DARTS = prove(` FAN (v,V,E) /\ x IN darts_of_hyp E V ==>
\r
1558 face (hypermap (HYP (v,V,E))) x SUBSET darts_of_hyp E V`,
\r
1559 IMP_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP THEN
\r
1560 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
\r
1561 SIMP_TAC[lemma_face_subset]);;
\r
1567 let FF_DISJOINT_ITS_IMAGE_CARD_EQ = prove_by_refinement
\r
1569 x IN darts_of_hyp E V /\
\r
1570 FF = face (hypermap (HYP (v,V,E))) x /\
\r
1571 simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF))) /\
\r
1573 FF INTER IMAGE (nn_of_hyp (v,v_prime V FF, e_prime E FF)) FF = {} /\
\r
1574 CARD FF = CARD (IMAGE (nn_of_hyp (v,v_prime V FF, e_prime E FF)) FF)`,
\r
1575 [ONCE_REWRITE_TAC[TAUT` a1/\a2/\a3/\a4/\a5 <=> (a2/\a1/\a3/\a5)/\a4`];
\r
1576 NHANH FAN_FACE_GT1_IMAGE_EE_OF_HYP;
\r
1578 SUBGOAL_THEN ` FAN (v,v_prime V (FF:real^3 # real^3 -> bool),e_prime E FF) `
\r
1581 NHANH_PAT `\x. x ==> i ` ELMS_OF_HYPERMAP_HYP;
\r
1582 ASM_MESON_TAC[IMP_FAN_V_PRIME_E_PRIME];
\r
1583 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1584 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1588 SUBGOAL_THEN ` (! x. (x:real^3 # real^3) IN FF ==>
\r
1589 ~( node_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x = x )) ` MP_TAC;
\r
1590 ONCE_REWRITE_TAC[inverse2_hypermap_maps];
\r
1593 REWRITE_TAC[o_THM];
\r
1594 NHANH (MESON[]` ( inverse f) x = y ==> f (( inverse f) x ) = f y `);
\r
1597 (hypermap (HYP (v,v_prime V FF,e_prime E FF))) ` edge_map_and_darts);
\r
1598 NHANH PERMUTES_INVERSES;
\r
1602 ABBREV_TAC ` f = face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1603 ABBREV_TAC ` e = edge_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1604 ABBREV_TAC ` n = node_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1605 ASM_CASES_TAC ` (f:real^3 # real^3 -> real^3 # real^3) x' = e x' `;
\r
1606 UNDISCH_TAC` FAN ((v:real^3),v_prime V FF,e_prime E FF) `;
\r
1608 NHANH FIRST_AAUHTVE2;
\r
1609 UNDISCH_TAC `FF = face (hypermap (HYP (v,V,E))) x`;
\r
1610 DISCH_THEN (ASSUME_TAC o SYM);
\r
1611 ASM_REWRITE_TAC[];
\r
1613 UNDISCH_TAC ` inverse (e:real^3#real^3->real^3#real^3) (inverse
\r
1614 (f:real^3#real^3->real^3#real^3) x') = (x':real^3 # real^3 ) `;
\r
1616 NHANH (MESON[]` inverse e ( f x ) = y ==> e (inverse e ( f x )) = e y `);
\r
1617 NHANH (MESON[]` e (inverse e ((inverse f ) x )) = y ==>f ( e (inverse e ( (inverse f ) x ))) = f y `);
\r
1618 UNDISCH_TAC `e permutes dart
\r
1619 (hypermap (HYP (v,v_prime V FF,e_prime E FF)))`;
\r
1620 UNDISCH_TAC ` f permutes dart
\r
1621 (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1623 NHANH PERMUTES_INVERSES;
\r
1626 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;
\r
1629 NHANH lemma_face_identity;
\r
1630 SUBGOAL_THEN ` orbit_map f (x':real^3 # real^3) = {x', e x'} ` ASSUME_TAC;
\r
1631 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];
\r
1633 MATCH_MP_TAC FX_IN_S_IMP_ORBIT_SUBSET;
\r
1634 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
\r
1635 GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC;
\r
1637 FIRST_X_ASSUM SUBST1_TAC;
\r
1638 FIRST_X_ASSUM ACCEPT_TAC;
\r
1640 FIRST_X_ASSUM SUBST1_TAC;
\r
1641 FIRST_X_ASSUM (ACCEPT_TAC o SYM);
\r
1642 REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY];
\r
1644 FIRST_X_ASSUM SUBST1_TAC;
\r
1645 REWRITE_TAC[orbit_reflect];
\r
1646 FIRST_X_ASSUM SUBST1_TAC;
\r
1647 REWRITE_TAC[orbit_reflect];
\r
1649 REWRITE_TAC[GSYM face];
\r
1650 ASM_MESON_TAC[lemma_inverse_in_face; face_refl];
\r
1652 ASM_REWRITE_TAC[face];
\r
1653 MP_TAC LOCALIZE_PRESERVE_FACE;
\r
1655 ASM_REWRITE_TAC[];
\r
1657 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1659 ASM_SIMP_TAC[face];
\r
1663 NHANH (MESON[orbit_reflect]` S = orbit_map f x ==> x IN S `);
\r
1665 REWRITE_TAC[GSYM face];
\r
1666 NHANH lemma_face_identity;
\r
1668 REPLICATE_TAC 3 DOWN;
\r
1669 UNDISCH_TAC ` 2 < CARD (FF:real^3 # real^3 -> bool) `;
\r
1671 REWRITE_TAC[GSYM face];
\r
1673 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
1677 DISCH_THEN (SUBST1_TAC o SYM);
\r
1680 MESON_TAC[Geomdetail.CARD2; ARITH_RULE` a <= 2 ==> ~(2 < a ) `];
\r
1681 MP_TAC (ISPEC `hypermap (HYP (v,v_prime V FF,e_prime E FF)) `
\r
1683 UNDISCH_TAC `FF = face (hypermap (HYP (v,V,E))) (x:real^3 # real^3) `;
\r
1684 DISCH_THEN (ASSUME_TAC o SYM);
\r
1685 ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM];
\r
1687 FIRST_ASSUM (MP_TAC o (SPEC `x':real^3 # real^3 `));
\r
1689 NHANH (MESON[]` f x = y ==> f ( f x ) = f y `);
\r
1690 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF) `;
\r
1691 NHANH FIRST_AAUHTVE2;
\r
1692 DOWN THEN REMOVE_TAC;
\r
1693 ASM_REWRITE_TAC[];
\r
1696 SIMP_TAC[FUN_EQ_THM; o_THM; I_THM];
\r
1698 UNDISCH_TAC `simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF)))
\r
1700 REWRITE_TAC[simple_hypermap];
\r
1702 FIRST_X_ASSUM (MP_TAC o (SPEC `
\r
1703 (f:real^3 # real^3 -> real^3 # real^3) x' `));
\r
1705 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF) `;
\r
1706 NHANH (SMOOTH_GEN_ALL (GEN `y:real^3 # real^3 `
\r
1707 FAN_IMP_IN_DARTS_IFF_FF_TOO));
\r
1708 ASM_REWRITE_TAC[];
\r
1710 FIRST_ASSUM (fun x -> ONCE_REWRITE_TAC[GSYM x]);
\r
1711 UNDISCH_TAC `darts_of_hyp (e_prime E FF) (v_prime V FF) =
\r
1712 dart (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1713 DISCH_THEN (ASSUME_TAC o SYM);
\r
1714 FIRST_ASSUM SUBST1_TAC;
\r
1715 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
1716 ASM_REWRITE_TAC[];
\r
1717 MATCH_MP_TAC FAN_DARTS_OF_IN_D;
\r
1718 ASM_REWRITE_TAC[];
\r
1721 ISPECL [`hypermap (HYP (v,v_prime V FF,e_prime E FF)) `;
\r
1722 ` (f:real^3 # real^3 -> real^3 # real^3) x' ` ] face_refl);
\r
1724 NHANH lemma_inverse_in_face;
\r
1725 NHANH lemma_inverse_in_face;
\r
1726 ASM_SIMP_TAC[PERMUTES_INVERSES];
\r
1727 UNDISCH_TAC `f permutes dart (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;
\r
1728 NHANH PERMUTES_INVERSES;
\r
1730 ASM_REWRITE_TAC[];
\r
1732 SUBGOAL_THEN ` n (f (x':real^3 # real^3)) IN node (hypermap (HYP (v,v_prime V FF,e_prime E
\r
1733 FF))) (f x') ` MP_TAC;
\r
1735 REWRITE_TAC[node; in_orbit_map1];
\r
1736 ASM_REWRITE_TAC[];
\r
1738 MATCH_MP_TAC (SET_RULE` ~( a IN B INTER A ) ==> a IN A ==> ~( a IN B ) `);
\r
1739 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
\r
1741 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IMAGE; IN_ELIM_THM];
\r
1743 UNDISCH_TAC ` simple_hypermap (hypermap (HYP
\r
1744 (v,v_prime V FF,e_prime E FF))) `;
\r
1745 REWRITE_TAC[simple_hypermap];
\r
1747 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` x'':real^3 # real^3 `));
\r
1750 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF)`;
\r
1752 SIMP_TAC[FAN_DART_DARTS];
\r
1754 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
1755 ASM_REWRITE_TAC[];
\r
1756 MATCH_MP_TAC FAN_DARTS_OF_IN_D;
\r
1757 ASM_REWRITE_TAC[];
\r
1758 MP_TAC (SPEC ` x'': real^3 # real^3 ` (GEN `x:real^3 # real^3 `
\r
1759 LOCALIZE_PRESERVE_FACE));
\r
1761 ASM_REWRITE_TAC[];
\r
1763 MATCH_MP_TAC (SET_RULE` x IN FF /\ FF SUBSET A ==> x IN A `);
\r
1764 ASM_REWRITE_TAC[];
\r
1765 MATCH_MP_TAC lemma_face_subset;
\r
1766 UNDISCH_TAC ` FAN (v:real^3,V,E)`;
\r
1767 NHANH ELMS_OF_HYPERMAP_HYP;
\r
1769 MATCH_MP_TAC lemma_face_identity;
\r
1770 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;
\r
1773 REWRITE_TAC[EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY];
\r
1775 FIRST_X_ASSUM (MP_TAC o (SPEC ` x':real^3 # real^3 `));
\r
1776 FIRST_X_ASSUM (MP_TAC o (SPEC ` x'': real^3 # real^3 `));
\r
1778 ASM_REWRITE_TAC[];
\r
1779 SUBGOAL_THEN ` x' IN node (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x''`
\r
1781 ASM_REWRITE_TAC[node; in_orbit_map1];
\r
1783 REPLICATE_TAC 4 DOWN THEN PHA;
\r
1785 MATCH_MP_TAC CARD_IMAGE_INJ;
\r
1786 MP_TAC (ISPEC ` hypermap (HYP (v,v_prime V FF,e_prime E FF)) `
\r
1787 node_map_and_darts);
\r
1788 REWRITE_TAC[permutes; EXISTS_UNIQUE];
\r
1793 UNDISCH_TAC ` FAN (v:real^3,V,E) `;
\r
1794 NHANH FAN_IMP_FIMITE_DARTS;
\r
1795 ASM_REWRITE_TAC[];
\r
1796 MATCH_MP_TAC (MESON[FINITE_SUBSET]` (a ==> A SUBSET B) ==>
\r
1797 a /\ FINITE B ==> FINITE A `);
\r
1799 MATCH_MP_TAC FACE_SUBSET_DARTS;
\r
1800 ASM_REWRITE_TAC[]]);;
\r
1806 let HYP_MAPS_INJ = prove(
\r
1807 `(! (x:A) y. edge_map H x = edge_map H y <=> x = y ) /\
\r
1808 (! x y. node_map H x = node_map H y <=> x = y ) /\
\r
1809 (! x y. face_map H x = face_map H y <=> x = y ) `,
\r
1810 MP_TAC (SPEC_ALL hypermap_lemma) THEN
\r
1811 REWRITE_TAC[permutes] THEN MESON_TAC[]);;
\r
1817 let SIMPLE_FACE_DISJOINT_NODE_MAP_2 = prove_by_refinement
\r
1818 (` (x:A) IN dart H /\
\r
1819 face H x SUBSET dart H /\
\r
1820 simple_hypermap H /\
\r
1821 face H x INTER IMAGE (node_map H) (face H x) = {} /\
\r
1822 dart H = face H x UNION IMAGE (node_map H) (face H x)
\r
1823 ==> !x. x IN dart H
\r
1824 ==> ~(node_map H x = x) /\ node_map H (node_map H x) = x `,
\r
1826 ASM_REWRITE_TAC[IN_UNION];
\r
1829 SUBGOAL_THEN ` ~( node_map H x':A = x') ` ASSUME_TAC;
\r
1831 FIRST_X_ASSUM DISJ_CASES_TAC;
\r
1832 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;
\r
1834 REWRITE_TAC[SET_RULE `~( a INTER b = {} ) <=> ? x. x IN a /\ x IN b `];
\r
1835 REPEAT (EXISTS_TAC ` x':A` THEN
\r
1836 ASM_REWRITE_TAC[IN_IMAGE]);
\r
1838 REWRITE_TAC[IN_IMAGE];
\r
1840 REWRITE_TAC[HYP_MAPS_INJ];
\r
1845 ASM_REWRITE_TAC[];
\r
1846 UNDISCH_TAC ` x' IN face H x \/ x' IN IMAGE (node_map H) (face H (x:A)) `;
\r
1847 SPEC_TAC (`x':A`,` x':A `);
\r
1848 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c ) /\ ( b ==> c ) `;
\r
1849 MESON[]` (! x. P x /\ Q x ) <=> (! x. P x ) /\ (! x. Q x ) `];
\r
1850 MATCH_MP_TAC (TAUT` a /\ ( a ==> b ) ==> a /\ b `);
\r
1852 DOWN THEN REMOVE_TAC;
\r
1854 ASM_CASES_TAC ` node_map H (x':A) = x' `;
\r
1855 ASM_REWRITE_TAC[];
\r
1856 ASSUME_TAC2 lemma_face_subset;
\r
1857 SUBGOAL_THEN` x':A IN dart H ` MP_TAC;
\r
1859 REWRITE_TAC[SUBSET];
\r
1860 DISCH_THEN MATCH_MP_TAC;
\r
1861 ASM_REWRITE_TAC[];
\r
1862 NHANH lemma_dart_invariant;
\r
1864 UNDISCH_TAC `node_map H x':A IN dart H `;
\r
1865 NHANH lemma_dart_invariant;
\r
1867 UNDISCH_TAC `node_map H (node_map H x':A) IN dart H `;
\r
1868 ASM_REWRITE_TAC[IN_UNION];
\r
1870 UNDISCH_TAC ` simple_hypermap (H:(A)hypermap) `;
\r
1871 REWRITE_TAC[simple_hypermap];
\r
1872 DISCH_THEN (MP_TAC o (SPEC `x': A `));
\r
1874 FIRST_ASSUM ACCEPT_TAC;
\r
1875 REWRITE_TAC[EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY];
\r
1876 DISCH_THEN (fun x -> REWRITE_TAC[GSYM x]);
\r
1877 ASM_REWRITE_TAC[];
\r
1878 UNDISCH_TAC ` x':A IN face H x `;
\r
1879 NHANH_PAT`\x. x ==> i ` lemma_face_identity;
\r
1882 REWRITE_TAC[node];
\r
1883 MESON_TAC[orbit_reflect;IN_ORBIT_MAP_IMP_F_Y];
\r
1886 REWRITE_TAC[IN_IMAGE; HYP_MAPS_INJ];
\r
1888 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;
\r
1889 REWRITE_TAC[SET_RULE` A INTER B = {} <=> ! x. x IN A ==> ~( x IN B ) `];
\r
1890 DISCH_THEN (MP_TAC o (SPEC` x'':A`));
\r
1892 ASM_REWRITE_TAC[];
\r
1894 REWRITE_TAC[IN_IMAGE];
\r
1895 UNDISCH_TAC ` (x':A) IN face H x `;
\r
1898 REWRITE_TAC[IN_IMAGE];
\r
1901 FIRST_X_ASSUM NHANH;
\r
1902 ASM_SIMP_TAC[]]);;
\r
1907 let ITER12 = prove(` ! f x. ITER 1 f x = f x /\ ITER 2 f x = f ( f x )`,
\r
1908 REWRITE_TAC[ARITH_RULE` 2 = SUC 1 /\ 1 = SUC 0`; ITER]);;
\r
1914 prove(t, MESON_TAC[edge_map_and_darts;hypermap_lemma; convolution_rep]);;
\r
1916 let EDGE_MAP_RESO_INVERSE = ENF_RULE
\r
1917 ` (edge_map H ) o (edge_map H ) = I <=> inverse (edge_map H ) = edge_map H `;;
\r
1920 let EDGE_MAP_RESO_INVERSE = CONJ EDGE_MAP_RESO_INVERSE (
\r
1921 ENF_RULE `node_map H o node_map H = I <=> inverse (node_map H) = node_map H `);;
\r
1925 let HAS_ORD2_INTERPRET = prove(` f has_orders 2 <=> f o f = I /\ ~( f = I ) `,
\r
1926 SIMP_TAC[has_orders; ITER12; FUN_EQ_THM; o_THM; ARITH_RULE ` 0 < c /\ c < 2
\r
1927 <=> c = 1 `] THEN MESON_TAC[]);;
\r
1932 let HYP_MAPS_INVS = prove(` edge_map H (inverse ( edge_map H ) x ) = x /\
\r
1933 inverse (edge_map H) ( edge_map H x ) = x /\
\r
1934 face_map H (inverse ( face_map H ) x ) = x /\
\r
1935 inverse (face_map H) ( face_map H x ) = x /\
\r
1936 node_map H (inverse ( node_map H ) x ) = x /\
\r
1937 inverse (node_map H) ( node_map H x ) = x `,
\r
1938 MESON_TAC[PERMUTES_INVERSES; hypermap_lemma]);;
\r
1942 let ITER_CYCLIC_ORBIT = prove(` 0 < i /\ ITER i f x = x ==> orbit_map f x =
\r
1943 {ITER n f x | n < i } `,
\r
1944 REWRITE_TAC[ARITH_RULE` 0 < i <=> ~( i = 0 ) `; GSYM POWER_TO_ITER] THEN
\r
1945 NHANH orbit_cyclic THEN SIMP_TAC[]);;
\r
1949 let FACE_CYCLE_CARD = prove(
\r
1950 `! x y H. y IN face H x ==> (face_map H POWER CARD (face H x )) y = y`,
\r
1951 NHANH lemma_face_identity THEN SIMP_TAC[lemma_face_cycle]);;
\r
1956 let INVERSE_FACE_CYCLE = prove(
\r
1957 `! (x:A) H. (inverse (face_map H) POWER (CARD (face H x)) ) x = x `,
\r
1958 REWRITE_TAC[FACE_NODE_EDGE_ORBIT_INVERSE] THEN
\r
1959 REPEAT GEN_TAC THEN
\r
1960 MP_TAC (SPEC_ALL face_map_and_darts) THEN
\r
1961 NHANH PERMUTES_INVERSE THEN
\r
1962 MESON_TAC[lemma_cycle_orbit]);;
\r
1966 let INVERSE_FACE_CYCLE_ALL = prove(` ! x y H. y IN face H x ==>
\r
1967 (inverse (face_map H) POWER (CARD (face H x)) ) y = y `,
\r
1968 NHANH lemma_face_identity THEN
\r
1969 SIMP_TAC[INVERSE_FACE_CYCLE]);;
\r
1973 let DIH2K_IMP_SIMPLE_HYPERMAP2 = prove(
\r
1974 ` dih2k (H:(A)hypermap) k /\ ~( k = 0) ==> simple_hypermap H `,
\r
1975 MP_TAC face_map_and_darts THEN
\r
1976 MESON_TAC[DIH2K_IMP_SIMPLE_HYPERMAP]);;
\r
1982 let DIH2K_FACE_SIMPLIZED = prove_by_refinement
\r
1983 (` edge_map H has_orders 2 /\
\r
1984 (x:A) IN dart H /\ simple_hypermap H /\
\r
1985 (face H x ) INTER IMAGE (node_map H ) (face H x ) = {} /\
\r
1986 dart H = (face H x ) UNION IMAGE (node_map H) (face H x )
\r
1987 <=> dih2k H (CARD (face H x )) /\ x IN dart H`,
\r
1990 NHANH lemma_face_subset;
\r
1991 REWRITE_TAC[dih2k];
\r
1994 MP_TAC (SPEC_ALL FACE_FINITE);
\r
1995 NHANH (ISPEC ` node_map (H:(A)hypermap) ` FINITE_IMAGE);
\r
1996 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;
\r
1997 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];
\r
2002 ASM_REWRITE_TAC[];
\r
2003 MATCH_MP_TAC (ARITH_RULE` b = a ==> x = a + b ==> x = 2 * a `);
\r
2004 MATCH_MP_TAC CARD_IMAGE_INJ;
\r
2005 ASM_REWRITE_TAC[];
\r
2006 SIMP_TAC[HYP_MAPS_INJ];
\r
2007 SUBGOAL_THEN `(! (x:A). x IN dart H ==> ~( node_map H x = x ) /\
\r
2008 (node_map H (node_map H x )) = x )` ASSUME_TAC;
\r
2010 MESON_TAC[SIMPLE_FACE_DISJOINT_NODE_MAP_2];
\r
2013 SUBGOAL_THEN ` node_map (H:(A)hypermap) has_orders 2 ` MP_TAC;
\r
2014 REWRITE_TAC[has_orders];
\r
2015 REWRITE_TAC[FUN_EQ_THM];
\r
2017 REWRITE_TAC[ARITH_RULE` 0 < x /\ x < 2 <=> x = 1 `];
\r
2018 SIMP_TAC[ITER12; I_THM];
\r
2019 GEN_TAC THEN STRIP_TAC;
\r
2020 REWRITE_TAC[NOT_FORALL_THM];
\r
2023 REWRITE_TAC[ITER12; I_THM];
\r
2025 ASM_CASES_TAC ` (x':A) IN dart H `;
\r
2028 MP_TAC (REWRITE_RULE[permutes] hypermap_lemma);
\r
2033 SUBGOAL_THEN ` ! y. y IN face H (x:A) ==> face_map H (node_map H y) =
\r
2034 node_map H ( (inverse (face_map H )) y )` MP_TAC;
\r
2036 PAT_ONCE_REWRITE_TAC `\x. f x = y ` [inverse2_hypermap_maps];
\r
2038 REWRITE_TAC[HAS_ORD2_INTERPRET; EDGE_MAP_RESO_INVERSE];
\r
2042 MESON[inverse2_hypermap_maps]` face_map H = inverse (node_map H) o
\r
2043 inverse (edge_map H) `];
\r
2045 REWRITE_TAC[o_THM; HYP_MAPS_INVS];
\r
2046 ASM_REWRITE_TAC[];
\r
2051 SUBGOAL_THEN` !y. y IN face H (x:A)
\r
2052 ==> ( ! n. ITER n (face_map H) (node_map H y) =
\r
2053 node_map H (ITER n (inverse (face_map H)) y))` MP_TAC;
\r
2054 GEN_TAC THEN STRIP_TAC;
\r
2056 REWRITE_TAC[ITER];
\r
2057 SUBGOAL_THEN ` ITER n (inverse (face_map H)) (y:A) IN face H (x:A) ` ASSUME_TAC;
\r
2059 NHANH_PAT `\x. x ==> y ` lemma_face_identity;
\r
2062 REWRITE_TAC[FACE_NODE_EDGE_ORBIT_INVERSE; orbit_map; IN_ELIM_THM];
\r
2063 EXISTS_TAC `n:num `;
\r
2064 REWRITE_TAC[POWER_TO_ITER; ARITH_RULE ` x >= 0`];
\r
2065 REWRITE_TAC[ITER];
\r
2067 FIRST_ASSUM NHANH;
\r
2068 ASM_REWRITE_TAC[];
\r
2073 (* ,,,,,,,,,,,,,, *)
\r
2075 MATCH_MP_TAC (TAUT` a /\ ( a ==> b ) ==> a /\ b `);
\r
2079 REWRITE_TAC[IN_UNION];
\r
2083 NHANH lemma_face_identity;
\r
2087 REWRITE_TAC[IN_IMAGE];
\r
2093 MATCH_MP_TAC (SET_RULE` a = y /\ b = x ==> a UNION b = x UNION y `);
\r
2094 SUBGOAL_THEN ` IMAGE (node_map H) (face H (x:A)) = S` ASSUME_TAC;
\r
2095 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
2096 ASM_REWRITE_TAC[];
\r
2097 UNDISCH_TAC ` x'':A IN face H x `;
\r
2098 NHANH lemma_face_identity;
\r
2101 PAT_ONCE_REWRITE_TAC `\x. x = y ` [FACE_NODE_EDGE_ORBIT_INVERSE];
\r
2102 REWRITE_TAC[IMAGE; face; orbit_map; EXTENSION; IN_ELIM_THM; POWER_TO_ITER; ARITH_RULE ` x >= 0 `];
\r
2105 FIRST_X_ASSUM NHANH;
\r
2107 STRIP_TAC THEN STRIP_TAC;
\r
2111 REWRITE_TAC[GSYM IMAGE_o];
\r
2112 UNDISCH_TAC ` node_map (H:(A)hypermap) has_orders 2`;
\r
2113 SIMP_TAC[HAS_ORD2_INTERPRET; IMAGE_I];
\r
2115 REWRITE_TAC[has_orders; FUN_EQ_THM; I_THM];
\r
2120 REWRITE_TAC[NOT_FORALL_THM];
\r
2124 ISPECL [`i:num`;`(face_map H): A -> A `] (GEN_ALL ITER_CYCLIC_ORBIT));
\r
2126 REWRITE_TAC[GSYM face];
\r
2127 NHANH (MESON[CARD_LE_K_OF_SET_K_FIRST_ELMS]`
\r
2128 S = { ITER n f x | n < i } ==> CARD S <= i`);
\r
2130 MESON_TAC[ARITH_RULE` a < (b:num) ==> ~( b <= a ) `];
\r
2131 REWRITE_TAC[GSYM POWER_TO_ITER; lemma_face_cycle];
\r
2133 ASM_CASES_TAC `x':A IN dart H `;
\r
2135 ASM_REWRITE_TAC[IN_UNION];
\r
2138 REWRITE_TAC[FACE_CYCLE_CARD];
\r
2140 REWRITE_TAC[IN_IMAGE];
\r
2141 DOWN THEN FIRST_ASSUM NHANH;
\r
2143 ASM_REWRITE_TAC[POWER_TO_ITER];
\r
2144 REWRITE_TAC[GSYM POWER_TO_ITER];
\r
2145 ASM_SIMP_TAC[INVERSE_FACE_CYCLE_ALL];
\r
2146 DOWN THEN NHANH NOT_IN_DART_IMP_IDE;
\r
2147 SIMP_TAC[POWER_TO_ITER; ITER_FIXPOINT2];
\r
2151 MP_TAC (SPEC_ALL face_map_and_darts);
\r
2152 NHANH_PAT `\x. a ==> x ==> y ` lemma_face_subset;
\r
2153 STRIP_TAC THEN STRIP_TAC;
\r
2154 UNDISCH_TAC ` face H (x:A) SUBSET dart H`;
\r
2155 UNDISCH_TAC ` FINITE (dart (H:(A) hypermap)) `;
\r
2157 NHANH FINITE_SUBSET;
\r
2158 IMP_TAC THEN STRIP_TAC;
\r
2159 MP_TAC (SPEC_ALL face_refl);
\r
2161 REWRITE_TAC[SET_RULE` x IN A <=> {x} SUBSET A `];
\r
2162 NHANH CARD_SUBSET;
\r
2163 REWRITE_TAC[CARD_SINGLETON];
\r
2164 NHANH (ARITH_RULE` 1 <= a ==> ~( a = 0 ) `);
\r
2167 UNDISCH_TAC ` dih2k H (CARD (face H (x:A)))`;
\r
2169 NHANH DIH2K_IMP_SIMPLE_HYPERMAP2;
\r
2170 ASM_SIMP_TAC[dih2k; INSERT_SUBSET; EMPTY_SUBSET];
\r
2173 UNDISCH_TAC ` (x:A) IN dart H `;
\r
2174 FIRST_X_ASSUM NHANH;
\r
2177 MATCH_MP_TAC (MESON[CARD_UNION_OVERLAP_EQ]`
\r
2178 FINITE s /\ FINITE t /\ CARD (s UNION t) = CARD s + CARD t
\r
2179 ==> s INTER t = {}`);
\r
2180 FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);
\r
2181 ASM_REWRITE_TAC[ARITH_RULE` 2 * x = x + v <=> x = v `];
\r
2183 MATCH_MP_TAC FINITE_IMAGE;
\r
2184 ASM_REWRITE_TAC[];
\r
2185 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
2186 MATCH_MP_TAC CARD_IMAGE_INJ;
\r
2187 ASM_REWRITE_TAC[HYP_MAPS_INJ];
\r
2191 UNDISCH_TAC ` (x:A) IN dart H `;
\r
2192 FIRST_X_ASSUM NHANH;
\r
2198 let EE_OF_HYP_IDE_FST_SND_EQ = prove(`z IN darts_of_hyp E V ==>
\r
2199 ( ee_of_hyp (x,V,E) z = z <=> FST z = SND z )`,
\r
2200 REWRITE_TAC[ee_of_hyp2] THEN SIMP_TAC[] THEN
\r
2201 ONCE_REWRITE_TAC[PAIR_EQ2] THEN
\r
2202 SIMP_TAC[EQ_SYM_EQ]);;
\r
2206 let MP_TAC2 th = MP_TAC th THEN ANTS_TAC THENL [
\r
2207 ASM_SIMP_TAC[]; SIMP_TAC[]] ;;
\r
2211 let TR_ENF_TAC = MATCH_MP_TAC W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE THEN
\r
2212 REWRITE_TAC[GSYM face; GSYM node; GSYM edge; lemma_face_identity;
\r
2213 lemma_node_identity; lemma_edge_identity];;
\r
2216 let ENF_IMAGE_ITSELF = let t1 = CONJ ( prove(
\r
2217 ` face H x = IMAGE (face_map H ) (face H x )`, TR_ENF_TAC))
\r
2219 ` node H x = IMAGE (node_map H ) (node H x )`, TR_ENF_TAC)) in
\r
2221 ` edge H x = IMAGE (edge_map H ) (edge H x )`, TR_ENF_TAC)) t1;;
\r
2225 let IDE_ON_S_IMP_SAME_IMAGE = prove(` (! x. x IN S ==> f x = g x ) ==>
\r
2226 IMAGE f S = IMAGE g S `,
\r
2227 REWRITE_TAC[EXTENSION; IMAGE; IN_ELIM_THM] THEN
\r
2232 let DIH_K_HYP_E_PRIME = prove_by_refinement
\r
2234 x IN darts_of_hyp E V /\
\r
2235 FF = face (hypermap (HYP (v,V,E))) x /\
\r
2236 simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF))) /\
\r
2238 dih2k (hypermap (HYP (v,v_prime V FF,e_prime E FF))) (CARD FF ) `,
\r
2239 [ONCE_REWRITE_TAC[TAUT` a1/\a2/\a3/\a4/\a5 <=> (a2/\a1/\a3/\a5)/\a4`];
\r
2240 NHANH FAN_FACE_GT1_IMAGE_EE_OF_HYP;
\r
2242 MP_TAC LOCALIZE_PRESERVE_FACE THEN ANTS_TAC;
\r
2243 ASM_REWRITE_TAC[];
\r
2244 DOWN_TAC THEN NHANH FAN_DART_DARTS;
\r
2246 ABBREV_TAC ` hy = HYP (v,v_prime V FF,e_prime E FF) `;
\r
2249 MATCH_MP_TAC (MESON[]` dih2k H k /\ (x:A) IN dart H ==> dih2k H k `);
\r
2250 REWRITE_TAC[GSYM DIH2K_FACE_SIMPLIZED];
\r
2252 REWRITE_TAC[HAS_ORD2_INTERPRET];
\r
2254 MP_TAC IMP_FAN_V_PRIME_E_PRIME;
\r
2256 ASM_REWRITE_TAC[];
\r
2257 DOWN_TAC THEN NHANH FAN_DART_DARTS;
\r
2260 NHANH FIRST_AAUHTVE2;
\r
2261 NHANH ELMS_OF_HYPERMAP_HYP;
\r
2266 MP_TAC IMP_FAN_V_PRIME_E_PRIME;
\r
2268 ASM_REWRITE_TAC[];
\r
2269 DOWN_TAC THEN NHANH FAN_DART_DARTS;
\r
2273 REWRITE_TAC[FUN_EQ_THM; NOT_FORALL_THM];
\r
2274 EXISTS_TAC `x:real^3 # real^3 `;
\r
2275 REWRITE_TAC[I_THM];
\r
2278 SIMP_TAC[ELMS_OF_HYPERMAP_HYP];
\r
2280 SUBGOAL_THEN ` (x:real^3 # real^3) IN
\r
2281 darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;
\r
2284 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
2285 ASM_SIMP_TAC[face_refl];
\r
2286 SIMP_TAC[EE_OF_HYP_IDE_FST_SND_EQ];
\r
2289 REWRITE_TAC[darts_of_hyp; IN_UNION; IN_ORD_E_EQ_IN_E];
\r
2292 REWRITE_TAC[e_prime; IN_ELIM_THM];
\r
2293 UNDISCH_TAC `FAN (v:real^3, V,E) `;
\r
2294 REWRITE_TAC[FAN; graph; HAS_SIZE];
\r
2295 STRIP_TAC THEN STRIP_TAC;
\r
2296 UNDISCH_TAC ` {v',w:real^3} IN E `;
\r
2298 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
2299 FIRST_X_ASSUM NHANH;
\r
2300 REWRITE_TAC[Geomdetail.CARD2];
\r
2302 SUBGOAL_THEN ` ff_of_hyp (v:real^3,v_prime V FF,e_prime E FF) x = x ` MP_TAC;
\r
2304 SIMP_TAC[ff_of_hyp3];
\r
2305 PAT_ONCE_REWRITE_TAC `\x. x ==> i ` [orbit_one_point];
\r
2306 REWRITE_TAC[ETA_AX];
\r
2307 UNDISCH_TAC ` FF = face (hypermap hy) (x:real^3 # real^3 )`;
\r
2308 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF)`;
\r
2310 REWRITE_TAC[face];
\r
2311 SIMP_TAC[GSYM ELMS_OF_HYPERMAP_HYP];
\r
2312 ONCE_REWRITE_TAC[EQ_SYM_EQ];
\r
2314 NHANH (MESON[CARD_SINGLETON]` {p} = FF ==> CARD FF = 1 `);
\r
2316 UNDISCH_TAC ` CARD (FF:real^3#real^3->bool) = 1 `;
\r
2317 UNDISCH_TAC ` 2 < CARD (FF:real^3#real^3->bool) `;
\r
2321 MP_TAC2 IMP_FAN_V_PRIME_E_PRIME;
\r
2322 ASM_MESON_TAC[ELMS_OF_HYPERMAP_HYP];
\r
2324 NHANH FAN_DART_DARTS;
\r
2328 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;
\r
2329 ASM_REWRITE_TAC[face_refl];
\r
2334 FIRST_X_ASSUM (ASSUME_TAC o SYM);
\r
2335 UNDISCH_TAC ` FF = face (hypermap (HYP ((v:real^3),V,E))) x`;
\r
2336 DISCH_THEN (ASSUME_TAC o SYM);
\r
2337 ASM_REWRITE_TAC[];
\r
2338 MP_TAC2 FF_DISJOINT_ITS_IMAGE_CARD_EQ;
\r
2339 MP_TAC2 IMP_FAN_V_PRIME_E_PRIME;
\r
2342 ASM_MESON_TAC[ELMS_OF_HYPERMAP_HYP; face_refl];
\r
2343 NHANH ELMS_OF_HYPERMAP_HYP;
\r
2349 ABBREV_TAC ` nn = nn_of_hyp (v,v_prime V FF, e_prime E FF)`;
\r
2350 MP_TAC2 LOCALIZE_PRESERVE_FACE;
\r
2351 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2352 DISCH_THEN (ASSUME_TAC o SYM);
\r
2353 FIRST_ASSUM ( fun x -> PAT_ONCE_REWRITE_TAC `\x. c = a UNION x ` [GSYM x]);
\r
2354 PAT_ONCE_REWRITE_TAC `\x. c = a UNION x ` [ENF_IMAGE_ITSELF];
\r
2355 ASM_REWRITE_TAC[GSYM IMAGE_o];
\r
2359 MP_TAC2 FAN_FACE_GT1_IMAGE_EE_OF_HYP;
\r
2361 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
2362 ASM_SIMP_TAC[ARITH_RULE` 2 < a ==> 1 < a `];
\r
2365 MP_TAC2 CARD_GT1_EE_OF_HYP_E_PRIME_EQ;
\r
2366 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2367 DOWN THEN DOWN THEN DOWN THEN PHA THEN REMOVE_TAC;
\r
2368 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
2369 ASM_SIMP_TAC[ARITH_RULE` 2 < c ==> 1 < c`];
\r
2370 NHANH IDE_ON_S_IMP_SAME_IMAGE;
\r
2374 MATCH_MP_TAC (MESON[]` a = x ==> f a = f x `);
\r
2375 MATCH_MP_TAC (MESON[]` a = x ==> IMAGE a S = IMAGE x S `);
\r
2376 UNDISCH_TAC `FAN (v:real^3,v_prime V FF,e_prime E FF) `;
\r
2377 NHANH FIRST_AAUHTVE2;
\r
2378 ASM_REWRITE_TAC[];
\r
2379 ABBREV_TAC ` e = ee_of_hyp (v:real^3,v_prime V FF,e_prime E FF) `;
\r
2380 ABBREV_TAC ` f = ff_of_hyp (v:real^3,v_prime V FF,e_prime E FF) `;
\r
2381 ASM_REWRITE_TAC[];
\r
2382 NHANH (MESON[]` e o x = I /\ e o e = I ==> e o e o x = e o I `);
\r
2383 REWRITE_TAC[I_O_ID; o_ASSOC];
\r
2385 REWRITE_TAC[MESON[]` x = y /\ (x o t ) o i = p <=>
\r
2386 x = y /\ (y o t ) o i = p`; I_O_ID];
\r
2387 SIMP_TAC[EQ_SYM_EQ]]);;
\r
2393 let LVDUCXU = prove_by_refinement
\r
2394 (` FAN ((vec 0):real^3,V,E) /\
\r
2395 x IN darts_of_hyp E V /\
\r
2396 FF = face (hypermap (HYP (vec 0,V,E))) x
\r
2397 ==> FF = face (hypermap (HYP (vec 0,v_prime V FF,e_prime E FF))) x /\
\r
2398 (! x. x IN FF ==> azim_in_fan x E = azim_in_fan x (e_prime E FF ) /\
\r
2399 wedge_in_fan_ge x E = wedge_in_fan_ge x (e_prime E FF) /\
\r
2400 wedge_in_fan_gt x E = wedge_in_fan_gt x (e_prime E FF)) /\
\r
2402 simple_hypermap (hypermap (HYP (vec 0,v_prime V FF,e_prime E FF))) ==>
\r
2403 local_fan (v_prime V FF,e_prime E FF,FF) ) `,
\r
2406 MATCH_MP_TAC LOCALIZE_PRESERVE_FACE;
\r
2407 ASM_REWRITE_TAC[];
\r
2408 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2410 GEN_TAC THEN STRIP_TAC;
\r
2412 MATCH_MP_TAC (SPEC `x:real^3 # real^3 ` (GEN `v:real^3 # real^3 ` AZIM_IN_FAN_EQ_IZIM_E_PRIME));
\r
2413 ASM_REWRITE_TAC[];
\r
2414 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2415 MATCH_MP_TAC (SPEC `x:real^3 # real^3 ` (GEN `v:real^3 # real^3 `
\r
2416 WEDGE_IN_FAN_EQ_WITH_E_PRIME));
\r
2417 ASM_REWRITE_TAC[];
\r
2418 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2419 REWRITE_TAC[local_fan];
\r
2423 SPEC `(vec 0): real^3 ` (GEN `v:real^3` IMP_FAN_V_PRIME_E_PRIME));
\r
2424 EXISTS_TAC `x:real^3 # real^3 `;
\r
2426 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2433 EXISTS_TAC ` x:real^3 # real^3 `;
\r
2434 FIRST_X_ASSUM (SUBST1_TAC o SYM);
\r
2435 DOWN THEN SIMP_TAC[FAN_DART_DARTS];
\r
2438 ISPEC `x:real^3 # real^3 ` (GEN `x:A#A`
\r
2439 IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME));
\r
2440 ASM_SIMP_TAC[GSYM FAN_DART_DARTS; face_refl];
\r
2441 DISCH_TAC THEN MATCH_MP_TAC LOCALIZE_PRESERVE_FACE;
\r
2442 ASM_SIMP_TAC[FAN_DART_DARTS];
\r
2444 MATCH_MP_TAC DIH_K_HYP_E_PRIME;
\r
2445 ASM_REWRITE_TAC[]]);;
\r
2450 (* ______________________________________________________________
\r
2451 _________________________________________________________________
\r
2452 flyspeck_needs "general/update_database_310.ml";;
\r