text_formalization/local/WRGCVDR_CIZMRRH.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Definitions:                                                               *)\r
   5 (* Chapter: Local Fan                                                         *)\r
   6 (* Author: Truong Nguyen Quang                                                *)\r
   7 (* Date: 2010-03 - 30                                                         *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 \r
  11 (* needs "/home/user1/flyspeck/working/flyspeck_needs.hl";; *) \r
  12 (* =========== snapshot 1631 ===================== *)\r
  13 \r
  14 \r
  15 let build_sequence = \r
  16   ["general/sphere.hl";\r
  17    "general/prove_by_refinement.hl";\r
  18    "trigonometry/trig1.hl";\r
  19    "trigonometry/trig2.hl";\r
  20    "hypermap/hypermap.hl"; \r
  21    "fan/introduction.hl"; \r
  22    "fan/topology.hl"];;\r
  23 \r
  24 map flyspeck_needs build_sequence;;\r
  25 \r
  26 \r
  27 module type Wrgcvdr_cizmrrh = sig \r
  28 \r
  29 end;;\r
  30 \r
  31 module Wrgcvdr_cizmrrh = struct\r
  32 \r
  33 \r
  34 open Sphere;;\r
  35 open Trigonometry1;;\r
  36 open Trigonometry2;;\r
  37 open Hypermap;;\r
  38 open Fan;;\r
  39 open Topology;;\r
  40 open Prove_by_refinement;;\r
  41 \r
  42 \r
  43 let SET_TAC = let basicthms =\r
  44 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
  45 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
  46 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
  47 [IN_ELIM_THM; IN] in\r
  48 let PRESET_TAC =\r
  49 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
  50 REPEAT COND_CASES_TAC THEN\r
  51 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
  52 REWRITE_TAC allthms in\r
  53 fun ths ->\r
  54 PRESET_TAC THEN\r
  55 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
  56 MESON_TAC ths ;;\r
  57 \r
  58 (* =========== improved SET_RULE ============= *)\r
  59 let TR_SET_RULE a = fun x -> prove(x, SET_TAC a );;\r
  60 let SET_RULE tm = prove(tm,SET_TAC[]);; \r
  61 \r
  62 \r
  63 let all_hy_map = let t1 = CONJ dart edge_map in\r
  64 let t2 = CONJ t1 node_map in\r
  65 CONJ t2 face_map;;\r
  66 \r
  67 \r
  68 \r
  69 let SPEC_HY_ELEMS = prove_by_refinement(\r
  70 `! (H: (A)hypermap) . tuple_hypermap H = (D,e,n,f) <=>\r
  71 dart H = D /\ edge_map H = e /\ node_map H = n /\ face_map H = f `,\r
  72 [ REWRITE_TAC[dart; all_hy_map];\r
  73 GEN_TAC THEN EQ_TAC;\r
  74 SIMP_TAC[FST; SND; PAIR];\r
  75 DISCH_TAC;\r
  76 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  77 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[];\r
  78 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  79 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[];\r
  80 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  81 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[]]);;\r
  82 \r
  83 (* =============================== *)\r
  84 (* =============================== *)\r
  85 \r
  86 let hypermap = prove_by_refinement(\r
  87 `! H: (A) hypermap. tuple_hypermap H = D,e,n,f ==>\r
  88 e permutes D /\ n permutes D /\ f permutes D /\ e o n o f = I `,\r
  89 [REWRITE_TAC[SPEC_HY_ELEMS];\r
  90 GEN_TAC THEN MP_TAC (SPEC_ALL hypermap_lemma);\r
  91 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `];\r
  92 SIMP_TAC[]]);;\r
  93 \r
  94 \r
  95 parse_as_infix("has_orders",(12,"right"));;\r
  96 parse_as_infix("cyclic_on",(13,"right"));;\r
  97 \r
  98 let has_orders = new_definition ` (f: A -> A) has_orders k <=>\r
  99 (! i. 0 < i /\ i < k ==> ~( ITER i f = I )) /\\r
 100 ITER k f = I `;;\r
 101 \r
 102 let cyclic_on = new_definition` f cyclic_on (S:A -> bool) <=>\r
 103 (! x. x IN S ==> S = {z | ?n. z = ITER n f x }) `;;\r
 104 \r
 105 \r
 106 let dih2k = new_definition` dih2k (H: (A) hypermap) k <=> \r
 107 CARD (dart H) = 2 * k\r
 108 /\ (! x. x IN (dart H) ==> let S = face H x in \r
 109          dart H = S UNION (IMAGE (node_map H) S ))\r
 110 /\ (face_map H ) has_orders k /\\r
 111 (edge_map H ) has_orders 2 /\\r
 112 (node_map H) has_orders 2 `;;\r
 113 \r
 114 \r
 115 let EE = new_definition` EE v S = {w | {v,w} IN S }`;;\r
 116 \r
 117 let ord_pairs = new_definition` ord_pairs E = { a,b | {a,b} IN E } `;;\r
 118 \r
 119 let self_pairs = new_definition` self_pairs E V = { (v,v) | v IN V /\\r
 120  EE v E = {} } `;;\r
 121 \r
 122 let darts_of_hyp = new_definition` darts_of_hyp E V = ord_pairs E UNION \r
 123 self_pairs E V `;;\r
 124 \r
 125 let ee_of_hyp = new_definition` ee_of_hyp (x,V,E) ((a:real^3),(b:real^3)) = \r
 126 if (a,b) IN darts_of_hyp E V then (b,a) else (a,b)`;;\r
 127 \r
 128 let ee_of_hyp2 = prove(` ee_of_hyp (x,V,E) u = \r
 129 if u IN darts_of_hyp E V then (SND u, FST u) else u `,\r
 130 PAT_ONCE_REWRITE_TAC `\x. f x = y ` [GSYM PAIR] THEN \r
 131 PURE_REWRITE_TAC[ee_of_hyp] THEN REWRITE_TAC[]);;\r
 132 \r
 133 let nn_of_hyp = new_definition` nn_of_hyp (x,V,E) (v,u) =\r
 134 if (v,u) IN darts_of_hyp E V then\r
 135 (v, azim_cycle (EE v E) x v u) else (v,u)`;;\r
 136 \r
 137 \r
 138 \r
 139 let nn_of_hyp2 = prove(` nn_of_hyp (x,V,E) u = \r
 140 if u IN darts_of_hyp E V then\r
 141 (FST u, azim_cycle (EE (FST u) E) x (FST u) (SND u)) else u `,\r
 142 PAT_ONCE_REWRITE_TAC `\x. f x = y ` [GSYM PAIR] THEN \r
 143 PURE_REWRITE_TAC[nn_of_hyp] THEN REWRITE_TAC[]);;\r
 144 \r
 145 \r
 146 let ivs_azim_cycle = new_definition`ivs_azim_cycle W v0 v w =\r
 147 if W = {} then w else \r
 148 (@x. x IN W /\ azim_cycle W v0 v x = w ) `;;\r
 149 \r
 150 let ff_of_hyp = new_definition` ff_of_hyp (x,V,E) (v,u) =\r
 151 if (v,u) IN darts_of_hyp E V then\r
 152 (u, ivs_azim_cycle (EE u E) x u  v) else (v,u)`;;\r
 153 \r
 154 let ff_of_hyp2 = prove(` ff_of_hyp (x,V,E) u = \r
 155 if u IN darts_of_hyp E V then\r
 156 (SND u, ivs_azim_cycle (EE (SND u) E) x (SND u)  (FST u)) else u`,\r
 157 PAT_ONCE_REWRITE_TAC `\x. f x = y ` [GSYM PAIR] THEN \r
 158 PURE_REWRITE_TAC[ff_of_hyp] THEN REWRITE_TAC[]);;\r
 159 \r
 160 let HYP = new_definition` HYP (x,V,E) = (darts_of_hyp E V,\r
 161 ee_of_hyp (x,V,E), nn_of_hyp (x,V,E), ff_of_hyp (x,V,E)) `;;\r
 162 \r
 163 \r
 164 let local_fan = new_definition ` local_fan (V,E,FF ) <=>\r
 165  let H = hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) in\r
 166   FAN (vec 0, V, E) /\\r
 167   (?x. x IN ( dart H) /\ FF = face H x ) /\\r
 168 dih2k H (CARD FF ) `;;\r
 169 \r
 170 \r
 171 let azim_in_fan = new_definition` azim_in_fan (v:real^3,w:real^3) E = \r
 172 let d = (azim_cycle (EE v E) ( vec 0 ) v w) in\r
 173  if CARD ( EE v E ) > 1 then \r
 174  azim (vec 0 ) v w d else &2 * pi `;;\r
 175 \r
 176 let wedge_in_fan_gt = new_definition`wedge_in_fan_gt (v,w) E = \r
 177   if CARD (EE v E) > 1 then\r
 178 wedge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else if \r
 179 EE v E = {w} then { x | ~ ( x IN aff_ge {vec 0, v} {w} ) } else\r
 180 { x | ~ ( x IN aff {vec 0, v} )} `;;\r
 181 \r
 182 let wedge_ge = new_definition `wedge_ge  v0 v1 w1 w2 = { z |\r
 183 &0 <= azim v0 v1 w1 z /\ azim v0 v1 w1 z <= azim v0 v1 w1 w2 }`;;\r
 184 \r
 185 let wedge_in_fan_ge = new_definition` wedge_in_fan_ge ((v:real^3),w) E = \r
 186   if CARD (EE v E) > 1 then\r
 187 wedge_ge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else { x:real^3 | T } `;;\r
 188 \r
 189 let convex_local_fan = new_definition\r
 190   `convex_local_fan (V,E,FF) <=>\r
 191    local_fan (V,E,FF) /\\r
 192    (!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E)`;;\r
 193 \r
 194 let FST_SND_FORM_OF_4_TUPLE = GEN_ALL (\r
 195 prove_by_refinement(` FST X = D /\ FST (SND X) = e /\ \r
 196 FST (SND (SND X)) = n /\ SND (SND (SND X)) = f <=> X = D,e,n,f `,\r
 197 [EQ_TAC;\r
 198 STRIP_TAC;\r
 199 REPEAT (PAT_ONCE_REWRITE_TAC `\x. x = y `[GSYM PAIR] THEN\r
 200  ASM_SIMP_TAC[PAIR_EQ]);\r
 201 SIMP_TAC[PAIR_EQ]]));;\r
 202 (* =================================================== *)\r
 203 \r
 204 \r
 205 \r
 206 let V_IN_DARTS_IFF_E_V_IN_DARTS = prove_by_refinement\r
 207 (`v IN darts_of_hyp E V <=> ee_of_hyp (x,V,E) v IN darts_of_hyp E V `,\r
 208 [EQ_TAC;\r
 209 REWRITE_TAC[ee_of_hyp2];\r
 210 SIMP_TAC[darts_of_hyp; IN_UNION; ord_pairs; self_pairs];\r
 211 DISCH_THEN DISJ_CASES_TAC;\r
 212 DISJ1_TAC;\r
 213 DOWN;\r
 214 REWRITE_TAC[IN_ELIM_THM];\r
 215 STRIP_TAC;\r
 216 ASM_SIMP_TAC[];\r
 217 EXISTS_TAC `b:real^3 `;\r
 218 EXISTS_TAC `a:real^3 `;\r
 219 ASM_SIMP_TAC[INSERT_COMM];\r
 220 DISJ2_TAC;\r
 221 DOWN THEN REWRITE_TAC[IN_ELIM_THM];\r
 222 STRIP_TAC;\r
 223 EXISTS_TAC `v':real^3 `;\r
 224 ASM_SIMP_TAC[];\r
 225 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
 226 SIMP_TAC[ee_of_hyp2]]);;\r
 227 \r
 228 \r
 229 \r
 230 \r
 231 let V_IN_DARTS_IMP_SWICH_SO_DO = prove_by_refinement\r
 232 (` (v:A#A) IN darts_of_hyp E V ==> SND v, FST v IN darts_of_hyp E V `,\r
 233 [REWRITE_TAC[darts_of_hyp; ord_pairs; self_pairs; IN_UNION; IN_ELIM_THM];\r
 234 STRIP_TAC;\r
 235 DISJ1_TAC;\r
 236 EXISTS_TAC `b:A `;\r
 237 EXISTS_TAC `a:A`;\r
 238 ASM_SIMP_TAC[INSERT_COMM];\r
 239 DISJ2_TAC;\r
 240 EXISTS_TAC ` v':A`;\r
 241 ASM_SIMP_TAC[]]);;\r
 242 let V_IN_DARTS_IFF_SWICH_SO_DO = V_IN_DARTS_IMP_SWICH_SO_DO;;\r
 243 \r
 244 \r
 245 (* removed, 2011-08-01, `fan` deprecated, thales\r
 246 let fan_expand = let t1 = CONJ fan fan1 in\r
 247 let t2 = CONJ fan2 t1 in\r
 248 let t3 = CONJ fan3 t2 in\r
 249 let t4 = CONJ fan4 t3 in\r
 250 let t5 = CONJ fan5 t4 in\r
 251 let t6 = CONJ fan6 t5 in\r
 252 let t7 = CONJ fan7 t6 in\r
 253 CONJ FAN t7;;\r
 254 *)\r
 255 \r
 256 \r
 257 \r
 258 \r
 259 \r
 260 \r
 261 let IN_V_OF_FAN_EXISTS_DART = GEN_ALL (\r
 262 prove_by_refinement(\r
 263 ` UNIONS E SUBSET (V:real^3 -> bool) /\ u IN V ==> \r
 264      ? v. v IN V /\ (u,v) IN darts_of_hyp E V `,\r
 265 [REWRITE_TAC[darts_of_hyp; IN_UNION; ord_pairs; self_pairs];\r
 266 PHA THEN DAO THEN STRIP_TAC THEN ASM_CASES_TAC `?(v:real^3). {u,v} IN E `;\r
 267 (* Subgoal 1 *)\r
 268 FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `v:real^3 `;\r
 269 ASSUME_TAC2 (prove(` UNIONS E SUBSET V /\ {(u:real^3), v} IN E ==> v IN V `,\r
 270 REWRITE_TAC[ UNIONS_SUBSET] THEN \r
 271 STRIP_TAC THEN \r
 272 MATCH_MP_TAC (TR_SET_RULE[]` {u,v} SUBSET V ==> v IN V `) THEN \r
 273 FIRST_X_ASSUM MATCH_MP_TAC THEN \r
 274 ASM_SIMP_TAC[]));\r
 275 ASM_REWRITE_TAC[] THEN EVERY_ASSUM (fun x -> SET_TAC[x]);\r
 276 (* Subgoal 2 *)\r
 277 EXISTS_TAC `u:real^3 ` THEN ASM_REWRITE_TAC[EE];\r
 278 DISJ2_TAC THEN FIRST_X_ASSUM MP_TAC THEN SET_TAC[]]));;\r
 279 \r
 280 \r
 281 \r
 282 \r
 283 \r
 284 \r
 285 let X_IN_ITS_ORBIT = prove(` (x:A) IN orbit_map f x `,\r
 286 REWRITE_TAC[orbit_map; IN_ELIM_THM] THEN \r
 287 EXISTS_TAC ` 0 ` THEN REWRITE_TAC[POWER; I_THM; GE_REFL]);;\r
 288 \r
 289 let X_IN_HYP_ORBITS = prove(`! (x:A). x IN edge H x /\ x IN node H x /\ x IN face H x `,\r
 290 REWRITE_TAC[node; edge; face; X_IN_ITS_ORBIT]);;\r
 291 \r
 292 \r
 293 \r
 294 \r
 295 \r
 296 prove(` UNIONS E SUBSET V /\ {a, b} IN E ==> a IN V /\ b IN V `,\r
 297 REWRITE_TAC[UNIONS_SUBSET;\r
 298 (GSYM o (TR_SET_RULE[]))` {a,b} SUBSET V <=> a IN V /\ b IN V `] THEN \r
 299 MESON_TAC[]);;\r
 300 \r
 301 \r
 302 \r
 303 let IN_DARTS_HYP_IMP_FST_SND_IN_V = prove_by_refinement\r
 304 (`UNIONS E SUBSET V /\ (y:A#A) IN darts_of_hyp E V ==> FST y IN V /\ SND y IN V `,\r
 305 [SIMP_TAC[darts_of_hyp; ord_pairs; self_pairs; IN_UNION; IN_ELIM_THM];\r
 306 STRIP_TAC;\r
 307 (* sub 1 *)\r
 308 ASM_SIMP_TAC[];\r
 309 MATCH_MP_TAC (prove(` UNIONS E SUBSET V /\ {a, b} IN E ==> a IN V /\ b IN V `,\r
 310 REWRITE_TAC[UNIONS_SUBSET;\r
 311 (GSYM o (TR_SET_RULE[]))` {a,b} SUBSET V <=> a IN V /\ b IN V `] THEN \r
 312 MESON_TAC[]));\r
 313 ASM_SIMP_TAC[];\r
 314 (* sub 2 *)\r
 315 ASM_SIMP_TAC[FST; SND]]);;\r
 316 \r
 317 \r
 318 \r
 319 let POWER_SND = prove_by_refinement\r
 320 (`!n. f POWER SUC n = f o (f POWER n)`,\r
 321 [INDUCT_TAC;\r
 322 REWRITE_TAC[POWER; FUN_EQ_THM; o_THM; I_THM];\r
 323 DOWN THEN SIMP_TAC[POWER; FUN_EQ_THM; o_THM]]);;\r
 324 \r
 325 \r
 326 let POWER_TO_ITER = prove(`! n. (f POWER n) = ITER n f `,\r
 327 INDUCT_TAC THENL [\r
 328 REWRITE_TAC[POWER; ITER; FUN_EQ_THM; I_THM];\r
 329 ASM_REWRITE_TAC[POWER_SND; ITER; FUN_EQ_THM; o_THM]]);;\r
 330 \r
 331 \r
 332 let SND_IN_SET_OF_DART_OF_FRST = prove(\r
 333 ` UNIONS (E:(A -> bool) -> bool) SUBSET (V:A -> bool) /\ y IN darts_of_hyp E V ==> \r
 334 FST y = SND y \/ SND y IN set_of_edge (FST y) V E`,\r
 335 REWRITE_TAC[set_of_edge; darts_of_hyp; ord_pairs; \r
 336 self_pairs; IN_ELIM_THM; IN_UNION] THEN\r
 337 STRIP_TAC THENL [\r
 338 ASM_SIMP_TAC[] THEN \r
 339 DISJ2_TAC THEN \r
 340 ASM_MESON_TAC[prove(` UNIONS E SUBSET V /\ {(u:A), v} IN E ==> v IN V `,\r
 341 REWRITE_TAC[ UNIONS_SUBSET] THEN \r
 342 STRIP_TAC THEN \r
 343 MATCH_MP_TAC (TR_SET_RULE[]` {u,v} SUBSET V ==> v IN V `) THEN \r
 344 FIRST_X_ASSUM MATCH_MP_TAC THEN \r
 345 ASM_SIMP_TAC[])];\r
 346 ASM_SIMP_TAC[]]);;\r
 347 \r
 348 \r
 349 \r
 350 let UNI_E_IMP_EE_EQ_SET_OF_EDGE = \r
 351 prove(` UNIONS E SUBSET V ==> EE (v:A) E = set_of_edge v V E `,\r
 352 REWRITE_TAC[EE; set_of_edge] THEN \r
 353 REWRITE_TAC[UNIONS_SUBSET; FUN_EQ_THM; IN_ELIM_THM]\r
 354 THEN REWRITE_TAC[MESON[]`( a <=> a /\ b ) <=> a ==> b `] \r
 355 THEN REPEAT STRIP_TAC\r
 356 THEN MATCH_MP_TAC (TR_SET_RULE[]` {v:A,b} SUBSET V ==> b IN V `)\r
 357 THEN ASM_MESON_TAC[]);;\r
 358 \r
 359 \r
 360 \r
 361 let types_in_th th = let t = frees (concl (SPEC_ALL th)) in\r
 362   map dest_var t;;\r
 363 \r
 364 \r
 365 let IN_ORD_PAIRS_IMP_IMP_IN_TOO = \r
 366 prove_by_refinement(\r
 367 `y IN ord_pairs E ==> ((FST y):A,d) IN darts_of_hyp E V ==>\r
 368   ((FST y),d) IN ord_pairs E `,\r
 369 [REWRITE_TAC[ord_pairs; darts_of_hyp; \r
 370 self_pairs; IN_ELIM_THM] THEN \r
 371 REPEAT STRIP_TAC;\r
 372 (* sub 1 *)\r
 373 EXISTS_TAC `FST (y:A#A)` THEN \r
 374 EXISTS_TAC `d: A` THEN \r
 375 DOWN;\r
 376 REWRITE_TAC[IN_UNION; IN_ELIM_THM];\r
 377 STRIP_TAC;\r
 378 DOWN_TAC;\r
 379 SIMP_TAC[PAIR_EQ];\r
 380 (* sub 2 *)\r
 381 DOWN_TAC;\r
 382 IMP_TAC THEN IMP_TAC THEN SIMP_TAC[];\r
 383 SIMP_TAC[EE; PAIR_EQ]; SET_TAC[]]);;\r
 384 \r
 385 \r
 386 \r
 387 \r
 388 let IN_ORD_PAIRS_IMP_SND_IN_EE_FST = prove(\r
 389 `y IN ord_pairs E ==> SND y IN (EE (FST y) E) `   ,\r
 390 REWRITE_TAC[ord_pairs; EE; IN_ELIM_THM]\r
 391 THEN STRIP_TAC \r
 392 THEN ASM_SIMP_TAC[]);;\r
 393 \r
 394 \r
 395 \r
 396 \r
 397 \r
 398 \r
 399 \r
 400 \r
 401 \r
 402 let IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL = \r
 403 prove_by_refinement(\r
 404 `! (v:A). y IN self_pairs E V /\ FST y,v IN darts_of_hyp E V ==> FST y = v`,\r
 405 [GEN_TAC THEN REWRITE_TAC[self_pairs; darts_of_hyp];\r
 406 REWRITE_TAC[IN_ELIM_THM; ord_pairs; IN_UNION; EE];\r
 407 STRIP_TAC;\r
 408 DOWN;\r
 409 ASM_SIMP_TAC[PAIR_EQ];\r
 410 STRIP_TAC;\r
 411 ASM SET_TAC[];\r
 412 DOWN THEN SIMP_TAC[PAIR_EQ]]);;\r
 413 \r
 414 \r
 415 \r
 416 let choose_nd_point = new_specification ["choose_nd_point"]\r
 417   (REWRITE_RULE[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] IN_V_OF_FAN_EXISTS_DART);;\r
 418 \r
 419 (* ============================ *)\r
 420 \r
 421 \r
 422 let ITER_N_I = prove(`! n. ITER n I = I`,\r
 423 INDUCT_TAC THENL [\r
 424 REWRITE_TAC[ITER; FUN_EQ_THM; I_THM];\r
 425 ASM_REWRITE_TAC[ITER; FUN_EQ_THM; I_THM]]);;\r
 426 \r
 427 \r
 428 \r
 429 \r
 430 \r
 431 \r
 432 let HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW = \r
 433 prove_by_refinement(\r
 434 `(f: A -> A) has_orders k /\ ~ (k = 0 ) ==>\r
 435 (! x. orbit_map f x = { y| ? n. 0 <= n /\ n < k /\ y = ITER n f x }) `,\r
 436 [ REWRITE_TAC[has_orders; orbit_map; POWER_TO_ITER];\r
 437 REWRITE_TAC[FUN_EQ_THM];\r
 438 REPEAT STRIP_TAC;\r
 439 REWRITE_TAC[IN_ELIM_THM];\r
 440 EQ_TAC;\r
 441 STRIP_TAC;\r
 442 EXISTS_TAC `n MOD k `;\r
 443 ASM_SIMP_TAC[LE_0; DIVISION];\r
 444 ASSUME_TAC2 (SPECL [` n: num `;` k:num `] DIVISION);\r
 445 FIRST_X_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC `\x. x = y ` [x]);\r
 446 REWRITE_TAC[GSYM ITER_ADD; GSYM ITER_MUL];\r
 447 UNDISCH_TAC `!x. ITER k (f: A -> A) x = I x`;\r
 448 SIMP_TAC[GSYM FUN_EQ_THM; ETA_AX; ITER_N_I; I_THM];\r
 449 STRIP_TAC;\r
 450 REWRITE_TAC[ARITH_RULE` n >= 0 `];\r
 451 EXISTS_TAC `n: num `;\r
 452 ASM_REWRITE_TAC[]]);;\r
 453 \r
 454 \r
 455 \r
 456 let FINITE_OF_N_FIRST_ELMS = \r
 457 prove_by_refinement(\r
 458 `! k (x:A). FINITE {y | ?n. n < k /\ y = ITER n f x}`,\r
 459 [INDUCT_TAC;\r
 460 REWRITE_TAC[ ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; FINITE_EMPTY];\r
 461 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 462 KHANANG;\r
 463 REWRITE_TAC[TR_SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 464   UNION { y | ? n. Q n y } `];\r
 465 DOWN;\r
 466 REWRITE_TAC[LE_0; TR_SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 467 SIMP_TAC[FINITE_UNION; FINITE_SINGLETON]]);;\r
 468 \r
 469 \r
 470 \r
 471 \r
 472 \r
 473 let F_HAS_ORDERS_IMP_FINITE_ORBIT = \r
 474 prove_by_refinement(\r
 475 ` (f: A -> A) has_orders k /\ ~( k = 0 ) ==>\r
 476 (! x. FINITE (orbit_map f x )) `,\r
 477 [NHANH HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW;\r
 478 SIMP_TAC[] THEN STRIP_TAC;\r
 479 SPEC_TAC (`k:num `,` k:num`);\r
 480 INDUCT_TAC;\r
 481 REWRITE_TAC[ ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; FINITE_EMPTY];\r
 482 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 483 KHANANG;\r
 484 REWRITE_TAC[TR_SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 485   UNION { y | ? n. Q n y } `];\r
 486 DOWN;\r
 487 REWRITE_TAC[LE_0; TR_SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 488 SIMP_TAC[FINITE_UNION; FINITE_SINGLETON]]);;\r
 489 \r
 490 \r
 491 \r
 492 \r
 493 \r
 494 \r
 495 \r
 496 let CARD_CLAUSES2 = prove(`FINITE (S: A -> bool) \r
 497  ==> (!x. x IN S ==> CARD (x INSERT S) = CARD S) /\\r
 498      (!x. ~(x IN S) ==> CARD (x INSERT S) = SUC (CARD S))`,\r
 499 SIMP_TAC[CARD_CLAUSES]);;\r
 500 \r
 501 \r
 502 let CARD_INSERT_GE_AND_LE = prove(\r
 503 `FINITE (S: A -> bool) ==> CARD S <= CARD (x INSERT S ) /\\r
 504 CARD (x INSERT S) <= SUC ( CARD S)`,\r
 505 SIMP_TAC[CARD_CLAUSES] THEN \r
 506 COND_CASES_TAC THENL [\r
 507 DISCH_TAC THEN ARITH_TAC;\r
 508 DISCH_TAC THEN ARITH_TAC]);;\r
 509 \r
 510 \r
 511 \r
 512 \r
 513 \r
 514 let HAVING_ORDERS_K_IMP_CARD_ORBIT_LE_K = \r
 515 prove_by_refinement(\r
 516 `(f: A -> A) has_orders k /\ ~( k = 0 ) ==>\r
 517 (! x. CARD (orbit_map f x) <= k )`,\r
 518 [SIMP_TAC[HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW ];\r
 519 STRIP_TAC;\r
 520 SPEC_TAC (`k: num `,` k: num`);\r
 521 INDUCT_TAC;\r
 522 REWRITE_TAC[LE_0; ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; CARD_CLAUSES];\r
 523 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 524 GEN_TAC;\r
 525 KHANANG;\r
 526 REWRITE_TAC[TR_SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 527   UNION { y | ? n. Q n y } `];\r
 528 DOWN;\r
 529 REWRITE_TAC[LE_0; TR_SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 530 SIMP_TAC[TR_SET_RULE[]` a UNION {x} = x INSERT a `];\r
 531 MP_TAC (SPECL [`k' :num `;`x: A `] FINITE_OF_N_FIRST_ELMS);\r
 532 NHANH (ISPEC ` ITER k' f (x:A) ` ( GEN `x :A ` CARD_INSERT_GE_AND_LE));\r
 533 STRIP_TAC THEN STRIP_TAC;\r
 534 FIRST_X_ASSUM (MP_TAC o (SPEC `x: A `));\r
 535 DOWN;\r
 536 ARITH_TAC]);;\r
 537 \r
 538 (* CARD_LE_K_OF_SET_K_FIRST_ELMS \r
 539 |- CARD {ITER i f x | i < k} <= k *)\r
 540 let CARD_LE_K_OF_SET_K_FIRST_ELMS = \r
 541 BETA_RULE (SPECL [`k: num `;`(\i. ITER i (f: A -> A) x )`] \r
 542 CARD_FINITE_SERIES_LE);;\r
 543 \r
 544 \r
 545 \r
 546 \r
 547 \r
 548 \r
 549 let CARD_K_FIRST_ELMS_EQ_K = \r
 550 prove_by_refinement(\r
 551 `! k (f: A -> A). CARD {ITER n f x | n < k} = k ==>\r
 552      CARD {ITER n f x | n < k - 1} = k - 1 /\\r
 553      (!i. i < k - 1 ==> ~(ITER i f x = ITER ( k - 1 ) f x))`,\r
 554 [INDUCT_TAC;\r
 555 REWRITE_TAC[ARITH_RULE ` ~( a < 0 - 1 ) `; LT];\r
 556 REWRITE_TAC[TR_SET_RULE[]` {ITER n f x | n | F} = {} `; CARD_CLAUSES];\r
 557 ARITH_TAC;\r
 558 GEN_TAC;\r
 559 REWRITE_TAC[ARITH_RULE ` a < SUC k <=> a < k  \/ a = k `];\r
 560 REWRITE_TAC[TR_SET_RULE[]` { ITER n f x | n < k \/ n = k } = ITER k f x INSERT { ITER n f x | n < k } `];\r
 561 ASM_CASES_TAC ` ITER k f (x:A) IN {ITER n f x | n < k} `;\r
 562 MP_TAC (SPEC_ALL FINITE_OF_N_FIRST_ELMS);\r
 563 REWRITE_TAC[TR_SET_RULE[]` {y | ?n. n < k /\ y = ITER n f x} = {ITER n f x | n < k} `];\r
 564 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_OF_N_FIRST_ELMS];\r
 565 DISCH_TAC THEN MP_TAC CARD_LE_K_OF_SET_K_FIRST_ELMS;\r
 566 ARITH_TAC;\r
 567 DOWN;\r
 568 MP_TAC (SPEC_ALL FINITE_OF_N_FIRST_ELMS);\r
 569 REWRITE_TAC[TR_SET_RULE[]` {y | ?n. n < k /\ y = ITER n f x} = {ITER n f x | n < k} `];\r
 570 SIMP_TAC[ARITH_RULE ` SUC k - 1 = k `; CARD_CLAUSES; SUC_INJ];\r
 571 DISCH_TAC;\r
 572 SET_TAC[]]);;\r
 573 \r
 574 \r
 575 let FINITENESS_OF_K_FIRST_ELMS = prove_by_refinement(\r
 576 `! k (f: num -> A). FINITE { f n | n < k }`,\r
 577 [INDUCT_TAC;\r
 578 REWRITE_TAC[LT; TR_SET_RULE[]` {f n | n | F } = {} `; FINITE_RULES];\r
 579 REWRITE_TAC[ARITH_RULE` n < SUC k <=> n < k \/ n = k `;\r
 580   TR_SET_RULE[]` {(f: num -> A) n | n < k \/ n = k} = f k INSERT {f n | n < k } `];\r
 581 ASM_REWRITE_TAC[FINITE_INSERT]]);;\r
 582 \r
 583 \r
 584 let LT_SUC_E = ARITH_RULE` i < SUC k <=> i < k \/ i = k `;;\r
 585 \r
 586 (* |- !k. CARD {f i | i < k} <= k *)\r
 587 let CARD_K_FIRST_ELMS_LE_K = \r
 588 GEN `k: num ` (SPECL [`k: num `;` f: num -> A `] CARD_FINITE_SERIES_LE);;\r
 589 \r
 590 \r
 591 \r
 592 let REMOVE_TAC = MATCH_MP_TAC (TAUT ` a ==> b ==> a `);;\r
 593 \r
 594 \r
 595 \r
 596 let CARD_N_FIRST_ELMS_UNDUCTIVE = prove_by_refinement(\r
 597 `! k (f: num -> A ). CARD { f n | n < k} = k <=>\r
 598     CARD {f n | n < k - 1} = k - 1 /\\r
 599      (!i. i < k - 1 ==> ~(f i = f ( k - 1 )))`,\r
 600 [REPEAT GEN_TAC;\r
 601 ASM_CASES_TAC ` k = 0 `;\r
 602 ASM_SIMP_TAC[ARITH_RULE` ~( x < 0 - 1 ) `; LT; ARITH_RULE` 0 - 1 = 0 `];\r
 603 DOWN;\r
 604 NHANH (ARITH_RULE` ~( k = 0 ) ==> (! n. n < k <=> n < k - 1 \/ n = k - 1 ) `);\r
 605 SIMP_TAC[];\r
 606 STRIP_TAC;\r
 607 REWRITE_TAC[TR_SET_RULE[]` {(f:num -> A) n | n < k - 1 \/ n = k - 1}\r
 608   = f ( k - 1 ) INSERT {f n | n < k - 1 }`];\r
 609 MP_TAC (SPECL [` k - 1 `;` f: num -> A `] FINITENESS_OF_K_FIRST_ELMS);\r
 610 DISCH_TAC;\r
 611 EQ_TAC;\r
 612 (* sub 1 *)\r
 613 ASM_SIMP_TAC[CARD_CLAUSES];\r
 614 COND_CASES_TAC;\r
 615 (* sub 1.1 *)\r
 616 MP_TAC (SPEC ` k - 1 ` CARD_K_FIRST_ELMS_LE_K);\r
 617 UNDISCH_TAC ` ~( k = 0 ) `;\r
 618 MESON_TAC[ARITH_RULE `~ ( ~(k = 0) /\ a <= k - 1 /\ a = k ) `];\r
 619 (* sub 1.2 *)\r
 620 UNDISCH_TAC ` ~( k = 0 ) `;\r
 621 SIMP_TAC[ARITH_RULE ` ~( k = 0 ) ==> ( SUC x = k <=> x = k - 1 )`];\r
 622 MATCH_MP_TAC (TAUT ` a ==> b ==> a `);\r
 623 MATCH_MP_TAC (TAUT ` a ==> b ==> a `);\r
 624 DOWN;\r
 625 REWRITE_TAC[IN_ELIM_THM];\r
 626 MESON_TAC[];\r
 627 (* SUB 2 *)\r
 628 STRIP_TAC;\r
 629 SUBGOAL_THEN ` ~( f ( k - 1 ) IN {(f: num -> A) n | n < k - 1})` ASSUME_TAC;\r
 630 DOWN THEN REWRITE_TAC[IN_ELIM_THM];\r
 631 MESON_TAC[];\r
 632 ASM_SIMP_TAC[CARD_CLAUSES];\r
 633 UNDISCH_TAC `~( k = 0 ) `;\r
 634 ARITH_TAC]);;\r
 635 \r
 636 \r
 637 \r
 638 \r
 639 \r
 640 let CARD_ADD1_LE = prove_by_refinement(\r
 641 `! f: num -> A. CARD { f n | n < k + 1 } <= CARD {f n | n < k } + 1 `,\r
 642 [REWRITE_TAC[ARITH_RULE` a < v + 1 <=> a < v \/ a = v `;\r
 643   TR_SET_RULE[]` {(f: num -> A) n | n < k \/ n = k} = f k INSERT {f n | n < k } `];\r
 644 GEN_TAC;\r
 645 MP_TAC (SPEC_ALL FINITENESS_OF_K_FIRST_ELMS);\r
 646 SIMP_TAC[CARD_CLAUSES];\r
 647 COND_CASES_TAC;\r
 648 DISCH_TAC THEN ARITH_TAC;\r
 649 DISCH_TAC THEN ARITH_TAC]);;\r
 650 \r
 651 \r
 652 \r
 653 \r
 654 \r
 655 let CARD_LT_KT_LE_ADDT = \r
 656 prove_by_refinement(\r
 657 ` CARD { (f: num -> A) n | n < k + t } <= CARD {f n | n < k } + t `,\r
 658 [SPEC_TAC (`t:num `,` t:num `);\r
 659 INDUCT_TAC;\r
 660 REWRITE_TAC[ADD_0; LE_REFL];\r
 661 REWRITE_TAC[ADD1];\r
 662 REWRITE_TAC[ARITH_RULE` a + b + 1 = (a + b ) + 1 `];\r
 663 MP_TAC (SPECL [` k + (t:num) `;` f: num -> A `] (GEN_ALL CARD_ADD1_LE));\r
 664 DOWN THEN ARITH_TAC]);;\r
 665 \r
 666 \r
 667 \r
 668 \r
 669 \r
 670 let CARD_KS_EQ_K_EQ_ALL_LE = prove_by_refinement\r
 671 (`! k (f: num -> A ). CARD { f n | n < k} = k <=>\r
 672 (! kk. kk <= k ==> CARD { f n | n < kk} = kk ) `,\r
 673 [REPEAT STRIP_TAC;\r
 674 EQ_TAC;\r
 675 REPEAT STRIP_TAC;\r
 676 ASM_CASES_TAC ` CARD {(f: num -> A) n | n < kk} = kk`;\r
 677 ASM_SIMP_TAC[];\r
 678 ASSUME_TAC (SPEC `kk: num ` CARD_K_FIRST_ELMS_LE_K );\r
 679 UNDISCH_TAC ` kk <= (k:num ) `;\r
 680 NHANH (ARITH_RULE` kk <= (k:num) ==> k = kk + k - kk`);\r
 681 STRIP_TAC;\r
 682 UNDISCH_TAC `CARD {(f:num -> A) n | n < k} = k`;\r
 683 FIRST_ASSUM (fun x -> ONCE_REWRITE_TAC[x]);\r
 684  MP_TAC (SPECL [`kk : num `;` f: num -> A `;` k - (kk: num ) `]\r
 685  (GEN_ALL CARD_LT_KT_LE_ADDT));\r
 686 REPEAT STRIP_TAC;\r
 687 UNDISCH_TAC `~(CARD {(f: num -> A) n | n < kk} = kk) `;\r
 688 UNDISCH_TAC ` CARD {(f: num -> A) i | i < kk} <= kk`;\r
 689 PHA;\r
 690 REWRITE_TAC[ARITH_RULE` a <= b /\ ~( a = b ) <=> a < (b: num) `];\r
 691 DOWN THEN DOWN;\r
 692 MESON_TAC[ARITH_RULE` ~( a <= b + c /\ a = kk + c /\ b < (kk: num) ) `];\r
 693 (* SUB 2 *)\r
 694 DISCH_THEN (MP_TAC o (SPEC `k: num `));\r
 695 SIMP_TAC[LE_REFL]]);;\r
 696 (* ======================== *)\r
 697 \r
 698 \r
 699 \r
 700 \r
 701 \r
 702 let CARD_K_ELMS_EQ_K_IMP_ALL_DISTINCT = \r
 703 prove_by_refinement(\r
 704 `! k (f: num -> A). CARD {f n | n < k} = k \r
 705 ==> (!i j. i < k /\ j < k /\ ~( i = j) ==> ~( f i = f j )) `,\r
 706 [INDUCT_TAC;\r
 707 REWRITE_TAC[LT];\r
 708 ONCE_REWRITE_TAC[CARD_N_FIRST_ELMS_UNDUCTIVE];\r
 709 REWRITE_TAC[ARITH_RULE` SUC k - 1 = k `];\r
 710 FIRST_X_ASSUM NHANH;\r
 711 REWRITE_TAC[ARITH_RULE` a < SUC b <=> a < b \/ a = b `];\r
 712 MESON_TAC[]]);;\r
 713 \r
 714 \r
 715 \r
 716 \r
 717 \r
 718 \r
 719 \r
 720 let CARD_UNION_NOT_DISTJ_LT = \r
 721 prove_by_refinement(\r
 722 ` FINITE (s: A -> bool) /\ FINITE t /\ ~( s INTER t = {} ) ==>\r
 723   CARD (s UNION t) < CARD s + CARD t `,\r
 724 [NGOAC;\r
 725 NHANH CARD_UNION_GEN;\r
 726 REWRITE_TAC[TR_SET_RULE[]` ~( x = {} ) <=> (?a. {a} SUBSET x ) `];\r
 727 NHANH (MESON[FINITE_INTER]` FINITE s /\ FINITE t ==> FINITE (s INTER t)`);\r
 728 STRIP_TAC;\r
 729 UNDISCH_TAC `FINITE ((s: A -> bool) INTER t)`;\r
 730 DOWN THEN PHA;\r
 731 NHANH CARD_SUBSET;\r
 732 REWRITE_TAC[CARD_SINGLETON];\r
 733 STRIP_TAC;\r
 734 UNDISCH_TAC `CARD ((s: A -> bool) UNION t) = \r
 735 (CARD s + CARD t) - CARD (s INTER t)`;\r
 736 ONCE_REWRITE_TAC[ARITH_RULE` a < b <=> 0 < b - a `];\r
 737 ASSUME_TAC2 (SPEC_ALL CARD_UNION_LE);\r
 738 ASSUME_TAC (TR_SET_RULE[]` (s INTER t) SUBSET (s: A -> bool) `);\r
 739 ASSUME_TAC2 (SPECL [`(s:A -> bool) INTER t `;` s: A -> bool`] CARD_SUBSET);\r
 740 DOWN THEN DOWN THEN REMOVE_TAC;\r
 741 DOWN THEN DOWN THEN PHA THEN ARITH_TAC]);;\r
 742 \r
 743 \r
 744 \r
 745 \r
 746 \r
 747 \r
 748 \r
 749 let CARD_ITER_K_EK_IMP_DIST = prove_by_refinement(\r
 750 `! k (f: A -> A). CARD {ITER n f x | n < k} = k ==>\r
 751      (!i j. i < k /\ j < k /\ ~(i = j ) ==> ~(ITER i f x = ITER j f x))`,\r
 752 [REPEAT GEN_TAC;\r
 753 REWRITE_TAC[BETA_RULE (SPECL [`k: num `;\r
 754 `(\n. ITER n (f:A -> A) x ) `] CARD_K_ELMS_EQ_K_IMP_ALL_DISTINCT)]]);;\r
 755 \r
 756 \r
 757 \r
 758 \r
 759 \r
 760 \r
 761 \r
 762 \r
 763 let DIH2K_IMP_PRE_SIMPLE_HYP = prove_by_refinement\r
 764 (`FINITE ( dart H ) /\ \r
 765 dih2k (H:(A)hypermap) k /\ ~( k = 0 ) \r
 766 ==> (! x. x IN dart H ==> ~( node_map H x IN face H (x:A) )) `,\r
 767 [REWRITE_TAC[ dih2k; simple_hypermap];\r
 768 STRIP_TAC;\r
 769 GEN_TAC;\r
 770 ASM_CASES_TAC `node_map H x IN face H (x:A) `;\r
 771 (* subgoal 1 *)\r
 772 FIRST_X_ASSUM NHANH;\r
 773 LET_TAC;\r
 774 STRIP_TAC;\r
 775 SUBGOAL_THEN ` ~( (S: A -> bool) INTER (IMAGE (node_map H) S) = {}) ` ASSUME_TAC;\r
 776 ASSUME_TAC (SPEC_ALL face_refl);\r
 777 DOWN;\r
 778 NHANH (ISPECL [`node_map (H:(A) hypermap)`;`S: A -> bool `;`x:A `] FUN_IN_IMAGE);\r
 779 UNDISCH_TAC `node_map H (x:A) IN S`;\r
 780 ASM_REWRITE_TAC[];\r
 781 SET_TAC[];\r
 782 ASSUME_TAC2 lemma_face_subset;\r
 783 ASSUME_TAC2 (SPECL [`face H (x:A) `;` dart (H:(A) hypermap)`] FINITE_SUBSET);\r
 784 ASSUME_TAC2 (ISPECL [` node_map (H:(A) hypermap) `;`face H (x:A) `] FINITE_IMAGE);\r
 785 REPLICATE_TAC 5 DOWN;\r
 786 PHA THEN ASM_REWRITE_TAC[];\r
 787 STRIP_TAC;\r
 788 ASSUME_TAC2 (SPECL [`S: A -> bool `;` IMAGE (node_map H)\r
 789  (S: A -> bool) `] (GEN_ALL CARD_UNION_NOT_DISTJ_LT));\r
 790 ASSUME_TAC2 (ISPECL [`node_map (H:(A) hypermap)`;` S:A -> bool`] CARD_IMAGE_LE);\r
 791 ASSUME_TAC2 (SPECL [`face_map (H:(A) hypermap)`;`k: num `] \r
 792 (GEN_ALL HAVING_ORDERS_K_IMP_CARD_ORBIT_LE_K));\r
 793 DOWN;\r
 794 ASM_REWRITE_TAC[GSYM face];\r
 795 DISCH_THEN (MP_TAC o (SPEC `x: A`));\r
 796 ASM_REWRITE_TAC[] THEN STRIP_TAC;\r
 797 DOWN THEN DOWN THEN DOWN THEN PHA;\r
 798 NHANH (ARITH_RULE`a < b + c /\ c <= b /\ b <= k ==> a < 2 * k `);\r
 799 FIRST_ASSUM (fun x -> REWRITE_TAC[SYM x]);\r
 800 STRIP_TAC;\r
 801 ASM_MESON_TAC[ARITH_RULE` x = 2 * k ==> ~(x < 2 * k ) `];\r
 802 (* subgoal 2 *)\r
 803 ASM_REWRITE_TAC[]]);;\r
 804 \r
 805 \r
 806 \r
 807 let ITER1 = prove(`ITER 1 f = (f:A -> A) `,\r
 808 REWRITE_TAC[ARITH_RULE` 1 = SUC 0 `; ITER; FUN_EQ_THM]);;\r
 809 \r
 810 \r
 811 \r
 812 \r
 813 \r
 814 \r
 815 let DIH2K_IMP_SIMPLE_HYPERMAP = prove_by_refinement(\r
 816  ` FINITE ( dart H ) /\ \r
 817 dih2k (H:(A)hypermap) k /\ ~( k = 0 ) ==> simple_hypermap H`,\r
 818 [NHANH DIH2K_IMP_PRE_SIMPLE_HYP;\r
 819 REWRITE_TAC[ dih2k; simple_hypermap];\r
 820 STRIP_TAC;\r
 821 GEN_TAC;\r
 822 ASSUME_TAC (ARITH_RULE` ~( 2 = 0 ) `);\r
 823 ASSUME_TAC2 (SPECL [`2`; `node_map (H:(A) hypermap) `] (GEN_ALL HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW));\r
 824 FIRST_X_ASSUM (MP_TAC o (SPEC `x:A `));\r
 825 REWRITE_TAC[GSYM node];\r
 826 REPEAT STRIP_TAC;\r
 827 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; TR_SET_RULE[]` (a INTER b) x <=> x IN a /\ x IN b `];\r
 828 REWRITE_TAC[TR_SET_RULE[]` {s} a <=> a = s `];\r
 829 GEN_TAC THEN EQ_TAC;\r
 830 ASM_SIMP_TAC[IN_ELIM_THM; ARITH_RULE` x < 2 <=> x = 0 \/ x = 1 `];\r
 831 STRIP_TAC;\r
 832 (* sub 1.1 *)\r
 833 REPLICATE_TAC 3 DOWN;\r
 834 SIMP_TAC[ITER];\r
 835 (* sub 1.2 *)\r
 836 REPLICATE_TAC 3 DOWN;\r
 837 SIMP_TAC[ITER; ITER1];\r
 838 ASM_MESON_TAC[];\r
 839 (* sub 2 *)\r
 840 SIMP_TAC[X_IN_HYP_ORBITS]]);;\r
 841 \r
 842 \r
 843 \r
 844 \r
 845 \r
 846 let IN_ORBIT_IMP_ORBIT_SUBSET = prove_by_refinement(\r
 847 `! x (y:A) f. x IN orbit_map f y ==> orbit_map f x SUBSET orbit_map f y `,\r
 848 [REPEAT GEN_TAC;\r
 849 REWRITE_TAC[orbit_map; IN_ELIM_THM; SUBSET; POWER_TO_ITER];\r
 850 REPEAT STRIP_TAC;\r
 851 ASM_SIMP_TAC[];\r
 852 REWRITE_TAC[ITER_ADD];\r
 853 EXISTS_TAC `n' + (n:num) `;\r
 854 REWRITE_TAC[ARITH_RULE ` a >= 0 `]]);;\r
 855 \r
 856 \r
 857 \r
 858 \r
 859 \r
 860 \r
 861 let IN_FACE_IMP_SUBSET_FACE = prove(\r
 862 `! (x:A). x IN face H y ==> face H x SUBSET face H y `,\r
 863 REWRITE_TAC[face] THEN \r
 864 NHANH IN_ORBIT_IMP_ORBIT_SUBSET THEN \r
 865 SIMP_TAC[]);;\r
 866 \r
 867 \r
 868 \r
 869 \r
 870 \r
 871 \r
 872 let HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT = prove_by_refinement(\r
 873 ` (f:A -> A) has_orders k /\ x IN orbit_map f y /\ ~( k = 0 ) ==>\r
 874 orbit_map f x = orbit_map f y `,\r
 875 [NHANH IN_ORBIT_IMP_ORBIT_SUBSET;\r
 876 SIMP_TAC[TR_SET_RULE[]` a = b <=> a SUBSET b /\ b SUBSET a `];\r
 877 STRIP_TAC;\r
 878 ASSUME_TAC2 HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW;\r
 879 UNDISCH_TAC `(x:A) IN orbit_map f y`;\r
 880 ASM_REWRITE_TAC[];\r
 881 REWRITE_TAC[SUBSET; IN_ELIM_THM];\r
 882 REPEAT STRIP_TAC;\r
 883 ASM_REWRITE_TAC[ITER_ADD];\r
 884 ASM_CASES_TAC ` (n:num) <= n' `;\r
 885 EXISTS_TAC ` n' - (n:num) `;\r
 886 ASM_SIMP_TAC[ARITH_RULE` n <= (n': num) ==> n' - n + n = n' `];\r
 887 ASM_ARITH_TAC;\r
 888 EXISTS_TAC ` (k: num) - n + n' `;\r
 889 ASM_SIMP_TAC[ARITH_RULE` n < k ==> (k - n + n') + n = n' + (k:num) `];\r
 890 UNDISCH_TAC `(f: A -> A) has_orders k `;\r
 891 SIMP_TAC[has_orders; GSYM ITER_ADD; I_THM];\r
 892 REMOVE_TAC THEN ASM_ARITH_TAC]);;\r
 893 \r
 894 \r
 895 \r
 896 \r
 897 \r
 898 \r
 899 \r
 900 \r
 901 \r
 902 \r
 903 \r
 904 \r
 905 \r
 906 let DIH_IMP_EVERY_NODE_INTER_FACE = prove_by_refinement\r
 907 (` dih2k (H:(A) hypermap) k \r
 908 ==> (! x y. {x,y} SUBSET dart H ==> ? d. d IN node H x /\ d IN face H y ) `,\r
 909 [REWRITE_TAC[dih2k; INSERT_SUBSET];\r
 910 REPEAT STRIP_TAC;\r
 911 UNDISCH_TAC `(y:A) IN dart H `;\r
 912 FIRST_X_ASSUM NHANH;\r
 913 REWRITE_TAC[let_CONV` let S = face H (y:A) in dart H = S UNION IMAGE (node_map H) S`];\r
 914 STRIP_TAC;\r
 915 UNDISCH_TAC `(x:A) IN dart H`;\r
 916 ASM_REWRITE_TAC[IN_UNION];\r
 917 STRIP_TAC;\r
 918 EXISTS_TAC `x:A`;\r
 919 ASM_SIMP_TAC[node_refl];\r
 920 DOWN;\r
 921 REWRITE_TAC[IN_IMAGE];\r
 922 STRIP_TAC;\r
 923 EXISTS_TAC `x':A`;\r
 924 ASM_REWRITE_TAC[node; orbit_map; IN_ELIM_THM];\r
 925 EXISTS_TAC `1 `;\r
 926 REWRITE_TAC[ARITH_RULE` 1 >= 0 `; POWER_1];\r
 927 REWRITE_TAC[ARITH_RULE` 1 >= 0 `; POWER_1];\r
 928 UNDISCH_TAC `node_map (H:(A) hypermap ) has_orders 2`;\r
 929 REWRITE_TAC[has_orders; FUN_EQ_THM; ITER; ARITH_RULE`2 = SUC 1 `; ITER1; I_THM];\r
 930 SIMP_TAC[EQ_SYM_EQ]]);;\r
 931 (* ================================  *)\r
 932 \r
 933 \r
 934 \r
 935 let F_INVERSE_F = prove(` (? y. f y = x ) ==> f ( (inverse f) x ) = x`,\r
 936 REWRITE_TAC[FUN_EQ_THM; I_THM; o_THM; inverse; IN_IMAGE]\r
 937 THEN ASM_MESON_TAC[]);;\r
 938 \r
 939 let F_INVERSE_F_F = MESON[F_INVERSE_F]` f ( inverse f (f x)) = f x `;;\r
 940 \r
 941 let INJ_IMP_INVERSE_FF = MESON[F_INVERSE_F_F]`(!y. f y = f x ==> y = x ) ==> inverse f ( f x ) = x `;;\r
 942 \r
 943 let BIJ_AND_BIJ_INVERSE = prove(` BIJ f S1 S2 /\ (! x. f x IN S2 ==> x IN S1 )\r
 944 ==> BIJ (inverse f) S2 S1 `,\r
 945 REWRITE_TAC[BIJ; INJ; SURJ] THEN \r
 946 ASM_MESON_TAC[F_INVERSE_F ]);;\r
 947 \r
 948 \r
 949 \r
 950 \r
 951 \r
 952 \r
 953 \r
 954 \r
 955 let INVERSE_FUNCTION_OF_BIJ = prove_by_refinement(\r
 956 `BIJ (f:A -> B) S1 S2 /\ g = (\x. if x IN S2 then (@t. t IN S1 /\ f t = x ) else tt )\r
 957 ==> BIJ g S2 S1 `,\r
 958 [REWRITE_TAC[BIJ; INJ; SURJ];\r
 959 STRIP_TAC;\r
 960 SUBGOAL_THEN `(!x. (x:B) IN S2 ==> g x IN (S1: A -> bool) /\ f ( g x ) = x )` ASSUME_TAC;\r
 961 ASM_REWRITE_TAC[];\r
 962 FIRST_X_ASSUM NHANH;\r
 963 SIMP_TAC[];\r
 964 MESON_TAC[];\r
 965 (* ================= *)\r
 966 CONJ_TAC;\r
 967 ASM_MESON_TAC[];\r
 968 CONJ_TAC;\r
 969 FIRST_X_ASSUM NHANH;\r
 970 SIMP_TAC[];\r
 971 REPEAT STRIP_TAC;\r
 972 EXISTS_TAC `(f:A -> B) x `;\r
 973 ASM_MESON_TAC[]]);;\r
 974 \r
 975 \r
 976 \r
 977 \r
 978 \r
 979 let TOW_BIJS_IMP_BIJ_BETWEEN_FIRST = prove_by_refinement(\r
 980 ` BIJ (f:B -> A ) S1 V /\ BIJ (g:C -> A) S2 V /\\r
 981 ff = (\x. if x IN S1 then (@a. a IN S2 /\ f x = g a) else aa) \r
 982 ==> BIJ ff S1 S2 `,\r
 983 [REWRITE_TAC[BIJ; INJ; SURJ];\r
 984 STRIP_TAC;\r
 985 SUBGOAL_THEN ` (!x. (x:B) IN S1 ==> ff x IN (S2: C -> bool) /\ (f:B -> A) x = g ( ff x )) ` ASSUME_TAC;\r
 986 ASM_REWRITE_TAC[];\r
 987 SIMP_TAC[];\r
 988 ASM_MESON_TAC[];\r
 989 ASM_MESON_TAC[]]);;\r
 990 \r
 991 \r
 992 \r
 993 \r
 994 \r
 995 \r
 996 \r
 997 let INDENT_IN_S1_IMP_BIJ = \r
 998 prove(` BIJ (f: A -> B) S1 S2 /\ (! x. x IN S1 ==> f x = g x )\r
 999 ==> BIJ g S1 S2 `,\r
1000 REWRITE_TAC[BIJ; INJ; SURJ] THEN \r
1001 MESON_TAC[]);;\r
1002 \r
1003 \r
1004 let LOCAL_FAN_IMP_FAN = prove(` local_fan (V,E,FF) ==> FAN ( vec 0, V,E) `,\r
1005 REWRITE_TAC[local_fan] THEN \r
1006 LET_TAC THEN SIMP_TAC[]);;\r
1007 \r
1008 \r
1009 \r
1010 \r
1011 \r
1012 \r
1013 let IN_ORBIT_MAP_IMP_F_Y = prove(` (y:A) IN orbit_map f x ==> f y IN orbit_map f x `,\r
1014 REWRITE_TAC[orbit_map; IN_ELIM_THM] THEN \r
1015 STRIP_TAC THEN \r
1016 EXISTS_TAC ` n + 1 ` THEN \r
1017 ASM_REWRITE_TAC[ARITH_RULE ` a >= 0 /\ \r
1018 n + 1 = SUC n`; COM_POWER; I_THM; o_THM]);;\r
1019 \r
1020 \r
1021 \r
1022 \r
1023 \r
1024 \r
1025 let SURJ_IMP_S2_EQ_IMAGE_S1 = prove(` SURJ (f:A ->B) S1 S2 ==> IMAGE f S1 = S2 `,\r
1026 REWRITE_TAC[IMAGE; SURJ] THEN SET_TAC[]);;\r
1027 \r
1028 \r
1029 \r
1030 \r
1031 let CYCLIC_SET_IMP_NOT_COLLINEAR =\r
1032 prove_by_refinement(\r
1033 ` cyclic_set W (x:real^3) y ==> (! v. v IN W ==> ~ collinear {v,x,y}) `,\r
1034 [REWRITE_TAC[TR_SET_RULE[]` x IN a <=> {x,x,x} SUBSET a `];\r
1035 STRIP_TAC THEN GEN_TAC;\r
1036 DOWN THEN PHA;\r
1037 ONCE_REWRITE_TAC[CONJ_SYM];\r
1038 NHANH Fan.subset_cyclic_set_fan;\r
1039 NHANH Fan.properties_of_cyclic_set;\r
1040 SIMP_TAC[INSERT_COMM]]);;\r
1041 \r
1042 \r
1043 \r
1044 \r
1045 \r
1046 let SLIDABLE_PROJECTION =\r
1047 prove_by_refinement(` ~( e = vec 0) ==> projection e ( t % e + x ) = projection e x `,\r
1048 [REWRITE_TAC[projection; DOT_LADD;\r
1049 REAL_FIELD` (a + b ) / c = a / c + b / c `; VECTOR_ADD_RDISTRIB;\r
1050 DOT_LMUL];\r
1051 SIMP_TAC[GSYM DOT_EQ_0; REAL_FIELD` ~( b = &0 ) ==> ( a * b ) / b = a `];\r
1052 DISCH_TAC;\r
1053 VECTOR_ARITH_TAC]);;\r
1054 \r
1055 \r
1056 \r
1057 \r
1058 \r
1059 \r
1060 let LINEAR_PROJECTION = prove(` projection e (t % x ) = t % ( projection e x ) `,\r
1061 REWRITE_TAC[projection; DOT_LMUL; REAL_ARITH ` ( a * b ) / c = a * ( b / c ) `; GSYM VECTOR_MUL_ASSOC; VECTOR_SUB_LDISTRIB]);;\r
1062 \r
1063 \r
1064 \r
1065 \r
1066 \r
1067 let IDENTIFY_AZIM_CYCLE = prove_by_refinement\r
1068 (` ~( W SUBSET {p}) /\ ~collinear {p,v,w} /\\r
1069  cyclic_set W v w /\ ( ~(u = p) /\ W u ) /\\r
1070 (!q. ~(q = p) /\ W q\r
1071                           ==> azim v w p u < azim v w p q \/\r
1072                               azim v w p u = azim v w p q /\\r
1073                               norm (projection (w - v) (u - v)) <=\r
1074                               norm (projection (w - v) (q - v)))\r
1075 ==> azim_cycle W v w p = u `,\r
1076 [ABBREV_TAC ` uu = azim_cycle W v w (p:real^3) `;\r
1077 STRIP_TAC;\r
1078 SUBGOAL_THEN` ~( uu = p) /\ W (uu:real^3) /\\r
1079 (!q. ~(q = p) /\ W q\r
1080           ==> azim v w p uu < azim v w p q \/\r
1081               azim v w p uu = azim v w p q /\\r
1082               norm (projection (w - v) (uu - v)) <=\r
1083               norm (projection (w - v) (q - v))) ` ASSUME_TAC;\r
1084 EXPAND_TAC "uu";\r
1085 UNDISCH_TAC ` ~(W SUBSET {p:real^3} ) `;\r
1086 SIMP_TAC[azim_cycle];\r
1087 DISCH_TAC;\r
1088 CONV_TAC SELECT_CONV;\r
1089 EXISTS_TAC `u:real^3 `;\r
1090 ASM_REWRITE_TAC[];\r
1091 DOWN THEN STRIP_TAC;\r
1092 UNDISCH_TAC `(W:real^3 -> bool) (u:real^3) `;\r
1093 UNDISCH_TAC `~( u = (p:real^3)) `;\r
1094 PHA;\r
1095 FIRST_X_ASSUM NHANH;\r
1096 DISCH_TAC;\r
1097 UNDISCH_TAC `(W:real^3 -> bool) (uu:real^3) `;\r
1098 UNDISCH_TAC `~( uu = (p:real^3)) `;\r
1099 PHA;\r
1100 FIRST_ASSUM NHANH;\r
1101 DOWN THEN STRIP_TAC;\r
1102 STRIP_TAC;\r
1103 ASM_REAL_ARITH_TAC;\r
1104 ASM_REAL_ARITH_TAC;\r
1105 STRIP_TAC;\r
1106 ASM_REAL_ARITH_TAC;\r
1107 UNDISCH_TAC `cyclic_set W v (w:real^3) `;\r
1108 NHANH CYCLIC_SET_IMP_NOT_COLLINEAR;\r
1109 REWRITE_TAC[IN];\r
1110 STRIP_TAC;\r
1111 UNDISCH_TAC `(W:real^3 -> bool) u `;\r
1112 UNDISCH_TAC `(W:real^3 -> bool) uu `;\r
1113 FIRST_ASSUM NHANH;\r
1114 STRIP_TAC THEN STRIP_TAC;\r
1115 MP_TAC (MESON[AZIM_EQ]`~collinear {v, w, (p:real^3)} /\\r
1116            ~collinear {v, w, u} /\\r
1117            ~collinear {v, w, uu} /\\r
1118            azim v w p u = azim v w p uu \r
1119 ==>  uu IN aff_gt {v,w} {u}`);\r
1120 ANTS_TAC;\r
1121 SIMP_TAC[INSERT_COMM];\r
1122 CONJ_TAC;\r
1123 FIRST_ASSUM ACCEPT_TAC;\r
1124 CONJ_TAC;\r
1125 FIRST_ASSUM ACCEPT_TAC;\r
1126 CONJ_TAC;\r
1127 FIRST_X_ASSUM ACCEPT_TAC;\r
1128 FIRST_X_ASSUM ACCEPT_TAC;\r
1129 DOWN;\r
1130 NHANH (MESON[COLLINEAR_2; INSERT_INSERT; INSERT_COMM]` \r
1131 ~ collinear {a,b,c} ==> ~( a = b ) /\ ~( a = c )`);\r
1132 REWRITE_TAC[TR_SET_RULE[]`~(u = v) /\ ~(u = w) <=> DISJOINT {v,w} {u} `];\r
1133 NHANH AFF_GT_2_1;\r
1134 SIMP_TAC[IN_ELIM_THM];\r
1135 STRIP_TAC;\r
1136 STRIP_TAC;\r
1137 UNDISCH_TAC` norm (projection (w - v) (uu - v)) <= norm (projection (w - v) (u - (v:real^3))) `;\r
1138 UNDISCH_TAC `norm (projection (w - v) (u - v)) <= norm (projection (w - v) (uu - (v:real^3)))`;\r
1139 PHA;\r
1140 REWRITE_TAC[REAL_ARITH` a <= b /\ b <= a <=> a = b `];\r
1141 ASM_REWRITE_TAC[];\r
1142 UNDISCH_TAC ` t1 + t2 + t3 = &1 `;\r
1143 SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `;\r
1144 VECTOR_ARITH` (((&1 - (t2 + t3)) % v + t2 % w + t3 % u) - v) =\r
1145 t2 % ( w - v ) + t3 % ( u - v ) `];\r
1146 UNDISCH_TAC ` cyclic_set W v (w:real^3) `;\r
1147 REWRITE_TAC[cyclic_set];\r
1148 ONCE_REWRITE_TAC[VECTOR_ARITH` a = b <=> b - a = vec 0 `];\r
1149 SIMP_TAC[SLIDABLE_PROJECTION; LINEAR_PROJECTION];\r
1150 REWRITE_TAC[NORM_MUL; REAL_FIELD` a = x * a <=> a = &0 \/ x = &1 `];\r
1151 REPEAT STRIP_TAC;\r
1152 DOWN;\r
1153 REWRITE_TAC[NORM_EQ_0; projection];\r
1154 REWRITE_TAC[VECTOR_ARITH` u - v - x % ( w - v ) = vec 0 <=>\r
1155 u = (&1 - x ) % v + x % w `];\r
1156 DISCH_TAC;\r
1157 SUBGOAL_THEN` (u:real^3) IN aff {v,w} ` ASSUME_TAC;\r
1158 REWRITE_TAC[AFF2; IN_ELIM_THM];\r
1159 DOWN;\r
1160 MESON_TAC[REAL_ARITH` a = &1 - (&1 - a ) `];\r
1161 UNDISCH_TAC`~(w - (v:real^3) = vec 0 ) `;\r
1162 REWRITE_TAC[VECTOR_SUB_EQ];\r
1163 NHANH NOT_EQ_IMP_AFF_AND_COLL3;\r
1164 SIMP_TAC[INSERT_COMM];\r
1165 STRIP_TAC;\r
1166 FIRST_X_ASSUM SUBST_ALL_TAC;\r
1167 ASM_MESON_TAC[];\r
1168 ASSUME_TAC2 (SPEC `t3:real ` (GEN_ALL LT_IMP_ABS_REFL));\r
1169 DOWN THEN ASM_REWRITE_TAC[];\r
1170 STRIP_TAC;\r
1171 SUBGOAL_THEN` uu + ( -- t1) % ( v - w ) - (u:real^3) = vec 0 ` ASSUME_TAC;\r
1172 ASM_REWRITE_TAC[];\r
1173 EXPAND_TAC "t3";\r
1174 VECTOR_ARITH_TAC;\r
1175 DOWN;\r
1176 UNDISCH_TAC`(W:real^3 -> bool) uu `;\r
1177 UNDISCH_TAC `(W:real^3 -> bool) u `;\r
1178 PHA;\r
1179 REWRITE_TAC[VECTOR_ARITH` a + b - (c:real^N) = (a + b ) - c `];\r
1180 FIRST_ASSUM NHANH;\r
1181 STRIP_TAC;\r
1182 DOWN;\r
1183 ASM_REWRITE_TAC[];\r
1184 VECTOR_ARITH_TAC]);;\r
1185 \r
1186 \r
1187 \r
1188 \r
1189 (* *)\r
1190 \r
1191 let EXISTS_SMALLEST_ELMS = prove_by_refinement \r
1192 (` FINITE W /\ ~(W = {} ) /\\r
1193 (! x (y:A). ll x y \/ ll y x ) /\\r
1194 (! x y z. ll x y /\ ll y z ==> ll x z ) \r
1195 ==> ? v. v IN W /\ (! w. w IN W ==> ll v w ) `,\r
1196 [WF_INDUCT_TAC `CARD (W:A -> bool) `;\r
1197 REWRITE_TAC[TR_SET_RULE[]`~( a = {}) <=> ? x. x IN a `];\r
1198 STRIP_TAC;\r
1199 ASSUME_TAC2 (ISPECL [`W:A -> bool`;`x:A`] CARD_MINUS_ONE);\r
1200 DOWN;\r
1201 NHANH (ARITH_RULE` a = b + 1 ==> b < a `);\r
1202 FIRST_ASSUM NHANH;\r
1203 UNDISCH_TAC `!(W':A -> bool). CARD W' < CARD (W:A -> bool)\r
1204            ==> FINITE W' /\\r
1205                ~(W' = {}) /\\r
1206                (!x y. ll (x:A) (y:A) \/ ll y x) /\\r
1207                (!x y z. ll x y /\ ll y z ==> ll x z)\r
1208            ==> (?v. v IN W' /\ (!w. w IN W' ==> ll v w)) `;\r
1209 DISCH_TAC;\r
1210 FIRST_ASSUM NHANH;\r
1211 STRIP_TAC THEN DOWN;\r
1212 ASM_CASES_TAC ` W = {x:A} `;\r
1213 REMOVE_TAC;\r
1214 EXISTS_TAC `x:A`;\r
1215 ASM_SIMP_TAC[IN_ELIM_THM; IN_SING];\r
1216 UNDISCH_TAC `! x y. (ll:A -> A -> bool) x y \/ ll y x `;\r
1217 MESON_TAC[];\r
1218 ASSUME_TAC2 (TR_SET_RULE[]` (x:A) IN W /\ ~(W = {x}) ==> ~(W DELETE x = {}) `);\r
1219 ANTS_TAC;\r
1220 ASM_SIMP_TAC[FINITE_DELETE];\r
1221 FIRST_X_ASSUM ACCEPT_TAC;\r
1222 STRIP_TAC;\r
1223 USE_FIRST `! x y. (ll: A -> A -> bool) x y \/ ll y x ` (DISJ_CASES_TAC o (SPECL[` x:A `;` v:A`]));\r
1224 EXISTS_TAC `x:A`;\r
1225 ASM_REWRITE_TAC[];\r
1226 ASSUME_TAC2 (\r
1227 TR_SET_RULE[]` x:A IN W ==> (! a. a IN W <=> a IN (W DELETE x) \/ a = x )`);\r
1228 ASM_REWRITE_TAC[];\r
1229 ASM_MESON_TAC[];\r
1230 EXISTS_TAC `v:A`;\r
1231 ASSUME_TAC2 (TR_SET_RULE[]` (v:A) IN W DELETE x ==> v IN W`);\r
1232 ASM_REWRITE_TAC[];\r
1233 ASSUME_TAC2 (\r
1234 TR_SET_RULE[]` x:A IN W ==> (! a. a IN W <=> a IN (W DELETE x) \/ a = x )`);\r
1235 ASM_REWRITE_TAC[];\r
1236 ASM_MESON_TAC[]]);;\r
1237 \r
1238 \r
1239 \r
1240 \r
1241 \r
1242 \r
1243 \r
1244 let EXIS_SMALLEST_WITH_AZIM_ORD = prove_by_refinement\r
1245 (`~(W SUBSET {p}) /\ FINITE W\r
1246 ==> ?u. \r
1247        (~(u = p) /\ W u) /\\r
1248        (!q. ~(q = p) /\ W q\r
1249             ==> azim v w p u < azim v w p q \/\r
1250                 azim v w p u = azim v w p q /\\r
1251                 norm (projection (w - v) (u - v)) <=\r
1252                 norm (projection (w - v) (q - v))) `,\r
1253 [ABBREV_TAC ` ll (u:real^3) (q:real^3) <=>\r
1254    ~ (W:real^3 -> bool) u  \/ W u /\ W q /\\r
1255             (  azim v w p u < azim v w p q \/\r
1256                 azim v w p u = azim v w p q /\\r
1257                 norm (projection (w - v) (u - v)) <=\r
1258                 norm (projection (w - v) (q - v)))`;\r
1259 STRIP_TAC;\r
1260 MP_TAC (ISPECL [`(W:real^3 -> bool) DELETE p`;` ll:real^3 -> real^3 -> bool` ] (GEN_ALL EXISTS_SMALLEST_ELMS));\r
1261 ANTS_TAC;\r
1262 DOWN_TAC;\r
1263 SIMP_TAC[cyclic_set];\r
1264 NHANH (TR_SET_RULE[]` ~( a SUBSET {b}) ==> ~(a DELETE b = {}) `);\r
1265 SIMP_TAC[FINITE_DELETE];\r
1266 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1267 STRIP_TAC;\r
1268 CONJ_TAC;\r
1269 ASM_REWRITE_TAC[REAL_LE_REFL];\r
1270 GEN_TAC THEN GEN_TAC;\r
1271 ASM_CASES_TAC ` ~ (W:real^3 -> bool)  x `;\r
1272 REPEAT DISJ1_TAC;\r
1273 FIRST_ASSUM ACCEPT_TAC;\r
1274 ASM_CASES_TAC ` ~ (W:real^3 -> bool)  y `;\r
1275 DISJ2_TAC;\r
1276 DISJ1_TAC;\r
1277 FIRST_ASSUM ACCEPT_TAC;\r
1278 DOWN THEN DOWN THEN PHA;\r
1279 SIMP_TAC[];\r
1280 DISCH_TAC;\r
1281 REAL_ARITH_TAC;\r
1282 REPEAT GEN_TAC;\r
1283 ASM_REWRITE_TAC[];\r
1284 IMP_TAC THEN DISCH_TAC;\r
1285 FIRST_X_ASSUM DISJ_CASES_TAC;\r
1286 ASM_REWRITE_TAC[];\r
1287 DISCH_TAC;\r
1288 FIRST_X_ASSUM DISJ_CASES_TAC;\r
1289 DOWN THEN MATCH_MP_TAC (TAUT` a ==> ~ a ==> b `);\r
1290 ASM_REWRITE_TAC[];\r
1291 FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);\r
1292 FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);\r
1293 DISJ2_TAC;\r
1294 DOWN;\r
1295 FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);\r
1296 FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC);\r
1297 DOWN THEN PHA;\r
1298 ASM_REWRITE_TAC[];\r
1299 REAL_ARITH_TAC;\r
1300 \r
1301 \r
1302 DOWN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1303 STRIP_TAC;\r
1304 DOWN;\r
1305 DOWN;\r
1306 ASM_REWRITE_TAC[IN_DELETE; IN];\r
1307 SIMP_TAC[EQ_SYM_EQ];\r
1308 STRIP_TAC;\r
1309 STRIP_TAC;\r
1310 EXISTS_TAC`v':real^3 `;\r
1311 REPLICATE_TAC 3 DOWN THEN PHA;\r
1312 SIMP_TAC[CONJ_SYM];\r
1313 MESON_TAC[]]);;\r
1314 \r
1315 \r
1316 \r
1317 \r
1318 \r
1319 \r
1320 \r
1321 let AZIM_CYCLE_PROPERTIES = prove_by_refinement\r
1322 (` ~(W SUBSET {p}) /\ FINITE W ==>\r
1323 ~(azim_cycle W v w p = p) /\ W (azim_cycle W v w p) /\\r
1324               (!q. ~(q = p) /\ W q\r
1325                    ==> azim v w p (azim_cycle W v w p) < azim v w p q \/\r
1326                        azim v w p (azim_cycle W v w p) = azim v w p q /\\r
1327                        norm (projection (w - v) ((azim_cycle W v w p) - v)) <=\r
1328                        norm (projection (w - v) (q - v))) `,\r
1329 [NHANH EXIS_SMALLEST_WITH_AZIM_ORD;\r
1330 STRIP_TAC;\r
1331 REWRITE_TAC[azim_cycle];\r
1332 ASM_SIMP_TAC[];\r
1333 CONV_TAC SELECT_CONV;\r
1334 EXISTS_TAC `u:real^3 `;\r
1335 ASM_SIMP_TAC[]]);;\r
1336 \r
1337 \r
1338 \r
1339 let PROJECT_EQ_VEC0_IMP_PARALLED = prove(\r
1340 ` projection e x = vec 0 ==> (?t. x = t % e ) `,\r
1341 REWRITE_TAC[projection; VECTOR_SUB_EQ]\r
1342 THEN MESON_TAC[]);;\r
1343 \r
1344 \r
1345 \r
1346 \r
1347 \r
1348 let PROJECTION_VEC0 = prove(` projection e ( vec 0 ) = vec 0 `,\r
1349 REWRITE_TAC[projection; DOT_LZERO; REAL_ARITH` &0 / d = &0 `]\r
1350 THEN VECTOR_ARITH_TAC);;\r
1351 \r
1352 \r
1353 \r
1354 (* removed 2011-08-01, thales :\r
1355 let azim_cycle2 = new_definition\r
1356 ` azim_cycle2 W v w p = \r
1357    (if W SUBSET {p}\r
1358           then p\r
1359           else let le =\r
1360                    (\u q.\r
1361                         azim v w (CHOICE W) u < azim v w (CHOICE W) q \/\r
1362                         azim v w (CHOICE W) u = azim v w (CHOICE W) q /\\r
1363                         norm (projection (w - v) (u - v)) <=\r
1364                         norm (projection (w - v) (q - v))) in\r
1365                @u. ~(u = p) /\\r
1366                    W u /\\r
1367                    le p u /\\r
1368                    (!q. ~(q = p) /\ W q /\ le p q ==> le u q) \/\r
1369                    ~(u = p) /\ W u /\ (!q. W q ==> le u q)) `;;\r
1370 let W_SUBSET_SINGLETON_IMP_IDE2 = prove(\r
1371 ` W SUBSET {p} ==> azim_cycle2 W v w p = p `, SIMP_TAC[azim_cycle2]);;\r
1372 *)\r
1373 \r
1374 \r
1375 \r
1376 \r
1377 \r
1378 let LE_ORD_IS_ASSYMETRY = prove_by_refinement\r
1379 (` let le = (\u q.\r
1380                         azim v w (CHOICE W) u < azim v w (CHOICE W) q \/\r
1381                         azim v w (CHOICE W) u = azim v w (CHOICE W) q /\\r
1382                         norm (projection (w - v) (u - v)) <=\r
1383                         norm (projection (w - v) (q - v))) \r
1384 in cyclic_set W v w /\ {x,y} SUBSET W /\ le x y /\ le y x \r
1385 ==> x = y `,\r
1386 [LET_TAC;\r
1387 EXPAND_TAC "le";\r
1388 REWRITE_TAC[REAL_ARITH`( a < b \/ a = b /\ x <= y ) /\\r
1389 ( b < a \/ b = a /\ y <= x ) <=> a = b /\ x = y `];\r
1390 ASM_CASES_TAC ` (W:real^3 -> bool) = {} `;\r
1391 ASM_REWRITE_TAC[INSERT_SUBSET; NOT_IN_EMPTY];\r
1392 DOWN THEN NHANH CHOICE_DEF;\r
1393 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];\r
1394 NHANH CYCLIC_SET_IMP_NOT_COLLINEAR;\r
1395 STRIP_TAC;\r
1396 IMP_TAC THEN STRIP_TAC;\r
1397 UNDISCH_TAC ` CHOICE (W:real^3 -> bool) IN W `;\r
1398 FIRST_ASSUM NHANH;\r
1399 REPEAT STRIP_TAC;\r
1400 SUBGOAL_THEN ` azim v w (CHOICE W) x = azim v w (CHOICE W) y <=> \r
1401 x IN aff_gt {v, w} {y}` ASSUME_TAC;\r
1402 MATCH_MP_TAC AZIM_EQ_ALT;\r
1403 DOWN_TAC;\r
1404 SIMP_TAC[INSERT_COMM];\r
1405 FIRST_X_ASSUM SUBST_ALL_TAC;\r
1406 REPLICATE_TAC 3 DOWN THEN PHA;\r
1407 NHANH th3b;\r
1408 NHANH th3b1;\r
1409 REWRITE_TAC[SET_RULE` (a /\ ~( y = w )) /\ ~( y = u) <=> a /\ DISJOINT {u,w} {y} `];\r
1410 NHANH AFF_GT_2_1;\r
1411 IMP_TAC THEN STRIP_TAC;\r
1412 ASM_REWRITE_TAC[IN_ELIM_THM];\r
1413 REWRITE_TAC[REAL_ARITH` a + b + c = d <=> c = d - a - b `];\r
1414 IMP_TAC THEN STRIP_TAC;\r
1415 ASM_REWRITE_TAC[];\r
1416 REWRITE_TAC[VECTOR_ARITH` (t1 % v + t2 % w + (&1 - t1 - t2) % y) - v =\r
1417 t2 % ( w - v ) + (&1 - t1 - t2 ) % ( y - v ) `];\r
1418 UNDISCH_TAC` cyclic_set W (v:real^3) w `;\r
1419 REWRITE_TAC[cyclic_set];\r
1420 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1421 IMP_TAC;\r
1422 PAT_ONCE_REWRITE_TAC `\x. x ==> y `[GSYM VECTOR_SUB_EQ];\r
1423 NHANH (MESON[SLIDABLE_PROJECTION]` ~ ( e = vec 0) ==> (! t x. projection e \r
1424 ( t % e + x ) = projection e x )`);\r
1425 STRIP_TAC;\r
1426 ASM_REWRITE_TAC[LINEAR_PROJECTION; NORM_MUL; REAL_RING` a = b * a <=> b = &1 \/ a = &0 `];\r
1427 STRIP_TAC THEN DISCH_THEN DISJ_CASES_TAC;\r
1428 DOWN;\r
1429 UNDISCH_TAC ` t3 = &1 - t1 - t2 `;\r
1430 UNDISCH_TAC ` &0 < t3 `;\r
1431 NHANH LT_IMP_ABS_REFL;\r
1432 STRIP_TAC;\r
1433 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1434 DISCH_TAC;\r
1435 ASM_REWRITE_TAC[];\r
1436 STRIP_TAC;\r
1437 USE_FIRST ` (x:real^3) = t1 % v + t2 % w + t3 % y ` MP_TAC;\r
1438 EXPAND_TAC "t3";\r
1439 ASSUME_TAC2 (REAL_ARITH` &1 - t1 - t2 = t3 /\ &1 = t3 ==> t2 = -- t1 `);\r
1440 DOWN THEN SIMP_TAC[] THEN STRIP_TAC;\r
1441 REWRITE_TAC[VECTOR_ARITH` x = t1 % v + --t1 % w + &1 % y <=> y + t1 %\r
1442 (v - w ) = x `];\r
1443 UNDISCH_TAC` (y:real^3) IN W `;\r
1444 UNDISCH_TAC` (x:real^3) IN W `;\r
1445 PHA;\r
1446 REWRITE_TAC[IN];\r
1447 FIRST_X_ASSUM NHANH;\r
1448 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1449 ASM_REWRITE_TAC[];\r
1450 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1451 SIMP_TAC[EQ_SYM_EQ];\r
1452 DOWN;\r
1453 REWRITE_TAC[NORM_EQ_0];\r
1454 NHANH PROJECT_EQ_VEC0_IMP_PARALLED;\r
1455 STRIP_TAC;\r
1456 DOWN;\r
1457 UNDISCH_TAC ` ~( w - (v:real^3) = vec 0 ) `;\r
1458 REWRITE_TAC[VECTOR_SUB_EQ];\r
1459 NHANH (SPECL [`a:real^3 `;` b:real^3 `;`y:real^3 `]\r
1460  (Collect_geom.NOT_TWO_EQ_IMP_COL_EQUAVALENT));\r
1461 REPEAT STRIP_TAC;\r
1462 SUBGOAL_THEN ` collinear {(y:real^3), w, v}` ASSUME_TAC;\r
1463 ASM_REWRITE_TAC[AFF2; IN_ELIM_THM];\r
1464 EXISTS_TAC `t:real `;\r
1465 DOWN;\r
1466 VECTOR_ARITH_TAC;\r
1467 MATCH_MP_TAC (TAUT` F ==> h `);\r
1468 DOWN; REWRITE_TAC[];\r
1469 ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a}`];\r
1470 FIRST_ASSUM ACCEPT_TAC]);;\r
1471 \r
1472 \r
1473 \r
1474 let LE_ORD_IS_ASSYMETRY2 = \r
1475 REWRITE_RULE[let_CONV (concl LE_ORD_IS_ASSYMETRY);\r
1476 REAL_ARITH` ( a < b \/ a = b /\ x <= y ) /\ ( b < a \/ b = a /\ y <= x )\r
1477 <=> a = b /\ x = y `]\r
1478 LE_ORD_IS_ASSYMETRY;;\r
1479 \r
1480 \r
1481 \r
1482 \r
1483 \r
1484 \r
1485 let W_SUBSET_SINGLETON_IMP_IDE =\r
1486 prove(` W SUBSET {p} ==> azim_cycle W v w p = p `,\r
1487 SIMP_TAC[azim_cycle]);;\r
1488 \r
1489 \r
1490 \r
1491 \r
1492 \r
1493 \r
1494 let AZIM_CYCLE_EQ_SIGMA_FAN = prove_by_refinement\r
1495 (` FAN ((x:real^3),V,E) /\ u IN set_of_edge v V E ==>\r
1496 azim_cycle (EE v E) x v u = sigma_fan x V E v u `,\r
1497 [REWRITE_TAC[sigma_fan;FAN];\r
1498 NHANH UNI_E_IMP_EE_EQ_SET_OF_EDGE;\r
1499 SIMP_TAC[];\r
1500 STRIP_TAC;\r
1501 ASM_CASES_TAC ` set_of_edge (v:real^3) V E SUBSET {u} `;\r
1502 ASM_SIMP_TAC[W_SUBSET_SINGLETON_IMP_IDE];\r
1503 DOWN THEN DOWN THEN PHA;\r
1504 NHANH (SET_RULE` u IN S /\ S SUBSET {u} ==> S = {u} `);\r
1505 STRIP_TAC THEN ASM_REWRITE_TAC[];\r
1506 REWRITE_TAC[GSYM sigma_fan];\r
1507 UNDISCH_TAC `fan1 ((x:real^3),(V:real^3 -> bool),(E: (real^3 -> bool) -> bool)) `;\r
1508 REWRITE_TAC[fan1];\r
1509 NHANH remark_finite_fan1;\r
1510 STRIP_TAC;\r
1511 UNDISCH_TAC ` FINITE (set_of_edge (v:real^3) V E) `;\r
1512 UNDISCH_TAC ` ~( set_of_edge (v:real^3) V E SUBSET {u})`;\r
1513 PHA;\r
1514 NHANH (\r
1515 SPECL [`W:real^3 -> bool`;` p:real^3` ;`v:real^3`;` x:real^3`] \r
1516 (GEN_ALL AZIM_CYCLE_PROPERTIES));\r
1517 STRIP_TAC;\r
1518 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1519 MATCH_MP_TAC UNIQUE_SIGMA_FAN;\r
1520 ASM_REWRITE_TAC[FAN; IN; fan1];\r
1521 CONJ_TAC;\r
1522 MATCH_MP_TAC (SET_RULE` u IN S /\ ~( S SUBSET {u}) ==> ~( S = {u}) `);\r
1523 ASM_REWRITE_TAC[];\r
1524 ONCE_REWRITE_TAC[TAUT` a /\ b <=> b /\ a `];\r
1525 FIRST_X_ASSUM NHANH;\r
1526 GEN_TAC THEN IMP_TAC;\r
1527 STRIP_TAC;\r
1528 REAL_ARITH_TAC]);;\r
1529 \r
1530 \r
1531 \r
1532 \r
1533 \r
1534 let IVS_AZIM_AS_SIGMA_FAN = prove(\r
1535 ` FAN (x,V,E) /\ u IN set_of_edge v V E\r
1536 ==> ivs_azim_cycle (set_of_edge v V E) x v u =\r
1537           @xx. xx IN set_of_edge v V E /\ sigma_fan x V E v xx = u`,\r
1538 NHANH (REWRITE_RULE[ RIGHT_FORALL_IMP_THM; TAUT ` a/\ b ==> c \r
1539 <=> a ==> b ==> c `] (GEN_ALL AZIM_CYCLE_EQ_SIGMA_FAN)) THEN \r
1540 REWRITE_TAC[ivs_azim_cycle] THEN \r
1541 NHANH_PAT `\x. y /\ x ==> i ` (SET_RULE ` x IN a ==> ~( a = {} ) `) THEN \r
1542 SIMP_TAC[FAN; fan1] THEN \r
1543 NHANH UNI_E_IMP_EE_EQ_SET_OF_EDGE THEN \r
1544 STRIP_TAC THEN \r
1545 DOWN THEN \r
1546 ASM_REWRITE_TAC[] THEN \r
1547 SIMP_TAC[] THEN \r
1548 FIRST_X_ASSUM NHANH THEN \r
1549 ASM_REWRITE_TAC[] THEN \r
1550 PHA THEN \r
1551 REWRITE_TAC[MESON[]` a = b /\ a = c <=> a = b /\ b = c `]);;\r
1552 \r
1553 \r
1554 \r
1555 \r
1556 \r
1557 \r
1558 \r
1559 \r
1560 let IVS_AZIM_PROPERTIES = prove_by_refinement \r
1561 (` FAN (x,V,E) /\ u IN set_of_edge v V E\r
1562 ==> ivs_azim_cycle (set_of_edge v V E) x v u IN set_of_edge v V E /\\r
1563 sigma_fan x V E v (ivs_azim_cycle (set_of_edge v V E) x v u) = u `,\r
1564 [STRIP_TAC;\r
1565 ASSUME_TAC2 IVS_AZIM_AS_SIGMA_FAN;\r
1566 ASM_REWRITE_TAC[];\r
1567 CONV_TAC SELECT_CONV;\r
1568 MP_TAC (SPEC_ALL SUR_SIGMA_FAN);\r
1569 ANTS_TAC;\r
1570 ASM_REWRITE_TAC[];\r
1571 DOWN_TAC;\r
1572 SIMP_TAC[set_of_edge; IN_ELIM_THM];\r
1573 STRIP_TAC;\r
1574 EXISTS_TAC ` w:real^3 `;\r
1575 ASM_REWRITE_TAC[set_of_edge; IN_ELIM_THM];\r
1576 MATCH_MP_TAC (SET_RULE` UNIONS E SUBSET V /\ x IN UNIONS E ==> x IN V `);\r
1577 DOWN_TAC;\r
1578 REWRITE_TAC[FAN; fan1];\r
1579 SIMP_TAC[IN_UNIONS];\r
1580 STRIP_TAC;\r
1581 EXISTS_TAC ` {v,(w:real^3) }`;\r
1582 ASM_REWRITE_TAC[];\r
1583 SET_TAC[]]);;\r
1584 \r
1585 \r
1586 \r
1587 \r
1588 \r
1589 \r
1590 \r
1591 let IVS_AZIM_EQ_INVERSE_SIGMA_FAN = prove_by_refinement\r
1592 (`FAN (x,V,E) /\ {v,u} IN E\r
1593 ==> ivs_azim_cycle (EE v E ) x v u = inverse1_sigma_fan x V E v u `,\r
1594 [STRIP_TAC;\r
1595 ASSUME_TAC2 properties_of_set_of_edge_fan;\r
1596 UNDISCH_TAC ` {v,u:real^3 } IN E `;\r
1597 ASM_REWRITE_TAC[];\r
1598 STRIP_TAC;\r
1599 ASSUME_TAC2 IVS_AZIM_PROPERTIES;\r
1600 ASSUME_TAC2 INVERSE1_SIGMA_FAN;\r
1601 SUBGOAL_THEN ` {v,u:real^3} IN E ` MP_TAC;\r
1602 ASM_REWRITE_TAC[];\r
1603 DOWN THEN STRIP_TAC;\r
1604 DOWN THEN FIRST_X_ASSUM NHANH;\r
1605 FIRST_X_ASSUM NHANH;\r
1606 REPEAT STRIP_TAC;\r
1607 MATCH_MP_TAC (SPEC_ALL MONO_SIGMA_FAN);\r
1608 ASM_REWRITE_TAC[];\r
1609 UNDISCH_TAC ` FAN ((x:real^3),V,E) `;\r
1610 REWRITE_TAC[FAN; fan1];\r
1611 SIMP_TAC[UNI_E_IMP_EE_EQ_SET_OF_EDGE];\r
1612 ASM_REWRITE_TAC[]]);;\r
1613 \r
1614 \r
1615 \r
1616 \r
1617 \r
1618 \r
1619 \r
1620 let IVS_AZIM_EQ_INVERSE_SIGMA_FAN2 = prove(`FAN (x,V,E) /\ {v, u} IN E\r
1621      ==> ivs_azim_cycle (set_of_edge v V E) x v u =\r
1622  inverse1_sigma_fan x V E v u `,\r
1623 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN THEN \r
1624 REWRITE_TAC[FAN; fan1] THEN \r
1625 NHANH UNI_E_IMP_EE_EQ_SET_OF_EDGE THEN \r
1626 IMP_TAC THEN STRIP_TAC THEN \r
1627 ASM_REWRITE_TAC[]);;\r
1628 \r
1629 \r
1630 \r
1631 \r
1632 \r
1633 \r
1634 let EE_OF_HYP_PERMUTES_DARTS = prove_by_refinement\r
1635 (` (ee_of_hyp (x,V,E) ) permutes ( darts_of_hyp E V )`,\r
1636 [REWRITE_TAC[permutes];\r
1637 CONJ_TAC;\r
1638 SIMP_TAC[ee_of_hyp2];\r
1639 REWRITE_TAC[EXISTS_UNIQUE; ee_of_hyp2];\r
1640 GEN_TAC;\r
1641 ASM_CASES_TAC ` y IN darts_of_hyp E (V:real^3 -> bool) `;\r
1642 EXISTS_TAC `SND (y:real^3 # real^3 ), FST y `;\r
1643 DOWN;\r
1644 NHANH_PAT `\x. x ==> l ` V_IN_DARTS_IMP_SWICH_SO_DO;\r
1645 SIMP_TAC[];\r
1646 STRIP_TAC;\r
1647 GEN_TAC THEN COND_CASES_TAC;\r
1648 DISCH_TAC;\r
1649 EXPAND_TAC "y";\r
1650 REWRITE_TAC[];\r
1651 ASM_MESON_TAC[];\r
1652 EXISTS_TAC ` y:real^3 # real^3 `;\r
1653 ASM_REWRITE_TAC[];\r
1654 GEN_TAC THEN COND_CASES_TAC;\r
1655 DOWN;\r
1656 NHANH V_IN_DARTS_IMP_SWICH_SO_DO;\r
1657 ASM_MESON_TAC[];\r
1658 REWRITE_TAC[]]);;\r
1659 \r
1660 \r
1661 \r
1662 let EE_SUBSET_UNIONS_E = prove_by_refinement\r
1663 (` EE (v:A) E SUBSET UNIONS E `,\r
1664 [REWRITE_TAC[EE];\r
1665 REWRITE_TAC[SUBSET];\r
1666 GEN_TAC;\r
1667 REWRITE_TAC[IN_ELIM_THM; IN_UNIONS];\r
1668 STRIP_TAC;\r
1669 EXISTS_TAC ` ({v,(x:A) }) `;\r
1670 ASM_REWRITE_TAC[];\r
1671 SET_TAC[]]);;\r
1672 \r
1673 \r
1674 let FAN_IMP_FINITE_EE = prove(`\r
1675  FAN ((x:real^3),V,E) ==> FINITE ( EE v E ) `,\r
1676 REWRITE_TAC[FAN;fan2; fan1] THEN \r
1677 PHA THEN ONCE_REWRITE_TAC[TAUT` a /\ b /\ c /\ d <=> (c /\ a ) /\ b /\ d `]\r
1678 THEN NHANH FINITE_SUBSET THEN \r
1679 MESON_TAC[EE_SUBSET_UNIONS_E; FINITE_SUBSET]);;\r
1680 \r
1681 \r
1682 \r
1683 \r
1684 let SMOOTH_GEN_ALL t = \r
1685 REWRITE_RULE[ RIGHT_FORALL_IMP_THM; TAUT ` a/\ b ==> c <=> a ==> b ==> c `] (GEN_ALL t);;\r
1686 \r
1687 let W_SUBSET_SINGLETON_IMP_IDE = \r
1688 SMOOTH_GEN_ALL (GENL [`v:real^3 `;`w:real^3`] W_SUBSET_SINGLETON_IMP_IDE);;\r
1689 \r
1690 \r
1691 \r
1692 let IN_SELF_PAIRS_IMP_EE_EMPTY = prove(\r
1693 ` x IN self_pairs E V ==> EE (FST x) E = {} `,\r
1694 REWRITE_TAC[self_pairs; IN_ELIM_THM; EE] THEN \r
1695 STRIP_TAC THEN ASM_REWRITE_TAC[]);;\r
1696 \r
1697 \r
1698 \r
1699 \r
1700 let IN_DARTS_IFF_NN_OF_HYP_TOO = prove_by_refinement\r
1701 (` FAN (x,V,E) ==>\r
1702 ( y IN darts_of_hyp E V <=> nn_of_hyp (x,V,E) y IN darts_of_hyp E V )`,\r
1703 [DISCH_TAC THEN EQ_TAC;\r
1704 \r
1705 SIMP_TAC[nn_of_hyp2; darts_of_hyp; IN_UNION];\r
1706 STRIP_TAC;\r
1707 DISJ1_TAC;\r
1708 DOWN;\r
1709 NHANH IN_ORD_PAIRS_IMP_SND_IN_EE_FST;\r
1710 REWRITE_TAC[ord_pairs; IN_ELIM_THM];\r
1711 ASSUME_TAC2 (SPEC `FST (y:real^3 # real^ 3) ` (GEN `v:real^3` FAN_IMP_FINITE_EE));\r
1712 STRIP_TAC;\r
1713 DOWN;\r
1714 ASM_CASES_TAC ` (EE (FST y) E) SUBSET {SND (y:real^3 # real^3 )} `;\r
1715 DOWN;\r
1716 NHANH W_SUBSET_SINGLETON_IMP_IDE;\r
1717 SIMP_TAC[];\r
1718 ASM_MESON_TAC[];\r
1719 STRIP_TAC;\r
1720 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3)) E)`;\r
1721 UNDISCH_TAC ` ~(EE ((FST y):real^3) E SUBSET {SND y}) `;\r
1722 PHA;\r
1723 NHANH (REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `]\r
1724 (SMOOTH_GEN_ALL AZIM_CYCLE_PROPERTIES));\r
1725 STRIP_TAC;\r
1726 FIRST_X_ASSUM (MP_TAC o (SPECL [` FST (y:real^3 # real^ 3) `;` x:real^3 `]));\r
1727 STRIP_TAC;\r
1728 ASM_REWRITE_TAC[IN];\r
1729 UNDISCH_TAC `EE (FST y) E (azim_cycle (EE (FST y) E) x (FST y) (SND y)) `;\r
1730 ASM_REWRITE_TAC[];\r
1731 REWRITE_TAC[EE; IN_ELIM_THM; IN];\r
1732 MESON_TAC[];\r
1733 DISJ2_TAC;\r
1734 DOWN;\r
1735 NHANH IN_SELF_PAIRS_IMP_EE_EMPTY;\r
1736 SIMP_TAC[azim_cycle; EMPTY_SUBSET];\r
1737 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
1738 SIMP_TAC[nn_of_hyp2]]);;\r
1739 \r
1740 \r
1741 \r
1742 \r
1743 \r
1744 \r
1745 let IN_E_IMP_IMP_IN_DARTS = prove(\r
1746 ` {a,b} IN E ==> (a,b) IN darts_of_hyp E V `,\r
1747 REWRITE_TAC[darts_of_hyp; IN_UNION] THEN \r
1748 STRIP_TAC THEN DISJ1_TAC THEN \r
1749 REWRITE_TAC[ord_pairs; IN_ELIM_THM]\r
1750 THEN ASM_MESON_TAC[]);;\r
1751 \r
1752 \r
1753 \r
1754 \r
1755 \r
1756 let PAIR_EQ2 =\r
1757 MESON[PAIR; PAIR_EQ]` (a:A#B) = b <=> FST a = FST b /\ SND a = SND b `;;\r
1758 \r
1759 \r
1760 \r
1761 let IN_ORD_E_EQ_IN_E = prove(\r
1762 ` x IN ord_pairs E <=> {FST x, SND x } IN E `,\r
1763 REWRITE_TAC[ord_pairs; IN_ELIM_THM; PAIR_EQ2]\r
1764 THEN MESON_TAC[]);;\r
1765 \r
1766 \r
1767 \r
1768 \r
1769 \r
1770 let FAN_IMP_NN_OF_HYP_PERMUTES_DARTS = prove_by_refinement\r
1771 (`FAN (x,V,E) ==> nn_of_hyp (x,V,E) permutes darts_of_hyp E V `,\r
1772 [REWRITE_TAC[permutes];\r
1773 STRIP_TAC;\r
1774 CONJ_TAC;\r
1775 SIMP_TAC[nn_of_hyp2];\r
1776 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE];\r
1777 ASM_CASES_TAC ` y IN darts_of_hyp E (V:real^3 -> bool) `;\r
1778 ASSUME_TAC2 (SMOOTH_GEN_ALL INVERSE1_SIGMA_FAN);\r
1779 FIRST_X_ASSUM (MP_TAC o SPEC `FST (y:real^3 # real^3)`);\r
1780 STRIP_TAC;\r
1781 DOWN;\r
1782 FIRST_X_ASSUM (MP_TAC o SPEC `SND (y:real^3 # real^3)`);\r
1783 REPEAT STRIP_TAC;\r
1784 ASM_CASES_TAC ` (y:real^3 # real^3) IN self_pairs E V `;\r
1785 EXISTS_TAC `y:real^3 # real^3 `;\r
1786 REWRITE_TAC[nn_of_hyp2];\r
1787 ASM_REWRITE_TAC[];\r
1788 DOWN;\r
1789 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
1790 STRIP_TAC;\r
1791 ASM_SIMP_TAC[W_SUBSET_SINGLETON_IMP_IDE; EMPTY_SUBSET];\r
1792 GEN_TAC;\r
1793 COND_CASES_TAC;\r
1794 REWRITE_TAC[PAIR_EQ];\r
1795 DOWN;\r
1796 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
1797 STRIP_TAC;\r
1798 DOWN;\r
1799 REWRITE_TAC[ord_pairs; IN_ELIM_THM];\r
1800 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
1801 ASM_REWRITE_TAC[];\r
1802 STRIP_TAC;\r
1803 STRIP_TAC;\r
1804 UNDISCH_TAC ` b IN set_of_edge (a:real^3) V E`;\r
1805 UNDISCH_TAC ` FAN ((x:real^3),V,E) `;\r
1806 PHA;\r
1807 NHANH sigma_fan_in_set_of_edge;\r
1808 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
1809 DOWN;\r
1810 DOWN;\r
1811 ASM_REWRITE_TAC[];\r
1812 PHA;\r
1813 IMP_TAC;\r
1814 ASM_SIMP_TAC[EMPTY_SUBSET; W_SUBSET_SINGLETON_IMP_IDE];\r
1815 IMP_TAC;\r
1816 ASM_SIMP_TAC[EMPTY_SUBSET; W_SUBSET_SINGLETON_IMP_IDE];\r
1817 ONCE_REWRITE_TAC[GSYM PAIR];\r
1818 REWRITE_TAC[PAIR_EQ];\r
1819 ASM_SIMP_TAC[];\r
1820 SIMP_TAC[];\r
1821 EXISTS_TAC ` FST y, inverse1_sigma_fan x V E (FST y) (SND y) `;\r
1822 SUBGOAL_THEN ` nn_of_hyp (x,V,E) (FST y,inverse1_sigma_fan x V E (FST y) (SND y)) = y ` ASSUME_TAC;\r
1823 REWRITE_TAC[nn_of_hyp];\r
1824 UNDISCH_TAC ` y IN darts_of_hyp E (V:real^3 -> bool) `;\r
1825 PAT_REWRITE_TAC `\x. x ==> y ` [darts_of_hyp];\r
1826 ASM_REWRITE_TAC[IN_UNION];\r
1827 REWRITE_TAC[ord_pairs; IN_ELIM_THM];\r
1828 STRIP_TAC;\r
1829 SUBGOAL_THEN ` {FST (y:real^3 # real^3),\r
1830 inverse1_sigma_fan x V E (FST y) b} IN E ` ASSUME_TAC;\r
1831 ASM_MESON_TAC[PAIR; PAIR_EQ];\r
1832 DOWN THEN NHANH IN_E_IMP_IMP_IN_DARTS;\r
1833 STRIP_TAC THEN ASM_SIMP_TAC[];\r
1834 DOWN THEN ASM_SIMP_TAC[];\r
1835 \r
1836 STRIP_TAC;\r
1837 REWRITE_TAC[PAIR_EQ];\r
1838 SUBGOAL_THEN ` (inverse1_sigma_fan x V E a b) IN set_of_edge a V E `\r
1839 ASSUME_TAC;\r
1840 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
1841 FIRST_X_ASSUM (fun c -> REWRITE_TAC[GSYM c]);\r
1842 DOWN THEN DOWN;\r
1843 ASM_REWRITE_TAC[TAUT ` a ==> b ==> a `];\r
1844 DOWN;\r
1845 UNDISCH_TAC `FAN (x:real^3, V, E) `;\r
1846 PHA;\r
1847 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
1848 ASM_SIMP_TAC[];\r
1849 STRIP_TAC;\r
1850 UNDISCH_TAC ` {FST (y:real^3 # real^3), SND y} IN E\r
1851       ==> sigma_fan x V E (FST y) (inverse1_sigma_fan x V E (FST y) (SND y)) =\r
1852           SND y `;\r
1853 ANTS_TAC;\r
1854 ASM_SIMP_TAC[];\r
1855 ASM_SIMP_TAC[];\r
1856 ASM_REWRITE_TAC[];\r
1857 GEN_TAC;\r
1858 ASSUME_TAC2 (SMOOTH_GEN_ALL (GEN `y:real^3 # real^3`  IN_DARTS_IFF_NN_OF_HYP_TOO));\r
1859 REWRITE_TAC[nn_of_hyp2];\r
1860 COND_CASES_TAC;\r
1861 REWRITE_TAC[PAIR_EQ2];\r
1862 ASM_SIMP_TAC[];\r
1863 UNDISCH_TAC` nn_of_hyp (x,V,E) (FST y,inverse1_sigma_fan x V E (FST y) (SND y)) = y `;\r
1864 REWRITE_TAC[nn_of_hyp2];\r
1865 UNDISCH_TAC ` (y:real^3 # real^3) IN darts_of_hyp E V `;\r
1866 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
1867 ASM_SIMP_TAC[IN_ORD_E_EQ_IN_E];\r
1868 REWRITE_TAC[PAIR_EQ2];\r
1869 REPEAT STRIP_TAC;\r
1870 SUBGOAL_THEN ` (inverse1_sigma_fan x V E (FST y) (SND y)) IN\r
1871 set_of_edge (FST y) V E /\\r
1872 SND y' IN set_of_edge (FST y') V E ` MP_TAC;\r
1873 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
1874 FIRST_ASSUM (fun x -> REWRITE_TAC[GSYM x]);\r
1875 CONJ_TAC;\r
1876 ASM_MESON_TAC[];\r
1877 UNDISCH_TAC ` y' IN darts_of_hyp E (V:real^3 -> bool) `;\r
1878 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
1879 STRIP_TAC;\r
1880 DOWN;\r
1881 REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
1882 DOWN;\r
1883 NHANH IN_SELF_PAIRS_IMP_EE_EMPTY;\r
1884 STRIP_TAC;\r
1885 FIRST_X_ASSUM SUBST_ALL_TAC;\r
1886 UNDISCH_TAC `azim_cycle {} x (FST y') (SND y') = SND (y:real^3 # real^3)`;\r
1887 SIMP_TAC[W_SUBSET_SINGLETON_IMP_IDE; EMPTY_SUBSET];\r
1888 STRIP_TAC;\r
1889 FIRST_X_ASSUM SUBST_ALL_TAC;\r
1890 FIRST_X_ASSUM SUBST_ALL_TAC;\r
1891 FIRST_X_ASSUM ACCEPT_TAC;\r
1892 ASM_REWRITE_TAC[];\r
1893 STRIP_TAC;\r
1894 DOWN;\r
1895 UNDISCH_TAC ` FAN (x:real^3, V, E) `;\r
1896 PHA;\r
1897 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
1898 STRIP_TAC;\r
1899 UNDISCH_TAC ` inverse1_sigma_fan x V E (FST y) (SND y) IN set_of_edge (FST y) V E `;\r
1900 UNDISCH_TAC ` FAN (x:real^3, V, E) `;\r
1901 PHA;\r
1902 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
1903 STRIP_TAC;\r
1904 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
1905 UNDISCH_TAC ` SND (y':real^3 # real^3) IN set_of_edge (FST (y:real^3 # real^3)) V E`;\r
1906 FIRST_ASSUM (fun x -> REWRITE_TAC[ GSYM x]);\r
1907 ASM_MESON_TAC[MONO_SIGMA_FAN];\r
1908 ASM_MESON_TAC[];\r
1909 EXISTS_TAC ` y:real^3 # real^3 `;\r
1910 ASM_REWRITE_TAC[nn_of_hyp2];\r
1911 GEN_TAC;\r
1912 REWRITE_TAC[GSYM nn_of_hyp2];\r
1913 ASM_MESON_TAC[IN_DARTS_IFF_NN_OF_HYP_TOO; nn_of_hyp2]]);;\r
1914 \r
1915 \r
1916 \r
1917 \r
1918 \r
1919 let IVS_AZIM_EMPTY_IDE = prove(` ivs_azim_cycle {} x y t = t `,\r
1920 REWRITE_TAC[ivs_azim_cycle]);;\r
1921 \r
1922 \r
1923 \r
1924 \r
1925 \r
1926 \r
1927 let FAN_IMP_IN_DARTS_IFF_FF_TOO = prove_by_refinement\r
1928 (` FAN (x,V,E) ==>\r
1929 (y IN darts_of_hyp E V <=> ff_of_hyp (x,V,E) y IN darts_of_hyp E V)`,\r
1930 [STRIP_TAC;\r
1931 EQ_TAC;\r
1932 REWRITE_TAC[ff_of_hyp2];\r
1933 SIMP_TAC[darts_of_hyp; IN_UNION];\r
1934 STRIP_TAC;\r
1935 DISJ1_TAC;\r
1936 DOWN THEN REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
1937 DOWN THEN PHA;\r
1938 ONCE_REWRITE_TAC[INSERT_COMM];\r
1939 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN;\r
1940 SIMP_TAC[];\r
1941 NHANH (SMOOTH_GEN_ALL INVERSE1_SIGMA_FAN);\r
1942 IMP_TAC THEN STRIP_TAC;\r
1943 FIRST_X_ASSUM (MP_TAC o (SPEC ` SND (y:real^3 # real^3) `));\r
1944 STRIP_TAC;\r
1945 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` FST (y:real^3 # real^3) `));\r
1946 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` FST (y:real^3 # real^3) `));\r
1947 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` FST (y:real^3 # real^3) `));\r
1948 DOWN;\r
1949 ANTS_TAC;\r
1950 FIRST_X_ASSUM ACCEPT_TAC;\r
1951 SIMP_TAC[INSERT_COMM];\r
1952 DISJ2_TAC;\r
1953 DOWN;\r
1954 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
1955 STRIP_TAC;\r
1956 EXISTS_TAC ` v:real^3 `;\r
1957 ASM_SIMP_TAC[IVS_AZIM_EMPTY_IDE];\r
1958 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
1959 SIMP_TAC[ff_of_hyp2]]);;\r
1960 \r
1961 \r
1962 \r
1963 \r
1964 \r
1965 \r
1966 let IN_E_IFF_IN_ORD_E = prove(\r
1967 ` {a,b}  IN E <=> (a,b) IN ord_pairs E`,\r
1968 REWRITE_TAC[ord_pairs; IN_ELIM_THM]\r
1969 THEN MESON_TAC[PAIR_EQ]);;\r
1970 \r
1971 \r
1972 \r
1973 \r
1974 let IN_ORD_E_IFF_SWITCH_TOO = prove_by_refinement\r
1975 (` (x:A#A) IN ord_pairs E <=> (SND x, FST x) IN ord_pairs E  `,\r
1976 [REWRITE_TAC[ord_pairs; IN_ELIM_THM];\r
1977 EQ_TAC;\r
1978 STRIP_TAC;\r
1979 EXISTS_TAC`b:A`;\r
1980 EXISTS_TAC `a:A`;\r
1981 ASM_SIMP_TAC[INSERT_COMM];\r
1982 STRIP_TAC;\r
1983 EXISTS_TAC`b:A`;\r
1984 EXISTS_TAC `a:A`;\r
1985 DOWN;\r
1986 ASM_SIMP_TAC[INSERT_COMM; PAIR_EQ2]]);;\r
1987 \r
1988 \r
1989 \r
1990 \r
1991 \r
1992 let SIG_AND_INVERSE1_SIG = prove(` FAN (x,V,E) /\ {u,w} IN E ==>\r
1993 (sigma_fan x V E u w = v ==> inverse1_sigma_fan x V E u v =  w )`,\r
1994 NHANH (SMOOTH_GEN_ALL INVERSE1_SIGMA_FAN) THEN \r
1995 ASM_MESON_TAC[]);;\r
1996 \r
1997 \r
1998 let INVERSE1_SIG_AND_SIG = prove(` FAN (x,V,E) /\ {u,v} IN E ==>\r
1999 (inverse1_sigma_fan x V E u v = w ==> sigma_fan x V E u w = v ) `,\r
2000 NHANH (SMOOTH_GEN_ALL INVERSE1_SIGMA_FAN) THEN \r
2001 ASM_MESON_TAC[]);;\r
2002 \r
2003 \r
2004 \r
2005 \r
2006 \r
2007 \r
2008 let FAN_IMP_FACE_MAP_PERMUTES_DARTS = prove_by_refinement\r
2009 (` FAN (x,V,E) ==> ff_of_hyp (x,V,E) permutes darts_of_hyp E V `,\r
2010 [STRIP_TAC;\r
2011 REWRITE_TAC[permutes];\r
2012 CONJ_TAC;\r
2013 SIMP_TAC[ff_of_hyp2];\r
2014 GEN_TAC;\r
2015 REWRITE_TAC[EXISTS_UNIQUE];\r
2016 ASM_CASES_TAC ` (y:real^3 # real^3) IN darts_of_hyp E V `;\r
2017 FIRST_ASSUM MP_TAC;\r
2018 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
2019 STRIP_TAC;\r
2020 DOWN THEN REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
2021 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2022 PHA;\r
2023 ONCE_REWRITE_TAC[INSERT_COMM];\r
2024 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN;\r
2025 STRIP_TAC;\r
2026 ASSUME_TAC2 (SMOOTH_GEN_ALL INVERSE1_SIGMA_FAN);\r
2027 FIRST_X_ASSUM (MP_TAC o (SPEC ` FST (y:real^3 # real^3 )`));\r
2028 STRIP_TAC;\r
2029 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` SND (y:real^3 # real^3 )`));\r
2030 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` SND (y:real^3 # real^3 )`));\r
2031 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` SND (y:real^3 # real^3 )`));\r
2032 DOWN;\r
2033 ANTS_TAC;\r
2034 ONCE_REWRITE_TAC[INSERT_COMM];\r
2035 FIRST_X_ASSUM ACCEPT_TAC;\r
2036 STRIP_TAC;\r
2037 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
2038 UNDISCH_TAC `{SND (y:real^3 # real^3), FST y} IN E `;\r
2039 ONCE_REWRITE_TAC[INSERT_COMM];\r
2040 FIRST_ASSUM (fun x -> REWRITE_TAC[x]);\r
2041 UNDISCH_TAC ` FAN (x:real^3, V,E) `;\r
2042 PHA;\r
2043 NHANH sigma_fan_in_set_of_edge;\r
2044 FIRST_ASSUM (fun x -> REWRITE_TAC[GSYM x]);\r
2045 REWRITE_TAC[IN_E_IFF_IN_ORD_E];\r
2046 STRIP_TAC;\r
2047 EXISTS_TAC `sigma_fan x V E (FST y) (SND y), FST y `;\r
2048 ASM_REWRITE_TAC[ff_of_hyp; darts_of_hyp; IN_UNION];\r
2049 ONCE_REWRITE_TAC[IN_ORD_E_IFF_SWITCH_TOO];\r
2050 ASM_REWRITE_TAC[];\r
2051 SUBGOAL_THEN` FST y,\r
2052  ivs_azim_cycle (EE (FST y) E) x (FST y) (sigma_fan x V E (FST y) (SND y)) =\r
2053  y ` ASSUME_TAC;\r
2054 REWRITE_TAC[PAIR_EQ2];\r
2055 SUBGOAL_THEN ` {FST y, sigma_fan x V E (FST y) (SND y)} IN E ` ASSUME_TAC;\r
2056 ASM_REWRITE_TAC[];\r
2057 MATCH_MP_TAC sigma_fan_in_set_of_edge;\r
2058 ASM_REWRITE_TAC[];\r
2059 USE_FIRST ` !v u. {v, u} IN E <=> u IN set_of_edge (v:real^3) V E ` (fun x -> REWRITE_TAC[GSYM x ]);\r
2060 REWRITE_TAC[IN_E_IFF_IN_ORD_E];\r
2061 FIRST_X_ASSUM ACCEPT_TAC;\r
2062 DOWN;\r
2063 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2064 PHA;\r
2065 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN;\r
2066 SIMP_TAC[];\r
2067 STRIP_TAC;\r
2068 UNDISCH_TAC ` (y:real^3 # real^3) IN ord_pairs E `;\r
2069 REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
2070 FIRST_X_ASSUM NHANH;\r
2071 FIRST_X_ASSUM NHANH;\r
2072 SIMP_TAC[];\r
2073 ASM_SIMP_TAC[];\r
2074 GEN_TAC;\r
2075 ASM_CASES_TAC ` (y':real^3 # real^3) IN darts_of_hyp E V `;\r
2076 ASM_REWRITE_TAC[ff_of_hyp2; PAIR_EQ2];\r
2077 SIMP_TAC[];\r
2078 DOWN;\r
2079 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
2080 STRIP_TAC;\r
2081 DOWN;\r
2082 REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
2083 ONCE_REWRITE_TAC[INSERT_COMM];\r
2084 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2085 REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2086 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN;\r
2087 DOWN;\r
2088 REWRITE_TAC[PAIR_EQ2];\r
2089 REPEAT STRIP_TAC;\r
2090 UNDISCH_TAC `FST y,sigma_fan x V E (FST y) (SND y) IN ord_pairs E `;\r
2091 REWRITE_TAC[IN_ORD_E_EQ_IN_E];\r
2092 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2093 PHA;\r
2094 NHANH IVS_AZIM_EQ_INVERSE_SIGMA_FAN;\r
2095 STRIP_TAC;\r
2096 FIRST_X_ASSUM SUBST_ALL_TAC;\r
2097 UNDISCH_TAC ` ivs_azim_cycle (EE (SND (y':real^3 # real^3)) E) x (SND y')\r
2098  (FST y') = SND (y:real^3 # real^3) `;\r
2099 ASM_SIMP_TAC[];\r
2100 SUBGOAL_THEN` {FST (y:real^3 # real^3), FST (y':real^3 # real^3)} IN E ` ASSUME_TAC;\r
2101 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
2102 ASM_REWRITE_TAC[];\r
2103 UNDISCH_TAC `inverse1_sigma_fan x V E (FST y) (sigma_fan x V E (FST y) (SND y)) =\r
2104       SND y `;\r
2105 DOWN THEN DOWN;\r
2106 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2107 PHA;\r
2108 MESON_TAC[INVERSE1_SIG_AND_SIG];\r
2109 DOWN;\r
2110 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
2111 STRIP_TAC;\r
2112 ASM_REWRITE_TAC[];\r
2113 UNDISCH_TAC ` (y:real^3 # real^3) IN ord_pairs E `;\r
2114 NHANH IN_ORD_PAIRS_IMP_SND_IN_EE_FST;\r
2115 STRIP_TAC THEN STRIP_TAC;\r
2116 UNDISCH_TAC ` SND (y:real^3 # real^3) IN EE (FST y) E `;\r
2117 ASM_MESON_TAC[NOT_IN_EMPTY];\r
2118 ASM_SIMP_TAC[NOT_IN_EMPTY];\r
2119 ASM_MESON_TAC[FAN_IMP_IN_DARTS_IFF_FF_TOO];\r
2120 DOWN;\r
2121 REWRITE_TAC[self_pairs; IN_ELIM_THM; ff_of_hyp2];\r
2122 STRIP_TAC;\r
2123 EXISTS_TAC ` (v,v:real^3)`;\r
2124 DOWN;\r
2125 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2126 ASM_SIMP_TAC[ff_of_hyp2; IVS_AZIM_EMPTY_IDE];\r
2127 STRIP_TAC;\r
2128 GEN_TAC;\r
2129 COND_CASES_TAC;\r
2130 EXPAND_TAC "y";\r
2131 REWRITE_TAC[PAIR_EQ];\r
2132 STRIP_TAC;\r
2133 DOWN;\r
2134 FIRST_X_ASSUM SUBST_ALL_TAC;\r
2135 ASM_REWRITE_TAC[IVS_AZIM_EMPTY_IDE; PAIR_EQ2];\r
2136 SIMP_TAC[];\r
2137 REWRITE_TAC[];\r
2138 EXISTS_TAC `y:real^3 # real^3 `;\r
2139 ASM_REWRITE_TAC[ff_of_hyp2];\r
2140 ASM_MESON_TAC[FAN_IMP_IN_DARTS_IFF_FF_TOO; ff_of_hyp2]]);;\r
2141 \r
2142 \r
2143 \r
2144 \r
2145 \r
2146 let nn_of_hyp3 = prove_by_refinement\r
2147 (` nn_of_hyp (x,V,E) y = (if  ~( y IN darts_of_hyp E V ) \/ y IN self_pairs E V then y else ( FST y, (azim_cycle (EE (FST y) E ) x (FST y) (SND y))))`,\r
2148 [REWRITE_TAC[nn_of_hyp2];\r
2149 COND_CASES_TAC;\r
2150 REWRITE_TAC[];\r
2151 COND_CASES_TAC;\r
2152 DOWN;\r
2153 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
2154 STRIP_TAC;\r
2155 ASM_SIMP_TAC[W_SUBSET_SINGLETON_IMP_IDE; EMPTY_SUBSET];\r
2156 REWRITE_TAC[];\r
2157 REWRITE_TAC[]]);;\r
2158 \r
2159 \r
2160 let ff_of_hyp3 = prove_by_refinement\r
2161 (` ff_of_hyp (x,V,E) u = if ~( u IN darts_of_hyp E V) \/ u IN self_pairs E V\r
2162 then u else SND u,ivs_azim_cycle (EE (SND u) E) x (SND u) (FST u) `,\r
2163 [REWRITE_TAC[ff_of_hyp2];\r
2164 COND_CASES_TAC;\r
2165 ASM_REWRITE_TAC[];\r
2166 COND_CASES_TAC;\r
2167 DOWN;\r
2168 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
2169 STRIP_TAC;\r
2170 ASM_SIMP_TAC[IVS_AZIM_EMPTY_IDE];\r
2171 REWRITE_TAC[];\r
2172 REWRITE_TAC[]]);;\r
2173 \r
2174 \r
2175 \r
2176 \r
2177 let FAN_IMP_FIMITE_DARTS = prove_by_refinement\r
2178 (` FAN ((x:real^N),V,E) ==> FINITE (darts_of_hyp E V) `,\r
2179 [REWRITE_TAC[FAN; fan1];\r
2180 NHANH_PAT `\x. x ==> l ` (TAUT` FINITE S ==> FINITE S `);\r
2181 NHANH FINITE_PRODUCT;\r
2182 STRIP_TAC;\r
2183 UNDISCH_TAC ` FINITE {x,(y:real^N) | x IN V /\ y IN V}`;\r
2184 MATCH_MP_TAC (REWRITE_RULE[TAUT` a /\ b ==> c <=> b ==> a ==> c `]FINITE_SUBSET);\r
2185 REWRITE_TAC[darts_of_hyp; SUBSET; IN_UNION; ord_pairs; self_pairs; IN_ELIM_THM];\r
2186 REPEAT STRIP_TAC;\r
2187 EXISTS_TAC `a:real^N`;\r
2188 EXISTS_TAC `b:real^N`;\r
2189 ASM_REWRITE_TAC[];\r
2190 DOWN_TAC;\r
2191 NHANH lemma_sub_support;\r
2192 REWRITE_TAC[INSERT_SUBSET; SUBSET];\r
2193 MESON_TAC[];\r
2194 ASM_MESON_TAC[]]);;\r
2195 \r
2196 \r
2197 \r
2198 \r
2199 \r
2200 let FAN_IMP_EE_EQ_SET_OF_EDGE = prove(\r
2201 ` FAN ((x:real^N),V,E) ==> EE v E = set_of_edge v V E `,\r
2202 SIMP_TAC[FAN; UNI_E_IMP_EE_EQ_SET_OF_EDGE]);;\r
2203 \r
2204 \r
2205 \r
2206 \r
2207 let FAN_IMP_IN_SELF_PAIRS_IFF_FF_OF_HYP = prove_by_refinement\r
2208 (` FAN (x,V,E) ==>\r
2209 (y IN self_pairs E V <=> ff_of_hyp (x,V,E) y IN self_pairs E V )`,\r
2210 [STRIP_TAC;\r
2211 EQ_TAC;\r
2212 SIMP_TAC[ff_of_hyp3];\r
2213 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
2214 SIMP_TAC[ff_of_hyp3];\r
2215 STRIP_TAC;\r
2216 COND_CASES_TAC;\r
2217 FIRST_X_ASSUM ACCEPT_TAC;\r
2218 DOWN;\r
2219 ASM_REWRITE_TAC[darts_of_hyp; IN_UNION; IN_ORD_E_EQ_IN_E];\r
2220 ASSUME_TAC2 (SMOOTH_GEN_ALL properties_of_set_of_edge_fan);\r
2221 ONCE_REWRITE_TAC[INSERT_COMM];\r
2222 ASM_REWRITE_TAC[];\r
2223 UNDISCH_TAC `FAN (x:real^3,V,E) `;\r
2224 PHA;\r
2225 NHANH IVS_AZIM_PROPERTIES;\r
2226 STRIP_TAC;\r
2227 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2228 NHANH (SMOOTH_GEN_ALL (GEN `v:real^N` FAN_IMP_EE_EQ_SET_OF_EDGE));\r
2229 SIMP_TAC[];\r
2230 STRIP_TAC;\r
2231 REWRITE_TAC[self_pairs; IN_ELIM_THM; PAIR_EQ];\r
2232 STRIP_TAC;\r
2233 ASM_MESON_TAC[NOT_IN_EMPTY]]);;\r
2234 \r
2235 \r
2236 \r
2237 \r
2238 \r
2239 \r
2240 \r
2241 \r
2242 \r
2243 \r
2244 let FIRST_AAUHTVE = prove_by_refinement\r
2245 (`FAN (x,V,E) /\ HYP (x,V,E) = D,e,n,f\r
2246    ==> FINITE D /\\r
2247        e permutes D /\\r
2248        n permutes D /\\r
2249        f permutes D /\\r
2250        e o n o f = I /\\r
2251        e o e = I `,\r
2252 [NHANH FAN_IMP_NN_OF_HYP_PERMUTES_DARTS;\r
2253 NHANH FAN_IMP_FACE_MAP_PERMUTES_DARTS;\r
2254 REWRITE_TAC[HYP; PAIR_EQ; FAN; fan1; fan2];\r
2255 STRIP_TAC;\r
2256 CONJ_TAC;\r
2257 EXPAND_TAC "D";\r
2258 MATCH_MP_TAC FAN_IMP_FIMITE_DARTS;\r
2259 ASM_REWRITE_TAC[FAN;fan1; fan2];\r
2260 EXPAND_TAC "e";\r
2261 EXPAND_TAC "D";\r
2262 REWRITE_TAC[EE_OF_HYP_PERMUTES_DARTS];\r
2263 CONJ_TAC;\r
2264 ASM_MESON_TAC[];\r
2265 CONJ_TAC;\r
2266 ASM_MESON_TAC[];\r
2267 CONJ_TAC;\r
2268 EXPAND_TAC "n";\r
2269 EXPAND_TAC "f";\r
2270 REWRITE_TAC[FUN_EQ_THM];\r
2271 GEN_TAC;\r
2272 REWRITE_TAC[o_THM; I_THM; ff_of_hyp3];\r
2273 ASM_CASES_TAC ` ~(x' IN darts_of_hyp E (V:real^3 -> bool)) \/ x' IN self_pairs E V `;\r
2274 ASM_SIMP_TAC[];\r
2275 EXPAND_TAC "n";\r
2276 REWRITE_TAC[nn_of_hyp3];\r
2277 ASM_REWRITE_TAC[];\r
2278 EXPAND_TAC "e";\r
2279 REWRITE_TAC[ee_of_hyp2];\r
2280 DOWN;\r
2281 ASM_REWRITE_TAC[];\r
2282 DISCH_THEN DISJ_CASES_TAC;\r
2283 ASM_REWRITE_TAC[];\r
2284 DOWN;\r
2285 EXPAND_TAC "D";\r
2286 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
2287 SIMP_TAC[self_pairs; IN_ELIM_THM];\r
2288 STRIP_TAC;\r
2289 ASM_REWRITE_TAC[];\r
2290 DOWN;\r
2291 SIMP_TAC[];\r
2292 REWRITE_TAC[nn_of_hyp3];\r
2293 SIMP_TAC[];\r
2294 SUBGOAL_THEN ` FAN (x:real^3, V, E) ` ASSUME_TAC;\r
2295 ASM_REWRITE_TAC[FAN;fan1;fan2];\r
2296 \r
2297 ASSUME_TAC2 (SMOOTH_GEN_ALL (GEN `y:real^3 # real^3 ` FAN_IMP_IN_DARTS_IFF_FF_TOO));\r
2298 ASSUME_TAC2 (SMOOTH_GEN_ALL (GEN `y:real^3 # real^3 ` FAN_IMP_IN_SELF_PAIRS_IFF_FF_OF_HYP));\r
2299 NHANH (TAUT` ~ a ==> ~ a `);\r
2300 FIRST_X_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC` \x. y /\ x ==> i ` [x]);\r
2301 FIRST_X_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC` \x. y /\ x ==> i ` [x]);\r
2302 IMP_TAC;\r
2303 STRIP_TAC;\r
2304 REWRITE_TAC[ff_of_hyp3];\r
2305 ASM_REWRITE_TAC[];\r
2306 EXPAND_TAC "n";\r
2307 REWRITE_TAC[nn_of_hyp3];\r
2308 ASM_SIMP_TAC[];\r
2309 ASSUME_TAC2 (\r
2310 SMOOTH_GEN_ALL (GEN `y:real^3# real^3 ` IN_DARTS_IFF_NN_OF_HYP_TOO));\r
2311 NHANH (TAUT` ~ a ==> ~ a `);\r
2312 EXPAND_TAC "D";\r
2313 FIRST_X_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC` \x. y /\ x ==> i ` [x]);\r
2314 REWRITE_TAC[DE_MORGAN_THM];\r
2315 IMP_TAC;\r
2316 SIMP_TAC[nn_of_hyp2];\r
2317 EXPAND_TAC "e";\r
2318 SIMP_TAC[ee_of_hyp];\r
2319 REPEAT STRIP_TAC;\r
2320 REWRITE_TAC[PAIR_EQ2];\r
2321 SUBGOAL_THEN ` (ivs_azim_cycle (EE (SND x') E) x (SND x') (FST x')) IN\r
2322 set_of_edge (SND x') V E ` ASSUME_TAC;\r
2323 ASSUME_TAC2 (SMOOTH_GEN_ALL (GSYM properties_of_set_of_edge_fan));\r
2324 ASM_REWRITE_TAC[IN_E_IFF_IN_ORD_E];\r
2325 UNDISCH_TAC ` SND x',ivs_azim_cycle (EE (SND x') E) x (SND x') (FST x') IN\r
2326       darts_of_hyp E V `;\r
2327 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
2328 ASM_REWRITE_TAC[];\r
2329 DOWN;\r
2330 UNDISCH_TAC `FAN (x:real^3,V,E) `;\r
2331 PHA;\r
2332 NHANH AZIM_CYCLE_EQ_SIGMA_FAN;\r
2333 SIMP_TAC[];\r
2334 STRIP_TAC;\r
2335 ASSUME_TAC2 (SMOOTH_GEN_ALL (GSYM properties_of_set_of_edge_fan));\r
2336 SUBGOAL_THEN ` FST (x':real^3 # real^3) IN set_of_edge (SND x') V E `\r
2337 MP_TAC;\r
2338 ASM_REWRITE_TAC[IN_E_IFF_IN_ORD_E];\r
2339 ONCE_REWRITE_TAC[IN_ORD_E_IFF_SWITCH_TOO];\r
2340 REWRITE_TAC[];\r
2341 UNDISCH_TAC ` ~(~(x' IN darts_of_hyp E (V:real^3 -> bool)) \/ x' IN self_pairs E V)  `;\r
2342 REWRITE_TAC[DE_MORGAN_THM; darts_of_hyp; IN_UNION];\r
2343 CONV_TAC TAUT;\r
2344 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2345 PHA;\r
2346 NHANH IVS_AZIM_PROPERTIES;\r
2347 NHANH (\r
2348 SMOOTH_GEN_ALL (GEN `v:real^N ` FAN_IMP_EE_EQ_SET_OF_EDGE));\r
2349 SIMP_TAC[];\r
2350 \r
2351 \r
2352 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM];\r
2353 GEN_TAC;\r
2354 ASM_CASES_TAC ` (x':real^3 # real^3) IN D `;\r
2355 REWRITE_TAC[ee_of_hyp2];\r
2356 ASM_REWRITE_TAC[];\r
2357 DOWN;\r
2358 EXPAND_TAC "D";\r
2359 SIMP_TAC[V_IN_DARTS_IFF_SWICH_SO_DO];\r
2360 ASM_REWRITE_TAC[ee_of_hyp2]]);;\r
2361 \r
2362 \r
2363 \r
2364 let HYP_LEMMA = prove_by_refinement(\r
2365 `! (x:real^3). FAN (x,V,E) ==> \r
2366 tuple_hypermap (hypermap (HYP (x,V,E))) = HYP (x,V,E) `,\r
2367 [GEN_TAC THEN ABBREV_TAC ` D = FST (HYP (x,V,E)) `;\r
2368 ABBREV_TAC ` e = FST ( SND (HYP (x,V,E))) `;\r
2369 ABBREV_TAC `n = FST (SND (SND (HYP (x,V,E)))) `;\r
2370 ABBREV_TAC `f = SND (SND (SND (HYP (x,V,E)))) `;\r
2371 REPEAT (DOWN THEN ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `]);\r
2372 PHA;\r
2373 REWRITE_TAC[FST_SND_FORM_OF_4_TUPLE];\r
2374 NHANH (FIRST_AAUHTVE);\r
2375 SIMP_TAC[];\r
2376 SIMP_TAC[GSYM hypermap_tybij]]);;\r
2377 \r
2378 \r
2379 \r
2380 \r
2381 \r
2382 \r
2383 \r
2384 let ELMS_OF_HYPERMAP_HYP = prove_by_refinement\r
2385 (`FAN (x,V,E)\r
2386  ==> dart (hypermap (HYP (x,V,E))) = darts_of_hyp E V /\\r
2387      edge_map (hypermap (HYP (x,V,E))) = ee_of_hyp (x,V,E) /\\r
2388      node_map (hypermap (HYP (x,V,E))) = nn_of_hyp (x,V,E) /\\r
2389      face_map (hypermap (HYP (x,V,E))) = ff_of_hyp (x,V,E)`,\r
2390 [REWRITE_TAC[dart;edge_map; node_map; face_map];\r
2391 SIMP_TAC[HYP_LEMMA; HYP]]);;\r
2392 \r
2393 \r
2394 \r
2395 \r
2396 let NN_OF_HYP_POWER_IDE = prove(\r
2397 ` ~ ( y IN darts_of_hyp E V ) \/ y IN self_pairs E V \r
2398 ==> ! n. (nn_of_hyp (x,V,E) POWER n) y = y `,\r
2399 DISCH_TAC THEN INDUCT_TAC THENL\r
2400 [REWRITE_TAC[POWER; I_THM];\r
2401 ASM_REWRITE_TAC[COM_POWER; o_THM] THEN\r
2402 ASM_REWRITE_TAC[nn_of_hyp3]]);;\r
2403 \r
2404 \r
2405 let XX_SS_TT = prove_by_refinement\r
2406 (` FAN (x,V,E) /\ y IN ord_pairs E ==> SND ( nn_of_hyp (x,V,E) y) IN EE (FST y) E `,\r
2407 [REWRITE_TAC[nn_of_hyp2; darts_of_hyp; IN_UNION];\r
2408 SIMP_TAC[];\r
2409 NHANH (SMOOTH_GEN_ALL (GEN` v:real^3 ` FAN_IMP_FINITE_EE));\r
2410 STRIP_TAC;\r
2411 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` FST (y:real^3 # real^3)`));\r
2412 DOWN_TAC THEN NHANH IN_ORD_PAIRS_IMP_SND_IN_EE_FST;\r
2413 STRIP_TAC;\r
2414 ASM_CASES_TAC ` EE (FST (y:real^3 # real^3)) E SUBSET {SND y} `;\r
2415 ASM_REWRITE_TAC[azim_cycle];\r
2416 UNDISCH_TAC ` FINITE (EE (FST (y:real^3 # real^3 )) E) `;\r
2417 DOWN;\r
2418 PHA;\r
2419 NHANH (SMOOTH_GEN_ALL AZIM_CYCLE_PROPERTIES);\r
2420 SIMP_TAC[IN]]);;\r
2421 \r
2422 \r
2423 \r
2424 let IN_ORD_PAIRS_IMP_NN_OF_HYP_IN_ORD =\r
2425 prove(`FAN (x,V,E) /\ y IN ord_pairs E\r
2426      ==> (nn_of_hyp (x,V,E) y) IN ord_pairs E `,\r
2427 NHANH XX_SS_TT THEN IMP_TAC THEN \r
2428 SIMP_TAC[nn_of_hyp2; darts_of_hyp; IN_UNION] THEN \r
2429 REWRITE_TAC[EE; ord_pairs; IN_ELIM_THM] THEN \r
2430 MESON_TAC[]);;\r
2431 \r
2432 \r
2433 \r
2434 \r
2435 \r
2436 \r
2437 let NN_OF_HYP_POWER_IN_ORD_PAIRS = prove_by_refinement\r
2438 (` FAN (x,V,E) /\ y IN ord_pairs E \r
2439 ==> ! n. ((nn_of_hyp (x,V,E) POWER n ) y) IN ord_pairs E `,\r
2440 [STRIP_TAC; INDUCT_TAC;\r
2441 ASM_REWRITE_TAC[POWER; I_THM];\r
2442 REWRITE_TAC[COM_POWER; o_THM];\r
2443 ASM_MESON_TAC[IN_ORD_PAIRS_IMP_NN_OF_HYP_IN_ORD]]);;\r
2444 \r
2445 \r
2446 \r
2447 \r
2448 \r
2449 \r
2450 let N_HYP_TO_AZIM_CYCLE_LEM = \r
2451 prove_by_refinement (\r
2452 `FAN (x,V,E) /\ u,v IN darts_of_hyp E V ==> !n. (nn_of_hyp (x,V,E) POWER n) (u,v) = u,((azim_cycle (EE u E) x u) POWER n) v`,\r
2453 [STRIP_TAC;\r
2454 INDUCT_TAC;\r
2455 REWRITE_TAC[POWER; I_THM];\r
2456 ABBREV_TAC ` y = (u:real^3, v:real^3 ) `;\r
2457 ASM_CASES_TAC ` (y:real^3 # real^3) IN self_pairs E V `;\r
2458 SUBGOAL_THEN ` ! n.  (nn_of_hyp (x,V,E) POWER n) (y:real^3 # real^3) IN self_pairs E V ` ASSUME_TAC;\r
2459 INDUCT_TAC;\r
2460 ASM_REWRITE_TAC[POWER; I_THM];\r
2461 ASM_REWRITE_TAC[COM_POWER; I_THM];\r
2462 DOWN;\r
2463 STRIP_TAC;\r
2464 REWRITE_TAC[COM_POWER; o_THM];\r
2465 ABBREV_TAC ` tr = (nn_of_hyp ((x:real^3),V,E) POWER n') y`;\r
2466 ASM_REWRITE_TAC[nn_of_hyp3; IN_UNION];\r
2467 ASM_REWRITE_TAC[COM_POWER];\r
2468 ASM_REWRITE_TAC[o_THM; nn_of_hyp3];\r
2469 REWRITE_TAC[PAIR_EQ];\r
2470 DOWN THEN DOWN THEN PHA;\r
2471 EXPAND_TAC "y";\r
2472 REWRITE_TAC[self_pairs; IN_ELIM_THM; PAIR_EQ];\r
2473 STRIP_TAC;\r
2474 ASM_SIMP_TAC[W_SUBSET_SINGLETON_IMP_IDE; EMPTY_SUBSET];\r
2475 SUBGOAL_THEN ` ! n . (nn_of_hyp (x,V,E) POWER n) y IN darts_of_hyp E V `\r
2476 ASSUME_TAC;\r
2477 INDUCT_TAC;\r
2478 ASM_REWRITE_TAC[POWER; I_THM];\r
2479 REWRITE_TAC[COM_POWER; o_THM];\r
2480 ASM_MESON_TAC[IN_DARTS_IFF_NN_OF_HYP_TOO];\r
2481 ASM_REWRITE_TAC[COM_POWER; o_THM; nn_of_hyp2]]);;\r
2482 \r
2483 \r
2484 \r
2485 let iter_sigma_fan_in_set_of_edge =\r
2486 prove_by_refinement(`!x V E v u.\r
2487          FAN (x,V,E) /\ u IN set_of_edge v V E\r
2488          ==> ! n. ITER n (sigma_fan x V E v) u IN set_of_edge v V E`,\r
2489 [REPEAT GEN_TAC;\r
2490 STRIP_TAC; INDUCT_TAC;\r
2491 ASM_REWRITE_TAC[ITER];\r
2492 ASM_REWRITE_TAC[ITER];\r
2493 ASM_MESON_TAC[sigma_fan_in_set_of_edge]]);;\r
2494 \r
2495 \r
2496 \r
2497 \r
2498 \r
2499 let ITER_AZIM_CYCLE_EQ_ITER_SIGMA = prove_by_refinement\r
2500 (`FAN (x,V,E) /\ {v, u} IN E\r
2501  ==> (!a. a IN EE v E\r
2502           ==> (!n. ITER n (azim_cycle (EE v E) x v) a =\r
2503                    ITER n (sigma_fan x V E v) a))`,\r
2504 [NHANH (SMOOTH_GEN_ALL AZIM_CYCLE_EQ_SIGMA_FAN);\r
2505 STRIP_TAC THEN STRIP_TAC;\r
2506 DISCH_TAC;\r
2507 INDUCT_TAC;\r
2508 REWRITE_TAC[ITER];\r
2509 ASM_REWRITE_TAC[ITER];\r
2510 DOWN_TAC;\r
2511 NHANH (SMOOTH_GEN_ALL (GEN `v:real^N` FAN_IMP_EE_EQ_SET_OF_EDGE));\r
2512 IMP_TAC;\r
2513 SIMP_TAC[];\r
2514 STRIP_TAC THEN STRIP_TAC;\r
2515 UNDISCH_TAC ` (a:real^3) IN set_of_edge v V E`;\r
2516 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2517 PHA;\r
2518 NHANH iter_sigma_fan_in_set_of_edge;\r
2519 ASM_MESON_TAC[AZIM_CYCLE_EQ_SIGMA_FAN]]);;\r
2520 \r
2521 \r
2522 \r
2523 \r
2524 \r
2525 let pmp_to_iter = prove(\r
2526 `!n. power_map_points f x V E v w n = ITER n (f x V E v) w `,\r
2527 INDUCT_TAC THENL [\r
2528 REWRITE_TAC[power_map_points; ITER];\r
2529 ASM_REWRITE_TAC[power_map_points; ITER]]);;\r
2530 \r
2531 \r
2532 \r
2533 \r
2534 \r
2535 let CYCLIC_SET_IMP_STABLE_SET2 = prove_by_refinement\r
2536 (`FAN (x,V,E) /\ {v, u} IN E\r
2537  ==> (!a. a IN EE v E\r
2538           ==> EE v E = {y | ?n. y = ITER n (azim_cycle (EE v E) x v) a})`,\r
2539 [NHANH ITER_AZIM_CYCLE_EQ_ITER_SIGMA;\r
2540 SIMP_TAC[];\r
2541 NHANH (SMOOTH_GEN_ALL (GEN `v:real^N` FAN_IMP_EE_EQ_SET_OF_EDGE));\r
2542 SIMP_TAC[];\r
2543 NHANH (SMOOTH_GEN_ALL AZIM_CYCLE_EQ_SIGMA_FAN);\r
2544 NHANH (\r
2545 SMOOTH_GEN_ALL (GSYM properties_of_set_of_edge_fan));\r
2546 SIMP_TAC[];\r
2547 STRIP_TAC;\r
2548 GEN_TAC;\r
2549 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2550 PHA;\r
2551 NHANH ORBITS_EQ_SET_EDGE_FAN;\r
2552 SIMP_TAC[];\r
2553 REPEAT STRIP_TAC;\r
2554 REWRITE_TAC[set_of_orbits_points_fan; power_map_points];\r
2555 REWRITE_TAC[pmp_to_iter; FUN_EQ_THM; IN_ELIM_THM];\r
2556 REWRITE_TAC[ARITH_RULE ` 0 <= n `]]);;\r
2557 \r
2558 \r
2559 \r
2560 \r
2561 let FAN_IMP_BIJ_V_NODE_OF_HYP = \r
2562 prove_by_refinement(`FAN ((x:real^3),V,E) /\\r
2563  f =\r
2564  (\u. if u IN V\r
2565       then node (hypermap (HYP (x,V,E))) (u,choose_nd_point u E V)\r
2566       else {})\r
2567  ==> BIJ f V {node (hypermap (HYP (x,V,E))) y | y | y IN darts_of_hyp E V}`,\r
2568 [STRIP_TAC;\r
2569 ASM_SIMP_TAC[];\r
2570 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);\r
2571 ASSUME_TAC choose_nd_point;\r
2572 REWRITE_TAC[BIJ] THEN CONJ_TAC;\r
2573 (* subgoal 1 *)\r
2574 REWRITE_TAC[INJ] THEN CONJ_TAC;\r
2575 (* subgoal 1.1 *)\r
2576 GEN_TAC THEN SIMP_TAC[];\r
2577 UNDISCH_TAC `FAN ((x:real^3),V,E) `;\r
2578 REWRITE_TAC[FAN] THEN REPEAT STRIP_TAC;\r
2579 ASM SET_TAC[];\r
2580 (* subgoal 1.2 *)\r
2581 IMP_TAC THEN IMP_TAC THEN SIMP_TAC[];\r
2582 NHANH (MESON[X_IN_HYP_ORBITS] `node H (x:A) = A ==> x IN A `);\r
2583 REPEAT STRIP_TAC;\r
2584 DOWN;\r
2585 ASM_SIMP_TAC[node; ELMS_OF_HYPERMAP_HYP; orbit_map; IN_ELIM_THM];\r
2586 STRIP_TAC;\r
2587 \r
2588 \r
2589 DOWN;\r
2590 SUBGOAL_THEN ` y:real^3 IN V ` MP_TAC;\r
2591 \r
2592 FIRST_ASSUM ACCEPT_TAC;\r
2593 SUBGOAL_THEN ` UNIONS E SUBSET (V:real^3 -> bool) ` MP_TAC;\r
2594 UNDISCH_TAC ` FAN (x:real^3,V,E) `;\r
2595 SIMP_TAC[FAN];\r
2596 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2597 NHANH choose_nd_point;\r
2598 IMP_TAC;\r
2599 REMOVE_TAC;\r
2600 IMP_TAC THEN REMOVE_TAC;\r
2601 SUBGOAL_THEN ` FAN (x:real^3, V,E) ` MP_TAC;\r
2602 ASM_REWRITE_TAC[];\r
2603 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2604 SIMP_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
2605 REMOVE_TAC;\r
2606 \r
2607 \r
2608 SIMP_TAC[PAIR_EQ];\r
2609 (* suggoal 2 *)\r
2610 REWRITE_TAC[SURJ] THEN CONJ_TAC;\r
2611 (* subgoal 2.1 *)\r
2612 GEN_TAC THEN SIMP_TAC[];\r
2613 UNDISCH_TAC `FAN ((x:real^3),V,E) `;\r
2614 REWRITE_TAC[FAN] THEN REPEAT STRIP_TAC;\r
2615 ASM SET_TAC[];\r
2616 (* subgaol 2.2 *)\r
2617 GEN_TAC;\r
2618 REWRITE_TAC[IN_ELIM_THM];\r
2619 STRIP_TAC;\r
2620 EXISTS_TAC ` FST (y:real^3 # real^3 )`;\r
2621 UNDISCH_TAC ` FAN ((x:real^3),V,E) `;\r
2622 REWRITE_TAC[FAN] THEN STRIP_TAC;\r
2623 ASSUME_TAC2 (ISPECL [`E:(real^3 -> bool) -> bool `;\r
2624 ` y: real^3 # real^3`;`V:real^3 -> bool `]\r
2625   (GEN_ALL IN_DARTS_HYP_IMP_FST_SND_IN_V));\r
2626 ASM_SIMP_TAC[node; REWRITE_RULE[FAN] ELMS_OF_HYPERMAP_HYP];\r
2627 MP_TAC (ISPECL [`x: real^3 `;` V:real^3 -> bool `;\r
2628 ` E: (real^3 -> bool) -> bool`;\r
2629   `FST (y:real^3# real^3 ) `] XOHLED);\r
2630 ANTS_TAC;\r
2631 REPLICATE_TAC 5 DOWN;\r
2632 PHA THEN ASM_SIMP_TAC[FAN];\r
2633 \r
2634 \r
2635 REWRITE_TAC[orbit_map];\r
2636 \r
2637 SUBGOAL_THEN ` FST (y:real^3#real^3) IN V ` MP_TAC;\r
2638 ASM_REWRITE_TAC[];\r
2639 SUBGOAL_THEN ` UNIONS E SUBSET (V:real^3 -> bool) ` MP_TAC;\r
2640 ASM_REWRITE_TAC[];\r
2641 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2642 NHANH choose_nd_point;\r
2643 IMP_TAC;\r
2644 REMOVE_TAC;\r
2645 IMP_TAC THEN REMOVE_TAC;\r
2646 SUBGOAL_THEN ` FAN (x:real^3, V,E) ` MP_TAC;\r
2647 ASM_REWRITE_TAC[FAN];\r
2648 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2649 SIMP_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
2650 REMOVE_TAC;\r
2651 \r
2652 MP_TAC (ISPEC `y: real^3#real^3` (GSYM PAIR));\r
2653 ABBREV_TAC `fy = FST (y:real^3#real^3)`;\r
2654 ABBREV_TAC `sy = SND (y:real^3#real^3)`;\r
2655 \r
2656 (*\r
2657 e (SIMP_TAC[N_HYP_TO_AZIM_CYCLE_LEM]);;\r
2658 \r
2659 *)\r
2660 \r
2661 \r
2662 \r
2663 STRIP_TAC;\r
2664 SUBGOAL_THEN ` (y:real^3 # real^3) IN darts_of_hyp E V ` MP_TAC;\r
2665 ASM_REWRITE_TAC[];\r
2666 SUBGOAL_THEN ` FAN (x:real^3, V,E) ` MP_TAC;\r
2667 ASM_REWRITE_TAC[FAN];\r
2668 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
2669 FIRST_ASSUM (fun x -> REWRITE_TAC[x]);\r
2670 SIMP_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
2671 REMOVE_TAC;\r
2672 DOWN;\r
2673 (* ==================================== *)\r
2674 DISCH_TAC;\r
2675 FIRST_X_ASSUM (MP_TAC o (SPECL [`fy: real^3 `]));\r
2676 \r
2677 DISCH_THEN (MP_TAC o SPEC_ALL) THEN ANTS_TAC;\r
2678 (* sub I *)\r
2679 ASM_SIMP_TAC[];\r
2680 (* sub II *)\r
2681 REPEAT STRIP_TAC;\r
2682 ASSUME_TAC2 (SPEC_ALL (ISPECL [`fy:real^3`] (GEN_ALL UNI_E_IMP_EE_EQ_SET_OF_EDGE)));\r
2683 FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);\r
2684 ASM_CASES_TAC `(y:real^3 # real^3) IN ord_pairs E `;\r
2685 ASSUME_TAC (UNDISCH (SPEC_ALL (\r
2686 ISPECL [`V: real^3 -> bool `;` y:real^3 # real^3 `;` (choose_nd_point: real^3 -> \r
2687 ((real^3 -> bool) -> bool) ->(real^3 -> bool) -> real^3) fy E V`;`\r
2688 E:(real^3 -> bool) -> bool `]\r
2689  (GEN_ALL IN_ORD_PAIRS_IMP_IMP_IN_TOO))));\r
2690 DOWN;\r
2691 ASM_REWRITE_TAC[];\r
2692 DOWN THEN NHANH IN_ORD_PAIRS_IMP_SND_IN_EE_FST;\r
2693 ASM_REWRITE_TAC[];\r
2694 REPEAT STRIP_TAC;\r
2695 \r
2696 \r
2697 \r
2698 (*\r
2699 e (DOWN_TAC THEN NHANH CYCLIC_SET_IMP_STABLE_SET);;\r
2700 \r
2701 *)\r
2702 \r
2703 \r
2704 \r
2705 SUBGOAL_THEN ` {fy:real^3, sy} IN E ` MP_TAC;\r
2706 UNDISCH_TAC ` (sy:real^3) IN EE fy E `;\r
2707 REWRITE_TAC[EE; IN_ELIM_THM];\r
2708 SUBGOAL_THEN ` FAN (x:real^3,V,E) ` MP_TAC;\r
2709 ASM_REWRITE_TAC[FAN];\r
2710 PHA;\r
2711 NHANH CYCLIC_SET_IMP_STABLE_SET2;\r
2712 STRIP_TAC;\r
2713 FIRST_ASSUM (ASSUME_TAC o (SPEC `sy:real^3 `));\r
2714 \r
2715 FIRST_ASSUM (ASSUME_TAC o (SPEC `(choose_nd_poind: real^3 -> \r
2716 ((real^3 -> bool) -> bool) ->(real^3 -> bool) -> real^3) fy E V`));\r
2717 \r
2718 \r
2719 DOWN THEN DOWN THEN DISCH_THEN ASSUME_TAC2;\r
2720 FIRST_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC `\x. x = a ==> b ` [x]);\r
2721 STRIP_TAC;\r
2722 \r
2723 REWRITE_TAC[EXTENSION];\r
2724 GEN_TAC THEN EQ_TAC;\r
2725 (* sub 2.1 *)\r
2726 REWRITE_TAC[IN_ELIM_THM; ARITH_RULE` n >= 0 `];\r
2727 DISCH_THEN CHOOSE_TAC;\r
2728 ASM_SIMP_TAC[PAIR_EQ; POWER_TO_ITER];\r
2729 DOWN THEN DOWN;\r
2730 SET_TAC[];\r
2731 (* sub 2.2 *)\r
2732 REWRITE_TAC[IN_ELIM_THM; ARITH_RULE` n >= 0 `];\r
2733 DISCH_THEN CHOOSE_TAC;\r
2734 ASM_SIMP_TAC[PAIR_EQ; POWER_TO_ITER];\r
2735 DOWN THEN DOWN;\r
2736 SET_TAC[];\r
2737 (* sub IIIIII *)\r
2738 \r
2739 ASSUME_TAC2 (prove(`y IN darts_of_hyp E (V:real^3 -> bool)\r
2740  /\ ~(y IN ord_pairs E)\r
2741 ==> y IN self_pairs E V `,\r
2742 REWRITE_TAC[darts_of_hyp; IN_UNION]\r
2743 THEN CONV_TAC TAUT));\r
2744 UNDISCH_TAC `fy,choose_nd_point fy E V IN darts_of_hyp E (V:real^3 -> bool) `;\r
2745 DOWN;\r
2746 EXPAND_TAC "fy";\r
2747 PHA;\r
2748 NHANH IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL;\r
2749 STRIP_TAC;\r
2750 UNDISCH_TAC `y IN darts_of_hyp E (V:real^3 -> bool) `;\r
2751 UNDISCH_TAC `y IN self_pairs E (V:real^3 -> bool) `;\r
2752 PHA;\r
2753 UNDISCH_TAC `y = (fy:real^3), (sy: real^3 ) `;\r
2754 ASM_REWRITE_TAC[];\r
2755 SIMP_TAC[];\r
2756 EXPAND_TAC "fy";\r
2757 DISCH_THEN (fun x -> PAT_REWRITE_TAC`\x. x /\ y ==> z ` [GSYM x]);\r
2758 NHANH IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL;\r
2759 DOWN;\r
2760 ASM_REWRITE_TAC[];\r
2761 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2762 SIMP_TAC[]]);;\r
2763 \r
2764 \r
2765 \r
2766 let LOCAL_FAN_IMP_FF_SUBSET_DARTS = prove_by_refinement(\r
2767 ` local_fan ((V:real^3 -> bool),E,FF) ==> FF SUBSET darts_of_hyp E V`,\r
2768 [REWRITE_TAC[local_fan];\r
2769 LET_TAC;\r
2770 STRIP_TAC;\r
2771 DOWN_TAC;\r
2772 NHANH lemma_face_subset;\r
2773 STRIP_TAC;\r
2774 UNDISCH_TAC ` face H (x:real^3#real^3) SUBSET dart H`;\r
2775 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` HYP_LEMMA);\r
2776 REWRITE_TAC[dart];\r
2777 EXPAND_TAC "H";\r
2778 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);\r
2779 ASM_REWRITE_TAC[HYP]]);;\r
2780 \r
2781 \r
2782 \r
2783 \r
2784 \r
2785 \r
2786 \r
2787 \r
2788 let LOCAL_IMP_FINITE_DARTS = prove_by_refinement(\r
2789 ` local_fan ((V:real^3 -> bool),E,FF) ==> FINITE (darts_of_hyp E V) `,\r
2790 [REWRITE_TAC[local_fan] THEN LET_TAC;\r
2791 EXPAND_TAC "H";\r
2792 NHANH HYP_LEMMA;\r
2793 REWRITE_TAC[dart];\r
2794 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
2795 SIMP_TAC[]]);;\r
2796 \r
2797 \r
2798 \r
2799 \r
2800 let LOCAL_FAN_FINITE_FF = prove_by_refinement(\r
2801 ` local_fan ((V:real^3 -> bool),E,FF) ==> FINITE FF `,\r
2802 [NHANH LOCAL_FAN_IMP_FF_SUBSET_DARTS;\r
2803 NHANH LOCAL_IMP_FINITE_DARTS;\r
2804 PHA THEN IMP_TAC THEN REMOVE_TAC;\r
2805 REWRITE_TAC[FINITE_SUBSET]]);;\r
2806 \r
2807 \r
2808 \r
2809 \r
2810 \r
2811 \r
2812 \r
2813 \r
2814 \r
2815 \r
2816 \r
2817 let LOCAL_FAN_IMP_BIJ_FF_NODES = prove_by_refinement(\r
2818 `local_fan ((V:real^3 -> bool),E,FF) /\\r
2819    f = (\y. node (hypermap (HYP (vec 0,V,E))) y ) ==> \r
2820 BIJ f FF {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V} `,\r
2821 [REWRITE_TAC[local_fan];\r
2822 LET_TAC;\r
2823 REWRITE_TAC[dih2k];\r
2824 STRIP_TAC;\r
2825 ASM_REWRITE_TAC[BIJ; INJ; SURJ];\r
2826 PHA;\r
2827 CONJ_TAC;\r
2828 (* SUB 1 *)\r
2829 GEN_TAC;\r
2830 ASSUME_TAC2 (ISPEC `(vec 0): real^3 ` HYP_LEMMA);\r
2831 DOWN;\r
2832 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
2833 ASSUME_TAC2 (ISPECL [`H: (real^3 # real^3)hypermap `;\r
2834 `x:real^3 # real^3 `] lemma_face_subset);\r
2835 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
2836 PHA THEN STRIP_TAC;\r
2837 UNDISCH_TAC `face H (x:real^3 # real^3) SUBSET dart H`;\r
2838 DOWN;\r
2839 DOWN_TAC THEN STRIP_TAC;\r
2840 EXPAND_TAC "H";\r
2841 USE_FIRST `dart (hypermap (HYP (vec 0,V,E))) = darts_of_hyp E (V:real^3 -> bool) `\r
2842   ( fun x -> REWRITE_TAC[GSYM x]);\r
2843 REPLICATE_TAC 3 DOWN;\r
2844 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2845 ASM_REWRITE_TAC[IN_ELIM_THM; SUBSET];\r
2846 MESON_TAC[];\r
2847 (* SUB 2.1 *)\r
2848 CONJ_TAC;\r
2849 (* sub 2.1.1 *)\r
2850 REPEAT STRIP_TAC;\r
2851 MP_TAC LOCAL_FAN_FINITE_FF;\r
2852 ANTS_TAC THENL [\r
2853 REWRITE_TAC[local_fan; dih2k] THEN \r
2854 LET_TAC THEN ASM_SIMP_TAC[] THEN \r
2855 ASM_MESON_TAC[];\r
2856 ASM_CASES_TAC ` CARD (FF:real^3 # real^3 -> bool) = 0`];\r
2857 (* sub I *)\r
2858 DOWN THEN PHA;\r
2859 NHANH (MESON[CARD_EQ_0]` CARD FF = 0 /\ FINITE FF ==> FF = {} `);\r
2860 STRIP_TAC;\r
2861 MP_TAC (ISPECL [`H: (real^3#real^3) hypermap `;` x: real^3 # real^3 `] face_refl);\r
2862 DOWN;\r
2863 ASM_SIMP_TAC[NOT_IN_EMPTY];\r
2864 (* SUB II *)\r
2865 MP_TAC (ISPECL [` CARD (FF: (real^3 # real^3 ) -> bool) `;` y: real^3 # real^3 `;\r
2866   `face_map (H:(real^3 # real^3) hypermap) `;` x: real^3 # real^3 `] \r
2867 (GEN_ALL HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT));\r
2868 ANTS_TAC THENL [\r
2869 ASM_REWRITE_TAC[GSYM face];\r
2870 REWRITE_TAC[GSYM face]];\r
2871 DISCH_TAC;\r
2872 MP_TAC (ISPECL [` CARD (FF: (real^3 # real^3 ) -> bool) `;` x': real^3 # real^3 `;\r
2873   `face_map (H:(real^3 # real^3) hypermap) `;` x: real^3 # real^3 `] \r
2874 (GEN_ALL HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT));\r
2875 ANTS_TAC THENL [\r
2876 ASM_REWRITE_TAC[GSYM face];\r
2877 ASM_REWRITE_TAC[GSYM face]];\r
2878 REPEAT STRIP_TAC;\r
2879 MP_TAC (ISPECL [`CARD (FF: real^3 # real^3 -> bool) `;\r
2880 ` H: (real^3 # real^3) hypermap `] (GEN_ALL DIH2K_IMP_SIMPLE_HYPERMAP));\r
2881 ANTS_TAC;\r
2882 (* SUB GOAL *)\r
2883 \r
2884 \r
2885 ASM_SIMP_TAC[dih2k];\r
2886 EXPAND_TAC "H";\r
2887 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^ 3 ` ELMS_OF_HYPERMAP_HYP));\r
2888 MP_TAC (REWRITE_RULE[local_fan] LOCAL_IMP_FINITE_DARTS);\r
2889 ANTS_TAC THENL [\r
2890 LET_TAC THEN \r
2891 REWRITE_TAC[dih2k] THEN \r
2892 ASM_MESON_TAC[];\r
2893 ASM_REWRITE_TAC[]];\r
2894 \r
2895 (* =============== *)\r
2896 (* SUB             *)\r
2897 NHANH lemma_simple_hypermap;\r
2898 STRIP_TAC;\r
2899 FIRST_ASSUM (MP_TAC o (SPEC `y: real^3 # real^3 `));\r
2900 UNDISCH_TAC `node H x' = node H (y: real^3 # real^3 ) `;\r
2901 DISCH_THEN (fun x -> REWRITE_TAC[SYM x]);\r
2902 ASM_REWRITE_TAC[];\r
2903 UNDISCH_TAC `face H x' = face H (x: real^3 # real^3 ) `;\r
2904 DISCH_THEN (fun x -> REWRITE_TAC[SYM x]);\r
2905 ASM_REWRITE_TAC[];\r
2906 SET_TAC[];\r
2907 \r
2908 \r
2909 (* ---------------------------------- *)\r
2910 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
2911 DOWN;\r
2912 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2913 ASM_SIMP_TAC[];\r
2914 STRIP_TAC;\r
2915 ASSUME_TAC2 (ISPEC `H:(real^3 # real^3 ) hypermap ` lemma_face_subset);\r
2916 CONJ_TAC;\r
2917 STRIP_TAC THEN DOWN THEN PHA;\r
2918 SET_TAC[];\r
2919 REWRITE_TAC[IN_ELIM_THM];\r
2920 REPEAT STRIP_TAC;\r
2921 MP_TAC (ISPECL [`CARD (FF: real^3#real^3->bool) `;` H : (real^3#real^3)hypermap`]\r
2922   ( GEN_ALL DIH_IMP_EVERY_NODE_INTER_FACE));\r
2923 ANTS_TAC THENL [\r
2924 REWRITE_TAC[dih2k] THEN \r
2925 ASM_SIMP_TAC[];\r
2926 DISCH_THEN (MP_TAC o (SPECL [`y:real^3 # real^3 `;`x:real^3# real^3`]))];\r
2927 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];\r
2928 DISCH_THEN ASSUME_TAC2;\r
2929 FIRST_X_ASSUM CHOOSE_TAC;\r
2930 EXISTS_TAC `d: real^3 # real^3 `;\r
2931 FIRST_X_ASSUM MP_TAC THEN NHANH lemma_node_identity;\r
2932 ASM_SIMP_TAC[]]);;\r
2933 \r
2934 \r
2935 \r
2936 \r
2937 (* ++++++++++++++ *)\r
2938 \r
2939 \r
2940 \r
2941 \r
2942 \r
2943 \r
2944 \r
2945 \r
2946 \r
2947 \r
2948 \r
2949 (* +++++++++++++ *)\r
2950 \r
2951 \r
2952 \r
2953 \r
2954 \r
2955 (*  local_fan (V,E,FF) /\ f = (\y. node (hypermap (HYP (vec 0,V,E))) y)\r
2956      ==> BIJ f FF\r
2957          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}\r
2958 *)\r
2959 \r
2960 REWRITE_RULE[MESON[]` (! h. a /\ h = f ==> BIJ h S C ) <=> ( a ==> BIJ f S C ) `]\r
2961   (GEN `f: real^3#real^3->real^3#real^3->bool ` LOCAL_FAN_IMP_BIJ_FF_NODES);;\r
2962 \r
2963 \r
2964 (*\r
2965 val it : thm =\r
2966   |- local_fan (V,E,FF)\r
2967      ==> BIJ (\y. node (hypermap (HYP (vec 0,V,E))) y) FF\r
2968          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}\r
2969 \r
2970 *)\r
2971 \r
2972 REWRITE_RULE[MESON[]` (! h. a /\ h = f ==> BIJ h S C ) <=> ( a ==> BIJ f S C ) `]\r
2973   (GEN `f: real^3->real^3#real^3->bool` FAN_IMP_BIJ_V_NODE_OF_HYP);;\r
2974 \r
2975 FAN_IMP_BIJ_V_NODE_OF_HYP ;;\r
2976 (*   val it : thm =\r
2977   |- FAN (x,V,E) /\\r
2978      f =\r
2979      (\u. if u IN V\r
2980           then node (hypermap (HYP (x,V,E))) (u,choose_nd_point u E V)\r
2981           else {})\r
2982      ==> BIJ f V\r
2983          {node (hypermap (HYP (x,V,E))) y | y | y IN darts_of_hyp E V}\r
2984 \r
2985 *)\r
2986 \r
2987 \r
2988 let NOT_IN_DARTS_NN_IDE = prove(\r
2989 ` ~( y IN darts_of_hyp E V) \r
2990 ==> nn_of_hyp (x,V,E) y = y `,\r
2991 REWRITE_TAC[nn_of_hyp2] THEN SIMP_TAC[]);;\r
2992 \r
2993 let ITER_FIXPOINT2 = \r
2994 MESON[ITER_FIXPOINT]`! f x. f x = x ==> ! n . ITER n f x = x `;;\r
2995 \r
2996 \r
2997 \r
2998 let NOT_IN_DARTS_NN_OF_HYP_POWER_IDE = prove(\r
2999 ` ~( y IN darts_of_hyp E V) \r
3000 ==> ! n. (nn_of_hyp (x,V,E) POWER n ) y = y `,\r
3001 STRIP_TAC THEN INDUCT_TAC THENL [\r
3002 REWRITE_TAC[POWER; I_THM];\r
3003 ASM_REWRITE_TAC[COM_POWER; o_THM; nn_of_hyp2]]);;\r
3004 \r
3005 \r
3006 \r
3007 \r
3008 \r
3009 let IN_NODE_IMP_FIRST_EQ = prove_by_refinement(\r
3010 ` FAN (x,V,E) /\ a IN ( node (hypermap (HYP (x,V,E))) b )\r
3011   ==> FST a = FST b `,\r
3012 [REWRITE_TAC[node];\r
3013 NHANH ELMS_OF_HYPERMAP_HYP;\r
3014 IMP_TAC;\r
3015 SIMP_TAC[];\r
3016 STRIP_TAC;\r
3017 REWRITE_TAC[IN_ELIM_THM; orbit_map];\r
3018 STRIP_TAC;\r
3019 DOWN;\r
3020 PAT_ONCE_REWRITE_TAC `\x. a = P x ==> y ` [GSYM PAIR];\r
3021 ASM_CASES_TAC ` (b:real^3# real^3 ) IN darts_of_hyp E V `;\r
3022 ABBREV_TAC ` u = FST (b:real^3# real^3) `;\r
3023 ABBREV_TAC ` v = SND (b:real^3# real^3) `;\r
3024 MP_TAC N_HYP_TO_AZIM_CYCLE_LEM;\r
3025 ANTS_TAC;\r
3026 ASM_REWRITE_TAC[];\r
3027 ASM_MESON_TAC[PAIR_EQ2; PAIR];\r
3028 SIMP_TAC[];\r
3029 DOWN;\r
3030 NHANH NOT_IN_DARTS_NN_OF_HYP_POWER_IDE;\r
3031 SIMP_TAC[]]);;\r
3032 \r
3033 \r
3034 \r
3035 \r
3036 \r
3037 \r
3038 let BIJ_BETWEEN_FF_AND_V = prove_by_refinement(\r
3039 `local_fan (V,E,FF) /\ k = (\x. FST x )\r
3040 ==> BIJ k FF V `,\r
3041 [ABBREV_TAC ` f =\r
3042      (\u. if (u:real^3) IN V\r
3043           then node (hypermap (HYP (vec 0,V,E))) (u,choose_nd_point u E V)\r
3044           else {}) `;\r
3045 ABBREV_TAC `h = (\y. node (hypermap (HYP (vec 0,V,E))) y) ` ;\r
3046 DOWN_TAC;\r
3047 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3048 STRIP_TAC;\r
3049 ASSUME_TAC2 (\r
3050 prove(` local_fan (V,E,FF) /\\r
3051      f =\r
3052      (\u. if (u:real^3) IN V\r
3053           then node (hypermap (HYP (vec 0,V,E))) (u,choose_nd_point u E V)\r
3054           else {}) /\\r
3055  h = (\y. node (hypermap (HYP (vec 0,V,E))) y)\r
3056      ==> BIJ h FF\r
3057          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V} /\\r
3058    BIJ f V\r
3059          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}`,\r
3060 SIMP_TAC[FAN_IMP_BIJ_V_NODE_OF_HYP ; LOCAL_FAN_IMP_BIJ_FF_NODES] THEN \r
3061 REWRITE_TAC[local_fan] THEN LET_TAC THEN \r
3062 EXPAND_TAC "H" THEN \r
3063 SIMP_TAC[FAN_IMP_BIJ_V_NODE_OF_HYP]));\r
3064 DOWN;\r
3065 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]\r
3066   (GEN `ff: B -> C ` (REWRITE_RULE[TAUT` a/\b/\c ==> d <=>\r
3067  a /\ b ==> c ==> d `] TOW_BIJS_IMP_BIJ_BETWEEN_FIRST)));\r
3068 REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `];\r
3069 ABBREV_TAC ` ff = (\x. if x IN FF then @a. a IN V /\ \r
3070 (h:real^3#real^3->real^3#real^3->bool) x = f (a:real^3) else aa) `;\r
3071 STRIP_TAC;\r
3072 SUBGOAL_THEN `(!x. x IN FF ==> (ff: real^3#real^3->real^3)\r
3073  x = k x ) ` ASSUME_TAC;\r
3074 SUBGOAL_THEN ` (! x. (x:real^3 # real^3) IN FF ==> ff x IN (V:real^3 -> bool) /\\r
3075   (h:real^3#real^3->real^3#real^3->bool) x = f ( ff x )) ` ASSUME_TAC;\r
3076 \r
3077 (* SUBGOAL 1 *)\r
3078 EXPAND_TAC "ff";\r
3079 SIMP_TAC[];\r
3080 STRIP_TAC THEN STRIP_TAC;\r
3081 CONV_TAC SELECT_CONV;\r
3082 DOWN_TAC;\r
3083 REWRITE_TAC[BIJ; INJ; SURJ];\r
3084 MESON_TAC[];\r
3085 (* end 1 *)\r
3086 \r
3087 (* sub 2 *)\r
3088 FIRST_X_ASSUM NHANH;\r
3089 STRIP_TAC;\r
3090 STRIP_TAC;\r
3091 DOWN;\r
3092 ASM_REWRITE_TAC[];\r
3093 STRIP_TAC;\r
3094 MP_TAC (ISPECL [` hypermap (HYP (vec 0,V,E)) `;` x: real^3 # real^3 `] node_refl);\r
3095 ASM_REWRITE_TAC[];\r
3096 ASSUME_TAC2 LOCAL_FAN_IMP_FAN;\r
3097 DOWN THEN PHA;\r
3098 NHANH IN_NODE_IMP_FIRST_EQ;\r
3099 EXPAND_TAC "k";\r
3100 SIMP_TAC[EQ_SYM_EQ];\r
3101 (* subgoal -------------------------- *)\r
3102 (* oooooooooooooooooooooooooooooooooo *)\r
3103 \r
3104 DOWN THEN DOWN;\r
3105 PHA;\r
3106 REWRITE_TAC[INDENT_IN_S1_IMP_BIJ ]]);;\r
3107 \r
3108 \r
3109 \r
3110 \r
3111 \r
3112 let WRGCVDR = prove_by_refinement(\r
3113 `local_fan (V,E,FF) /\ k = (\x. FST x)\r
3114  ==> BIJ k FF V /\\r
3115      ((!x. x IN V ==> x,hro x IN FF) /\\r
3116       (!x. x IN FF ==> x = FST x,hro (FST x))\r
3117       ==> (!x. x IN V ==> V = orbit_map hro x))`,\r
3118 [STRIP_TAC;\r
3119 ASSUME_TAC2 BIJ_BETWEEN_FF_AND_V;\r
3120 ASM_REWRITE_TAC[];\r
3121 REPEAT STRIP_TAC;\r
3122 DOWN_TAC;\r
3123 REWRITE_TAC[local_fan; dih2k];\r
3124 LET_TAC;\r
3125 STRIP_TAC;\r
3126 SUBGOAL_THEN ` (x:real^3), (hro:real^3 -> real^3) x IN FF ` ASSUME_TAC;\r
3127 FIRST_X_ASSUM MATCH_MP_TAC;\r
3128 ASM_SIMP_TAC[];\r
3129 DOWN;\r
3130 UNDISCH_TAC ` FF = face H (x':real^3 # real^3 ) `;\r
3131 SIMP_TAC[] THEN STRIP_TAC;\r
3132 NHANH lemma_face_identity;\r
3133 DOWN_TAC THEN REWRITE_TAC[BIJ];\r
3134 NHANH (prove(` SURJ (f:A ->B) S1 S2 ==> IMAGE f S1 = S2 `,\r
3135 REWRITE_TAC[IMAGE; SURJ] THEN SET_TAC[]));\r
3136 STRIP_TAC;\r
3137 EXPAND_TAC "V";\r
3138 REPLICATE_TAC 3 DOWN THEN PHA;\r
3139 SIMP_TAC[];\r
3140 STRIP_TAC;\r
3141 REWRITE_TAC[face; IMAGE; orbit_map; IN_ELIM_THM];\r
3142 SUBGOAL_THEN ` (! n. (face_map H POWER n) (x,(hro:real^3 -> real^3 ) x) = \r
3143 ((hro POWER n) x, (hro POWER ( n + 1 )) x )) `  ASSUME_TAC;\r
3144 INDUCT_TAC;\r
3145 REWRITE_TAC[POWER; I_THM; ARITH_RULE` 0 + 1 = 1`; POWER_1];\r
3146 ASM_REWRITE_TAC[COM_POWER; o_THM];\r
3147 DOWN THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3148 NHANH in_orbit_lemma;\r
3149 ASSUME_TAC2 (SPEC `(vec 0):real^3 ` (GEN `x:real^3 ` ELMS_OF_HYPERMAP_HYP));\r
3150 DOWN;\r
3151 ASM_SIMP_TAC[FUN_EQ_THM];\r
3152 STRIP_TAC;\r
3153 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3154 STRIP_TAC;\r
3155 SUBGOAL_THEN `ff_of_hyp (vec 0,(V:real^3 -> bool),E) ((face_map H POWER n) (x,hro x)) IN (FF: real^3 # real^3 -> bool) `\r
3156   ASSUME_TAC;\r
3157 ASM_SIMP_TAC[];\r
3158 DOWN;\r
3159 NHANH IN_ORBIT_MAP_IMP_F_Y;\r
3160 REWRITE_TAC[GSYM face];\r
3161 ASM_SIMP_TAC[];\r
3162 (* gggggggggggggggggggg *)\r
3163 DOWN;\r
3164 \r
3165 ASM_REWRITE_TAC[];\r
3166 SUBGOAL_THEN` (hro POWER n) (x:real^3),(hro POWER (n + 1)) x IN \r
3167 darts_of_hyp E V ` MP_TAC;\r
3168 DOWN;\r
3169 REWRITE_TAC[GSYM face];\r
3170 DOWN_TAC THEN NHANH lemma_face_subset;\r
3171 STRIP_TAC;\r
3172 SUBGOAL_THEN` (x:real^3), (hro: real^3 -> real^3) x IN dart H ` MP_TAC;\r
3173 MATCH_MP_TAC (SET_RULE` face H (x':real^3 # real^3) SUBSET S/\\r
3174 y IN face H (x':real^3 # real^3) ==> y IN S `);\r
3175 ASM_REWRITE_TAC[];\r
3176 NHANH lemma_face_subset;\r
3177 STRIP_TAC;\r
3178 DOWN;\r
3179 DOWN_TAC THEN REWRITE_TAC[GSYM FUN_EQ_THM; ETA_AX];\r
3180 STRIP_TAC;\r
3181 DOWN;\r
3182 ASM_REWRITE_TAC[];\r
3183 MATCH_MP_TAC (SET_RULE` x IN a ==> a SUBSET b ==> x IN b `);\r
3184 FIRST_X_ASSUM ACCEPT_TAC;\r
3185 ASM_SIMP_TAC[ff_of_hyp];\r
3186 REMOVE_TAC;\r
3187 DOWN_TAC;\r
3188 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3189 STRIP_TAC;\r
3190 DOWN;\r
3191 UNDISCH_TAC `face H (x,(hro: real^3 -> real^3) x) = face H x' `;\r
3192 SIMP_TAC[];\r
3193 DISCH_TAC;\r
3194 UNDISCH_TAC `face H (x':real^3 # real^3 ) = FF`;\r
3195 SIMP_TAC[];\r
3196 FIRST_ASSUM NHANH;\r
3197 REWRITE_TAC[PAIR_EQ];\r
3198 SIMP_TAC[GSYM ADD1; COM_POWER; o_THM];\r
3199 (* iiiiiiiiiiiiiiiiiiiiiiii *)\r
3200 REWRITE_TAC[FUN_EQ_THM];\r
3201 GEN_TAC THEN EQ_TAC;\r
3202 REWRITE_TAC[IN_ELIM_THM];\r
3203 STRIP_TAC;\r
3204 DOWN;\r
3205 ASM_SIMP_TAC[];\r
3206 STRIP_TAC;\r
3207 EXISTS_TAC `n: num `;\r
3208 ASM_SIMP_TAC[];\r
3209 (* ::::::::::::::::::: *)\r
3210 REWRITE_TAC[IN_ELIM_THM];\r
3211 STRIP_TAC;\r
3212 EXISTS_TAC `(hro POWER n) (x: real^3 ), (hro POWER (n + 1)) x `;\r
3213 ASM_REWRITE_TAC[];\r
3214 EXISTS_TAC `n:num `;\r
3215 ASM_REWRITE_TAC[]]);;\r
3216 \r
3217 \r
3218 \r
3219 \r
3220 \r
3221 \r
3222 \r
3223 \r
3224 let SET_TAC =\r
3225 let basicthms =\r
3226 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
3227 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
3228 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
3229 [IN_ELIM_THM; IN] in\r
3230 let PRESET_TAC =\r
3231 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
3232 REPEAT COND_CASES_TAC THEN\r
3233 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
3234 REWRITE_TAC allthms in\r
3235 fun ths ->\r
3236 PRESET_TAC THEN\r
3237 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
3238 MESON_TAC[];;\r
3239 \r
3240 let SET_RULE tm = prove(tm,SET_TAC[]);; \r
3241 \r
3242 \r
3243 (* ====================================== *)\r
3244 \r
3245 (* ============ MFMPCVM ================  *)\r
3246 \r
3247 (* =====================================  *)\r
3248 \r
3249 \r
3250 \r
3251 (* ================================= *)\r
3252 (*              PJRIMCV              *)\r
3253 (* ================================= *)\r
3254 \r
3255 \r
3256 (* \r
3257 let wedge_fan_gt = new_definition\r
3258 ` wedge_fan_gt v E = wedge_in_fan_gt (v, rho_fan v) E `;;\r
3259 \r
3260 \r
3261 let wedge_fan_ge = new_definition\r
3262 `wedge_fan_ge v E = wedge_in_fan_ge (v, rho_fan v) E`;;\r
3263 \r
3264 *)\r
3265 \r
3266 (* ============================= *)\r
3267 (*          localization         *)\r
3268 (*            BIFQATK            *)\r
3269 (* ============================= *)\r
3270 \r
3271 \r
3272 let v_prime = new_definition `v_prime V FF = {v| v IN V /\\r
3273  (?w. (v,w) IN FF )} `;;\r
3274 \r
3275 let e_prime = new_definition ` e_prime E FF = {{v,w} | {v,w} IN E /\ \r
3276 (v,w) IN FF } `;;\r
3277 \r
3278 \r
3279 let IMP_FAN_V_PRIME_E_PRIME = prove_by_refinement\r
3280 (`FAN (v, V, E) /\ (?x. x IN dart (hypermap (HYP (v,V,E))) /\\r
3281 FF = face ( hypermap (HYP (v, V, E))) x)\r
3282 ==> FAN (v, v_prime V FF , e_prime E FF ) `,\r
3283 [REWRITE_TAC[FAN; v_prime; e_prime];\r
3284 STRIP_TAC;\r
3285 CONJ_TAC;\r
3286 REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM];\r
3287 REPEAT STRIP_TAC;\r
3288 DOWN THEN SIMP_TAC[];\r
3289 DOWN;\r
3290 MP_TAC (SPEC `v: real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
3291 ANTS_TAC THENL [\r
3292 ASM_REWRITE_TAC[FAN];\r
3293 DOWN THEN DOWN];\r
3294 REWRITE_TAC[face];\r
3295 SIMP_TAC[];\r
3296 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC;\r
3297 NHANH_PAT `\x. x ==> y ` IN_ORBIT_MAP_IMP_F_Y;\r
3298 REWRITE_TAC[ff_of_hyp];\r
3299 FIRST_ASSUM (fun x -> REWRITE_TAC[GSYM x; GSYM face]);\r
3300 SUBGOAL_THEN ` x IN dart (hypermap (HYP ((v:real^3),V,E))) ` MP_TAC;\r
3301 ASM_REWRITE_TAC[];\r
3302 IMP_TAC;\r
3303 NHANH lemma_face_subset;\r
3304 IMP_TAC THEN REMOVE_TAC;\r
3305 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];\r
3306 ONCE_REWRITE_TAC[SET_RULE` a SUBSET b /\ x IN a <=> x IN b /\ a SUBSET b /\ x IN a `];\r
3307 ASM_SIMP_TAC[];\r
3308 IMP_TAC THEN REMOVE_TAC;\r
3309 UNDISCH_TAC ` {v', (w:real^3) } IN E `;\r
3310 UNDISCH_TAC ` UNIONS E SUBSET (V: real^3 -> bool) `;\r
3311 REWRITE_TAC[UNIONS_SUBSET];\r
3312 DISCH_THEN NHANH;\r
3313 SET_TAC[];\r
3314 UNDISCH_TAC ` graph (E:(real^3 -> bool) -> bool) `;\r
3315 REWRITE_TAC[graph];\r
3316 DISCH_TAC;\r
3317 CONJ_TAC;\r
3318 DOWN THEN SET_TAC[];\r
3319 REWRITE_TAC[fan1; fan2; fan6; fan7];\r
3320 CONJ_TAC;\r
3321 DOWN_TAC;\r
3322 REWRITE_TAC[fan1];\r
3323 STRIP_TAC;\r
3324 CONJ_TAC;\r
3325 UNDISCH_TAC `FINITE (V:real^3 -> bool) `;\r
3326 MATCH_MP_TAC (REWRITE_RULE[TAUT` a /\ b ==> c <=> \r
3327 b ==> a ==> c `] FINITE_SUBSET);\r
3328 SET_TAC[];\r
3329 DOWN THEN DOWN;\r
3330 NHANH (MESON[face_refl]` FF = face H x ==> x IN FF `);\r
3331 REPEAT STRIP_TAC;\r
3332 MP_TAC (SPEC `v:real^3 ` (GEN `x:real^3 ` ELMS_OF_HYPERMAP_HYP));\r
3333 ANTS_TAC THENL [\r
3334 ASM_REWRITE_TAC[FAN; graph; fan1];\r
3335 STRIP_TAC];\r
3336 UNDISCH_TAC `x IN dart (hypermap (HYP (v,V,E)))`;\r
3337 ASM_REWRITE_TAC[];\r
3338 STRIP_TAC;\r
3339 ASSUME_TAC2 (\r
3340 ISPEC `x:real^3#real^3 ` (GEN `y:A#A ` IN_DARTS_HYP_IMP_FST_SND_IN_V));\r
3341 UNDISCH_TAC `(x:real^3 # real^3 ) IN FF `;\r
3342 REWRITE_TAC[];\r
3343 ONCE_REWRITE_TAC[GSYM PAIR];\r
3344 ABBREV_TAC ` fx = FST (x:real^3 # real^3) `;\r
3345 ASM SET_TAC[];\r
3346 DOWN_TAC THEN REWRITE_TAC[fan1; fan2];\r
3347 STRIP_TAC;\r
3348 CONJ_TAC;\r
3349 ASM SET_TAC[];\r
3350 DOWN_TAC THEN REWRITE_TAC[fan6; fan7];\r
3351 SET_TAC[]]);;\r
3352 \r
3353 \r
3354 \r
3355 \r
3356 let E_PRIME_SUBSET_E = prove(` e_prime E FF SUBSET E `,\r
3357 REWRITE_TAC[e_prime; SUBSET; IN_ELIM_THM] THEN \r
3358 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;\r
3359 \r
3360 let SUBSET_IMP_SO_DO_EE =\r
3361 prove(` W1 SUBSET W2 ==> EE v W1 SUBSET EE v W2 `,\r
3362 REWRITE_TAC[EE] THEN SET_TAC[]);;\r
3363 \r
3364 \r
3365 \r
3366 \r
3367 let FST_SND_X_IN_EE_E_PRIME =prove(` \r
3368 (x:A #A) IN FF /\ {FST x, SND x} IN E \r
3369 ==> FST x IN EE (SND x) (e_prime E FF ) /\\r
3370 SND x IN EE (FST x) (e_prime E FF) `,\r
3371 PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [GSYM PAIR] THEN \r
3372 ABBREV_TAC ` ax = FST (x:A#A) ` THEN \r
3373 REWRITE_TAC[EE; IN_ELIM_THM; e_prime] THEN \r
3374 STRIP_TAC THEN \r
3375 CONJ_TAC THENL [\r
3376 EXISTS_TAC `ax: A ` THEN \r
3377 EXISTS_TAC `SND (x:A#A) ` THEN \r
3378 ASM_SIMP_TAC[INSERT_COMM] ;\r
3379 EXISTS_TAC `ax:A` THEN \r
3380 EXISTS_TAC `SND (x:A#A) ` THEN \r
3381 ASM_REWRITE_TAC[]]);;\r
3382 \r
3383 \r
3384 \r
3385 \r
3386 \r
3387 let CYCLIC_MAP_IMP_CIRCLE_ITSELF =\r
3388 prove_by_refinement(`\r
3389 (!(x:A). x IN W ==> W = orbit_map f x ) /\ y IN W\r
3390 ==> (?x. x IN W /\ y = f x )`, [\r
3391 IMP_TAC THEN DISCH_TAC;\r
3392 FIRST_ASSUM (NHANH_PAT `\x. x ==> l`);\r
3393 STRIP_TAC;\r
3394 UNDISCH_TAC `y:A IN W `;\r
3395 FIRST_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [x]);\r
3396 NHANH IN_ORBIT_MAP_IMP_F_Y;\r
3397 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
3398 FIRST_ASSUM (NHANH_PAT `\x. x ==> y `);\r
3399 STRIP_TAC;\r
3400 UNDISCH_TAC `y:A IN W `;\r
3401 FIRST_ASSUM (fun x -> PAT_REWRITE_TAC`\x. x ==> y `[x]);\r
3402 REWRITE_TAC[orbit_map; IN_ELIM_THM; POWER_FUNCTION; GSYM COM_POWER_FUNCTION];\r
3403 STRIP_TAC;\r
3404 EXISTS_TAC `(f POWER n) (y:A) `;\r
3405 CONJ_TAC;\r
3406 ASM_REWRITE_TAC[lemma_in_orbit];\r
3407 FIRST_X_ASSUM ACCEPT_TAC]);;\r
3408 \r
3409 \r
3410 \r
3411 \r
3412 \r
3413 \r
3414 \r
3415 (* ================================= *)\r
3416 (*   definition 7.8   RTPRRJS        *)\r
3417 (*   chapter: Local Fan              *)\r
3418 (* ================================= *)\r
3419 \r
3420 \r
3421 let generic = new_definition` generic V E <=>\r
3422 (! v w u. {v,w} IN E /\ u IN V ==> aff_ge { vec 0 } {v,w} INTER \r
3423 aff_lt {vec 0} {u} = {} )`;;\r
3424 \r
3425 \r
3426 let circular = new_definition ` circular V E <=> \r
3427 (? v w u. {v,w} IN E /\ u IN V /\ ~(aff_gt { vec 0 } {v,w} INTER \r
3428 aff_lt {vec 0} {u} = {}) )`;;\r
3429 \r
3430 \r
3431 let lunar = new_definition\r
3432 ` lunar (v,w) V E <=> ~(circular V E) /\ {v,w} SUBSET V /\\r
3433 ~( v = w ) /\ collinear {vec 0, v, w } `;;\r
3434 \r
3435 open Aff_sgn_tac;;\r
3436 let AFF_SGN_TRULE tm = prove (tm, AFF_SGN_TAC);;\r
3437 \r
3438 \r
3439 let DIH2K_IMP_NODE_MAP_X_DIFF_X =\r
3440 prove(`FINITE (dart H) /\ dih2k H k /\ ~(k = 0) ==> \r
3441 (!x. x IN dart H ==> ~((node_map H) x = x )) `,\r
3442 NHANH DIH2K_IMP_PRE_SIMPLE_HYP THEN \r
3443 STRIP_TAC THEN FIRST_ASSUM NHANH THEN \r
3444 MESON_TAC[face_refl]);;\r
3445 \r
3446 \r
3447 \r
3448 \r
3449 let FAN_IMP_FINITE_DARTS = \r
3450 prove(` FAN ((x:real^3),V,E) ==> FINITE (darts_of_hyp E V) `,\r
3451 NHANH HYP_LEMMA THEN \r
3452 SIMP_TAC[GSYM hypermap_tybij; HYP]);;\r
3453 \r
3454 \r
3455 \r
3456 let FAN_IMP_NOT_EMPTY_DARTS =\r
3457 prove(` FAN ((x:real^N),V,E) ==> ~(darts_of_hyp E V = {} ) `,\r
3458 REWRITE_TAC[darts_of_hyp; FAN; fan1; ord_pairs; self_pairs; EE]\r
3459 THEN SET_TAC[]);;\r
3460 \r
3461 \r
3462 \r
3463 \r
3464 \r
3465 \r
3466 \r
3467 let FAN7_SIMPLE =\r
3468 prove(`!x. fan7 ((x:real^N),V,E) ==> (!a b. a IN V /\ b IN V \r
3469 ==> aff_ge {x} {a} INTER aff_ge {x} {b} =\r
3470 aff_ge {x} ({a} INTER {b})) `,\r
3471 REWRITE_TAC[fan7] THEN SET_TAC[]);;\r
3472 \r
3473 \r
3474 \r
3475 \r
3476 \r
3477 let FAN_IMP_DIFF =\r
3478 prove(`FAN (x,V,E) ==> (!v. v IN V \/ v IN UNIONS E ==> ~( v = x )) `,\r
3479 REWRITE_TAC[FAN; fan2] THEN SET_TAC[]);;\r
3480 \r
3481 \r
3482 \r
3483 let AFF_GE_TO_AFF_GT2_GE1 = prove_by_refinement(\r
3484 ` ~( u = x ) /\ ~( v = x ) ==>\r
3485 aff_ge {x} {u,v} = aff_gt {x} {u,v} UNION aff_ge {x} {u} \r
3486 UNION aff_ge {x} {v} `,\r
3487 [SIMP_TAC[\r
3488 AFF_SGN_TRULE` ~( u = x ) /\ ~( v = x ) ==>\r
3489 aff_ge {x} {u,v} = {w| ? tx tu tv. &0 <= tu /\ &0 <= tv /\\r
3490 tx + tu + tv = &1 /\ w = tx % x + tu % u + tv % v } `];\r
3491 SIMP_TAC[\r
3492 AFF_SGN_TRULE` ~( u = x ) /\ ~( v = x ) ==>\r
3493 aff_gt {x} {u,v} = {w| ? tx tu tv. &0 < tu /\ &0 < tv /\\r
3494 tx + tu + tv = &1 /\ w = tx % x + tu % u + tv % v } `];\r
3495 SIMP_TAC[\r
3496 AFF_SGN_TRULE` ~( u = x ) ==>\r
3497 aff_ge {x} {u} = {w| ? tx tu . &0 <= tu /\ \r
3498 tx + tu  = &1 /\ w = tx % x + tu % u} `];\r
3499 REWRITE_TAC[SET_RULE` a = b <=> (!x. x IN a <=> x IN b) `; IN_ELIM_THM; IN_UNION];\r
3500 REPEAT STRIP_TAC;\r
3501 EQ_TAC;\r
3502 STRIP_TAC;\r
3503 ASM_CASES_TAC ` tu = &0 `;\r
3504 DISJ2_TAC THEN DISJ2_TAC;\r
3505 EXISTS_TAC ` tx: real `;\r
3506 EXISTS_TAC `tv:real`;\r
3507 ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];\r
3508 ASM_REAL_ARITH_TAC;\r
3509 (* ========= *)\r
3510 ASM_CASES_TAC ` tv = &0 `;\r
3511 DISJ2_TAC THEN DISJ1_TAC;\r
3512 EXISTS_TAC `tx:real`;\r
3513 EXISTS_TAC `tu:real`;\r
3514 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];\r
3515 ASM_REAL_ARITH_TAC;\r
3516 DISJ1_TAC;\r
3517 ASM_MESON_TAC[REAL_ARITH` &0 <= a /\ ~(a = &0 ) <=> &0 < a `];\r
3518 (* _______________ *)\r
3519 STRIP_TAC;\r
3520 ASM_MESON_TAC[REAL_ARITH` &0 <= a /\ ~(a = &0 ) <=> &0 < a `];\r
3521 (* iiiii *)\r
3522 EXISTS_TAC `tx:real`;\r
3523 EXISTS_TAC `tu:real `;\r
3524 EXISTS_TAC ` &0 `;\r
3525 ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_ADD_RID];\r
3526 REAL_ARITH_TAC;\r
3527 (* yyyyyyyyyyyy *)\r
3528 EXISTS_TAC ` tx:real `;\r
3529 EXISTS_TAC ` &0 `;\r
3530 EXISTS_TAC `tu:real`;\r
3531 ASM_SIMP_TAC[REAL_ADD_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID];\r
3532 REAL_ARITH_TAC]);;\r
3533 \r
3534 \r
3535 \r
3536 \r
3537 \r
3538 \r
3539 \r
3540 let AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL = \r
3541 prove_by_refinement(`~((v:real^3) = vec 0)/\\r
3542 ~( u = vec 0 ) /\\r
3543 ~(aff_ge {vec 0} {v} INTER aff_lt {vec 0} {u} = {}) \r
3544 ==> ~ (u = v ) /\ collinear {vec 0, u, v } `,\r
3545 [ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3546 STRIP_TAC THEN DOWN;\r
3547 ASM_SIMP_TAC[AFF_GE_1_1; \r
3548 REWRITE_RULE[SET_RULE` DISJOINT {a} {b} <=> ~( a = b ) `]\r
3549 AFF_LT_1_1; SET_RULE` ~( {} = a INTER b ) <=> ?x. x IN a /\ x IN b `];\r
3550 REWRITE_TAC[IN_ELIM_THM];\r
3551 STRIP_TAC;\r
3552 CONJ_TAC;\r
3553 STRIP_TAC;\r
3554 UNDISCH_TAC` x = t1' % vec 0 + t2' % (u:real^3) `;\r
3555 ASM_SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
3556 REWRITE_TAC[VECTOR_ARITH` a % x = b % x <=> (a - b ) % x = vec 0 `];\r
3557 REWRITE_TAC[VECTOR_MUL_EQ_0];\r
3558 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3559 ASM_SIMP_TAC[DE_MORGAN_THM];\r
3560 ASM_REAL_ARITH_TAC;\r
3561 (* hhhhhhhhhh *)\r
3562 ASM_REWRITE_TAC[COLLINEAR_LEMMA];\r
3563 EXISTS_TAC ` t2' / (t2:real) `;\r
3564 DOWN;\r
3565 ASM_SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
3566 \r
3567 ASM_CASES_TAC ` t2 = &0 `;\r
3568 ASM_SIMP_TAC[VECTOR_ARITH` &0 % x = c <=> c = vec 0`;VECTOR_MUL_EQ_0];\r
3569 ASM_REAL_ARITH_TAC;\r
3570 ASSUME_TAC2 (REAL_FIELD` ~( t2 = &0) ==> t2' = t2 * (t2' / t2 ) `);\r
3571 FIRST_ASSUM SUBST1_TAC;\r
3572 REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; VECTOR_MUL_LCANCEL];\r
3573 DOWN THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3574 SIMP_TAC[];\r
3575 REPEAT STRIP_TAC;\r
3576 ASM_REAL_ARITH_TAC]);;\r
3577 \r
3578 \r
3579 \r
3580 \r
3581 \r
3582 \r
3583 \r
3584 \r
3585 let CIZMRRH = prove_by_refinement\r
3586 (`local_fan (V,E,FF) ==>\r
3587 generic V E /\ ~(circular V E \/ (? v w. lunar (v,w) V E )) \/ \r
3588 circular V E /\ ~(generic V E \/ (? v w. lunar (v,w) V E )) \/ \r
3589 (? v w. lunar (v,w) V E ) /\ ~( generic V E \/ circular V E )  `,\r
3590 [ASM_CASES_TAC `(!v w u.\r
3591               {(v:real^3), w} IN E /\ u IN V\r
3592               ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})`;\r
3593 REWRITE_TAC[convex_local_fan; generic];\r
3594 STRIP_TAC;\r
3595 DISJ1_TAC;\r
3596 ASM_REWRITE_TAC[circular; lunar; DE_MORGAN_THM];\r
3597 CONJ_TAC;\r
3598 REWRITE_TAC[NOT_EXISTS_THM;\r
3599 TAUT` ~( a /\ b /\ c) <=> a /\ b ==> ~c `];\r
3600 ASM_MESON_TAC[\r
3601 SET_RULE` a INTER b = {} /\ aa SUBSET a ==> aa INTER b = {} `;\r
3602 AFF_GT_SUBSET_AFF_GE];\r
3603 REWRITE_TAC[GSYM circular; NOT_EXISTS_THM; DE_MORGAN_THM];\r
3604 REPEAT GEN_TAC THEN DISJ2_TAC;\r
3605 ASM_CASES_TAC `{v:real^3, w} SUBSET V `;\r
3606 DISJ2_TAC;\r
3607 REWRITE_TAC[GSYM (TAUT` ~ a ==> b <=> a \/ b `)];\r
3608 \r
3609 DOWN_TAC;\r
3610 REWRITE_TAC[local_fan];\r
3611 LET_TAC;\r
3612 NHANH FAN_IMP_NOT_EMPTY_DARTS;\r
3613 NHANH ELMS_OF_HYPERMAP_HYP;\r
3614 ASM_SIMP_TAC[];\r
3615 IMP_TAC;\r
3616 REWRITE_TAC[TAUT`(a/\b)/\c <=> a/\b/\c`];\r
3617 IMP_TAC;\r
3618 IMP_TAC;\r
3619 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3620 SIMP_TAC[];\r
3621 NHANH (MESON[dih2k]` dih2k H d ==> CARD (dart H) = 2 * d `);\r
3622 MP_TAC (ISPEC `H: (real^3#real^3)hypermap ` hypermap_lemma);\r
3623 REPEAT STRIP_TAC;\r
3624 ASSUME_TAC2 (ISPEC `dart (H:(real^3#real^3)hypermap)` CARD_EQ_0);\r
3625 UNDISCH_TAC` ~( {} = dart (H:(real^3#real^3)hypermap)) `;\r
3626 REWRITE_TAC[];\r
3627 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3628 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
3629 DOWN;\r
3630 ASM_REWRITE_TAC[ARITH_RULE`2 * k = 0 <=> k = 0 `];\r
3631 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
3632 STRIP_TAC;\r
3633 ASSUME_TAC2 (\r
3634 ISPECL [`CARD (FF:real^3#real^3 -> bool) `;`H:(real^3#real^3) hypermap `] \r
3635 (GEN_ALL DIH2K_IMP_NODE_MAP_X_DIFF_X));\r
3636 DOWN_TAC;\r
3637 REWRITE_TAC[FAN; INSERT_SUBSET; EMPTY_SUBSET];\r
3638 STRIP_TAC;\r
3639 ASSUME_TAC2 (SPEC `v:real^3 ` IN_V_OF_FAN_EXISTS_DART);\r
3640 DOWN;\r
3641 ASM_REWRITE_TAC[];\r
3642 FIRST_X_ASSUM NHANH;\r
3643 STRIP_TAC;\r
3644 DOWN THEN DOWN;\r
3645 UNDISCH_TAC` darts_of_hyp E (V:real^3 -> bool) = dart H `;\r
3646 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3647 SIMP_TAC[];\r
3648 STRIP_TAC;\r
3649 REWRITE_TAC[darts_of_hyp; IN_UNION; self_pairs; IN_ELIM_THM];\r
3650 ONCE_REWRITE_TAC[TAUT`a\/b <=> b\/a`];\r
3651 DISCH_THEN DISJ_CASES_TAC;\r
3652 DOWN THEN STRIP_TAC;\r
3653 UNDISCH_TAC `nn_of_hyp (vec 0,(V:real^3 -> bool),E) = node_map H`;\r
3654 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
3655 SIMP_TAC[];\r
3656 STRIP_TAC;\r
3657 \r
3658 \r
3659 SUBGOAL_THEN ` (v:real^3,v':real^3) IN darts_of_hyp E V ` MP_TAC;\r
3660 REWRITE_TAC[darts_of_hyp; IN_UNION];\r
3661 DISJ2_TAC;\r
3662 REWRITE_TAC[self_pairs; IN_ELIM_THM];\r
3663 EXISTS_TAC `v'':real^3`;\r
3664 ASM_REWRITE_TAC[];\r
3665 SIMP_TAC[nn_of_hyp];\r
3666 REMOVE_TAC;\r
3667 UNDISCH_TAC` EE (v'':real^3) E = {} `;\r
3668 DOWN THEN DOWN;\r
3669 SIMP_TAC[PAIR_EQ; EMPTY_SUBSET; W_SUBSET_SINGLETON_IMP_IDE];\r
3670 (* --------------------------------------------------- *)\r
3671 DOWN;\r
3672 REWRITE_TAC[ord_pairs; IN_ELIM_THM; PAIR_EQ];\r
3673 STRIP_TAC;\r
3674 ASM_REWRITE_TAC[];\r
3675 STRIP_TAC;\r
3676 UNDISCH_TAC` (w:real^3) IN V `;\r
3677 UNDISCH_TAC ` {(a:real^3),b} IN E `;\r
3678 PHA;\r
3679 UNDISCH_TAC `!v w u.\r
3680           {(v:real^3), w} IN E /\ u IN V\r
3681           ==> {} = aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u}`;\r
3682 DISCH_TAC;\r
3683 FIRST_ASSUM NHANH;\r
3684 DOWN_TAC;\r
3685 REWRITE_TAC[fan2];\r
3686 REWRITE_TAC[SET_RULE` ~( x IN s) <=> (!a. a IN s ==> ~(a = x )) `];\r
3687 REPLICATE_TAC 10 (IMP_TAC THEN DISCH_TAC);\r
3688 FIRST_X_ASSUM NHANH;\r
3689 STRIP_TAC;\r
3690 REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];\r
3691 CONJ_TAC THENL [\r
3692 EXPAND_TAC "a" THEN \r
3693 FIRST_ASSUM ACCEPT_TAC;\r
3694 CONJ_TAC THENL [\r
3695 FIRST_ASSUM ACCEPT_TAC;\r
3696 REWRITE_TAC[]]];\r
3697 \r
3698 ASSUME_TAC2 (ISPEC `vec 0:real^3 ` FAN7_SIMPLE);\r
3699 DOWN THEN PHA THEN STRIP_TAC;\r
3700 STRIP_TAC;\r
3701 ASM_CASES_TAC `c = &0 ` THENL [\r
3702 UNDISCH_TAC `w = c % (a:real^3)` THEN \r
3703 ASM_REWRITE_TAC[VECTOR_MUL_LZERO];\r
3704 ASM_CASES_TAC ` c = &1 `] THENL [\r
3705 UNDISCH_TAC `w = c % (a:real^3) ` THEN \r
3706 ASM_SIMP_TAC[VECTOR_MUL_LID] THEN \r
3707 EXPAND_TAC "a" THEN \r
3708 FIRST_X_ASSUM ACCEPT_TAC;\r
3709 ASM_CASES_TAC ` &0 < c `];\r
3710 (* ---------- sub 1    ---------- *)\r
3711 UNDISCH_TAC` w IN (V:real^3 -> bool) `;\r
3712 UNDISCH_TAC` v IN (V:real^3 -> bool) `;\r
3713 PHA;\r
3714 FIRST_ASSUM NHANH;\r
3715 UNDISCH_TAC`~(w = (v:real^3)) `;\r
3716 SIMP_TAC[SET_RULE`~(a = b) <=> {a} INTER {b} = {} `; INTER_COMM];\r
3717 REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];\r
3718 ASSUME_TAC2 (AFF_SGN_TRULE`!v. ~((v:real^3) = vec 0) ==>\r
3719 aff_ge {vec 0} {v} = { x| ?t0 tv. &0 <= tv /\ t0 + tv = &1 /\\r
3720 x = t0 % (vec 0) + tv % v } `);\r
3721 ASSUME_TAC2 (SPEC `w:real^3` (AFF_SGN_TRULE`!v. ~((v:real^3) = vec 0) ==>\r
3722 aff_ge {vec 0} {v} = { x| ?t0 tv. &0 <= tv /\ t0 + tv = &1 /\\r
3723 x = t0 % (vec 0) + tv % v } `));\r
3724 DOWN THEN DOWN THEN PHA THEN SIMP_TAC[];\r
3725 REPEAT STRIP_TAC;\r
3726 DOWN;\r
3727 UNDISCH_TAC ` ~((w:real^3) = vec 0) `;\r
3728 PHA;\r
3729 MATCH_MP_TAC (SET_RULE` a IN S ==> ~(~(a = x ) /\ S = {x}) `);\r
3730 REWRITE_TAC[IN_INTER; IN_ELIM_THM];\r
3731 CONJ_TAC;\r
3732 EXISTS_TAC` &1 - c `;\r
3733 EXISTS_TAC `c:real`;\r
3734 UNDISCH_TAC `&0 < c `;\r
3735 SIMP_TAC[REAL_ARITH` &0 < a ==> &0 <= a `;\r
3736 REAL_ARITH` &1 - c + c = &1 `; VECTOR_MUL_RZERO;\r
3737 VECTOR_ADD_LID];\r
3738 ASM_REWRITE_TAC[];\r
3739 (* ============================ *)\r
3740 EXISTS_TAC `&0 `;\r
3741 EXISTS_TAC `&1 `;\r
3742 \r
3743 SIMP_TAC[VECTOR_MUL_LID; VECTOR_MUL_RZERO;\r
3744 VECTOR_ADD_LID];\r
3745 REAL_ARITH_TAC;\r
3746 UNDISCH_TAC ` ~(c = &0 ) `;\r
3747 DOWN;\r
3748 PHA;\r
3749 REWRITE_TAC[REAL_ARITH` ~(&0 < c) /\ ~(c = &0) <=> c < &0 `];\r
3750 STRIP_TAC;\r
3751 UNDISCH_TAC` {} = aff_ge {vec 0} {a, b} INTER aff_lt {vec 0} {(w:real^3)}`;\r
3752 EXPAND_TAC "a";\r
3753 EXPAND_TAC "b";\r
3754 ASSUME_TAC2 (AFF_SGN_TRULE` ~((w:real^3) = vec 0) ==>\r
3755 aff_lt {vec 0} {w} = {x | ? t0 tw . tw < &0 /\ t0 + tw = &1 /\\r
3756 x = t0 % (vec 0) + tw % w }`);\r
3757 ASSUME_TAC2 (\r
3758 AFF_SGN_TRULE` ~((v:real^3) = vec 0) /\ ~( v' = vec 0) ==>\r
3759 aff_ge {vec 0} {v,v'} = {x | ? t0 tv tv' . &0 <= tv /\ \r
3760 &0 <= tv' /\ t0 + tv + tv' = &1 /\\r
3761 x = t0 % (vec 0) + tv % v + tv' % v'  }`);\r
3762 MATCH_MP_TAC (\r
3763 SET_RULE` -- (w:real^3) IN S ==> {} = S ==> F `);\r
3764 DOWN THEN DOWN THEN PHA THEN SIMP_TAC[];\r
3765 REMOVE_TAC;\r
3766 REWRITE_TAC[IN_INTER; IN_ELIM_THM];\r
3767 CONJ_TAC;\r
3768 EXISTS_TAC` &1 + c `;\r
3769 EXISTS_TAC ` -- (c:real) `;\r
3770 EXISTS_TAC `&0 `;\r
3771 ASM_REWRITE_TAC[VECTOR_MUL_LNEG; VECTOR_MUL_RZERO; VECTOR_MUL_LZERO; \r
3772 VECTOR_ADD_RID; VECTOR_ADD_LID];\r
3773 DOWN THEN REAL_ARITH_TAC;\r
3774 (* =================== *)\r
3775 EXISTS_TAC `&2 `;\r
3776 EXISTS_TAC ` -- &1 `;\r
3777 REWRITE_TAC[VECTOR_MUL_LNEG; VECTOR_MUL_LID; VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
3778 REAL_ARITH_TAC;\r
3779 (* +++++++++++++++++++++++++++++++++++++++++++++++++ *)\r
3780 (* ================================================= *)\r
3781 ASM_SIMP_TAC[];\r
3782 (* ************************************************* *)\r
3783 (* ================================================= *)\r
3784 DOWN;\r
3785 REWRITE_TAC[NOT_FORALL_THM; TAUT` ~( a ==> b) <=> a /\ ~ b `;\r
3786 local_fan];\r
3787 LET_TAC;\r
3788 REPEAT STRIP_TAC;\r
3789 DOWN_TAC;\r
3790 NHANH FAN_IMP_DIFF;\r
3791 STRIP_TAC;\r
3792 SUBGOAL_THEN ` (v:real^3) IN UNIONS E /\ w IN UNIONS E ` ASSUME_TAC\r
3793 THENL [REWRITE_TAC[IN_UNIONS] THEN \r
3794 ASM_MESON_TAC[SET_RULE` a IN {a,b} /\ b IN {a,b} `];\r
3795 DOWN_TAC];\r
3796 REWRITE_TAC[MESON[]`(!x. P x \/ Q x ==> R x) <=>\r
3797 (! x. P x ==> R x ) /\ (!x. Q x ==> R x ) `];\r
3798 STRIP_TAC;\r
3799 DOWN THEN DOWN;\r
3800 FIRST_X_ASSUM NHANH;\r
3801 UNDISCH_TAC `(u:real^3) IN V `;\r
3802 FIRST_ASSUM NHANH;\r
3803 REPEAT STRIP_TAC;\r
3804 ASSUME_TAC2 (\r
3805 AFF_SGN_TRULE` ~((v:real^3) = vec 0 ) /\ ~(w = vec 0 ) ==>\r
3806 aff_ge {vec 0} {v, w} = {x | ? t0 tv tw. &0 <= tv /\ &0 <= tw /\\r
3807 t0 + tv + tw = &1 /\ x = t0 % (vec 0) + tv % v + tw % w } `);\r
3808 ASSUME_TAC2 (\r
3809 ISPECL [`(vec 0):real^3 `;`u:real^3`] (REWRITE_RULE[DISJOINT; \r
3810 SET_RULE` {a} INTER {b} = {} <=> ~( b = a )`] AFF_LT_1_1));\r
3811 SUBGOAL_THEN` ~ (generic (V:real^3 -> bool) E )` ASSUME_TAC\r
3812 THENL [REWRITE_TAC[generic] THEN \r
3813 ASM_MESON_TAC[];\r
3814 UNDISCH_TAC `~(aff_ge {vec 0} {(v:real^3), w} INTER \r
3815 aff_lt {vec 0} {u} = {})`];\r
3816 ASSUME_TAC2 (\r
3817 ISPECL [` v:real^3 `;` (vec 0): real^3 `;` w:real^3 `] \r
3818 (GEN_ALL AFF_GE_TO_AFF_GT2_GE1));\r
3819 DOWN THEN SIMP_TAC[];\r
3820 STRIP_TAC;\r
3821 REWRITE_TAC[SET_RULE`( a UNION b ) INTER c = {} <=> a INTER c = {} /\\r
3822 b INTER c = {} `];\r
3823 STRIP_TAC;\r
3824 ASM_SIMP_TAC[];\r
3825 DOWN THEN REWRITE_TAC[DE_MORGAN_THM];\r
3826 DISCH_TAC;\r
3827 ASM_CASES_TAC ` circular (V:real^3 -> bool) E ` THENL [\r
3828 ASM_SIMP_TAC[lunar];\r
3829 DISJ2_TAC];\r
3830 ASM_SIMP_TAC[lunar];\r
3831 DOWN THEN DOWN THEN STRIP_TAC;\r
3832 (* there are three subgoal here *)\r
3833 (* -------- sub 1  -------------- *)\r
3834 REWRITE_TAC[circular];\r
3835 ASM_MESON_TAC[];\r
3836 (* --------- sub 2 --------------  *)\r
3837 DISCH_TAC;\r
3838 EXISTS_TAC `v:real^3`;\r
3839 EXISTS_TAC `u:real^3 `;\r
3840 ASSUME_TAC2 AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL;\r
3841 DOWN;\r
3842 ASM_SIMP_TAC[INSERT_COMM; INSERT_SUBSET; EMPTY_SUBSET];\r
3843 DISCH_TAC;\r
3844 MATCH_MP_TAC (SET_RULE`v IN UNIONS E /\ UNIONS E SUBSET V ==> v IN V `);\r
3845 DOWN_TAC;\r
3846 SIMP_TAC[FAN];\r
3847 (* -------------- sub 3 ------------- *)\r
3848 DISCH_TAC;\r
3849 EXISTS_TAC `u:real^3 `;\r
3850 EXISTS_TAC `w:real^3 `;\r
3851 ASSUME_TAC2 (\r
3852 SPEC `w:real^3 ` (GEN `v:real^3 ` AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL));\r
3853 ASM_SIMP_TAC[];\r
3854 ASM_SIMP_TAC[INSERT_COMM; INSERT_SUBSET; EMPTY_SUBSET];\r
3855 MATCH_MP_TAC (SET_RULE`v IN UNIONS E /\ UNIONS E SUBSET V ==> v IN V `);\r
3856 DOWN_TAC;\r
3857 SIMP_TAC[FAN]]);;\r
3858 \r
3859 \r
3860 end;;\r