text_formalization/tame/TameGeneral.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Tame Hypermap                                                     *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2010-06-17                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 (* General properties of a contravening packing   *)\r
  10 \r
  11 \r
  12 flyspeck_needs "leg/collect_geom.hl";;\r
  13 flyspeck_needs "trigonometry/trigonometry.hl";;\r
  14 flyspeck_needs "nonlinear/ineq.hl";;\r
  15 \r
  16 flyspeck_needs "fan/HypermapAndFan.hl";;\r
  17 flyspeck_needs "tame/CKQOWSA.hl";;\r
  18 flyspeck_needs "tame/tame_defs.hl";;\r
  19 \r
  20 \r
  21 module Tame_general = struct\r
  22 \r
  23 open Fan_defs;;\r
  24 open Hypermap_and_fan;;\r
  25 open Tame_defs;;\r
  26 \r
  27 \r
  28 \r
  29 (* Non-linear inequalities *)\r
  30 (* let tame_hypermap_calcs_concl = new_definition Tame_defs.tame_hypermap_calcs;; *)\r
  31 \r
  32 \r
  33 (* tame ==> restricted *)\r
  34 let RUNOQPQ = prove(`!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`,\r
  35     GEN_TAC THEN REWRITE_TAC[tame_hypermap; restricted_hypermap] THEN\r
  36       SIMP_TAC[tame_1; tame_2; tame_3; tame_5a; tame_9a] THEN\r
  37       REPEAT STRIP_TAC THENL\r
  38       [\r
  39         FIRST_X_ASSUM (MP_TAC o check (fun th -> (concl th) = `tame_8 (H:(A)hypermap)`)) THEN\r
  40           REWRITE_TAC[tame_8; Hypermap.number_of_faces; Hypermap.face_set; Hypermap.set_of_orbits] THEN\r
  41           SUBGOAL_THEN `{orbit_map (face_map (H:(A)hypermap)) x | x | x IN dart H} = {}` (fun th -> REWRITE_TAC[th]) THENL\r
  42           [\r
  43             ASM_REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN\r
  44               X_GEN_TAC `ff:A->bool` THEN\r
  45               REWRITE_TAC[IN_ELIM_THM];\r
  46             ALL_TAC\r
  47           ] THEN\r
  48           REWRITE_TAC[CARD_CLAUSES; ARITH_RULE `~(0 >= 3)`];\r
  49 \r
  50         MP_TAC (SPEC `H:(A)hypermap` Hypermap.lemmaZHQCZLX) THEN\r
  51           ASM_SIMP_TAC[is_node_nondegenerate; GSYM GE];\r
  52 \r
  53         POP_ASSUM MP_TAC THEN\r
  54           REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits] THEN\r
  55           ONCE_REWRITE_TAC[GSYM Hypermap.face] THEN\r
  56           REWRITE_TAC[IN_ELIM_THM] THEN\r
  57           STRIP_TAC THEN\r
  58           ASM_SIMP_TAC[]\r
  59       ]);;\r
  60 \r
  61 \r
  62 (* UBHDEUU1 = CKQOWSA *)\r
  63 let UBHDEUU1 = Ckqowsa.CKQOWSA;;\r
  64 \r
  65 \r
  66 (* (V,ECTC V) is a fan *)\r
  67 let UBHDEUU2 = prove(`!V. packing V /\ V SUBSET ball_annulus /\ ~(V = {}) ==> FAN(vec 0, V, ECTC V)`,\r
  68    REPEAT STRIP_TAC THEN\r
  69      MATCH_MP_TAC Topology.CTVTAQA THEN\r
  70      EXISTS_TAC `ESTD V` THEN\r
  71      ASM_SIMP_TAC[UBHDEUU1] THEN\r
  72      REWRITE_TAC[ECTC; ESTD; SUBSET; IN_ELIM_THM] THEN\r
  73      REPEAT STRIP_TAC THEN\r
  74      MAP_EVERY EXISTS_TAC [`v:real^3`; `w:real^3`] THEN\r
  75      ASM_SIMP_TAC[Sphere.h0; REAL_ARITH `a = &2 ==> a <= &2 * #1.26`]);;\r
  76    \r
  77 \r
  78 \r
  79 (*********************)\r
  80 (* Numerical results *)\r
  81 (*********************)\r
  82 \r
  83 let COS_PI3 = prove(`cos (pi / &3) = &1 / &2`,\r
  84    REWRITE_TAC[COS_SIN] THEN\r
  85      REWRITE_TAC[REAL_ARITH `pi / &2 - pi / &3 = pi / &6`] THEN\r
  86      REWRITE_TAC[SIN_PI6]);;\r
  87 \r
  88 \r
  89 let ACS_2 = prove(`acs (&1 / &2) = pi / &3`,\r
  90    REWRITE_TAC[SYM COS_PI3] THEN\r
  91      MATCH_MP_TAC ACS_COS THEN\r
  92      REWRITE_TAC[REAL_ARITH `(&0 <= a / &3 <=> &0 <= a) /\ (a / &3 <= a <=> &0 <= a)`] THEN\r
  93      MATCH_MP_TAC REAL_LT_IMP_LE THEN\r
  94      REWRITE_TAC[PI_POS]);;\r
  95 \r
  96 \r
  97 let sol0_POS = prove(`&0 < sol0`,\r
  98    REWRITE_TAC[Pack_defs.sol0] THEN\r
  99      REWRITE_TAC[REAL_ARITH `&0 < &3 * a - pi <=> pi / &3 < a`] THEN\r
 100      REWRITE_TAC[SYM ACS_2] THEN\r
 101      MATCH_MP_TAC ACS_MONO_LT THEN\r
 102      REAL_ARITH_TAC);;\r
 103 \r
 104          \r
 105 (****************************************)       \r
 106 \r
 107 \r
 108 \r
 109 (*******************************************************************************************)\r
 110 (* Connections between algebraic definitions in Sphere and geometric definitions elsewhere *)\r
 111 (*******************************************************************************************)\r
 112 \r
 113 (* ly = lmfun *)\r
 114 let ly_EQ_lmfun = prove(`!x:real^3#real^3. norm (FST x) <= &2 * h0 ==> lmfun (h_dart x) = ly (norm (FST x))`,\r
 115    REWRITE_TAC[Pack_defs.lmfun; Sphere.ly; Sphere.interp; h_dart; Pack_defs.h0] THEN\r
 116      REAL_ARITH_TAC);;\r
 117 \r
 118 \r
 119 \r
 120 (* sol0 = const1 * pi *)\r
 121 let sol0_EQ_sol_y = prove(`sol0 = sol_y (&2) (&2) (&2) (&2) (&2) (&2)`,\r
 122     REWRITE_TAC[Pack_defs.sol0; Sphere.sol_y; Sphere.dih_y; Sphere.dih_x; Sphere.delta_x4; Sphere.delta_x] THEN\r
 123       CONV_TAC (DEPTH_CONV let_CONV) THEN\r
 124       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN\r
 125       MP_TAC (SPEC `&1 / &3` Trigonometry2.acs_atn2) THEN\r
 126       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN\r
 127       DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 128       REWRITE_TAC [REAL_ARITH `&3 * (a - b) - c = (a + d) + (a + d) + (a + d) - c <=> --b = d`] THEN\r
 129       MP_TAC (SPECL [`sqrt (&8 / &9)`; `&1 / &3`] Trigonometry1.ATN2_RNEG) THEN\r
 130       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN\r
 131       DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN\r
 132       SUBGOAL_THEN `sqrt (&2048) = &48 * sqrt (&8 / &9) /\ -- &16 = &48 * (-- &1 / &3)` ASSUME_TAC THENL\r
 133       [\r
 134         MP_TAC (SPECL [`&48`; `&8 / &9`] Vol1.SQRT_MUL_POW_2) THEN\r
 135           CONV_TAC (REAL_RAT_REDUCE_CONV);\r
 136         ALL_TAC\r
 137       ] THEN\r
 138       ASM_REWRITE_TAC[] THEN\r
 139       MATCH_MP_TAC (GSYM Trigonometry1.ATN2_LMUL_EQ) THEN\r
 140       REAL_ARITH_TAC);;\r
 141 \r
 142 \r
 143 (* sol0 = const1 *)\r
 144 let sol0_over_pi_EQ_const1 = prove(`sol0 / pi = const1`,\r
 145    REWRITE_TAC[sol0_EQ_sol_y; Sphere.const1]);;\r
 146          \r
 147 \r
 148          \r
 149 (* Alternative form for ineq *)\r
 150 let INEQ_ALT = prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,\r
 151   GEN_TAC THEN\r
 152     MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL\r
 153     [\r
 154       REWRITE_TAC[Sphere.ineq; ALL];\r
 155       ALL_TAC\r
 156     ] THEN\r
 157     MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN\r
 158     DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN\r
 159     DISCH_THEN (CHOOSE_THEN MP_TAC) THEN\r
 160     MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN\r
 161     DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN\r
 162     DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN\r
 163     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 164     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 165     ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;\r
 166 \r
 167 \r
 168 (* delta = delta_x *)   \r
 169 let DELTA_EQ_DELTA_X = prove(`!x1 x2 x3 x4 x5 x6. \r
 170                                delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,\r
 171   REPEAT GEN_TAC THEN\r
 172     REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN\r
 173     REAL_ARITH_TAC);;\r
 174 \r
 175 \r
 176 (* Connection between delta_x and delta_x4 *)\r
 177 let DELTA_X_AND_DELTA_X4 = prove(`!x1 x2 x3 x4 x5 x6.\r
 178                                  (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in\r
 179                                  let d = delta_x x1 x2 x3 x4 x5 x6 in\r
 180                                  let v1 = ups_x x1 x2 x6 in\r
 181                                  let v2 = ups_x x1 x3 x5 in\r
 182                                  &4 * x1 * d = v1 * v2 - d4 * d4)`,\r
 183   REPEAT GEN_TAC THEN \r
 184     REPEAT (CONV_TAC let_CONV) THEN\r
 185     REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN\r
 186     REAL_ARITH_TAC);;\r
 187 \r
 188 \r
 189 \r
 190 \r
 191 (* dihV = dih_y *)\r
 192 let DIHV_EQ_DIH_Y = prove(`!v0:real^3 v1 v2 v3. ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3}\r
 193                             ==> (let v01 = dist (v0, v1) in\r
 194                                  let v02 = dist (v0, v2) in\r
 195                                  let v03 = dist (v0, v3) in\r
 196                                  let v12 = dist (v1, v2) in\r
 197                                  let v13 = dist (v1, v3) in\r
 198                                  let v23 = dist (v2, v3) in\r
 199                                    dihV v0 v1 v2 v3 = dih_y v01 v02 v03 v23 v13 v12)`,\r
 200   REPEAT GEN_TAC THEN\r
 201     DISCH_TAC THEN\r
 202     FIRST_ASSUM (MP_TAC o (fun th -> CONJUNCT2 (MATCH_MP (let_RULE Trigonometry.OJEKOJF) th))) THEN\r
 203     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 204     REPEAT (CONV_TAC let_CONV) THEN\r
 205     MAP_EVERY ABBREV_TAC [`v01 = dist(v0:real^3,v1)`; `v02 = dist(v0:real^3,v2)`;\r
 206                           `v03 = dist(v0:real^3,v3)`; `v12 = dist(v1:real^3,v2)`;\r
 207                           `v13 = dist(v1:real^3,v3)`; `v23 = dist(v2:real^3,v3)`;\r
 208                           `d = delta_x (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`;\r
 209                           `d4 = delta_x4 (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`] THEN\r
 210     REWRITE_TAC[let_RULE Sphere.dih_y; let_RULE Sphere.dih_x; GSYM REAL_POW_2] THEN\r
 211     ASM_REWRITE_TAC[REAL_ARITH `a - b = a + c <=> c = --b`] THEN\r
 212     \r
 213     MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN\r
 214     DISJ_CASES_TAC (TAUT `~(d4 = &0) \/ d4 = &0`) THEN ASM_REWRITE_TAC[] THEN\r
 215     MATCH_MP_TAC SQRT_POS_LT THEN\r
 216 \r
 217     MP_TAC (let_RULE (SPECL [`v01 pow 2`; `v02 pow 2`; `v03 pow 2`; `v23 pow 2`; `v13 pow 2`; `v12 pow 2`] DELTA_X_AND_DELTA_X4)) THEN\r
 218     ASM_REWRITE_TAC[] THEN\r
 219     DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a - &0 * &0 = a`]) THEN\r
 220     \r
 221     MP_TAC (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT) THEN\r
 222     ASM_REWRITE_TAC[] THEN\r
 223     MP_TAC (INST [`v3:real^3`,`v2:real^3`] (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)) THEN\r
 224     ASM_REWRITE_TAC[] THEN\r
 225     REPEAT DISCH_TAC THEN\r
 226     MATCH_MP_TAC REAL_LT_MUL THEN\r
 227     ASM_REWRITE_TAC[]);;\r
 228 \r
 229         \r
 230 \r
 231     \r
 232 \r
 233 (************************************************************************************)  \r
 234 \r
 235 \r
 236  (* Properties of a contravening packing *)\r
 237  \r
 238  (* LEMMA: aux *)\r
 239  let DIFF_LEMMA = prove(`!A B. A SUBSET B ==> (A = B DIFF (B DIFF A))`,\r
 240                        REWRITE_TAC[SUBSET; EXTENSION; IN_DIFF; DE_MORGAN_THM] THEN\r
 241                          REWRITE_TAC[TAUT `P /\ (~P \/ Q) <=> P /\ Q`] THEN\r
 242                          REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[]);;\r
 243 \r
 244 \r
 245 \r
 246 (* (V,ESTD V) is a fan for a contravening packing V *)\r
 247 let CONTRAVENING_FAN = prove(`!V. contravening V ==> FAN (vec 0,V,ESTD V)`,\r
 248    REWRITE_TAC[contravening] THEN\r
 249      GEN_TAC THEN REWRITE_TAC[GSYM IMP_IMP] THEN\r
 250      REPLICATE_TAC 5 DISCH_TAC THEN\r
 251      REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN\r
 252      MATCH_MP_TAC Ckqowsa.CKQOWSA THEN\r
 253      ASM_REWRITE_TAC[] THEN\r
 254      POP_ASSUM (LABEL_TAC "A") THEN DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN\r
 255      ASM_REWRITE_TAC[CARD_CLAUSES] THEN\r
 256      ARITH_TAC);;\r
 257      \r
 258 \r
 259 \r
 260 \r
 261 (* LEMMA: aux *)\r
 262 let CONTRAVENING_IMP_SURROUNDED = prove(`!V v. contravening V /\ v IN V ==> surrounded_node (V,ESTD V) v`,\r
 263                                         ASM_SIMP_TAC[contravening]);;\r
 264 \r
 265 \r
 266 let CONTRAVENING_IMP_FULLY_SURROUNDED = prove(`!V. FAN (vec 0,V,ESTD V) /\ contravening V \r
 267                                               ==> fully_surrounded (V,ESTD V)`,\r
 268    REPEAT STRIP_TAC THEN\r
 269      ASM_SIMP_TAC[FULLY_SURROUNDED] THEN\r
 270      REPEAT STRIP_TAC THEN\r
 271      ASM_SIMP_TAC[CONTRAVENING_IMP_SURROUNDED]);;\r
 272     \r
 273 \r
 274 \r
 275 (* LEMMA: general *)\r
 276 let CONTRAVENING_IMP_IN_DART1_OF_FAN = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)\r
 277                                                  ==> x IN dart1_of_fan (V,ESTD V)`,\r
 278    REPEAT GEN_TAC THEN\r
 279      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN\r
 280      STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 281      REPEAT STRIP_TAC THEN\r
 282      ASSUME_TAC (SPEC `V:real^3->bool` CONTRAVENING_FAN) THEN\r
 283      MATCH_MP_TAC SURROUNDED_IMP_IN_DART1_OF_FAN THEN\r
 284      ASM_SIMP_TAC[] THEN\r
 285      MATCH_MP_TAC CONTRAVENING_IMP_SURROUNDED THEN\r
 286      ASM_REWRITE_TAC[] THEN\r
 287      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x':real^3`; `y:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 288      ASM_SIMP_TAC[]);;\r
 289 \r
 290 \r
 291 (* LEMMA: general *)\r
 292 let CONTRAVENING_IMP_DART_FST_NEQ_SND = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)\r
 293                                                 ==> ~(FST x = SND x)`,\r
 294    REPEAT STRIP_TAC THEN\r
 295      POP_ASSUM MP_TAC THEN\r
 296      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 297      MP_TAC (SPEC_ALL CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN\r
 298      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 299      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART1_OF_FAN) THEN\r
 300      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN\r
 301      ASM_REWRITE_TAC[] THEN\r
 302      MATCH_MP_TAC PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ THEN\r
 303      MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `ESTD V`] THEN\r
 304      ASM_REWRITE_TAC[]);;\r
 305      \r
 306 \r
 307 \r
 308 \r
 309 (* LEMMA: general *)\r
 310 let CONTRAVENING_DIST = prove(`!V v. contravening V /\ v IN V\r
 311                               ==> #2.0 <= dist(vec 0, v) /\ dist(vec 0,v) <= #2.52\r
 312                                /\ (!w. w IN V /\ ~(v = w) ==> #2.0 <= dist(v, w))`,\r
 313    REPEAT GEN_TAC THEN\r
 314      REWRITE_TAC[contravening] THEN\r
 315      DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
 316      DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (MP_TAC o CONJUNCT1)) THEN\r
 317      REWRITE_TAC[Pack_defs.ball_annulus; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN\r
 318      REWRITE_TAC[SUBSET; IN_DIFF; cball; ball; IN_ELIM_THM; REAL_NOT_LT] THEN\r
 319      DISCH_THEN (MP_TAC o SPEC `v:real^3`) THEN\r
 320      ASM_SIMP_TAC[REAL_ARITH `&2 = #2.0`] THEN\r
 321      DISCH_THEN (fun th -> ALL_TAC) THEN\r
 322      REWRITE_TAC[Sphere.packing; REAL_ARITH `#2.0 = &2`] THEN\r
 323      ASM SET_TAC[]);;\r
 324          \r
 325          \r
 326 (* LEMMA: aux *)\r
 327 let IN_ESTD = prove(`!V v w. {v,w} IN ESTD V <=> v IN V /\ w IN V /\ ~(v = w) /\ dist(v,w) <= #2.52`,\r
 328     REPEAT GEN_TAC THEN\r
 329       REWRITE_TAC[ESTD; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN\r
 330       EQ_TAC THENL\r
 331       [\r
 332         REWRITE_TAC[IN_ELIM_THM] THEN\r
 333           STRIP_TAC THEN\r
 334           SUBGOAL_THEN `(v:real^3 = v' /\ w:real^3 = w') \/ (v = w' /\ w = v')` MP_TAC THENL\r
 335           [\r
 336             POP_ASSUM MP_TAC THEN SET_TAC[];\r
 337             ALL_TAC\r
 338           ] THEN\r
 339           ASM_MESON_TAC[DIST_SYM];\r
 340         SET_TAC[]\r
 341       ]);;\r
 342 \r
 343 \r
 344 (* LEMMA: general *)\r
 345 let CONTRAVENING_ESTD_DIST = prove(`!V v w. contravening V /\ v IN V /\ w IN V /\ {v,w} IN ESTD V\r
 346                                    ==> #2.0 <= dist(v,w) /\ dist(v,w) <= #2.52`,\r
 347    REPEAT GEN_TAC THEN\r
 348      REWRITE_TAC[contravening; IN_ESTD; Sphere.packing] THEN\r
 349      DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
 350      DISCH_THEN (MP_TAC o CONJUNCT1) THEN\r
 351      ASM_REWRITE_TAC[REAL_ARITH `#2.0 = &2`] THEN\r
 352      ASM SET_TAC[]);;\r
 353 \r
 354 \r
 355 \r
 356 (* LEMMA: general *)\r
 357 let CONTRAVENING_DART_DIST = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)\r
 358                                      ==> #2.0 <= dist x /\ dist x <= #2.52`,\r
 359    REPEAT GEN_TAC THEN DISCH_TAC THEN\r
 360      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 361      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN\r
 362      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 363      MATCH_MP_TAC CONTRAVENING_ESTD_DIST THEN\r
 364      EXISTS_TAC `V:real^3->bool` THEN\r
 365      ASM_REWRITE_TAC[] THEN\r
 366      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN\r
 367      MP_TAC (SPEC_ALL CONTRAVENING_IMP_SURROUNDED) THEN\r
 368      ASM_REWRITE_TAC[] THEN\r
 369      DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 370      REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN\r
 371      STRIP_TAC THEN\r
 372      ASM_REWRITE_TAC[]);;\r
 373                         \r
 374 \r
 375     \r
 376 \r
 377 (* LEMMA: general *)\r
 378 let CONTRAVENING_LMFUN_BOUND = prove(`!V v. contravening V /\ v IN V\r
 379                                        ==> lmfun (norm v / &2) <= &1`,\r
 380    REPEAT GEN_TAC THEN \r
 381      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP CONTRAVENING_DIST th)) THEN\r
 382      REWRITE_TAC[DIST_SYM] THEN\r
 383      REWRITE_TAC[dist; VECTOR_SUB_RZERO; Pack_defs.lmfun; Pack_defs.h0] THEN\r
 384      REAL_ARITH_TAC);;\r
 385 \r
 386 \r
 387 \r
 388 \r
 389 \r
 390 (* LEMMA: aux *)\r
 391 let CONTRAVENING_IMP_AZIM_DART_EQ_AZIM = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)\r
 392                         ==> azim_dart (V,ESTD V) (v,w) = azim (vec 0) v w (sigma_fan (vec 0) V (ESTD V) v w)`,\r
 393    REPEAT STRIP_TAC THEN\r
 394      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 395      MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_DART_FST_NEQ_SND) THEN\r
 396      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`] SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3) THEN\r
 397      MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_IMP_SURROUNDED) THEN\r
 398      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 399      ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN\r
 400      ASM_SIMP_TAC[azim_dart; azim_fan; ARITH_RULE `a >= 3 ==> a > 1`]);;\r
 401 \r
 402 \r
 403 \r
 404 \r
 405 (* 0, v, w, and sigma(v)(w) are not coplanar *)\r
 406 let CONTRAVENING_IMP_NOT_COPLANAR = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)\r
 407                             ==> ~coplanar {vec 0, v, w, sigma_fan (vec 0) V (ESTD V) v w}`,\r
 408    REPEAT GEN_TAC THEN DISCH_TAC THEN\r
 409      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN  \r
 410      MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN\r
 411      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 412      MP_TAC (SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `sigma_fan (vec 0) V (ESTD V) v w`] AZIM_EQ_0_PI_EQ_COPLANAR) THEN\r
 413      ANTS_TAC THENL\r
 414      [\r
 415        MATCH_MP_TAC DART1_NOT_COLLINEAR_2 THEN\r
 416          ASM_REWRITE_TAC[];\r
 417        ALL_TAC\r
 418      ] THEN\r
 419      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN\r
 420      REWRITE_TAC[DE_MORGAN_THM] THEN\r
 421      ASM_SIMP_TAC[GSYM CONTRAVENING_IMP_AZIM_DART_EQ_AZIM] THEN\r
 422      CONJ_TAC THENL\r
 423      [\r
 424        MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN\r
 425          MATCH_MP_TAC AZIM_DART_POS THEN\r
 426          ASM_REWRITE_TAC[];\r
 427        MATCH_MP_TAC (REAL_ARITH `a < pi ==> ~(a = pi)`) THEN\r
 428          MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN\r
 429          ASM_REWRITE_TAC[fully_surrounded] THEN\r
 430          DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN\r
 431          ASM_SIMP_TAC[]\r
 432      ]);;\r
 433          \r
 434          \r
 435 \r
 436  \r
 437 \r
 438 (* azim_dart = dih_y *)  \r
 439 let CONTRAVENING_AZIM_DART_EQ_DIH_Y = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)\r
 440                 ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in\r
 441                     let y1 = norm v in\r
 442                     let y2 = norm w in\r
 443                     let y3 = norm w' in\r
 444                     let y4 = dist (w,w') in\r
 445                     let y5 = dist (v,w') in\r
 446                     let y6 = dist (v,w) in\r
 447                       azim_dart (V,ESTD V) (v,w) = dih_y y1 y2 y3 y4 y5 y6`,\r
 448    REPEAT STRIP_TAC THEN REPEAT (CONV_TAC let_CONV) THEN\r
 449      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 450      ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN\r
 451      MP_TAC (SPEC_ALL CONTRAVENING_IMP_AZIM_DART_EQ_AZIM) THEN\r
 452      MP_TAC (SPEC_ALL CONTRAVENING_IMP_NOT_COPLANAR) THEN\r
 453      ASM_REWRITE_TAC[] THEN\r
 454      REPEAT STRIP_TAC THEN\r
 455 \r
 456      SUBGOAL_THEN `~collinear {vec 0, v, w:real^3} /\ ~collinear {vec 0, v, w'}` ASSUME_TAC THENL\r
 457      [\r
 458        CONJ_TAC THEN MATCH_MP_TAC NOT_COPLANAR_NOT_COLLINEAR THENL\r
 459          [\r
 460            EXISTS_TAC `w':real^3` THEN ASM_REWRITE_TAC[];\r
 461            EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[SET_RULE `{a:real^3,b,c,d} = {a,b,d,c}`]\r
 462          ];\r
 463        ALL_TAC\r
 464      ] THEN\r
 465      \r
 466      MP_TAC ((let_RULE o SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `w':real^3`]) DIHV_EQ_DIH_Y) THEN\r
 467      ASM_REWRITE_TAC[DIST_0] THEN\r
 468      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN\r
 469      MATCH_MP_TAC AZIM_DIHV_SAME THEN\r
 470      POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 471      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 472      MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN\r
 473      ASM_REWRITE_TAC[fully_surrounded] THEN\r
 474      DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN\r
 475      ASM_SIMP_TAC[]);;\r
 476 \r
 477 \r
 478 \r
 479       \r
 480 (* Lower bound for CARD(face) in a contravening packing *)\r
 481 let CONTRAVENING_IMP_CARD_FACE_GE_3 = prove(`!V. contravening V\r
 482                       ==> (!x. x IN dart_of_fan (V,ESTD V) ==> CARD (face (hypermap_of_fan (V,ESTD V)) x) >= 3)`,\r
 483                             MESON_TAC[CONTRAVENING_FAN; FULLY_SURROUNDED_IMP_CARD_FACE_GE_3; CONTRAVENING_IMP_FULLY_SURROUNDED]);;\r
 484 \r
 485 \r
 486 \r
 487 (* Alternative form for type_of_node H x *)\r
 488 let NODE_TYPE_lemma = prove(`!H (x:A). simple_hypermap H /\ x IN dart H\r
 489                     ==> type_of_node H x = CARD {y | y IN node H x /\ CARD (face H y) = 3},\r
 490                                            CARD {y | y IN node H x /\ CARD (face H y) = 4},\r
 491                                            CARD {y | y IN node H x /\ CARD (face H y) >= 5}`,\r
 492    REPEAT GEN_TAC THEN\r
 493      DISCH_THEN (MP_TAC o (fun th -> MATCH_MP SIMPLE_HYPERMAP_lemma th)) THEN\r
 494      REWRITE_TAC[type_of_node] THEN\r
 495      REWRITE_TAC[set_of_triangles_meeting_node; set_of_quadrilaterals_meeting_node; set_of_exceptional_meeting_node] THEN\r
 496      DISCH_THEN (fun th -> REWRITE_TAC[th]));;\r
 497 \r
 498 \r
 499 (* CARD (node) = p + q + r *)\r
 500 let FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE = \r
 501   prove(`!V E x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 502           fully_surrounded (V,E) /\ x IN dart_of_fan (V,E)\r
 503         ==> (let p,q,r = type_of_node (hypermap_of_fan (V,E)) x in\r
 504                CARD (node (hypermap_of_fan (V,E)) x) = p + q + r)`,\r
 505    REPEAT STRIP_TAC THEN\r
 506      MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN\r
 507      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 508      DISCH_THEN (fun th -> ALL_TAC) THEN\r
 509      CONV_TAC let_CONV THEN\r
 510      ABBREV_TAC `H = hypermap_of_fan (V:real^3->bool,E)` THEN\r
 511      ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN\r
 512      ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN\r
 513      ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN\r
 514      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN\r
 515      ASM_REWRITE_TAC[] THEN\r
 516      DISCH_THEN (MP_TAC o let_RULE) THEN\r
 517      ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN\r
 518      ASM_REWRITE_TAC[] THEN\r
 519      STRIP_TAC THEN \r
 520 \r
 521      SUBGOAL_THEN `CARD (B:real^3#real^3->bool) + CARD (C:real^3#real^3->bool) = CARD (D:real^3#real^3->bool)` MP_TAC THENL\r
 522      [\r
 523        MATCH_MP_TAC CARD_UNION_EQ THEN\r
 524          ASM_SIMP_TAC[GSYM DISJOINT];\r
 525        ALL_TAC\r
 526      ] THEN\r
 527 \r
 528      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 529      MATCH_MP_TAC EQ_SYM THEN\r
 530      MATCH_MP_TAC CARD_UNION_EQ THEN\r
 531      ASM_SIMP_TAC[Hypermap.NODE_FINITE; GSYM DISJOINT]);;\r
 532 \r
 533          \r
 534          \r
 535 (******************************************************************************)\r
 536 \r
 537 \r
 538 (* tauVEF = taum for a triangular face *)\r
 539 let tauVEF_EQ_taum = prove(`!V f. contravening V /\\r
 540                              f IN face_set_of_fan (V,ESTD V) /\\r
 541                              CARD (f) = 3 \r
 542         ==> (!v w. (v,w) IN f ==>\r
 543              let w' = sigma_fan (vec 0) V (ESTD V) v w in\r
 544              let y1 = norm v in\r
 545              let y2 = norm w in\r
 546              let y3 = norm w' in\r
 547              let y4 = dist(w,w') in\r
 548              let y5 = dist(v,w') in\r
 549              let y6 = dist(v,w) in\r
 550                tauVEF (V,ESTD V,f) = taum y1 y2 y3 y4 y5 y6)`,\r
 551    REPEAT STRIP_TAC THEN\r
 552      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 553      UNDISCH_TAC `f IN face_set_of_fan (V,ESTD V)` THEN\r
 554      REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN\r
 555      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 556      STRIP_TAC THEN\r
 557      SUBGOAL_THEN `face (hypermap_of_fan (V,ESTD V)) (v,w) = f` MP_TAC THENL\r
 558      [\r
 559        ASM_REWRITE_TAC[] THEN\r
 560          MATCH_MP_TAC (GSYM Hypermap.lemma_face_identity) THEN\r
 561          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);\r
 562        ALL_TAC\r
 563      ] THEN\r
 564      SUBGOAL_THEN `(v,w) IN dart1_of_fan (V,ESTD V)` MP_TAC THENL\r
 565      [\r
 566        MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 567          EXISTS_TAC `f:real^3#real^3->bool` THEN\r
 568          ASM_REWRITE_TAC[] THEN\r
 569          MATCH_MP_TAC FACE_SUBSET_DART1_OF_FAN THEN\r
 570          ASM_SIMP_TAC[CONTRAVENING_IMP_IN_DART1_OF_FAN];\r
 571        ALL_TAC\r
 572      ] THEN\r
 573      REMOVE_ASSUM THEN REMOVE_ASSUM THEN\r
 574      REPEAT DISCH_TAC THEN\r
 575      REPEAT (CONV_TAC let_CONV) THEN\r
 576      ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN\r
 577      REWRITE_TAC[tauVEF] THEN\r
 578      MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE)) THEN\r
 579      ASM_REWRITE_TAC[] THEN\r
 580      STRIP_TAC THEN\r
 581      SUBGOAL_THEN `(w,w') IN dart1_of_fan (V,ESTD V) /\ w',v IN dart1_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
 582      [\r
 583        CONJ_TAC THEN MATCH_MP_TAC IN_FACE_IMP_IN_DART1_OF_FAN THEN EXISTS_TAC `v:real^3,w:real^3` THEN ASM_REWRITE_TAC[IN_INSERT];\r
 584        ALL_TAC\r
 585      ] THEN\r
 586 \r
 587      ASM_REWRITE_TAC[] THEN\r
 588      ASM_SIMP_TAC[Hypermap.FINITE_TWO_ELEMENTS; Hypermap.FINITE_SINGLETON; SUM_CLAUSES; SUM_SING] THEN\r
 589      SUBGOAL_THEN `~(v,w IN {(w,w'), (w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL\r
 590      [\r
 591        REWRITE_TAC[IN_INSERT; PAIR_EQ; NOT_IN_EMPTY; DE_MORGAN_THM] THEN\r
 592          MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN\r
 593          ASM_SIMP_TAC[];\r
 594        ALL_TAC\r
 595      ] THEN\r
 596      SUBGOAL_THEN `~(w,w' IN {(w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL\r
 597      [\r
 598        REWRITE_TAC[IN_SING; PAIR_EQ] THEN\r
 599          MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN\r
 600          ASM_SIMP_TAC[];\r
 601        ALL_TAC\r
 602      ] THEN\r
 603      REWRITE_TAC[sol0_over_pi_EQ_const1] THEN\r
 604      ABBREV_TAC `a1 = azim_dart (V,ESTD V) (v,w)` THEN\r
 605      ABBREV_TAC `a2 = azim_dart (V,ESTD V) (w,w')` THEN\r
 606      ABBREV_TAC `a3 = azim_dart (V,ESTD V) (w',v)` THEN\r
 607      ABBREV_TAC `l1 = lmfun (h_dart (v:real^3,w:real^3))` THEN\r
 608      ABBREV_TAC `l2 = lmfun (h_dart (w:real^3,w':real^3))` THEN\r
 609      ABBREV_TAC `l3 = lmfun (h_dart (w':real^3,v:real^3))` THEN\r
 610      SUBGOAL_THEN `(pi + sol0) = pi * (&1 + const1)` (fun th -> REWRITE_TAC[th]) THENL\r
 611      [\r
 612        MP_TAC sol0_over_pi_EQ_const1 THEN\r
 613          MP_TAC PI_POS THEN\r
 614          CONV_TAC REAL_FIELD;\r
 615        ALL_TAC\r
 616      ] THEN\r
 617      \r
 618      REWRITE_TAC[Sphere.taum; Sphere.sol_y; Sphere.lnazim] THEN\r
 619      SUBGOAL_THEN `v,w IN dart_of_fan (V,ESTD V) /\ w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
 620      [\r
 621        REPEAT CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN EXISTS_TAC `dart1_of_fan (V,ESTD V)` THEN ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];\r
 622        ALL_TAC\r
 623      ] THEN\r
 624 \r
 625      MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `v:real^3`; `w:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN\r
 626      MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w:real^3`; `w':real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN\r
 627      MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w':real^3`; `v:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN\r
 628      ASM_REWRITE_TAC[DIST_SYM] THEN\r
 629      REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[SYM th])) THEN\r
 630      \r
 631      MP_TAC (SPEC `v:real^3,w:real^3` ly_EQ_lmfun) THEN\r
 632      MP_TAC (SPEC `w:real^3,w':real^3` ly_EQ_lmfun) THEN\r
 633      MP_TAC (SPEC `w':real^3,v:real^3` ly_EQ_lmfun) THEN\r
 634 \r
 635      MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN\r
 636      MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN\r
 637      MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN\r
 638      \r
 639      ASM_REWRITE_TAC[] THEN\r
 640      SUBGOAL_THEN `w' IN V /\ w IN V /\ v IN (V:real^3->bool)` (fun th -> REWRITE_TAC[th]) THENL\r
 641      [\r
 642        MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 643          MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 644          MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w':real^3`; `v:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 645          ASM_SIMP_TAC[];\r
 646        ALL_TAC\r
 647      ] THEN\r
 648      SIMP_TAC[DIST_0; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN\r
 649      REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN\r
 650      REAL_ARITH_TAC);;\r
 651 \r
 652 \r
 653 let CONTRAVENING_TAUVEF_EQ_TAUM = prove(`!V v w. contravening V /\ \r
 654                                                (v,w) IN dart_of_fan (V,ESTD V) /\\r
 655                                                CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3\r
 656                                          ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in\r
 657                                              let y1 = norm v in\r
 658                                              let y2 = norm w in\r
 659                                              let y3 = norm w' in\r
 660                                              let y4 = dist(w,w') in\r
 661                                              let y5 = dist(v,w') in\r
 662                                              let y6 = dist(v,w) in\r
 663                                                tauVEF (V,ESTD V,face (hypermap_of_fan (V,ESTD V)) (v,w)) = taum y1 y2 y3 y4 y5 y6`,\r
 664    REPEAT STRIP_TAC THEN\r
 665      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 666      MP_TAC (SPECL [`V:real^3->bool`; `face (hypermap_of_fan (V,ESTD V)) (v,w)`] tauVEF_EQ_taum) THEN\r
 667      ANTS_TAC THENL\r
 668      [\r
 669        ASM_REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 670          REWRITE_TAC[IN_ELIM_THM] THEN\r
 671          EXISTS_TAC `v:real^3,w:real^3` THEN\r
 672          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN];\r
 673        ALL_TAC\r
 674      ] THEN\r
 675      DISCH_THEN MATCH_MP_TAC THEN\r
 676      REWRITE_TAC[Hypermap.face_refl]);;\r
 677 \r
 678 \r
 679 (* Bounds for distances in a triangular face *)\r
 680          \r
 681 let CONTRAVENING_TRIANGULAR_FACE_DIST = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V) /\\r
 682                                                 CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3\r
 683     ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in\r
 684         let y1 = norm v in\r
 685         let y2 = norm w in\r
 686         let y3 = norm w' in\r
 687         let y4 = dist(w,w') in\r
 688         let y5 = dist(v,w') in\r
 689         let y6 = dist(v,w) in\r
 690           (&2 <= y1 /\ y1 <= #2.52) /\\r
 691           (&2 <= y2 /\ y2 <= #2.52) /\\r
 692           (&2 <= y3 /\ y3 <= #2.52) /\\r
 693           (&2 <= y4 /\ y4 <= #2.52) /\\r
 694           (&2 <= y5 /\ y5 <= #2.52) /\\r
 695           (&2 <= y6 /\ y6 <= #2.52)`,\r
 696     REPEAT STRIP_TAC THEN CONV_TAC (DEPTH_CONV let_CONV) THEN\r
 697       MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 698       ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN\r
 699       MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE) THEN\r
 700       ASM_REWRITE_TAC[] THEN\r
 701       ANTS_TAC THENL\r
 702       [\r
 703         MATCH_MP_TAC CONTRAVENING_IMP_IN_DART1_OF_FAN THEN\r
 704           ASM_REWRITE_TAC[];\r
 705         ALL_TAC\r
 706       ] THEN\r
 707       CONV_TAC (DEPTH_CONV let_CONV) THEN\r
 708       DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN\r
 709       SUBGOAL_THEN `w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
 710       [\r
 711         CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN \r
 712           EXISTS_TAC `face (hypermap_of_fan (V,ESTD V)) (v,w)` THEN\r
 713           ASM_SIMP_TAC[FACE_SUBSET_DART_OF_FAN; IN_INSERT];\r
 714         ALL_TAC\r
 715       ] THEN\r
 716       SUBGOAL_THEN `v IN V /\ w IN V /\ w' IN (V:real^3->bool)` ASSUME_TAC THENL\r
 717       [\r
 718         MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 719           MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN\r
 720           ASM_SIMP_TAC[];\r
 721         ALL_TAC\r
 722       ] THEN\r
 723       REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN\r
 724       MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN\r
 725       MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN\r
 726       MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN\r
 727       ASM_REWRITE_TAC[DIST_0] THEN\r
 728       REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[th])) THEN\r
 729       MAP_EVERY (fun tm -> MP_TAC (SPECL [`V:real^3->bool`; tm] CONTRAVENING_DART_DIST)) [`v:real^3,w:real^3`; `w:real^3,w':real^3`; `w':real^3,v:real^3`] THEN\r
 730       ASM_SIMP_TAC[DIST_SYM]);;\r
 731          \r
 732 \r
 733 (* Bounds for azim_dart in a triangular face *)\r
 734 \r
 735 let azim_dart_bounds_3_list = map (fun id -> (hd (Ineq.getexact id)).ineq) ["5735387903"; "5490182221"];;\r
 736 \r
 737 let azim_dart_bounds_3 = list_mk_conj azim_dart_bounds_3_list;;\r
 738 \r
 739 let TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl = mk_imp (azim_dart_bounds_3,\r
 740                                                      `!V x. contravening V /\\r
 741                                                        x IN dart_of_fan (V,ESTD V) /\\r
 742                                                        CARD (face (hypermap_of_fan (V,ESTD V)) x) = 3\r
 743                                                          ==> #0.852 < azim_dart (V,ESTD V) x /\ azim_dart (V,ESTD V) x < #1.893`);;\r
 744 \r
 745 (* g(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl);; *)\r
 746 let TRIANGULAR_FACE_AZIM_DART_BOUNDS = prove(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl,\r
 747    REWRITE_TAC[Ineq.dart_std3; INEQ_ALT; ALL; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN\r
 748      STRIP_TAC THEN\r
 749 \r
 750      REPEAT GEN_TAC THEN STRIP_TAC THEN\r
 751      POP_ASSUM MP_TAC THEN\r
 752      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 753 \r
 754      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN\r
 755      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 756      MP_TAC (SPEC_ALL CONTRAVENING_AZIM_DART_EQ_DIH_Y) THEN\r
 757      ASM_REWRITE_TAC[] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN\r
 758      ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN\r
 759      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 760 \r
 761      MP_TAC (SPEC_ALL CONTRAVENING_TRIANGULAR_FACE_DIST) THEN\r
 762      ASM_REWRITE_TAC[] THEN\r
 763      CONV_TAC (DEPTH_CONV let_CONV) THEN\r
 764      REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN\r
 765      DISCH_TAC THEN\r
 766 \r
 767      CONJ_TAC THENL\r
 768      [\r
 769        REWRITE_TAC[GSYM real_gt] THEN\r
 770          FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 771          ASM_REWRITE_TAC[];\r
 772        FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 773          ASM_REWRITE_TAC[]\r
 774      ]);;\r
 775 \r
 776 \r
 777 \r
 778 (******************************************************************************)         \r
 779          \r
 780 (* Properties of rho_node (might be useful) *)\r
 781 (*       \r
 782 let RHO_NODE_lemma = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 783                              f IN face_set (hypermap_of_fan (V,E)) /\ x IN f\r
 784                            ==> ?!w. (FST x,w) IN f`,\r
 785    REPEAT STRIP_TAC THEN\r
 786      REWRITE_TAC[EXISTS_UNIQUE] THEN\r
 787      EXISTS_TAC `SND (x:real^3#real^3)` THEN\r
 788      ASM_REWRITE_TAC[PAIR] THEN\r
 789      REPEAT STRIP_TAC THEN\r
 790      MP_TAC (INST [`FST (x:real^3#real^3),y:real^3`, `y:real^3#real^3`] (SPEC_ALL HYPERMAP_OF_FAN_FACE_NODE_INJ)) THEN\r
 791      ASM_REWRITE_TAC[] THEN\r
 792      ONCE_REWRITE_TAC[GSYM PAIR] THEN\r
 793      REWRITE_TAC[PAIR_EQ; EQ_SYM_EQ]);;\r
 794 \r
 795 \r
 796 \r
 797 \r
 798 let RHO_NODE_LEMMA = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 799                             f IN face_set (hypermap_of_fan (V,E)) /\ x IN f\r
 800                             ==> rho_node (V,E,f) (FST x) = SND x`,\r
 801    REPEAT GEN_TAC THEN\r
 802      DISCH_TAC THEN\r
 803      MP_TAC (SPEC_ALL RHO_NODE_lemma) THEN ASM_REWRITE_TAC[EXISTS_UNIQUE] THEN\r
 804      STRIP_TAC THEN\r
 805      SUBGOAL_THEN `w = SND (x:real^3#real^3)` ASSUME_TAC THENL\r
 806      [\r
 807        MATCH_MP_TAC EQ_SYM THEN\r
 808          POP_ASSUM (fun th -> MATCH_MP_TAC th) THEN\r
 809          ASM_REWRITE_TAC[PAIR];\r
 810        ALL_TAC\r
 811      ] THEN\r
 812      REWRITE_TAC[rho_node] THEN\r
 813      MATCH_MP_TAC SELECT_UNIQUE THEN\r
 814      GEN_TAC THEN BETA_TAC THEN\r
 815      EQ_TAC THENL\r
 816      [\r
 817        DISCH_TAC THEN\r
 818          FIRST_X_ASSUM (MP_TAC o SPEC `y:real^3`) THEN\r
 819          ASM_REWRITE_TAC[];\r
 820        DISCH_THEN (fun th -> ASM_REWRITE_TAC[th])\r
 821      ]);;\r
 822 \r
 823 \r
 824 \r
 825 \r
 826 let RHO_NODE_EQ_FACE_MAP = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 827                                    x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x\r
 828                                    ==> f_fan_pair_ext (V,E) x = (rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x))`,\r
 829    REPEAT STRIP_TAC THEN\r
 830      REWRITE_TAC[Hypermap.POWER_2; o_THM] THEN\r
 831      ABBREV_TAC `w = rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST (x:real^3#real^3))` THEN\r
 832      MATCH_MP_TAC HYPERMAP_OF_FAN_FACE_NODE_INJ THEN\r
 833      MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`; `f:real^3#real^3->bool`] THEN\r
 834      ASM_REWRITE_TAC[] THEN\r
 835 \r
 836      SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL\r
 837      [\r
 838        ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 839          REWRITE_TAC[IN_ELIM_THM] THEN\r
 840          EXISTS_TAC `x:real^3#real^3` THEN\r
 841          REWRITE_TAC[] THEN\r
 842          MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 843          EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN\r
 844          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 845          REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];\r
 846        ALL_TAC\r
 847      ] THEN\r
 848      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 849 \r
 850      SUBGOAL_THEN `f_fan_pair_ext (V,E) x IN f` MP_TAC THENL\r
 851      [\r
 852        ASM_REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN\r
 853          ASM_SIMP_TAC[HYPERMAP_OF_FAN; Hypermap.in_orbit_map1];\r
 854        ALL_TAC\r
 855      ] THEN\r
 856      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 857 \r
 858      CONJ_TAC THENL\r
 859      [\r
 860        REWRITE_TAC[rho_node] THEN\r
 861          MATCH_MP_TAC (BETA_RULE (ISPECL [`(\w':real^3. (w:real^3,w') IN face (hypermap_of_fan (V,E)) x)`] SELECT_AX)) THEN\r
 862          POP_ASSUM MP_TAC THEN\r
 863          MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN\r
 864          ASM_REWRITE_TAC[Hypermap.face_refl] THEN\r
 865          MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN\r
 866          STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair] THEN\r
 867          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 868          DISCH_TAC THEN\r
 869          EXISTS_TAC `inverse_sigma_fan (vec 0) V E y x'` THEN\r
 870          ASM_REWRITE_TAC[];\r
 871        ALL_TAC\r
 872      ] THEN\r
 873 \r
 874      MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN\r
 875      ASM_REWRITE_TAC[Hypermap.face_refl] THEN\r
 876      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 877      MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN\r
 878      STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair]);;\r
 879    \r
 880 \r
 881 \r
 882 let RHO_NODE_POWER_EQ_FACE_MAP_POWER = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 883                                                x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x\r
 884                                                ==> !i. (f_fan_pair_ext (V,E) POWER i) x = \r
 885                                                    ((\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) POWER i) x`,\r
 886    REPEAT STRIP_TAC THEN\r
 887      ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN\r
 888      SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL\r
 889      [\r
 890        ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
 891          REWRITE_TAC[IN_ELIM_THM] THEN\r
 892          EXISTS_TAC `x:real^3#real^3` THEN\r
 893          REWRITE_TAC[] THEN\r
 894          MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 895          EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN\r
 896          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 897          REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];\r
 898        ALL_TAC\r
 899      ] THEN\r
 900      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 901      \r
 902      SPEC_TAC (`i:num`,`i:num`) THEN\r
 903      INDUCT_TAC THENL\r
 904      [\r
 905        REWRITE_TAC[Hypermap.POWER];\r
 906        ALL_TAC\r
 907      ] THEN\r
 908      \r
 909      REWRITE_TAC[ARITH_RULE `SUC i = 1 + i`; Hypermap.addition_exponents; Hypermap.POWER_1; o_THM] THEN\r
 910      ABBREV_TAC `y = (f_fan_pair_ext (V,E) POWER i) x` THEN\r
 911      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `y:real^3#real^3`; `f:real^3#real^3->bool`] RHO_NODE_EQ_FACE_MAP) THEN\r
 912      FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (rator (concl th)) = `y:real^3#real^3`)) THEN\r
 913      ASM_REWRITE_TAC[] THEN\r
 914      \r
 915      SUBGOAL_THEN `y IN face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL\r
 916      [\r
 917        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 918          ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN\r
 919          REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN\r
 920          EXISTS_TAC `i:num` THEN\r
 921          REWRITE_TAC[GE; LE_0];\r
 922        ALL_TAC\r
 923      ] THEN\r
 924 \r
 925      SUBGOAL_THEN `face (hypermap_of_fan (V,E)) x = face (hypermap_of_fan (V,E)) y` ASSUME_TAC THENL\r
 926      [\r
 927        MATCH_MP_TAC Hypermap.lemma_face_identity THEN\r
 928          ASM_REWRITE_TAC[];\r
 929        ALL_TAC\r
 930      ] THEN\r
 931 \r
 932      SUBGOAL_THEN `y IN dart1_of_fan (V:real^3->bool,E)` (fun th -> REWRITE_TAC[th]) THENL\r
 933      [\r
 934        MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 935          EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN\r
 936          ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];\r
 937        ALL_TAC\r
 938      ] THEN\r
 939 \r
 940      ASM_REWRITE_TAC[] THEN\r
 941      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN\r
 942      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 943      EXPAND_TAC "g" THEN BETA_TAC THEN\r
 944      ASM_REWRITE_TAC[]);;\r
 945      \r
 946 \r
 947 \r
 948 \r
 949 \r
 950 let ORBIT_MAP_FUN_EQ_lemma = prove(`!(f:A->A) g x. (!y. y IN orbit_map f x ==> g y = f y) \r
 951                                    ==> orbit_map g x = orbit_map f x`,\r
 952    REPEAT STRIP_TAC THEN\r
 953      MATCH_MP_TAC Hypermap.lemma_orbit_eq THEN\r
 954      INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER] THEN\r
 955      REWRITE_TAC[GSYM Hypermap.POWER] THEN\r
 956      ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN\r
 957      FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 958      REWRITE_TAC[Hypermap.lemma_in_orbit]);;\r
 959      \r
 960 \r
 961 \r
 962 \r
 963 let RHO_NODE_face = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 964                             x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x\r
 965                             ==> f = orbit_map (\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) x`,\r
 966    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 967      SUBGOAL_THEN `orbit_map (f_fan_pair_ext (V,E)) x = face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL\r
 968      [\r
 969        ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN];\r
 970        ALL_TAC\r
 971      ] THEN\r
 972      FIRST_ASSUM (fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN\r
 973      MATCH_MP_TAC EQ_SYM THEN\r
 974      MATCH_MP_TAC ORBIT_MAP_FUN_EQ_lemma THEN\r
 975      ASM_REWRITE_TAC[] THEN\r
 976      REPEAT STRIP_TAC THEN\r
 977      MATCH_MP_TAC EQ_SYM THEN BETA_TAC THEN\r
 978      MATCH_MP_TAC RHO_NODE_EQ_FACE_MAP THEN\r
 979      ASM_REWRITE_TAC[] THEN\r
 980      CONJ_TAC THENL\r
 981      [\r
 982        MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
 983          EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN\r
 984          ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];\r
 985        ALL_TAC\r
 986      ] THEN\r
 987      MATCH_MP_TAC Hypermap.lemma_face_identity THEN\r
 988      ASM_REWRITE_TAC[]);;\r
 989 \r
 990 \r
 991 \r
 992 let RHO_NODE_POWER = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
 993                             x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x\r
 994                             ==> !i. ((\x. rho_node (V,E,f) (FST x),(rho_node (V,E,f) POWER 2) (FST x)) POWER i) x\r
 995                                  = (\x. (rho_node (V,E,f) POWER i) (FST x), (rho_node (V,E,f) POWER (i + 1)) (FST x)) x`,\r
 996    REPEAT STRIP_TAC THEN\r
 997      SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL\r
 998      [\r
 999        ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN\r
1000          REWRITE_TAC[IN_ELIM_THM] THEN\r
1001          EXISTS_TAC `x:real^3#real^3` THEN\r
1002          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
1003          MATCH_MP_TAC Hypermap.lemma_in_subset THEN\r
1004          EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN\r
1005          ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];\r
1006        ALL_TAC\r
1007      ] THEN     \r
1008      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
1009 \r
1010      SPEC_TAC (`i:num`, `i:num`) THEN\r
1011      INDUCT_TAC THEN BETA_TAC THENL\r
1012      [\r
1013        REWRITE_TAC[Hypermap.POWER; ARITH_RULE `0 + 1 = 1`; Hypermap.POWER_1; I_THM] THEN\r
1014          MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN\r
1015          ASM_REWRITE_TAC[Hypermap.face_refl] THEN\r
1016          DISCH_THEN (fun th -> REWRITE_TAC[th]);\r
1017        ALL_TAC\r
1018      ] THEN\r
1019 \r
1020      ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM; PAIR_EQ] THEN\r
1021      REWRITE_TAC[ARITH_RULE `SUC i + 1 = 2 + i`] THEN\r
1022      REWRITE_TAC[Hypermap.addition_exponents; o_THM]);;\r
1023 \r
1024 *)\r
1025 \r
1026 (* Alternative definition of the perimeter of a face *)\r
1027 (*\r
1028 let PERIMETER_lemma = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\\r
1029                               x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x\r
1030                               ==> per (V,E,f) (FST x) (CARD f) = sum f (\(v,w). arcV (vec 0) v w)`,\r
1031    REPEAT STRIP_TAC THEN\r
1032      REWRITE_TAC[per] THEN\r
1033      ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN\r
1034      ABBREV_TAC `orbit = orbit_map (f_fan_pair_ext (V,E)) x` THEN\r
1035 \r
1036      SUBGOAL_THEN `0 < CARD (orbit:real^3#real^3->bool)` ASSUME_TAC THENL\r
1037      [\r
1038        SUBGOAL_THEN `FINITE (orbit:real^3#real^3->bool)` ASSUME_TAC THENL\r
1039          [\r
1040            EXPAND_TAC "orbit" THEN\r
1041              MATCH_MP_TAC Hypermap.lemma_orbit_finite THEN\r
1042              EXISTS_TAC `dart_of_fan (V,E)` THEN\r
1043              ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN];\r
1044            ALL_TAC\r
1045          ] THEN\r
1046          DISJ_CASES_TAC (ARITH_RULE `0 < CARD (orbit:real^3#real^3->bool) \/ CARD orbit = 0`) THEN ASM_REWRITE_TAC[] THEN\r
1047          POP_ASSUM MP_TAC THEN\r
1048          POP_ASSUM (MP_TAC o (MATCH_MP CARD_EQ_0)) THEN\r
1049          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
1050          DISCH_TAC THEN\r
1051          MP_TAC (ISPECL [`f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.orbit_reflect) THEN\r
1052          ASM_REWRITE_TAC[NOT_IN_EMPTY];\r
1053        ALL_TAC\r
1054      ] THEN\r
1055 \r
1056      SUBGOAL_THEN `!i. arcV (vec 0:real^3) ((rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) POWER i) (FST (x:real^3#real^3))) ((rho_node (V,E,f) POWER (i + 1)) (FST x)) = ((\(v,w). arcV (vec 0) v w) o (\i. (g POWER i) x)) i` MP_TAC THENL\r
1057      [\r
1058        REWRITE_TAC[LAMBDA_PAIR; o_THM] THEN BETA_TAC THEN\r
1059          MP_TAC (SPEC_ALL RHO_NODE_POWER) THEN\r
1060          ASM_REWRITE_TAC[] THEN\r
1061          DISCH_THEN (fun th -> REWRITE_TAC[th]);\r
1062        ALL_TAC\r
1063      ] THEN\r
1064 \r
1065      ASM_REWRITE_TAC[] THEN\r
1066      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
1067      \r
1068      SUBGOAL_THEN `f:real^3#real^3->bool = IMAGE (\i. (g:real^3#real^3->real^3#real^3 POWER i) x) (0..CARD f - 1)` MP_TAC THENL\r
1069      [\r
1070        ASM_REWRITE_TAC[GSYM IMAGE_LEMMA; IN_NUMSEG; LE_0] THEN\r
1071          ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN\r
1072          MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`; `CARD (orbit_map (f_fan_pair_ext (V,E)) x)`] FINITE_ORBIT_MAP) THEN\r
1073          ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN\r
1074          DISCH_THEN (fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN\r
1075          MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN\r
1076          ASM_REWRITE_TAC[] THEN\r
1077          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
1078          POP_ASSUM MP_TAC THEN\r
1079          SIMP_TAC[ARITH_RULE `0 < c ==> !i. i < c <=> i <= c - 1`];\r
1080        ALL_TAC\r
1081      ] THEN\r
1082      ASM_REWRITE_TAC[] THEN\r
1083      DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN\r
1084      REWRITE_TAC[ETA_AX] THEN\r
1085 \r
1086      MATCH_MP_TAC (GSYM SUM_IMAGE) THEN\r
1087 \r
1088      X_GEN_TAC `n:num` THEN X_GEN_TAC `m:num` THEN\r
1089      REWRITE_TAC[IN_NUMSEG; LE_0] THEN\r
1090      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN\r
1091      MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN\r
1092      ASM_REWRITE_TAC[] THEN\r
1093      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN\r
1094      \r
1095      STRIP_TAC THEN\r
1096      SUBGOAL_THEN `inj_orbit (f_fan_pair_ext (V,E)) x (CARD (f:real^3#real^3->bool) - 1)` MP_TAC THENL\r
1097      [\r
1098        MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.lemma_segment_orbit) THEN\r
1099          ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN\r
1100          DISCH_THEN (MP_TAC o SPEC `CARD (f:real^3#real^3->bool) - 1`) THEN\r
1101          ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN\r
1102          ANTS_TAC THENL\r
1103          [\r
1104            REPLICATE_TAC 3 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN\r
1105              ARITH_TAC;\r
1106            SIMP_TAC[]\r
1107          ];\r
1108        ALL_TAC\r
1109      ] THEN\r
1110 \r
1111      REWRITE_TAC[Hypermap.lemma_inj_orbit] THEN\r
1112      DISCH_THEN MATCH_MP_TAC THEN\r
1113      ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN]);;\r
1114 *)\r
1115 \r
1116 \r
1117 end;;\r