1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Tame Hypermap *)
6 (* Authors: Trieu Thi Diep, Alexey Solovyev *)
8 (* ========================================================================== *)
12 module type Tame_opposite_type = sig
16 flyspeck_needs "hypermap/hypermap.hl";;
17 flyspeck_needs "tame/tame_defs.hl";;
19 module Tame_opposite = struct
27 let tuple_opposite_hypermap = prove
28 (`!(H:(A)hypermap). tuple_hypermap (opposite_hypermap H) = ((dart H),face_map H o node_map H , inverse(node_map H),inverse(face_map H))`,
29 GEN_TAC THEN REWRITE_TAC[opposite_hypermap] THEN
30 REWRITE_TAC[GSYM hypermap_tybij] THEN
31 MP_TAC (SPEC `H:(A)hypermap` hypermap_lemma) THEN
33 ASM_SIMP_TAC[PERMUTES_INVERSE; PERMUTES_COMPOSE] THEN
34 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
35 MP_TAC (ISPECL [`(node_map H):A->A`; `(dart H):A->bool`] PERMUTES_INVERSES_o) THEN
36 MP_TAC (ISPECL [`(face_map H):A->A`; `(dart H):A->bool`] PERMUTES_INVERSES_o) THEN
37 ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM]);;
42 (* LEMMA: plain (tame_1a) *)
43 let opposite_hypermap_plain = prove ( `!(H:(A)hypermap).
44 plain_hypermap H ==> plain_hypermap (opposite_hypermap H)`,
46 REWRITE_TAC[plain_hypermap] THEN
48 REWRITE_TAC[edge_map; tuple_opposite_hypermap] THEN
49 SUBGOAL_THEN `(face_map (H:(A)hypermap) o node_map H) o face_map H o node_map H = (face_map H) o ((node_map H) o (face_map H) o (edge_map H)) o (edge_map H) o (node_map H)` MP_TAC THENL
52 SIMP_TAC[FUN_EQ_THM; o_THM; I_THM];
55 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
56 REWRITE_TAC[hypermap_cyclic; I_O_ID]);;
61 let opposite_components = prove(`!(H:(A)hypermap) x.
62 dart (opposite_hypermap H) = dart H /\
63 node (opposite_hypermap H) x = node H x /\
64 face (opposite_hypermap H) x = face H x`,
65 REPEAT GEN_TAC THEN REWRITE_TAC[dart; tuple_opposite_hypermap] THEN
68 REWRITE_TAC[node; node_map; tuple_opposite_hypermap] THEN
69 REWRITE_TAC[GSYM node_map];
70 REWRITE_TAC[face; face_map; tuple_opposite_hypermap] THEN
71 REWRITE_TAC[GSYM face_map]
73 MATCH_MP_TAC lemma_card_inverse_map_eq THEN
74 EXISTS_TAC `(dart H):A->bool` THEN
75 REWRITE_TAC[hypermap_lemma]);;
80 (* LEMMA: simple (tame_2b) *)
81 let opposite_hypermap_simple = prove ( `!(H:(A)hypermap).
82 simple_hypermap H ==> simple_hypermap (opposite_hypermap H)`,
84 REWRITE_TAC[simple_hypermap; opposite_components] THEN
85 REWRITE_TAC[dart; tuple_opposite_hypermap]);;
90 let hypermap_eq_lemma = prove(`!(H:(A)hypermap). tuple_hypermap H = dart H,edge_map H,node_map H,face_map H`,
92 MP_TAC (ISPEC `tuple_hypermap (H:(A)hypermap)` PAIR_SURJECTIVE) THEN
94 MP_TAC (ISPEC `y:(A->A)#(A->A)#(A->A)` PAIR_SURJECTIVE) THEN
96 MP_TAC (ISPEC `y':(A->A)#(A->A)` PAIR_SURJECTIVE) THEN
98 ASM_REWRITE_TAC[PAIR_EQ] THEN
99 ASM_REWRITE_TAC[dart; edge_map; node_map; face_map]);;
104 let opposite_opposite_hypermap_eq_hypermap = prove(`!(H:(A)hypermap). opposite_hypermap (opposite_hypermap H) = H`,
105 ONCE_REWRITE_TAC[GSYM hypermap_tybij] THEN
108 REWRITE_TAC[tuple_opposite_hypermap; hypermap_eq_lemma; PAIR_EQ] THEN
109 REWRITE_TAC[dart; face_map; node_map; tuple_opposite_hypermap] THEN
110 REWRITE_TAC[GSYM dart; GSYM face_map; GSYM node_map] THEN
111 REWRITE_TAC[GSYM inverse2_hypermap_maps] THEN
112 CONJ_TAC THEN MATCH_MP_TAC (GEN_ALL PERMUTES_INVERSE_INVERSE) THEN
113 EXISTS_TAC `dart (H:(A)hypermap)` THEN
114 REWRITE_TAC[hypermap_lemma]);;
121 let truncated_path_lemma = prove(`!(H:(A)hypermap) p q n. is_path H p n /\
122 (!i. i <= n ==> q i = p i)
124 REPLICATE_TAC 3 GEN_TAC THEN
125 INDUCT_TAC THEN REWRITE_TAC[is_path] THEN
127 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
128 ASM_REWRITE_TAC[] THEN
132 ASM_SIMP_TAC[ARITH_RULE `i <= n ==> i <= SUC n`];
135 FIRST_ASSUM (MP_TAC o SPEC `n:num`) THEN
136 FIRST_ASSUM (MP_TAC o SPEC `SUC n`) THEN
137 REWRITE_TAC[LE_REFL; ARITH_RULE `n <= SUC n`] THEN
143 let opposite_path = prove(`!(H:(A)hypermap) p n. is_path H p n ==>
144 ?q m. is_path (opposite_hypermap H) q m /\
145 q 0 = p 0 /\ q m = p n`,
146 GEN_TAC THEN GEN_TAC THEN
147 INDUCT_TAC THEN REWRITE_TAC[is_path] THENL
149 MAP_EVERY EXISTS_TAC [`p:num->A`; `0`] THEN
150 REWRITE_TAC[is_path];
154 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
155 ASM_REWRITE_TAC[] THEN
157 FIRST_X_ASSUM (MP_TAC o check (fun th -> rator (rator (concl th)) = `go_one_step (H:(A)hypermap)`)) THEN
158 REWRITE_TAC[go_one_step] THEN
161 EXISTS_TAC `(\i:num. if i <= m then (q:num->A) i else (if i = m + 1 then inverse (node_map H) (q m) else edge_map H ((p:num->A) n)))` THEN
162 EXISTS_TAC `SUC(SUC m)` THEN
164 ASM_SIMP_TAC[LE_0; ARITH_RULE `~(SUC (SUC m) <= m)`; ARITH_RULE `~(SUC(SUC m) = m + 1)`] THEN
165 REWRITE_TAC[is_path] THEN
166 REPEAT STRIP_TAC THENL
168 MATCH_MP_TAC truncated_path_lemma THEN
169 EXISTS_TAC `q:num->A` THEN
172 ASM_REWRITE_TAC[LE_REFL; ARITH_RULE `~(m = m + 1)`; ARITH_RULE `~(SUC m <= m)`; ARITH_RULE `SUC m = m + 1`] THEN
173 REWRITE_TAC[go_one_step] THEN
174 DISJ2_TAC THEN DISJ1_TAC THEN
175 GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [node_map] THEN
176 REWRITE_TAC[tuple_opposite_hypermap];
178 ASM_REWRITE_TAC[ARITH_RULE `~(SUC m <= m) /\ ~(SUC (SUC m) <= m) /\ ~(SUC (SUC m) = m + 1) /\ SUC m = m + 1`] THEN
179 REWRITE_TAC[go_one_step] THEN
180 DISJ2_TAC THEN DISJ2_TAC THEN
181 REWRITE_TAC[face_map] THEN
182 REWRITE_TAC[tuple_opposite_hypermap] THEN
183 MP_TAC (SPEC `H:(A)hypermap` inverse2_hypermap_maps) THEN
184 SIMP_TAC[o_THM; FUN_EQ_THM];
187 EXISTS_TAC `(\i:num. if i <= m then (q:num->A) i else (if i = m + 1 then ((face_map H) o (node_map H)) (q m) else node_map H ((p:num->A) n)))` THEN
188 EXISTS_TAC `SUC(SUC m)` THEN
190 ASM_SIMP_TAC[LE_0; ARITH_RULE `~(SUC (SUC m) <= m)`; ARITH_RULE `~(SUC(SUC m) = m + 1)`] THEN
191 REWRITE_TAC[is_path] THEN
192 REPEAT STRIP_TAC THENL
194 MATCH_MP_TAC truncated_path_lemma THEN
195 EXISTS_TAC `q:num->A` THEN
198 ASM_REWRITE_TAC[LE_REFL; ARITH_RULE `~(m = m + 1)`; ARITH_RULE `~(SUC m <= m)`; ARITH_RULE `SUC m = m + 1`] THEN
199 REWRITE_TAC[go_one_step] THEN
201 GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [edge_map] THEN
202 REWRITE_TAC[tuple_opposite_hypermap];
204 ASM_REWRITE_TAC[ARITH_RULE `~(SUC m <= m) /\ ~(SUC (SUC m) <= m) /\ ~(SUC (SUC m) = m + 1) /\ SUC m = m + 1`] THEN
205 REWRITE_TAC[go_one_step] THEN
206 DISJ2_TAC THEN DISJ2_TAC THEN
207 REWRITE_TAC[face_map] THEN
208 REWRITE_TAC[tuple_opposite_hypermap] THEN
209 REWRITE_TAC[GSYM face_map] THEN
210 REWRITE_TAC[o_THM] THEN
211 MP_TAC (ISPECL [`face_map (H:(A)hypermap)`; `dart (H:(A)hypermap)`] PERMUTES_INVERSES_o) THEN
212 REWRITE_TAC[hypermap_lemma; FUN_EQ_THM; o_THM; I_THM] THEN
216 EXISTS_TAC `(\i:num. if i <= m then (q:num->A) i else (if i = m + 1 then inverse (node_map H) (q m) else face_map H ((p:num->A) n)))` THEN
217 EXISTS_TAC `SUC(SUC m)` THEN
219 ASM_SIMP_TAC[LE_0; ARITH_RULE `~(SUC (SUC m) <= m)`; ARITH_RULE `~(SUC(SUC m) = m + 1)`] THEN
220 REWRITE_TAC[is_path] THEN
221 REPEAT STRIP_TAC THENL
223 MATCH_MP_TAC truncated_path_lemma THEN
224 EXISTS_TAC `q:num->A` THEN
227 ASM_REWRITE_TAC[LE_REFL; ARITH_RULE `~(m = m + 1)`; ARITH_RULE `~(SUC m <= m)`; ARITH_RULE `SUC m = m + 1`] THEN
228 REWRITE_TAC[go_one_step] THEN
229 DISJ2_TAC THEN DISJ1_TAC THEN
230 GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [node_map] THEN
231 REWRITE_TAC[tuple_opposite_hypermap];
233 ASM_REWRITE_TAC[ARITH_RULE `~(SUC m <= m) /\ ~(SUC (SUC m) <= m) /\ ~(SUC (SUC m) = m + 1) /\ SUC m = m + 1`] THEN
234 REWRITE_TAC[go_one_step] THEN
236 REWRITE_TAC[edge_map] THEN
237 REWRITE_TAC[tuple_opposite_hypermap] THEN
238 MP_TAC (ISPECL [`node_map (H:(A)hypermap)`; `dart (H:(A)hypermap)`] PERMUTES_INVERSES_o) THEN
239 REWRITE_TAC[hypermap_lemma; FUN_EQ_THM; o_THM; I_THM] THEN
247 let opposite_path_alt = prove(`!(H:(A)hypermap) q m. is_path (opposite_hypermap H) q m
248 ==> (?p n. is_path H p n /\
249 p 0 = q 0 /\ p n = q m)`,
250 REPEAT STRIP_TAC THEN
251 ONCE_REWRITE_TAC[GSYM opposite_opposite_hypermap_eq_hypermap] THEN
252 MATCH_MP_TAC opposite_path THEN
258 let opposite_sets_of_components = prove(`!H:(A)hypermap.
259 node_set (opposite_hypermap H) = node_set H /\
260 face_set (opposite_hypermap H) = face_set H /\
261 set_of_components (opposite_hypermap H) = set_of_components H`,
263 REWRITE_TAC[node_set; face_set; set_of_orbits] THEN
264 REWRITE_TAC[GSYM node; GSYM face; opposite_components] THEN
265 REWRITE_TAC[dart; tuple_opposite_hypermap] THEN
266 SUBGOAL_THEN `!x y:A. (?(p:num->A) n. p 0 = x /\ p n = y /\ is_path H p n) <=> (?(q:num->A) m. q 0 = x /\ q m = y /\ is_path (opposite_hypermap H) q m)` ASSUME_TAC THENL
268 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
270 ONCE_REWRITE_TAC[TAUT `A /\ B /\ C <=> C /\ A /\ B`] THEN
271 REPLICATE_TAC 2 (FIRST_X_ASSUM ((fun th -> REWRITE_TAC[SYM th]) o check (is_eq o concl))) THEN
272 MATCH_MP_TAC opposite_path THEN
274 ONCE_REWRITE_TAC[TAUT `A /\ B /\ C <=> C /\ A /\ B`] THEN
275 REPLICATE_TAC 2 (FIRST_X_ASSUM ((fun th -> REWRITE_TAC[SYM th]) o check (is_eq o concl))) THEN
276 MATCH_MP_TAC opposite_path_alt THEN
281 REWRITE_TAC[set_of_components; set_part_components; dart; tuple_opposite_hypermap] THEN
282 ASM_REWRITE_TAC[GSYM dart; comb_component; is_in_component]);;
287 (* LEMMA: connected (tame_2a) *)
288 let opposite_hypermap_connected = prove (
289 `!(H:(A)hypermap).connected_hypermap H ==> connected_hypermap (opposite_hypermap H)`,
290 REWRITE_TAC[connected_hypermap;number_of_components; opposite_sets_of_components]);;
294 (* LEMMA: is_edge_nondegenerate (tame_3) *)
295 let opposite_nondegenerate = prove (`!(H:(A)hypermap).
296 plain_hypermap H /\ is_edge_nondegenerate H ==> is_edge_nondegenerate (opposite_hypermap H)`,
298 REWRITE_TAC[plain_hypermap; is_edge_nondegenerate] THEN
299 REPEAT STRIP_TAC THEN
300 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
301 REWRITE_TAC[dart; edge_map; tuple_opposite_hypermap] THEN
302 REWRITE_TAC[GSYM dart] THEN
303 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o check (is_forall o concl)) THEN
304 ONCE_REWRITE_TAC[TAUT `(A ==> ~B) <=> (B ==> ~A)`] THEN
305 REWRITE_TAC[NOT_FORALL_THM; TAUT `~(A ==> ~B) <=> A /\ B`] THEN
306 REWRITE_TAC[o_THM] THEN DISCH_TAC THEN
307 EXISTS_TAC `node_map H (x:A)` THEN
308 ASM_SIMP_TAC[lemma_dart_invariant] THEN
309 POP_ASSUM (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [SYM th]) THEN
310 MP_TAC (REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM] hypermap_lemma) THEN
316 (* LEMMA: is_no_double_joints (tame_5a) *)
317 let opposite_no_double_joints = prove(`!H:(A)hypermap.
318 is_no_double_joints H /\ plain_hypermap H
319 ==> is_no_double_joints (opposite_hypermap H)`,
320 GEN_TAC THEN REWRITE_TAC[is_no_double_joints; edge_map_convolution] THEN
322 REWRITE_TAC[tuple_opposite_hypermap; opposite_components; edge_map] THEN
323 REPEAT STRIP_TAC THEN
324 ABBREV_TAC `z:A = node_map H y` THEN
325 ABBREV_TAC `u:A = node_map H x` THEN
326 SUBGOAL_THEN `z:A = u:A ==> x:A = y` MATCH_MP_TAC THENL
328 EXPAND_TAC "z" THEN EXPAND_TAC "u" THEN
329 SIMP_TAC[node_map_injective; EQ_SYM];
332 MATCH_MP_TAC EQ_SYM THEN
333 FIRST_X_ASSUM MATCH_MP_TAC THEN
334 SUBGOAL_THEN `node H (y:A) = node H x` ASSUME_TAC THENL
336 MATCH_MP_TAC EQ_SYM THEN
337 MATCH_MP_TAC lemma_node_identity THEN
342 REPEAT CONJ_TAC THENL
345 ASM_SIMP_TAC[lemma_dart_invariant];
347 SUBGOAL_THEN `node H (u:A) = node H y` ASSUME_TAC THENL
349 MATCH_MP_TAC EQ_SYM THEN
350 MATCH_MP_TAC lemma_node_identity THEN
351 ASM_REWRITE_TAC[] THEN
353 MATCH_MP_TAC lemma_in_node1 THEN
354 REWRITE_TAC[node_refl];
357 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
359 MATCH_MP_TAC lemma_in_node1 THEN
360 REWRITE_TAC[node_refl];
364 ASM_REWRITE_TAC[o_THM] THEN
365 SUBGOAL_THEN `!v w:A. v IN node H w ==> node_map H v IN node H (node_map H w)` MATCH_MP_TAC THENL
367 REPEAT STRIP_TAC THEN
368 MATCH_MP_TAC lemma_in_node1 THEN
369 SUBGOAL_THEN `node H (node_map H (w:A)) = node H w` (fun th -> REWRITE_TAC[th]) THENL
371 MATCH_MP_TAC EQ_SYM THEN
372 MATCH_MP_TAC lemma_node_identity THEN
373 MATCH_MP_TAC lemma_in_node1 THEN
374 REWRITE_TAC[node_refl];
380 FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
381 REWRITE_TAC[o_THM] THEN
382 EXPAND_TAC "z" THEN EXPAND_TAC "u" THEN
388 let plain_hypermap_edge = prove(`!(H:(A)hypermap) x.
389 plain_hypermap H ==> edge H x = {x, edge_map H x}`,
390 REPEAT GEN_TAC THEN REWRITE_TAC[plain_hypermap] THEN
392 REWRITE_TAC[edge] THEN
393 SPEC_TAC (`x:A`, `x:A`) THEN
394 MATCH_MP_TAC lemma_orbit_convolution_map THEN
398 (* LEMMA: no_loops (tame_4) *)
399 let opposite_no_loops = prove(`!H:(A)hypermap.
400 no_loops H /\ plain_hypermap H
401 ==> no_loops (opposite_hypermap H)`,
402 GEN_TAC THEN REWRITE_TAC[no_loops] THEN
404 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP plain_hypermap_edge th)) THEN
405 FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP opposite_hypermap_plain th)) THEN
406 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP plain_hypermap_edge th)) THEN
407 POP_ASSUM MP_TAC THEN REWRITE_TAC[edge_map_convolution] THEN
409 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
411 REWRITE_TAC[opposite_components; edge_map; tuple_opposite_hypermap; o_THM] THEN
412 REWRITE_TAC[Collect_geom.IN_SET2] THEN
413 REPEAT STRIP_TAC THEN
414 SUBGOAL_THEN `node_map H (x:A) = node_map H y ==> x = y` MATCH_MP_TAC THENL
416 REWRITE_TAC[node_map_injective];
419 FIRST_X_ASSUM MATCH_MP_TAC THEN
422 ASM_REWRITE_TAC[o_THM; Collect_geom.IN_SET2];
423 MATCH_MP_TAC lemma_in_node1 THEN
424 SUBGOAL_THEN `node H (node_map H (y:A)) = node H y` (fun th -> REWRITE_TAC[th]) THENL
426 MATCH_MP_TAC EQ_SYM THEN
427 MATCH_MP_TAC lemma_node_identity THEN
428 MATCH_MP_TAC lemma_in_node1 THEN
429 REWRITE_TAC[node_refl];
438 let edge_CARD_dart = prove(`!H:(A)hypermap.
439 plain_hypermap H /\ is_edge_nondegenerate H ==>
440 CARD (dart H) = 2 * number_of_edges H`,
442 REWRITE_TAC[plain_hypermap; is_edge_nondegenerate] THEN
444 REWRITE_TAC[number_of_edges; edge_set] THEN
445 MATCH_MP_TAC (REWRITE_RULE[number_of_orbits] lemma_card_eq) THEN
446 REWRITE_TAC[hypermap_lemma] THEN
447 REPEAT STRIP_TAC THEN
448 MP_TAC (SPECL [`(dart H):A->bool`; `(edge_map H):A->A`] lemma_orbit_of_size_2) THEN
449 REWRITE_TAC[hypermap_lemma] THEN
450 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
451 FIRST_X_ASSUM (MP_TAC o SPEC `x:A`) THEN
452 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
453 ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM]);;
457 let edge_CARD = prove(`!H:(A)hypermap.
458 plain_hypermap H /\ is_edge_nondegenerate H ==>
459 number_of_edges H = CARD (dart H) DIV 2`,
461 DISCH_THEN (ASSUME_TAC o (fun th -> MATCH_MP edge_CARD_dart th)) THEN
462 MATCH_MP_TAC EQ_SYM THEN MATCH_MP_TAC DIV_UNIQ THEN
463 EXISTS_TAC `0` THEN ASM_REWRITE_TAC[] THEN
469 (* LEMMA: planar (tame_1b) *)
470 let opposite_planar = prove ( `!(H:(A)hypermap).
471 planar_hypermap H /\ is_edge_nondegenerate H /\ plain_hypermap H
472 ==> planar_hypermap (opposite_hypermap H)`,
473 GEN_TAC THEN REWRITE_TAC[planar_hypermap] THEN
474 REWRITE_TAC[number_of_nodes; number_of_faces; number_of_components] THEN
475 REWRITE_TAC[opposite_sets_of_components] THEN
476 DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
477 MP_TAC (SPEC `opposite_hypermap (H:(A)hypermap)` edge_CARD) THEN
478 ASM_SIMP_TAC[opposite_hypermap_plain; opposite_nondegenerate] THEN
479 MP_TAC (SPEC `H:(A)hypermap` edge_CARD) THEN
480 ASM_SIMP_TAC[dart; tuple_opposite_hypermap]);;
486 let CARD_faces1 = prove (`! (H:(A)hypermap).
487 tame_8 H ==> tame_8 (opposite_hypermap H) `,
488 REWRITE_TAC[tame_8; number_of_faces; opposite_sets_of_components]);;
493 let CARD_in_face = prove ( `!(H:(A)hypermap).
494 tame_9a H ==> tame_9a (opposite_hypermap H) `,
495 REWRITE_TAC[tame_9a; opposite_components] THEN
496 SIMP_TAC[dart; tuple_opposite_hypermap]);;
500 let CARD_nodes = prove (`!H:(A)hypermap.
501 tame_10 H ==> tame_10 (opposite_hypermap H)`,
502 REWRITE_TAC[tame_10; opposite_sets_of_components; number_of_nodes]);;
505 (* LEMMA: tame_11a /\ tame_11b *)
506 let CARD_in_node = prove ( `!(H:(A)hypermap).
507 tame_11a H /\ tame_11b H ==>
508 tame_11a (opposite_hypermap H) /\ tame_11b (opposite_hypermap H)`,
509 REWRITE_TAC[tame_11a; tame_11b; opposite_components] THEN
510 SIMP_TAC[dart; tuple_opposite_hypermap]);;
515 let the_SAME_orbit_triangles = prove (`!(H:(A)hypermap) x.
516 set_of_triangles_meeting_node H x =
517 set_of_triangles_meeting_node (opposite_hypermap H) x`,
519 REWRITE_TAC[set_of_triangles_meeting_node] THEN
520 REWRITE_TAC[opposite_components] THEN
521 REWRITE_TAC[dart; tuple_opposite_hypermap]);;
525 let the_SAME_orbit_quadrilaterals = prove (`!(H:(A)hypermap) x.
526 set_of_quadrilaterals_meeting_node H x =
527 set_of_quadrilaterals_meeting_node (opposite_hypermap H) x`,
529 REWRITE_TAC[set_of_quadrilaterals_meeting_node] THEN
530 REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
534 let the_SAME_orbit_exceptional = prove (`!(H:(A)hypermap) x.
535 set_of_exceptional_meeting_node H x =
536 set_of_exceptional_meeting_node (opposite_hypermap H) x`,
538 REWRITE_TAC[set_of_exceptional_meeting_node] THEN
539 REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
544 let the_SAME_orbit_face = prove (`!(H:(A)hypermap) x.
545 set_of_face_meeting_node H x = set_of_face_meeting_node (opposite_hypermap H) x`,
547 REWRITE_TAC[set_of_face_meeting_node] THEN
548 REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
552 let the_SAME_type = prove(`!H (x:A). type_of_node H x = type_of_node (opposite_hypermap H) x`,
553 REWRITE_TAC[type_of_node; PAIR_EQ] THEN
554 REWRITE_TAC[GSYM the_SAME_orbit_triangles] THEN
555 REWRITE_TAC[GSYM the_SAME_orbit_quadrilaterals] THEN
556 REWRITE_TAC[GSYM the_SAME_orbit_exceptional]);;
560 (* LEMMA: tame_12o *)
561 let opposite_tame_12o = prove(`!H:(A)hypermap. tame_12o H ==> tame_12o (opposite_hypermap H)`,
562 REWRITE_TAC[tame_12o] THEN
563 REWRITE_TAC[node_type_exceptional_face; exceptional_face] THEN
564 REWRITE_TAC[node_exceptional_face] THEN
565 SIMP_TAC[opposite_components; GSYM the_SAME_type] THEN
566 SIMP_TAC[exceptional_face; opposite_components]);;
569 (* LEMMA: tame_13a *)
570 let opposite_tame_13a = prove(`!H:(A)hypermap.
571 tame_13a H ==> tame_13a (opposite_hypermap H)`,
572 GEN_TAC THEN REWRITE_TAC[tame_13a] THEN
573 REWRITE_TAC[admissible_weight; adm_1; adm_2; adm_3] THEN
574 REWRITE_TAC[GSYM the_SAME_type] THEN
575 REWRITE_TAC[GSYM the_SAME_orbit_exceptional] THEN
576 REWRITE_TAC[GSYM the_SAME_orbit_quadrilaterals] THEN
577 REWRITE_TAC[GSYM the_SAME_orbit_triangles] THEN
578 REWRITE_TAC[GSYM the_SAME_orbit_face] THEN
579 REWRITE_TAC[opposite_components] THEN
581 EXISTS_TAC `w:(A->bool)->real` THEN
582 ASM_REWRITE_TAC[] THEN
583 POP_ASSUM MP_TAC THEN
584 REWRITE_TAC[total_weight] THEN
585 REWRITE_TAC[opposite_sets_of_components]);;
590 (* LEMMA: tame H ==> tame (opposite H) *)
591 let tame_opposite_hypermap = prove ( `!(H:(A)hypermap). tame_hypermap H ==> tame_hypermap (opposite_hypermap H)`,
592 GEN_TAC THEN REWRITE_TAC[tame_hypermap; tame_1; tame_2; tame_3; tame_4; tame_5a] THEN
593 SIMP_TAC[opposite_hypermap_plain; opposite_planar; opposite_hypermap_connected; opposite_hypermap_simple] THEN
594 SIMP_TAC[opposite_nondegenerate; opposite_no_loops; opposite_no_double_joints] THEN
595 SIMP_TAC[CARD_faces1; CARD_in_face; CARD_nodes; CARD_in_node] THEN
596 SIMP_TAC[opposite_tame_12o; opposite_tame_13a]);;
601 (* LEMMA: the main result *)
602 let PPHEUFG = prove (`!(H:(A)hypermap). tame_hypermap H <=> tame_hypermap (opposite_hypermap H)`,
603 GEN_TAC THEN EQ_TAC THENL
605 REWRITE_TAC[tame_opposite_hypermap];
607 ONCE_REWRITE_TAC[GSYM opposite_opposite_hypermap_eq_hypermap] THEN
608 MATCH_MP_TAC tame_opposite_hypermap THEN