formal_lp/old/ineqs/list_hypermap_iso.hl

   1 needs "../formal_lp/hypermap/list_hypermap.hl";;
   2 needs "tame/tame_defs.hl";;
   3
   4 open Hypermap_and_fan;;
   5 open Tame_defs;;
   6
   7
   8 let IN_TRANS = prove(`!(x:A) s t. t SUBSET s /\ x IN t ==> x IN s`,
   9    SET_TAC[]);;
  10
  11
  12
  13
  14 (* TODO: move to HypermapAndFan.hl *)
  15 let FST_NODE_HYPERMAP_OF_FAN = prove(`!V E x y. FAN (vec 0,V,E) /\
  16                                        x IN node (hypermap_of_fan (V,E)) y
  17                                        ==> FST x = FST y`,
  18    REPEAT STRIP_TAC THEN
  19      MATCH_MP_TAC FAN_NODE_EQ_lemma THEN
  20      MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
  21      ASM_REWRITE_TAC[] THEN
  22      MATCH_MP_TAC EQ_SYM THEN
  23      MATCH_MP_TAC Hypermap.lemma_node_identity THEN
  24      ASM_REWRITE_TAC[]);;
  25
  26 let E_FAN_PAIR_EXT_EXPLICIT = prove(`!V E v w. (v,w) IN dart_of_fan (V,E)
  27                                       ==> e_fan_pair_ext (V,E) (v,w) = (w,v)`,
  28    REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION] THEN
  29      REPEAT GEN_TAC THEN
  30      REWRITE_TAC[Fan_defs.e_fan_pair_ext] THEN
  31      COND_CASES_TAC THEN REWRITE_TAC[Fan_defs.e_fan_pair] THEN
  32      REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
  33      STRIP_TAC THEN
  34      ASM_REWRITE_TAC[]);;
  35
  36 let DART_OF_FAN_SYM = prove(`!V E v w. (v,w) IN dart_of_fan (V,E) <=> (w,v) IN dart_of_fan (V,E)`,
  37    GEN_TAC THEN GEN_TAC THEN
  38      SUBGOAL_THEN `!v w. (v,w) IN dart_of_fan (V,E) ==> (w,v) IN dart_of_fan (V,E)` ASSUME_TAC THENL
  39      [
  40        REWRITE_TAC[dart_of_fan; IN_UNION; IN_ELIM_THM; PAIR_EQ] THEN
  41          REPEAT STRIP_TAC THENL
  42          [
  43            DISJ1_TAC THEN
  44              EXISTS_TAC `v':real^3` THEN
  45              ASM_REWRITE_TAC[];
  46            ALL_TAC
  47          ] THEN
  48          DISJ2_TAC THEN
  49          MAP_EVERY EXISTS_TAC [`w':real^3`; `v':real^3`] THEN
  50          ASM_REWRITE_TAC[Collect_geom.PER_SET2];
  51        ALL_TAC
  52      ] THEN
  53      REPEAT GEN_TAC THEN EQ_TAC THEN ASM_REWRITE_TAC[]);;
  54
  55
  56
  57
  58
  59 (* Isomorphism between hypermap_of_fan and hypermap_of_list *)
  60
  61 let isomorphism = new_definition `isomorphism f (H, G) <=>
  62                           BIJ f (dart H) (dart G) /\
  63                           (!x. x IN dart H ==>
  64                              edge_map G (f x) = f (edge_map H x) /\
  65                              node_map G (f x) = f (node_map H x) /\
  66                              face_map G (f x) = f (face_map H x))`;;
  67
  68
  69 let res_inverse = new_definition `res_inverse f s = (\y. @x. f x = y /\ x IN s)`;;
  70
  71
  72 let INJ_IMP_RES_INVERSE = prove(`!(f:A->B) s t. INJ f s t ==>
  73                               (!x. x IN s ==> res_inverse f s (f x) = x)`,
  74    REWRITE_TAC[INJ] THEN
  75      REPEAT STRIP_TAC THEN
  76      REWRITE_TAC[res_inverse] THEN
  77      MATCH_MP_TAC SELECT_UNIQUE THEN
  78      REWRITE_TAC[] THEN
  79      GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  80      FIRST_X_ASSUM MATCH_MP_TAC THEN
  81      ASM_REWRITE_TAC[]);;
  82
  83
  84 let SURJ_IMP_RES_INVERSE = prove(`!(f:A->B) s t. SURJ f s t ==>
  85        (!y. y IN t ==> f (res_inverse f s y) = y /\ res_inverse f s y IN s)`,
  86    REWRITE_TAC[SURJ; res_inverse] THEN
  87      REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
  88      MP_TAC (ISPEC `\x. (f:A->B) x = y /\ x IN s` SELECT_AX) THEN
  89      FIRST_X_ASSUM (MP_TAC o SPEC `y:B`) THEN
  90      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  91      DISCH_THEN (MP_TAC o SPEC `y':A`) THEN
  92      ASM_SIMP_TAC[]);;
  93
  94
  95 let BIJ_IMP_RES_INVERSE = prove(`!(f:A->B) s t. BIJ f s t ==>
  96         (!x. x IN s ==> res_inverse f s (f x) = x) /\
  97         (!y. y IN t ==> f (res_inverse f s y) = y) /\
  98         (!y. y IN t ==> res_inverse f s y IN s)`,
  99    REWRITE_TAC[BIJ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 100      MP_TAC (SPEC_ALL INJ_IMP_RES_INVERSE) THEN
 101      MP_TAC (SPEC_ALL SURJ_IMP_RES_INVERSE) THEN
 102      ASM_SIMP_TAC[]);;
 103
 104
 105
 106
 107 let INJ_ALT = prove(`!(f:A->B) s t. INJ f s t <=> (!x. x IN s ==> f x IN t) /\
 108                       ?g. !x. x IN s ==> g (f x) = x`,
 109    REPEAT GEN_TAC THEN
 110      EQ_TAC THEN STRIP_TAC THENL
 111      [
 112        CONJ_TAC THENL
 113          [
 114            POP_ASSUM MP_TAC THEN SIMP_TAC[INJ];
 115            ALL_TAC
 116          ] THEN
 117
 118          EXISTS_TAC `res_inverse (f:A->B) s` THEN
 119          MP_TAC (SPEC_ALL INJ_IMP_RES_INVERSE) THEN
 120          ASM_REWRITE_TAC[];
 121        ASM_REWRITE_TAC[INJ] THEN
 122          REPEAT STRIP_TAC THEN
 123          POP_ASSUM (MP_TAC o AP_TERM `g:B->A`) THEN
 124          ASM_SIMP_TAC[]
 125      ]);;
 126
 127
 128 let SURJ_ALT = prove(`!(f:A->B) s t. SURJ f s t <=> (!x. x IN s ==> f x IN t) /\
 129                        ?g. !y. y IN t ==> f (g y) = y /\ g y IN s`,
 130    REPEAT GEN_TAC THEN
 131      EQ_TAC THEN STRIP_TAC THENL
 132      [
 133        CONJ_TAC THENL [ POP_ASSUM MP_TAC THEN SIMP_TAC[SURJ]; ALL_TAC ] THEN
 134          EXISTS_TAC `res_inverse (f:A->B) s` THEN
 135          MP_TAC (SPEC_ALL SURJ_IMP_RES_INVERSE) THEN
 136          ASM_SIMP_TAC[];
 137        ASM_REWRITE_TAC[SURJ] THEN
 138          REPEAT STRIP_TAC THEN
 139          FIRST_X_ASSUM (MP_TAC o SPEC `x:B`) THEN
 140          ASM_REWRITE_TAC[] THEN
 141          DISCH_TAC THEN
 142          EXISTS_TAC `(g:B->A) x` THEN
 143          ASM_REWRITE_TAC[]
 144      ]);;
 145
 146
 147 let BIJ_ALT = prove(`!(f:A->B) s t. BIJ f s t <=> (!x. x IN s ==> f x IN t) /\
 148                       ?g. (!x. x IN s ==> g (f x) = x) /\
 149                           (!y. y IN t ==> f (g y) = y /\ g y IN s)`,
 150    REWRITE_TAC[BIJ] THEN
 151      REPEAT GEN_TAC THEN EQ_TAC THENL
 152      [
 153        STRIP_TAC THEN
 154          MP_TAC (SPEC_ALL INJ_IMP_RES_INVERSE) THEN
 155          MP_TAC (SPEC_ALL SURJ_IMP_RES_INVERSE) THEN
 156          ASM_REWRITE_TAC[] THEN
 157          POP_ASSUM MP_TAC THEN SIMP_TAC[SURJ] THEN
 158          REPEAT STRIP_TAC THEN
 159          EXISTS_TAC `res_inverse (f:A->B) s` THEN
 160          ASM_SIMP_TAC[];
 161        STRIP_TAC THEN
 162          ASM_REWRITE_TAC[INJ_ALT; SURJ_ALT] THEN
 163          CONJ_TAC THEN EXISTS_TAC `g:B->A` THEN ASM_REWRITE_TAC[]
 164      ]);;
 165
 166
 167 let BIJ_RES_INVERSE = prove(`!(f:A->B) s t. BIJ f s t ==> BIJ (res_inverse f s) t s`,
 168    REWRITE_TAC[BIJ] THEN
 169      REPEAT GEN_TAC THEN STRIP_TAC THEN
 170      MP_TAC (SPEC_ALL INJ_IMP_RES_INVERSE) THEN
 171      MP_TAC (SPEC_ALL SURJ_IMP_RES_INVERSE) THEN
 172      ASM_REWRITE_TAC[] THEN
 173
 174      REPEAT STRIP_TAC THENL
 175      [
 176        REWRITE_TAC[INJ_ALT] THEN
 177          ASM_SIMP_TAC[] THEN
 178          EXISTS_TAC `f:A->B` THEN
 179          ASM_SIMP_TAC[];
 180        REWRITE_TAC[SURJ_ALT] THEN
 181          ASM_SIMP_TAC[] THEN
 182          EXISTS_TAC `f:A->B` THEN
 183          ASM_SIMP_TAC[] THEN
 184          UNDISCH_TAC `INJ (f:A->B) s t` THEN
 185          SIMP_TAC[INJ]
 186      ]);;
 187
 188
 189
 190
 191 let RES_INVERSE = prove(`!(f:A->B) g s t. (!y. y IN t ==> g y IN s) /\
 192                           (!x. x IN s ==> g (f x) = x) /\
 193                           (!y. y IN t ==> f (g y) = y)
 194                         ==> (!y. y IN t ==> res_inverse f s y = g y)`,
 195    REPEAT STRIP_TAC THEN
 196      REWRITE_TAC[res_inverse] THEN
 197      MATCH_MP_TAC SELECT_UNIQUE THEN
 198      X_GEN_TAC `v:A` THEN
 199      REWRITE_TAC[] THEN
 200      EQ_TAC THEN STRIP_TAC THENL
 201      [
 202        UNDISCH_TAC `(f:A->B) v = y` THEN
 203          DISCH_THEN (MP_TAC o AP_TERM `g:B->A`) THEN
 204          ASM_SIMP_TAC[];
 205        ASM_SIMP_TAC[]
 206      ]);;
 207
 208
 209
 210 let COMM_RES_INVERSE_LEMMA = prove(`!(f:A->B) s t g1 g2. BIJ f s t /\
 211                                      (!x. x IN s ==> g1 x IN s) /\
 212                                      (!y. y IN t ==> g2 y IN t) /\
 213                                      (!x. x IN s ==> f (g1 x) = g2 (f x))
 214                ==> (!y. y IN t ==> res_inverse f s (g2 y) = g1 (res_inverse f s y))`,
 215    REPEAT STRIP_TAC THEN
 216      MP_TAC (SPEC_ALL BIJ_IMP_RES_INVERSE) THEN
 217      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 218      POP_ASSUM (MP_TAC o SPEC `y:B`) THEN
 219      POP_ASSUM (MP_TAC o SPEC `y:B`) THEN
 220      POP_ASSUM (MP_TAC o SPEC `g1 (res_inverse (f:A->B) s y):A`) THEN
 221      ASM_REWRITE_TAC[] THEN
 222      REPEAT DISCH_TAC THEN
 223      FIRST_X_ASSUM (MP_TAC o SPEC `res_inverse (f:A->B) s y`) THEN
 224      ASM_REWRITE_TAC[] THEN
 225      DISCH_THEN (MP_TAC o AP_TERM `res_inverse (f:A->B) s`) THEN
 226      FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
 227      FIRST_X_ASSUM (MP_TAC o SPEC `res_inverse (f:A->B) s y`) THEN
 228      ASM_SIMP_TAC[]);;
 229
 230
 231 let COMM_RES_INVERSE_LEMMA' = prove(`!(f:A->B) s t g1 g2. BIJ f s t /\
 232                                       g1 permutes s /\ g2 permutes t /\
 233                                       (!x. x IN s ==> f (g1 x) = g2 (f x))
 234                 ==> (!y. y IN t ==> res_inverse f s (g2 y) = g1 (res_inverse f s y))`,
 235    REPEAT GEN_TAC THEN STRIP_TAC THEN
 236      MATCH_MP_TAC COMM_RES_INVERSE_LEMMA THEN
 237      ASM_REWRITE_TAC[] THEN
 238      ASM_SIMP_TAC[PERMUTES_IMP_INSIDE]);;
 239
 240
 241
 242 let ISOMORPHISM_INVERSE = prove(`!(f:A->B) H G. isomorphism f (H, G) ==>
 243                                   isomorphism (res_inverse f (dart H)) (G, H)`,
 244    REWRITE_TAC[isomorphism] THEN
 245      REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
 246      [
 247        ASM_SIMP_TAC[BIJ_RES_INVERSE];
 248        ALL_TAC
 249      ] THEN
 250
 251      REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN SPEC_TAC (`x:B`, `x:B`) THEN
 252      MATCH_MP_TAC (GSYM COMM_RES_INVERSE_LEMMA') THEN
 253      REWRITE_TAC[ETA_AX] THEN
 254      ASM_SIMP_TAC[Hypermap.hypermap_lemma]);;
 255
 256
 257
 258 let POWER_IN_LEMMA = prove(`!g s. (!x:A. x IN s ==> g x IN s)
 259                              ==> (!x n. x IN s ==> (g POWER n) x IN s)`,
 260    REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
 261      INDUCT_TAC THENL
 262      [
 263        REWRITE_TAC[Hypermap.POWER_0; I_THM];
 264        ALL_TAC
 265      ] THEN
 266      ASM_SIMP_TAC[Hypermap.COM_POWER; o_THM]);;
 267
 268
 269
 270
 271 let COMM_POWER_LEMMA = prove(`!(f:A->B) g1 g2 s. (!x. x IN s ==> g1 x IN s) /\
 272                                (!x. x IN s ==> f (g1 x) = g2 (f x))
 273                          ==> (!x n. x IN s ==> f ((g1 POWER n) x) = (g2 POWER n) (f x))`,
 274    REPEAT GEN_TAC THEN STRIP_TAC THEN
 275      GEN_TAC THEN INDUCT_TAC THENL
 276      [
 277        REWRITE_TAC[Hypermap.POWER_0; I_THM];
 278        ALL_TAC
 279      ] THEN
 280      DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o check(is_imp o concl)) THEN
 281      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 282      REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
 283      FIRST_X_ASSUM (MP_TAC o SPEC `(g1 POWER n) (x:A)`) THEN
 284      ASM_SIMP_TAC[POWER_IN_LEMMA]);;
 285
 286
 287
 288 let COMM_POWER_LEMMA_PERMUTES = prove(`!(f:A->B) g1 g2 s. g1 permutes s /\
 289                                         (!x. x IN s ==> f (g1 x) = g2 (f x))
 290                         ==> (!x n. x IN s ==> f ((g1 POWER n) x) = (g2 POWER n) (f x))`,
 291    REPEAT GEN_TAC THEN STRIP_TAC THEN
 292      MATCH_MP_TAC COMM_POWER_LEMMA THEN
 293      ASM_SIMP_TAC[PERMUTES_IMP_INSIDE]);;
 294
 295
 296
 297 let COMM_INVERSE_LEMMA = prove(`!(f:A->B) g1 g2 s t x. FINITE s /\
 298                                  g1 permutes s /\ g2 permutes t /\
 299                                  (!x. x IN s ==> f (g1 x) = g2 (f x)) /\ x IN s
 300                                  ==> f (inverse g1 x) = inverse g2 (f x)`,
 301    REPEAT STRIP_TAC THEN
 302      MP_TAC (ISPECL[`s:A->bool`; `g1:A->A`] Hypermap.inverse_element_lemma) THEN
 303      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 304      ASM_REWRITE_TAC[] THEN
 305      SUBGOAL_THEN `inverse g2 (f x) = (g2 POWER j) ((f:A->B) x)` (fun th -> REWRITE_TAC[th]) THENL
 306      [
 307        MATCH_MP_TAC (GSYM Hypermap.inverse_function) THEN
 308          EXISTS_TAC `t:B->bool` THEN
 309          ASM_REWRITE_TAC[] THEN
 310          MP_TAC (SPEC_ALL COMM_POWER_LEMMA_PERMUTES) THEN
 311          ASM_REWRITE_TAC[] THEN
 312          DISCH_THEN (MP_TAC o SPECL [`x:A`; `j:num`]) THEN
 313          ASM_REWRITE_TAC[] THEN
 314          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 315          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 316          FIRST_X_ASSUM (MP_TAC o SPEC `inverse (g1:A->A) (x:A)`) THEN
 317          ANTS_TAC THENL
 318          [
 319            MP_TAC (ISPECL [`inverse (g1:A->A)`; `s:A->bool`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
 320              ASM_SIMP_TAC[PERMUTES_INVERSE];
 321            ALL_TAC
 322          ] THEN
 323          DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 324          MP_TAC (ISPECL [`g1:A->A`; `s:A->bool`] PERMUTES_INVERSES) THEN
 325          ASM_SIMP_TAC[];
 326        ALL_TAC
 327      ] THEN
 328      MP_TAC (SPEC_ALL COMM_POWER_LEMMA_PERMUTES) THEN
 329      ASM_REWRITE_TAC[] THEN
 330      DISCH_THEN MATCH_MP_TAC THEN
 331      ASM_REWRITE_TAC[]);;
 332
 333
 334
 335
 336
 337
 338 let COMM_ORBIT_IMAGE_LEMMA = prove(`!(f:A->B) s g1 g2. (!x. x IN s ==> g1 x IN s) /\
 339                                      (!x. x IN s ==> f (g1 x) = g2 (f x))
 340                 ==> (!x. x IN s ==> orbit_map g2 (f x) = IMAGE f (orbit_map g1 x))`,
 341    REPEAT STRIP_TAC THEN
 342      REWRITE_TAC[Hypermap.orbit_map] THEN
 343      MP_TAC (SPEC_ALL COMM_POWER_LEMMA) THEN
 344      ASM_REWRITE_TAC[] THEN
 345      DISCH_THEN (MP_TAC o SPEC `x:A`) THEN
 346      ASM_REWRITE_TAC[] THEN
 347      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
 348      REWRITE_TAC[GSYM IMAGE_LEMMA; IN_ELIM_THM] THEN
 349      SET_TAC[]);;
 350
 351
 352
 353 let COMM_ORBIT_IMAGE_LEMMA_PERMUTES = prove(`!(f:A->B) s g1 g2 y. y IN s /\ g1 permutes s /\
 354                                               (!x. x IN s ==> f (g1 x) = g2 (f x))
 355                 ==> orbit_map g2 (f y) = IMAGE f (orbit_map g1 y)`,
 356    REPEAT GEN_TAC THEN STRIP_TAC THEN
 357      MP_TAC (SPEC_ALL COMM_ORBIT_IMAGE_LEMMA) THEN
 358      ASM_SIMP_TAC[PERMUTES_IMP_INSIDE]);;
 359
 360
 361
 362 let ISOMORPHISM_COMPONENT_IMAGE = prove(`!(f:A->B) H G d. isomorphism f (H,G) /\ d IN dart H
 363                 ==> node G (f d) = IMAGE f (node H d) /\
 364                     edge G (f d) = IMAGE f (edge H d) /\
 365                     face G (f d) = IMAGE f (face H d)`,
 366    REWRITE_TAC[isomorphism] THEN
 367      REPEAT GEN_TAC THEN STRIP_TAC THEN
 368      REWRITE_TAC[Hypermap.node; Hypermap.edge; Hypermap.face] THEN
 369      REPEAT CONJ_TAC THEN MATCH_MP_TAC COMM_ORBIT_IMAGE_LEMMA_PERMUTES THEN
 370      EXISTS_TAC `dart H:A->bool` THEN
 371      ASM_SIMP_TAC[Hypermap.hypermap_lemma]);;
 372
 373
 374
 375
 376 let ISOMORPHISM_IMP_ISO = prove(`!(f:A->B) H G. isomorphism f (H, G)
 377                                   ==> iso H G`,
 378    REWRITE_TAC[isomorphism; Hypermap.iso] THEN
 379      REPEAT STRIP_TAC THEN
 380      EXISTS_TAC `f:A->B` THEN
 381      ASM_REWRITE_TAC[] THEN
 382      REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 383      REWRITE_TAC[FUN_EQ_THM; o_THM] THEN
 384      SIMP_TAC[]);;
 385
 386
 387 let ISO_IMP_ISOMORPHISM = prove(`!H G. iso H G ==> ?f:A->B. isomorphism f (H, G)`,
 388    REWRITE_TAC[Hypermap.iso; isomorphism]);;
 389
 390
 391
 392
 393
 394
 395
 396
 397 let ISOMORPHISM_FAN_LIST = prove(`!V E L (f:real^3#real^3->A#A). FAN (vec 0,V,E) /\
 398                                    good_list L /\ good_list_nodes L /\
 399                                    isomorphism f (hypermap_of_fan (V,E), hypermap_of_list L)
 400            ==> ?h. BIJ h V (elements_of_list L) /\
 401                    (!d. d IN dart_of_fan (V,E) ==> f d = (h (FST d), h (SND d)))`,
 402    REPEAT GEN_TAC THEN STRIP_TAC THEN
 403      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[isomorphism] THEN STRIP_TAC THEN
 404      SUBGOAL_THEN `!d:real^3#real^3. d IN dart_of_fan (V,E) ==> (f d):A#A IN darts_of_list L` ASSUME_TAC THENL
 405      [
 406        REPEAT STRIP_TAC THEN
 407          FIRST_X_ASSUM (MP_TAC o check(fun th -> (fst o dest_const o rator o rator o rator o concl) th = "BIJ")) THEN
 408          REWRITE_TAC[BIJ; INJ] THEN
 409          DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (fun th -> ALL_TAC)) THEN
 410          DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (fun th -> ALL_TAC)) THEN
 411          DISCH_THEN (MP_TAC o SPEC `d:real^3#real^3`) THEN
 412          ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN; COMPONENTS_HYPERMAP_OF_LIST];
 413        ALL_TAC
 414      ] THEN
 415
 416      ABBREV_TAC `h = (\v. FST ((f:real^3#real^3->A#A) (v, if (v,v) IN dart_of_fan (V,E) then v else CHOICE (set_of_edge v V E))))` THEN
 417      EXISTS_TAC `h:real^3->A` THEN
 418      SUBGOAL_THEN `?g. !v w:real^3. (v,w) IN dart_of_fan (V,E) ==> f(v,w) = (h v:A, g (v,w):A)` ASSUME_TAC THENL
 419      [
 420        EXISTS_TAC `\d:real^3#real^3. SND (f d:A#A)` THEN
 421          REPEAT STRIP_TAC THEN
 422          REWRITE_TAC[] THEN
 423          MP_TAC (ISPEC `(f:real^3#real^3->A#A) (v,w)` PAIR_SURJECTIVE) THEN
 424          STRIP_TAC THEN
 425          ASM_REWRITE_TAC[PAIR_EQ] THEN
 426          EXPAND_TAC "h" THEN
 427          COND_CASES_TAC THENL
 428          [
 429            SUBGOAL_THEN `set_of_edge (v:real^3) V E = {}` ASSUME_TAC THENL
 430              [
 431                POP_ASSUM MP_TAC THEN
 432                  REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION; IN_ELIM_THM] THEN
 433                  STRIP_TAC THENL
 434                  [
 435                    POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
 436                      ASM_SIMP_TAC[];
 437                    ALL_TAC
 438                  ] THEN
 439
 440                  MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `v:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
 441                  ASM_REWRITE_TAC[];
 442                ALL_TAC
 443              ] THEN
 444
 445              UNDISCH_TAC `v,w IN dart_of_fan (V:real^3->bool, E)` THEN
 446              REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION; IN_ELIM_THM] THEN
 447              STRIP_TAC THENL
 448              [
 449                POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
 450                  DISCH_TAC THEN
 451                  UNDISCH_TAC `f(v:real^3,w:real^3) = x:A,y:A` THEN
 452                  ASM_SIMP_TAC[];
 453                ALL_TAC
 454              ] THEN
 455
 456              MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN) THEN
 457              ASM_REWRITE_TAC[NOT_IN_EMPTY];
 458            ALL_TAC
 459          ] THEN
 460
 461          SUBGOAL_THEN `v,w IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
 462          [
 463            UNDISCH_TAC `v,w IN dart_of_fan (V:real^3->bool,E)` THEN
 464              DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN
 465              REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_ELIM_THM; IN_UNION] THEN
 466              STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 467              POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
 468              DISCH_TAC THEN
 469              UNDISCH_TAC `v,w IN dart_of_fan (V:real^3->bool,E)` THEN
 470              UNDISCH_TAC `~(v,v IN dart_of_fan (V:real^3->bool,E))` THEN
 471              ASM_SIMP_TAC[];
 472            ALL_TAC
 473          ] THEN
 474
 475          ABBREV_TAC `w' = CHOICE (set_of_edge (v:real^3) V E)` THEN
 476
 477          SUBGOAL_THEN `(v,w') IN node (hypermap_of_fan (V,E)) (v,w)` MP_TAC THENL
 478          [
 479            ASM_SIMP_TAC[Hypermap_and_fan.NODE_HYPERMAP_OF_FAN_ALT] THEN
 480              REWRITE_TAC[IN_ELIM_THM] THEN
 481              EXISTS_TAC `w':real^3` THEN
 482              REWRITE_TAC[] THEN
 483              EXPAND_TAC "w'" THEN
 484              MATCH_MP_TAC CHOICE_DEF THEN
 485              DISCH_TAC THEN
 486              MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN) THEN
 487              ASM_REWRITE_TAC[NOT_IN_EMPTY];
 488            ALL_TAC
 489          ] THEN
 490
 491          REWRITE_TAC[Hypermap.node; Hypermap.node_map] THEN
 492          ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
 493          REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN
 494          STRIP_TAC THEN
 495          ASM_REWRITE_TAC[] THEN
 496          MP_TAC (ISPECL [`f:real^3#real^3->A#A`; `node_map (hypermap_of_fan (V,E))`; `node_map (hypermap_of_list (L:((A)list)list))`; `dart (hypermap_of_fan (V,E))`] COMM_POWER_LEMMA_PERMUTES) THEN
 497          ASM_SIMP_TAC[Hypermap.hypermap_lemma] THEN
 498          DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
 499          DISCH_THEN (MP_TAC o SPEC `n:num`) THEN
 500          ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN] THEN
 501          DISCH_THEN (fun th -> ALL_TAC) THEN
 502          ASM_SIMP_TAC[Hypermap.node_map; HYPERMAP_OF_LIST] THEN
 503
 504          MATCH_MP_TAC (GSYM FST_N_LIST_EXT_POWER) THEN
 505          ASM_REWRITE_TAC[] THEN
 506          FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
 507          ASM_REWRITE_TAC[];
 508        ALL_TAC
 509      ] THEN
 510
 511      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 512
 513      REPEAT STRIP_TAC THENL
 514      [
 515        REWRITE_TAC[BIJ; INJ; SURJ] THEN
 516          SUBGOAL_THEN `!x:real^3. x IN V ==> (h x):A IN elements_of_list L` ASSUME_TAC THENL
 517          [
 518            REWRITE_TAC[elements_of_list; IN_SET_OF_LIST] THEN
 519              REWRITE_TAC[MEM_LIST_OF_ELEMENTS] THEN
 520              X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
 521              MP_TAC (SPEC_ALL DART_EXISTS) THEN
 522              ASM_REWRITE_TAC[] THEN
 523              STRIP_TAC THEN
 524              FIRST_X_ASSUM (MP_TAC o SPECL[`v:real^3`; `w:real^3`]) THEN
 525              ASM_REWRITE_TAC[] THEN
 526              DISCH_TAC THEN
 527              EXISTS_TAC `g (v:real^3,w:real^3):A` THEN
 528              POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 529              REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list] THEN
 530              FIRST_X_ASSUM MATCH_MP_TAC THEN
 531              ASM_REWRITE_TAC[];
 532            ALL_TAC
 533          ] THEN
 534
 535          ASM_REWRITE_TAC[] THEN
 536          CONJ_TAC THENL
 537          [
 538            MAP_EVERY X_GEN_TAC [`v1:real^3`; `v2:real^3`] THEN
 539              STRIP_TAC THEN
 540              MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v1:real^3`] DART_EXISTS) THEN
 541              MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v2:real^3`] DART_EXISTS) THEN
 542              ASM_REWRITE_TAC[] THEN
 543              DISCH_THEN (X_CHOOSE_THEN `w2:real^3` ASSUME_TAC) THEN
 544              DISCH_THEN (X_CHOOSE_THEN `w1:real^3` ASSUME_TAC) THEN
 545              ABBREV_TAC `d1:A#A = f (v1:real^3,w1:real^3)` THEN
 546              ABBREV_TAC `d2:A#A = f (v2:real^3,w2:real^3)` THEN
 547              SUBGOAL_THEN `MEM (d1:A#A) (list_of_darts L) /\ MEM (d2:A#A) (list_of_darts L)` ASSUME_TAC THENL
 548              [
 549                REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list] THEN
 550                  POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 551                  POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 552                  ASM_SIMP_TAC[];
 553                ALL_TAC
 554              ] THEN
 555
 556              SUBGOAL_THEN `d1:A#A IN node (hypermap_of_list L) d2` MP_TAC THENL
 557              [
 558                FIRST_ASSUM MP_TAC THEN REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list] THEN
 559                  DISCH_TAC THEN
 560                  ASM_SIMP_TAC[GOOD_LIST_NODE] THEN
 561                  REWRITE_TAC[IN_ELIM_THM] THEN
 562                  EXISTS_TAC `SND (d1:A#A)` THEN
 563                  SUBGOAL_THEN `FST (d2:A#A) = FST (d1:A#A)` ASSUME_TAC THENL
 564                  [
 565                    FIRST_ASSUM (MP_TAC o SPECL [`v2:real^3`; `w2:real^3`]) THEN
 566                      FIRST_X_ASSUM (MP_TAC o SPECL [`v1:real^3`; `w1:real^3`]) THEN
 567                      ASM_SIMP_TAC[];
 568                    ALL_TAC
 569                  ] THEN
 570                  ASM_REWRITE_TAC[];
 571                ALL_TAC
 572              ] THEN
 573
 574              MP_TAC (ISPECL [`f:real^3#real^3->A#A`; `hypermap_of_fan (V,E)`; `hypermap_of_list (L:((A)list)list)`; `(v2:real^3,w2:real^3)`] ISOMORPHISM_COMPONENT_IMAGE) THEN
 575              ANTS_TAC THENL
 576              [
 577                ASM_REWRITE_TAC[] THEN
 578                  ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN];
 579                ALL_TAC
 580              ] THEN
 581              ASM_REWRITE_TAC[] THEN
 582              DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 583
 584              REWRITE_TAC[IN_IMAGE] THEN
 585              STRIP_TAC THEN
 586              SUBGOAL_THEN `x = (v1:real^3,w1:real^3)` ASSUME_TAC THENL
 587              [
 588                UNDISCH_TAC `BIJ f (dart (hypermap_of_fan (V,E))) (dart (hypermap_of_list (L:((A)list)list)))` THEN
 589                  REWRITE_TAC[BIJ; INJ] THEN
 590                  STRIP_TAC THEN
 591                  FIRST_X_ASSUM MATCH_MP_TAC THEN
 592                  ASM_REWRITE_TAC[] THEN
 593                  CONJ_TAC THENL
 594                  [
 595                    MATCH_MP_TAC IN_TRANS THEN
 596                      EXISTS_TAC `node (hypermap_of_fan (V,E)) (v2,w2)` THEN
 597                      ASM_REWRITE_TAC[] THEN
 598                      MATCH_MP_TAC Hypermap.lemma_node_subset THEN
 599                      ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN];
 600                    ALL_TAC
 601                  ] THEN
 602                  ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN];
 603                ALL_TAC
 604              ] THEN
 605
 606              UNDISCH_TAC `x IN node (hypermap_of_fan (V,E)) (v2,w2)` THEN
 607              POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 608              DISCH_TAC THEN
 609              MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v1:real^3,w1:real^3`; `v2:real^3,w2:real^3`] FST_NODE_HYPERMAP_OF_FAN) THEN
 610              ASM_REWRITE_TAC[];
 611            ALL_TAC
 612          ] THEN
 613
 614          REWRITE_TAC[elements_of_list; IN_SET_OF_LIST; MEM_LIST_OF_ELEMENTS] THEN
 615          REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list] THEN
 616          REPEAT STRIP_TAC THEN
 617          UNDISCH_TAC `BIJ f (dart (hypermap_of_fan (V,E))) (dart (hypermap_of_list (L:((A)list)list)))` THEN
 618          REWRITE_TAC[BIJ; SURJ] THEN
 619          STRIP_TAC THEN
 620          FIRST_X_ASSUM (MP_TAC o SPEC `x:A,y:A`) THEN
 621          ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST; COMPONENTS_HYPERMAP_OF_FAN] THEN
 622          DISCH_THEN (X_CHOOSE_THEN `d:real^3#real^3` MP_TAC) THEN STRIP_TAC THEN
 623          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `d:real^3#real^3`] IN_DART_OF_FAN) THEN
 624          ASM_REWRITE_TAC[] THEN
 625          STRIP_TAC THEN
 626          EXISTS_TAC `v:real^3` THEN
 627          ASM_REWRITE_TAC[] THEN
 628          FIRST_X_ASSUM (MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
 629          UNDISCH_TAC `f (d:real^3#real^3) = x:A,y:A` THEN
 630          ASM_REWRITE_TAC[] THEN
 631          DISCH_THEN (fun th -> SIMP_TAC[th; PAIR_EQ]);
 632        ALL_TAC
 633      ] THEN
 634
 635      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `d:real^3#real^3`] IN_DART_OF_FAN) THEN
 636      ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN STRIP_TAC THEN
 637      FIRST_ASSUM (MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
 638      UNDISCH_TAC `v:real^3,w:real^3 IN dart_of_fan (V,E)` THEN
 639      DISCH_TAC THEN FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 640      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 641      ASM_REWRITE_TAC[PAIR_EQ] THEN
 642
 643      FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
 644      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 645      FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
 646      ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_FAN] THEN
 647
 648      DISCH_THEN (MP_TAC o CONJUNCT1) THEN
 649      ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
 650      ASM_REWRITE_TAC[e_list_ext; res] THEN
 651      ASM_SIMP_TAC[E_FAN_PAIR_EXT_EXPLICIT] THEN
 652      REWRITE_TAC[e_list] THEN
 653      FIRST_X_ASSUM (MP_TAC o SPECL [`w:real^3`; `v:real^3`]) THEN
 654      ASM_REWRITE_TAC[DART_OF_FAN_SYM] THEN
 655      SIMP_TAC[PAIR_EQ]);;
 656
 657
 658
 659 (*
 660 prove(`!(H:(A)hypermap) P k. is_no_double_joints H /\ connected_hypermap H /\
 661         plain_hypermap H /\
 662         (!x. x IN dart H ==> P x (node_map H x) /\ ~(P x (edge_map H x)))
 663         ==>
 664         (!x y g n. x IN dart H /\ y IN dart H /\ n <= k /\ P x y /\
 665            x = g 0 /\ y = g n /\ is_path H g n
 666              ==> y IN node H x) /\
 667         (!x y g n t. x IN dart H /\ y IN dart H /\ n <= k /\ P x y /\
 668            x = g 0 /\ y = (edge_map H o (node_map H POWER t) o g) n /\ is_path H g n
 669              ==> y IN node H x)`,
 670    REWRITE_TAC[is_no_double_joints]
 671
 672 *)