text_formalization/fan/HypermapAndFan.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                                               *)
   5 (* Author: Alexey Solovyev                                                    *)
   6 (* Date: 2010-06-16                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11 flyspeck_needs "fan/fan_defs.hl";;
  12 flyspeck_needs "fan/introduction.hl";;
  13 flyspeck_needs "fan/topology.hl";;
  14 flyspeck_needs "fan/fan_misc.hl";;
  15
  16
  17
  18 module Hypermap_and_fan (* : Hypermap_and_fan_type *) = struct
  19
  20
  21 (* Several tactics and simple lemmas *)
  22
  23 let REMOVE_ASSUM = POP_ASSUM(fun th -> ALL_TAC);;
  24
  25 let let_RULE = fun th -> REWRITE_RULE[DEPTH_CONV let_CONV (concl th)] th;;
  26
  27 let IMAGE_LEMMA = prove(`!f s. {f x | x IN s} = IMAGE f s`, SET_TAC[IMAGE]);;
  28
  29 let CHOICE_LEMMA = MESON[] `!y (P:A->bool). ((?x. P x) /\ (!x. P x ==> (x = y))) ==> (@x. P x) = y`;;
  30
  31 let INVERSE_LEMMA = prove(`!f y. (?!x. f x = y) ==> f((inverse f) y) = y`, MESON_TAC[inverse]);;
  32
  33 let PERMUTES_IMP_INSIDE = prove(`!f s. f permutes s ==> (!x. x IN s ==> f x IN s)`,
  34                                                         REPEAT GEN_TAC THEN
  35                                                         DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMAGE th)) THEN
  36                                                         SET_TAC[]);;
  37
  38
  39 (* Open relevant modules *)
  40
  41 open Fan_defs;;
  42 open Fan_misc;;
  43
  44
  45 (* Properties of restricted functions *)
  46
  47 let RES_RES = prove(`!f s. res (res f s) s = res f s`,
  48                     SIMP_TAC[FUN_EQ_THM; Sphere.res]);;
  49
  50
  51 let RES_RES2 = prove(`!f s t. res (res f s) t = res f (s INTER t)`,
  52                      REWRITE_TAC[FUN_EQ_THM; Sphere.res; IN_INTER] THEN MESON_TAC[]);;
  53
  54
  55 let RES_DECOMPOSITION = prove(`!(f:A->A) s. (!x. x IN s ==> f x IN s) ==> f = (res f (UNIV DIFF s)) o res f s`,
  56    REWRITE_TAC[FUN_EQ_THM; o_THM; Sphere.res] THEN REPEAT STRIP_TAC THEN
  57      DISJ_CASES_TAC (TAUT `x:A IN s \/ ~(x IN s)`) THENL
  58      [
  59        SUBGOAL_THEN `~(x IN (:A) DIFF s)` ASSUME_TAC THENL [ ASM SET_TAC[]; ALL_TAC ] THEN
  60          ASM_SIMP_TAC[] THEN
  61          SUBGOAL_TAC "A" `~((f:(A->A)) x IN (:A) DIFF s)` [ ASM SET_TAC[]; ALL_TAC ] THEN
  62          ASM_SIMP_TAC[];
  63
  64        SUBGOAL_TAC "A" `x IN (:A) DIFF s` [ ASM SET_TAC[] ] THEN
  65          ASM_SIMP_TAC[]
  66      ]);;
  67
  68
  69 let RES_EMPTY = prove(`!f. res f {} = I`,
  70                       REWRITE_TAC[FUN_EQ_THM; I_THM; Sphere.res; NOT_IN_EMPTY]);;
  71
  72
  73 let PERMUTES_IMP_RES_EQ_FUN = prove(`!f s. f permutes s ==> res f s = f`,
  74                 REWRITE_TAC[permutes; Sphere.res; FUN_EQ_THM] THEN SET_TAC[]);;
  75
  76
  77 let RES_PERMUTES_UNION = prove(`!f A B. f permutes A ==>
  78                                  (res f A) permutes (A UNION B)`,
  79    REWRITE_TAC[permutes; Sphere.res] THEN
  80      SET_TAC[]);;
  81
  82
  83 let RES_PERMUTES_DISJOINT_UNIONS = prove(`!(f:A->A) c. (!t. t IN c ==> res f t permutes t)
  84                                        /\ (!a b. a IN c /\ b IN c /\ ~(a = b) ==> DISJOINT a b)
  85                                        ==> res f (UNIONS c) permutes (UNIONS c)`,
  86   REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "A") ASSUME_TAC) THEN
  87     SUBGOAL_THEN `!t. t IN c ==> (!y:A. y IN t ==> f y IN t)` (LABEL_TAC "B") THENL
  88     [
  89       GEN_TAC THEN DISCH_TAC THEN
  90         REMOVE_THEN "A" (MP_TAC o SPEC `t:A->bool`) THEN
  91         ASM_REWRITE_TAC[] THEN
  92         DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMP_INSIDE th)) THEN
  93         REWRITE_TAC[Sphere.res] THEN
  94         MESON_TAC[];
  95       ALL_TAC
  96     ] THEN
  97     REMOVE_THEN "A" MP_TAC THEN
  98     REWRITE_TAC[permutes] THEN SIMP_TAC[Sphere.res] THEN
  99     ASM SET_TAC[]);;
 100
 101
 102 let RES_PERMUTES = prove(`!(f:A->A) s. (!x. x IN s ==> f x IN s)
 103                   /\ (!y. y IN s ==> (?x. x IN s /\ y = f x))
 104                   /\ (!x1 x2. x1 IN s /\ x2 IN s /\ f x1 = f x2 ==> x1 = x2)
 105                   ==> res f s permutes s`,
 106   REWRITE_TAC[permutes; Sphere.res] THEN
 107     ASM_MESON_TAC[]);;
 108
 109
 110 (* Hypermap properties *)
 111
 112 (* e_fan_pair_ext permutes dart1_of_fan *)
 113
 114 let E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN = prove(`!V:(A->bool) E. e_fan_pair_ext (V,E) permutes dart1_of_fan (V,E)`,
 115   REPEAT GEN_TAC THEN
 116     REWRITE_TAC[E_FAN_PAIR_EXT] THEN
 117     MATCH_MP_TAC RES_PERMUTES THEN
 118     REWRITE_TAC[dart1_of_fan; IN_ELIM_THM] THEN
 119     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[e_fan_pair] THENL
 120     [
 121       EXISTS_TAC `w:A` THEN EXISTS_TAC `v:A` THEN
 122                 REWRITE_TAC[PAIR_EQ] THEN
 123                 ASM_REWRITE_TAC[SET_RULE `{w,v} = {v,w}`];
 124       EXISTS_TAC `(w:A,v:A)` THEN
 125                 REWRITE_TAC[e_fan_pair; PAIR_EQ] THEN
 126                 EXISTS_TAC `w:A` THEN EXISTS_TAC `v:A` THEN
 127                 ASM_REWRITE_TAC[SET_RULE `{w,v} = {v,w}`];
 128       POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan_pair; PAIR_EQ] THEN
 129                 SIMP_TAC[]
 130     ]);;
 131
 132
 133
 134 let DART1_OF_FAN_EQ_DISJOINT_UNIONS = prove(`!(V:A->bool) E. UNIONS E SUBSET V ==> ?c. dart1_of_fan (V,E) = UNIONS c
 135                                             /\ (!a b. a IN c /\ b IN c /\ ~(a = b) ==> DISJOINT a b)
 136                                             /\ (!a. a IN c ==> (?v. v IN V /\ a = {(v,w) | w | w IN set_of_edge v V E}))`,
 137    REPEAT GEN_TAC THEN DISCH_TAC THEN
 138      SUBGOAL_THEN `!v w:A. {v,w} IN E ==> v IN V /\ w IN V` ASSUME_TAC THENL
 139      [
 140        REPEAT GEN_TAC THEN
 141          POP_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET; IN_UNIONS] THEN
 142          REWRITE_TAC[IMP_IMP] THEN DISCH_THEN (CONJUNCTS_THEN2 (LABEL_TAC "A") ASSUME_TAC) THEN
 143          USE_THEN "A" (MP_TAC o SPEC `v:A`) THEN
 144          REMOVE_THEN "A" (MP_TAC o SPEC `w:A`) THEN
 145          ANTS_TAC THENL [ EXISTS_TAC `{v:A,w}` THEN ASM SET_TAC[]; ALL_TAC ] THEN
 146          DISCH_TAC THEN
 147          ANTS_TAC THENL [ EXISTS_TAC `{v:A,w}` THEN ASM SET_TAC[]; ALL_TAC ] THEN
 148          ASM_REWRITE_TAC[];
 149        ALL_TAC
 150      ] THEN
 151
 152      REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN
 153      ABBREV_TAC `B v = {v:A,w | w | {v,w} IN E /\ w IN V}` THEN
 154      EXISTS_TAC `{(B:A->(A#A->bool)) v | v | (v:A) IN V}` THEN
 155      REPEAT STRIP_TAC THENL
 156      [
 157        REWRITE_TAC[dart1_of_fan] THEN
 158          ASM SET_TAC[];
 159
 160        REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
 161          REWRITE_TAC[IN_ELIM_THM] THEN
 162          STRIP_TAC THEN STRIP_TAC THEN
 163          ASM_REWRITE_TAC[] THEN
 164          DISCH_TAC THEN
 165          SUBGOAL_TAC "A" `~(v:A = v')` [ ASM_MESON_TAC[] ] THEN
 166          REWRITE_TAC[DISJOINT; EXTENSION; NOT_IN_EMPTY; IN_INTER] THEN
 167          GEN_TAC THEN
 168          POP_ASSUM MP_TAC THEN
 169          REWRITE_TAC[TAUT `~A ==> ~B <=> B ==> A`] THEN
 170          REPLICATE_TAC 5 REMOVE_ASSUM THEN
 171          POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]) THEN
 172          REWRITE_TAC[IN_ELIM_THM] THEN
 173          MESON_TAC[PAIR_EQ];
 174
 175        ASM SET_TAC[]
 176      ]);;
 177
 178
 179
 180 (* n_fan_pair_ext permutes dart1_of_fan *)
 181
 182 let N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN = prove(`!V E. FAN (vec 0,V,E) ==> n_fan_pair_ext (V,E) permutes dart1_of_fan (V,E)`,
 183   REPEAT STRIP_TAC THEN
 184     MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] DART1_OF_FAN_EQ_DISJOINT_UNIONS) THEN
 185     FIRST_ASSUM MP_TAC THEN REWRITE_TAC[Fan.FAN] THEN
 186     SIMP_TAC[] THEN DISCH_THEN (fun th -> ALL_TAC) THEN
 187     STRIP_TAC THEN
 188     ASM_REWRITE_TAC[N_FAN_PAIR_EXT] THEN
 189     MATCH_MP_TAC RES_PERMUTES_DISJOINT_UNIONS THEN
 190     ASM_REWRITE_TAC[] THEN
 191     GEN_TAC THEN DISCH_TAC THEN
 192     FIRST_X_ASSUM (MP_TAC o SPEC `t:real^3#real^3->bool`) THEN
 193     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 194
 195     DISJ_CASES_TAC (TAUT `t:real^3#real^3->bool = {} \/ ~(t = {})`) THENL
 196     [
 197       POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
 198         REWRITE_TAC[PERMUTES_EMPTY; RES_EMPTY];
 199       ALL_TAC
 200     ] THEN
 201
 202     SUBGOAL_THEN `extension_sigma_fan (vec 0) V E v permutes set_of_edge v V E ==> res (n_fan_pair (V:real^3->bool,E)) t permutes t` (fun th -> MATCH_MP_TAC th) THENL
 203     [
 204       REMOVE_ASSUM THEN
 205         REWRITE_TAC[Fan.extension_sigma_fan; permutes; Sphere.res] THEN
 206         SIMP_TAC[] THEN DISCH_TAC THEN
 207         GEN_TAC THEN
 208         MP_TAC (ISPEC `y:real^3#real^3` PAIR_SURJECTIVE) THEN
 209         DISCH_THEN (X_CHOOSE_THEN `p:real^3` MP_TAC) THEN
 210         DISCH_THEN (X_CHOOSE_THEN `q:real^3` ASSUME_TAC) THEN
 211         DISJ_CASES_TAC (TAUT `~(p:real^3 = v) \/ p = v`) THENL
 212         [
 213           SUBGOAL_THEN `~(y:real^3#real^3 IN t)` ASSUME_TAC THENL
 214             [
 215               ASM_REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
 216               ALL_TAC
 217             ] THEN
 218
 219             REWRITE_TAC[EXISTS_UNIQUE] THEN
 220             EXISTS_TAC `y:real^3#real^3` THEN
 221             ASM_REWRITE_TAC[] THEN
 222             GEN_TAC THEN
 223             DISJ_CASES_TAC (TAUT `y' IN {v:real^3,w:real^3 | w | w IN set_of_edge v V E} \/ ~(y' IN {v,w | w | w IN set_of_edge v V E})`) THENL
 224             [
 225               ASM_REWRITE_TAC[] THEN
 226                 POP_ASSUM MP_TAC THEN
 227                 REWRITE_TAC[IN_ELIM_THM] THEN
 228                 ASM SET_TAC[n_fan_pair];
 229               ALL_TAC
 230             ] THEN
 231             ASM_SIMP_TAC[PAIR_EQ];
 232           ALL_TAC
 233         ] THEN
 234
 235         FIRST_X_ASSUM (MP_TAC o SPEC `q:real^3`) THEN
 236         ASM_REWRITE_TAC[IN_ELIM_THM] THEN
 237         REWRITE_TAC[EXISTS_UNIQUE] THEN
 238         STRIP_TAC THEN
 239         EXISTS_TAC `(v:real^3,x:real^3)` THEN
 240         REWRITE_TAC[n_fan_pair] THEN
 241         CONJ_TAC THENL
 242         [
 243           REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 244             DISJ_CASES_TAC (TAUT `~(x:real^3 IN set_of_edge v V E) \/ (x IN set_of_edge v V E)`) THENL
 245             [
 246               ASM_SIMP_TAC[] THEN DISCH_TAC THEN
 247                 REWRITE_TAC[PAIR_EQ] THEN
 248                 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 249                 ASM_MESON_TAC[];
 250               ALL_TAC
 251             ] THEN
 252
 253             ASM_MESON_TAC[];
 254           ALL_TAC
 255         ] THEN
 256
 257         GEN_TAC THEN
 258         MP_TAC (ISPEC `y':real^3#real^3` PAIR_SURJECTIVE) THEN
 259         DISCH_THEN (X_CHOOSE_THEN `pp:real^3` MP_TAC) THEN
 260         DISCH_THEN (X_CHOOSE_THEN `qq:real^3` ASSUME_TAC) THEN
 261         POP_ASSUM (fun th -> REWRITE_TAC[th; PAIR_EQ; n_fan_pair]) THEN
 262
 263         DISJ_CASES_TAC (MESON[] `(?w:real^3. w IN set_of_edge v V E /\ pp = v /\ qq = w) \/ ~(?w:real^3. w IN set_of_edge v V E /\ pp = v /\ qq = w)`) THENL
 264         [
 265           ASM_REWRITE_TAC[PAIR_EQ] THEN
 266             SIMP_TAC[] THEN
 267             POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 268             FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`) THEN
 269             ASM_REWRITE_TAC[];
 270           ALL_TAC
 271         ] THEN
 272
 273         ASM_REWRITE_TAC[PAIR_EQ] THEN
 274         SIMP_TAC[] THEN
 275         ASM_MESON_TAC[];
 276
 277       ALL_TAC
 278     ] THEN
 279
 280     MATCH_MP_TAC Fan.permutes_sigma_fan THEN
 281     ASM_REWRITE_TAC[] THEN
 282     SUBGOAL_THEN `?x:real^3#real^3. x IN t` ASSUME_TAC THENL
 283     [
 284       POP_ASSUM MP_TAC THEN
 285         SET_TAC[];
 286       ALL_TAC
 287     ] THEN
 288     POP_ASSUM (CHOOSE_THEN MP_TAC) THEN
 289     ASM_REWRITE_TAC[IN_ELIM_THM; Fan.set_of_edge] THEN
 290     MESON_TAC[]);;
 291
 292
 293
 294 (* e o n o f = I for e_fan_pair_ext, n_fan_pair_ext, f_fan_pair_ext *)
 295
 296 let E_N_F_EQ_I = prove(`!V E. FAN(vec 0,V,E) ==> (e_fan_pair_ext (V,E) o n_fan_pair_ext (V,E) o f_fan_pair_ext (V,E) = I)`,
 297    REPEAT STRIP_TAC THEN
 298      REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN
 299      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 300      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
 301      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
 302      ASM_REWRITE_TAC[] THEN
 303      REWRITE_TAC[I_THM; o_THM] THEN
 304      REWRITE_TAC[f_fan_pair_ext; f_fan_pair; n_fan_pair_ext; n_fan_pair] THEN
 305      DISJ_CASES_TAC (TAUT `~((v:real^3,w:real^3) IN dart1_of_fan (V,E)) \/ (v,w) IN dart1_of_fan (V,E)`) THEN ASM_REWRITE_TAC[] THENL
 306      [
 307        ASM_REWRITE_TAC[e_fan_pair_ext];
 308        ALL_TAC
 309      ] THEN
 310      POP_ASSUM MP_TAC THEN
 311      REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
 312      STRIP_TAC THEN
 313      SUBGOAL_THEN `inverse_sigma_fan (vec 0) V E w (v:real^3) = inverse1_sigma_fan (vec 0) V E w v` (fun th -> REWRITE_TAC[th]) THENL
 314      [
 315        MATCH_MP_TAC (GSYM INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN) THEN
 316          ASM_MESON_TAC[SET_RULE `{w,v} = {v,w}`];
 317        ALL_TAC
 318      ] THEN
 319
 320      SUBGOAL_THEN `?v' w':real^3. {v',w'} IN E /\ w = v' /\ inverse1_sigma_fan (vec 0) V E w v = w'` (fun th -> REWRITE_TAC[th]) THENL
 321      [
 322        MP_TAC (SPECL [`(vec 0):real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`] Fan.INVERSE1_SIGMA_FAN) THEN
 323          ASM_REWRITE_TAC[] THEN
 324          DISCH_THEN (CONJUNCTS_THEN2 (MP_TAC o SPEC `v':real^3`) (fun th -> ALL_TAC)) THEN
 325          ASM_MESON_TAC[SET_RULE `{w,v} = {v,w}`];
 326        ALL_TAC
 327      ] THEN
 328
 329      REWRITE_TAC[n_fan_pair] THEN
 330      MP_TAC (SPECL [`(vec 0):real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`] Fan.INVERSE1_SIGMA_FAN) THEN
 331      ASM_REWRITE_TAC[] THEN
 332      DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
 333      DISCH_THEN (CONJUNCTS_THEN2 (MP_TAC o SPEC `v':real^3`) (fun th -> ALL_TAC)) THEN
 334      ASM_REWRITE_TAC[SET_RULE `{w',v'} = {v',w'}`] THEN
 335      SIMP_TAC[e_fan_pair_ext; e_fan_pair] THEN
 336      SUBGOAL_THEN `w':real^3,v':real^3 IN dart1_of_fan (V,E)` (fun th -> REWRITE_TAC[th]) THEN
 337      REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
 338      ASM_MESON_TAC[SET_RULE `{v',w'} = {w',v'}`]);;
 339
 340
 341
 342 (* f_fan_pair_ext permutes dart1_of_fan *)
 343
 344 let INVERSE_PERMUTES = prove(`!(f:A->A) g s. f permutes s /\ f o g = I ==> g permutes s`,
 345   REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
 346     FIRST_ASSUM (ASSUME_TAC o (fun th -> CONJUNCT2 (MATCH_MP PERMUTES_INVERSES_o th))) THEN
 347     DISCH_THEN (MP_TAC o (fun th -> AP_TERM `(\h:A->A. inverse (f:A->A) o h)` th)) THEN
 348     BETA_TAC THEN
 349     ASM_REWRITE_TAC[o_ASSOC; I_O_ID] THEN
 350     ASM_MESON_TAC[PERMUTES_INVERSE]);;
 351
 352 let F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN = prove(`!V E. FAN (vec 0,V,E) ==> f_fan_pair_ext (V,E) permutes dart1_of_fan (V,E)`,
 353   REPEAT STRIP_TAC THEN
 354     FIRST_ASSUM (ASSUME_TAC o (fun th -> MATCH_MP E_N_F_EQ_I th)) THEN
 355     MATCH_MP_TAC INVERSE_PERMUTES THEN
 356     EXISTS_TAC `e_fan_pair_ext (V:real^3->bool,E) o n_fan_pair_ext (V,E)` THEN
 357     ASM_REWRITE_TAC[GSYM o_ASSOC] THEN
 358     MATCH_MP_TAC PERMUTES_COMPOSE THEN
 359     REWRITE_TAC[E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN] THEN
 360     ASM_SIMP_TAC[N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 361
 362
 363
 364 (* e_fan_pair, n_fan_pair, f_fan_pair map dart1_of_fan into dart1_of_fan *)
 365
 366 let E_N_F_IN_DART1_OF_FAN = prove(`!V E x. FAN(vec 0,V,E) /\ x IN dart1_of_fan (V,E) ==>
 367                                     e_fan_pair (V,E) x IN dart1_of_fan (V,E) /\
 368                                     n_fan_pair (V,E) x IN dart1_of_fan (V,E) /\
 369                                     f_fan_pair (V,E) x IN dart1_of_fan (V,E)`,
 370    REPEAT STRIP_TAC THENL
 371      [
 372        MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN) THEN
 373          DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMP_INSIDE th)) THEN
 374          DISCH_THEN (MP_TAC o SPEC `x:real^3#real^3`) THEN
 375          ASM_REWRITE_TAC[e_fan_pair_ext];
 376        FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN th)) THEN
 377          DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMP_INSIDE th)) THEN
 378          DISCH_THEN (MP_TAC o SPEC `x:real^3#real^3`) THEN
 379          ASM_REWRITE_TAC[n_fan_pair_ext];
 380        FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN th)) THEN
 381          DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMP_INSIDE th)) THEN
 382          DISCH_THEN (MP_TAC o SPEC `x:real^3#real^3`) THEN
 383          ASM_REWRITE_TAC[f_fan_pair_ext];
 384      ]);;
 385
 386
 387 (* inverse (f_fan_pair_ext) maps dart1_of_fan into dart1_of_fan *)
 388
 389 let INVERSE_F_IN_DART1_OF_FAN = prove(`!V E x. FAN(vec 0,V,E) /\ x IN dart1_of_fan (V,E)
 390                                         ==> inverse (f_fan_pair_ext (V,E)) x IN dart1_of_fan (V,E)`,
 391    REPEAT STRIP_TAC THEN
 392      FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN th)) THEN
 393      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_INVERSE th)) THEN
 394      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP PERMUTES_IMP_INSIDE th)) THEN
 395      ASM_SIMP_TAC[]);;
 396
 397
 398
 399
 400 (* dart_of_fan is finite *)
 401
 402 let FINITE_DART_OF_FAN = prove(`!x V E. FAN (x,V,E) ==> FINITE (dart_of_fan (V,E))`,
 403  REWRITE_TAC[Fan.FAN; Fan.fan1; dart_of_fan] THEN
 404    REPEAT GEN_TAC THEN
 405    DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 406    DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) (ASSUME_TAC o CONJUNCT1 o CONJUNCT1)) THEN
 407    REWRITE_TAC[FINITE_UNION] THEN
 408    CONJ_TAC THENL
 409    [
 410      MATCH_MP_TAC FINITE_SUBSET THEN
 411        EXISTS_TAC `{v,v | v IN (V:real^3->bool)}` THEN
 412        CONJ_TAC THENL
 413        [
 414          REWRITE_TAC[IMAGE_LEMMA] THEN
 415            MATCH_MP_TAC FINITE_IMAGE THEN
 416            ASM_REWRITE_TAC[];
 417          ALL_TAC
 418        ] THEN
 419        SET_TAC[];
 420      ALL_TAC
 421    ] THEN
 422
 423    MATCH_MP_TAC FINITE_SUBSET THEN
 424    EXISTS_TAC `{(v:real^3,w) | v, w| v IN V /\ w IN V}` THEN
 425    ASM_SIMP_TAC[FINITE_PRODUCT] THEN
 426    REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 427    REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN
 428    DISCH_TAC THEN
 429    GEN_TAC THEN STRIP_TAC THEN
 430    EXISTS_TAC `v:real^3` THEN EXISTS_TAC `w:real^3` THEN
 431    FIRST_ASSUM (MP_TAC o SPEC `v:real^3`) THEN
 432    FIRST_ASSUM (MP_TAC o SPEC `w:real^3`) THEN
 433    ANTS_TAC THENL [ EXISTS_TAC `{v:real^3,w}` THEN ASM SET_TAC[]; ALL_TAC] THEN
 434    DISCH_TAC THEN
 435    ANTS_TAC THENL [ EXISTS_TAC `{v:real^3,w}` THEN ASM SET_TAC[]; ALL_TAC] THEN
 436    ASM_SIMP_TAC[]);;
 437
 438
 439
 440 (* e_fan_pair_ext permutes dart_of_fan *)
 441
 442 let E_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN = prove(`!(V:real^3->bool) E. e_fan_pair_ext (V,E) permutes dart_of_fan (V,E)`,
 443    REPEAT GEN_TAC THEN
 444      SUBGOAL_TAC "A" `e_fan_pair_ext (V:real^3->bool,E) = res (e_fan_pair_ext (V,E)) (dart1_of_fan (V,E))` [ REWRITE_TAC[E_FAN_PAIR_EXT; RES_RES] ] THEN
 445     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 446     REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan] THEN
 447     ONCE_REWRITE_TAC[UNION_ACI] THEN
 448     MATCH_MP_TAC RES_PERMUTES_UNION THEN
 449     REWRITE_TAC[E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 450
 451
 452 (* f_fan_pair_ext permutes dart_of_fan *)
 453
 454 let F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN = prove(`!(V:real^3->bool) E. FAN (vec 0,V,E) ==> f_fan_pair_ext (V,E) permutes dart_of_fan (V,E)`,
 455    REPEAT STRIP_TAC THEN
 456      SUBGOAL_TAC "A" `f_fan_pair_ext (V:real^3->bool,E) = res (f_fan_pair_ext (V,E)) (dart1_of_fan (V,E))` [ REWRITE_TAC[F_FAN_PAIR_EXT; RES_RES] ] THEN
 457     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 458     REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan] THEN
 459     ONCE_REWRITE_TAC[UNION_ACI] THEN
 460     MATCH_MP_TAC RES_PERMUTES_UNION THEN
 461     ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 462
 463
 464 (* n_fan_pair_ext permutes dart_of_fan *)
 465
 466 let N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN = prove(`!(V:real^3->bool) E. FAN (vec 0,V,E) ==> n_fan_pair_ext (V,E) permutes dart_of_fan (V,E)`,
 467    REPEAT STRIP_TAC THEN
 468      SUBGOAL_TAC "A" `n_fan_pair_ext (V:real^3->bool,E) = res (n_fan_pair_ext (V,E)) (dart1_of_fan (V,E))` [ REWRITE_TAC[N_FAN_PAIR_EXT; RES_RES] ] THEN
 469     POP_ASSUM (fun th -> ONCE_REWRITE_TAC[th]) THEN
 470     REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan] THEN
 471     ONCE_REWRITE_TAC[UNION_ACI] THEN
 472     MATCH_MP_TAC RES_PERMUTES_UNION THEN
 473     ASM_SIMP_TAC[N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 474
 475
 476 (* Main result: hypermap_of_fan is a hypermap *)
 477
 478 let HYPERMAP_OF_FAN = prove(`!V E. FAN (vec 0,V,E) ==> tuple_hypermap (hypermap_of_fan (V,E)) =
 479                          (dart_of_fan (V,E), e_fan_pair_ext (V,E),
 480                           n_fan_pair_ext (V,E), f_fan_pair_ext (V,E))`,
 481   REWRITE_TAC[hypermap_of_fan] THEN
 482     CONV_TAC (DEPTH_CONV let_CONV) THEN
 483     BETA_TAC THEN
 484     REWRITE_TAC[GSYM E_FAN_PAIR_EXT; GSYM N_FAN_PAIR_EXT; GSYM F_FAN_PAIR_EXT] THEN
 485     REWRITE_TAC[GSYM Hypermap.hypermap_tybij] THEN
 486     GEN_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 487     FIRST_ASSUM (fun th -> REWRITE_TAC[MATCH_MP FINITE_DART_OF_FAN th]) THEN
 488     ASM_SIMP_TAC[N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
 489     ASM_SIMP_TAC[E_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
 490     ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
 491     ASM_SIMP_TAC[E_N_F_EQ_I] );;
 492
 493
 494
 495 let COMPONENTS_HYPERMAP_OF_FAN = prove(`!V E. FAN (vec 0,V,E) ==>
 496                                          dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E) /\
 497                                            edge_map (hypermap_of_fan (V,E)) = e_fan_pair_ext (V,E) /\
 498                                            node_map (hypermap_of_fan (V,E)) = n_fan_pair_ext (V,E) /\
 499                                            face_map (hypermap_of_fan (V,E)) = f_fan_pair_ext (V,E)`,
 500    SIMP_TAC[Hypermap.dart; Hypermap.edge_map; Hypermap.node_map; Hypermap.face_map; HYPERMAP_OF_FAN]);;
 501
 502
 503
 504 (* Additional properties of the face map *)
 505
 506 let INVERSE_F_FAN_PAIR_EXT = prove(`!V E. FAN(vec 0,V,E) ==>
 507                                      inverse (f_fan_pair_ext (V,E)) = e_fan_pair_ext (V,E) o n_fan_pair_ext (V,E)`,
 508    REPEAT STRIP_TAC THEN
 509      FIRST_ASSUM (ASSUME_TAC o (fun th -> MATCH_MP E_N_F_EQ_I th)) THEN
 510      MATCH_MP_TAC INVERSE_UNIQUE_o THEN
 511      ASM_REWRITE_TAC[GSYM o_ASSOC] THEN
 512      MP_TAC (ISPECL [`dart_of_fan ((V:real^3->bool),E)`; `e_fan_pair_ext (V:real^3->bool,E)`; `n_fan_pair_ext (V:real^3->bool,E)`; `f_fan_pair_ext (V:real^3->bool,E)`] Hypermap.cyclic_maps) THEN
 513      ASM_SIMP_TAC[E_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN; N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
 514      ASM_MESON_TAC[FINITE_DART_OF_FAN]);;
 515
 516
 517 (* Explicit formula for inverse (f_fan_pair_ext) *)
 518
 519 let INVERSE_F_FAN_PAIR_EXT_EXPLICIT = prove(`!V E. FAN(vec 0,V,E) ==>
 520    inverse (f_fan_pair_ext (V,E)) = res (\(v,w). sigma_fan (vec 0) V E v w, v) (dart1_of_fan (V,E))`,
 521   REPEAT STRIP_TAC THEN
 522     FIRST_ASSUM ((fun th -> REWRITE_TAC[th]) o (fun th -> MATCH_MP INVERSE_F_FAN_PAIR_EXT th)) THEN
 523     REWRITE_TAC[FUN_EQ_THM; o_THM] THEN
 524     GEN_TAC THEN
 525     REWRITE_TAC[Sphere.res; n_fan_pair_ext] THEN
 526     DISJ_CASES_TAC (TAUT `~(x IN dart1_of_fan (V:real^3->bool,E)) \/ x IN dart1_of_fan (V,E)`) THENL
 527     [
 528       ASM_REWRITE_TAC[e_fan_pair_ext];
 529       ALL_TAC
 530     ] THEN
 531     ASM_REWRITE_TAC[e_fan_pair_ext] THEN
 532     ASM_SIMP_TAC[E_N_F_IN_DART1_OF_FAN] THEN
 533     MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 534     DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
 535     DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
 536     ASM_REWRITE_TAC[n_fan_pair; e_fan_pair]);;
 537
 538
 539
 540 (* Further results *)
 541
 542 let DART_EXISTS = prove(`!V E (v:real^3). v IN V ==> ?w. (v,w) IN dart_of_fan (V,E)`,
 543                         REPEAT STRIP_TAC THEN
 544                           DISJ_CASES_TAC (SET_RULE `set_of_edge (v:real^3) V E = {} \/ (?w. w IN set_of_edge v V E)`) THENL
 545                           [
 546                             EXISTS_TAC `v:real^3` THEN
 547                               REWRITE_TAC[dart_of_fan; IN_UNION] THEN
 548                               DISJ1_TAC THEN
 549                               ASM SET_TAC[];
 550                             POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 551                               EXISTS_TAC `w:real^3` THEN
 552                               REWRITE_TAC[dart_of_fan; IN_UNION] THEN
 553                               DISJ2_TAC THEN
 554                               POP_ASSUM MP_TAC THEN REWRITE_TAC[Fan.set_of_edge] THEN
 555                               ASM SET_TAC[]
 556                           ]);;
 557
 558
 559
 560 let E_N_F_DEGENERATE_CASE = prove(`!V E x. FAN (vec 0,V,E) /\ ~(x IN dart1_of_fan (V,E))
 561                                   ==> edge (hypermap_of_fan (V,E)) x = {x} /\
 562                                       node (hypermap_of_fan (V,E)) x = {x} /\
 563                                       face (hypermap_of_fan (V,E)) x = {x}`,
 564     REPEAT GEN_TAC THEN
 565       REWRITE_TAC[Hypermap.edge; Hypermap.node; Hypermap.face] THEN
 566       SIMP_TAC[Hypermap.edge_map; Hypermap.node_map; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
 567       ONCE_REWRITE_TAC[GSYM Hypermap.orbit_one_point] THEN
 568       SIMP_TAC[e_fan_pair_ext; n_fan_pair_ext; f_fan_pair_ext]);;
 569
 570
 571
 572
 573
 574 let DART1_OF_FAN_SUBSET_DART_OF_FAN = prove(`!V E. dart1_of_fan (V,E) SUBSET dart_of_fan (V,E)`,
 575                                             REWRITE_TAC[dart1_of_fan; dart_of_fan; SUBSET] THEN
 576                                               SET_TAC[]);;
 577
 578
 579
 580 let NODE_SUBSET_DART1_OF_FAN = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
 581                                        ==> node (hypermap_of_fan (V,E)) x SUBSET dart1_of_fan (V,E)`,
 582    REPEAT STRIP_TAC THEN
 583      ASM_SIMP_TAC[Hypermap.node; Hypermap.node_map; HYPERMAP_OF_FAN] THEN
 584      MP_TAC (ISPECL [`dart1_of_fan (V:real^3->bool,E)`; `n_fan_pair_ext (V:real^3->bool,E)`] Hypermap.orbit_subset) THEN
 585      ASM_SIMP_TAC[N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 586
 587
 588
 589 let NODE_SUBSET_DART_OF_FAN = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
 590                                        ==> node (hypermap_of_fan (V,E)) x SUBSET dart_of_fan (V,E)`,
 591    REPEAT STRIP_TAC THEN
 592      ASM_SIMP_TAC[Hypermap.node; Hypermap.node_map; HYPERMAP_OF_FAN] THEN
 593      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `n_fan_pair_ext (V:real^3->bool,E)`] Hypermap.orbit_subset) THEN
 594      ASM_SIMP_TAC[N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
 595
 596
 597
 598
 599
 600 let FACE_SUBSET_DART1_OF_FAN = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
 601                                        ==> face (hypermap_of_fan (V,E)) x SUBSET dart1_of_fan (V,E)`,
 602    REPEAT STRIP_TAC THEN
 603      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
 604      MP_TAC (ISPECL [`dart1_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V:real^3->bool,E)`] Hypermap.orbit_subset) THEN
 605      ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 606
 607
 608
 609 let FACE_SUBSET_DART_OF_FAN = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
 610                                        ==> face (hypermap_of_fan (V,E)) x SUBSET dart_of_fan (V,E)`,
 611    REPEAT STRIP_TAC THEN
 612      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
 613      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V:real^3->bool,E)`] Hypermap.orbit_subset) THEN
 614      ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
 615
 616
 617
 618
 619 let EDGE_SUBSET_DART1_OF_FAN = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
 620                                        ==> edge (hypermap_of_fan (V,E)) x SUBSET dart1_of_fan (V,E)`,
 621    REPEAT STRIP_TAC THEN
 622      ASM_SIMP_TAC[Hypermap.edge; Hypermap.edge_map; HYPERMAP_OF_FAN] THEN
 623      MP_TAC (ISPECL [`dart1_of_fan (V:real^3->bool,E)`; `e_fan_pair_ext (V:real^3->bool,E)`] Hypermap.orbit_subset) THEN
 624      ASM_SIMP_TAC[E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN]);;
 625
 626
 627 let PAIR_IN_DART_OF_FAN = prove(`!V E (v:real^3) w. FAN (vec 0,V,E) /\ (v,w) IN dart_of_fan (V,E)
 628                                  ==> v IN V /\ w IN V`,
 629   REWRITE_TAC[dart_of_fan; IN_UNION; IN_ELIM_THM; PAIR_EQ] THEN
 630     REPEAT GEN_TAC THEN STRIP_TAC THENL
 631     [
 632       ASM_MESON_TAC[];
 633       ASM_MESON_TAC[Fan_misc.FAN_IN_SET_OF_EDGE]
 634     ]);;
 635
 636
 637
 638 let PAIR_IN_DART1_OF_FAN = prove(`!V E (v:real^3) w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
 639                                 ==> v IN V /\ w IN V /\ w IN set_of_edge v V E /\ v IN set_of_edge w V E`,
 640   REPEAT GEN_TAC THEN DISCH_TAC THEN
 641     SUBGOAL_THEN `{v:real^3,w} IN E` ASSUME_TAC THENL
 642     [
 643       POP_ASSUM (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 644         REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
 645         SET_TAC[];
 646       ALL_TAC
 647     ] THEN
 648     ASM_MESON_TAC[Fan_misc.FAN_IN_SET_OF_EDGE]);;
 649
 650
 651
 652 let PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ = prove(`!V E v w. FAN (vec 0:real^N,V,E) /\ (v,w) IN dart1_of_fan (V,E) ==> ~(v = w)`,
 653    REPEAT GEN_TAC THEN
 654      REWRITE_TAC[Fan.FAN; dart1_of_fan; Fan.graph] THEN
 655      DISCH_THEN (CONJUNCTS_THEN2 (ASSUME_TAC o CONJUNCT1 o CONJUNCT2) MP_TAC) THEN
 656      REWRITE_TAC[IN_ELIM_THM] THEN
 657      STRIP_TAC THEN
 658      FIRST_X_ASSUM (MP_TAC o SPEC `{v':real^N,w'}`) THEN
 659      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 660      SIMP_TAC[IN; PAIR_EQ] THEN
 661      DISCH_TAC THEN DISCH_TAC THEN
 662      MATCH_MP_TAC (TAUT `(B ==> ~A) ==> (A ==> ~B)`) THEN
 663      DISCH_TAC THEN
 664      ASM_REWRITE_TAC[HAS_SIZE; SET_RULE `{w',w'} = {w'}`] THEN
 665      SIMP_TAC[Hypermap.CARD_SINGLETON; ARITH_RULE `~(1 = 2)`]);;
 666
 667
 668
 669 let NOT_IN_DART1_OF_FAN = prove(`!V E (v:real^3). FAN (vec 0,V,E) ==> ~(v,v IN dart1_of_fan (V,E))`,
 670    REPEAT STRIP_TAC THEN
 671      MP_TAC (REFL `v:real^3`) THEN
 672      PURE_REWRITE_TAC[TAUT `A ==> F <=> ~A`] THEN
 673      MATCH_MP_TAC (SPEC_ALL PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
 674      ASM_REWRITE_TAC[]);;
 675
 676
 677
 678
 679
 680 let IN_DART_OF_FAN = prove(`!(V:real^3->bool) E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
 681                                   ==> ?v w. x = (v,w) /\ (v,w) IN dart_of_fan (V,E) /\ v IN V /\ w IN V`,
 682    REPEAT STRIP_TAC THEN
 683      POP_ASSUM MP_TAC THEN
 684      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 685      STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 686      EXISTS_TAC `x':real^3` THEN EXISTS_TAC `y:real^3` THEN
 687      ASM_REWRITE_TAC[] THEN
 688      MATCH_MP_TAC PAIR_IN_DART_OF_FAN THEN
 689      EXISTS_TAC `E:(real^3->bool)->bool` THEN
 690      ASM_REWRITE_TAC[]);;
 691
 692
 693
 694 let IN_DART1_OF_FAN = prove(`!(V:real^3->bool) E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
 695                               ==> (?v w. x = v,w /\ (v,w) IN dart1_of_fan (V,E) /\
 696                                      v IN V /\ w IN V /\ {v,w} IN E /\
 697                                      w IN set_of_edge v V E /\ v IN set_of_edge w V E)`,
 698    REPEAT STRIP_TAC THEN
 699      POP_ASSUM MP_TAC THEN
 700      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 701      STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 702      EXISTS_TAC `x':real^3` THEN EXISTS_TAC `y:real^3` THEN
 703      ASM_REWRITE_TAC[] THEN
 704      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x':real^3`; `y:real^3`] PAIR_IN_DART1_OF_FAN) THEN
 705      ASM_SIMP_TAC[] THEN DISCH_THEN (fun th -> ALL_TAC) THEN
 706      POP_ASSUM MP_TAC THEN
 707      REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
 708      STRIP_TAC THEN
 709      ASM_REWRITE_TAC[]);;
 710
 711
 712
 713
 714
 715 (* A dart set of a hypermap is a union of components *)
 716 let DART_EQ_UNIONS = prove(`!H:(A)hypermap. dart H = UNIONS (face_set H) /\
 717                                             dart H = UNIONS (node_set H) /\
 718                                             dart H = UNIONS (edge_set H)`,
 719    GEN_TAC THEN REWRITE_TAC[Hypermap.face_set; Hypermap.node_set; Hypermap.edge_set] THEN
 720      REPEAT CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_partition THEN
 721      REWRITE_TAC[Hypermap.hypermap_lemma]);;
 722
 723
 724 (* A double sum over the set of orbits is a sum over a set itself *)
 725 let SUM_SET_OF_ORBITS = prove(`!s (f:A->A) g. FINITE s /\ f permutes s
 726                                 ==> sum (set_of_orbits s f) (\y. sum y g) = sum s g`,
 727    REPEAT GEN_TAC THEN DISCH_TAC THEN
 728      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP Hypermap.lemma_partition th)) THEN
 729      DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 730      MATCH_MP_TAC (GSYM SUM_UNIONS_NONZERO) THEN
 731      ASM_SIMP_TAC[Hypermap.finite_orbits_lemma] THEN
 732      CONJ_TAC THENL
 733      [
 734        GEN_TAC THEN
 735          REWRITE_TAC[Hypermap.set_of_orbits; IN_ELIM_THM] THEN
 736          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 737          MATCH_MP_TAC Hypermap.lemma_orbit_finite THEN
 738          EXISTS_TAC `s:A->bool` THEN ASM_REWRITE_TAC[];
 739        ALL_TAC
 740      ] THEN
 741      REWRITE_TAC[Hypermap.set_of_orbits; IN_ELIM_THM] THEN
 742      REPEAT STRIP_TAC THEN
 743      REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
 744      FIRST_X_ASSUM (MP_TAC o (MATCH_MP Hypermap.partition_orbit)) THEN
 745      DISCH_THEN (MP_TAC o SPECL [`x':A`; `x'':A`]) THEN
 746      ASM_REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; DE_MORGAN_THM] THEN
 747      DISCH_THEN (MP_TAC o SPEC `x:A`) THEN
 748      ASM_REWRITE_TAC[]);;
 749
 750
 751
 752 (* Specialization of the previos lemma for the components of a hypermap *)
 753 let DART_SUM_lemma = prove(`!(H:(A)hypermap) (g:A->real).
 754                              sum (face_set H) (\f. sum f g) = sum (dart H) g /\
 755                              sum (node_set H) (\n. sum n g) = sum (dart H) g`,
 756    REPEAT GEN_TAC THEN REWRITE_TAC[Hypermap.face_set; Hypermap.node_set] THEN
 757      CONJ_TAC THEN MATCH_MP_TAC SUM_SET_OF_ORBITS THEN REWRITE_TAC[Hypermap.hypermap_lemma]);;
 758
 759
 760
 761
 762 (*************************************)
 763 (* Several simple theorem-generators *)
 764 (*************************************)
 765
 766 let rec range a b =
 767   if (a > b) then []
 768   else a :: range (a+1) b
 769 ;;
 770
 771
 772
 773 (* a1 = b1, a2 = b2, ..., an = bn ==> {a1,...,an} = {b1,...,bn} *)
 774 let gen_ELEMENTS_EQ_IMP_SET_EQ n =
 775   let indices = range 1 n in
 776   let labels ch = map (fun i -> String.concat "" [ch; string_of_int i]) indices in
 777   let a_terms = map (fun name -> mk_var (name, `:A`)) (labels "a") in
 778   let b_terms = map (fun name -> mk_var (name, `:A`)) (labels "b") in
 779   let lhs = list_mk_conj (map2 (fun a b -> mk_eq (a,b)) a_terms b_terms) in
 780   let rhs = mk_eq (mk_fset a_terms, mk_fset b_terms) in
 781   let imp = mk_imp (lhs, rhs) in
 782     GEN_ALL (prove(imp, SIMP_TAC[]));;
 783
 784
 785 (* n < k <=> n = 0 \/ n = 1 \/ ... \/ n = k - 1 *)
 786 let gen_NUM_CASES k =
 787   let var = mk_var("k", `:num`) in
 788   let lhs = mk_binary "<" (var, mk_numeral (Int k)) in
 789   let rhs = list_mk_disj (map (fun i -> mk_eq (var, mk_numeral (Int i))) (range 0 (k-1))) in
 790   let suc = SYM ((DEPTH_CONV NUM_SUC_CONV) (funpow k (fun term -> mk_comb(`SUC`, term)) `0`)) in
 791     GEN_ALL (prove(mk_iff(lhs, rhs),
 792                    REWRITE_TAC[suc; LT] THEN
 793                      CONV_TAC (DEPTH_CONV NUM_SUC_CONV) THEN
 794                      REWRITE_TAC[DISJ_ACI]));;
 795
 796
 797 (* {f k | k < n} = {f 0, f 1, ..., f (n - 1)} *)
 798 let gen_FINITE_SET n =
 799   let f = mk_var ("f", `:num->A`) in
 800   let k = mk_var ("k", `:num`) in
 801   let x = mk_var ("x", `:A`) in
 802   let rhs = mk_fset (map (fun i -> mk_comb (f, mk_small_numeral i)) (range 0 (n - 1))) in
 803   let lhs =
 804     let body = list_mk_icomb "SETSPEC" [x; mk_binary "<" (k, mk_small_numeral n); mk_comb (f, k)] in
 805       mk_comb (`GSPEC:(A->bool)->(A->bool)`, mk_abs (x, mk_exists (k, body))) in
 806     GEN_ALL(prove(mk_eq(lhs,rhs),
 807                   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 808                     REWRITE_TAC[gen_NUM_CASES n] THEN
 809                     SET_TAC[]));;
 810
 811
 812 (*************************************)
 813
 814 (* Some auxiliary results about orbits *)
 815
 816 let FINITE_ORBIT_MAP = prove(`!s f (x:A) n. FINITE s /\ f permutes s
 817                              /\ CARD (orbit_map f x) = n
 818                              ==> orbit_map f x = {(f POWER k) x | k < n}`,
 819    REPEAT STRIP_TAC THEN
 820      MATCH_MP_TAC Hypermap.orbit_cyclic THEN
 821      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`] Hypermap.lemma_cycle_orbit) THEN
 822      ASM_REWRITE_TAC[] THEN
 823      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 824      MP_TAC (SPECL [`orbit_map (f:A->A) x`; `x:A`] Hypermap.CARD_ATLEAST_1) THEN
 825      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`] Hypermap.lemma_orbit_finite) THEN
 826      ASM_SIMP_TAC[Hypermap.orbit_reflect; ARITH_RULE `1 <= n ==> ~(n = 0)`]);;
 827
 828
 829
 830 let ORBIT_MAP_CARD_POS = prove(`!s f (x:A). FINITE s /\ f permutes s ==> 0 < CARD (orbit_map f x)`,
 831    REPEAT STRIP_TAC THEN
 832      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`; `x:A`] Hypermap.lemma_index_on_orbit) THEN
 833      ASM_REWRITE_TAC[Hypermap.orbit_reflect] THEN
 834      STRIP_TAC THEN
 835      MATCH_MP_TAC LET_TRANS THEN
 836      EXISTS_TAC `n:num` THEN
 837      ASM_REWRITE_TAC[LE_0]);;
 838
 839
 840
 841 let ORBIT_MAP_INJ = prove(`!s f (x:A) i j k. FINITE s /\ f permutes s /\ CARD (orbit_map f x) = k /\
 842     i < k /\ j < k /\ (f POWER i) x = (f POWER j) x
 843     ==> i = j`,
 844    REPEAT STRIP_TAC THEN
 845      SUBGOAL_THEN `inj_orbit f (x:A) (k - 1)` MP_TAC THENL
 846      [
 847        MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`] Hypermap.lemma_segment_orbit) THEN
 848          ASM_REWRITE_TAC[] THEN
 849          DISCH_THEN MATCH_MP_TAC THEN
 850          MP_TAC (SPEC_ALL ORBIT_MAP_CARD_POS) THEN
 851          ASM_REWRITE_TAC[] THEN
 852          ARITH_TAC;
 853        ALL_TAC
 854      ] THEN
 855      REWRITE_TAC[Hypermap.lemma_inj_orbit] THEN
 856      DISCH_THEN MATCH_MP_TAC THEN
 857      ASM_SIMP_TAC[ARITH_RULE `i < k ==> i <= k - 1`]);;
 858
 859
 860
 861 let INVERSE_ADD_EXPONENTS = prove(`!a b (f:A->A) s. f permutes s /\ b <= a
 862                                   ==> (f POWER a) o ((inverse f) POWER b) = f POWER (a - b)
 863                                       /\ ((inverse f) POWER b) o (f POWER a) = f POWER (a - b)`,
 864   REPEAT STRIP_TAC THENL
 865     [
 866       MP_TAC (ARITH_RULE `b:num <= a ==> a = (a - b) + b`) THEN
 867         ASM_REWRITE_TAC[] THEN
 868         DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
 869         REWRITE_TAC[Hypermap.addition_exponents; GSYM o_ASSOC] THEN
 870         MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `b:num`] Hypermap.lemma_power_inverse_map) THEN
 871         ASM_REWRITE_TAC[] THEN
 872         DISCH_THEN (fun th -> REWRITE_TAC[th; I_O_ID]);
 873
 874       MP_TAC (ARITH_RULE `b:num <= a ==> a = b + (a - b)`) THEN
 875         ASM_REWRITE_TAC[] THEN
 876         DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
 877         REWRITE_TAC[Hypermap.addition_exponents; o_ASSOC] THEN
 878         MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `b:num`] Hypermap.lemma_power_inverse_map) THEN
 879         ASM_REWRITE_TAC[] THEN
 880         DISCH_THEN (fun th -> REWRITE_TAC[th; I_O_ID])
 881     ]);;
 882
 883
 884
 885 let FINITE_ORBIT_MAP_INVERSE = prove(`!f s (x:A) n k. FINITE s /\ f permutes s
 886                               /\ CARD (orbit_map f x) = n /\ k <= n
 887                               ==> (inverse f POWER k) x = (f POWER (n - k)) x`,
 888   REPEAT STRIP_TAC THEN
 889     ONCE_REWRITE_TAC[CONJUNCT2 (ISPEC `inverse (f:A->A) POWER k` (GSYM I_O_ID))] THEN
 890     SUBGOAL_THEN `I (x:A) = (f POWER n) x` ASSUME_TAC THENL
 891     [
 892       MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`] Hypermap.lemma_cycle_orbit) THEN
 893         ASM_REWRITE_TAC[I_THM] THEN SIMP_TAC[];
 894       ALL_TAC
 895     ] THEN
 896     SUBGOAL_THEN `((inverse f POWER k) o I) (x:A) = ((inverse f POWER k) o (f POWER n)) x` (fun th -> REWRITE_TAC[th]) THENL
 897     [
 898       ASM_REWRITE_TAC[o_THM];
 899       ALL_TAC
 900     ] THEN
 901     ASM_MESON_TAC[INVERSE_ADD_EXPONENTS]);;
 902
 903
 904
 905
 906
 907
 908
 909 let ORBIT_MAP_TRANSLATION = prove(`!s f (x:A) k n. FINITE s /\ f permutes s /\ CARD (orbit_map f x) = k
 910     ==> orbit_map f x = IMAGE (\i. (f POWER i) x) (n..n + k - 1)`,
 911    REPEAT STRIP_TAC THEN
 912      POP_ASSUM MP_TAC THEN
 913      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`; `n:num`] Hypermap.lemma_orbit_power) THEN
 914      ASM_REWRITE_TAC[] THEN
 915      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 916      DISCH_TAC THEN
 917      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `((f:A->A) POWER n) x:A`; `k:num`] FINITE_ORBIT_MAP) THEN
 918      ASM_REWRITE_TAC[] THEN
 919      DISCH_THEN (fun th -> GEN_REWRITE_TAC (DEPTH_CONV o LAND_CONV) [th]) THEN
 920
 921      MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `(f POWER n) x:A`] ORBIT_MAP_CARD_POS) THEN
 922      ASM_REWRITE_TAC[] THEN
 923
 924      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
 925      REWRITE_TAC[GSYM IMAGE_LEMMA] THEN
 926      SUBGOAL_THEN `!k. ((f:A->A) POWER k) ((f POWER n) x) = (f POWER (k + n)) x` (fun th -> REWRITE_TAC[th]) THENL
 927      [
 928        GEN_TAC THEN REWRITE_TAC[Hypermap.addition_exponents; o_THM];
 929        ALL_TAC
 930      ] THEN
 931      REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 932      GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
 933      [
 934        EXISTS_TAC `(k':num) + n` THEN
 935          REWRITE_TAC[IN_NUMSEG] THEN
 936          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 937          POP_ASSUM MP_TAC THEN
 938          ARITH_TAC;
 939        EXISTS_TAC `(x'':num) - n` THEN
 940          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
 941          REWRITE_TAC[IN_NUMSEG] THEN
 942          STRIP_TAC THEN
 943          MP_TAC (ARITH_RULE `n:num <= x'' ==> x'' - n + n = x''`) THEN
 944          ASM_SIMP_TAC[] THEN
 945          DISCH_THEN (fun th -> ALL_TAC) THEN
 946          POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 947          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 948          ARITH_TAC
 949      ]);;
 950
 951
 952
 953 let SUM_ORBIT = prove(`!P s f (x:A) k n. FINITE s /\ f permutes s /\ CARD (orbit_map f x) = k
 954     ==> sum (orbit_map f x) P = sum (n..n + k - 1) (\i. P ((f POWER i) x))`,
 955    REPEAT STRIP_TAC THEN
 956      MP_TAC (SPEC_ALL ORBIT_MAP_TRANSLATION) THEN
 957      ASM_REWRITE_TAC[] THEN
 958      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 959      SUBGOAL_THEN `(\i. (P:A->real) ((f POWER i) (x:A))) = P o (\i. (f POWER i) x)` (fun th -> REWRITE_TAC[th]) THENL
 960      [
 961        REWRITE_TAC[FUN_EQ_THM; o_THM];
 962        ALL_TAC
 963      ] THEN
 964      MATCH_MP_TAC SUM_IMAGE THEN
 965      X_GEN_TAC `i:num` THEN
 966      X_GEN_TAC `j:num` THEN
 967      REWRITE_TAC[IN_NUMSEG] THEN
 968      REPEAT STRIP_TAC THEN
 969      MATCH_MP_TAC (ARITH_RULE `n <= i /\ n <= j /\ i - n = j - n ==> (i = j:num)`) THEN
 970      ASM_REWRITE_TAC[] THEN
 971      POP_ASSUM (MP_TAC o AP_TERM `(inverse (f:A->A)) POWER n`) THEN
 972      MP_TAC (SPECL [`i:num`; `n:num`; `f:A->A`; `s:A->bool`] INVERSE_ADD_EXPONENTS) THEN
 973      ASM_REWRITE_TAC[FUN_EQ_THM; o_THM] THEN
 974      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 975      MP_TAC (SPECL [`j:num`; `n:num`; `f:A->A`; `s:A->bool`] INVERSE_ADD_EXPONENTS) THEN
 976      ASM_REWRITE_TAC[FUN_EQ_THM; o_THM] THEN
 977      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 978      DISCH_TAC THEN
 979      MATCH_MP_TAC (SPEC_ALL ORBIT_MAP_INJ) THEN
 980      ASM_REWRITE_TAC[] THEN
 981      MP_TAC (SPEC_ALL ORBIT_MAP_CARD_POS) THEN
 982      ASM_REWRITE_TAC[] THEN
 983      REMOVE_ASSUM THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN
 984      ARITH_TAC);;
 985
 986
 987 (*  Additional results for orbit maps of sizes 2, 3 *)
 988
 989
 990 let ORBIT_MAP_3 = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 3
 991                         ==> orbit_map f x = {x, f x, f(f x)} /\ f (f (f x)) = x`,
 992   REPEAT GEN_TAC THEN
 993     DISCH_TAC THEN
 994     FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP FINITE_ORBIT_MAP th)) THEN
 995     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 996     REWRITE_TAC[gen_FINITE_SET 3] THEN
 997     CONJ_TAC THENL
 998     [
 999       MATCH_MP_TAC (gen_ELEMENTS_EQ_IMP_SET_EQ 3) THEN
1000         ASM_REWRITE_TAC[Hypermap.POWER; Hypermap.POWER_2; Hypermap.POWER_1] THEN
1001         REWRITE_TAC[I_THM; o_THM];
1002       SUBGOAL_THEN `f (f (f x)) = (f POWER 3) (x:A)` (fun th -> REWRITE_TAC[th]) THENL
1003         [
1004           REWRITE_TAC[ARITH_RULE `3 = SUC 2`; Hypermap.POWER; Hypermap.POWER_2; o_THM];
1005           ALL_TAC
1006         ] THEN
1007         FIRST_ASSUM (fun th -> REWRITE_TAC[GSYM th]) THEN
1008         MATCH_MP_TAC Hypermap.lemma_cycle_orbit THEN
1009         EXISTS_TAC `s:A->bool` THEN
1010         ASM_REWRITE_TAC[]
1011     ]);;
1012
1013
1014
1015
1016 let ORBIT_MAP_2 = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 2
1017                          ==> orbit_map f x = {x, f x} /\ f (f x) = x`,
1018    REPEAT GEN_TAC THEN
1019      DISCH_TAC THEN
1020      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP FINITE_ORBIT_MAP th)) THEN
1021      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1022      REWRITE_TAC[gen_FINITE_SET 2] THEN
1023      CONJ_TAC THENL
1024      [
1025        MATCH_MP_TAC (gen_ELEMENTS_EQ_IMP_SET_EQ 2) THEN
1026          ASM_REWRITE_TAC[Hypermap.POWER; Hypermap.POWER_1; I_THM];
1027        SUBGOAL_THEN `f (f x) = (f POWER 2) (x:A)` (fun th -> REWRITE_TAC[th]) THENL
1028          [
1029            REWRITE_TAC[Hypermap.POWER_2; o_THM];
1030            ALL_TAC
1031          ] THEN
1032          FIRST_ASSUM (fun th -> REWRITE_TAC[GSYM th]) THEN
1033          MATCH_MP_TAC Hypermap.lemma_cycle_orbit THEN
1034          EXISTS_TAC `s:A->bool` THEN
1035          ASM_REWRITE_TAC[]
1036      ]);;
1037
1038
1039
1040 let ORBIT_MAP_INV_3 = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 3
1041                             ==> f x = inverse f (inverse f x) /\
1042                                 f (f x) = inverse f x /\
1043                                 inverse f (inverse f (inverse f x)) = x`,
1044    REPEAT STRIP_TAC THENL
1045      [
1046        SUBGOAL_THEN `inverse f (inverse f x) = (inverse f POWER 2) (x:A)` (fun th -> REWRITE_TAC[th]) THENL
1047          [
1048            REWRITE_TAC[Hypermap.POWER_2; o_THM];
1049            ALL_TAC
1050          ] THEN
1051          SUBGOAL_THEN `f (x:A) = (f POWER (3 - 2)) x` (fun th -> REWRITE_TAC[th]) THENL
1052          [
1053            REWRITE_TAC[ARITH_RULE `3 - 2 = 1`; Hypermap.POWER_1];
1054            ALL_TAC
1055          ] THEN
1056          MATCH_MP_TAC (GSYM FINITE_ORBIT_MAP_INVERSE) THEN
1057          EXISTS_TAC `s:A->bool` THEN
1058          ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`];
1059        SUBGOAL_THEN `f (f x) = (f POWER (3 - 1)) (x:A) /\ inverse f x = (inverse f POWER 1) x` (fun th -> REWRITE_TAC[th]) THENL
1060          [
1061            REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; Hypermap.POWER_2; Hypermap.POWER_1; o_THM];
1062            ALL_TAC
1063          ] THEN
1064          MATCH_MP_TAC (GSYM FINITE_ORBIT_MAP_INVERSE) THEN
1065          EXISTS_TAC `s:A->bool` THEN
1066          ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`];
1067        POP_ASSUM MP_TAC THEN
1068          MP_TAC (SPECL [`s:A->bool`; `f:A->A`; `x:A`] Hypermap.lemma_orbit_inverse_map_eq) THEN
1069          ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1070          DISCH_TAC THEN
1071          SUBGOAL_THEN `inverse f (inverse f (inverse f x)) = (inverse f POWER 3) (x:A)` (fun th -> REWRITE_TAC[th]) THENL
1072          [
1073            REWRITE_TAC[ARITH_RULE `3 = SUC 2`; Hypermap.POWER; Hypermap.POWER_2; o_THM];
1074            ALL_TAC
1075          ] THEN
1076          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1077          MATCH_MP_TAC Hypermap.lemma_cycle_orbit THEN
1078          EXISTS_TAC `s:A->bool` THEN ASM_SIMP_TAC[PERMUTES_INVERSE]
1079      ]);;
1080
1081
1082 let ORBIT_MAP_INV_3_SET = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 3
1083     ==> orbit_map f x = {x, inverse f (inverse f x), inverse f x}`,
1084    REPEAT GEN_TAC THEN DISCH_TAC THEN
1085      FIRST_ASSUM (MP_TAC o MATCH_MP ORBIT_MAP_3) THEN
1086      FIRST_ASSUM (MP_TAC o MATCH_MP ORBIT_MAP_INV_3) THEN
1087      SIMP_TAC[]);;
1088
1089
1090
1091 let ORBIT_MAP_INV_2 = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 2
1092                              ==> f x = inverse f x /\
1093                                  inverse f (inverse f x) = x`,
1094    REPEAT GEN_TAC THEN DISCH_TAC THEN
1095      SUBGOAL_THEN `(f:A->A) x = inverse f x` ASSUME_TAC THENL
1096      [
1097        SUBGOAL_THEN `(f:A->A) x = (f POWER (2 - 1)) x /\ inverse f x = (inverse f POWER 1) x` (fun th -> REWRITE_TAC[th]) THENL
1098          [
1099            REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; Hypermap.POWER_1];
1100            ALL_TAC
1101          ] THEN
1102          FIRST_ASSUM (fun th -> REWRITE_TAC[GSYM th]) THEN
1103          MATCH_MP_TAC (GSYM FINITE_ORBIT_MAP_INVERSE) THEN
1104          EXISTS_TAC `s:A->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`];
1105        ALL_TAC
1106      ] THEN
1107      ASM_REWRITE_TAC[] THEN
1108      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1109      MP_TAC (ISPECL [`f:A->A`; `s:A->bool`] PERMUTES_INVERSES) THEN
1110      ASM_SIMP_TAC[]);;
1111
1112
1113 let ORBIT_MAP_INV_2_SET = prove(`!s f (x:A). FINITE s /\ f permutes s /\ CARD (orbit_map f x) = 2
1114                                  ==> orbit_map f x = {x, inverse f x}`,
1115    REPEAT GEN_TAC THEN DISCH_TAC THEN
1116      FIRST_ASSUM (MP_TAC o MATCH_MP ORBIT_MAP_2) THEN
1117      FIRST_ASSUM (MP_TAC o MATCH_MP ORBIT_MAP_INV_2) THEN
1118      SIMP_TAC[]);;
1119
1120
1121
1122
1123 (* Properties of faces *)
1124
1125 let FAN_PAIR_FIXED_POINT = prove(`!V x. x IN {v,v | v IN V /\ set_of_edge v V E = {}} ==> n_fan_pair_ext (V,E) x = x /\ f_fan_pair (V,E) x = x`,
1126    REPEAT GEN_TAC THEN
1127      REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
1128      ASM_REWRITE_TAC[n_fan_pair_ext; f_fan_pair; PAIR_EQ; inverse_sigma_fan; Fan_misc.EXTENSION_SIGMA_FAN_EQ_RES] THEN
1129      REWRITE_TAC[RES_EMPTY; INVERSE_I; I_THM] THEN
1130      COND_CASES_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
1131      SUBGOAL_THEN `v:real^3 IN set_of_edge v V E` (fun th -> ASM SET_TAC[th]) THEN
1132      POP_ASSUM MP_TAC THEN
1133      REWRITE_TAC[dart1_of_fan; Fan.set_of_edge; IN_ELIM_THM; PAIR_EQ] THEN
1134      STRIP_TAC THEN
1135      ASM_MESON_TAC[]);;
1136
1137
1138
1139
1140
1141 let CARD_FACE_GT_1 = prove(`!V E x. FAN (vec 0,V,E) /\ CARD (face (hypermap_of_fan (V,E)) x) > 1
1142                            ==> x IN dart1_of_fan (V, E)`,
1143   REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1144     REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
1145     ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1146     DISJ_CASES_TAC (TAUT `x IN dart1_of_fan (V:real^3->bool,E) \/ ~(x IN dart1_of_fan (V,E))`) THENL
1147     [
1148       ASM_REWRITE_TAC[];
1149       ALL_TAC
1150     ] THEN
1151
1152     SUBGOAL_THEN `orbit_map (f_fan_pair_ext (V:real^3->bool,E)) x = {x}` MP_TAC THENL
1153     [
1154       ONCE_REWRITE_TAC[GSYM Hypermap.orbit_one_point] THEN
1155         MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1156         DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1157         DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1158         ASM_REWRITE_TAC[f_fan_pair_ext];
1159       ALL_TAC
1160     ] THEN
1161
1162     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1163     REWRITE_TAC[Hypermap.CARD_SINGLETON; ARITH_RULE `~(1 > 1)`]);;
1164
1165
1166
1167
1168
1169 let LINEAR_FACE = prove(`!V E v w. FAN (vec 0,V,E) /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 2
1170                           ==> face (hypermap_of_fan (V,E)) (v,w) = {(v,w), (w,v)}`,
1171    REPEAT STRIP_TAC THEN
1172      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `(v:real^3,w:real^3)`] CARD_FACE_GT_1) THEN
1173      ASM_REWRITE_TAC[ARITH_RULE `2 > 1`] THEN
1174      POP_ASSUM MP_TAC THEN
1175      REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
1176      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1177      REPEAT STRIP_TAC THEN
1178      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V:real^3->bool,E)`; `(v:real^3,w:real^3)`] ORBIT_MAP_INV_2_SET) THEN
1179      ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
1180      ASM_SIMP_TAC[INVERSE_F_FAN_PAIR_EXT_EXPLICIT; Sphere.res] THEN
1181      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V:real^3->bool,E)`; `v:real^3,w:real^3`] ORBIT_MAP_2) THEN
1182      ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
1183      ASM_SIMP_TAC[f_fan_pair_ext; Sphere.res; f_fan_pair] THEN
1184      DISCH_THEN (fun th -> ALL_TAC) THEN
1185      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP (SET_RULE `{a,b} = {a,c} ==> c = a \/ c = b`) th)) THEN
1186      STRIP_TAC THENL
1187      [
1188        POP_ASSUM MP_TAC THEN
1189          REWRITE_TAC[PAIR_EQ] THEN
1190          DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
1191          SIMP_TAC[];
1192        POP_ASSUM MP_TAC THEN
1193          REWRITE_TAC[PAIR_EQ] THEN
1194          DISCH_THEN (fun th -> REWRITE_TAC[th])
1195      ]);;
1196
1197
1198
1199 let LINEAR_FACE_2 = prove(`!V E v w. FAN (vec 0,V,E) /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 2
1200                             ==> f_fan_pair_ext (V,E) (v,w) = (w,v)`,
1201    REPEAT GEN_TAC THEN DISCH_TAC THEN
1202      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP LINEAR_FACE th)) THEN
1203      POP_ASSUM (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1204      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
1205      ABBREV_TAC `f = f_fan_pair_ext (V:real^3->bool,E)` THEN
1206      MP_TAC (ISPECL [`f:real^3#real^3->real^3#real^3`; `v:real^3,w:real^3`] Hypermap.in_orbit_map1) THEN
1207      REPEAT DISCH_TAC THEN
1208      SUBGOAL_THEN `f (v:real^3,w:real^3) = w,v \/ f (v,w) = v,w` MP_TAC THENL
1209      [
1210        ASM SET_TAC[];
1211        ALL_TAC
1212      ] THEN
1213      STRIP_TAC THEN
1214      POP_ASSUM (MP_TAC o (fun th -> ONCE_REWRITE_RULE[Hypermap.orbit_one_point] th)) THEN
1215      REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1216      REWRITE_TAC[IMP_IMP] THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1217      ASM_REWRITE_TAC[Hypermap.CARD_SINGLETON; ARITH_RULE `~(1 = 2)`]);;
1218
1219
1220
1221
1222 let TRIANGULAR_FACE = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E) /\
1223                               CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3
1224     ==> let w' = sigma_fan (vec 0) V E v w in
1225          face (hypermap_of_fan (V,E)) (v,w) = {(v,w), (w,w'), (w',v)} /\
1226          sigma_fan (vec 0) V E w w' = v /\
1227          sigma_fan (vec 0) V E w' v = w`,
1228    REPEAT GEN_TAC THEN
1229      REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1230      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] FACE_SUBSET_DART1_OF_FAN) THEN
1231      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
1232      ASM_REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN
1233      CONV_TAC let_CONV THEN
1234      ABBREV_TAC `w' = sigma_fan (vec 0) V E v w` THEN
1235      ABBREV_TAC `f = f_fan_pair_ext (V,E)` THEN
1236      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `v:real^3,w:real^3`] ORBIT_MAP_3) THEN
1237      ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN; SPEC `vec 0:real^3` FINITE_DART_OF_FAN] THEN
1238      DISCH_TAC THEN
1239      SUBGOAL_THEN `f (v:real^3,w:real^3) IN dart1_of_fan (V:real^3->bool,E) /\ f (f (v,w)) IN dart1_of_fan (V,E)` ASSUME_TAC THENL
1240      [
1241        CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_INSERT];
1242        ALL_TAC
1243      ] THEN
1244
1245      MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `v:real^3,w:real^3`] ORBIT_MAP_INV_3) THEN
1246      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `3`)) THEN
1247      ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN; SPEC `vec 0:real^3` FINITE_DART_OF_FAN] THEN
1248      DISCH_THEN (fun th -> ALL_TAC) THEN STRIP_TAC THEN REMOVE_ASSUM THEN
1249      SUBGOAL_THEN `inverse f (v:real^3,w:real^3) = (w':real^3,v:real^3)` ASSUME_TAC THENL
1250      [
1251        EXPAND_TAC "f" THEN
1252          ASM_SIMP_TAC[INVERSE_F_FAN_PAIR_EXT_EXPLICIT] THEN
1253          ASM_REWRITE_TAC[Sphere.res];
1254        ALL_TAC
1255      ] THEN
1256      SUBGOAL_THEN `w',v IN dart1_of_fan (V:real^3->bool,E)` MP_TAC THENL
1257      [
1258        REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
1259          ASM_REWRITE_TAC[];
1260        ALL_TAC
1261      ] THEN
1262      FIRST_X_ASSUM (MP_TAC o CONJUNCT1 o check (is_conj o concl)) THEN
1263      FIRST_X_ASSUM (MP_TAC o check (fun th -> concl th = `f (v:real^3,w:real^3) = inverse f (inverse f (v,w))`)) THEN
1264      FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1265      REWRITE_TAC[IMP_IMP] THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1266      EXPAND_TAC "f" THEN
1267      ASM_SIMP_TAC[f_fan_pair_ext; INVERSE_F_FAN_PAIR_EXT_EXPLICIT; Sphere.res] THEN
1268      REWRITE_TAC[f_fan_pair; PAIR_EQ] THEN
1269      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1270      FIRST_X_ASSUM (CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC) THEN
1271      ASM_REWRITE_TAC[] THEN
1272      FIRST_X_ASSUM (MP_TAC o AP_TERM `extension_sigma_fan (vec 0) V E w`) THEN
1273      MP_TAC (SPECL [`vec 0:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`] INVERSE_SIGMA_FAN) THEN
1274      ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
1275      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1276      REWRITE_TAC[extension_sigma_fan; IMP_IMP] THEN
1277      DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1278      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`; `w':real^3`] PAIR_IN_DART1_OF_FAN) THEN
1279      ASM_SIMP_TAC[]);;
1280
1281
1282
1283
1284
1285
1286 let IN_FACE_IMP_IN_DART1_OF_FAN = prove(`!V E x y. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
1287                                           /\ y IN face (hypermap_of_fan (V,E)) x
1288                                           ==> y IN dart1_of_fan (V,E)`,
1289    REPEAT GEN_TAC THEN
1290      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1291      REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
1292      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1293      STRIP_TAC THEN
1294      MP_TAC (ISPECL [`dart1_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext ((V:real^3->bool),E)`] Hypermap.orbit_subset) THEN
1295      ASM_SIMP_TAC[F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN] THEN
1296      ASM_MESON_TAC[SUBSET]);;
1297
1298
1299
1300
1301
1302 let FACE_LAST_POINT = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1303          ==> (let w' = sigma_fan (vec 0) V E v w in
1304                 (w',v) IN face (hypermap_of_fan (V,E)) (v,w))`,
1305   REPEAT STRIP_TAC THEN
1306     CONV_TAC let_CONV THEN ABBREV_TAC `w' = sigma_fan (vec 0:real^3) V E v w` THEN
1307     REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
1308     ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1309     SUBGOAL_THEN `w',v = inverse (f_fan_pair_ext (V:real^3->bool,E)) (v,w)` ASSUME_TAC THENL
1310     [
1311       ASM_SIMP_TAC[INVERSE_F_FAN_PAIR_EXT_EXPLICIT] THEN
1312         ASM_REWRITE_TAC[Sphere.res];
1313       ALL_TAC
1314     ] THEN
1315     ASM_REWRITE_TAC[] THEN
1316     MATCH_MP_TAC Hypermap.lemma_inverse_in_orbit THEN
1317     EXISTS_TAC `dart_of_fan (V:real^3->bool,E)` THEN
1318     ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
1319
1320
1321
1322
1323
1324 let IN_DART1_OF_FAN_IMP_CARD_FACE_GT_1 = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
1325                                                  ==> CARD (face (hypermap_of_fan (V,E)) x) > 1`,
1326    REPEAT GEN_TAC THEN
1327      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1328      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1329      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1330      ASM_REWRITE_TAC[] THEN
1331      DISCH_TAC THEN
1332      MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `v:real^3,w:real^3`] Hypermap.FACE_FINITE) THEN
1333      FIRST_ASSUM (MP_TAC o (fun th -> MATCH_MP (let_RULE FACE_LAST_POINT) th)) THEN
1334      ABBREV_TAC `w':real^3 = sigma_fan (vec 0) V E v w` THEN
1335      MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `v:real^3,w:real^3`] Hypermap.face_refl) THEN
1336      ABBREV_TAC `s = face (hypermap_of_fan (V:real^3->bool,E)) (v,w)` THEN
1337      ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
1338      MATCH_MP_TAC (ARITH_RULE `~(a = 0 \/ a = 1) ==> a > 1`) THEN
1339      STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IMP_IMP; GSYM HAS_SIZE] THENL
1340      [
1341        ASM_MESON_TAC[HAS_SIZE_0; NOT_IN_EMPTY];
1342        ALL_TAC
1343      ] THEN
1344      REWRITE_TAC[HAS_SIZE_1_EXISTS] THEN
1345      REWRITE_TAC[EXISTS_UNIQUE; NOT_EXISTS_THM; DE_MORGAN_THM] THEN
1346      GEN_TAC THEN DISJ2_TAC THEN
1347      DISJ_CASES_TAC (TAUT `(x' = v:real^3,w:real^3) \/ ~(x' = v,w)`) THENL
1348      [
1349        REWRITE_TAC[NOT_FORALL_THM] THEN
1350          EXISTS_TAC `w':real^3,v:real^3` THEN
1351            ASM_REWRITE_TAC[PAIR_EQ] THEN
1352            ASM_MESON_TAC[PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ];
1353        ASM_MESON_TAC[]
1354      ]);;
1355
1356
1357
1358
1359 (* AAUHTVE lemmas for new definitions *)
1360 let PLAIN_HYPERMAP_OF_FAN = prove(`!V E. FAN (vec 0,V,E) ==> plain_hypermap (hypermap_of_fan (V,E))`,
1361     REPEAT STRIP_TAC THEN
1362       REWRITE_TAC[Hypermap.plain_hypermap; Hypermap.edge_map] THEN
1363       ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1364       REWRITE_TAC[FUN_EQ_THM; I_THM; o_THM; e_fan_pair_ext] THEN
1365       GEN_TAC THEN
1366       DISJ_CASES_TAC (TAUT `~(x IN dart1_of_fan (V:real^3->bool,E)) \/ x IN dart1_of_fan (V,E)`) THENL
1367       [
1368         ASM_SIMP_TAC[];
1369         ALL_TAC
1370       ] THEN
1371       ASM_SIMP_TAC[E_N_F_IN_DART1_OF_FAN] THEN
1372       MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1373       REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[e_fan_pair]);;
1374
1375
1376 let E_HAS_NO_FIXED_POINTS_IN_D1 = prove(`!(V:real^3->bool) E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
1377                                         ==> ~(e_fan_pair (V,E) x = x)`,
1378    REPEAT GEN_TAC THEN STRIP_TAC THEN
1379      POP_ASSUM MP_TAC THEN
1380      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1381      STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1382      DISCH_TAC THEN
1383      REWRITE_TAC[e_fan_pair; PAIR_EQ] THEN
1384      MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`;`x':real^3`;`y:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
1385      ASM_SIMP_TAC[]);;
1386
1387
1388 let F_HAS_NO_FIXED_POINTS_IN_D1 = prove(`!(V:real^3->bool) E x. FAN (vec 0,V,E) /\ x IN dart1_of_fan (V,E)
1389                                           ==> ~(f_fan_pair (V,E) x = x)`,
1390    REPEAT GEN_TAC THEN STRIP_TAC THEN
1391      POP_ASSUM MP_TAC THEN
1392      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1393      STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair; PAIR_EQ] THEN
1394      DISCH_TAC THEN
1395      ASM_MESON_TAC[PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ]);;
1396
1397
1398
1399 let UNIQUE_ORBIT = prove(`!s f (x:A). FINITE s /\ f permutes s /\ x IN s ==> ?!c. c IN set_of_orbits s f /\ x IN c`,
1400     REPEAT STRIP_TAC THEN
1401       REWRITE_TAC[EXISTS_UNIQUE; Hypermap.set_of_orbits; IN_ELIM_THM] THEN
1402       EXISTS_TAC `orbit_map (f:A->A) x` THEN
1403       CONJ_TAC THENL
1404       [
1405         REWRITE_TAC[Hypermap.orbit_reflect] THEN
1406           EXISTS_TAC `x:A` THEN
1407           ASM_REWRITE_TAC[];
1408         ALL_TAC
1409       ] THEN
1410
1411       GEN_TAC THEN STRIP_TAC THEN
1412       MP_TAC (SPECL [`s:A->bool`; `f:A->A`] Hypermap.partition_orbit) THEN
1413       ASM_REWRITE_TAC[] THEN
1414       DISCH_THEN (MP_TAC o SPECL [`x:A`; `x':A`]) THEN
1415       STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1416       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1417       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1418       DISCH_TAC THEN
1419       SUBGOAL_THEN `x IN orbit_map (f:A->A) x INTER y` MP_TAC THENL
1420       [
1421         ASM_REWRITE_TAC[IN_INTER; Hypermap.orbit_reflect];
1422         SET_TAC[]
1423       ]);;
1424
1425
1426
1427
1428 let DART_IN_UNIQUE_NODE = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
1429                                   ==> ?!n. n IN node_set (hypermap_of_fan (V,E)) /\ x IN n`,
1430    REPEAT STRIP_TAC THEN
1431      REWRITE_TAC[Hypermap.node_set; Hypermap.node_map; Hypermap.dart] THEN
1432      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1433      MATCH_MP_TAC UNIQUE_ORBIT THEN
1434      ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
1435
1436
1437
1438 let DART_IN_UNIQUE_FACE = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
1439                                   ==> ?!f. f IN face_set (hypermap_of_fan (V,E)) /\ x IN f`,
1440    REPEAT STRIP_TAC THEN
1441      REWRITE_TAC[Hypermap.face_set; Hypermap.face_map; Hypermap.dart] THEN
1442      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1443      MATCH_MP_TAC UNIQUE_ORBIT THEN
1444      ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
1445
1446
1447
1448
1449 let DART_IN_UNIQUE_EDGE = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
1450                                   ==> ?!e. e IN edge_set (hypermap_of_fan (V,E)) /\ x IN e`,
1451    REPEAT STRIP_TAC THEN
1452      REWRITE_TAC[Hypermap.edge_set; Hypermap.edge_map; Hypermap.dart] THEN
1453      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1454      MATCH_MP_TAC UNIQUE_ORBIT THEN
1455      ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; E_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
1456
1457
1458
1459 let EDGE_HYPERMAP_OF_FAN = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1460                                  ==> edge (hypermap_of_fan (V,E)) (v,w) = {(v,w), (w,v)}`,
1461    REPEAT STRIP_TAC THEN
1462      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] PLAIN_HYPERMAP_OF_FAN) THEN
1463      ASM_REWRITE_TAC[Hypermap.edge; Hypermap.edge_map; Hypermap.plain_hypermap] THEN
1464      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1465      DISCH_TAC THEN
1466      MP_TAC (ISPECL [`e_fan_pair_ext (V:real^3->bool,E)`] Hypermap.lemma_orbit_convolution_map) THEN
1467      ASM_SIMP_TAC[e_fan_pair_ext; e_fan_pair]);;
1468
1469
1470
1471 let N_FAN_PAIR_EXT_IN_DART1_OF_FAN = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1472                 ==> orbit_map (n_fan_pair_ext (V,E)) (v,w) SUBSET dart1_of_fan (V,E)`,
1473    REPEAT STRIP_TAC THEN
1474      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN) THEN
1475      ASM_REWRITE_TAC[] THEN
1476      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP Hypermap.orbit_subset th)) THEN
1477      DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
1478      ASM_REWRITE_TAC[]);;
1479
1480
1481
1482 let N_FAN_PAIR_EXT_POWER = prove(`!V E v w n. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1483                                  ==> (n_fan_pair_ext (V,E) POWER n) (v,w) =
1484                                      (v, ((sigma_fan (vec 0) V E v) POWER n) w)`,
1485    REPEAT STRIP_TAC THEN
1486      SPEC_TAC (`n:num`,`n:num`) THEN
1487      INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER; I_THM] THEN
1488      REWRITE_TAC[GSYM Hypermap.POWER; ARITH_RULE `SUC n = 1 + n`] THEN
1489      REWRITE_TAC[Hypermap.addition_exponents] THEN
1490      ASM_REWRITE_TAC[o_THM; Hypermap.POWER_1] THEN
1491      REWRITE_TAC[n_fan_pair_ext] THEN
1492      SUBGOAL_THEN `v,(sigma_fan (vec 0) V E v POWER n) w IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
1493      [
1494        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1495          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] N_FAN_PAIR_EXT_IN_DART1_OF_FAN) THEN
1496          ASM_REWRITE_TAC[SUBSET] THEN
1497          DISCH_THEN (MP_TAC o SPEC `(n_fan_pair_ext (V:real^3->bool,E) POWER n) (v,w)`) THEN
1498          ANTS_TAC THEN SIMP_TAC[] THEN
1499          REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN
1500          EXISTS_TAC `n:num` THEN
1501          REWRITE_TAC[ARITH_RULE `n >= 0`];
1502        ALL_TAC
1503      ] THEN
1504      ASM_REWRITE_TAC[n_fan_pair]);;
1505
1506
1507
1508
1509 let NODE_HYPERMAP_OF_FAN = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E) ==>
1510                                    node (hypermap_of_fan (V,E)) (v,w) =
1511                                      {(v, (sigma_fan (vec 0) V E v POWER k) w) | k >= 0}`,
1512     REPEAT STRIP_TAC THEN
1513       REWRITE_TAC[Hypermap.node; Hypermap.node_map] THEN
1514       ASM_SIMP_TAC[HYPERMAP_OF_FAN; Hypermap.orbit_map; N_FAN_PAIR_EXT_POWER]);;
1515
1516
1517
1518 (* Alternative form of the node (hypermap_of_fan (V,E)) (v,w) *)
1519
1520 let SIGMA_FAN_POWER = prove(`!V E v u i. power_map_points sigma_fan (vec 0) V E v u i =
1521     (sigma_fan (vec 0) V E v POWER i) u`,
1522         REPLICATE_TAC 4 GEN_TAC THEN
1523           INDUCT_TAC THENL
1524           [
1525             REWRITE_TAC[Hypermap.POWER; Fan.power_map_points; I_THM];
1526             ALL_TAC
1527           ] THEN
1528           REWRITE_TAC[Fan.power_map_points] THEN
1529           REWRITE_TAC[ARITH_RULE `SUC i = 1 + i`; Hypermap.addition_exponents] THEN
1530           ASM_REWRITE_TAC[Hypermap.POWER_1; o_THM]);;
1531
1532
1533 let NODE_HYPERMAP_OF_FAN_lemma = prove(`!V E v u. FAN (vec 0,V,E) /\ (v,u) IN dart1_of_fan (V,E)
1534                                  ==> node (hypermap_of_fan (V,E)) (v,u) =
1535                                      {(v, power_map_points sigma_fan (vec 0) V E v u i) | 0 <= i }`,
1536    REPEAT STRIP_TAC THEN
1537      REWRITE_TAC[Hypermap.node; Hypermap.node_map] THEN
1538      ASM_SIMP_TAC[HYPERMAP_OF_FAN] THEN
1539      REWRITE_TAC[Hypermap.orbit_map] THEN
1540      ASM_SIMP_TAC[N_FAN_PAIR_EXT_POWER; SIGMA_FAN_POWER] THEN
1541      SET_TAC[ARITH_RULE `!n. n >= 0 <=> 0 <= n`]);;
1542
1543
1544
1545 let NODE_HYPERMAP_OF_FAN_ALT = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1546                        ==> node (hypermap_of_fan (V,E)) (v,w) = {(v,u) | u | u IN set_of_edge v V E}`,
1547    REPEAT STRIP_TAC THEN
1548      ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN_lemma] THEN
1549      SUBGOAL_THEN `{v:real^3,w} IN E` ASSUME_TAC THENL
1550      [
1551        POP_ASSUM MP_TAC THEN REWRITE_TAC[dart1_of_fan] THEN
1552          REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
1553          SET_TAC[];
1554        ALL_TAC
1555      ] THEN
1556
1557      MP_TAC (SPECL [`vec 0:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] Topology.ORBITS_EQ_SET_EDGE_FAN)  THEN
1558      ASM_REWRITE_TAC[Topology.set_of_orbits_points_fan] THEN
1559      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1560      SET_TAC[]);;
1561
1562
1563 (* CARD (node (v,w)) = CARD(set_of_edge v) *)
1564 let CARD_NODE_HYPERMAP_OF_FAN = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
1565                 ==> CARD (node (hypermap_of_fan (V,E)) (v,w)) = CARD (set_of_edge v V E)`,
1566    REPEAT STRIP_TAC THEN
1567      MP_TAC (SPEC_ALL NODE_HYPERMAP_OF_FAN_ALT) THEN
1568      ASM_REWRITE_TAC[] THEN
1569      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1570      REWRITE_TAC[IMAGE_LEMMA] THEN
1571      MATCH_MP_TAC CARD_IMAGE_INJ THEN
1572      ASM_SIMP_TAC[SPEC `vec 0:real^3` Fan.remark1_fan; PAIR_EQ]);;
1573
1574
1575 (* FST x is a bijection between V and node_set *)
1576
1577 let HYPERMAP_OF_FAN_NODE_EQ = prove(`!V E x y. FAN (vec 0,V,E) /\
1578                 x IN dart_of_fan (V,E) /\ y IN dart_of_fan (V,E) /\ FST x = FST y
1579                 ==> node (hypermap_of_fan (V,E)) x = node (hypermap_of_fan (V,E)) y`,
1580    REPEAT GEN_TAC THEN
1581      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1582      MP_TAC (ISPEC `y:real^3#real^3` PAIR_SURJECTIVE) THEN
1583      DISCH_THEN (X_CHOOSE_THEN `v':real^3` MP_TAC) THEN
1584      DISCH_THEN (X_CHOOSE_THEN `u:real^3` ASSUME_TAC) THEN
1585      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1586      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1587      ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1588      POP_ASSUM (ASSUME_TAC o (fun th -> ONCE_REWRITE_RULE[EQ_SYM_EQ] th)) THEN
1589      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
1590      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1591
1592      DISJ_CASES_TAC (TAUT `(v:real^3,w:real^3) IN dart1_of_fan (V,E) \/ ~(v,w IN dart1_of_fan (V,E))`) THENL
1593      [
1594        MP_TAC (SPEC_ALL PAIR_IN_DART1_OF_FAN) THEN
1595          ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1596          SUBGOAL_THEN `v:real^3,u:real^3 IN dart1_of_fan (V,E)` ASSUME_TAC THENL
1597          [
1598            REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
1599              REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION] THEN
1600              STRIP_TAC THENL
1601              [
1602                POP_ASSUM MP_TAC THEN
1603                  REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN STRIP_TAC THEN
1604                  FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
1605                  ASM_REWRITE_TAC[NOT_IN_EMPTY];
1606                ASM_SIMP_TAC[]
1607              ];
1608            ALL_TAC
1609          ] THEN
1610
1611          MP_TAC (SPEC_ALL NODE_HYPERMAP_OF_FAN_ALT) THEN
1612          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `u:real^3`] NODE_HYPERMAP_OF_FAN_ALT) THEN
1613          ASM_SIMP_TAC[];
1614        ALL_TAC
1615      ] THEN
1616
1617      REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
1618      ASM_REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION] THEN
1619      REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
1620      REPEAT STRIP_TAC THENL
1621      [
1622        POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1623          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1624          ASM_REWRITE_TAC[];
1625        ALL_TAC
1626      ] THEN
1627
1628      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `u:real^3`] PAIR_IN_DART1_OF_FAN) THEN
1629      ASM_REWRITE_TAC[NOT_IN_EMPTY]);;
1630
1631
1632
1633 let FST_NODE_lemma = prove(`!V E n. FAN (vec 0,V,E) /\ n IN node_set (hypermap_of_fan (V,E))
1634                                 ==> !x y. x IN n /\ y IN n ==> FST x = FST y`,
1635    REWRITE_TAC[Hypermap.node_set; Hypermap.set_of_orbits; GSYM Hypermap.node; IN_ELIM_THM] THEN
1636      REPEAT GEN_TAC THEN STRIP_TAC THEN
1637      ASM_CASES_TAC `x IN dart1_of_fan (V:real^3->bool,E)` THENL
1638      [
1639        POP_ASSUM MP_TAC THEN
1640          MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1641          DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1642          DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1643          ASM_REWRITE_TAC[] THEN
1644          DISCH_TAC THEN
1645          MP_TAC (SPEC_ALL NODE_HYPERMAP_OF_FAN) THEN
1646          ASM_REWRITE_TAC[] THEN
1647          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1648          REWRITE_TAC[IN_ELIM_THM] THEN
1649          REPEAT STRIP_TAC THEN
1650          ASM_REWRITE_TAC[];
1651        MP_TAC (SPEC_ALL E_N_F_DEGENERATE_CASE) THEN
1652          ASM_REWRITE_TAC[] THEN
1653          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1654          SIMP_TAC[IN_SING]
1655      ]);;
1656
1657
1658
1659 let FAN_NODE_EQ_lemma = prove(`!V E x y. FAN (vec 0,V,E) /\
1660                                 node (hypermap_of_fan (V,E)) x = node (hypermap_of_fan (V,E)) y
1661                                 ==> FST x = FST y`,
1662    REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
1663      ASM_CASES_TAC `x IN dart1_of_fan (V:real^3->bool,E)` THENL
1664      [
1665        POP_ASSUM MP_TAC THEN
1666          MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1667          DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1668          DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1669          ASM_REWRITE_TAC[] THEN
1670          DISCH_TAC THEN
1671          MP_TAC (SPEC_ALL NODE_HYPERMAP_OF_FAN) THEN
1672          ASM_REWRITE_TAC[] THEN
1673          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1674          DISCH_TAC THEN
1675          MP_TAC (ISPECL [`hypermap_of_fan (V,E)`; `y:real^3#real^3`] Hypermap.node_refl) THEN
1676          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1677          REWRITE_TAC[IN_ELIM_THM] THEN
1678          STRIP_TAC THEN
1679          ASM_REWRITE_TAC[];
1680        ALL_TAC
1681      ] THEN
1682
1683    MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] E_N_F_DEGENERATE_CASE) THEN
1684    ASM_SIMP_TAC[] THEN
1685    DISCH_THEN (fun th -> ALL_TAC) THEN
1686    DISCH_TAC THEN
1687    SUBGOAL_THEN `y IN {x:real^3#real^3}` MP_TAC THENL
1688    [
1689      ASM_REWRITE_TAC[Hypermap.node_refl];
1690      ALL_TAC
1691    ] THEN
1692    SIMP_TAC[IN_SING]);;
1693
1694
1695
1696 (* node_set = IMAGE f V *)
1697 let NODE_SET_AS_IMAGE = prove(`!V E. FAN (vec 0,V,E) ==>
1698                                 ?f. (!v w. f v = f w ==> v = w) /\
1699                                     (!v x. x IN f v ==> FST x = v) /\
1700                                     (!v. FST (CHOICE (f v)) = v) /\
1701                                     node_set (hypermap_of_fan (V,E)) = IMAGE f V`,
1702    REPEAT STRIP_TAC THEN
1703      REWRITE_TAC[Hypermap.node_set; Hypermap.set_of_orbits; GSYM Hypermap.node] THEN
1704      EXISTS_TAC `(\v. node (hypermap_of_fan (V,E)) (if set_of_edge v V E = {} then (v,v) else (v, CHOICE (set_of_edge v V E))))` THEN
1705      CONJ_TAC THENL
1706      [
1707        BETA_TAC THEN
1708          REPEAT GEN_TAC THEN
1709          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] FAN_NODE_EQ_lemma) THEN
1710          ASM_REWRITE_TAC[] THEN
1711          DISCH_THEN (fun th -> DISCH_THEN (fun th2 -> MP_TAC (MATCH_MP th th2))) THEN
1712          ASM_CASES_TAC `set_of_edge (v:real^3) V E = {}` THEN ASM_REWRITE_TAC[] THENL
1713          [
1714            ASM_CASES_TAC `set_of_edge (w:real^3) V E = {}` THEN ASM_REWRITE_TAC[];
1715            ASM_CASES_TAC `set_of_edge (w:real^3) V E = {}` THEN ASM_REWRITE_TAC[]
1716          ];
1717        ALL_TAC
1718      ] THEN
1719
1720      BETA_TAC THEN
1721      SUBGOAL_THEN `!v x. x IN node (hypermap_of_fan (V,E)) (if set_of_edge v V E = {} then v,v else v,CHOICE (set_of_edge v V E)) ==> FST x = v` ASSUME_TAC THENL
1722      [
1723        REPEAT GEN_TAC THEN
1724          DISCH_THEN (MP_TAC o (MATCH_MP Hypermap.lemma_node_identity)) THEN
1725          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] FAN_NODE_EQ_lemma) THEN
1726          ASM_REWRITE_TAC[] THEN
1727          DISCH_THEN (fun th -> DISCH_THEN (MP_TAC o (MATCH_MP th))) THEN
1728          ASM_CASES_TAC `set_of_edge (v:real^3) V E = {}` THEN ASM_SIMP_TAC[];
1729        ALL_TAC
1730      ] THEN
1731
1732      ASM_REWRITE_TAC[] THEN
1733      CONJ_TAC THENL
1734      [
1735        GEN_TAC THEN
1736          POP_ASSUM MATCH_MP_TAC THEN
1737          MATCH_MP_TAC CHOICE_DEF THEN
1738          REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
1739          EXISTS_TAC `if set_of_edge v V E = {} then v,v else v,CHOICE (set_of_edge (v:real^3) V E)` THEN
1740          REWRITE_TAC[Hypermap.node_refl];
1741        ALL_TAC
1742      ] THEN
1743      REMOVE_ASSUM THEN
1744
1745      ONCE_REWRITE_TAC[EXTENSION] THEN
1746      X_GEN_TAC `n:real^3#real^3->bool` THEN
1747      REWRITE_TAC[IN_ELIM_THM; IN_IMAGE] THEN
1748      EQ_TAC THENL
1749      [
1750        ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
1751          DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
1752          MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
1753          DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1754          DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
1755          ASM_REWRITE_TAC[] THEN
1756          STRIP_TAC THEN
1757          EXISTS_TAC `v:real^3` THEN
1758          MP_TAC (SPEC_ALL PAIR_IN_DART_OF_FAN) THEN
1759          ASM_SIMP_TAC[] THEN DISCH_TAC THEN
1760
1761          MATCH_MP_TAC HYPERMAP_OF_FAN_NODE_EQ THEN
1762          ASM_REWRITE_TAC[] THEN
1763          ASM_CASES_TAC `set_of_edge (v:real^3) V E = {}` THEN ASM_REWRITE_TAC[] THENL
1764          [
1765            SUBGOAL_THEN `~(v:real^3,w IN dart1_of_fan (V,E))` ASSUME_TAC THENL
1766              [
1767                POP_ASSUM MP_TAC THEN
1768                  MATCH_MP_TAC (TAUT `(A ==> ~B) ==> (B ==> ~A)`) THEN
1769                  REPEAT STRIP_TAC THEN
1770                  MP_TAC (SPEC_ALL PAIR_IN_DART1_OF_FAN) THEN
1771                  ASM_REWRITE_TAC[NOT_IN_EMPTY];
1772                ALL_TAC
1773              ] THEN
1774
1775              FIRST_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
1776              GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [dart_of_fan] THEN
1777              ASM_REWRITE_TAC[GSYM dart1_of_fan; IN_UNION] THEN
1778              REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
1779              STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1780              REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN
1781              ASM_SIMP_TAC[];
1782            ALL_TAC
1783          ] THEN
1784
1785          ASM_REWRITE_TAC[dart_of_fan; IN_UNION; IN_ELIM_THM] THEN
1786          DISJ2_TAC THEN
1787          MAP_EVERY EXISTS_TAC [`v:real^3`; `CHOICE (set_of_edge (v:real^3) V E)`] THEN
1788          REWRITE_TAC[] THEN
1789          POP_ASSUM (MP_TAC o (MATCH_MP CHOICE_DEF)) THEN
1790          SIMP_TAC[set_of_edge; IN_ELIM_THM];
1791        ALL_TAC
1792      ] THEN
1793
1794      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
1795      ASM_CASES_TAC `set_of_edge (v:real^3) V E = {}` THEN ASM_REWRITE_TAC[] THENL
1796      [
1797        DISCH_TAC THEN
1798          EXISTS_TAC `v:real^3,v` THEN
1799          ASM_REWRITE_TAC[] THEN
1800          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
1801          REWRITE_TAC[dart_of_fan; IN_UNION] THEN
1802          DISJ1_TAC THEN
1803          REWRITE_TAC[IN_ELIM_THM] THEN
1804          EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[];
1805        ALL_TAC
1806      ] THEN
1807
1808      DISCH_TAC THEN
1809      EXISTS_TAC `v:real^3,CHOICE (set_of_edge v V E)` THEN
1810      ASM_REWRITE_TAC[] THEN
1811      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
1812      REWRITE_TAC[dart_of_fan; IN_UNION] THEN
1813      DISJ2_TAC THEN
1814      REWRITE_TAC[IN_ELIM_THM] THEN
1815      MAP_EVERY EXISTS_TAC [`v:real^3`; `CHOICE (set_of_edge (v:real^3) V E)`] THEN
1816      REWRITE_TAC[] THEN
1817      REMOVE_ASSUM THEN POP_ASSUM (MP_TAC o (MATCH_MP CHOICE_DEF)) THEN
1818      SIMP_TAC[set_of_edge; IN_ELIM_THM]);;
1819
1820
1821
1822 (* Results for simple hypermaps *)
1823 let SIMPLE_HYPERMAP_IMP_FACE_INJ = prove(`!H (x:A) u v. simple_hypermap H /\ x IN dart H /\
1824                                            u IN node H x /\ v IN node H x /\ face H u = face H v
1825                                              ==> u = v`,
1826    REWRITE_TAC[Hypermap.simple_hypermap] THEN
1827      REPEAT STRIP_TAC THEN
1828      SUBGOAL_THEN `!y. y IN node H (x:A) ==> y IN dart H` ASSUME_TAC THENL
1829      [
1830        ASM_SIMP_TAC[GSYM SUBSET; Hypermap.lemma_node_subset];
1831        ALL_TAC
1832      ] THEN
1833
1834      SUBGOAL_THEN `node H (u:A) = node H (x:A) /\ node H (v:A) = node H (x:A)` ASSUME_TAC THENL
1835      [
1836        CONJ_TAC THEN MATCH_MP_TAC EQ_SYM THEN MATCH_MP_TAC Hypermap.lemma_node_identity THEN ASM_REWRITE_TAC[];
1837        ALL_TAC
1838      ] THEN
1839
1840      FIRST_ASSUM (MP_TAC o SPEC `v:A`) THEN
1841      FIRST_X_ASSUM (MP_TAC o SPEC `u:A`) THEN
1842      ASM_REWRITE_TAC[] THEN
1843      REPEAT DISCH_TAC THEN
1844      FIRST_ASSUM (MP_TAC o SPEC `v:A`) THEN
1845      FIRST_X_ASSUM (MP_TAC o SPEC `u:A`) THEN
1846      ASM_REWRITE_TAC[] THEN
1847      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1848      REWRITE_TAC[Hypermap.SING_EQ]);;
1849
1850
1851
1852 let SIMPLE_HYPERMAP_lemma = prove(`!H (x:A) P. simple_hypermap H /\ x IN dart H
1853                                     ==> CARD {face H y | y | y IN dart H /\ P y /\ y IN node H x}
1854                                       = CARD {y | y IN node H x /\ P y}`,
1855    REPEAT STRIP_TAC THEN
1856      SUBGOAL_THEN `!y. y IN node H (x:A) ==> y IN dart H` ASSUME_TAC THENL
1857      [
1858        ASM_SIMP_TAC[GSYM SUBSET; Hypermap.lemma_node_subset];
1859        ALL_TAC
1860      ] THEN
1861
1862      MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
1863      EXISTS_TAC `face (H:(A)hypermap)` THEN
1864      REPEAT STRIP_TAC THENL
1865      [
1866        MATCH_MP_TAC FINITE_SUBSET THEN
1867          EXISTS_TAC `node (H:(A)hypermap) x` THEN
1868          REWRITE_TAC[Hypermap.NODE_FINITE] THEN
1869          SIMP_TAC[SUBSET; IN_ELIM_THM];
1870
1871        POP_ASSUM MP_TAC THEN
1872          REWRITE_TAC[IN_ELIM_THM] THEN
1873          DISCH_TAC THEN
1874          EXISTS_TAC `x':A` THEN
1875          ASM_SIMP_TAC[];
1876
1877        ALL_TAC
1878      ] THEN
1879
1880      POP_ASSUM MP_TAC THEN
1881      REWRITE_TAC[IN_ELIM_THM] THEN
1882      DISCH_THEN (X_CHOOSE_THEN `v:A` ASSUME_TAC) THEN
1883      REWRITE_TAC[EXISTS_UNIQUE] THEN
1884      EXISTS_TAC `v:A` THEN
1885      ASM_REWRITE_TAC[] THEN
1886      POP_ASSUM (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
1887      REPEAT STRIP_TAC THEN
1888      MP_TAC (SPECL [`H:(A)hypermap`; `x:A`; `y:A`; `v:A`] SIMPLE_HYPERMAP_IMP_FACE_INJ) THEN
1889      ASM_SIMP_TAC[]);;
1890
1891
1892
1893
1894 let HYPERMAP_OF_FAN_FACE_NODE_INJ = prove(`!V E f x y. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
1895                                             f IN face_set (hypermap_of_fan (V,E))
1896                                           /\ x IN f /\ y IN f /\ FST x = FST y ==> x = y`,
1897    REPEAT GEN_TAC THEN
1898      REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN
1899      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1900      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
1901      REPEAT STRIP_TAC THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1902      MATCH_MP_TAC SIMPLE_HYPERMAP_IMP_FACE_INJ THEN
1903      MAP_EVERY EXISTS_TAC [`hypermap_of_fan (V,E)`; `x:real^3#real^3`] THEN
1904      ASM_REWRITE_TAC[Hypermap.node_refl] THEN
1905      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
1906
1907      SUBGOAL_THEN `x IN dart_of_fan (V:real^3->bool,E) /\ y IN dart_of_fan (V,E)` ASSUME_TAC THENL
1908      [
1909        CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN
1910          EXISTS_TAC `face (hypermap_of_fan (V,E)) x'` THEN
1911          ASM_SIMP_TAC[FACE_SUBSET_DART_OF_FAN];
1912        ALL_TAC
1913      ] THEN
1914
1915      SUBGOAL_THEN `node (hypermap_of_fan (V,E)) x = node (hypermap_of_fan (V,E)) y` (fun th -> ASM_REWRITE_TAC[th; Hypermap.node_refl]) THENL
1916      [
1917        MATCH_MP_TAC HYPERMAP_OF_FAN_NODE_EQ THEN
1918          ASM_REWRITE_TAC[];
1919        ALL_TAC
1920      ] THEN
1921
1922      MATCH_MP_TAC Hypermap.lemma_face_identity THEN
1923      SUBGOAL_THEN `face (hypermap_of_fan (V,E)) x = face (hypermap_of_fan (V,E)) x'` (fun th -> ASM_REWRITE_TAC[th]) THEN
1924      MATCH_MP_TAC (GSYM Hypermap.lemma_face_identity) THEN
1925      ASM_REWRITE_TAC[]);;
1926
1927
1928
1929
1930 (* ULEKUUB for hypermap_of_fan: preliminaries *)
1931
1932 let NODE_HYPERMAP_OF_FAN_POWER_MAP_POINTS = prove(`!V E v u. FAN (vec 0,V,E) /\ (v,u) IN dart1_of_fan (V,E)
1933         ==> node (hypermap_of_fan (V,E)) (v,u) =
1934             {(v, power_map_points sigma_fan (vec 0) V E v u i) | i | i < CARD (set_of_edge v V E) }`,
1935    REPEAT STRIP_TAC THEN
1936      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `u:real^3`] CARD_NODE_HYPERMAP_OF_FAN) THEN
1937      ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN_lemma; SIGMA_FAN_POWER; GSYM N_FAN_PAIR_EXT_POWER] THEN
1938      REWRITE_TAC[ARITH_RULE `0 <= i <=> i >= 0`; GSYM Hypermap.orbit_map] THEN
1939      ABBREV_TAC `n = CARD (set_of_edge (v:real^3) V E)` THEN
1940      DISCH_TAC THEN
1941      MATCH_MP_TAC FINITE_ORBIT_MAP THEN
1942      EXISTS_TAC `dart_of_fan (V:real^3->bool,E)` THEN
1943      ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN]);;
1944
1945
1946 let AZIM_I_FAN_EQ_AZIM_DART = prove(`!V E v u i. FAN (vec 0,V,E) /\ (v,u) IN dart1_of_fan (V,E)
1947                                     /\ CARD (set_of_edge v V E) > 1
1948                   ==> azim_i_fan (vec 0) V E v u i =
1949                       azim_dart (V,E) (v, power_map_points sigma_fan (vec 0) V E v u i)`,
1950    REPEAT STRIP_TAC THEN
1951      MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `u:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
1952      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1953      REWRITE_TAC[azim_dart] THEN
1954      DISJ_CASES_TAC (ARITH_RULE `i = 0 \/ 0 < i`) THENL
1955      [
1956        ASM_REWRITE_TAC[Topology.azim_i_fan; Fan.power_map_points; Topology.azim_fan];
1957        ALL_TAC
1958      ] THEN
1959
1960      SUBGOAL_THEN `~(v:real^3 = power_map_points sigma_fan (vec 0) V E v u i)` ASSUME_TAC THENL
1961      [
1962        SUBGOAL_THEN `(v:real^3,power_map_points sigma_fan (vec 0) V E v u i) IN dart1_of_fan (V,E)` MP_TAC THENL
1963          [
1964            REWRITE_TAC[SIGMA_FAN_POWER] THEN
1965
1966              MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `u:real^3`] N_FAN_PAIR_EXT_IN_DART1_OF_FAN) THEN
1967              ASM_REWRITE_TAC[SUBSET] THEN
1968              DISCH_THEN (MP_TAC o SPEC `(n_fan_pair_ext (V:real^3->bool,E) POWER i) (v,u)`) THEN
1969              ANTS_TAC THENL
1970              [
1971                REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN
1972                  EXISTS_TAC `i:num` THEN
1973                  ASM_SIMP_TAC[ARITH_RULE `0 < i ==> i >= 0`];
1974                ASM_SIMP_TAC[N_FAN_PAIR_EXT_POWER]
1975              ];
1976            ALL_TAC
1977          ] THEN
1978
1979          ABBREV_TAC `w:real^3 = power_map_points sigma_fan (vec 0) V E v u i` THEN
1980          DISCH_TAC THEN
1981          MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
1982          ASM_REWRITE_TAC[];
1983        ALL_TAC
1984      ] THEN
1985
1986      ASM_REWRITE_TAC[Topology.azim_i_fan; Topology.azim_fan; Fan.power_map_points]);;
1987
1988
1989
1990
1991 (* ULEKUUB for hypermap_of_fan *)
1992 let SUM_lemma = prove(`!V E v u. FAN (vec 0,V,E) /\ (v,u) IN dart1_of_fan (V,E) /\ CARD (set_of_edge v V E) > 1
1993                   ==> sum (0..CARD (set_of_edge v V E) - 1) (azim_i_fan (vec 0) V E v u) =
1994                       sum (node (hypermap_of_fan (V,E)) (v,u)) (azim_dart (V,E))`,
1995    REPEAT STRIP_TAC THEN
1996      ABBREV_TAC `n = CARD (set_of_edge (v:real^3) V E)` THEN
1997      SUBGOAL_THEN `node(hypermap_of_fan (V:real^3->bool,E)) (v,u) = IMAGE (\i:num. v,power_map_points sigma_fan (vec 0) V E v u i) (0..n-1)` MP_TAC THENL
1998      [
1999        ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN_POWER_MAP_POINTS] THEN
2000          REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG_0] THEN
2001          ASM_SIMP_TAC[ARITH_RULE `n > 1 ==> (x <= n - 1 <=> x < n)`] THEN
2002          SET_TAC[];
2003        ALL_TAC
2004      ] THEN
2005      STRIP_TAC THEN
2006      ASM_REWRITE_TAC[] THEN
2007      ABBREV_TAC `f = (\i. v:real^3,power_map_points sigma_fan (vec 0) V E v u i)` THEN
2008
2009      SUBGOAL_THEN `sum (IMAGE f (0..n-1)) (azim_dart (V:real^3->bool,E)) = sum(0..n-1) ((azim_dart (V,E)) o f)` MP_TAC THENL
2010      [
2011        MATCH_MP_TAC SUM_IMAGE THEN
2012          MATCH_MP_TAC IMAGE_IMP_INJECTIVE_GEN THEN
2013          EXISTS_TAC `node (hypermap_of_fan (V:real^3->bool,E)) (v,u)` THEN
2014          REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG] THEN
2015          ASM_SIMP_TAC[CARD_NODE_HYPERMAP_OF_FAN; ARITH_RULE `n > 1 ==> (n - 1 + 1) - 0 = n`];
2016        ALL_TAC
2017      ] THEN
2018
2019      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2020
2021      SUBGOAL_THEN `azim_dart (V:real^3->bool,E) o f = azim_i_fan (vec 0) V E v u` (fun th -> REWRITE_TAC[th]) THEN
2022      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2023      REWRITE_TAC[FUN_EQ_THM; o_THM] THEN
2024      ASM_SIMP_TAC[AZIM_I_FAN_EQ_AZIM_DART]);;
2025
2026
2027
2028 let SUM_AZIM_DART = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
2029                             ==> sum (node (hypermap_of_fan (V,E)) x) (azim_dart (V,E)) = &2 * pi`,
2030     REPEAT GEN_TAC THEN
2031       MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
2032       DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
2033       DISCH_THEN (X_CHOOSE_THEN `u:real^3` MP_TAC) THEN
2034       DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2035       REPEAT STRIP_TAC THEN
2036
2037       ASM_CASES_TAC `~(v:real^3,u IN dart1_of_fan (V,E))` THENL
2038       [
2039         ASM_SIMP_TAC[E_N_F_DEGENERATE_CASE] THEN
2040           REWRITE_TAC[SUM_SING] THEN
2041           FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
2042           REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan] THEN
2043           ASM_REWRITE_TAC[IN_UNION; IN_ELIM_THM; PAIR_EQ] THEN
2044           STRIP_TAC THEN
2045           ASM_REWRITE_TAC[azim_dart];
2046         ALL_TAC
2047       ] THEN
2048       POP_ASSUM MP_TAC THEN REMOVE_ASSUM THEN
2049       REWRITE_TAC[NOT_CLAUSES] THEN DISCH_TAC THEN
2050
2051       SUBGOAL_THEN `{v:real^3,u} IN E` ASSUME_TAC THENL
2052       [
2053         POP_ASSUM MP_TAC THEN
2054           REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
2055           SET_TAC[];
2056         ALL_TAC
2057       ] THEN
2058
2059       ABBREV_TAC `n = CARD (set_of_edge (v:real^3) V E)` THEN
2060       DISJ_CASES_TAC (ARITH_RULE `n = 0 \/ n = 1 \/ n > 1`) THENL
2061       [
2062         SUBGOAL_THEN `set_of_edge (v:real^3) V E = {}` MP_TAC THENL
2063           [
2064             ASM_REWRITE_TAC[GSYM HAS_SIZE_0; HAS_SIZE] THEN
2065               MATCH_MP_TAC Fan.remark_finite_fan1 THEN
2066               ASM_MESON_TAC[Fan.FAN; Fan.fan1];
2067             ALL_TAC
2068           ] THEN
2069
2070           SUBGOAL_THEN `u:real^3 IN set_of_edge v V E` MP_TAC THENL
2071           [
2072             ASM_MESON_TAC[Fan_misc.FAN_IN_SET_OF_EDGE];
2073             ALL_TAC
2074           ] THEN
2075           MESON_TAC[NOT_IN_EMPTY];
2076         ALL_TAC
2077       ] THEN
2078
2079       POP_ASSUM MP_TAC THEN STRIP_TAC THENL
2080       [
2081         SUBGOAL_THEN `node (hypermap_of_fan (V:real^3->bool,E)) (v,u) = {(v,u)}` MP_TAC THENL
2082           [
2083             ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN_POWER_MAP_POINTS] THEN
2084               REWRITE_TAC[ARITH_RULE `i < 1 <=> i = 0`] THEN
2085               REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN
2086               GEN_TAC THEN
2087               MESON_TAC[Fan.power_map_points];
2088             ALL_TAC
2089           ] THEN
2090
2091           DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2092           REWRITE_TAC[SUM_SING] THEN
2093           ASM_REWRITE_TAC[azim_dart; Topology.azim_fan; ARITH_RULE `~(1 > 1)`] THEN
2094           MESON_TAC[];
2095         ALL_TAC
2096       ] THEN
2097
2098       POP_ASSUM MP_TAC THEN EXPAND_TAC "n" THEN
2099       REMOVE_ASSUM THEN DISCH_TAC THEN
2100
2101       ASM_SIMP_TAC[GSYM SUM_lemma] THEN
2102       MATCH_MP_TAC Topology.SUM_AZIMS_EQ_2PI_FAN THEN
2103       ASM_SIMP_TAC[ARITH_RULE `a > 1 ==> 1 < a`] THEN
2104       POP_ASSUM MP_TAC THEN
2105       MATCH_MP_TAC (TAUT `(A ==> ~B) ==> (B ==> ~A)`) THEN
2106       DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2107       REWRITE_TAC[Hypermap.CARD_SINGLETON; ARITH_RULE `~(1 > 1)`]);;
2108
2109
2110
2111 (* Properties of surrounded nodes and fully surrounded fans *)
2112
2113 (* LEMMA: aux *)
2114 let SUM_BOUND_LT_ALT = prove(`!s (f:A->real) b n. FINITE s /\ CARD s <= n /\
2115                                (!x. x IN s ==> f x <= b) /\ (?x. x IN s /\ f x < b) /\ &0 <= b
2116                                ==> sum s f < &n * b`,
2117    REPEAT GEN_TAC THEN
2118      DISCH_TAC THEN
2119      MP_TAC (ISPECL [`s:A->bool`; `f:A->real`; `b:real`] SUM_BOUND_LT) THEN
2120      ASM_REWRITE_TAC[] THEN
2121      SUBGOAL_THEN `&(CARD (s:A->bool)) * b <= &n * b` MP_TAC THENL
2122      [
2123        MATCH_MP_TAC REAL_LE_RMUL THEN
2124          ASM_REWRITE_TAC[REAL_OF_NUM_LE];
2125        ALL_TAC
2126      ] THEN
2127      REAL_ARITH_TAC);;
2128
2129
2130
2131
2132
2133 (* Alternative definition *)
2134 let FULLY_SURROUNDED = prove(`!V E. FAN (vec 0,V,E) ==>
2135                                (fully_surrounded (V,E) <=> !v. v IN V ==> surrounded_node (V,E) v)`,
2136    REPEAT STRIP_TAC THEN
2137      REWRITE_TAC[Fan_defs.fully_surrounded; surrounded_node] THEN
2138      EQ_TAC THENL
2139      [
2140        SIMP_TAC[];
2141        ALL_TAC
2142      ] THEN
2143      REPEAT STRIP_TAC THEN
2144      MP_TAC (SPEC_ALL IN_DART_OF_FAN) THEN
2145      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2146      FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`) THEN
2147      ASM_REWRITE_TAC[] THEN
2148      DISCH_THEN (MP_TAC o SPEC `x:real^3#real^3`) THEN
2149      ASM_REWRITE_TAC[]);;
2150
2151
2152
2153
2154 (* LEMMA: general *)
2155 let SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3 = prove(`!V E v. FAN (vec 0,V,E) /\ v IN V /\ surrounded_node (V,E) v
2156                                             ==> CARD (set_of_edge v V E) >= 3`,
2157    REWRITE_TAC[surrounded_node] THEN
2158      REPEAT STRIP_TAC THEN
2159      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] DART_EXISTS) THEN
2160      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2161
2162      SUBGOAL_THEN `(v:real^3,w:real^3) IN dart1_of_fan (V,E)` MP_TAC THENL
2163      [
2164        FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
2165          ASM_REWRITE_TAC[azim_dart] THEN
2166          DISJ_CASES_TAC (TAUT `v:real^3 = w \/ ~(v = w)`) THEN ASM_REWRITE_TAC[] THENL
2167          [
2168            REWRITE_TAC[(MATCH_MP (REAL_ARITH `&0 < a ==> ~(&2 * a < a)`) PI_POS)];
2169            ALL_TAC
2170          ] THEN
2171          DISCH_THEN (fun th -> ALL_TAC) THEN
2172          FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
2173          REWRITE_TAC[dart_of_fan; dart1_of_fan; IN_UNION] THEN
2174          STRIP_TAC THEN
2175          POP_ASSUM MP_TAC THEN
2176          ASM_REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
2177          ASM_MESON_TAC[];
2178        ALL_TAC
2179      ] THEN
2180
2181      DISCH_TAC THEN
2182      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] CARD_NODE_HYPERMAP_OF_FAN) THEN
2183      ASM_REWRITE_TAC[] THEN
2184      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2185
2186      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] SUM_AZIM_DART) THEN
2187      ASM_REWRITE_TAC[] THEN
2188      MATCH_MP_TAC (TAUT `(~B ==> ~A) ==> (A ==> B)`) THEN
2189      REWRITE_TAC[ARITH_RULE `~(a >= 3) <=> a <= 2`] THEN
2190
2191      SUBGOAL_THEN `!x. x IN node(hypermap_of_fan (V:real^3->bool,E)) (v,w) ==> azim_dart (V,E) x < pi` ASSUME_TAC THENL
2192      [
2193        REPEAT STRIP_TAC THEN
2194          FIRST_X_ASSUM (fun th -> MATCH_MP_TAC th) THEN
2195
2196          CONJ_TAC THENL
2197          [
2198            ASM SET_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN; NODE_SUBSET_DART1_OF_FAN];
2199            ALL_TAC
2200          ] THEN
2201
2202          POP_ASSUM MP_TAC THEN
2203          ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN; IN_ELIM_THM; PAIR_EQ] THEN
2204          STRIP_TAC THEN ASM_SIMP_TAC[];
2205        ALL_TAC
2206      ] THEN
2207
2208      ABBREV_TAC `s = node (hypermap_of_fan (V,E)) (v:real^3,w)` THEN
2209      DISCH_TAC THEN
2210      MATCH_MP_TAC (REAL_ARITH `a < &2 * pi ==> ~(a = &2 * pi)`) THEN
2211      MATCH_MP_TAC SUM_BOUND_LT_ALT THEN
2212      ASM_SIMP_TAC[REAL_LT_IMP_LE; PI_POS] THEN
2213      MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `v:real^3,w:real^3`] Hypermap.NODE_FINITE) THEN
2214      ASM_SIMP_TAC[] THEN
2215      DISCH_THEN (fun th -> ALL_TAC) THEN
2216      EXISTS_TAC `v:real^3,w:real^3` THEN
2217      CONJ_TAC THENL
2218      [
2219        REMOVE_ASSUM THEN
2220          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2221          ASM_SIMP_TAC[Hypermap.node; Hypermap.node_map; Hypermap.orbit_reflect];
2222        ALL_TAC
2223      ] THEN
2224
2225      REPLICATE_TAC 3 REMOVE_ASSUM THEN
2226      FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
2227      ASM SET_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN]);;
2228
2229
2230
2231 (* LEMMA: general *)
2232 let SURROUNDED_IMP_IN_DART1_OF_FAN = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart_of_fan (V,E)
2233                                            /\ surrounded_node (V,E) v
2234                                            ==> (v,w) IN dart1_of_fan (V,E)`,
2235    REWRITE_TAC[dart_of_fan; dart1_of_fan; IN_UNION] THEN
2236      REPEAT STRIP_TAC THEN
2237      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3) THEN
2238      ASM_REWRITE_TAC[] THEN
2239      ANTS_TAC THENL
2240      [
2241        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2242          SIMP_TAC[IN_ELIM_THM; PAIR_EQ] THEN
2243          STRIP_TAC THEN
2244          ASM_SIMP_TAC[];
2245        ALL_TAC
2246      ] THEN
2247      REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2248      REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
2249      STRIP_TAC THEN
2250      ASM_REWRITE_TAC[CARD_CLAUSES; ARITH_RULE `~(0 >= 3)`]);;
2251
2252
2253
2254 (* LEMMA: general *)
2255 let SURROUNDED_IMP_CARD_NODE_GE_3 = prove(`!V E v w. FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
2256                                           /\ surrounded_node (V,E) v
2257                                             ==> CARD (node (hypermap_of_fan (V,E)) (v,w)) >= 3`,
2258     REPEAT STRIP_TAC THEN
2259       ASM_SIMP_TAC[CARD_NODE_HYPERMAP_OF_FAN] THEN
2260       MATCH_MP_TAC SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3 THEN
2261       ASM_SIMP_TAC[dart1_of_fan] THEN
2262       REMOVE_ASSUM THEN
2263       SUBGOAL_THEN `{v:real^3,w} IN E` ASSUME_TAC THENL
2264       [
2265         POP_ASSUM MP_TAC THEN
2266           REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
2267           MESON_TAC[];
2268         ALL_TAC
2269       ] THEN
2270       ASM_MESON_TAC[ISPEC `vec 0:real^3` Fan_misc.FAN_IN_SET_OF_EDGE]);;
2271
2272
2273
2274 (* LEMMA: general *)
2275 let CARD_SET_OF_EDGE_GT_1_IMP_CARD_FACE_GE_3 = prove(`!V E. FAN (vec 0,V,E) /\
2276                                                        (!v. v IN V ==> CARD(set_of_edge v V E) > 1)
2277                                ==> (!x. x IN dart_of_fan (V,E) ==> CARD (face (hypermap_of_fan (V,E)) x) >= 3)`,
2278     REPEAT STRIP_TAC THEN
2279       SUBGOAL_THEN `x IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
2280       [
2281         POP_ASSUM MP_TAC THEN
2282           REWRITE_TAC[dart_of_fan; dart1_of_fan; IN_UNION] THEN
2283           STRIP_TAC THEN
2284           POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
2285           STRIP_TAC THEN
2286           FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`) THEN
2287           ASM_REWRITE_TAC[CARD_CLAUSES; ARITH_RULE `~(0 > 1)`];
2288         ALL_TAC
2289       ] THEN
2290       MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] IN_DART1_OF_FAN_IMP_CARD_FACE_GT_1) THEN
2291       ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2292
2293       MATCH_MP_TAC (ARITH_RULE `~(a = 0 \/ a = 1 \/ a = 2) ==> a >= 3`) THEN
2294       STRIP_TAC THEN POP_ASSUM MP_TAC THENL
2295       [
2296         ASM_SIMP_TAC[ARITH_RULE `a > 1 ==> ~(a = 0)`];
2297         ASM_SIMP_TAC[ARITH_RULE `a > 1 ==> ~(a = 1)`];
2298         ALL_TAC
2299       ] THEN
2300
2301       REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
2302       MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
2303       DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
2304       DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
2305       ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
2306
2307       MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] LINEAR_FACE_2) THEN
2308       ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair; PAIR_EQ] THEN
2309       DISCH_THEN (MP_TAC o (fun th -> AP_TERM `extension_sigma_fan (vec 0) V E (w:real^3)` th)) THEN
2310       MP_TAC (ISPECL [`vec 0:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`] Fan_misc.INVERSE_SIGMA_FAN) THEN
2311       ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
2312       DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2313       REWRITE_TAC[Fan.extension_sigma_fan] THEN
2314       SUBGOAL_THEN `v:real^3 IN set_of_edge w V E /\ w IN V` ASSUME_TAC THENL
2315       [
2316         SUBGOAL_THEN `{v:real^3,w} IN E` ASSUME_TAC THENL
2317           [
2318             REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2319               REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
2320               SET_TAC[];
2321             ALL_TAC
2322           ] THEN
2323           ASM_MESON_TAC[Fan_misc.FAN_IN_SET_OF_EDGE];
2324         ALL_TAC
2325       ] THEN
2326       FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`) THEN
2327       ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2328       SUBGOAL_THEN `~(set_of_edge (w:real^3) V E = {v})` ASSUME_TAC THENL
2329       [
2330         POP_ASSUM MP_TAC THEN
2331           MATCH_MP_TAC (TAUT `(A ==> ~B) ==> (B ==> ~A)`) THEN
2332           DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2333           REWRITE_TAC[Hypermap.CARD_SINGLETON; ARITH_RULE `~(1 > 1)`];
2334         ALL_TAC
2335       ] THEN
2336
2337       ASM_MESON_TAC[Fan.SIGMA_FAN]);;
2338
2339
2340
2341 (* LEMMA: general *)
2342 let FULLY_SURROUNDED_IMP_CARD_FACE_GE_3 = prove(`!V E. FAN (vec 0,V,E) /\ fully_surrounded (V,E)
2343                       ==> (!x. x IN dart_of_fan (V,E) ==> CARD (face (hypermap_of_fan (V,E)) x) >= 3)`,
2344         REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2345           ASM_SIMP_TAC[FULLY_SURROUNDED] THEN DISCH_TAC THEN
2346           MATCH_MP_TAC CARD_SET_OF_EDGE_GT_1_IMP_CARD_FACE_GE_3 THEN
2347           ASM_REWRITE_TAC[] THEN GEN_TAC THEN DISCH_TAC THEN
2348           FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`) THEN
2349           ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2350           MATCH_MP_TAC (ARITH_RULE `a >= 3 ==> a > 1`) THEN
2351           MATCH_MP_TAC SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3 THEN
2352           ASM_REWRITE_TAC[]);;
2353
2354
2355
2356 (* ULEKUUB for surrounded fans *)
2357
2358 let FULLY_SURROUNDED_NODE_DECOMPOSITION = prove(`!V E x. FAN (vec 0,V,E) /\
2359                                             fully_surrounded (V,E) /\
2360                                             x IN dart_of_fan (V,E)
2361                                 ==> (let H = hypermap_of_fan (V,E) in
2362                                      let A = {y | y IN node H x /\ CARD (face H y) = 3} in
2363                                      let B = {y | y IN node H x /\ CARD (face H y) = 4} in
2364                                      let C = {y | y IN node H x /\ CARD (face H y) >= 5} in
2365                                      let D = {y | y IN node H x /\ CARD (face H y) >= 4} in
2366                                        node H x = A UNION D /\ DISJOINT A D /\
2367                                          D = B UNION C /\ DISJOINT B C /\
2368                                          FINITE D /\ FINITE A)`,
2369     REPEAT STRIP_TAC THEN
2370       REPEAT (CONV_TAC let_CONV) THEN
2371       ABBREV_TAC `H = hypermap_of_fan (V,E)` THEN
2372       ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
2373       ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN
2374       ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN
2375       ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
2376
2377       SUBGOAL_THEN `A:real^3#real^3->bool SUBSET node H x /\ D SUBSET node H x` ASSUME_TAC THENL
2378       [
2379         EXPAND_TAC "A" THEN EXPAND_TAC "D" THEN
2380           SIMP_TAC[SUBSET; IN_ELIM_THM];
2381         ALL_TAC
2382       ] THEN
2383
2384       SUBGOAL_THEN `DISJOINT (A:real^3#real^3->bool) D` ASSUME_TAC THENL
2385       [
2386         EXPAND_TAC "A" THEN EXPAND_TAC "D" THEN
2387           REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM] THEN
2388           GEN_TAC THEN MATCH_MP_TAC (TAUT `~(A /\ B) ==> ~((X /\ A) /\ X /\ B)`) THEN
2389           ARITH_TAC;
2390         ALL_TAC
2391       ] THEN
2392
2393       SUBGOAL_THEN `(A:real^3#real^3->bool) UNION D = node H x` (fun th -> REWRITE_TAC[th]) THENL
2394       [
2395         MATCH_MP_TAC SUBSET_ANTISYM THEN
2396           CONJ_TAC THENL
2397           [
2398             ASM_REWRITE_TAC[UNION_SUBSET];
2399             ALL_TAC
2400           ] THEN
2401
2402           REWRITE_TAC[SUBSET; IN_UNION] THEN GEN_TAC THEN
2403           REPLICATE_TAC 2 REMOVE_ASSUM THEN
2404           REPLICATE_TAC 4 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
2405           DISCH_TAC THEN
2406           MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] FULLY_SURROUNDED_IMP_CARD_FACE_GE_3) THEN
2407           ASM_REWRITE_TAC[] THEN
2408           DISCH_THEN (MP_TAC o SPEC `x':real^3#real^3`) THEN
2409           SUBGOAL_THEN `x' IN dart_of_fan (V:real^3->bool,E)` (fun th -> REWRITE_TAC[th]) THENL
2410           [
2411             MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] NODE_SUBSET_DART_OF_FAN) THEN
2412               ASM_SIMP_TAC[SUBSET];
2413             ALL_TAC
2414           ] THEN
2415
2416           REWRITE_TAC[ARITH_RULE `a >= 3 <=> a = 3 \/ a >= 4`; IN_ELIM_THM] THEN
2417           ASM_SIMP_TAC[];
2418         ALL_TAC
2419       ] THEN
2420
2421       POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
2422
2423       REPEAT CONJ_TAC THENL
2424       [
2425         MAP_EVERY EXPAND_TAC ["B"; "C"; "D"] THEN
2426           REWRITE_TAC[EXTENSION; IN_UNION; IN_ELIM_THM] THEN
2427           REWRITE_TAC[ARITH_RULE `a >= 4 <=> a = 4 \/ a >= 5`] THEN
2428           REWRITE_TAC[TAUT `A /\ (B \/ C) <=> A /\ B \/ A /\ C`];
2429
2430         EXPAND_TAC "B" THEN EXPAND_TAC "C" THEN
2431           REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM] THEN
2432           GEN_TAC THEN MATCH_MP_TAC (TAUT `~(A /\ B) ==> ~((X /\ A) /\ X /\ B)`) THEN
2433           ARITH_TAC;
2434
2435         MATCH_MP_TAC FINITE_SUBSET THEN
2436           EXISTS_TAC `node H (x:real^3#real^3)` THEN
2437           ASM_REWRITE_TAC[Hypermap.NODE_FINITE];
2438
2439         MATCH_MP_TAC FINITE_SUBSET THEN
2440           EXISTS_TAC `node H (x:real^3#real^3)` THEN
2441           ASM_REWRITE_TAC[Hypermap.NODE_FINITE]
2442       ]);;
2443
2444
2445
2446
2447 let SUM_AZIM_DART_FULLY_SURROUNDED = prove(`!V E x. FAN (vec 0,V,E) /\ fully_surrounded (V,E)
2448                                      /\ x IN dart_of_fan (V,E)
2449                                     ==> (let H = hypermap_of_fan (V,E) in
2450                                          let A = {y | y IN node H x /\ CARD (face H y) = 3} in
2451                                          let B = {y | y IN node H x /\ CARD (face H y) >= 4} in
2452                                            sum A (azim_dart (V,E)) + sum B (azim_dart(V,E)) = &2 * pi)`,
2453     REPEAT STRIP_TAC THEN REPEAT (CONV_TAC let_CONV) THEN
2454       ABBREV_TAC `H = hypermap_of_fan (V:real^3->bool,E)` THEN
2455       ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
2456       ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
2457       ABBREV_TAC `f = azim_dart (V:real^3->bool,E)` THEN
2458       MP_TAC (SPEC_ALL FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN
2459       ASM_REWRITE_TAC[] THEN
2460       DISCH_THEN (MP_TAC o let_RULE) THEN
2461       ASM_REWRITE_TAC[] THEN
2462       REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2463       REPLICATE_TAC 2 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
2464       DISCH_TAC THEN
2465
2466       SUBGOAL_THEN `sum (A:real^3#real^3->bool) f + sum B f = sum (A UNION B) f` (fun th -> REWRITE_TAC[th]) THENL
2467       [
2468         MATCH_MP_TAC (GSYM SUM_UNION) THEN
2469           ASM_REWRITE_TAC[];
2470         ALL_TAC
2471       ] THEN
2472
2473       REMOVE_ASSUM THEN REMOVE_ASSUM THEN
2474       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2475
2476       EXPAND_TAC "H" THEN
2477       EXPAND_TAC "f" THEN
2478
2479       MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
2480       STRIP_TAC THEN FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN
2481       MATCH_MP_TAC SUM_AZIM_DART THEN
2482       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2483       ASM_REWRITE_TAC[]);;
2484
2485
2486 (* TODO: move this definitions to hypermap.hl? *)
2487
2488 let no_loops = new_definition `no_loops (H:(A) hypermap) <=> ! (x:A) (y:A). x IN edge H y /\ x IN node H y ==> x = y`;;
2489
2490 let is_no_double_joints = new_definition `is_no_double_joints (H:(A)hypermap)
2491    <=> (!x y. x IN dart H /\ y IN node H x /\ edge_map H y IN node H (edge_map H x) ==> x = y)`;;
2492
2493
2494 (* Surrounded ==> is_edge_nondegenerate (hypermap_of_fan (V,E)) *)
2495 let HYPERMAP_OF_FAN_EDGE_NONDEGENERATE = prove(`!V E. FAN (vec 0,V,E) /\ fully_surrounded (V,E)
2496                                                ==> is_edge_nondegenerate (hypermap_of_fan (V,E))`,
2497    REWRITE_TAC[Hypermap.is_edge_nondegenerate] THEN
2498      REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2499      ASM_SIMP_TAC[FULLY_SURROUNDED] THEN DISCH_TAC THEN
2500      REPEAT STRIP_TAC THEN
2501      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
2502      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
2503      DISCH_THEN (X_CHOOSE_THEN `w:real^3` MP_TAC) THEN
2504      DISCH_TAC THEN
2505      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN
2506      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
2507      ASM_SIMP_TAC[] THEN
2508      FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl)) THEN
2509      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
2510      REPEAT STRIP_TAC THEN
2511      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] E_HAS_NO_FIXED_POINTS_IN_D1) THEN
2512      ASM_REWRITE_TAC[] THEN
2513      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `x:real^3#real^3`)) THEN
2514      ASM_SIMP_TAC[Hypermap.edge_map; HYPERMAP_OF_FAN] THEN
2515      ASM_REWRITE_TAC[e_fan_pair_ext]);;
2516
2517
2518
2519 (* no_loops (hypermap_of_fan (V,E)) *)
2520 let HYPERMAP_OF_FAN_NO_LOOPS = prove(`!V E. FAN (vec 0,V,E) ==>
2521                                        no_loops (hypermap_of_fan (V,E))`,
2522    REPEAT STRIP_TAC THEN
2523      REWRITE_TAC[no_loops] THEN
2524      REPEAT GEN_TAC THEN
2525      MP_TAC (ISPEC `y:real^3#real^3` PAIR_SURJECTIVE) THEN
2526      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
2527      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
2528      ASM_REWRITE_TAC[] THEN
2529      ASM_CASES_TAC `v,w IN dart1_of_fan (V:real^3->bool,E)` THENL
2530      [
2531        MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] EDGE_HYPERMAP_OF_FAN) THEN
2532          ASM_SIMP_TAC[] THEN
2533          DISCH_THEN (fun th -> ALL_TAC) THEN
2534          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] NODE_HYPERMAP_OF_FAN) THEN
2535          ASM_SIMP_TAC[] THEN
2536          DISCH_THEN (fun th -> ALL_TAC) THEN
2537          ASM_REWRITE_TAC[SET_RULE `x IN {a, b} <=> x = a \/ x = b`] THEN
2538          STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
2539          POP_ASSUM MP_TAC THEN
2540          REWRITE_TAC[IN_ELIM_THM] THEN
2541          STRIP_TAC THEN
2542          SUBGOAL_THEN `v:real^3 = w` MP_TAC THENL
2543          [
2544            POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[PAIR_EQ; EQ_SYM_EQ];
2545            ALL_TAC
2546          ] THEN
2547          MP_TAC (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
2548          ASM_SIMP_TAC[];
2549        ALL_TAC
2550      ] THEN
2551      ASM_SIMP_TAC[Hypermap.edge; Hypermap.node; Hypermap.edge_map; Hypermap.node_map; HYPERMAP_OF_FAN] THEN
2552      SUBGOAL_THEN `orbit_map (e_fan_pair_ext (V:real^3->bool,E)) (v,w) = {(v,w)}` MP_TAC THENL
2553      [
2554        REWRITE_TAC[GSYM Hypermap.orbit_one_point] THEN
2555          ASM_SIMP_TAC[e_fan_pair_ext];
2556        ALL_TAC
2557      ] THEN
2558      SUBGOAL_THEN `orbit_map (n_fan_pair_ext (V:real^3->bool,E)) (v,w) = {(v,w)}` MP_TAC THENL
2559      [
2560        REWRITE_TAC[GSYM Hypermap.orbit_one_point] THEN
2561          ASM_REWRITE_TAC[n_fan_pair_ext];
2562        ALL_TAC
2563      ] THEN
2564      REPLICATE_TAC 2 (DISCH_THEN (fun th -> REWRITE_TAC[th])) THEN
2565      REWRITE_TAC[IN_SING]);;
2566
2567
2568
2569 (* is_no_double_joints (hypermap_of_fan (V,E)) *)
2570 let HYPERMAP_OF_FAN_NO_DOUBLE_JOINTS = prove(`!V E. FAN (vec 0,V,E) ==>
2571                                                is_no_double_joints (hypermap_of_fan (V,E))`,
2572    REPEAT STRIP_TAC THEN
2573      REWRITE_TAC[is_no_double_joints] THEN
2574      REPEAT GEN_TAC THEN
2575      ASM_SIMP_TAC[Hypermap.edge_map; HYPERMAP_OF_FAN] THEN
2576      DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC) THEN
2577      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
2578      DISCH_THEN (X_CHOOSE_THEN `v:real^3` MP_TAC) THEN
2579      DISCH_THEN (X_CHOOSE_THEN `w:real^3` ASSUME_TAC) THEN
2580      ASM_REWRITE_TAC[e_fan_pair_ext] THEN
2581      ASM_CASES_TAC `v,w IN dart1_of_fan (V:real^3->bool,E)` THENL
2582      [
2583        DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2584          SUBGOAL_THEN `y IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
2585          [
2586            MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] NODE_SUBSET_DART1_OF_FAN) THEN
2587              ASM_SIMP_TAC[SUBSET];
2588            ALL_TAC
2589          ] THEN
2590          ASM_REWRITE_TAC[e_fan_pair] THEN
2591          REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2592          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] NODE_HYPERMAP_OF_FAN) THEN
2593          ASM_REWRITE_TAC[] THEN
2594          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2595          REWRITE_TAC[IN_ELIM_THM] THEN
2596          STRIP_TAC THEN
2597          ASM_REWRITE_TAC[e_fan_pair; PAIR_EQ] THEN
2598          SUBGOAL_THEN `w,v IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
2599          [
2600            REPLICATE_TAC 2 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2601              REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
2602              STRIP_TAC THEN
2603              EXISTS_TAC `w:real^3` THEN EXISTS_TAC `v:real^3` THEN
2604              ASM_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`];
2605            ALL_TAC
2606          ] THEN
2607          MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `w:real^3`; `v:real^3`] NODE_HYPERMAP_OF_FAN) THEN
2608          ASM_REWRITE_TAC[] THEN
2609          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2610          REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
2611          STRIP_TAC THEN ASM_SIMP_TAC[];
2612        ALL_TAC
2613      ] THEN
2614      ASM_SIMP_TAC[Hypermap.node; Hypermap.node_map; HYPERMAP_OF_FAN] THEN
2615      SUBGOAL_THEN `orbit_map (n_fan_pair_ext (V:real^3->bool,E)) (v,w) = {(v,w)}` ASSUME_TAC THENL
2616      [
2617        ONCE_REWRITE_TAC[GSYM Hypermap.orbit_one_point] THEN
2618          ASM_REWRITE_TAC[n_fan_pair_ext];
2619        ALL_TAC
2620      ] THEN
2621      ASM_REWRITE_TAC[IN_SING] THEN
2622      ASM_SIMP_TAC[]);;
2623
2624
2625
2626 (* azim_dart x is always positive *)
2627 let AZIM_DART_POS = prove(`!V E x. FAN (vec 0,V,E) /\ x IN dart_of_fan (V,E)
2628                             ==> &0 < azim_dart (V,E) x`,
2629    REPEAT STRIP_TAC THEN
2630      MP_TAC (SPEC_ALL IN_DART_OF_FAN) THEN
2631      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2632      ASM_CASES_TAC `v,w IN dart1_of_fan (V:real^3->bool,E)` THENL
2633      [
2634        MP_TAC (SPEC_ALL (ISPEC `V:real^3->bool` PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ)) THEN
2635          ASM_SIMP_TAC[azim_dart; azim_fan] THEN DISCH_TAC THEN
2636          ASM_CASES_TAC `CARD (set_of_edge (v:real^3) V E) > 1` THEN ASM_REWRITE_TAC[] THENL
2637          [
2638            MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ ~(a = &0) ==> &0 < a`) THEN
2639              REWRITE_TAC[azim] THEN
2640              ABBREV_TAC `w' = sigma_fan (vec 0) V E v w` THEN
2641              MP_TAC (SPEC_ALL PAIR_IN_DART1_OF_FAN) THEN
2642              ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2643              SUBGOAL_THEN `w' IN (set_of_edge v V E) /\ ~(w' = w:real^3)` STRIP_ASSUME_TAC THENL
2644              [
2645                MP_TAC (SPECL [`vec 0:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`; `w:real^3`] Fan.SIGMA_FAN) THEN
2646                  ASM_REWRITE_TAC[] THEN
2647                  ANTS_TAC THEN SIMP_TAC[] THEN
2648                  FIRST_ASSUM (MP_TAC o check (is_binary ">" o concl)) THEN
2649                  MATCH_MP_TAC (TAUT `(A ==> ~B) ==> (B ==> ~A)`) THEN
2650                  DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
2651                  REWRITE_TAC[Hypermap.CARD_SINGLETON] THEN
2652                  REWRITE_TAC[GT; LT_REFL];
2653                ALL_TAC
2654              ] THEN
2655              POP_ASSUM MP_TAC THEN
2656              REWRITE_TAC[CONTRAPOS_THM] THEN
2657              DISCH_TAC THEN
2658              MATCH_MP_TAC (GSYM Fan.UNIQUE_AZIM_0_POINT_FAN) THEN
2659              MAP_EVERY EXISTS_TAC [`vec 0:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] THEN
2660              ASM_REWRITE_TAC[] THEN
2661              REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
2662              SIMP_TAC[set_of_edge; IN_ELIM_THM];
2663            ALL_TAC
2664          ] THEN
2665          MATCH_MP_TAC REAL_LT_MUL THEN
2666          REWRITE_TAC[PI_POS] THEN REAL_ARITH_TAC;
2667        ALL_TAC
2668      ] THEN
2669      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `dart_of_fan (V:real^3->bool,E)`)) THEN
2670      ASM_REWRITE_TAC[dart_of_fan; GSYM dart1_of_fan; IN_UNION] THEN
2671      REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
2672      ASM_REWRITE_TAC[] THEN REWRITE_TAC[azim_dart] THEN
2673      MATCH_MP_TAC REAL_LT_MUL THEN
2674      REWRITE_TAC[PI_POS] THEN REAL_ARITH_TAC);;
2675
2676
2677
2678 (* 0,v,w are not collinear *)
2679 let DART1_NOT_COLLINEAR = prove(`!V E v (w:real^3). FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
2680                                   ==> ~collinear {vec 0,v,w}`,
2681    REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_TAC THEN
2682      FIRST_ASSUM MP_TAC THEN
2683      REWRITE_TAC[FAN; fan6] THEN STRIP_TAC THEN
2684      MP_TAC (SPEC_ALL (SPEC `V:real^3->bool` PAIR_IN_DART1_OF_FAN)) THEN
2685      ASM_REWRITE_TAC[set_of_edge; IN_ELIM_THM] THEN
2686      STRIP_TAC THEN
2687      FIRST_ASSUM (MP_TAC o SPEC `{v:real^3,w}`) THEN
2688      REWRITE_TAC[SET_RULE `{a:real^3} UNION {v,w} = {a,v,w}`] THEN
2689      ASM_SIMP_TAC[]);;
2690
2691
2692 (* {0,v,w} and {0,v,sigma(v)(w)} are not collinear *)
2693 let DART1_NOT_COLLINEAR_2 = prove(`!V E v (w:real^3). FAN (vec 0,V,E) /\ (v,w) IN dart1_of_fan (V,E)
2694                                     ==> ~collinear {vec 0,v,w} /\ ~collinear {vec 0,v,sigma_fan (vec 0) V E v w}`,
2695    REPEAT GEN_TAC THEN DISCH_TAC THEN
2696      MP_TAC (SPEC_ALL DART1_NOT_COLLINEAR) THEN
2697      ASM_SIMP_TAC[] THEN DISCH_TAC THEN
2698      SUBGOAL_THEN `(v,sigma_fan (vec 0) V E v w) IN dart1_of_fan (V:real^3->bool,E)` ASSUME_TAC THENL
2699      [
2700        MATCH_MP_TAC Hypermap.lemma_in_subset THEN
2701          EXISTS_TAC `node (hypermap_of_fan (V,E)) (v,w)` THEN CONJ_TAC THENL
2702          [
2703            ASM_SIMP_TAC[NODE_SUBSET_DART1_OF_FAN];
2704            ALL_TAC
2705          ] THEN
2706          ASM_SIMP_TAC[NODE_HYPERMAP_OF_FAN; IN_ELIM_THM] THEN
2707          EXISTS_TAC `1` THEN
2708          REWRITE_TAC[ARITH_RULE `1 >= 0`; Hypermap.POWER_1];
2709        ALL_TAC
2710      ] THEN
2711      MATCH_MP_TAC DART1_NOT_COLLINEAR THEN
2712      MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
2713      ASM_REWRITE_TAC[]);;
2714
2715
2716 open Hypermap;;
2717
2718 let ORBIT_MAP_RES_LEMMA = prove(`!f (x:A) s. orbit_map f x SUBSET s ==>
2719                             orbit_map (res f s) x = orbit_map f x`,
2720    REWRITE_TAC[SUBSET; orbit_map; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
2721      REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
2722      SUBGOAL_THEN `!n. (res f s POWER n) x = (f POWER n) (x:A)` ASSUME_TAC THENL
2723      [
2724        INDUCT_TAC THEN REWRITE_TAC[POWER_0] THEN
2725          ASM_REWRITE_TAC[COM_POWER; o_THM] THEN
2726          REWRITE_TAC[res] THEN
2727          SUBGOAL_THEN `(f POWER n) (x:A) IN s` (fun th -> REWRITE_TAC[th]) THEN
2728          FIRST_X_ASSUM MATCH_MP_TAC THEN
2729          EXISTS_TAC `n:num` THEN
2730          REWRITE_TAC[GE; LE_0];
2731        ALL_TAC
2732      ] THEN
2733      ASM_REWRITE_TAC[]);;
2734
2735
2736 let ORBIT_SUBSET_LEMMA = prove(`!f s (x:A). x IN s /\ (!y. y IN s ==> f y IN s)
2737                                  ==> orbit_map f x SUBSET s`,
2738    REPEAT STRIP_TAC THEN
2739      REWRITE_TAC[orbit_map; SUBSET; IN_ELIM_THM] THEN
2740      GEN_TAC THEN DISCH_THEN CHOOSE_TAC THEN POP_ASSUM MP_TAC THEN
2741      SPEC_TAC (`x':A`, `y:A`) THEN
2742      SPEC_TAC (`n:num`, `n:num`) THEN
2743      INDUCT_TAC THEN ASM_SIMP_TAC[GE; LE_0; POWER_0; I_THM] THEN
2744      GEN_TAC THEN REWRITE_TAC[COM_POWER; o_THM] THEN
2745      DISCH_TAC THEN
2746      FIRST_X_ASSUM (MP_TAC o SPEC `(f POWER n) (x:A)`) THEN
2747      ASM_REWRITE_TAC[GE; LE_0]);;
2748
2749
2750 let ORBIT_MAP_RES = prove(`!f (x:A) s. x IN s /\ (res f s) permutes s
2751                             ==> orbit_map (res f s) x = orbit_map f x`,
2752    REPEAT STRIP_TAC THEN
2753      MATCH_MP_TAC ORBIT_MAP_RES_LEMMA THEN
2754      MATCH_MP_TAC ORBIT_SUBSET_LEMMA THEN
2755      ASM_REWRITE_TAC[] THEN
2756      REPEAT STRIP_TAC THEN
2757      SUBGOAL_THEN `(f:A->A) y = (res f s) y` (fun th -> REWRITE_TAC[th]) THENL
2758      [
2759        ASM_REWRITE_TAC[res];
2760        ALL_TAC
2761      ] THEN
2762      MP_TAC (ISPECL [`res (f:A->A) s`; `s:A->bool`] PERMUTES_IMP_INSIDE) THEN
2763      ASM_SIMP_TAC[]);;
2764
2765
2766
2767 end;;