text_formalization/local/LVDUCXU.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Local Fan                                                   *)\r
   5 (* Author: Nguyen Quang Truong                                          *)\r
   6 (* Date: 2010-05-09                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 (* needs "/home/user1/flyspeck/working/flyspeck_needs.hl";; *)\r
  10 (* =========== snapshot 1631 ===================== *)\r
  11 \r
  12 flyspeck_needs "fan/planarity.hl";;\r
  13 flyspeck_needs "local/WRGCVDR_CIZMRRH.hl";; \r
  14 \r
  15 \r
  16 module type Lvducxu_type = sig\r
  17 \r
  18 end;;\r
  19 \r
  20 \r
  21 module Lvducxu = struct\r
  22 \r
  23 parse_as_infix("has_orders",(12,"right"));;\r
  24 \r
  25 \r
  26 \r
  27 open Sphere;;\r
  28 open Trigonometry1;;\r
  29 open Trigonometry2;;\r
  30 open Hypermap;;\r
  31 open Fan;;\r
  32 open Planarity;;\r
  33 open Prove_by_refinement;;\r
  34 open Wrgcvdr_cizmrrh;;\r
  35 \r
  36 let PROPERTIES_OF_IVS_AZIM_CYCLE2 = IVS_AZIM_PROPERTIES;;\r
  37 \r
  38 \r
  39 \r
  40 let IN_FF_IMP_FST_SND_IN_V = prove_by_refinement\r
  41 (` UNIONS E SUBSET (V:A -> bool) /\ FF SUBSET darts_of_hyp E V\r
  42 /\ x IN FF ==> FST x IN V /\ SND x IN V `,\r
  43 [REWRITE_TAC[darts_of_hyp; SUBSET];\r
  44 STRIP_TAC;\r
  45 DOWN;\r
  46 FIRST_ASSUM NHANH;\r
  47 REWRITE_TAC[ord_pairs; IN_UNION; self_pairs; IN_ELIM_THM];\r
  48 STRIP_TAC;\r
  49 ASM_REWRITE_TAC[];\r
  50 SUBGOAL_THEN` (a:A) IN UNIONS E /\ b IN UNIONS E ` ASSUME_TAC;\r
  51 REWRITE_TAC[IN_UNIONS];\r
  52 ASM_MESON_TAC[SET_RULE` a IN {a,b} /\ b IN {a,b} `];\r
  53 ASM_MESON_TAC[];\r
  54 ASM_SIMP_TAC[]]);;\r
  55 \r
  56 \r
  57 \r
  58 \r
  59 \r
  60 \r
  61 \r
  62 \r
  63 \r
  64 \r
  65 let W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE = \r
  66 prove_by_refinement(\r
  67 `(!(x:A). x IN W ==> W = orbit_map f x)\r
  68 ==> W = IMAGE f W `,\r
  69 [STRIP_TAC;\r
  70 REWRITE_TAC[FUN_EQ_THM];\r
  71 GEN_TAC THEN EQ_TAC;\r
  72 PAT_ONCE_REWRITE_TAC `\x. x ==> x ` [GSYM IN];\r
  73 DOWN THEN PHA;\r
  74 NHANH CYCLIC_MAP_IMP_CIRCLE_ITSELF;\r
  75 REWRITE_TAC[IMAGE; IN_ELIM_THM];\r
  76 SIMP_TAC[];\r
  77 REWRITE_TAC[IMAGE; IN_ELIM_THM];\r
  78 FIRST_ASSUM NHANH;\r
  79 ASSUME_TAC in_orbit_map1;\r
  80 DOWN THEN REWRITE_TAC[IN];\r
  81 MESON_TAC[]]);;\r
  82 \r
  83 \r
  84 \r
  85 \r
  86 \r
  87 \r
  88 \r
  89 \r
  90 \r
  91 let FINITE_AND_LOOP_IMP_BIJ_S_IM_S = \r
  92 prove_by_refinement(\r
  93 `! S:A -> bool. FINITE S /\ (! x. x IN S ==> S = orbit_map f x )\r
  94 ==> BIJ f S (IMAGE f S ) `,\r
  95 [NHANH W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE;\r
  96 REWRITE_TAC[BIJ; INJ; SURJ];\r
  97 REPEAT GEN_TAC THEN STRIP_TAC;\r
  98 REWRITE_TAC[FUN_IN_IMAGE; IN_IMAGE];\r
  99 SIMP_TAC[CONJ_SYM; EQ_SYM_EQ];\r
 100 ASM_MESON_TAC[IMAGE_IMP_INJECTIVE_GEN]]);;\r
 101 \r
 102 \r
 103 \r
 104 \r
 105 let CYCLIC_SET_IMP_SELF_LOPP2 = prove_by_refinement\r
 106 (`FAN (x,V,E) /\ {v, u} IN E\r
 107      ==> (!a. a IN EE v E\r
 108               ==> EE v E = orbit_map (azim_cycle (EE v E) x v) a)`,\r
 109 [NHANH CYCLIC_SET_IMP_STABLE_SET2;\r
 110 STRIP_TAC;\r
 111 FIRST_X_ASSUM NHANH;\r
 112 REPEAT STRIP_TAC;\r
 113 ABBREV_TAC ` f = azim_cycle (EE v E) x v `;\r
 114 ASM_REWRITE_TAC[orbit_map; FUN_EQ_THM; IN_ELIM_THM; POWER_TO_ITER];\r
 115 REWRITE_TAC[ARITH_RULE` x >= 0 `]]);;\r
 116 \r
 117 \r
 118 let FIN_LOOP_IMP_BIJ_ITSELF = prove_by_refinement(\r
 119 `! S: A -> bool. FINITE S /\ (! x. x IN S ==> S = orbit_map f x )\r
 120 ==> BIJ f S S `,\r
 121 [NHANH FINITE_AND_LOOP_IMP_BIJ_S_IM_S;\r
 122 NHANH W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE;\r
 123 MESON_TAC[]]);;\r
 124 \r
 125 \r
 126 \r
 127 \r
 128 \r
 129 (* +++++++++++++++++++++++++++\r
 130 let CYCLIC_SET_IMP_BIJ_AZIM_CYCLE =\r
 131 prove_by_refinement(` cyclic_set W v w ==>\r
 132 BIJ (azim_cycle W v w) W W `,\r
 133 [NHANH CYCLIC_SET_IMP_SELF_LOPP;\r
 134 REWRITE_TAC[cyclic_set];\r
 135 STRIP_TAC;\r
 136 DOWN;\r
 137 UNDISCH_TAC `FINITE (W:real^3 -> bool) `;\r
 138 PHA;\r
 139 NHANH FIN_LOOP_IMP_BIJ_ITSELF;\r
 140 SIMP_TAC[]]);;\r
 141 \r
 142 +++++++++++++++++++++++++++++++ *)\r
 143 \r
 144 (* a very important lemma for proving \r
 145     second lemma in local fan chapter *)\r
 146 (* ================================== *)\r
 147 \r
 148 \r
 149 \r
 150 \r
 151 let IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME = prove_by_refinement\r
 152 (` (x:A#A) IN darts_of_hyp E V /\ x IN FF ==>\r
 153 x IN darts_of_hyp (e_prime E FF) (v_prime V FF) `,\r
 154 [REWRITE_TAC[IN_ELIM_THM; darts_of_hyp; IN_UNION; ord_pairs; self_pairs];\r
 155 REWRITE_TAC[e_prime; v_prime; IN_ELIM_THM];\r
 156 STRIP_TAC;\r
 157 DISJ1_TAC;\r
 158 ASM_MESON_TAC[];\r
 159 DISJ2_TAC;\r
 160 EXISTS_TAC `v:A`;\r
 161 ASM_REWRITE_TAC[];\r
 162 CONJ_TAC;\r
 163 ASM_MESON_TAC[];\r
 164 DOWN_TAC THEN REWRITE_TAC[EE];\r
 165 SET_TAC[]]);;\r
 166 \r
 167 \r
 168 \r
 169 \r
 170 \r
 171 let PROPERTIES_OF_IVS_AZIM_CYCLE2 =\r
 172 prove_by_refinement(` FAN (x,V,E) /\ w IN EE v E ==>\r
 173 ivs_azim_cycle (EE v E) x v w IN EE v E /\\r
 174 azim_cycle  (EE v E ) x v ( ivs_azim_cycle  (EE v E) x v w ) = w `,\r
 175 [IMP_TAC;\r
 176 NHANH FAN_IMP_EE_EQ_SET_OF_EDGE;\r
 177 STRIP_TAC;\r
 178 UNDISCH_TAC` FAN ((x:real^3),V,E) `;\r
 179 PHA;\r
 180 ASM_REWRITE_TAC[];\r
 181 NHANH IVS_AZIM_PROPERTIES;\r
 182 SIMP_TAC[];\r
 183 STRIP_TAC;\r
 184 UNDISCH_TAC `ivs_azim_cycle (set_of_edge v V E) x v w IN \r
 185 set_of_edge v V E `;\r
 186 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
 187 PHA;\r
 188 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
 189 ASM_SIMP_TAC[]]);;\r
 190 \r
 191 \r
 192 \r
 193 let IN_EE_IFF_IN_E = prove(` x IN EE v E <=> {v,x} IN E `,\r
 194 REWRITE_TAC[EE; IN_ELIM_THM]);;\r
 195 \r
 196 \r
 197 let CYCLIC_SET_IMP_SELF_LOPP3 = prove(`FAN (x,V,E) \r
 198        ==> (!a. a IN EE v E\r
 199                 ==> EE v E = orbit_map (azim_cycle (EE v E) x v) a)`,\r
 200 MESON_TAC[CYCLIC_SET_IMP_SELF_LOPP2;IN_EE_IFF_IN_E]);;\r
 201 \r
 202 \r
 203 \r
 204 let BIJ_AZIM_CYCLE_EE = prove(\r
 205 ` FAN (x,V,E) ==> BIJ (azim_cycle (EE v E) x v) (EE v E) (EE v E) `,\r
 206 NHANH CYCLIC_SET_IMP_SELF_LOPP3 THEN \r
 207 NHANH FAN_IMP_FINITE_EE THEN \r
 208 MESON_TAC[FIN_LOOP_IMP_BIJ_ITSELF]);;\r
 209 \r
 210 \r
 211 \r
 212 \r
 213 \r
 214 \r
 215 \r
 216 (* ++++++++++++++++++ *)\r
 217 \r
 218 \r
 219 \r
 220 let IN_FF_FACE_MAP_IDE = prove_by_refinement\r
 221 (` FAN (v,V,E) /\\r
 222      (?x. x IN dart (hypermap (HYP (v,V,E))) /\\r
 223           FF = face (hypermap (HYP (v,V,E))) x)\r
 224 ==> (! x. x IN FF ==> face_map (hypermap (HYP (v,V,E))) x =\r
 225 face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x ) `,\r
 226 [NHANH IMP_FAN_V_PRIME_E_PRIME;\r
 227 NHANH ELMS_OF_HYPERMAP_HYP;\r
 228 STRIP_TAC;\r
 229 STRIP_TAC THEN STRIP_TAC;\r
 230 UNDISCH_TAC`FF = face (hypermap (HYP (v,V,E))) x`;\r
 231 DISCH_THEN (ASSUME_TAC o SYM);\r
 232 ASM_REWRITE_TAC[ff_of_hyp];\r
 233 PAT_ONCE_REWRITE_TAC `\x. P x = Q x ` [GSYM PAIR];\r
 234 \r
 235 \r
 236 SUBGOAL_THEN `x IN dart (hypermap (HYP ((v:real^3),V,E))) ` MP_TAC;\r
 237 ASM_REWRITE_TAC[];\r
 238 NHANH lemma_face_subset;\r
 239 ASM_REWRITE_TAC[];\r
 240 STRIP_TAC;\r
 241 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;\r
 242 DOWN THEN DOWN THEN DOWN THEN SET_TAC[];\r
 243 SUBGOAL_THEN ` x':real^3 # real^3 IN \r
 244 darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;\r
 245 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;\r
 246 DOWN THEN DOWN THEN DOWN THEN SET_TAC[];\r
 247 ASM_SIMP_TAC[IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME];\r
 248 PHA;\r
 249 SIMP_TAC[ff_of_hyp2];\r
 250 REMOVE_TAC THEN DOWN THEN REMOVE_TAC;\r
 251 \r
 252 \r
 253 \r
 254 REWRITE_TAC[ff_of_hyp];\r
 255 UNDISCH_TAC `(x': real^3 #real^3 ) IN FF `;\r
 256 EXPAND_TAC "FF";\r
 257 REWRITE_TAC[face];\r
 258 NHANH IN_ORBIT_MAP_IMP_F_Y;\r
 259 REWRITE_TAC[GSYM face];\r
 260 \r
 261 \r
 262 ASM_REWRITE_TAC[];\r
 263 IMP_TAC THEN DISCH_TAC;\r
 264 \r
 265 \r
 266 SUBGOAL_THEN `x IN dart (hypermap (HYP ((v:real^3),V,E))) ` MP_TAC;\r
 267 ASM_REWRITE_TAC[];\r
 268 NHANH lemma_face_subset;\r
 269 ASM_REWRITE_TAC[];\r
 270 STRIP_TAC;\r
 271 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;\r
 272 DOWN THEN DOWN THEN SET_TAC[];\r
 273 SIMP_TAC[ff_of_hyp2];\r
 274 REMOVE_TAC;\r
 275 DOWN THEN REMOVE_TAC;\r
 276 DOWN THEN PHA;\r
 277 \r
 278 \r
 279 IMP_TAC THEN DISCH_TAC;\r
 280 PAT_ONCE_REWRITE_TAC `\x. P h x IN FF ==> y `\r
 281 [ISPEC `x': real^3 # real^3 ` (GSYM PAIR)];\r
 282 \r
 283 \r
 284 ABBREV_TAC ` fx = FST (x':real^3 # real^3 ) `;\r
 285 ABBREV_TAC `snx = SND (x':real^3 # real^3 ) `;\r
 286 MP_TAC (ISPEC `x': real^3 # real^3 ` (GSYM PAIR));\r
 287 DISCH_TAC;\r
 288 \r
 289 \r
 290 UNDISCH_TAC `x IN dart (hypermap (HYP (v,V,E))) `;\r
 291 NHANH lemma_face_subset;\r
 292 STRIP_TAC;\r
 293 UNDISCH_TAC` (x':real^3#real^3) IN FF `;\r
 294 DOWN;\r
 295 PHA;\r
 296 ASM_REWRITE_TAC[];\r
 297 NHANH (SET_RULE` a SUBSET b /\ x IN a /\ l ==> x IN b `);\r
 298 STRIP_TAC;\r
 299 DOWN;\r
 300 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
 301 ONCE_REWRITE_TAC[DISJ_SYM];\r
 302 STRIP_TAC;\r
 303 (* 2 goals araise here *)\r
 304 (* sub 1 *)\r
 305 DOWN;\r
 306 REWRITE_TAC[self_pairs];\r
 307 UNDISCH_TAC `(x':real^3 # real^3) = FST x',SND x'`;\r
 308 DISCH_TAC;\r
 309 FIRST_X_ASSUM (fun x -> ONCE_REWRITE_TAC[x]);\r
 310 PURE_REWRITE_TAC[IN_ELIM_THM; BETA_THM; PAIR_EQ];\r
 311 ASM_REWRITE_TAC[];\r
 312 STRIP_TAC;\r
 313 ASM_REWRITE_TAC[];\r
 314 ASSUME_TAC (let tm = \r
 315 MATCH_MP (SPECL [`{}:real^3 -> bool `;` v:real^3 `;` v':real^3 `] (GEN_ALL (MESON[W_SUBSET_SINGLETON_IMP_IDE]` W SUBSET {p} ==> azim_cycle W v w p = p`)))  (SET_RULE` {} SUBSET {(q:real^3)} `) in\r
 316 GEN `q:real^3 ` tm);\r
 317 \r
 318 \r
 319 ASSUME_TAC2 (\r
 320 ISPECL [`FF:real^3 # real^3 -> bool `] (GEN_ALL E_PRIME_SUBSET_E));\r
 321 DOWN;\r
 322 NHANH (\r
 323 let ge = \r
 324 GEN_ALL SUBSET_IMP_SO_DO_EE in\r
 325 ISPECL [`W1:(A -> bool ) -> bool`;`v':A `] ge);\r
 326 ASM_SIMP_TAC[SUBSET_EMPTY];\r
 327 (* SUB 2 *)\r
 328 REWRITE_TAC[PAIR_EQ];\r
 329 DOWN_TAC THEN NHANH (\r
 330 MESON[FAN]` FAN (x,V,E) ==> UNIONS E SUBSET V `);\r
 331 STRIP_TAC;\r
 332 ASSUME_TAC2 (\r
 333 ISPEC `x': real^3 # real ^3 ` (GEN `x:A#A` IN_FF_IMP_FST_SND_IN_V));\r
 334 DOWN THEN ASM_SIMP_TAC[];\r
 335 STRIP_TAC;\r
 336 SUBGOAL_THEN` snx:real^3 IN v_prime V (FF:real^3 # real^3 -> bool)` ASSUME_TAC;\r
 337 REWRITE_TAC[v_prime; IN_ELIM_THM];\r
 338 ASM_SIMP_TAC[];\r
 339 EXISTS_TAC `ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;\r
 340 FIRST_ASSUM ACCEPT_TAC;\r
 341 DOWN;\r
 342 ASSUME_TAC2 (\r
 343 SPECL [`v:real^3 `;`V:real^3 -> bool`;` E:(real^3 -> bool) -> bool`;` snx:real^3`] XOHLED);\r
 344 UNDISCH_TAC`FAN ((v:real^3),v_prime V FF,e_prime E FF)`;\r
 345 PHA;\r
 346 NHANH XOHLED;\r
 347 DOWN;\r
 348 ASM_SIMP_TAC[GSYM UNI_E_IMP_EE_EQ_SET_OF_EDGE];\r
 349 SUBGOAL_THEN `{FST (x':real^3 # real^3), SND x'} IN e_prime E FF ` ASSUME_TAC;\r
 350 ASM_REWRITE_TAC[e_prime; IN_ELIM_THM];\r
 351 EXISTS_TAC`(fx:real^3 )`;\r
 352 EXISTS_TAC `snx:real^3 `;\r
 353 REPLICATE_TAC 5 DOWN;\r
 354 PHA;\r
 355 REWRITE_TAC[ord_pairs; IN_ELIM_THM];\r
 356 STRIP_TAC;\r
 357 EXPAND_TAC "fx";\r
 358 EXPAND_TAC "snx";\r
 359 REPLICATE_TAC 6 DOWN;\r
 360 SIMP_TAC[];\r
 361 MESON_TAC[];\r
 362 SUBGOAL_THEN ` fx:real^3 IN EE snx E /\ fx IN EE snx (e_prime E FF) ` ASSUME_TAC;\r
 363 REWRITE_TAC[EE; IN_ELIM_THM];\r
 364 REPLICATE_TAC 4 DOWN THEN PHA;\r
 365 ASM_SIMP_TAC[INSERT_COMM; ord_pairs; IN_ELIM_THM];\r
 366 IMP_TAC THEN STRIP_TAC;\r
 367 DOWN THEN DOWN;\r
 368 EXPAND_TAC "fx";\r
 369 EXPAND_TAC "snx";\r
 370 SIMP_TAC[];\r
 371 DOWN;\r
 372 REPEAT STRIP_TAC;\r
 373 UNDISCH_TAC ` fx:real^3 IN EE snx E `;\r
 374 UNDISCH_TAC ` cyclic_set (EE snx E) (v:real^3) snx`;\r
 375 PHA;\r
 376 IMP_TAC THEN STRIP_TAC;\r
 377 SUBGOAL_THEN ` FAN (v:real^3,V,E)` MP_TAC;\r
 378 ASM_REWRITE_TAC[];\r
 379 PHA;\r
 380 NHANH PROPERTIES_OF_IVS_AZIM_CYCLE2;\r
 381 PHA THEN IMP_TAC THEN REMOVE_TAC;\r
 382 STRIP_TAC;\r
 383 \r
 384 UNDISCH_TAC `(fx:real^3) IN EE snx (e_prime E FF)`;\r
 385 UNDISCH_TAC `cyclic_set (EE snx (e_prime E FF)) (v:real^3) snx`;\r
 386 PHA;\r
 387 \r
 388 \r
 389 \r
 390 IMP_TAC THEN STRIP_TAC;\r
 391 SUBGOAL_THEN ` FAN (v:real^3,v_prime V FF, e_prime E FF)` MP_TAC;\r
 392 ASM_REWRITE_TAC[];\r
 393 PHA;\r
 394 NHANH PROPERTIES_OF_IVS_AZIM_CYCLE2;\r
 395 PHA THEN IMP_TAC THEN REMOVE_TAC;\r
 396 STRIP_TAC;\r
 397 ASSUME_TAC2 (\r
 398 ISPECL [`FF:real^3 # real^3 -> bool`;`snx:real^3 `] (GEN_ALL (MATCH_MP SUBSET_IMP_SO_DO_EE E_PRIME_SUBSET_E)));\r
 399 \r
 400 SUBGOAL_THEN `ivs_azim_cycle (EE snx E) v snx fx IN EE snx (e_prime E FF) ` ASSUME_TAC;\r
 401 PAT_REWRITE_TAC`\x. y IN x ` [EE];\r
 402 REWRITE_TAC[IN_ELIM_THM; e_prime];\r
 403 UNDISCH_TAC` ivs_azim_cycle (EE snx E) (v:real^3) snx fx IN EE snx E`;\r
 404 ABBREV_TAC `t = ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;\r
 405 REWRITE_TAC[EE; IN_ELIM_THM];\r
 406 STRIP_TAC;\r
 407 EXISTS_TAC `snx:real^3 `;\r
 408 EXISTS_TAC `t:real^3 `;\r
 409 ASM_REWRITE_TAC[];\r
 410 (* new subgoal *)\r
 411 \r
 412 ABBREV_TAC `t = ivs_azim_cycle (EE snx E) v snx (fx:real^3)`;\r
 413 ABBREV_TAC `tt = ivs_azim_cycle (EE snx (e_prime E FF)) v snx (fx:real^3)`;\r
 414 ABBREV_TAC `smalset = EE snx (e_prime (E:(real^3 -> bool) -> bool) FF)`;\r
 415 ABBREV_TAC `lset = EE (snx:real^3) E `;\r
 416 ASM_CASES_TAC ` lset SUBSET {t:real^3} `;\r
 417 DOWN;\r
 418 UNDISCH_TAC` smalset SUBSET (lset:real^3 -> bool) `;\r
 419 PHA;\r
 420 NHANH SUBSET_TRANS;\r
 421 UNDISCH_TAC `(tt:real^3) IN smalset `;\r
 422 SET_TAC[];\r
 423 DOWN;\r
 424 ASM_CASES_TAC `t = (tt:real^3) `;\r
 425 STRIP_TAC THEN FIRST_ASSUM ACCEPT_TAC;\r
 426 ASSUME_TAC2 (\r
 427 SET_RULE` ~(t = tt) /\ t IN smalset /\ (tt:real^3) IN smalset ==>\r
 428 ~( smalset SUBSET {tt}) `);\r
 429 USE_FIRST ` cyclic_set lset (v:real^3) snx` MP_TAC;\r
 430 USE_FIRST ` cyclic_set smalset (v:real^3) snx` MP_TAC;\r
 431 REWRITE_TAC[cyclic_set];\r
 432 REPEAT STRIP_TAC;\r
 433 UNDISCH_TAC `FINITE (lset:real^3 -> bool) `;\r
 434 DOWN THEN PHA;\r
 435 NHANH (\r
 436 SPECL [`lset:real^3 -> bool `;` t:real^3`;` snx:real^3 `;` v:real^3 ` ] (GEN_ALL AZIM_CYCLE_PROPERTIES));\r
 437 ASSUME_TAC2 (SPECL [`smalset:real^3 -> bool `;` tt:real^3`;` snx:real^3 `;` v:real^3 ` ] (GEN_ALL AZIM_CYCLE_PROPERTIES));\r
 438 DOWN;\r
 439 ASM_REWRITE_TAC[];\r
 440 STRIP_TAC;\r
 441 STRIP_TAC;\r
 442 MP_TAC (\r
 443 SPECL [`smalset:real^3 -> bool`;`v:real^3 `;`snx:real^3`;`t:real^3 `;` fx:real^3 `] (GEN_ALL IDENTIFY_AZIM_CYCLE));\r
 444 SUBGOAL_THEN ` ~(smalset SUBSET {t:real^3}) /\\r
 445   ~collinear {(t:real^3), v, snx} /\\r
 446   cyclic_set smalset v snx /\\r
 447   (~(fx = t) /\ smalset fx) /\\r
 448   (!q. ~(q = t) /\ smalset q\r
 449        ==> azim v snx t fx < azim v snx t q \/\r
 450            azim v snx t fx = azim v snx t q /\\r
 451            norm (projection (snx - v) (fx - v)) <=\r
 452            norm (projection (snx - v) (q - v)))` ASSUME_TAC;\r
 453 ASM_REWRITE_TAC[];\r
 454 CONJ_TAC;\r
 455 UNDISCH_TAC `~( t = (tt:real^3)) `;\r
 456 UNDISCH_TAC ` (tt:real^3) IN smalset`;\r
 457 SET_TAC[];\r
 458 CONJ_TAC;\r
 459 UNDISCH_TAC` cyclic_set lset (v:real^3) snx `;\r
 460 NHANH CYCLIC_SET_IMP_NOT_COLLINEAR;\r
 461 STRIP_TAC;\r
 462 UNDISCH_TAC ` (t:real^3) IN lset `;\r
 463 FIRST_X_ASSUM NHANH;\r
 464 SIMP_TAC[];\r
 465 UNDISCH_TAC ` smalset SUBSET (lset:real^3 -> bool) `;\r
 466 REWRITE_TAC[SUBSET];\r
 467 DOWN;\r
 468 MESON_TAC[IN];\r
 469 ANTS_TAC;\r
 470 FIRST_X_ASSUM ACCEPT_TAC;\r
 471 UNDISCH_TAC ` cyclic_set smalset (v:real^3) snx `;\r
 472 STRIP_TAC;\r
 473 SUBGOAL_THEN ` (FAN (v:real^3,v_prime V FF,e_prime E FF)) ` MP_TAC;\r
 474 FIRST_ASSUM ACCEPT_TAC;\r
 475 NHANH (SPEC `snx:real^3 ` (GEN `v:real^3 ` BIJ_AZIM_CYCLE_EE));\r
 476 IMP_TAC THEN REMOVE_TAC;\r
 477 \r
 478 \r
 479 \r
 480 REWRITE_TAC[BIJ; INJ];\r
 481 STRIP_TAC;\r
 482 STRIP_TAC;\r
 483 FIRST_X_ASSUM (MP_TAC o (SPECL [`t:real^3 `;` tt:real^3 `]));\r
 484 REWRITE_TAC[TAUT` ~( a ==> b) <=> a /\ ~ b `];\r
 485 ASM_REWRITE_TAC[]]);;\r
 486 \r
 487 \r
 488 \r
 489 let LOCALIZE_PRESERVE_FACE = prove_by_refinement\r
 490 (` FAN (v,V,E) /\\r
 491    x IN dart (hypermap (HYP (v,V,E))) /\\r
 492    FF = face  (hypermap (HYP (v,V,E))) x \r
 493 ==> FF = face  (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x`,\r
 494 [STRIP_TAC;\r
 495 MP_TAC IN_FF_FACE_MAP_IDE;\r
 496 ANTS_TAC;\r
 497 ASM_SIMP_TAC[];\r
 498 EXISTS_TAC`x: real^3 # real^3 `;\r
 499 ASM_REWRITE_TAC[];\r
 500 DOWN;\r
 501 NHANH (MESON[face_refl]` D = face H x ==> x IN D `);\r
 502 DISCH_TAC THEN DISCH_TAC;\r
 503 ABBREV_TAC ` hy2 = hypermap (HYP (v,v_prime V FF,e_prime E FF)) `;\r
 504 ASM_REWRITE_TAC[face; orbit_map];\r
 505 MATCH_MP_TAC (\r
 506 SET_RULE`(! n. Q n x = P n x ) ==> { Q n x | n >= 0 } = { P n x | n >= 0 } `);\r
 507 ASSUME_TAC (\r
 508 ISPECL [`face_map ((hypermap (HYP (v,V,E))) )` ] lemma_in_orbit);\r
 509 DOWN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
 510 SIMP_TAC[GSYM face];\r
 511 STRIP_TAC;\r
 512 DOWN;\r
 513 ASM_REWRITE_TAC[];\r
 514 STRIP_TAC;\r
 515 INDUCT_TAC;\r
 516 REWRITE_TAC[POWER];\r
 517 DOWN;\r
 518 FIRST_X_ASSUM (MP_TAC o (SPEC_ALL));\r
 519 ASM_REWRITE_TAC[];\r
 520 DISCH_TAC;\r
 521 DISCH_TAC;\r
 522 REWRITE_TAC[GSYM COM_POWER_FUNCTION];\r
 523 DOWN THEN DOWN;\r
 524 FIRST_ASSUM NHANH;\r
 525 ASM_REWRITE_TAC[];\r
 526 MESON_TAC[]]);;\r
 527 \r
 528 \r
 529 \r
 530 \r
 531 \r
 532 \r
 533 let FAN_IN_SEFL_PAIRS_IMP_PROGORIOUS_DEGENERATE = \r
 534 prove_by_refinement(` FAN (x,V,E) /\ v IN self_pairs E V \r
 535 ==> edge_map (hypermap (HYP(x,V,E))) v = v /\\r
 536 face_map (hypermap (HYP(x,V,E))) v = v /\\r
 537 node_map (hypermap (HYP(x,V,E))) v = v `,\r
 538 [NHANH ELMS_OF_HYPERMAP_HYP;\r
 539 SIMP_TAC[];\r
 540 STRIP_TAC;\r
 541 DOWN;\r
 542 SIMP_TAC[nn_of_hyp3; ff_of_hyp3];\r
 543 SIMP_TAC[ee_of_hyp2;darts_of_hyp; IN_UNION];\r
 544 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
 545 STRIP_TAC;\r
 546 ASM_SIMP_TAC[]]);;\r
 547 \r
 548 \r
 549 \r
 550 let FAN_FACE_IMP_IVS_F_IN_F =\r
 551 prove_by_refinement (` FAN (x,V,E) /\\r
 552 xx IN dart (hypermap (HYP (x,V,E))) /\\r
 553     FF = face (hypermap (HYP (x,V,E))) xx /\ y IN FF\r
 554 ==> inverse ( face_map (hypermap (HYP (x,V,E))) ) y IN FF /\\r
 555 ( face_map (hypermap (HYP (x,V,E))) ) o (inverse ( face_map (hypermap (HYP (x,V,E))) )) = I /\\r
 556 (inverse ( face_map (hypermap (HYP (x,V,E))) )) o ( face_map (hypermap (HYP (x,V,E))) ) = I `,\r
 557 [NHANH HYP_LEMMA;\r
 558 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
 559 STRIP_TAC;\r
 560 REPLICATE_TAC 3 DOWN THEN PHA;\r
 561 REWRITE_TAC[GSYM HYP];\r
 562 ASSUME_TAC2 ELMS_OF_HYPERMAP_HYP;\r
 563 NHANH lemma_face_subset;\r
 564 ASM_SIMP_TAC[SUBSET];\r
 565 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
 566 STRIP_TAC;\r
 567 DOWN;\r
 568 ASM_REWRITE_TAC[face];\r
 569 UNDISCH_TAC ` ff_of_hyp (x,V,E) permutes darts_of_hyp E V `;\r
 570 UNDISCH_TAC ` FINITE (darts_of_hyp E (V:real^3 -> bool))`;\r
 571 EXPAND_TAC "FF";\r
 572 PHA;\r
 573 DISCH_TAC THEN CONJ_TAC;\r
 574 DOWN;\r
 575 REWRITE_TAC[face];\r
 576 ASM_REWRITE_TAC[];\r
 577 MESON_TAC[lemma_orbit_identity; lemma_inverse_in_orbit];\r
 578 DOWN;\r
 579 NHANH PERMUTES_INVERSES_o;\r
 580 SIMP_TAC[]]);;\r
 581 \r
 582 \r
 583 let FAN_FACE_IMP_IVS_F_IN_F =\r
 584 prove_by_refinement \r
 585 (` FAN (x,V,E) /\\r
 586      FF = face (hypermap (HYP (x,V,E))) xx /\\r
 587      y IN FF\r
 588      ==> inverse (face_map (hypermap (HYP (x,V,E)))) y IN FF /\\r
 589          face_map (hypermap (HYP (x,V,E))) o\r
 590          inverse (face_map (hypermap (HYP (x,V,E)))) =\r
 591          I /\\r
 592          inverse (face_map (hypermap (HYP (x,V,E)))) o\r
 593          face_map (hypermap (HYP (x,V,E))) =\r
 594          I`,\r
 595 [STRIP_TAC;\r
 596 ASM_CASES_TAC` xx IN dart (hypermap (HYP ((x:real^3),V,E)))`;\r
 597 ASSUME_TAC2 FAN_FACE_IMP_IVS_F_IN_F;\r
 598 FIRST_X_ASSUM ACCEPT_TAC;\r
 599 DOWN_TAC THEN NHANH HYP_LEMMA;\r
 600 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
 601 NHANH ELMS_OF_HYPERMAP_HYP;\r
 602 STRIP_TAC;\r
 603 REWRITE_TAC[GSYM HYP];\r
 604 CONJ_TAC;\r
 605 REPLICATE_TAC 4 DOWN THEN PHA;\r
 606 REWRITE_TAC[GSYM HYP];\r
 607 NHANH lemma_face_exception;\r
 608 SIMP_TAC[];\r
 609 STRIP_TAC;\r
 610 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
 611 ASM_REWRITE_TAC[SET_RULE` x IN {c} <=> x = c `];\r
 612 SIMP_TAC[];\r
 613 USE_FIRST ` ff_of_hyp (x,V,E) permutes darts_of_hyp E V` MP_TAC;\r
 614 REWRITE_TAC[permutes];\r
 615 DOWN THEN DOWN THEN DOWN THEN ASM_REWRITE_TAC[];\r
 616 REWRITE_TAC[GSYM HYP];\r
 617 REPEAT STRIP_TAC;\r
 618 UNDISCH_TAC `~((xx:real^3 # real^3 ) IN darts_of_hyp E V) `;\r
 619 FIRST_X_ASSUM NHANH;\r
 620 STRIP_TAC;\r
 621 PAT_ONCE_REWRITE_TAC `\x. y = x ` [GSYM I_THM];\r
 622 UNDISCH_TAC `ff_of_hyp (x,V,E) permutes darts_of_hyp E V `;\r
 623 NHANH PERMUTES_INVERSES_o;\r
 624 STRIP_TAC;\r
 625 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
 626 REWRITE_TAC[o_THM];\r
 627 ASM_REWRITE_TAC[];\r
 628 UNDISCH_TAC `ff_of_hyp (x,V,E) permutes darts_of_hyp E V`;\r
 629 NHANH PERMUTES_INVERSES_o;\r
 630 ASM_MESON_TAC[]]);;\r
 631 \r
 632 \r
 633 \r
 634 \r
 635 let INVERSE_FACE_EQ_INV_FACE_LOCALLIZED =\r
 636 prove_by_refinement\r
 637 (`FAN (v,V,E) /\\r
 638    x IN dart (hypermap (HYP (v,V,E))) /\\r
 639    FF = face (hypermap (HYP (v,V,E))) x\r
 640 ==> (!x. x IN FF\r
 641               ==> inverse ( face_map (hypermap (HYP (v,V,E))) ) x =\r
 642                   inverse ( face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF)))) x)`,\r
 643 [STRIP_TAC;\r
 644 GEN_TAC;\r
 645 DOWN_TAC;\r
 646 NHANH FAN_FACE_IMP_IVS_F_IN_F;\r
 647 STRIP_TAC;\r
 648 MP_TAC (\r
 649 SPECL [` x:real^3 # real^3 `;` x':real^3 # real^3`;` FF:real^3#real^3->bool `;` v:real^3 `;` v_prime (V:real^3 -> bool) (FF:real^3 # real^3 -> bool) ` ;` e_prime E (FF:real^3 # real^3 -> bool)`] (GEN_ALL FAN_FACE_IMP_IVS_F_IN_F));\r
 650 ANTS_TAC;\r
 651 CONJ_TAC;\r
 652 MP_TAC IMP_FAN_V_PRIME_E_PRIME;\r
 653 ANTS_TAC;\r
 654 ASM_REWRITE_TAC[];\r
 655 EXISTS_TAC `x: real^3 # real^3 `;\r
 656 ASM_REWRITE_TAC[];\r
 657 REWRITE_TAC[];\r
 658 ASSUME_TAC2 LOCALIZE_PRESERVE_FACE;\r
 659 ASM_REWRITE_TAC[];\r
 660 REWRITE_TAC[GSYM HYP];\r
 661 UNDISCH_TAC `FF = face (hypermap (HYP (v,V,E))) x `;\r
 662 DOWN;\r
 663 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
 664 SIMP_TAC[];\r
 665 STRIP_TAC;\r
 666 DOWN;\r
 667 REMOVE_TAC;\r
 668 DOWN;\r
 669 REWRITE_TAC[FUN_EQ_THM];\r
 670 DISCH_THEN (MP_TAC o (SPEC `x': real^3 # real^3` ));\r
 671 ASSUME_TAC2 (SPECL [`x:real^3 # real^3 `;`x':real^3 # real^3 `;` FF: real^3 # real^3 -> bool`  ;` v:real^3 `] (GEN_ALL FAN_FACE_IMP_IVS_F_IN_F));\r
 672 REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC));\r
 673 DOWN THEN REMOVE_TAC;\r
 674 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
 675 REWRITE_TAC[o_THM];\r
 676 MP_TAC IN_FF_FACE_MAP_IDE;\r
 677 ANTS_TAC;\r
 678 ASM_REWRITE_TAC[];\r
 679 EXISTS_TAC `x:real^3# real^3 `;\r
 680 ASM_REWRITE_TAC[];\r
 681 DISCH_TAC;\r
 682 UNDISCH_TAC ` inverse (face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF)))) x' IN FF `;\r
 683 FIRST_X_ASSUM NHANH;\r
 684 STRIP_TAC;\r
 685 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
 686 UNDISCH_TAC ` FAN ((v:real^3),V,E) `;\r
 687 NHANH HYP_LEMMA;\r
 688 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
 689 STRIP_TAC;\r
 690 REWRITE_TAC[GSYM HYP];\r
 691 DOWN_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP;\r
 692 STRIP_TAC;\r
 693 DOWN;\r
 694 UNDISCH_TAC `ff_of_hyp (v,V,E) permutes darts_of_hyp E V `;\r
 695 ASM_REWRITE_TAC[permutes];\r
 696 MESON_TAC[]]);;\r
 697 \r
 698 \r
 699 \r
 700 \r
 701 \r
 702 \r
 703 \r
 704 let ED_MA_O_NO_MA_EQ_INV_FA =\r
 705 prove_by_refinement \r
 706 (`!(H:(A) hypermap ). edge_map H o node_map H = inverse ( face_map H ) `,\r
 707 [GEN_TAC;\r
 708 MP_TAC (SPEC_ALL hypermap_lemma);\r
 709 NHANH (MESON[]` x o y o z = b ==> (x o y o z ) o ( inverse z ) = b o  ( inverse z ) `);\r
 710 REWRITE_TAC[GSYM o_ASSOC; I_O_ID];\r
 711 NHANH PERMUTES_INVERSES_o;\r
 712 STRIP_TAC;\r
 713 DOWN;\r
 714 ASM_REWRITE_TAC[I_O_ID]]);;\r
 715 \r
 716 \r
 717 \r
 718 \r
 719 \r
 720 \r
 721 \r
 722 let IN_FF_IMP_AZIM_CYCLE_EQ = \r
 723 prove_by_refinement (\r
 724 ` FAN (v,V,E) /\\r
 725      x IN dart (hypermap (HYP (v,V,E))) /\\r
 726      FF = face (hypermap (HYP (v,V,E))) x\r
 727      ==> (!x. x IN FF ==>\r
 728 azim_cycle (EE (FST x ) E ) v (FST x ) (SND x ), FST x =\r
 729  azim_cycle (EE (FST x ) (e_prime E FF ) ) v (FST x ) (SND x ), FST x)`,\r
 730 [NHANH (\r
 731 prove(`FAN (v,V,E) /\\r
 732      x IN dart (hypermap (HYP (v,V,E))) /\\r
 733      FF = face (hypermap (HYP (v,V,E))) x\r
 734      ==> (!x. x IN FF ==>\r
 735 (edge_map (hypermap (HYP (v,V,E))) o node_map (hypermap (HYP (v,V,E))) ) x =\r
 736 (edge_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) o node_map ( hypermap (HYP (v,v_prime V FF,e_prime E FF))) ) x ) `,\r
 737 REWRITE_TAC[ED_MA_O_NO_MA_EQ_INV_FA;\r
 738 INVERSE_FACE_EQ_INV_FACE_LOCALLIZED]));\r
 739 STRIP_TAC;\r
 740 GEN_TAC THEN FIRST_X_ASSUM NHANH;\r
 741 MP_TAC IMP_FAN_V_PRIME_E_PRIME;\r
 742 ANTS_TAC;\r
 743 ASM_MESON_TAC[];\r
 744 DOWN_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP;\r
 745 STRIP_TAC;\r
 746 DOWN;\r
 747 ASM_REWRITE_TAC[];\r
 748 USE_FIRST ` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);\r
 749 REWRITE_TAC[o_THM];\r
 750 PAT_ONCE_REWRITE_TAC `\x. h ( d x ) = h ( i x ) ==> y ` [GSYM PAIR];\r
 751 SUBGOAL_THEN` (x':real^3 # real^3) IN darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;\r
 752 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
 753 ASM_SIMP_TAC[];\r
 754 UNDISCH_TAC ` x IN dart (hypermap (HYP (v,V,E))) `;\r
 755 NHANH lemma_face_subset;\r
 756 DOWN THEN DOWN THEN PHA THEN SET_TAC[];\r
 757 SUBGOAL_THEN ` x' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;\r
 758 UNDISCH_TAC ` x IN dart (hypermap (HYP (v,V,E))) `;\r
 759 NHANH lemma_face_subset;\r
 760 ASM_REWRITE_TAC[];\r
 761 DOWN THEN DOWN THEN MESON_TAC[SUBSET];\r
 762 FIRST_X_ASSUM (ASSUME_TAC o SYM);\r
 763 ASM_REWRITE_TAC[];\r
 764 ASSUME_TAC2 (\r
 765 MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]` FAN (v:real^3,V,E) ==> (! y. \r
 766 y IN darts_of_hyp E V ==> nn_of_hyp (v,V,E) y IN darts_of_hyp E V )`);\r
 767 FIRST_ASSUM NHANH;\r
 768 ASSUME_TAC2 (\r
 769 SPECL [`v_prime (V:real^3 -> bool) (FF:real^3 # real^3 -> bool) `;\r
 770 ` e_prime (E:(real^3 -> bool) -> bool) FF`] \r
 771 (MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]`! V E. FAN (v:real^3,V,E) ==> (! y. \r
 772 y IN darts_of_hyp E V ==> nn_of_hyp (v,V,E) y IN darts_of_hyp E V )`));\r
 773 FIRST_ASSUM NHANH;\r
 774 SIMP_TAC[ee_of_hyp2];\r
 775 SIMP_TAC[nn_of_hyp2]]);;\r
 776 \r
 777 \r
 778 \r
 779 \r
 780 \r
 781 let IN_DARTS_IMP_NN_OF_HYP_TOO =\r
 782  MESON[IN_DARTS_IFF_NN_OF_HYP_TOO]`! x V E. FAN (x,V,E) ==> \r
 783 (! y. y IN darts_of_hyp E V\r
 784 ==> nn_of_hyp (x,V,E) y IN darts_of_hyp E V )`;;\r
 785 \r
 786 \r
 787 \r
 788 \r
 789 \r
 790 \r
 791 \r
 792 \r
 793 let CARD_E_GT1_EQ_CARD_E_PRIME = prove_by_refinement\r
 794 (` FAN (x,V,E) /\ v IN dart (hypermap (HYP (x,V,E)) ) /\\r
 795  FF = face (hypermap (HYP (x,V,E))) v /\ y IN FF\r
 796 ==> ( CARD (EE (FST y) E) > 1 <=> CARD (EE (FST y) (e_prime E FF)) > 1 ) `,\r
 797 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c <=> b /\ a /\ c `];\r
 798 NHANH FAN_FACE_IMP_IVS_F_IN_F;\r
 799 ONCE_REWRITE_TAC[TAUT` a /\ ( b /\ c /\ d ) /\ p <=> (b /\ a /\ c ) /\ d /\ p`];\r
 800 NHANH INVERSE_FACE_EQ_INV_FACE_LOCALLIZED;\r
 801 REWRITE_TAC[GSYM ED_MA_O_NO_MA_EQ_INV_FA];\r
 802 IMP_TAC;\r
 803 STRIP_TAC;\r
 804 FIRST_X_ASSUM (NHANH_PAT`\x. x /\ y ==> k `);\r
 805 STRIP_TAC;\r
 806 MP_TAC (SPEC `x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));\r
 807 ANTS_TAC;\r
 808 ASM_MESON_TAC[];\r
 809 UNDISCH_TAC ` FAN ((x:real^3),V,E)`;\r
 810 NHANH ELMS_OF_HYPERMAP_HYP;\r
 811 PHA THEN STRIP_TAC;\r
 812 UNDISCH_TAC ` (edge_map (hypermap (HYP (x,V,E))) o node_map (hypermap (HYP (x,V,E))))\r
 813       y =\r
 814       (edge_map (hypermap (HYP (x,v_prime V FF,e_prime E FF))) o\r
 815        node_map (hypermap (HYP (x,v_prime V FF,e_prime E FF))))\r
 816       y `;\r
 817 UNDISCH_TAC `(edge_map (hypermap (HYP (x,V,E))) o node_map (hypermap (HYP (x,V,E))))\r
 818       y IN\r
 819       FF `;\r
 820 ASM_REWRITE_TAC[];\r
 821 UNDISCH_TAC ` FF = face (hypermap (HYP (x,V,E))) v `;\r
 822 DISCH_THEN (ASSUME_TAC o SYM);\r
 823 ASM_REWRITE_TAC[];\r
 824 PAT_ONCE_REWRITE_TAC `\x. P x IN FF ==> Q x = Y x ==> l ` [GSYM PAIR];\r
 825 \r
 826 \r
 827 PURE_REWRITE_TAC[o_THM];\r
 828 SUBGOAL_THEN ` v IN dart (hypermap (HYP (x,V,E))) ` MP_TAC;\r
 829 ASM_REWRITE_TAC[];\r
 830 NHANH lemma_face_subset;\r
 831 IMP_TAC THEN REMOVE_TAC;\r
 832 SUBGOAL_THEN ` (y:real^3 # real^3) IN FF ` MP_TAC;\r
 833 FIRST_ASSUM ACCEPT_TAC;\r
 834 DISCH_TAC;\r
 835 ASM_REWRITE_TAC[];\r
 836 DOWN;\r
 837 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];\r
 838 NHANH (SET_RULE` a SUBSET b /\ x IN a ==> x IN b `);\r
 839 IMP_TAC THEN IMP_TAC;\r
 840 REMOVE_TAC;\r
 841 DISCH_TAC;\r
 842 ASM_REWRITE_TAC[];\r
 843 DOWN;\r
 844 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];\r
 845 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
 846 ASSUME_TAC2 IN_DARTS_IMP_NN_OF_HYP_TOO;\r
 847 FIRST_X_ASSUM NHANH;\r
 848 ASSUME_TAC2 (\r
 849 SPECL [`x:real^3 `;` v_prime V (FF:real^3 # real^3 -> bool)`;\r
 850 ` e_prime (E:(real^3 -> bool) -> bool) FF `] IN_DARTS_IMP_NN_OF_HYP_TOO);\r
 851 FIRST_X_ASSUM NHANH;\r
 852 SIMP_TAC[ee_of_hyp2];\r
 853 SIMP_TAC[nn_of_hyp2];\r
 854 REMOVE_TAC;\r
 855 \r
 856 UNDISCH_TAC ` v IN dart (hypermap (HYP (x,V,E))) `;\r
 857 NHANH lemma_face_subset;\r
 858 ASM_REWRITE_TAC[SUBSET];\r
 859 STRIP_TAC;\r
 860 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF`;\r
 861 FIRST_ASSUM (NHANH_PAT` \x. x ==> y `);\r
 862 REWRITE_TAC[darts_of_hyp; IN_UNION; ord_pairs; self_pairs];\r
 863 STRIP_TAC;\r
 864 DOWN;\r
 865 REWRITE_TAC[IN_ELIM_THM];\r
 866 STRIP_TAC;\r
 867 FIRST_X_ASSUM SUBST_ALL_TAC;\r
 868 REWRITE_TAC[];\r
 869 SUBGOAL_THEN ` FINITE (EE (a:real^3) E ) ` ASSUME_TAC;\r
 870 ASM_MESON_TAC[FAN_IMP_FINITE_EE];\r
 871 STRIP_TAC;\r
 872 STRIP_TAC;\r
 873 EQ_TAC;\r
 874 DISCH_TAC;\r
 875 SUBGOAL_THEN` ~( EE (a:real^3) E SUBSET {b} ) ` ASSUME_TAC;\r
 876 REWRITE_TAC[SET_RULE` a SUBSET {b} <=> a = {} \/ a = {b} `];\r
 877 DOWN;\r
 878 MESON_TAC[ARITH_RULE` ~( 0 > 1 \/ 1 > 1 )`; CARD_CLAUSES; CARD_SINGLETON];\r
 879 UNDISCH_TAC ` FINITE (EE (a:real^3) E ) `;\r
 880 DOWN THEN PHA;\r
 881 \r
 882 \r
 883 \r
 884 NHANH (SPECL [`x:real^3 `; `a:real^3 `] (GENL [`v:real^3`;` w:real^3 `] AZIM_CYCLE_PROPERTIES));\r
 885 STRIP_TAC;\r
 886 SUBGOAL_THEN ` b IN EE (a:real^3) (e_prime E FF) /\\r
 887 azim_cycle (EE a E) x a b IN EE (a:real^3) (e_prime E FF) ` ASSUME_TAC;\r
 888 UNDISCH_TAC ` {(a:real^3), b} IN E `;\r
 889 UNDISCH_TAC ` (a:real^3),(b:real^3) IN FF `;\r
 890 UNDISCH_TAC `azim_cycle (EE a E) x a b,a IN FF `;\r
 891 UNDISCH_TAC `EE a E (azim_cycle (EE a E) x a b) `;\r
 892 PHA;\r
 893 REWRITE_TAC[EE; e_prime; IN_ELIM_THM];\r
 894 DISCH_TAC;\r
 895 CONJ_TAC;\r
 896 DOWN THEN MESON_TAC[];\r
 897 EXISTS_TAC `azim_cycle {(w:real^3) | {a, w} IN E} x a b`;\r
 898 EXISTS_TAC `a:real^3 `;\r
 899 ASM_SIMP_TAC[INSERT_COMM];\r
 900 UNDISCH_TAC ` FAN ((x:real^3),v_prime V FF,e_prime E FF) `;\r
 901 NHANH (SPEC ` a:real^3` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));\r
 902 DOWN;\r
 903 REWRITE_TAC[SET_RULE` a IN x /\ b IN x <=> {a,b} SUBSET x `];\r
 904 ONCE_REWRITE_TAC[TAUT` a ==> b /\ c ==> d <=> b /\ a /\ c ==> d `];\r
 905 NHANH CARD_SUBSET;\r
 906 UNDISCH_TAC ` ~(azim_cycle (EE a E) x a b = b) `;\r
 907 NHANH CARD_2_FAN;\r
 908 SIMP_TAC[INSERT_COMM];\r
 909 STRIP_TAC;\r
 910 STRIP_TAC THEN DOWN;\r
 911 ARITH_TAC;\r
 912 MP_TAC (\r
 913 ISPECL [`FF:real^3 # real^3 -> bool`;` E: (real^3 -> bool) -> bool`] (GEN_ALL E_PRIME_SUBSET_E));\r
 914 NHANH (\r
 915 ISPECL [`S: (A -> bool) -> bool`;` a:A`] (GEN_ALL SUBSET_IMP_SO_DO_EE));\r
 916 ASSUME_TAC2 (\r
 917 SPEC `a:real^3 ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));\r
 918 DOWN;\r
 919 ONCE_REWRITE_TAC[TAUT` a ==> b /\ c ==> d <=> b /\ c /\ a ==> d `];\r
 920 NHANH CARD_SUBSET;\r
 921 ARITH_TAC;\r
 922 DOWN;\r
 923 REWRITE_TAC[IN_ELIM_THM];\r
 924 STRIP_TAC;\r
 925 ASM_REWRITE_TAC[];\r
 926 REMOVE_TAC THEN REMOVE_TAC;\r
 927 MP_TAC (\r
 928 ISPECL [`FF:real^3 # real^3 -> bool`;` E: (real^3 -> bool) -> bool`] (GEN_ALL E_PRIME_SUBSET_E));\r
 929 NHANH (\r
 930 ISPECL [`S: (A -> bool) -> bool`;` v':A`] (GEN_ALL SUBSET_IMP_SO_DO_EE));\r
 931 ASM_SIMP_TAC[SUBSET_EMPTY]]);;\r
 932 \r
 933 \r
 934 \r
 935 \r
 936 \r
 937 (* OOOOOOOOOOOOOOOOOO *)\r
 938 (* working here *)\r
 939 \r
 940 \r
 941 \r
 942 \r
 943 \r
 944 \r
 945 \r
 946 \r
 947 let AZIM_IN_FAN_EQ_IZIM_E_PRIME = prove_by_refinement\r
 948 (` FAN (vec 0,V,E) /\ v IN dart (hypermap (HYP (vec 0,V,E)) ) /\\r
 949  FF = face (hypermap (HYP (vec 0,V,E))) v /\ y IN FF\r
 950 ==> azim_in_fan y E = azim_in_fan y ( e_prime E FF ) `,\r
 951 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a /\ b /\ c ) /\ d `];\r
 952 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;\r
 953 STRIP_TAC;\r
 954 ONCE_REWRITE_TAC[GSYM PAIR];\r
 955 REWRITE_TAC[azim_in_fan];\r
 956 LET_TAC;\r
 957 LET_TAC;\r
 958 ASSUME_TAC2 (\r
 959 SPEC` vec 0 : real^3 ` (GEN `x:real^3 ` CARD_E_GT1_EQ_CARD_E_PRIME));\r
 960 ASM_SIMP_TAC[];\r
 961 ASM_SIMP_TAC[];\r
 962 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF`;\r
 963 FIRST_X_ASSUM NHANH;\r
 964 ASM_CASES_TAC ` CARD (EE (FST (y:real^3 # real^3)) (E: (real^3->bool)->bool )) > 1 `;\r
 965 ASM_SIMP_TAC[PAIR_EQ];\r
 966 ASM_SIMP_TAC[];\r
 967 DOWN;\r
 968 ASM_SIMP_TAC[]]);;\r
 969 \r
 970 \r
 971 \r
 972 \r
 973 \r
 974 let AZIM_CY_FST_Y_IN_FF = \r
 975 prove_by_refinement(\r
 976 ` xx IN dart (hypermap (HYP (x,V,E))) /\\r
 977  FAN (x,V,E) /\ FF = face (hypermap (HYP (x,V,E))) xx /\ y IN FF\r
 978        ==> azim_cycle (EE (FST y) E) x (FST y) (SND y),FST y IN FF /\\r
 979 (inverse (face_map (hypermap (HYP (x,V,E))))) y = \r
 980 azim_cycle (EE (FST y) E) x (FST y) (SND y),FST y `,\r
 981 [NHANH FAN_FACE_IMP_IVS_F_IN_F;\r
 982 REWRITE_TAC[GSYM ED_MA_O_NO_MA_EQ_INV_FA; o_THM];\r
 983 NHANH ELMS_OF_HYPERMAP_HYP;\r
 984 IMP_TAC THEN IMP_TAC; STRIP_TAC ;\r
 985 SIMP_TAC[];\r
 986 STRIP_TAC;\r
 987 PAT_ONCE_REWRITE_TAC ` \x. f ( g x ) IN HH /\ hh ==> l ` [GSYM PAIR];\r
 988 SUBGOAL_THEN ` (y:real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;\r
 989 UNDISCH_TAC ` xx IN dart (hypermap (HYP (x,V,E))) `;\r
 990 NHANH lemma_face_subset;\r
 991 DOWN;\r
 992 PHA;\r
 993 ASM_REWRITE_TAC[];\r
 994 SET_TAC[];\r
 995 ASSUME_TAC2 IN_DARTS_IMP_NN_OF_HYP_TOO;\r
 996 FIRST_X_ASSUM NHANH;\r
 997 SIMP_TAC[ee_of_hyp2];\r
 998 SIMP_TAC[nn_of_hyp2]]);;\r
 999 \r
1000 \r
1001 \r
1002 \r
1003 \r
1004 \r
1005 \r
1006 let EE_FST_Y_EQ_SET_SET_SNDY = prove_by_refinement\r
1007 (` FAN (x,V,E) /\\r
1008      v IN dart (hypermap (HYP (x,V,E))) /\\r
1009      FF = face (hypermap (HYP (x,V,E))) v /\\r
1010      y IN FF\r
1011 ==> ( EE (FST y) E = {SND y} <=> EE (FST y) (e_prime E FF) = {SND y} ) `,\r
1012 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a/\b/\c) /\d `];\r
1013 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;\r
1014 PHA;\r
1015 ONCE_REWRITE_TAC[TAUT`a1/\a2/\a3/\a4/\a5 <=> a2 /\ a4 /\ a1/\a3/\a5 `];\r
1016 ONCE_REWRITE_TAC[TAUT` a /\ b /\ c <=> b /\ a /\ c `];\r
1017 NHANH AZIM_CY_FST_Y_IN_FF;\r
1018 STRIP_TAC;\r
1019 MP_TAC (\r
1020 SPEC ` x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));\r
1021 ANTS_TAC;\r
1022 ASM_MESON_TAC[];\r
1023 DOWN_TAC;\r
1024 NHANH (SPEC ` FST (y:real^3#real^3) ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));\r
1025 STRIP_TAC;\r
1026 EQ_TAC;\r
1027 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);\r
1028 NHANH (\r
1029 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==>  azim_cycle W v w p = p`) ));\r
1030 \r
1031 ASM_REWRITE_TAC[];\r
1032 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1033 FIRST_ASSUM NHANH;\r
1034 SIMP_TAC[PAIR_EQ];\r
1035 STRIP_TAC;\r
1036 STRIP_TAC;\r
1037 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) (e_prime E FF)) `;\r
1038 DOWN;\r
1039 PHA;\r
1040 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);\r
1041 UNDISCH_TAC ` EE (FST y) E = {SND (y:real^3 # real^3 )} `;\r
1042 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);\r
1043 IMP_TAC;\r
1044 STRIP_TAC;\r
1045 STRIP_TAC;\r
1046 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) (e_prime E FF)  ` ASSUME_TAC;\r
1047 DOWN;\r
1048 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1049 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];\r
1050 MESON_TAC[PAIR];\r
1051 DOWN THEN PHA;\r
1052 ASM_REWRITE_TAC[];\r
1053 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `];\r
1054 \r
1055 \r
1056 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);\r
1057 NHANH (\r
1058 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==>  azim_cycle W v w p = p`)));\r
1059 ASM_REWRITE_TAC[];\r
1060 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1061 FIRST_ASSUM NHANH;\r
1062 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1063 ASM_SIMP_TAC[PAIR_EQ];\r
1064 \r
1065 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1066 STRIP_TAC;\r
1067 STRIP_TAC;\r
1068 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) E) `;\r
1069 ASM_REWRITE_TAC[];\r
1070 DOWN;\r
1071 PHA;\r
1072 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);\r
1073 UNDISCH_TAC ` EE (FST y) (e_prime E (face (hypermap (HYP (x,V,E))) v)) = {SND (y:real^3 # real^3 )} `;\r
1074 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);\r
1075 IMP_TAC;\r
1076 STRIP_TAC;\r
1077 STRIP_TAC;\r
1078 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) E  ` ASSUME_TAC;\r
1079 DOWN;\r
1080 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];\r
1081 MESON_TAC[PAIR];\r
1082 DOWN THEN PHA;\r
1083 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `]]);;\r
1084 \r
1085 \r
1086 let W_SUBSET_SINGLETON_IMP_IDE =\r
1087 (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p}\r
1088  ==>  azim_cycle W v w p = p`);;\r
1089 \r
1090 \r
1091 let EE_FST_Y_EQ_SET_SET_SNDY = prove_by_refinement\r
1092 (` FAN (x,V,E) /\\r
1093      v IN dart (hypermap (HYP (x,V,E))) /\\r
1094      FF = face (hypermap (HYP (x,V,E))) v /\\r
1095      y IN FF\r
1096 ==> ( EE (FST y) E = {SND y} <=> EE (FST y) (e_prime E FF) = {SND y} ) `,\r
1097 [ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (a/\b/\c) /\d `];\r
1098 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;\r
1099 PHA;\r
1100 ONCE_REWRITE_TAC[TAUT`a1/\a2/\a3/\a4/\a5 <=> a4 /\ a2/\ a1/\a3/\a5 `];\r
1101 NHANH AZIM_CY_FST_Y_IN_FF;\r
1102 STRIP_TAC;\r
1103 MP_TAC (\r
1104 SPEC ` x:real^3 ` (GEN `v:real^3 ` IMP_FAN_V_PRIME_E_PRIME));\r
1105 ANTS_TAC;\r
1106 ASM_MESON_TAC[];\r
1107 DOWN_TAC;\r
1108 NHANH (SPEC ` FST (y:real^3#real^3) ` (GEN `v:real^3 ` FAN_IMP_FINITE_EE));\r
1109 STRIP_TAC;\r
1110 EQ_TAC;\r
1111 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);\r
1112 NHANH (\r
1113 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] (MESON[W_SUBSET_SINGLETON_IMP_IDE]`W SUBSET {p} ==>  azim_cycle W v w p = p`)));\r
1114 ASM_REWRITE_TAC[];\r
1115 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1116 FIRST_ASSUM NHANH;\r
1117 SIMP_TAC[PAIR_EQ];\r
1118 STRIP_TAC;\r
1119 STRIP_TAC;\r
1120 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) (e_prime E FF)) `;\r
1121 DOWN;\r
1122 PHA;\r
1123 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);\r
1124 UNDISCH_TAC ` EE (FST y) E = {SND (y:real^3 # real^3 )} `;\r
1125 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);\r
1126 IMP_TAC;\r
1127 STRIP_TAC;\r
1128 STRIP_TAC;\r
1129 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) (e_prime E FF)  ` ASSUME_TAC;\r
1130 DOWN;\r
1131 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1132 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];\r
1133 MESON_TAC[PAIR];\r
1134 DOWN THEN PHA;\r
1135 ASM_REWRITE_TAC[];\r
1136 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `];\r
1137 \r
1138 \r
1139 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = b ==> a SUBSET b `);\r
1140 NHANH (\r
1141 SPECL [` x:real^3 `;` FST (y:real^3 # real^3)`] (GENL [` v:real^3 `;` w:real^3 `] W_SUBSET_SINGLETON_IMP_IDE));\r
1142 ASM_REWRITE_TAC[];\r
1143 UNDISCH_TAC ` (y:real^3 # real^3 ) IN FF `;\r
1144 FIRST_ASSUM NHANH;\r
1145 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1146 ASM_SIMP_TAC[PAIR_EQ];\r
1147 \r
1148 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1149 STRIP_TAC;\r
1150 STRIP_TAC;\r
1151 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) E) `;\r
1152 ASM_REWRITE_TAC[];\r
1153 DOWN;\r
1154 PHA;\r
1155 NHANH (MESON[AZIM_CYCLE_PROPERTIES]` azim_cycle W v w p = p /\ FINITE W ==> W SUBSET {p}`);\r
1156 UNDISCH_TAC ` EE (FST y) (e_prime E (face (hypermap (HYP (x,V,E))) v)) = {SND (y:real^3 # real^3 )} `;\r
1157 NHANH_PAT `\x. x ==> y ` (SET_RULE` a = {b} ==> b IN a `);\r
1158 IMP_TAC;\r
1159 STRIP_TAC;\r
1160 STRIP_TAC;\r
1161 SUBGOAL_THEN ` SND (y:real^3 # real^3 ) IN EE (FST y) E  ` ASSUME_TAC;\r
1162 DOWN;\r
1163 REWRITE_TAC[e_prime; EE; IN_ELIM_THM];\r
1164 MESON_TAC[PAIR];\r
1165 DOWN THEN PHA;\r
1166 MESON_TAC[SET_RULE` a IN b /\ b SUBSET {a} ==> b = {a} `]]);;\r
1167 \r
1168 \r
1169 \r
1170 \r
1171 let WEDGE_IN_FAN_EQ_WITH_E_PRIME =\r
1172 prove_by_refinement (` FAN (vec 0,V,E) /\\r
1173      v IN dart (hypermap (HYP (vec 0,V,E))) /\\r
1174      FF = face (hypermap (HYP (vec 0,V,E))) v /\\r
1175      y IN FF\r
1176      ==> wedge_in_fan_ge y E = wedge_in_fan_ge y (e_prime E FF ) /\\r
1177 wedge_in_fan_gt y E = wedge_in_fan_gt y ( e_prime E FF ) `,\r
1178 [ONCE_REWRITE_TAC[TAUT` a /\ b /\c /\ d <=> (a /\ b /\ c ) /\ d `];\r
1179 NHANH IN_FF_IMP_AZIM_CYCLE_EQ;\r
1180 STRIP_TAC;\r
1181 ASSUME_TAC2 (\r
1182 SPEC `vec 0: real^3 ` (GEN `x:real^3 ` CARD_E_GT1_EQ_CARD_E_PRIME));\r
1183 DOWN THEN DOWN;\r
1184 FIRST_X_ASSUM NHANH;\r
1185 PAT_ONCE_REWRITE_TAC`\x. a ==> b ==> x ` [GSYM PAIR];\r
1186 SIMP_TAC[wedge_in_fan_ge; wedge_in_fan_gt];\r
1187 STRIP_TAC;\r
1188 DISCH_TAC;\r
1189 ASM_CASES_TAC `CARD (EE (FST (y:real^3 # real^3)) E) > 1 `;\r
1190 DOWN;\r
1191 ASM_SIMP_TAC[];\r
1192 ABBREV_TAC ` FD = face (hypermap (HYP (vec 0,V,E))) v `;\r
1193 DOWN_TAC;\r
1194 REWRITE_TAC[PAIR_EQ];\r
1195 SIMP_TAC[];\r
1196 DOWN;\r
1197 ASM_SIMP_TAC[];\r
1198 DOWN_TAC;\r
1199 STRIP_TAC;\r
1200 ABBREV_TAC ` FD = face (hypermap (HYP (vec 0,V,E))) v `;\r
1201 SUBGOAL_THEN ` EE (FST y) E = {SND (y:real^3 # real^3)} <=>\r
1202 EE (FST y) ( e_prime E FD ) = {SND y }` ASSUME_TAC;\r
1203 MATCH_MP_TAC (SPEC ` vec 0:real^3 ` (GEN `x:real^3 ` EE_FST_Y_EQ_SET_SET_SNDY));\r
1204 ASM_REWRITE_TAC[];\r
1205 DOWN;\r
1206 EXPAND_TAC "FD";\r
1207 ASM_SIMP_TAC[EQ_SYM_EQ];\r
1208 DOWN THEN MESON_TAC[]]);;\r
1209 \r
1210 \r
1211 \r
1212 \r
1213 \r
1214 let FACE_NODE_EDGE_ORBIT_INVERSE = prove(\r
1215 ` face (H:(A) hypermap) x = orbit_map ( inverse (face_map H )) x /\\r
1216 node H x = orbit_map (inverse ( node_map H)) x /\\r
1217 edge H x = orbit_map (inverse ( edge_map H )) x `,\r
1218 MP_TAC (SPEC_ALL hypermap_lemma) THEN \r
1219 SIMP_TAC[face;node;edge] THEN \r
1220 MESON_TAC[lemma_card_inverse_map_eq]);;\r
1221 \r
1222 \r
1223 \r
1224 \r
1225 \r
1226 \r
1227 \r
1228 let DARTS_E_PRIME_EQ_FF_UNION_SWITCH =\r
1229 prove_by_refinement(` (! x. x IN FF ==> {FST x, SND x } IN E )\r
1230 ==>  darts_of_hyp (e_prime E FF) (v_prime V FF) = \r
1231 FF UNION { ((v:A),w) | (w,v) IN FF }`,\r
1232 [REWRITE_TAC[darts_of_hyp;EXTENSION; IN_UNION];\r
1233 REWRITE_TAC[ord_pairs; self_pairs; IN_ELIM_THM; e_prime; v_prime];\r
1234 STRIP_TAC THEN GEN_TAC;\r
1235 EQ_TAC;\r
1236 STRIP_TAC;\r
1237 DOWN_TAC THEN REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];\r
1238 MESON_TAC[];\r
1239 DOWN THEN DOWN THEN REWRITE_TAC[EE];\r
1240 REWRITE_TAC[SET_RULE` x = {} <=> (! a. ~ ( a IN x ))`];\r
1241 REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM];\r
1242 ASM_MESON_TAC[FST;SND];\r
1243 STRIP_TAC;\r
1244 DISJ1_TAC;\r
1245 EXISTS_TAC ` FST (x:A#A) `;\r
1246 EXISTS_TAC ` SND (x:A#A) `;\r
1247 REWRITE_TAC[];\r
1248 EXISTS_TAC ` FST (x:A#A) `;\r
1249 EXISTS_TAC ` SND (x:A#A) `;\r
1250 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];\r
1251 DISJ1_TAC;\r
1252 EXISTS_TAC ` v:A`;\r
1253 EXISTS_TAC `w:A`;\r
1254 ASM_REWRITE_TAC[];\r
1255 EXISTS_TAC `w:A`;\r
1256 EXISTS_TAC ` v:A`;\r
1257 ASM_SIMP_TAC[INSERT_COMM;PAIR; FST; SND];\r
1258 ASM_MESON_TAC[INSERT_COMM;PAIR; FST; SND]]);;\r
1259 \r
1260 \r
1261 \r
1262 \r
1263 \r
1264 \r
1265 \r
1266 let CARD_FF_GT1_FF_SUBSET =\r
1267 prove_by_refinement(` FAN ((v:real^3),V,E) /\\r
1268     FF = face (hypermap (HYP (v,V,E))) x /\\r
1269     1 < CARD (FF)\r
1270  ==> (! y. y IN FF ==> {FST y, SND y} IN E ) `,\r
1271 [NHANH ELMS_OF_HYPERMAP_HYP;\r
1272 ASM_CASES_TAC ` ~( x IN darts_of_hyp E (V:real^3 -> bool) ) \/ \r
1273 x IN self_pairs E V `;\r
1274 STRIP_TAC;\r
1275 SUBGOAL_THEN ` face_map (hypermap (HYP (v,V,E))) x = x ` MP_TAC;\r
1276 ASM_SIMP_TAC[ff_of_hyp3];\r
1277 ABBREV_TAC ` tt = face_map (hypermap (HYP (v,V,E))) `;\r
1278 ONCE_REWRITE_TAC[orbit_one_point];\r
1279 REWRITE_TAC[BETA_THM];\r
1280 EXPAND_TAC "tt";\r
1281 REWRITE_TAC[GSYM face];\r
1282 UNDISCH_TAC ` 1 < CARD (FF: real^3 # real^3 -> bool) `;\r
1283 ASM_REWRITE_TAC[];\r
1284 MESON_TAC[CARD_SINGLETON; ARITH_RULE ` ~( 1 < 1 ) `];\r
1285 DOWN;\r
1286 REWRITE_TAC[DE_MORGAN_THM];\r
1287 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1288 STRIP_TAC THEN STRIP_TAC;\r
1289 UNDISCH_TAC ` x IN darts_of_hyp E (V:real^3 -> bool) `;\r
1290 ASM_REWRITE_TAC[];\r
1291 NHANH lemma_face_subset;\r
1292 DOWN_TAC;\r
1293 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1294 REWRITE_TAC[SUBSET];\r
1295 STRIP_TAC;\r
1296 ASM_REWRITE_TAC[];\r
1297 FIRST_X_ASSUM NHANH;\r
1298 ASM_REWRITE_TAC[darts_of_hyp; IN_UNION];\r
1299 REPEAT STRIP_TAC;\r
1300 DOWN;\r
1301 REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
1302 SUBGOAL_THEN ` face_map (hypermap (HYP (v,V,E))) y = y ` MP_TAC;\r
1303 ASM_REWRITE_TAC[];\r
1304 ASM_SIMP_TAC[ff_of_hyp3];\r
1305 ABBREV_TAC ` tt = face_map (hypermap (HYP (v,V,E))) `;\r
1306 ONCE_REWRITE_TAC[orbit_one_point];\r
1307 REPLICATE_TAC 3 DOWN;\r
1308 NHANH lemma_face_identity;\r
1309 REPEAT STRIP_TAC THEN DOWN;\r
1310 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1311 UNDISCH_TAC ` 1 < CARD (FF: real^3 # real^3 -> bool) `;\r
1312 ASM_REWRITE_TAC[GSYM face];\r
1313 MESON_TAC[CARD_SINGLETON; ARITH_RULE ` ~( 1 < 1 ) `]]);;\r
1314 \r
1315 \r
1316 \r
1317 \r
1318 \r
1319 \r
1320 \r
1321 \r
1322 \r
1323 let DARTS_E_PRIME_GT1_SWITCH = prove(\r
1324 ` FAN (v,V,E) /\ FF = face (hypermap (HYP (v,V,E))) x /\ 1 < CARD FF\r
1325 ==> darts_of_hyp (e_prime E FF) (v_prime V FF) =\r
1326            FF UNION {v,w | w,v IN FF}`,\r
1327 NHANH CARD_FF_GT1_FF_SUBSET THEN \r
1328 NHANH DARTS_E_PRIME_EQ_FF_UNION_SWITCH THEN SIMP_TAC[]);;\r
1329 \r
1330 \r
1331 \r
1332 \r
1333 \r
1334 \r
1335 let FAN_FACE_GT1_IMAGE_EE_OF_HYP =  prove_by_refinement\r
1336 (` x IN darts_of_hyp E V /\\r
1337 FAN (v,V,E) /\ FF = face (hypermap (HYP (v,V,E))) x /\ 1 < CARD FF\r
1338      ==> darts_of_hyp (e_prime E FF) (v_prime V FF) =\r
1339          FF UNION IMAGE (ee_of_hyp (v,V,E)) FF `,\r
1340 [NHANH DARTS_E_PRIME_GT1_SWITCH;\r
1341 NHANH ELMS_OF_HYPERMAP_HYP;\r
1342 SIMP_TAC[];\r
1343 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1344 STRIP_TAC;\r
1345 UNDISCH_TAC ` x IN darts_of_hyp E (V:real^3 -> bool) `;\r
1346 ASM_REWRITE_TAC[];\r
1347 NHANH lemma_face_subset;\r
1348 ASM_REWRITE_TAC[];\r
1349 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1350 STRIP_TAC;\r
1351 MATCH_MP_TAC (MESON[]` x = y ==> f x = f y `);\r
1352 REWRITE_TAC[IMAGE; EXTENSION; IN_ELIM_THM];\r
1353 UNDISCH_TAC ` ee_of_hyp (v,V,E) = edge_map (hypermap (HYP (v,V,E))) `;\r
1354 DISCH_THEN (SUBST1_TAC o SYM);\r
1355 DOWN;\r
1356 REWRITE_TAC[SUBSET];\r
1357 USE_FIRST ` darts_of_hyp E V = dart (hypermap (HYP (v,V,E))) ` (SUBST1_TAC\r
1358 o SYM);\r
1359 REWRITE_TAC[ee_of_hyp2];\r
1360 MESON_TAC[FST; SND; PAIR]]);;\r
1361 \r
1362 \r
1363 \r
1364 \r
1365 \r
1366 let IN_ORD_PAIRS_E_PRIME = prove(` x IN ord_pairs (e_prime E FF) ==>\r
1367 x IN ord_pairs E /\ x IN darts_of_hyp E V`,\r
1368 REWRITE_TAC[darts_of_hyp; IN_UNION; e_prime; ord_pairs; IN_ELIM_THM]\r
1369 THEN MESON_TAC[]);;\r
1370 \r
1371 \r
1372 \r
1373 \r
1374 let CARD_GT1_EE_OF_HYP_E_PRIME_EQ = prove_by_refinement\r
1375 (` FAN (v,V,E) /\ x IN dart (hypermap (HYP (v,V,E))) /\\r
1376     FF = face  (hypermap (HYP (v,V,E))) x /\\r
1377 1 < CARD FF \r
1378 ==> (! x. x IN FF ==> ee_of_hyp (v,V,E) x =\r
1379 ee_of_hyp (v,v_prime V FF,e_prime E FF) x ) `,\r
1380 [NHANH lemma_face_subset;\r
1381 NHANH ELMS_OF_HYPERMAP_HYP;\r
1382 ONCE_REWRITE_TAC[TAUT` (a1/\a2)/\a3/\a4 <=> a2 /\a3/\a1/\a4`];\r
1383 NHANH DARTS_E_PRIME_GT1_SWITCH;\r
1384 REPEAT STRIP_TAC;\r
1385 REWRITE_TAC[ee_of_hyp2];\r
1386 SUBGOAL_THEN ` x' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;\r
1387 UNDISCH_TAC ` face  (hypermap (HYP (v,V,E))) x SUBSET \r
1388 dart (hypermap (HYP (v,V,E))) `;\r
1389 ASM_REWRITE_TAC[SUBSET];\r
1390 DISCH_THEN MATCH_MP_TAC;\r
1391 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;\r
1392 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);\r
1393 FIRST_X_ASSUM ACCEPT_TAC;\r
1394 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;\r
1395 REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];\r
1396 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
1397 SIMP_TAC[]]);;\r
1398 \r
1399 \r
1400 \r
1401 \r
1402 let FF_IMAGE_EE_OF_HYP_EQ_E_PRIME = prove_by_refinement\r
1403 (` FAN (v,V,E) /\ x IN dart (hypermap (HYP (v,V,E))) /\\r
1404     FF = face  (hypermap (HYP (v,V,E))) x /\\r
1405 1 < CARD FF \r
1406 ==> IMAGE (ee_of_hyp (v,V,E)) FF = \r
1407     IMAGE (ee_of_hyp (v,v_prime V FF,e_prime E FF)) FF `,\r
1408 [NHANH lemma_face_subset;\r
1409 NHANH ELMS_OF_HYPERMAP_HYP;\r
1410 ONCE_REWRITE_TAC[TAUT` (a1/\a2)/\a3/\a4 <=> a2 /\a3/\a1/\a4`];\r
1411 NHANH DARTS_E_PRIME_GT1_SWITCH;\r
1412 STRIP_TAC;\r
1413 REWRITE_TAC[IMAGE; EXTENSION; IN_ELIM_THM];\r
1414 GEN_TAC THEN EQ_TAC;\r
1415 STRIP_TAC;\r
1416 EXISTS_TAC ` x'': real^3 # real^3 `;\r
1417 ASM_REWRITE_TAC[];\r
1418 REWRITE_TAC[ee_of_hyp2];\r
1419 SUBGOAL_THEN ` x'' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;\r
1420 UNDISCH_TAC ` face (hypermap (HYP (v,V,E))) x SUBSET \r
1421 dart (hypermap (HYP (v,V,E))) `;\r
1422 ASM_REWRITE_TAC[SUBSET];\r
1423 DISCH_THEN MATCH_MP_TAC;\r
1424 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;\r
1425 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);\r
1426 FIRST_X_ASSUM ACCEPT_TAC;\r
1427 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;\r
1428 REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];\r
1429 NHANH IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
1430 USE_FIRST ` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);\r
1431 SIMP_TAC[];\r
1432 STRIP_TAC;\r
1433 SUBGOAL_THEN ` x'' IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;\r
1434 UNDISCH_TAC ` face (hypermap (HYP (v,V,E))) x SUBSET \r
1435 dart (hypermap (HYP (v,V,E))) `;\r
1436 ASM_REWRITE_TAC[SUBSET];\r
1437 DISCH_THEN MATCH_MP_TAC;\r
1438 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;\r
1439 MATCH_MP_TAC (MESON[]` x = y ==> f x ==> f y `);\r
1440 FIRST_X_ASSUM ACCEPT_TAC;\r
1441 SUBGOAL_THEN ` x'':real^3 # real^3 IN darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;\r
1442 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;\r
1443 ASM_REWRITE_TAC[IN_UNION];\r
1444 CONV_TAC TAUT;\r
1445 REPEAT STRIP_TAC;\r
1446 EXISTS_TAC `x'':real^3 # real^3 `;\r
1447 ASM_REWRITE_TAC[];\r
1448 DOWN THEN DOWN;\r
1449 SIMP_TAC[ee_of_hyp2];\r
1450 USE_FIRST` FF = face (hypermap (HYP (v,V,E))) x ` (SUBST1_TAC o SYM);\r
1451 SIMP_TAC[]]);;\r
1452 \r
1453 \r
1454 \r
1455 \r
1456 let FIRST_AAUHTVE2 = prove(` FAN (x,V,E) ==>\r
1457      FINITE (darts_of_hyp E V) /\\r
1458      ee_of_hyp (x,V,E) permutes darts_of_hyp E V /\\r
1459      nn_of_hyp (x,V,E) permutes darts_of_hyp E V /\\r
1460      ff_of_hyp (x,V,E) permutes darts_of_hyp E V /\\r
1461      ee_of_hyp (x,V,E) o nn_of_hyp (x,V,E) o ff_of_hyp (x,V,E) = I /\\r
1462      ee_of_hyp (x,V,E) o ee_of_hyp (x,V,E) = I `,\r
1463 NHANH (SMOOTH_GEN_ALL (REWRITE_RULE[TAUT` a/\b ==> c <=> \r
1464 a ==> b ==> c `] FIRST_AAUHTVE)) THEN \r
1465 REWRITE_TAC[HYP; PAIR_EQ] THEN MESON_TAC[]);;\r
1466 \r
1467 \r
1468 \r
1469 \r
1470 \r
1471 \r
1472 \r
1473 let NOT_IN_DART_IMP_IDE = prove(\r
1474 ` ~( x IN dart H ) ==>\r
1475 edge_map H x = x /\\r
1476 node_map H x = x /\\r
1477 face_map H x = x:A `,\r
1478 MP_TAC (SPEC `H:(A) hypermap ` hypermap_lemma)\r
1479 THEN REWRITE_TAC[permutes] THEN SIMP_TAC[]);;\r
1480 \r
1481 \r
1482 \r
1483 \r
1484 \r
1485 let SIMPLE_IMP_DISTINCT_FF_NODE_IMAGE =\r
1486 prove_by_refinement(` simple_hypermap H /\ FF = face H x /\\r
1487 (! x. (x:A) IN FF ==> ~( node_map H x = x ))\r
1488 ==> FF INTER IMAGE (node_map H ) FF = {} `,\r
1489 [REWRITE_TAC[simple_hypermap; INTER; IMAGE];\r
1490 STRIP_TAC;\r
1491 REWRITE_TAC[ EXTENSION; NOT_IN_EMPTY];\r
1492 GEN_TAC;\r
1493 REWRITE_TAC[IN_ELIM_THM];\r
1494 STRIP_TAC;\r
1495 UNDISCH_TAC ` x'':A IN FF `;\r
1496 REWRITE_TAC[];\r
1497 FIRST_X_ASSUM NHANH;\r
1498 ASM_CASES_TAC ` x'':A IN dart H `;\r
1499 DOWN;\r
1500 FIRST_X_ASSUM NHANH;\r
1501 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SET_RULE` {x} a <=> x = a `];\r
1502 STRIP_TAC;\r
1503 ASM_REWRITE_TAC[];\r
1504 NHANH lemma_face_identity;\r
1505 STRIP_TAC;\r
1506 SUBGOAL_THEN ` x':A IN node H x'' /\ x'' IN node H x'' ` (fun x ->\r
1507 ASM_MESON_TAC[x]);\r
1508 ASM_REWRITE_TAC[node_refl; node; in_orbit_map1];\r
1509 DOWN;\r
1510 NHANH NOT_IN_DART_IMP_IDE;\r
1511 SIMP_TAC[]]);;\r
1512 \r
1513 \r
1514 \r
1515 \r
1516 \r
1517 let FX_IN_S_IMP_F_POWER_TOO =\r
1518 prove(` (! (x:A). x IN S ==> f x IN S ) /\ x IN S ==> \r
1519 (!n. (f POWER n ) x IN S ) `, DISCH_TAC THEN INDUCT_TAC THENL \r
1520 [ASM_REWRITE_TAC[POWER; I_THM];\r
1521 REWRITE_TAC[COM_POWER; o_THM] THEN \r
1522 ASM_MESON_TAC[]]);;\r
1523 \r
1524 let FX_IN_S_IMP_ORBIT_SUBSET = prove(\r
1525 ` (!(x:A). x IN S ==> f x IN S) /\ x IN S\r
1526 ==> orbit_map f x SUBSET S `,\r
1527 NHANH FX_IN_S_IMP_F_POWER_TOO THEN \r
1528 REWRITE_TAC[orbit_map; SUBSET; IN_ELIM_THM; ARITH_RULE` n >= 0`]\r
1529 THEN MESON_TAC[]);;\r
1530 \r
1531 \r
1532 \r
1533 \r
1534 \r
1535 let FAN_DARTS_OF_IN_D = prove_by_refinement(\r
1536 ` FAN (v,V,E) /\ x IN darts_of_hyp E V /\ \r
1537 FF = face (hypermap (HYP (v,V,E))) x /\\r
1538 x' IN FF ==> x' IN darts_of_hyp E V`,\r
1539 [NHANH ELMS_OF_HYPERMAP_HYP;\r
1540 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1541 IMP_TAC THEN STRIP_TAC;\r
1542 ASM_REWRITE_TAC[];\r
1543 NHANH_PAT `\x. x ==> y ` lemma_face_subset;\r
1544 REWRITE_TAC[SUBSET]; MESON_TAC[]]);;\r
1545 \r
1546 \r
1547 \r
1548 \r
1549 \r
1550 let FAN_DART_DARTS = prove(` FAN (x,V,E) ==> \r
1551 dart (hypermap (HYP (x,V,E))) = darts_of_hyp E V `,\r
1552 NHANH ELMS_OF_HYPERMAP_HYP THEN SIMP_TAC[]);;\r
1553 \r
1554 \r
1555 \r
1556 \r
1557 let FACE_SUBSET_DARTS = prove(` FAN (v,V,E) /\ x IN darts_of_hyp E V ==> \r
1558 face (hypermap (HYP (v,V,E))) x SUBSET darts_of_hyp E V`,\r
1559 IMP_TAC THEN NHANH ELMS_OF_HYPERMAP_HYP THEN \r
1560 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN \r
1561 SIMP_TAC[lemma_face_subset]);;\r
1562 \r
1563 \r
1564 \r
1565 \r
1566 \r
1567 let FF_DISJOINT_ITS_IMAGE_CARD_EQ = prove_by_refinement\r
1568 (` FAN (v,V,E) /\\r
1569     x IN darts_of_hyp E V /\\r
1570     FF = face (hypermap (HYP (v,V,E))) x /\\r
1571     simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF))) /\\r
1572     2 < CARD (FF) ==>\r
1573     FF INTER IMAGE (nn_of_hyp (v,v_prime V FF, e_prime E FF)) FF = {} /\\r
1574     CARD FF = CARD  (IMAGE (nn_of_hyp (v,v_prime V FF, e_prime E FF)) FF)`,\r
1575 [ONCE_REWRITE_TAC[TAUT` a1/\a2/\a3/\a4/\a5 <=> (a2/\a1/\a3/\a5)/\a4`];\r
1576 NHANH FAN_FACE_GT1_IMAGE_EE_OF_HYP;\r
1577 STRIP_TAC;\r
1578 SUBGOAL_THEN ` FAN (v,v_prime V (FF:real^3 # real^3 -> bool),e_prime E FF) `\r
1579  MP_TAC;\r
1580 DOWN_TAC;\r
1581 NHANH_PAT `\x. x ==> i `  ELMS_OF_HYPERMAP_HYP;\r
1582 ASM_MESON_TAC[IMP_FAN_V_PRIME_E_PRIME];\r
1583 NHANH ELMS_OF_HYPERMAP_HYP;\r
1584 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1585 SIMP_TAC[];\r
1586 STRIP_TAC;\r
1587 CONJ_TAC;\r
1588 SUBGOAL_THEN ` (! x. (x:real^3 # real^3) IN FF ==>\r
1589 ~( node_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x = x )) ` MP_TAC;\r
1590 ONCE_REWRITE_TAC[inverse2_hypermap_maps];\r
1591 REPEAT STRIP_TAC;\r
1592 DOWN;\r
1593 REWRITE_TAC[o_THM];\r
1594 NHANH (MESON[]` ( inverse f) x = y ==> f (( inverse f) x ) = f y `);\r
1595 \r
1596 MP_TAC (ISPEC ` \r
1597 (hypermap (HYP (v,v_prime V FF,e_prime E FF))) ` edge_map_and_darts);\r
1598 NHANH PERMUTES_INVERSES;\r
1599 SIMP_TAC[];\r
1600 STRIP_TAC;\r
1601 STRIP_TAC;\r
1602 ABBREV_TAC ` f = face_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1603 ABBREV_TAC ` e = edge_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1604 ABBREV_TAC ` n = node_map (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1605 ASM_CASES_TAC ` (f:real^3 # real^3 -> real^3 # real^3) x' = e x' `;\r
1606 UNDISCH_TAC` FAN ((v:real^3),v_prime V FF,e_prime E FF) `;\r
1607 REWRITE_TAC[];\r
1608 NHANH FIRST_AAUHTVE2;\r
1609 UNDISCH_TAC `FF = face  (hypermap (HYP (v,V,E))) x`;\r
1610 DISCH_THEN (ASSUME_TAC o SYM);\r
1611 ASM_REWRITE_TAC[];\r
1612 STRIP_TAC;\r
1613 UNDISCH_TAC ` inverse (e:real^3#real^3->real^3#real^3) (inverse\r
1614  (f:real^3#real^3->real^3#real^3) x') = (x':real^3 # real^3 ) `;\r
1615 REWRITE_TAC[];\r
1616 NHANH (MESON[]` inverse e ( f x ) = y ==> e (inverse e ( f x )) = e y `);\r
1617 NHANH (MESON[]` e (inverse e ((inverse f ) x )) = y ==>f ( e (inverse e ( (inverse f ) x ))) = f y `);\r
1618 UNDISCH_TAC `e permutes dart \r
1619 (hypermap (HYP (v,v_prime V FF,e_prime E FF)))`;\r
1620 UNDISCH_TAC ` f permutes dart \r
1621 (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1622 PHA;\r
1623 NHANH PERMUTES_INVERSES;\r
1624 SIMP_TAC[];\r
1625 REPEAT STRIP_TAC;\r
1626 UNDISCH_TAC ` x':real^3 # real^3 IN FF `;\r
1627 EXPAND_TAC "FF";\r
1628 PHA;\r
1629 NHANH lemma_face_identity;\r
1630 SUBGOAL_THEN ` orbit_map f (x':real^3 # real^3) = {x', e x'} ` ASSUME_TAC;\r
1631 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];\r
1632 CONJ_TAC;\r
1633 MATCH_MP_TAC FX_IN_S_IMP_ORBIT_SUBSET;\r
1634 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];\r
1635 GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC;\r
1636 DISJ2_TAC;\r
1637 FIRST_X_ASSUM SUBST1_TAC;\r
1638 FIRST_X_ASSUM ACCEPT_TAC;\r
1639 DISJ1_TAC;\r
1640 FIRST_X_ASSUM SUBST1_TAC;\r
1641 FIRST_X_ASSUM (ACCEPT_TAC o SYM);\r
1642 REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY];\r
1643 REPEAT STRIP_TAC;\r
1644 FIRST_X_ASSUM SUBST1_TAC;\r
1645 REWRITE_TAC[orbit_reflect];\r
1646 FIRST_X_ASSUM SUBST1_TAC;\r
1647 REWRITE_TAC[orbit_reflect];\r
1648 EXPAND_TAC "f";\r
1649 REWRITE_TAC[GSYM face];\r
1650 ASM_MESON_TAC[lemma_inverse_in_face; face_refl];\r
1651 DOWN;\r
1652 ASM_REWRITE_TAC[face];\r
1653 MP_TAC LOCALIZE_PRESERVE_FACE;\r
1654 ANTS_TAC;\r
1655 ASM_REWRITE_TAC[];\r
1656 DOWN_TAC;\r
1657 NHANH ELMS_OF_HYPERMAP_HYP;\r
1658 SIMP_TAC[];\r
1659 ASM_SIMP_TAC[face];\r
1660 REPEAT STRIP_TAC;\r
1661 DOWN;\r
1662 PHA;\r
1663 NHANH (MESON[orbit_reflect]` S = orbit_map f x ==> x IN S `);\r
1664 EXPAND_TAC "f";\r
1665 REWRITE_TAC[GSYM face];\r
1666 NHANH lemma_face_identity;\r
1667 ASM_SIMP_TAC[];\r
1668 REPLICATE_TAC 3 DOWN;\r
1669 UNDISCH_TAC ` 2 < CARD (FF:real^3 # real^3 -> bool) `;\r
1670 EXPAND_TAC "f";\r
1671 REWRITE_TAC[GSYM face];\r
1672 SIMP_TAC[];\r
1673 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1674 SIMP_TAC[];\r
1675 DISCH_TAC;\r
1676 REMOVE_TAC;\r
1677 DISCH_THEN (SUBST1_TAC o SYM);\r
1678 REMOVE_TAC;\r
1679 DOWN;\r
1680 MESON_TAC[Geomdetail.CARD2; ARITH_RULE` a <= 2 ==> ~(2 < a ) `];\r
1681 MP_TAC (ISPEC `hypermap (HYP (v,v_prime V FF,e_prime E FF)) `\r
1682  hypermap_lemma);\r
1683 UNDISCH_TAC `FF = face (hypermap (HYP (v,V,E))) (x:real^3 # real^3) `;\r
1684 DISCH_THEN (ASSUME_TAC o SYM);\r
1685 ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM];\r
1686 STRIP_TAC;\r
1687 FIRST_ASSUM (MP_TAC o (SPEC `x':real^3 # real^3 `));\r
1688 PHA;\r
1689 NHANH (MESON[]` f x = y ==> f ( f x ) = f y `);\r
1690 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF) `;\r
1691 NHANH FIRST_AAUHTVE2;\r
1692 DOWN THEN REMOVE_TAC;\r
1693 ASM_REWRITE_TAC[];\r
1694 STRIP_TAC;\r
1695 DOWN;\r
1696 SIMP_TAC[FUN_EQ_THM; o_THM; I_THM];\r
1697 REPEAT STRIP_TAC;\r
1698 UNDISCH_TAC `simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF)))\r
1699  `;\r
1700 REWRITE_TAC[simple_hypermap];\r
1701 STRIP_TAC;\r
1702 FIRST_X_ASSUM (MP_TAC o (SPEC ` \r
1703 (f:real^3 # real^3 -> real^3 # real^3) x' `));\r
1704 ANTS_TAC;\r
1705 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF) `;\r
1706 NHANH (SMOOTH_GEN_ALL (GEN `y:real^3 # real^3 `\r
1707  FAN_IMP_IN_DARTS_IFF_FF_TOO));\r
1708 ASM_REWRITE_TAC[];\r
1709 STRIP_TAC;\r
1710 FIRST_ASSUM (fun x -> ONCE_REWRITE_TAC[GSYM x]);\r
1711 UNDISCH_TAC `darts_of_hyp (e_prime E FF) (v_prime V FF) =\r
1712       dart (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1713 DISCH_THEN (ASSUME_TAC o SYM);\r
1714 FIRST_ASSUM SUBST1_TAC;\r
1715 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
1716 ASM_REWRITE_TAC[];\r
1717 MATCH_MP_TAC FAN_DARTS_OF_IN_D;\r
1718 ASM_REWRITE_TAC[];\r
1719 STRIP_TAC;\r
1720 MP_TAC (\r
1721 ISPECL [`hypermap (HYP (v,v_prime V FF,e_prime E FF)) `;\r
1722 ` (f:real^3 # real^3 -> real^3 # real^3) x' ` ] face_refl);\r
1723 PHA;\r
1724 NHANH lemma_inverse_in_face;\r
1725 NHANH lemma_inverse_in_face;\r
1726 ASM_SIMP_TAC[PERMUTES_INVERSES];\r
1727 UNDISCH_TAC `f permutes dart (hypermap (HYP (v,v_prime V FF,e_prime E FF))) `;\r
1728 NHANH PERMUTES_INVERSES;\r
1729 SIMP_TAC[];\r
1730 ASM_REWRITE_TAC[];\r
1731 REPEAT STRIP_TAC;\r
1732 SUBGOAL_THEN ` n (f (x':real^3 # real^3)) IN node (hypermap (HYP (v,v_prime V FF,e_prime E\r
1733  FF))) (f x') ` MP_TAC;\r
1734 EXPAND_TAC "n";\r
1735 REWRITE_TAC[node; in_orbit_map1];\r
1736 ASM_REWRITE_TAC[];\r
1737 DOWN;\r
1738 MATCH_MP_TAC (SET_RULE` ~( a IN B INTER A ) ==> a IN A ==> ~( a IN B ) `);\r
1739 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];\r
1740 STRIP_TAC;\r
1741 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IMAGE; IN_ELIM_THM];\r
1742 REPEAT STRIP_TAC;\r
1743 UNDISCH_TAC ` simple_hypermap (hypermap (HYP \r
1744 (v,v_prime V FF,e_prime E FF))) `;\r
1745 REWRITE_TAC[simple_hypermap];\r
1746 STRIP_TAC;\r
1747 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` x'':real^3 # real^3 `));\r
1748 DOWN;\r
1749 ANTS_TAC;\r
1750 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF)`;\r
1751 \r
1752 SIMP_TAC[FAN_DART_DARTS];\r
1753 STRIP_TAC;\r
1754 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
1755 ASM_REWRITE_TAC[];\r
1756 MATCH_MP_TAC FAN_DARTS_OF_IN_D;\r
1757 ASM_REWRITE_TAC[];\r
1758 MP_TAC (SPEC ` x'': real^3 # real^3 ` (GEN `x:real^3 # real^3 `\r
1759  LOCALIZE_PRESERVE_FACE));\r
1760 ANTS_TAC;\r
1761 ASM_REWRITE_TAC[];\r
1762 CONJ_TAC;\r
1763 MATCH_MP_TAC (SET_RULE` x IN FF /\ FF SUBSET A ==> x IN A `);\r
1764 ASM_REWRITE_TAC[];\r
1765 MATCH_MP_TAC lemma_face_subset;\r
1766 UNDISCH_TAC ` FAN (v:real^3,V,E)`;\r
1767 NHANH ELMS_OF_HYPERMAP_HYP;\r
1768 ASM_SIMP_TAC[];\r
1769 MATCH_MP_TAC lemma_face_identity;\r
1770 UNDISCH_TAC ` x'':real^3 # real^3 IN FF `;\r
1771 ASM_SIMP_TAC[];\r
1772 DISCH_TAC;\r
1773 REWRITE_TAC[EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY];\r
1774 STRIP_TAC;\r
1775 FIRST_X_ASSUM (MP_TAC o (SPEC ` x':real^3 # real^3 `));\r
1776 FIRST_X_ASSUM (MP_TAC o (SPEC ` x'': real^3 # real^3 `));\r
1777 ANTS_TAC;\r
1778 ASM_REWRITE_TAC[];\r
1779 SUBGOAL_THEN ` x' IN node  (hypermap (HYP (v,v_prime V FF,e_prime E FF))) x''`\r
1780 MP_TAC;\r
1781 ASM_REWRITE_TAC[node; in_orbit_map1];\r
1782 \r
1783 REPLICATE_TAC 4 DOWN THEN PHA;\r
1784 MESON_TAC[];\r
1785 MATCH_MP_TAC CARD_IMAGE_INJ;\r
1786 MP_TAC (ISPEC ` hypermap (HYP (v,v_prime V FF,e_prime E FF)) `\r
1787  node_map_and_darts);\r
1788 REWRITE_TAC[permutes; EXISTS_UNIQUE];\r
1789 STRIP_TAC;\r
1790 CONJ_TAC;\r
1791 DOWN;\r
1792 MESON_TAC[];\r
1793 UNDISCH_TAC ` FAN (v:real^3,V,E) `;\r
1794 NHANH FAN_IMP_FIMITE_DARTS;\r
1795 ASM_REWRITE_TAC[];\r
1796 MATCH_MP_TAC (MESON[FINITE_SUBSET]` (a ==> A SUBSET B) ==> \r
1797 a /\ FINITE B ==> FINITE A `);\r
1798 STRIP_TAC;\r
1799 MATCH_MP_TAC FACE_SUBSET_DARTS;\r
1800 ASM_REWRITE_TAC[]]);;\r
1801 \r
1802 \r
1803 \r
1804 \r
1805 \r
1806 let HYP_MAPS_INJ = prove(\r
1807 `(! (x:A) y. edge_map H x = edge_map H y <=> x = y ) /\\r
1808 (! x y. node_map H x = node_map H y <=> x = y ) /\\r
1809 (! x y. face_map H x = face_map H y <=> x = y ) `,\r
1810 MP_TAC (SPEC_ALL hypermap_lemma) THEN \r
1811 REWRITE_TAC[permutes] THEN MESON_TAC[]);;\r
1812 \r
1813 \r
1814 \r
1815 \r
1816 \r
1817 let SIMPLE_FACE_DISJOINT_NODE_MAP_2 = prove_by_refinement\r
1818 (` (x:A) IN dart H /\\r
1819 face H x SUBSET dart H /\\r
1820 simple_hypermap H /\\r
1821 face H x INTER IMAGE (node_map H) (face H x) = {} /\\r
1822 dart H = face H x UNION IMAGE (node_map H) (face H x)\r
1823 ==> !x. x IN dart H\r
1824           ==> ~(node_map H x = x) /\ node_map H (node_map H x) = x `,\r
1825 [STRIP_TAC;\r
1826 ASM_REWRITE_TAC[IN_UNION];\r
1827 GEN_TAC;\r
1828 DISCH_TAC;\r
1829 SUBGOAL_THEN ` ~( node_map H x':A = x') ` ASSUME_TAC;\r
1830 STRIP_TAC;\r
1831 FIRST_X_ASSUM DISJ_CASES_TAC;\r
1832 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;\r
1833 PHA;\r
1834 REWRITE_TAC[SET_RULE `~( a INTER b = {} ) <=> ? x. x IN a /\ x IN b `];\r
1835 REPEAT (EXISTS_TAC ` x':A` THEN \r
1836 ASM_REWRITE_TAC[IN_IMAGE]);\r
1837 DOWN;\r
1838 REWRITE_TAC[IN_IMAGE];\r
1839 EXPAND_TAC "x'";\r
1840 REWRITE_TAC[HYP_MAPS_INJ];\r
1841 STRIP_TAC;\r
1842 \r
1843 ASM SET_TAC[];\r
1844 \r
1845 ASM_REWRITE_TAC[];\r
1846 UNDISCH_TAC ` x' IN face H x \/ x' IN IMAGE (node_map H) (face H (x:A)) `;\r
1847 SPEC_TAC (`x':A`,` x':A `);\r
1848 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c ) /\ ( b ==> c ) `;\r
1849 MESON[]` (! x. P x /\ Q x ) <=> (! x. P x ) /\ (! x. Q x ) `];\r
1850 MATCH_MP_TAC (TAUT` a /\ ( a ==> b ) ==> a /\ b `);\r
1851 CONJ_TAC;\r
1852 DOWN THEN REMOVE_TAC;\r
1853 REPEAT STRIP_TAC;\r
1854 ASM_CASES_TAC ` node_map H (x':A) = x' `;\r
1855 ASM_REWRITE_TAC[];\r
1856 ASSUME_TAC2 lemma_face_subset;\r
1857 SUBGOAL_THEN` x':A IN dart H ` MP_TAC;\r
1858 DOWN;\r
1859 REWRITE_TAC[SUBSET];\r
1860 DISCH_THEN MATCH_MP_TAC;\r
1861 ASM_REWRITE_TAC[];\r
1862 NHANH lemma_dart_invariant;\r
1863 STRIP_TAC;\r
1864 UNDISCH_TAC `node_map H x':A IN dart H `;\r
1865 NHANH lemma_dart_invariant;\r
1866 STRIP_TAC;\r
1867 UNDISCH_TAC `node_map H (node_map H x':A) IN dart H `;\r
1868 ASM_REWRITE_TAC[IN_UNION];\r
1869 STRIP_TAC;\r
1870 UNDISCH_TAC ` simple_hypermap (H:(A)hypermap) `;\r
1871 REWRITE_TAC[simple_hypermap];\r
1872 DISCH_THEN (MP_TAC o (SPEC `x': A `));\r
1873 ANTS_TAC;\r
1874 FIRST_ASSUM ACCEPT_TAC;\r
1875 REWRITE_TAC[EXTENSION; IN_INTER; IN_INSERT; NOT_IN_EMPTY];\r
1876 DISCH_THEN (fun x -> REWRITE_TAC[GSYM x]);\r
1877 ASM_REWRITE_TAC[];\r
1878 UNDISCH_TAC ` x':A IN face H x `;\r
1879 NHANH_PAT`\x. x ==> i ` lemma_face_identity;\r
1880 STRIP_TAC;\r
1881 CONJ_TAC;\r
1882 REWRITE_TAC[node];\r
1883 MESON_TAC[orbit_reflect;IN_ORBIT_MAP_IMP_F_Y];\r
1884 ASM_MESON_TAC[];\r
1885 DOWN;\r
1886 REWRITE_TAC[IN_IMAGE; HYP_MAPS_INJ];\r
1887 STRIP_TAC;\r
1888 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;\r
1889 REWRITE_TAC[SET_RULE` A INTER B = {} <=> ! x. x IN A ==> ~( x IN B ) `];\r
1890 DISCH_THEN (MP_TAC o (SPEC` x'':A`));\r
1891 ANTS_TAC;\r
1892 ASM_REWRITE_TAC[];\r
1893 EXPAND_TAC "x''";\r
1894 REWRITE_TAC[IN_IMAGE];\r
1895 UNDISCH_TAC ` (x':A) IN face H x `;\r
1896 MESON_TAC[];\r
1897 STRIP_TAC;\r
1898 REWRITE_TAC[IN_IMAGE];\r
1899 REPEAT STRIP_TAC;\r
1900 DOWN;\r
1901 FIRST_X_ASSUM NHANH;\r
1902 ASM_SIMP_TAC[]]);;\r
1903 \r
1904 \r
1905 \r
1906 \r
1907 let ITER12 = prove(` ! f x. ITER 1 f x = f x /\ ITER 2 f x = f ( f x )`,\r
1908 REWRITE_TAC[ARITH_RULE` 2 = SUC 1 /\ 1 = SUC 0`; ITER]);;\r
1909 \r
1910 \r
1911 \r
1912 \r
1913 let ENF_RULE t = \r
1914 prove(t, MESON_TAC[edge_map_and_darts;hypermap_lemma; convolution_rep]);;\r
1915 \r
1916 let EDGE_MAP_RESO_INVERSE = ENF_RULE\r
1917 ` (edge_map H ) o (edge_map H ) = I <=> inverse (edge_map H ) = edge_map H `;;\r
1918 \r
1919 \r
1920 let EDGE_MAP_RESO_INVERSE = CONJ EDGE_MAP_RESO_INVERSE (\r
1921 ENF_RULE `node_map H o node_map H = I <=> inverse (node_map H) = node_map H `);;\r
1922 \r
1923 \r
1924 \r
1925 let HAS_ORD2_INTERPRET = prove(` f has_orders 2 <=> f o f = I /\ ~( f = I ) `,\r
1926 SIMP_TAC[has_orders; ITER12; FUN_EQ_THM; o_THM; ARITH_RULE ` 0 < c /\ c < 2 \r
1927 <=> c = 1 `] THEN MESON_TAC[]);;\r
1928 \r
1929 \r
1930 \r
1931 \r
1932 let HYP_MAPS_INVS = prove(` edge_map H (inverse ( edge_map H ) x ) = x /\\r
1933  inverse (edge_map H) ( edge_map H x ) = x /\\r
1934 face_map H (inverse ( face_map H ) x ) = x /\\r
1935  inverse (face_map H) ( face_map H x ) = x /\\r
1936 node_map H (inverse ( node_map H ) x ) = x /\\r
1937  inverse (node_map H) ( node_map H x ) = x `,\r
1938 MESON_TAC[PERMUTES_INVERSES; hypermap_lemma]);;\r
1939 \r
1940 \r
1941 \r
1942 let ITER_CYCLIC_ORBIT = prove(` 0 < i /\ ITER i f x = x  ==> orbit_map f x = \r
1943 {ITER n f x | n < i } `,\r
1944 REWRITE_TAC[ARITH_RULE` 0 < i <=> ~( i = 0 ) `; GSYM POWER_TO_ITER] THEN \r
1945 NHANH orbit_cyclic THEN SIMP_TAC[]);;\r
1946 \r
1947 \r
1948 \r
1949 let FACE_CYCLE_CARD = prove(\r
1950 `! x y H. y IN face H x ==> (face_map H POWER CARD (face H x )) y = y`,\r
1951 NHANH lemma_face_identity THEN SIMP_TAC[lemma_face_cycle]);;\r
1952 \r
1953 \r
1954 \r
1955 \r
1956 let INVERSE_FACE_CYCLE = prove(\r
1957 `! (x:A) H. (inverse (face_map H) POWER (CARD (face H x)) ) x = x `,\r
1958 REWRITE_TAC[FACE_NODE_EDGE_ORBIT_INVERSE] THEN \r
1959 REPEAT GEN_TAC  THEN \r
1960 MP_TAC (SPEC_ALL face_map_and_darts) THEN \r
1961 NHANH PERMUTES_INVERSE THEN \r
1962 MESON_TAC[lemma_cycle_orbit]);;\r
1963 \r
1964 \r
1965 \r
1966 let INVERSE_FACE_CYCLE_ALL = prove(` ! x y H. y IN face H x ==> \r
1967 (inverse (face_map H) POWER (CARD (face H x)) ) y = y `,\r
1968 NHANH lemma_face_identity THEN \r
1969 SIMP_TAC[INVERSE_FACE_CYCLE]);;\r
1970 \r
1971 \r
1972 \r
1973 let DIH2K_IMP_SIMPLE_HYPERMAP2 = prove(\r
1974 ` dih2k (H:(A)hypermap) k /\ ~( k = 0) ==> simple_hypermap H `,\r
1975 MP_TAC face_map_and_darts THEN \r
1976 MESON_TAC[DIH2K_IMP_SIMPLE_HYPERMAP]);;\r
1977 \r
1978 \r
1979 \r
1980 \r
1981 \r
1982 let DIH2K_FACE_SIMPLIZED = prove_by_refinement\r
1983 (` edge_map H has_orders 2 /\\r
1984 (x:A) IN dart H /\ simple_hypermap H /\\r
1985 (face H x ) INTER IMAGE (node_map H ) (face H x ) = {} /\\r
1986  dart H = (face H x ) UNION IMAGE (node_map H) (face H x ) \r
1987 <=> dih2k H (CARD (face H x )) /\ x IN dart H`,\r
1988 [EQ_TAC;\r
1989 SIMP_TAC[];\r
1990 NHANH lemma_face_subset;\r
1991 REWRITE_TAC[dih2k];\r
1992 STRIP_TAC;\r
1993 CONJ_TAC;\r
1994 MP_TAC (SPEC_ALL FACE_FINITE);\r
1995 NHANH (ISPEC ` node_map (H:(A)hypermap) ` FINITE_IMAGE);\r
1996 UNDISCH_TAC ` face H (x:A) INTER IMAGE (node_map H) (face H x) = {}`;\r
1997 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\ a ==> c `];\r
1998 PHA;\r
1999 NHANH CARD_UNION;\r
2000 STRIP_TAC;\r
2001 DOWN;\r
2002 ASM_REWRITE_TAC[];\r
2003 MATCH_MP_TAC (ARITH_RULE` b = a ==> x = a + b ==> x = 2 * a `);\r
2004 MATCH_MP_TAC CARD_IMAGE_INJ;\r
2005 ASM_REWRITE_TAC[];\r
2006 SIMP_TAC[HYP_MAPS_INJ];\r
2007 SUBGOAL_THEN `(! (x:A). x IN dart H ==> ~( node_map H x = x ) /\\r
2008 (node_map H (node_map H x )) = x )` ASSUME_TAC;\r
2009 DOWN_TAC;\r
2010 MESON_TAC[SIMPLE_FACE_DISJOINT_NODE_MAP_2];\r
2011 \r
2012 ASM_SIMP_TAC[];\r
2013 SUBGOAL_THEN ` node_map (H:(A)hypermap) has_orders 2 ` MP_TAC;\r
2014 REWRITE_TAC[has_orders];\r
2015 REWRITE_TAC[FUN_EQ_THM];\r
2016 CONJ_TAC;\r
2017 REWRITE_TAC[ARITH_RULE` 0 < x /\ x < 2 <=> x = 1 `];\r
2018 SIMP_TAC[ITER12; I_THM];\r
2019 GEN_TAC THEN STRIP_TAC;\r
2020 REWRITE_TAC[NOT_FORALL_THM];\r
2021 EXISTS_TAC `x:A`;\r
2022 ASM_MESON_TAC[];\r
2023 REWRITE_TAC[ITER12; I_THM];\r
2024 GEN_TAC;\r
2025 ASM_CASES_TAC ` (x':A) IN dart H `;\r
2026 ASM_MESON_TAC[];\r
2027 DOWN;\r
2028 MP_TAC (REWRITE_RULE[permutes] hypermap_lemma);\r
2029 SIMP_TAC[];\r
2030 SIMP_TAC[];\r
2031 \r
2032 STRIP_TAC;\r
2033 SUBGOAL_THEN ` ! y. y IN face H (x:A) ==> face_map H (node_map H y) =\r
2034 node_map H ( (inverse (face_map H )) y )` MP_TAC;\r
2035 REPEAT STRIP_TAC;\r
2036 PAT_ONCE_REWRITE_TAC `\x. f x = y ` [inverse2_hypermap_maps];\r
2037 DOWN_TAC;\r
2038 REWRITE_TAC[HAS_ORD2_INTERPRET; EDGE_MAP_RESO_INVERSE];\r
2039 SIMP_TAC[o_THM];\r
2040 STRIP_TAC;\r
2041 REWRITE_TAC[\r
2042 MESON[inverse2_hypermap_maps]`  face_map H = inverse (node_map H) o \r
2043 inverse (edge_map H) `];\r
2044 \r
2045 REWRITE_TAC[o_THM; HYP_MAPS_INVS];\r
2046 ASM_REWRITE_TAC[];\r
2047 STRIP_TAC;\r
2048 \r
2049 \r
2050 (* hhhhhhh *)\r
2051 SUBGOAL_THEN` !y. y IN face H (x:A)\r
2052           ==> ( ! n. ITER n (face_map H) (node_map H y) = \r
2053 node_map H (ITER n (inverse (face_map H)) y))` MP_TAC;\r
2054 GEN_TAC THEN STRIP_TAC;\r
2055 INDUCT_TAC;\r
2056 REWRITE_TAC[ITER];\r
2057 SUBGOAL_THEN ` ITER n (inverse (face_map H)) (y:A) IN face H (x:A) ` ASSUME_TAC;\r
2058 DOWN THEN DOWN;\r
2059 NHANH_PAT `\x. x ==> y ` lemma_face_identity;\r
2060 SIMP_TAC[];\r
2061 REPEAT STRIP_TAC;\r
2062 REWRITE_TAC[FACE_NODE_EDGE_ORBIT_INVERSE; orbit_map; IN_ELIM_THM];\r
2063 EXISTS_TAC `n:num `;\r
2064 REWRITE_TAC[POWER_TO_ITER; ARITH_RULE ` x >= 0`];\r
2065 REWRITE_TAC[ITER];\r
2066 DOWN;\r
2067 FIRST_ASSUM NHANH;\r
2068 ASM_REWRITE_TAC[];\r
2069 SIMP_TAC[];\r
2070 \r
2071 \r
2072 \r
2073 (* ,,,,,,,,,,,,,, *)\r
2074 STRIP_TAC;\r
2075 MATCH_MP_TAC (TAUT` a /\ ( a ==> b ) ==> a /\ b `);\r
2076 CONJ_TAC;\r
2077 \r
2078 GEN_TAC;\r
2079 REWRITE_TAC[IN_UNION];\r
2080 STRIP_TAC;\r
2081 LET_TAC;\r
2082 DOWN THEN DOWN;\r
2083 NHANH lemma_face_identity;\r
2084 SIMP_TAC[];\r
2085 LET_TAC;\r
2086 DOWN THEN DOWN;\r
2087 REWRITE_TAC[IN_IMAGE];\r
2088 STRIP_TAC;\r
2089 \r
2090 \r
2091 \r
2092 REPEAT STRIP_TAC;\r
2093 MATCH_MP_TAC (SET_RULE` a = y /\ b = x ==> a UNION b = x UNION y `);\r
2094 SUBGOAL_THEN ` IMAGE (node_map H) (face H (x:A)) = S` ASSUME_TAC;\r
2095 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2096 ASM_REWRITE_TAC[];\r
2097 UNDISCH_TAC ` x'':A IN face H x `;\r
2098 NHANH lemma_face_identity;\r
2099 SIMP_TAC[];\r
2100 STRIP_TAC;\r
2101 PAT_ONCE_REWRITE_TAC `\x. x = y ` [FACE_NODE_EDGE_ORBIT_INVERSE];\r
2102 REWRITE_TAC[IMAGE; face; orbit_map; EXTENSION; IN_ELIM_THM; POWER_TO_ITER; ARITH_RULE ` x >= 0 `];\r
2103 GEN_TAC;\r
2104 DOWN THEN DOWN;\r
2105 FIRST_X_ASSUM NHANH;\r
2106 SIMP_TAC[];\r
2107 STRIP_TAC THEN STRIP_TAC;\r
2108 MESON_TAC[];\r
2109 ASM_SIMP_TAC[];\r
2110 EXPAND_TAC "S";\r
2111 REWRITE_TAC[GSYM IMAGE_o];\r
2112 UNDISCH_TAC ` node_map (H:(A)hypermap) has_orders 2`;\r
2113 SIMP_TAC[HAS_ORD2_INTERPRET; IMAGE_I];\r
2114 \r
2115 REWRITE_TAC[has_orders; FUN_EQ_THM; I_THM];\r
2116 STRIP_TAC;\r
2117 CONJ_TAC;\r
2118 GEN_TAC;\r
2119 STRIP_TAC;\r
2120 REWRITE_TAC[NOT_FORALL_THM];\r
2121 EXISTS_TAC`x:A `;\r
2122 STRIP_TAC;\r
2123 ASSUME_TAC2 (\r
2124 ISPECL [`i:num`;`(face_map H): A -> A `] (GEN_ALL ITER_CYCLIC_ORBIT));\r
2125 DOWN THEN PHA;\r
2126 REWRITE_TAC[GSYM face];\r
2127 NHANH (MESON[CARD_LE_K_OF_SET_K_FIRST_ELMS]` \r
2128 S = { ITER n f x | n < i } ==> CARD S <= i`);\r
2129 DOWN THEN DOWN;\r
2130 MESON_TAC[ARITH_RULE` a < (b:num) ==> ~( b <= a ) `];\r
2131 REWRITE_TAC[GSYM POWER_TO_ITER; lemma_face_cycle];\r
2132 GEN_TAC;\r
2133 ASM_CASES_TAC `x':A IN dart H `;\r
2134 DOWN;\r
2135 ASM_REWRITE_TAC[IN_UNION];\r
2136 STRIP_TAC;\r
2137 DOWN;\r
2138 REWRITE_TAC[FACE_CYCLE_CARD];\r
2139 DOWN;\r
2140 REWRITE_TAC[IN_IMAGE];\r
2141 DOWN THEN FIRST_ASSUM NHANH;\r
2142 REPEAT STRIP_TAC;\r
2143 ASM_REWRITE_TAC[POWER_TO_ITER];\r
2144 REWRITE_TAC[GSYM POWER_TO_ITER];\r
2145 ASM_SIMP_TAC[INVERSE_FACE_CYCLE_ALL];\r
2146 DOWN THEN NHANH NOT_IN_DART_IMP_IDE;\r
2147 SIMP_TAC[POWER_TO_ITER; ITER_FIXPOINT2];\r
2148 \r
2149 \r
2150 \r
2151 MP_TAC (SPEC_ALL face_map_and_darts);\r
2152 NHANH_PAT `\x. a ==> x ==> y ` lemma_face_subset;\r
2153 STRIP_TAC THEN STRIP_TAC;\r
2154 UNDISCH_TAC ` face H (x:A) SUBSET dart H`;\r
2155 UNDISCH_TAC ` FINITE (dart (H:(A) hypermap)) `;\r
2156 PHA;\r
2157 NHANH FINITE_SUBSET;\r
2158 IMP_TAC THEN STRIP_TAC;\r
2159 MP_TAC (SPEC_ALL face_refl);\r
2160 PHA;\r
2161 REWRITE_TAC[SET_RULE` x IN A <=> {x} SUBSET A `];\r
2162 NHANH CARD_SUBSET;\r
2163 REWRITE_TAC[CARD_SINGLETON];\r
2164 NHANH (ARITH_RULE` 1 <= a ==> ~( a = 0 ) `);\r
2165 STRIP_TAC;\r
2166 DOWN;\r
2167 UNDISCH_TAC ` dih2k H (CARD (face H (x:A)))`;\r
2168 PHA;\r
2169 NHANH DIH2K_IMP_SIMPLE_HYPERMAP2;\r
2170 ASM_SIMP_TAC[dih2k; INSERT_SUBSET; EMPTY_SUBSET];\r
2171 STRIP_TAC;\r
2172 CONJ_TAC;\r
2173 UNDISCH_TAC ` (x:A) IN dart H `;\r
2174 FIRST_X_ASSUM NHANH;\r
2175 LET_TAC;\r
2176 STRIP_TAC;\r
2177 MATCH_MP_TAC (MESON[CARD_UNION_OVERLAP_EQ]`\r
2178 FINITE s /\ FINITE t /\ CARD (s UNION t) = CARD s + CARD t \r
2179 ==> s INTER t = {}`);\r
2180 FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);\r
2181 ASM_REWRITE_TAC[ARITH_RULE` 2 * x = x + v <=> x = v `];\r
2182 CONJ_TAC;\r
2183 MATCH_MP_TAC FINITE_IMAGE;\r
2184 ASM_REWRITE_TAC[];\r
2185 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2186 MATCH_MP_TAC CARD_IMAGE_INJ;\r
2187 ASM_REWRITE_TAC[HYP_MAPS_INJ];\r
2188 SIMP_TAC[];\r
2189 \r
2190 \r
2191 UNDISCH_TAC ` (x:A) IN dart H `;\r
2192 FIRST_X_ASSUM NHANH;\r
2193 LET_TAC;\r
2194 SIMP_TAC[]]);;\r
2195 \r
2196 \r
2197 \r
2198 let EE_OF_HYP_IDE_FST_SND_EQ = prove(`z IN darts_of_hyp E V ==>\r
2199 ( ee_of_hyp (x,V,E) z = z <=> FST z = SND z )`,\r
2200 REWRITE_TAC[ee_of_hyp2] THEN SIMP_TAC[] THEN \r
2201 ONCE_REWRITE_TAC[PAIR_EQ2] THEN \r
2202 SIMP_TAC[EQ_SYM_EQ]);;\r
2203 \r
2204 \r
2205 \r
2206 let MP_TAC2 th = MP_TAC th THEN ANTS_TAC THENL [\r
2207 ASM_SIMP_TAC[]; SIMP_TAC[]] ;;\r
2208 \r
2209 \r
2210 \r
2211 let TR_ENF_TAC = MATCH_MP_TAC W_EQ_ITS_ORBIT_IMP_EQ_ITS_IMAGE THEN \r
2212 REWRITE_TAC[GSYM face; GSYM node; GSYM edge; lemma_face_identity;\r
2213 lemma_node_identity; lemma_edge_identity];;\r
2214 \r
2215 \r
2216 let ENF_IMAGE_ITSELF = let t1 = CONJ ( prove(\r
2217 ` face H x = IMAGE (face_map H ) (face H x )`, TR_ENF_TAC))\r
2218  (prove(\r
2219 ` node H x = IMAGE (node_map H ) (node H x )`, TR_ENF_TAC)) in\r
2220 CONJ (prove(\r
2221 ` edge H x = IMAGE (edge_map H ) (edge H x )`, TR_ENF_TAC)) t1;;\r
2222 \r
2223 \r
2224 \r
2225 let IDE_ON_S_IMP_SAME_IMAGE = prove(` (! x. x IN S ==> f x = g x ) ==>\r
2226 IMAGE f S = IMAGE g S `,\r
2227 REWRITE_TAC[EXTENSION; IMAGE; IN_ELIM_THM] THEN \r
2228 MESON_TAC[]);;\r
2229 \r
2230 \r
2231 \r
2232 let DIH_K_HYP_E_PRIME = prove_by_refinement\r
2233 (` FAN (v,V,E) /\\r
2234     x IN darts_of_hyp E V /\\r
2235     FF = face (hypermap (HYP (v,V,E))) x /\\r
2236     simple_hypermap (hypermap (HYP (v,v_prime V FF,e_prime E FF))) /\\r
2237     2 < CARD (FF) ==>\r
2238     dih2k (hypermap (HYP (v,v_prime V FF,e_prime E FF))) (CARD FF ) `,\r
2239 [ONCE_REWRITE_TAC[TAUT` a1/\a2/\a3/\a4/\a5 <=> (a2/\a1/\a3/\a5)/\a4`];\r
2240 NHANH FAN_FACE_GT1_IMAGE_EE_OF_HYP;\r
2241 STRIP_TAC;\r
2242 MP_TAC LOCALIZE_PRESERVE_FACE THEN ANTS_TAC;\r
2243 ASM_REWRITE_TAC[];\r
2244 DOWN_TAC THEN NHANH FAN_DART_DARTS;\r
2245 SIMP_TAC[];\r
2246 ABBREV_TAC ` hy = HYP (v,v_prime V FF,e_prime E FF) `;\r
2247 SIMP_TAC[];\r
2248 STRIP_TAC;\r
2249 MATCH_MP_TAC (MESON[]` dih2k H k /\ (x:A) IN dart H ==> dih2k H k `);\r
2250 REWRITE_TAC[GSYM DIH2K_FACE_SIMPLIZED];\r
2251 CONJ_TAC;\r
2252 REWRITE_TAC[HAS_ORD2_INTERPRET];\r
2253 CONJ_TAC;\r
2254 MP_TAC IMP_FAN_V_PRIME_E_PRIME;\r
2255 ANTS_TAC;\r
2256 ASM_REWRITE_TAC[];\r
2257 DOWN_TAC THEN NHANH FAN_DART_DARTS;\r
2258 ASM_SIMP_TAC[];\r
2259 MESON_TAC[];\r
2260 NHANH FIRST_AAUHTVE2;\r
2261 NHANH ELMS_OF_HYPERMAP_HYP;\r
2262 ASM_MESON_TAC[];\r
2263 \r
2264 \r
2265 \r
2266 MP_TAC IMP_FAN_V_PRIME_E_PRIME;\r
2267 ANTS_TAC;\r
2268 ASM_REWRITE_TAC[];\r
2269 DOWN_TAC THEN NHANH FAN_DART_DARTS;\r
2270 ASM_SIMP_TAC[];\r
2271 MESON_TAC[];\r
2272 STRIP_TAC;\r
2273 REWRITE_TAC[FUN_EQ_THM; NOT_FORALL_THM];\r
2274 EXISTS_TAC `x:real^3 # real^3 `;\r
2275 REWRITE_TAC[I_THM];\r
2276 EXPAND_TAC "hy";\r
2277 DOWN;\r
2278 SIMP_TAC[ELMS_OF_HYPERMAP_HYP];\r
2279 STRIP_TAC;\r
2280 SUBGOAL_THEN ` (x:real^3 # real^3) IN \r
2281 darts_of_hyp (e_prime E FF) (v_prime V FF) ` MP_TAC;\r
2282 \r
2283 \r
2284 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
2285 ASM_SIMP_TAC[face_refl];\r
2286 SIMP_TAC[EE_OF_HYP_IDE_FST_SND_EQ];\r
2287 \r
2288 \r
2289 REWRITE_TAC[darts_of_hyp; IN_UNION; IN_ORD_E_EQ_IN_E];\r
2290 STRIP_TAC;\r
2291 DOWN;\r
2292 REWRITE_TAC[e_prime; IN_ELIM_THM];\r
2293 UNDISCH_TAC `FAN (v:real^3, V,E) `;\r
2294 REWRITE_TAC[FAN; graph; HAS_SIZE];\r
2295 STRIP_TAC THEN STRIP_TAC;\r
2296 UNDISCH_TAC ` {v',w:real^3} IN E `;\r
2297 REWRITE_TAC[IN];\r
2298 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2299 FIRST_X_ASSUM NHANH;\r
2300 REWRITE_TAC[Geomdetail.CARD2];\r
2301 SIMP_TAC[];\r
2302 SUBGOAL_THEN ` ff_of_hyp (v:real^3,v_prime V FF,e_prime E FF) x = x ` MP_TAC;\r
2303 DOWN;\r
2304 SIMP_TAC[ff_of_hyp3];\r
2305 PAT_ONCE_REWRITE_TAC `\x. x ==> i ` [orbit_one_point];\r
2306 REWRITE_TAC[ETA_AX];\r
2307 UNDISCH_TAC ` FF = face (hypermap hy) (x:real^3 # real^3 )`;\r
2308 UNDISCH_TAC ` FAN (v:real^3,v_prime V FF,e_prime E FF)`;\r
2309 EXPAND_TAC "hy";\r
2310 REWRITE_TAC[face];\r
2311 SIMP_TAC[GSYM ELMS_OF_HYPERMAP_HYP];\r
2312 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2313 SIMP_TAC[];\r
2314 NHANH (MESON[CARD_SINGLETON]` {p} = FF ==> CARD FF = 1 `);\r
2315 REPEAT STRIP_TAC;\r
2316 UNDISCH_TAC ` CARD (FF:real^3#real^3->bool) = 1 `;\r
2317 UNDISCH_TAC ` 2 < CARD (FF:real^3#real^3->bool) `;\r
2318 ARITH_TAC;\r
2319 \r
2320 EXPAND_TAC "hy";\r
2321 MP_TAC2 IMP_FAN_V_PRIME_E_PRIME;\r
2322 ASM_MESON_TAC[ELMS_OF_HYPERMAP_HYP];\r
2323 \r
2324 NHANH FAN_DART_DARTS;\r
2325 SIMP_TAC[];\r
2326 STRIP_TAC;\r
2327 CONJ_TAC;\r
2328 MATCH_MP_TAC IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME;\r
2329 ASM_REWRITE_TAC[face_refl];\r
2330 DOWN THEN DOWN;\r
2331 \r
2332 \r
2333 \r
2334 FIRST_X_ASSUM (ASSUME_TAC o SYM);\r
2335 UNDISCH_TAC ` FF = face (hypermap (HYP ((v:real^3),V,E))) x`;\r
2336 DISCH_THEN (ASSUME_TAC o SYM);\r
2337 ASM_REWRITE_TAC[];\r
2338 MP_TAC2 FF_DISJOINT_ITS_IMAGE_CARD_EQ;\r
2339 MP_TAC2 IMP_FAN_V_PRIME_E_PRIME;\r
2340 \r
2341 \r
2342 ASM_MESON_TAC[ELMS_OF_HYPERMAP_HYP; face_refl];\r
2343 NHANH ELMS_OF_HYPERMAP_HYP;\r
2344 \r
2345 ASM_SIMP_TAC[];\r
2346 EXPAND_TAC "hy";\r
2347 SIMP_TAC[];\r
2348 REPEAT STRIP_TAC;\r
2349 ABBREV_TAC ` nn = nn_of_hyp (v,v_prime V FF, e_prime E FF)`;\r
2350 MP_TAC2 LOCALIZE_PRESERVE_FACE;\r
2351 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2352 DISCH_THEN (ASSUME_TAC o SYM);\r
2353 FIRST_ASSUM ( fun x -> PAT_ONCE_REWRITE_TAC `\x. c = a UNION x ` [GSYM x]);\r
2354 PAT_ONCE_REWRITE_TAC `\x. c = a UNION x ` [ENF_IMAGE_ITSELF];\r
2355 ASM_REWRITE_TAC[GSYM IMAGE_o];\r
2356 \r
2357 \r
2358 \r
2359 MP_TAC2 FAN_FACE_GT1_IMAGE_EE_OF_HYP;\r
2360 DOWN THEN DOWN;\r
2361 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2362 ASM_SIMP_TAC[ARITH_RULE` 2 < a ==> 1 < a `];\r
2363 \r
2364 STRIP_TAC;\r
2365 MP_TAC2 CARD_GT1_EE_OF_HYP_E_PRIME_EQ;\r
2366 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2367 DOWN THEN DOWN THEN DOWN THEN PHA THEN REMOVE_TAC;\r
2368 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2369 ASM_SIMP_TAC[ARITH_RULE` 2 < c ==> 1 < c`];\r
2370 NHANH IDE_ON_S_IMP_SAME_IMAGE;\r
2371 SIMP_TAC[ETA_AX];\r
2372 STRIP_TAC;\r
2373 \r
2374 MATCH_MP_TAC (MESON[]` a = x ==> f a = f x `);\r
2375 MATCH_MP_TAC (MESON[]` a = x ==> IMAGE a S = IMAGE x S `);\r
2376 UNDISCH_TAC `FAN (v:real^3,v_prime V FF,e_prime E FF) `;\r
2377 NHANH FIRST_AAUHTVE2;\r
2378 ASM_REWRITE_TAC[];\r
2379 ABBREV_TAC ` e = ee_of_hyp (v:real^3,v_prime V FF,e_prime E FF) `;\r
2380 ABBREV_TAC ` f = ff_of_hyp (v:real^3,v_prime V FF,e_prime E FF) `;\r
2381 ASM_REWRITE_TAC[];\r
2382 NHANH (MESON[]` e o x = I /\ e o e = I ==> e o e o x = e o I `);\r
2383 REWRITE_TAC[I_O_ID; o_ASSOC];\r
2384 PHA;\r
2385 REWRITE_TAC[MESON[]` x = y /\ (x o t ) o i = p <=> \r
2386 x = y /\ (y o t ) o i = p`; I_O_ID];\r
2387 SIMP_TAC[EQ_SYM_EQ]]);;\r
2388 \r
2389 \r
2390 \r
2391 \r
2392 \r
2393 let LVDUCXU = prove_by_refinement\r
2394 (` FAN ((vec 0):real^3,V,E) /\\r
2395 x IN darts_of_hyp E V /\\r
2396 FF = face (hypermap (HYP (vec 0,V,E))) x \r
2397 ==> FF = face (hypermap (HYP (vec 0,v_prime V FF,e_prime E FF))) x /\\r
2398 (! x. x IN FF ==> azim_in_fan x E = azim_in_fan x (e_prime E FF ) /\\r
2399 wedge_in_fan_ge x E = wedge_in_fan_ge x (e_prime E FF) /\\r
2400 wedge_in_fan_gt x E = wedge_in_fan_gt x (e_prime E FF)) /\\r
2401 ( 2 < CARD FF /\ \r
2402 simple_hypermap (hypermap (HYP (vec 0,v_prime V FF,e_prime E FF))) ==>\r
2403 local_fan (v_prime V FF,e_prime E FF,FF) ) `,\r
2404 [STRIP_TAC;\r
2405 CONJ_TAC;\r
2406 MATCH_MP_TAC LOCALIZE_PRESERVE_FACE;\r
2407 ASM_REWRITE_TAC[];\r
2408 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2409 CONJ_TAC;\r
2410 GEN_TAC THEN STRIP_TAC;\r
2411 CONJ_TAC;\r
2412 MATCH_MP_TAC (SPEC `x:real^3 # real^3 ` (GEN `v:real^3 # real^3 ` AZIM_IN_FAN_EQ_IZIM_E_PRIME));\r
2413 ASM_REWRITE_TAC[];\r
2414 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2415 MATCH_MP_TAC (SPEC `x:real^3 # real^3 ` (GEN `v:real^3 # real^3 `\r
2416  WEDGE_IN_FAN_EQ_WITH_E_PRIME));\r
2417 ASM_REWRITE_TAC[];\r
2418 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2419 REWRITE_TAC[local_fan];\r
2420 STRIP_TAC;\r
2421 LET_TAC;\r
2422 MP_TAC2 (\r
2423 SPEC `(vec 0): real^3 ` (GEN `v:real^3` IMP_FAN_V_PRIME_E_PRIME));\r
2424 EXISTS_TAC `x:real^3 # real^3 `;\r
2425 REWRITE_TAC[];\r
2426 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2427 \r
2428 \r
2429 \r
2430 \r
2431 STRIP_TAC;\r
2432 CONJ_TAC;\r
2433 EXISTS_TAC ` x:real^3 # real^3 `;\r
2434 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2435 DOWN THEN SIMP_TAC[FAN_DART_DARTS];\r
2436 STRIP_TAC;\r
2437 MP_TAC2 (\r
2438 ISPEC `x:real^3 # real^3 ` (GEN `x:A#A`\r
2439  IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME));\r
2440 ASM_SIMP_TAC[GSYM FAN_DART_DARTS; face_refl];\r
2441 DISCH_TAC THEN MATCH_MP_TAC LOCALIZE_PRESERVE_FACE;\r
2442 ASM_SIMP_TAC[FAN_DART_DARTS];\r
2443 EXPAND_TAC "H";\r
2444 MATCH_MP_TAC DIH_K_HYP_E_PRIME;\r
2445 ASM_REWRITE_TAC[]]);;\r
2446 \r
2447 \r
2448 end;;\r
2449 \r
2450 (* ______________________________________________________________\r
2451 _________________________________________________________________ \r
2452 flyspeck_needs "general/update_database_310.ml";;\r
2453 \r
2454 \r
2455 *)\r