text_formalization/tame/tame_opposite.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: PPHEUFG                                                             *)
   5 (* Chapter: Tame Hypermap                                                     *)
   6 (* Authors: Trieu Thi Diep, Alexey Solovyev                                   *)
   7 (* Date: 2010-02-26                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12 module type Tame_opposite_type = sig
  13
  14 end;;
  15
  16 flyspeck_needs "hypermap/hypermap.hl";;
  17 flyspeck_needs "tame/tame_defs.hl";;
  18
  19 module Tame_opposite  = struct
  20
  21
  22 open Hypermap;;
  23 open Tame_defs;;
  24
  25
  26 (* LEMMA: general *)
  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
  32     STRIP_TAC 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]);;
  38
  39
  40
  41
  42 (* LEMMA: plain (tame_1a) *)
  43 let opposite_hypermap_plain = prove ( `!(H:(A)hypermap).
  44        plain_hypermap H ==> plain_hypermap (opposite_hypermap H)`,
  45    GEN_TAC THEN
  46      REWRITE_TAC[plain_hypermap] THEN
  47      DISCH_TAC 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
  50      [
  51        POP_ASSUM MP_TAC THEN
  52          SIMP_TAC[FUN_EQ_THM; o_THM; I_THM];
  53        ALL_TAC
  54      ] THEN
  55      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
  56      REWRITE_TAC[hypermap_cyclic; I_O_ID]);;
  57
  58
  59
  60 (* LEMMA: general *)
  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
  66      CONJ_TAC THENL
  67      [
  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]
  72      ] THEN
  73      MATCH_MP_TAC lemma_card_inverse_map_eq THEN
  74      EXISTS_TAC `(dart H):A->bool` THEN
  75      REWRITE_TAC[hypermap_lemma]);;
  76
  77
  78
  79
  80 (* LEMMA: simple (tame_2b) *)
  81 let opposite_hypermap_simple = prove ( `!(H:(A)hypermap).
  82                 simple_hypermap H ==> simple_hypermap (opposite_hypermap H)`,
  83    GEN_TAC THEN
  84      REWRITE_TAC[simple_hypermap; opposite_components] THEN
  85      REWRITE_TAC[dart; tuple_opposite_hypermap]);;
  86
  87
  88
  89 (* LEMMA: general *)
  90 let hypermap_eq_lemma = prove(`!(H:(A)hypermap). tuple_hypermap H = dart H,edge_map H,node_map H,face_map H`,
  91     GEN_TAC THEN
  92       MP_TAC (ISPEC `tuple_hypermap (H:(A)hypermap)` PAIR_SURJECTIVE) THEN
  93       STRIP_TAC THEN
  94       MP_TAC (ISPEC `y:(A->A)#(A->A)#(A->A)` PAIR_SURJECTIVE) THEN
  95       STRIP_TAC THEN
  96       MP_TAC (ISPEC `y':(A->A)#(A->A)` PAIR_SURJECTIVE) THEN
  97       STRIP_TAC THEN
  98       ASM_REWRITE_TAC[PAIR_EQ] THEN
  99       ASM_REWRITE_TAC[dart; edge_map; node_map; face_map]);;
 100
 101
 102
 103 (* LEMMA: general *)
 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
 106      GEN_TAC THEN
 107      AP_TERM_TAC 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]);;
 115
 116
 117
 118
 119
 120 (* LEMMA: aux *)
 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)
 123                                  ==> is_path H q n`,
 124    REPLICATE_TAC 3 GEN_TAC THEN
 125      INDUCT_TAC THEN REWRITE_TAC[is_path] THEN
 126      STRIP_TAC THEN
 127      FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
 128      ASM_REWRITE_TAC[] THEN
 129      ANTS_TAC THENL
 130      [
 131        GEN_TAC THEN
 132          ASM_SIMP_TAC[ARITH_RULE `i <= n ==> i <= SUC n`];
 133        ALL_TAC
 134      ] THEN
 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
 138      ASM_SIMP_TAC[]);;
 139
 140
 141
 142 (* LEMMA: general *)
 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
 148      [
 149        MAP_EVERY EXISTS_TAC [`p:num->A`; `0`] THEN
 150          REWRITE_TAC[is_path];
 151        ALL_TAC
 152      ] THEN
 153      STRIP_TAC THEN
 154      FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
 155      ASM_REWRITE_TAC[] THEN
 156      STRIP_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
 159      STRIP_TAC THENL
 160      [
 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
 163          BETA_TAC 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
 167          [
 168            MATCH_MP_TAC truncated_path_lemma THEN
 169              EXISTS_TAC `q:num->A` THEN
 170              ASM_SIMP_TAC[];
 171
 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];
 177
 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];
 185          ];
 186
 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
 189          BETA_TAC 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
 193          [
 194            MATCH_MP_TAC truncated_path_lemma THEN
 195              EXISTS_TAC `q:num->A` THEN
 196              ASM_SIMP_TAC[];
 197
 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
 200              DISJ1_TAC THEN
 201              GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [edge_map] THEN
 202              REWRITE_TAC[tuple_opposite_hypermap];
 203
 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
 213              SIMP_TAC[];
 214          ];
 215
 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
 218          BETA_TAC 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
 222          [
 223            MATCH_MP_TAC truncated_path_lemma THEN
 224              EXISTS_TAC `q:num->A` THEN
 225              ASM_SIMP_TAC[];
 226
 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];
 232
 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
 235              DISJ1_TAC 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
 240              SIMP_TAC[]
 241          ]
 242      ]);;
 243
 244
 245
 246 (* LEMMA: general *)
 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
 253      ASM_REWRITE_TAC[]);;
 254
 255
 256
 257 (* LEMMA: general *)
 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`,
 262   REPEAT GEN_TAC THEN
 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
 267     [
 268       REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
 269         [
 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
 273             ASM_REWRITE_TAC[];
 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
 277             ASM_REWRITE_TAC[]
 278         ];
 279       ALL_TAC
 280     ] 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]);;
 283
 284
 285
 286
 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]);;
 291
 292
 293
 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)`,
 297    GEN_TAC THEN
 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
 311      SIMP_TAC[]);;
 312
 313
 314
 315
 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
 321      STRIP_TAC 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
 327      [
 328        EXPAND_TAC "z" THEN EXPAND_TAC "u" THEN
 329          SIMP_TAC[node_map_injective; EQ_SYM];
 330        ALL_TAC
 331      ] THEN
 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
 335      [
 336        MATCH_MP_TAC EQ_SYM THEN
 337          MATCH_MP_TAC lemma_node_identity THEN
 338          ASM_REWRITE_TAC[];
 339        ALL_TAC
 340      ] THEN
 341
 342      REPEAT CONJ_TAC THENL
 343      [
 344        EXPAND_TAC "u" THEN
 345          ASM_SIMP_TAC[lemma_dart_invariant];
 346
 347        SUBGOAL_THEN `node H (u:A) = node H y` ASSUME_TAC THENL
 348          [
 349            MATCH_MP_TAC EQ_SYM THEN
 350              MATCH_MP_TAC lemma_node_identity THEN
 351              ASM_REWRITE_TAC[] THEN
 352              EXPAND_TAC "u" THEN
 353              MATCH_MP_TAC lemma_in_node1 THEN
 354              REWRITE_TAC[node_refl];
 355            ALL_TAC
 356          ] THEN
 357          POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 358          EXPAND_TAC "z" THEN
 359          MATCH_MP_TAC lemma_in_node1 THEN
 360          REWRITE_TAC[node_refl];
 361        ALL_TAC
 362      ] THEN
 363
 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
 366      [
 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
 370          [
 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];
 375            ALL_TAC
 376          ] THEN
 377          ASM_REWRITE_TAC[];
 378        ALL_TAC
 379      ] THEN
 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
 383      SIMP_TAC[]);;
 384
 385
 386
 387 (* LEMMA: general *)
 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
 391      DISCH_TAC THEN
 392      REWRITE_TAC[edge] THEN
 393      SPEC_TAC (`x:A`, `x:A`) THEN
 394      MATCH_MP_TAC lemma_orbit_convolution_map THEN
 395      ASM_REWRITE_TAC[]);;
 396
 397
 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
 403      STRIP_TAC 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
 408      DISCH_TAC THEN
 409      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 410      DISCH_TAC 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
 415      [
 416        REWRITE_TAC[node_map_injective];
 417        ALL_TAC
 418      ] THEN
 419      FIRST_X_ASSUM MATCH_MP_TAC THEN
 420      CONJ_TAC THENL
 421      [
 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
 425          [
 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];
 430            ALL_TAC
 431          ] THEN
 432          ASM_REWRITE_TAC[]
 433      ]);;
 434
 435
 436
 437 (* LEMMA: aux *)
 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`,
 441    GEN_TAC THEN
 442      REWRITE_TAC[plain_hypermap; is_edge_nondegenerate] THEN
 443      STRIP_TAC 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]);;
 454
 455
 456 (* LEMMA: aux *)
 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`,
 460    GEN_TAC THEN
 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
 464      ARITH_TAC);;
 465
 466
 467
 468
 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]);;
 481
 482
 483
 484
 485 (* LEMMA: tame_8 *)
 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]);;
 489
 490
 491
 492 (* LEMMA: tame_9a *)
 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]);;
 497
 498
 499 (* LEMMA: tame_10 *)
 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]);;
 503
 504
 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]);;
 511
 512
 513
 514 (* LEMMA: general *)
 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`,
 518    REPEAT GEN_TAC THEN
 519      REWRITE_TAC[set_of_triangles_meeting_node] THEN
 520      REWRITE_TAC[opposite_components] THEN
 521      REWRITE_TAC[dart; tuple_opposite_hypermap]);;
 522
 523
 524 (* LEMMA: general *)
 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`,
 528    REPEAT GEN_TAC THEN
 529      REWRITE_TAC[set_of_quadrilaterals_meeting_node] THEN
 530      REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
 531
 532
 533 (* LEMMA: general *)
 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`,
 537    REPEAT GEN_TAC THEN
 538      REWRITE_TAC[set_of_exceptional_meeting_node] THEN
 539      REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
 540
 541
 542
 543 (* LEMMA: general *)
 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`,
 546    REPEAT GEN_TAC THEN
 547      REWRITE_TAC[set_of_face_meeting_node] THEN
 548      REWRITE_TAC[opposite_components; dart; tuple_opposite_hypermap]);;
 549
 550
 551 (* LEMMA: general *)
 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]);;
 557
 558
 559
 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]);;
 567
 568
 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
 580      STRIP_TAC 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]);;
 586
 587
 588
 589
 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]);;
 597
 598
 599
 600
 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
 604      [
 605        REWRITE_TAC[tame_opposite_hypermap];
 606        DISCH_TAC THEN
 607          ONCE_REWRITE_TAC[GSYM opposite_opposite_hypermap_eq_hypermap] THEN
 608          MATCH_MP_TAC tame_opposite_hypermap THEN
 609          ASM_REWRITE_TAC[]
 610      ]);;
 611
 612
 613
 614
 615
 616 end;;