legacy/oldlocal/nguyenquangtruong270983/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 (* needs "/home/user1/flyspeck/working/flyspeck_needs.hl";; *)\r
  11 (* =========== snapshot 1631 ===================== *)\r
  12 \r
  13 module Wrgcvdr (* : Trigonometry2_type *) = struct\r
  14 \r
  15 let build_sequence = \r
  16   ["general/sphere.hl";\r
  17    "general/prove_by_refinement.hl";\r
  18 (* "leg/geomdetail.hl";\r
  19    "leg/affprops.hl";\r
  20    "leg/cayleyR_def.hl";\r
  21    "leg/collect_geom.hl";\r
  22 (* flyspeck_needs  "leg/collect_geom2.hl";*) (* slow and rarely needed *)\r
  23    "nonlinear/ineq.hl";\r
  24    "nonlinear/ineqdata3q1h.hl"; *)\r
  25    "trigonometry/trig1.hl";\r
  26    "trigonometry/trig2.hl";\r
  27 (*   "trigonometry/trigonometry.hl";\r
  28    "volume/vol1.hl"; *)\r
  29    "hypermap/hypermap.hl"; \r
  30    "fan/fan.hl"];;\r
  31 \r
  32 map flyspeck_needs build_sequence;;\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 Prove_by_refinement;;\r
  40 \r
  41 \r
  42 let SET_TAC = let basicthms =\r
  43 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
  44 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
  45 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
  46 [IN_ELIM_THM; IN] in\r
  47 let PRESET_TAC =\r
  48 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
  49 REPEAT COND_CASES_TAC THEN\r
  50 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
  51 REWRITE_TAC allthms in\r
  52 fun ths ->\r
  53 PRESET_TAC THEN\r
  54 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
  55 MESON_TAC ths ;;\r
  56 \r
  57 (* =========== improved SET_RULE ============= *)\r
  58 let SET_RULE a = fun x -> prove(x, SET_TAC a );;\r
  59 \r
  60 \r
  61 \r
  62 let all_hy_map = let t1 = CONJ dart edge_map in\r
  63 let t2 = CONJ t1 node_map in\r
  64 CONJ t2 face_map;;\r
  65 \r
  66 \r
  67 \r
  68 let SPEC_HY_ELEMS = prove_by_refinement(\r
  69 `! (H: (A)hypermap) . tuple_hypermap H = (D,e,n,f) <=>\r
  70 dart H = D /\ edge_map H = e /\ node_map H = n /\ face_map H = f `,\r
  71 [ REWRITE_TAC[dart; all_hy_map];\r
  72 GEN_TAC THEN EQ_TAC;\r
  73 SIMP_TAC[FST; SND; PAIR];\r
  74 DISCH_TAC;\r
  75 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  76 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[];\r
  77 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  78 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[];\r
  79 PAT_ONCE_REWRITE_TAC`\x. x = y ` [GSYM PAIR] THEN \r
  80 REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[]]);;\r
  81 \r
  82 (* =============================== *)\r
  83 (* =============================== *)\r
  84 \r
  85 let hypermap = prove_by_refinement(\r
  86 `! H: (A) hypermap. tuple_hypermap H = D,e,n,f ==>\r
  87 e permutes D /\ n permutes D /\ f permutes D /\ e o n o f = I `,\r
  88 [REWRITE_TAC[SPEC_HY_ELEMS];\r
  89 GEN_TAC THEN MP_TAC (SPEC_ALL hypermap_lemma);\r
  90 ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `];\r
  91 SIMP_TAC[]]);;\r
  92 \r
  93 \r
  94 parse_as_infix("has_orders",(12,"right"));;\r
  95 parse_as_infix("cyclic_on",(13,"right"));;\r
  96 \r
  97 let has_orders = new_definition ` (f: A -> A) has_orders k <=>\r
  98 (! i. 0 < i /\ i < k ==> ~( ITER i f = I )) /\\r
  99 ITER k f = I `;;\r
 100 \r
 101 let cyclic_on = new_definition` f cyclic_on (S:A -> bool) <=>\r
 102 (! x. x IN S ==> S = {z | ?n. z = ITER n f x }) `;;\r
 103 \r
 104 \r
 105 let dih2k = new_definition` dih2k (H: (A) hypermap) k <=> \r
 106 CARD (dart H) = 2 * k\r
 107 /\ (! x. x IN (dart H) ==> let S = face H x in \r
 108          dart H = S UNION (IMAGE (node_map H) S ))\r
 109 /\ (face_map H ) has_orders k /\\r
 110 (edge_map H ) has_orders 2 /\\r
 111 (node_map H) has_orders 2 `;;\r
 112 \r
 113 \r
 114 let EE = new_definition` EE v S = {w | {v,w} IN S }`;;\r
 115 \r
 116 let ord_pairs = new_definition` ord_pairs E = { a,b | {a,b} IN E } `;;\r
 117 \r
 118 let self_pairs = new_definition` self_pairs E V = { (v,v) | v IN V /\\r
 119  EE v E = {} } `;;\r
 120 \r
 121 let darts_of_hyp = new_definition` darts_of_hyp E V = ord_pairs E UNION \r
 122 self_pairs E V `;;\r
 123 \r
 124 let e_of_hyp = new_definition` e_of_hyp ((a:real^3),(b:real^3)) = (b,a) `;;\r
 125 \r
 126 let n_of_hyp = new_definition` n_of_hyp (x,V,E) (v,u) =\r
 127 (v, azim_cycle (EE v E) x v u) `;;\r
 128 \r
 129 let ivs_azim_cycle = new_definition`ivs_azim_cycle W v0 v w =\r
 130 (@x. x IN W /\ azim_cycle W v0 v x = w ) `;;\r
 131 \r
 132 \r
 133 let f_of_hyp = new_definition` f_of_hyp (x,V,E) (v,u) =\r
 134 (u, ivs_azim_cycle (EE u E) x u  v) `;;\r
 135 \r
 136 let HYP = new_definition` HYP (x,V,E) = (darts_of_hyp E V,\r
 137 e_of_hyp, n_of_hyp (x,V,E), f_of_hyp (x,V,E)) `;;\r
 138 \r
 139 \r
 140 let local_fan = new_definition ` local_fan (V,E,FF ) <=>\r
 141  let H = hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) in\r
 142   FAN (vec 0, V, E) /\\r
 143   (?x. x IN ( dart H) /\ FF = face H x ) /\\r
 144 dih2k H (CARD FF ) `;;\r
 145 \r
 146 \r
 147 let azim_in_fan = new_definition` azim_in_fan (v:real^3,w:real^3) E = \r
 148 let d = (azim_cycle (EE v E) ( vec 0 ) v w) in\r
 149  if CARD ( EE v E ) > 1 then \r
 150  azim (vec 0 ) v w d else &2 * pi `;;\r
 151 \r
 152 let wedge_in_fan_gt = new_definition`wedge_in_fan_gt (v,w) E = \r
 153   if CARD (EE v E) > 1 then\r
 154 wedge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else if \r
 155 EE v E = {w} then { x | ~ ( x IN aff_ge {vec 0, v} {w} ) } else\r
 156 { x | ~ ( x IN aff {vec 0, v} )} `;;\r
 157 \r
 158 let wedge_ge = new_definition `wedge_ge  v0 v1 w1 w2 = { z |\r
 159 &0 <= azim v0 v1 w1 z /\ azim v0 v1 w1 z <= azim v0 v1 w1 w2 }`;;\r
 160 \r
 161 let wedge_in_fan_ge = new_definition` wedge_in_fan_ge ((v:real^3),w) E = \r
 162   if CARD (EE v E) > 1 then\r
 163 wedge_ge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else { x:real^3 | T } `;;\r
 164 \r
 165 let convex_local_fan = new_definition\r
 166   `convex_local_fan (V,E,FF) <=>\r
 167    local_fan (V,E,FF) /\\r
 168    (!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E)`;;\r
 169 \r
 170 (* this is the first assertion of AAUHTVE *)\r
 171 let FIRST_AAUHTVE = new_axiom \r
 172 `FAN (x,V,E) /\ HYP (x,V,E) = D,e,n,f\r
 173    ==> FINITE D /\\r
 174        e permutes D /\\r
 175        n permutes D /\\r
 176        f permutes D /\\r
 177        e o n o f = I /\\r
 178        e o e = I `;;\r
 179 \r
 180 \r
 181 let FST_SND_FORM_OF_4_TUPLE = GEN_ALL (\r
 182 prove_by_refinement(` FST X = D /\ FST (SND X) = e /\ \r
 183 FST (SND (SND X)) = n /\ SND (SND (SND X)) = f <=> X = D,e,n,f `,\r
 184 [EQ_TAC;\r
 185 STRIP_TAC;\r
 186 REPEAT (PAT_ONCE_REWRITE_TAC `\x. x = y `[GSYM PAIR] THEN\r
 187  ASM_SIMP_TAC[PAIR_EQ]);\r
 188 SIMP_TAC[PAIR_EQ]]));;\r
 189 (* =================================================== *)\r
 190 \r
 191 let HYP_LEMMA = prove_by_refinement(\r
 192 `! (x:real^3). FAN (x,V,E) ==> \r
 193 tuple_hypermap (hypermap (HYP (x,V,E))) = HYP (x,V,E) `,\r
 194 [GEN_TAC THEN ABBREV_TAC ` D = FST (HYP (x,V,E)) `;\r
 195 ABBREV_TAC ` e = FST ( SND (HYP (x,V,E))) `;\r
 196 ABBREV_TAC `n = FST (SND (SND (HYP (x,V,E)))) `;\r
 197 ABBREV_TAC `f = SND (SND (SND (HYP (x,V,E)))) `;\r
 198 REPEAT (DOWN THEN ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `]);\r
 199 PHA;\r
 200 REWRITE_TAC[FST_SND_FORM_OF_4_TUPLE];\r
 201 NHANH (FIRST_AAUHTVE);\r
 202 SIMP_TAC[];\r
 203 SIMP_TAC[GSYM hypermap_tybij]]);;\r
 204 \r
 205 \r
 206 \r
 207 \r
 208 let fan_expand = let t1 = CONJ fan fan1 in\r
 209 let t2 = CONJ fan2 t1 in\r
 210 let t3 = CONJ fan3 t2 in\r
 211 let t4 = CONJ fan4 t3 in\r
 212 let t5 = CONJ fan5 t4 in\r
 213 let t6 = CONJ fan6 t5 in\r
 214 let t7 = CONJ fan7 t6 in\r
 215 CONJ FAN t7;;\r
 216 \r
 217 prove(` UNIONS E SUBSET V /\ {(u:real^3), v} IN E ==> v IN V `,\r
 218 REWRITE_TAC[ UNIONS_SUBSET] THEN \r
 219 STRIP_TAC THEN \r
 220 MATCH_MP_TAC (SET_RULE[]` {u,v} SUBSET V ==> v IN V `) THEN \r
 221 FIRST_X_ASSUM MATCH_MP_TAC THEN \r
 222 ASM_SIMP_TAC[]);;\r
 223 \r
 224 \r
 225 \r
 226 let IN_V_OF_FAN_EXISTS_DART = GEN_ALL (\r
 227 prove_by_refinement(\r
 228 ` UNIONS E SUBSET (V:real^3 -> bool) /\ u IN V ==> \r
 229      ? v. v IN V /\ (u,v) IN darts_of_hyp E V `,\r
 230 [REWRITE_TAC[darts_of_hyp; IN_UNION; ord_pairs; self_pairs];\r
 231 PHA THEN DAO THEN STRIP_TAC THEN ASM_CASES_TAC `?(v:real^3). {u,v} IN E `;\r
 232 (* Subgoal 1 *)\r
 233 FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `v:real^3 `;\r
 234 ASSUME_TAC2 (prove(` UNIONS E SUBSET V /\ {(u:real^3), v} IN E ==> v IN V `,\r
 235 REWRITE_TAC[ UNIONS_SUBSET] THEN \r
 236 STRIP_TAC THEN \r
 237 MATCH_MP_TAC (SET_RULE[]` {u,v} SUBSET V ==> v IN V `) THEN \r
 238 FIRST_X_ASSUM MATCH_MP_TAC THEN \r
 239 ASM_SIMP_TAC[]));\r
 240 ASM_REWRITE_TAC[] THEN EVERY_ASSUM (fun x -> SET_TAC[x]);\r
 241 (* Subgoal 2 *)\r
 242 EXISTS_TAC `u:real^3 ` THEN ASM_REWRITE_TAC[EE];\r
 243 DISJ2_TAC THEN FIRST_X_ASSUM MP_TAC THEN SET_TAC[]]));;\r
 244 \r
 245 (* ======================================================== *)\r
 246 \r
 247 let X_IN_ITS_ORBIT = prove(` (x:A) IN orbit_map f x `,\r
 248 REWRITE_TAC[orbit_map; IN_ELIM_THM] THEN \r
 249 EXISTS_TAC ` 0 ` THEN REWRITE_TAC[POWER; I_THM; GE_REFL]);;\r
 250 \r
 251 let X_IN_HYP_ORBITS = prove(`! (x:A). x IN edge H x /\ x IN node H x /\ x IN face H x `,\r
 252 REWRITE_TAC[node; edge; face; X_IN_ITS_ORBIT]);;\r
 253 \r
 254 \r
 255 \r
 256 \r
 257 let ELMS_OF_HYPERMAP_HYP = prove_by_refinement\r
 258 (`FAN (x,V,E)\r
 259  ==> dart (hypermap (HYP (x,V,E))) = darts_of_hyp E V /\\r
 260      edge_map (hypermap (HYP (x,V,E))) = e_of_hyp /\\r
 261      node_map (hypermap (HYP (x,V,E))) = n_of_hyp (x,V,E) /\\r
 262      face_map (hypermap (HYP (x,V,E))) = f_of_hyp (x,V,E)`,\r
 263 [REWRITE_TAC[dart;edge_map; node_map; face_map];\r
 264 SIMP_TAC[HYP_LEMMA; HYP]]);;\r
 265 \r
 266 \r
 267 let POWER_SND = prove_by_refinement\r
 268 (`!n. f POWER SUC n = f o (f POWER n)`,\r
 269 [INDUCT_TAC;\r
 270 REWRITE_TAC[POWER; FUN_EQ_THM; o_THM; I_THM];\r
 271 DOWN THEN SIMP_TAC[POWER; FUN_EQ_THM; o_THM]]);;\r
 272 \r
 273 \r
 274 \r
 275 \r
 276 let N_HYP_TO_AZIM_CYCLE_LEM = \r
 277 prove_by_refinement(\r
 278 `!n. (n_of_hyp (x,V,E) POWER n) (u,v) = u,((azim_cycle (EE u E) x u) POWER n) v`,\r
 279 [INDUCT_TAC;\r
 280 REWRITE_TAC[POWER; I_THM];\r
 281 ASM_REWRITE_TAC[POWER_SND; o_THM; n_of_hyp]]);;\r
 282 \r
 283 \r
 284 prove(` UNIONS E SUBSET V /\ {a, b} IN E ==> a IN V /\ b IN V `,\r
 285 REWRITE_TAC[UNIONS_SUBSET;\r
 286 (GSYM o (SET_RULE[]))` {a,b} SUBSET V <=> a IN V /\ b IN V `] THEN \r
 287 MESON_TAC[]);;\r
 288 \r
 289 \r
 290 \r
 291 let IN_DARTS_HYP_IMP_FST_SND_IN_V = prove_by_refinement\r
 292 (`UNIONS E SUBSET V /\ (y:A#A) IN darts_of_hyp E V ==> FST y IN V /\ SND y IN V `,\r
 293 [SIMP_TAC[darts_of_hyp; ord_pairs; self_pairs; IN_UNION; IN_ELIM_THM];\r
 294 STRIP_TAC;\r
 295 (* sub 1 *)\r
 296 ASM_SIMP_TAC[];\r
 297 MATCH_MP_TAC (prove(` UNIONS E SUBSET V /\ {a, b} IN E ==> a IN V /\ b IN V `,\r
 298 REWRITE_TAC[UNIONS_SUBSET;\r
 299 (GSYM o (SET_RULE[]))` {a,b} SUBSET V <=> a IN V /\ b IN V `] THEN \r
 300 MESON_TAC[]));\r
 301 ASM_SIMP_TAC[];\r
 302 (* sub 2 *)\r
 303 ASM_SIMP_TAC[FST; SND]]);;\r
 304 \r
 305 let POWER_TO_ITER = prove(`! n. (f POWER n) = ITER n f `,\r
 306 INDUCT_TAC THENL [\r
 307 REWRITE_TAC[POWER; ITER; FUN_EQ_THM; I_THM];\r
 308 ASM_REWRITE_TAC[POWER_SND; ITER; FUN_EQ_THM; o_THM]]);;\r
 309 \r
 310 \r
 311 let SND_IN_SET_OF_DART_OF_FRST = prove(\r
 312 ` UNIONS (E:(A -> bool) -> bool) SUBSET (V:A -> bool) /\ y IN darts_of_hyp E V ==> \r
 313 FST y = SND y \/ SND y IN set_of_edge (FST y) V E`,\r
 314 REWRITE_TAC[set_of_edge; darts_of_hyp; ord_pairs; \r
 315 self_pairs; IN_ELIM_THM; IN_UNION] THEN\r
 316 STRIP_TAC THENL [\r
 317 ASM_SIMP_TAC[] THEN \r
 318 DISJ2_TAC THEN \r
 319 ASM_MESON_TAC[prove(` UNIONS E SUBSET V /\ {(u:A), v} IN E ==> v IN V `,\r
 320 REWRITE_TAC[ UNIONS_SUBSET] THEN \r
 321 STRIP_TAC THEN \r
 322 MATCH_MP_TAC (SET_RULE[]` {u,v} SUBSET V ==> v IN V `) THEN \r
 323 FIRST_X_ASSUM MATCH_MP_TAC THEN \r
 324 ASM_SIMP_TAC[])];\r
 325 ASM_SIMP_TAC[]]);;\r
 326 \r
 327 \r
 328 \r
 329 let UNI_E_IMP_EE_EQ_SET_OF_EDGE = \r
 330 prove(` UNIONS E SUBSET V ==> EE (v:A) E = set_of_edge v V E `,\r
 331 REWRITE_TAC[EE; set_of_edge] THEN \r
 332 REWRITE_TAC[UNIONS_SUBSET; FUN_EQ_THM; IN_ELIM_THM]\r
 333 THEN REWRITE_TAC[MESON[]`( a <=> a /\ b ) <=> a ==> b `] \r
 334 THEN REPEAT STRIP_TAC\r
 335 THEN MATCH_MP_TAC (SET_RULE[]` {v:A,b} SUBSET V ==> b IN V `)\r
 336 THEN ASM_MESON_TAC[]);;\r
 337 \r
 338 \r
 339 \r
 340 let types_in_th th = let t = frees (concl (SPEC_ALL th)) in\r
 341   map dest_var t;;\r
 342 \r
 343 \r
 344 let IN_ORD_PAIRS_IMP_IMP_IN_TOO = \r
 345 prove_by_refinement(\r
 346 `y IN ord_pairs E ==> ((FST y):A,d) IN darts_of_hyp E V ==>\r
 347   ((FST y),d) IN ord_pairs E `,\r
 348 [REWRITE_TAC[ord_pairs; darts_of_hyp; \r
 349 self_pairs; IN_ELIM_THM] THEN \r
 350 REPEAT STRIP_TAC;\r
 351 (* sub 1 *)\r
 352 EXISTS_TAC `FST (y:A#A)` THEN \r
 353 EXISTS_TAC `d: A` THEN \r
 354 DOWN;\r
 355 REWRITE_TAC[IN_UNION; IN_ELIM_THM];\r
 356 STRIP_TAC;\r
 357 DOWN_TAC;\r
 358 SIMP_TAC[PAIR_EQ];\r
 359 (* sub 2 *)\r
 360 DOWN_TAC;\r
 361 IMP_TAC THEN IMP_TAC THEN SIMP_TAC[];\r
 362 SIMP_TAC[EE; PAIR_EQ]; SET_TAC[]]);;\r
 363 \r
 364 \r
 365 \r
 366 \r
 367 let IN_ORD_PAIRS_IMP_SND_IN_EE_FST = prove(\r
 368 `y IN ord_pairs E ==> SND y IN (EE (FST y) E) `   ,\r
 369 REWRITE_TAC[ord_pairs; EE; IN_ELIM_THM]\r
 370 THEN STRIP_TAC \r
 371 THEN ASM_SIMP_TAC[]);;\r
 372 \r
 373 \r
 374 \r
 375 \r
 376 \r
 377 \r
 378 let IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL = \r
 379 prove_by_refinement(\r
 380 `! (v:A). y IN self_pairs E V /\ FST y,v IN darts_of_hyp E V ==> FST y = v`,\r
 381 [GEN_TAC THEN REWRITE_TAC[self_pairs; darts_of_hyp];\r
 382 REWRITE_TAC[IN_ELIM_THM; ord_pairs; IN_UNION; EE];\r
 383 STRIP_TAC;\r
 384 DOWN;\r
 385 ASM_SIMP_TAC[PAIR_EQ];\r
 386 STRIP_TAC;\r
 387 ASM SET_TAC[];\r
 388 DOWN THEN SIMP_TAC[PAIR_EQ]]);;\r
 389 \r
 390 \r
 391 \r
 392 \r
 393 (* John is helping me in this lemma *)\r
 394 let CYCLIC_SET_IMP_STABLE_SET = new_axiom\r
 395 `cyclic_set (W:real^3 -> bool) v w ==> \r
 396 (! x. x IN W ==> W = { y | ? n. y = ITER n (azim_cycle W v w) x})`;;\r
 397 \r
 398 \r
 399 \r
 400 let choose_nd_point = new_specification ["choose_nd_point"]\r
 401   (REWRITE_RULE[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] IN_V_OF_FAN_EXISTS_DART);;\r
 402 \r
 403 \r
 404 \r
 405 \r
 406 \r
 407 \r
 408 let FAN_IMP_BIJ_V_NODE_OF_HYP = \r
 409 prove_by_refinement(\r
 410 `FAN ((x:real^3),V,E) /\\r
 411  f =\r
 412  (\u. if u IN V\r
 413       then node (hypermap (HYP (x,V,E))) (u,choose_nd_point u E V)\r
 414       else {})\r
 415  ==> BIJ f V {node (hypermap (HYP (x,V,E))) y | y | y IN darts_of_hyp E V}`,\r
 416 [STRIP_TAC;\r
 417 ASM_SIMP_TAC[];\r
 418 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);\r
 419 ASSUME_TAC choose_nd_point;\r
 420 REWRITE_TAC[BIJ] THEN CONJ_TAC;\r
 421 (* subgoal 1 *)\r
 422 REWRITE_TAC[INJ] THEN CONJ_TAC;\r
 423 (* subgoal 1.1 *)\r
 424 GEN_TAC THEN SIMP_TAC[];\r
 425 UNDISCH_TAC `FAN ((x:real^3),V,E) `;\r
 426 REWRITE_TAC[FAN] THEN REPEAT STRIP_TAC;\r
 427 ASM SET_TAC[];\r
 428 (* subgoal 1.2 *)\r
 429 IMP_TAC THEN IMP_TAC THEN SIMP_TAC[];\r
 430 NHANH (MESON[X_IN_HYP_ORBITS] `node H (x:A) = A ==> x IN A `);\r
 431 REPEAT STRIP_TAC;\r
 432 DOWN;\r
 433 ASM_SIMP_TAC[node; ELMS_OF_HYPERMAP_HYP; orbit_map; IN_ELIM_THM];\r
 434 STRIP_TAC;\r
 435 DOWN THEN REWRITE_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
 436 SIMP_TAC[PAIR_EQ];\r
 437 (* suggoal 2 *)\r
 438 REWRITE_TAC[SURJ] THEN CONJ_TAC;\r
 439 (* subgoal 2.1 *)\r
 440 GEN_TAC THEN SIMP_TAC[];\r
 441 UNDISCH_TAC `FAN ((x:real^3),V,E) `;\r
 442 REWRITE_TAC[FAN] THEN REPEAT STRIP_TAC;\r
 443 ASM SET_TAC[];\r
 444 (* subgaol 2.2 *)\r
 445 GEN_TAC;\r
 446 REWRITE_TAC[IN_ELIM_THM];\r
 447 STRIP_TAC;\r
 448 EXISTS_TAC ` FST (y:real^3 # real^3 )`;\r
 449 UNDISCH_TAC ` FAN ((x:real^3),V,E) `;\r
 450 REWRITE_TAC[FAN] THEN STRIP_TAC;\r
 451 ASSUME_TAC2 (ISPECL [`E:(real^3 -> bool) -> bool `;\r
 452 ` y: real^3 # real^3`;`V:real^3 -> bool `]\r
 453   (GEN_ALL IN_DARTS_HYP_IMP_FST_SND_IN_V));\r
 454 ASM_SIMP_TAC[node; REWRITE_RULE[FAN] ELMS_OF_HYPERMAP_HYP];\r
 455 MP_TAC (ISPECL [`x: real^3 `;` V:real^3 -> bool `;\r
 456 ` E: (real^3 -> bool) -> bool`;\r
 457   `FST (y:real^3# real^3 ) `] XOHLED);\r
 458 ANTS_TAC;\r
 459 REPLICATE_TAC 5 DOWN;\r
 460 PHA THEN ASM_SIMP_TAC[FAN];\r
 461 REWRITE_TAC[orbit_map;N_HYP_TO_AZIM_CYCLE_LEM];\r
 462 MP_TAC (ISPEC `y: real^3#real^3` (GSYM PAIR));\r
 463 ABBREV_TAC `fy = FST (y:real^3#real^3)`;\r
 464 ABBREV_TAC `sy = SND (y:real^3#real^3)`;\r
 465 SIMP_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
 466 DISCH_TAC;\r
 467 FIRST_X_ASSUM (MP_TAC o (SPECL [`fy: real^3 `]));\r
 468 DISCH_THEN (MP_TAC o SPEC_ALL) THEN ANTS_TAC;\r
 469 (* sub I *)\r
 470 ASM_SIMP_TAC[];\r
 471 (* sub II *)\r
 472 REPEAT STRIP_TAC;\r
 473 ASSUME_TAC2 (SPEC_ALL (ISPECL [`fy:real^3`] (GEN_ALL UNI_E_IMP_EE_EQ_SET_OF_EDGE)));\r
 474 FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);\r
 475 ASM_CASES_TAC `(y:real^3 # real^3) IN ord_pairs E `;\r
 476 ASSUME_TAC (UNDISCH (SPEC_ALL (\r
 477 ISPECL [`V: real^3 -> bool `;` y:real^3 # real^3 `;` (choose_nd_point: real^3 -> \r
 478 ((real^3 -> bool) -> bool) ->(real^3 -> bool) -> real^3) fy E V`;`\r
 479 E:(real^3 -> bool) -> bool `]\r
 480  (GEN_ALL IN_ORD_PAIRS_IMP_IMP_IN_TOO))));\r
 481 DOWN;\r
 482 ASM_REWRITE_TAC[];\r
 483 DOWN THEN NHANH IN_ORD_PAIRS_IMP_SND_IN_EE_FST;\r
 484 ASM_REWRITE_TAC[];\r
 485 REPEAT STRIP_TAC;\r
 486 \r
 487 DOWN_TAC THEN NHANH CYCLIC_SET_IMP_STABLE_SET;\r
 488 STRIP_TAC;\r
 489 FIRST_ASSUM (ASSUME_TAC o (SPEC `sy:real^3 `));\r
 490 \r
 491 FIRST_ASSUM (ASSUME_TAC o (SPEC `(choose_nd_poind: real^3 -> \r
 492 ((real^3 -> bool) -> bool) ->(real^3 -> bool) -> real^3) fy E V`));\r
 493 \r
 494 \r
 495 DOWN THEN DOWN THEN DISCH_THEN ASSUME_TAC2;\r
 496 FIRST_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC `\x. x = a ==> b ` [x]);\r
 497 STRIP_TAC;\r
 498 \r
 499 REWRITE_TAC[EXTENSION];\r
 500 GEN_TAC THEN EQ_TAC;\r
 501 (* sub 2.1 *)\r
 502 REWRITE_TAC[IN_ELIM_THM; ARITH_RULE` n >= 0 `];\r
 503 DISCH_THEN CHOOSE_TAC;\r
 504 ASM_SIMP_TAC[PAIR_EQ; POWER_TO_ITER];\r
 505 DOWN THEN DOWN;\r
 506 SET_TAC[];\r
 507 (* sub 2.2 *)\r
 508 REWRITE_TAC[IN_ELIM_THM; ARITH_RULE` n >= 0 `];\r
 509 DISCH_THEN CHOOSE_TAC;\r
 510 ASM_SIMP_TAC[PAIR_EQ; POWER_TO_ITER];\r
 511 DOWN THEN DOWN;\r
 512 SET_TAC[];\r
 513 (* sub IIIIII *)\r
 514 \r
 515 ASSUME_TAC2 (prove(`y IN darts_of_hyp E (V:real^3 -> bool)\r
 516  /\ ~(y IN ord_pairs E)\r
 517 ==> y IN self_pairs E V `,\r
 518 REWRITE_TAC[darts_of_hyp; IN_UNION]\r
 519 THEN CONV_TAC TAUT));\r
 520 UNDISCH_TAC `fy,choose_nd_point fy E V IN darts_of_hyp E (V:real^3 -> bool) `;\r
 521 DOWN;\r
 522 EXPAND_TAC "fy";\r
 523 PHA;\r
 524 NHANH IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL;\r
 525 STRIP_TAC;\r
 526 UNDISCH_TAC `y IN darts_of_hyp E (V:real^3 -> bool) `;\r
 527 UNDISCH_TAC `y IN self_pairs E (V:real^3 -> bool) `;\r
 528 PHA;\r
 529 UNDISCH_TAC `y = (fy:real^3), (sy: real^3 ) `;\r
 530 ASM_REWRITE_TAC[];\r
 531 SIMP_TAC[];\r
 532 EXPAND_TAC "fy";\r
 533 DISCH_THEN (fun x -> PAT_REWRITE_TAC`\x. x /\ y ==> z ` [GSYM x]);\r
 534 NHANH IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL;\r
 535 DOWN;\r
 536 ASM_REWRITE_TAC[];\r
 537 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
 538 SIMP_TAC[]]);;\r
 539 \r
 540 \r
 541 \r
 542 \r
 543 \r
 544 \r
 545 \r
 546 \r
 547 \r
 548 \r
 549 let ITER_N_I = prove(`! n. ITER n I = I`,\r
 550 INDUCT_TAC THENL [\r
 551 REWRITE_TAC[ITER; FUN_EQ_THM; I_THM];\r
 552 ASM_REWRITE_TAC[ITER; FUN_EQ_THM; I_THM]]);;\r
 553 \r
 554 \r
 555 \r
 556 \r
 557 \r
 558 \r
 559 let HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW = \r
 560 prove_by_refinement(\r
 561 `(f: A -> A) has_orders k /\ ~ (k = 0 ) ==>\r
 562 (! x. orbit_map f x = { y| ? n. 0 <= n /\ n < k /\ y = ITER n f x }) `,\r
 563 [ REWRITE_TAC[has_orders; orbit_map; POWER_TO_ITER];\r
 564 REWRITE_TAC[FUN_EQ_THM];\r
 565 REPEAT STRIP_TAC;\r
 566 REWRITE_TAC[IN_ELIM_THM];\r
 567 EQ_TAC;\r
 568 STRIP_TAC;\r
 569 EXISTS_TAC `n MOD k `;\r
 570 ASM_SIMP_TAC[LE_0; DIVISION];\r
 571 ASSUME_TAC2 (SPECL [` n: num `;` k:num `] DIVISION);\r
 572 FIRST_X_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC `\x. x = y ` [x]);\r
 573 REWRITE_TAC[GSYM ITER_ADD; GSYM ITER_MUL];\r
 574 UNDISCH_TAC `!x. ITER k (f: A -> A) x = I x`;\r
 575 SIMP_TAC[GSYM FUN_EQ_THM; ETA_AX; ITER_N_I; I_THM];\r
 576 STRIP_TAC;\r
 577 REWRITE_TAC[ARITH_RULE` n >= 0 `];\r
 578 EXISTS_TAC `n: num `;\r
 579 ASM_REWRITE_TAC[]]);;\r
 580 \r
 581 \r
 582 \r
 583 let FINITE_OF_N_FIRST_ELMS = \r
 584 prove_by_refinement(\r
 585 `! k (x:A). FINITE {y | ?n. n < k /\ y = ITER n f x}`,\r
 586 [INDUCT_TAC;\r
 587 REWRITE_TAC[ ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; FINITE_EMPTY];\r
 588 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 589 KHANANG;\r
 590 REWRITE_TAC[SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 591   UNION { y | ? n. Q n y } `];\r
 592 DOWN;\r
 593 REWRITE_TAC[LE_0; SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 594 SIMP_TAC[FINITE_UNION; FINITE_SINGLETON]]);;\r
 595 \r
 596 \r
 597 \r
 598 \r
 599 \r
 600 let F_HAS_ORDERS_IMP_FINITE_ORBIT = \r
 601 prove_by_refinement(\r
 602 ` (f: A -> A) has_orders k /\ ~( k = 0 ) ==>\r
 603 (! x. FINITE (orbit_map f x )) `,\r
 604 [NHANH HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW;\r
 605 SIMP_TAC[] THEN STRIP_TAC;\r
 606 SPEC_TAC (`k:num `,` k:num`);\r
 607 INDUCT_TAC;\r
 608 REWRITE_TAC[ ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; FINITE_EMPTY];\r
 609 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 610 KHANANG;\r
 611 REWRITE_TAC[SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 612   UNION { y | ? n. Q n y } `];\r
 613 DOWN;\r
 614 REWRITE_TAC[LE_0; SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 615 SIMP_TAC[FINITE_UNION; FINITE_SINGLETON]]);;\r
 616 \r
 617 \r
 618 \r
 619 \r
 620 \r
 621 \r
 622 \r
 623 let CARD_CLAUSES2 = prove(`FINITE (S: A -> bool) \r
 624  ==> (!x. x IN S ==> CARD (x INSERT S) = CARD S) /\\r
 625      (!x. ~(x IN S) ==> CARD (x INSERT S) = SUC (CARD S))`,\r
 626 SIMP_TAC[CARD_CLAUSES]);;\r
 627 \r
 628 \r
 629 let CARD_INSERT_GE_AND_LE = prove(\r
 630 `FINITE (S: A -> bool) ==> CARD S <= CARD (x INSERT S ) /\\r
 631 CARD (x INSERT S) <= SUC ( CARD S)`,\r
 632 SIMP_TAC[CARD_CLAUSES] THEN \r
 633 COND_CASES_TAC THENL [\r
 634 DISCH_TAC THEN ARITH_TAC;\r
 635 DISCH_TAC THEN ARITH_TAC]);;\r
 636 \r
 637 \r
 638 \r
 639 \r
 640 \r
 641 let HAVING_ORDERS_K_IMP_CARD_ORBIT_LE_K = \r
 642 prove_by_refinement(\r
 643 `(f: A -> A) has_orders k /\ ~( k = 0 ) ==>\r
 644 (! x. CARD (orbit_map f x) <= k )`,\r
 645 [SIMP_TAC[HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW ];\r
 646 STRIP_TAC;\r
 647 SPEC_TAC (`k: num `,` k: num`);\r
 648 INDUCT_TAC;\r
 649 REWRITE_TAC[LE_0; ARITH_RULE ` ~( n < 0 ) `; EMPTY_GSPEC; CARD_CLAUSES];\r
 650 REWRITE_TAC[ARITH_RULE` x < SUC k <=> x < k \/ x = k `];\r
 651 GEN_TAC;\r
 652 KHANANG;\r
 653 REWRITE_TAC[SET_RULE[]` { y | ? n. P n y \/ Q n y } = {y | ? n. P n y }\r
 654   UNION { y | ? n. Q n y } `];\r
 655 DOWN;\r
 656 REWRITE_TAC[LE_0; SET_RULE[]` {y| ? n. n = k /\ y = P n } = { P k } `];\r
 657 SIMP_TAC[SET_RULE[]` a UNION {x} = x INSERT a `];\r
 658 MP_TAC (SPECL [`k' :num `;`x: A `] FINITE_OF_N_FIRST_ELMS);\r
 659 NHANH (ISPEC ` ITER k' f (x:A) ` ( GEN `x :A ` CARD_INSERT_GE_AND_LE));\r
 660 STRIP_TAC THEN STRIP_TAC;\r
 661 FIRST_X_ASSUM (MP_TAC o (SPEC `x: A `));\r
 662 DOWN;\r
 663 ARITH_TAC]);;\r
 664 \r
 665 (* CARD_LE_K_OF_SET_K_FIRST_ELMS \r
 666 |- CARD {ITER i f x | i < k} <= k *)\r
 667 let CARD_LE_K_OF_SET_K_FIRST_ELMS = \r
 668 BETA_RULE (SPECL [`k: num `;`(\i. ITER i (f: A -> A) x )`] \r
 669 CARD_FINITE_SERIES_LE);;\r
 670 \r
 671 \r
 672 \r
 673 \r
 674 \r
 675 \r
 676 let CARD_K_FIRST_ELMS_EQ_K = \r
 677 prove_by_refinement(\r
 678 `! k (f: A -> A). CARD {ITER n f x | n < k} = k ==>\r
 679      CARD {ITER n f x | n < k - 1} = k - 1 /\\r
 680      (!i. i < k - 1 ==> ~(ITER i f x = ITER ( k - 1 ) f x))`,\r
 681 [INDUCT_TAC;\r
 682 REWRITE_TAC[ARITH_RULE ` ~( a < 0 - 1 ) `; LT];\r
 683 REWRITE_TAC[SET_RULE[]` {ITER n f x | n | F} = {} `; CARD_CLAUSES];\r
 684 ARITH_TAC;\r
 685 GEN_TAC;\r
 686 REWRITE_TAC[ARITH_RULE ` a < SUC k <=> a < k  \/ a = k `];\r
 687 REWRITE_TAC[SET_RULE[]` { ITER n f x | n < k \/ n = k } = ITER k f x INSERT { ITER n f x | n < k } `];\r
 688 ASM_CASES_TAC ` ITER k f (x:A) IN {ITER n f x | n < k} `;\r
 689 MP_TAC (SPEC_ALL FINITE_OF_N_FIRST_ELMS);\r
 690 REWRITE_TAC[SET_RULE[]` {y | ?n. n < k /\ y = ITER n f x} = {ITER n f x | n < k} `];\r
 691 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_OF_N_FIRST_ELMS];\r
 692 DISCH_TAC THEN MP_TAC CARD_LE_K_OF_SET_K_FIRST_ELMS;\r
 693 ARITH_TAC;\r
 694 DOWN;\r
 695 MP_TAC (SPEC_ALL FINITE_OF_N_FIRST_ELMS);\r
 696 REWRITE_TAC[SET_RULE[]` {y | ?n. n < k /\ y = ITER n f x} = {ITER n f x | n < k} `];\r
 697 SIMP_TAC[ARITH_RULE ` SUC k - 1 = k `; CARD_CLAUSES; SUC_INJ];\r
 698 DISCH_TAC;\r
 699 SET_TAC[]]);;\r
 700 \r
 701 \r
 702 let FINITENESS_OF_K_FIRST_ELMS = prove_by_refinement(\r
 703 `! k (f: num -> A). FINITE { f n | n < k }`,\r
 704 [INDUCT_TAC;\r
 705 REWRITE_TAC[LT; SET_RULE[]` {f n | n | F } = {} `; FINITE_RULES];\r
 706 REWRITE_TAC[ARITH_RULE` n < SUC k <=> n < k \/ n = k `;\r
 707   SET_RULE[]` {(f: num -> A) n | n < k \/ n = k} = f k INSERT {f n | n < k } `];\r
 708 ASM_REWRITE_TAC[FINITE_INSERT]]);;\r
 709 \r
 710 \r
 711 let LT_SUC_E = ARITH_RULE` i < SUC k <=> i < k \/ i = k `;;\r
 712 \r
 713 (* |- !k. CARD {f i | i < k} <= k *)\r
 714 let CARD_K_FIRST_ELMS_LE_K = \r
 715 GEN `k: num ` (SPECL [`k: num `;` f: num -> A `] CARD_FINITE_SERIES_LE);;\r
 716 \r
 717 \r
 718 \r
 719 let REMOVE_TAC = MATCH_MP_TAC (TAUT ` a ==> b ==> a `);;\r
 720 \r
 721 \r
 722 \r
 723 let CARD_N_FIRST_ELMS_UNDUCTIVE = prove_by_refinement(\r
 724 `! k (f: num -> A ). CARD { f n | n < k} = k <=>\r
 725     CARD {f n | n < k - 1} = k - 1 /\\r
 726      (!i. i < k - 1 ==> ~(f i = f ( k - 1 )))`,\r
 727 [REPEAT GEN_TAC;\r
 728 ASM_CASES_TAC ` k = 0 `;\r
 729 ASM_SIMP_TAC[ARITH_RULE` ~( x < 0 - 1 ) `; LT; ARITH_RULE` 0 - 1 = 0 `];\r
 730 DOWN;\r
 731 NHANH (ARITH_RULE` ~( k = 0 ) ==> (! n. n < k <=> n < k - 1 \/ n = k - 1 ) `);\r
 732 SIMP_TAC[];\r
 733 STRIP_TAC;\r
 734 REWRITE_TAC[SET_RULE[]` {(f:num -> A) n | n < k - 1 \/ n = k - 1}\r
 735   = f ( k - 1 ) INSERT {f n | n < k - 1 }`];\r
 736 MP_TAC (SPECL [` k - 1 `;` f: num -> A `] FINITENESS_OF_K_FIRST_ELMS);\r
 737 DISCH_TAC;\r
 738 EQ_TAC;\r
 739 (* sub 1 *)\r
 740 ASM_SIMP_TAC[CARD_CLAUSES];\r
 741 COND_CASES_TAC;\r
 742 (* sub 1.1 *)\r
 743 MP_TAC (SPEC ` k - 1 ` CARD_K_FIRST_ELMS_LE_K);\r
 744 UNDISCH_TAC ` ~( k = 0 ) `;\r
 745 MESON_TAC[ARITH_RULE `~ ( ~(k = 0) /\ a <= k - 1 /\ a = k ) `];\r
 746 (* sub 1.2 *)\r
 747 UNDISCH_TAC ` ~( k = 0 ) `;\r
 748 SIMP_TAC[ARITH_RULE ` ~( k = 0 ) ==> ( SUC x = k <=> x = k - 1 )`];\r
 749 MATCH_MP_TAC (TAUT ` a ==> b ==> a `);\r
 750 MATCH_MP_TAC (TAUT ` a ==> b ==> a `);\r
 751 DOWN;\r
 752 REWRITE_TAC[IN_ELIM_THM];\r
 753 MESON_TAC[];\r
 754 (* SUB 2 *)\r
 755 STRIP_TAC;\r
 756 SUBGOAL_THEN ` ~( f ( k - 1 ) IN {(f: num -> A) n | n < k - 1})` ASSUME_TAC;\r
 757 DOWN THEN REWRITE_TAC[IN_ELIM_THM];\r
 758 MESON_TAC[];\r
 759 ASM_SIMP_TAC[CARD_CLAUSES];\r
 760 UNDISCH_TAC `~( k = 0 ) `;\r
 761 ARITH_TAC]);;\r
 762 \r
 763 \r
 764 \r
 765 \r
 766 \r
 767 let CARD_ADD1_LE = prove_by_refinement(\r
 768 `! f: num -> A. CARD { f n | n < k + 1 } <= CARD {f n | n < k } + 1 `,\r
 769 [REWRITE_TAC[ARITH_RULE` a < v + 1 <=> a < v \/ a = v `;\r
 770   SET_RULE[]` {(f: num -> A) n | n < k \/ n = k} = f k INSERT {f n | n < k } `];\r
 771 GEN_TAC;\r
 772 MP_TAC (SPEC_ALL FINITENESS_OF_K_FIRST_ELMS);\r
 773 SIMP_TAC[CARD_CLAUSES];\r
 774 COND_CASES_TAC;\r
 775 DISCH_TAC THEN ARITH_TAC;\r
 776 DISCH_TAC THEN ARITH_TAC]);;\r
 777 \r
 778 \r
 779 \r
 780 \r
 781 \r
 782 let CARD_LT_KT_LE_ADDT = \r
 783 prove_by_refinement(\r
 784 ` CARD { (f: num -> A) n | n < k + t } <= CARD {f n | n < k } + t `,\r
 785 [SPEC_TAC (`t:num `,` t:num `);\r
 786 INDUCT_TAC;\r
 787 REWRITE_TAC[ADD_0; LE_REFL];\r
 788 REWRITE_TAC[ADD1];\r
 789 REWRITE_TAC[ARITH_RULE` a + b + 1 = (a + b ) + 1 `];\r
 790 MP_TAC (SPECL [` k + (t:num) `;` f: num -> A `] (GEN_ALL CARD_ADD1_LE));\r
 791 DOWN THEN ARITH_TAC]);;\r
 792 \r
 793 \r
 794 \r
 795 \r
 796 \r
 797 let CARD_KS_EQ_K_EQ_ALL_LE = prove_by_refinement\r
 798 (`! k (f: num -> A ). CARD { f n | n < k} = k <=>\r
 799 (! kk. kk <= k ==> CARD { f n | n < kk} = kk ) `,\r
 800 [REPEAT STRIP_TAC;\r
 801 EQ_TAC;\r
 802 REPEAT STRIP_TAC;\r
 803 ASM_CASES_TAC ` CARD {(f: num -> A) n | n < kk} = kk`;\r
 804 ASM_SIMP_TAC[];\r
 805 ASSUME_TAC (SPEC `kk: num ` CARD_K_FIRST_ELMS_LE_K );\r
 806 UNDISCH_TAC ` kk <= (k:num ) `;\r
 807 NHANH (ARITH_RULE` kk <= (k:num) ==> k = kk + k - kk`);\r
 808 STRIP_TAC;\r
 809 UNDISCH_TAC `CARD {(f:num -> A) n | n < k} = k`;\r
 810 FIRST_ASSUM (fun x -> ONCE_REWRITE_TAC[x]);\r
 811  MP_TAC (SPECL [`kk : num `;` f: num -> A `;` k - (kk: num ) `]\r
 812  (GEN_ALL CARD_LT_KT_LE_ADDT));\r
 813 REPEAT STRIP_TAC;\r
 814 UNDISCH_TAC `~(CARD {(f: num -> A) n | n < kk} = kk) `;\r
 815 UNDISCH_TAC ` CARD {(f: num -> A) i | i < kk} <= kk`;\r
 816 PHA;\r
 817 REWRITE_TAC[ARITH_RULE` a <= b /\ ~( a = b ) <=> a < (b: num) `];\r
 818 DOWN THEN DOWN;\r
 819 MESON_TAC[ARITH_RULE` ~( a <= b + c /\ a = kk + c /\ b < (kk: num) ) `];\r
 820 (* SUB 2 *)\r
 821 DISCH_THEN (MP_TAC o (SPEC `k: num `));\r
 822 SIMP_TAC[LE_REFL]]);;\r
 823 \r
 824 \r
 825 \r
 826 \r
 827 \r
 828 \r
 829 let CARD_K_ELMS_EQ_K_IMP_ALL_DISTINCT = \r
 830 prove_by_refinement(\r
 831 `! k (f: num -> A). CARD {f n | n < k} = k \r
 832 ==> (!i j. i < k /\ j < k /\ ~( i = j) ==> ~( f i = f j )) `,\r
 833 [INDUCT_TAC;\r
 834 REWRITE_TAC[LT];\r
 835 ONCE_REWRITE_TAC[CARD_N_FIRST_ELMS_UNDUCTIVE];\r
 836 REWRITE_TAC[ARITH_RULE` SUC k - 1 = k `];\r
 837 FIRST_X_ASSUM NHANH;\r
 838 REWRITE_TAC[ARITH_RULE` a < SUC b <=> a < b \/ a = b `];\r
 839 MESON_TAC[]]);;\r
 840 \r
 841 \r
 842 \r
 843 \r
 844 \r
 845 \r
 846 \r
 847 let CARD_UNION_NOT_DISTJ_LT = \r
 848 prove_by_refinement(\r
 849 ` FINITE (s: A -> bool) /\ FINITE t /\ ~( s INTER t = {} ) ==>\r
 850   CARD (s UNION t) < CARD s + CARD t `,\r
 851 [NGOAC;\r
 852 NHANH CARD_UNION_GEN;\r
 853 REWRITE_TAC[SET_RULE[]` ~( x = {} ) <=> (?a. {a} SUBSET x ) `];\r
 854 NHANH (MESON[FINITE_INTER]` FINITE s /\ FINITE t ==> FINITE (s INTER t)`);\r
 855 STRIP_TAC;\r
 856 UNDISCH_TAC `FINITE ((s: A -> bool) INTER t)`;\r
 857 DOWN THEN PHA;\r
 858 NHANH CARD_SUBSET;\r
 859 REWRITE_TAC[CARD_SINGLETON];\r
 860 STRIP_TAC;\r
 861 UNDISCH_TAC `CARD ((s: A -> bool) UNION t) = \r
 862 (CARD s + CARD t) - CARD (s INTER t)`;\r
 863 ONCE_REWRITE_TAC[ARITH_RULE` a < b <=> 0 < b - a `];\r
 864 ASSUME_TAC2 (SPEC_ALL CARD_UNION_LE);\r
 865 ASSUME_TAC (SET_RULE[]` (s INTER t) SUBSET (s: A -> bool) `);\r
 866 ASSUME_TAC2 (SPECL [`(s:A -> bool) INTER t `;` s: A -> bool`] CARD_SUBSET);\r
 867 DOWN THEN DOWN THEN REMOVE_TAC;\r
 868 DOWN THEN DOWN THEN PHA THEN ARITH_TAC]);;\r
 869 \r
 870 \r
 871 \r
 872 \r
 873 \r
 874 \r
 875 \r
 876 let CARD_ITER_K_EK_IMP_DIST = prove_by_refinement(\r
 877 `! k (f: A -> A). CARD {ITER n f x | n < k} = k ==>\r
 878      (!i j. i < k /\ j < k /\ ~(i = j ) ==> ~(ITER i f x = ITER j f x))`,\r
 879 [REPEAT GEN_TAC;\r
 880 REWRITE_TAC[BETA_RULE (SPECL [`k: num `;\r
 881 `(\n. ITER n (f:A -> A) x ) `] CARD_K_ELMS_EQ_K_IMP_ALL_DISTINCT)]]);;\r
 882 \r
 883 \r
 884 \r
 885 \r
 886 \r
 887 \r
 888 \r
 889 \r
 890 let DIH2K_IMP_PRE_SIMPLE_HYP = prove_by_refinement\r
 891 (`FINITE ( dart H ) /\ \r
 892 dih2k (H:(A)hypermap) k /\ ~( k = 0 ) \r
 893 ==> (! x. x IN dart H ==> ~( node_map H x IN face H (x:A) )) `,\r
 894 [REWRITE_TAC[ dih2k; simple_hypermap];\r
 895 STRIP_TAC;\r
 896 GEN_TAC;\r
 897 ASM_CASES_TAC `node_map H x IN face H (x:A) `;\r
 898 (* subgoal 1 *)\r
 899 FIRST_X_ASSUM NHANH;\r
 900 LET_TAC;\r
 901 STRIP_TAC;\r
 902 SUBGOAL_THEN ` ~( (S: A -> bool) INTER (IMAGE (node_map H) S) = {}) ` ASSUME_TAC;\r
 903 ASSUME_TAC (SPEC_ALL face_refl);\r
 904 DOWN;\r
 905 NHANH (ISPECL [`node_map (H:(A) hypermap)`;`S: A -> bool `;`x:A `] FUN_IN_IMAGE);\r
 906 UNDISCH_TAC `node_map H (x:A) IN S`;\r
 907 ASM_REWRITE_TAC[];\r
 908 SET_TAC[];\r
 909 ASSUME_TAC2 lemma_face_subset;\r
 910 ASSUME_TAC2 (SPECL [`face H (x:A) `;` dart (H:(A) hypermap)`] FINITE_SUBSET);\r
 911 ASSUME_TAC2 (ISPECL [` node_map (H:(A) hypermap) `;`face H (x:A) `] FINITE_IMAGE);\r
 912 REPLICATE_TAC 5 DOWN;\r
 913 PHA THEN ASM_REWRITE_TAC[];\r
 914 STRIP_TAC;\r
 915 ASSUME_TAC2 (SPECL [`S: A -> bool `;` IMAGE (node_map H)\r
 916  (S: A -> bool) `] (GEN_ALL CARD_UNION_NOT_DISTJ_LT));\r
 917 ASSUME_TAC2 (ISPECL [`node_map (H:(A) hypermap)`;` S:A -> bool`] CARD_IMAGE_LE);\r
 918 ASSUME_TAC2 (SPECL [`face_map (H:(A) hypermap)`;`k: num `] \r
 919 (GEN_ALL HAVING_ORDERS_K_IMP_CARD_ORBIT_LE_K));\r
 920 DOWN;\r
 921 ASM_REWRITE_TAC[GSYM face];\r
 922 DISCH_THEN (MP_TAC o (SPEC `x: A`));\r
 923 ASM_REWRITE_TAC[] THEN STRIP_TAC;\r
 924 DOWN THEN DOWN THEN DOWN THEN PHA;\r
 925 NHANH (ARITH_RULE`a < b + c /\ c <= b /\ b <= k ==> a < 2 * k `);\r
 926 FIRST_ASSUM (fun x -> REWRITE_TAC[SYM x]);\r
 927 STRIP_TAC;\r
 928 ASM_MESON_TAC[ARITH_RULE` x = 2 * k ==> ~(x < 2 * k ) `];\r
 929 (* subgoal 2 *)\r
 930 ASM_REWRITE_TAC[]]);;\r
 931 \r
 932 \r
 933 \r
 934 let ITER1 = prove(`ITER 1 f = (f:A -> A) `,\r
 935 REWRITE_TAC[ARITH_RULE` 1 = SUC 0 `; ITER; FUN_EQ_THM]);;\r
 936 \r
 937 \r
 938 \r
 939 \r
 940 \r
 941 \r
 942 let DIH2K_IMP_SIMPLE_HYPERMAP = prove_by_refinement(\r
 943  ` FINITE ( dart H ) /\ \r
 944 dih2k (H:(A)hypermap) k /\ ~( k = 0 ) ==> simple_hypermap H`,\r
 945 [NHANH DIH2K_IMP_PRE_SIMPLE_HYP;\r
 946 REWRITE_TAC[ dih2k; simple_hypermap];\r
 947 STRIP_TAC;\r
 948 GEN_TAC;\r
 949 ASSUME_TAC (ARITH_RULE` ~( 2 = 0 ) `);\r
 950 ASSUME_TAC2 (SPECL [`2`; `node_map (H:(A) hypermap) `] (GEN_ALL HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW));\r
 951 FIRST_X_ASSUM (MP_TAC o (SPEC `x:A `));\r
 952 REWRITE_TAC[GSYM node];\r
 953 REPEAT STRIP_TAC;\r
 954 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SET_RULE[]` (a INTER b) x <=> x IN a /\ x IN b `];\r
 955 REWRITE_TAC[SET_RULE[]` {s} a <=> a = s `];\r
 956 GEN_TAC THEN EQ_TAC;\r
 957 ASM_SIMP_TAC[IN_ELIM_THM; ARITH_RULE` x < 2 <=> x = 0 \/ x = 1 `];\r
 958 STRIP_TAC;\r
 959 (* sub 1.1 *)\r
 960 REPLICATE_TAC 3 DOWN;\r
 961 SIMP_TAC[ITER];\r
 962 (* sub 1.2 *)\r
 963 REPLICATE_TAC 3 DOWN;\r
 964 SIMP_TAC[ITER; ITER1];\r
 965 ASM_MESON_TAC[];\r
 966 (* sub 2 *)\r
 967 SIMP_TAC[X_IN_HYP_ORBITS]]);;\r
 968 \r
 969 \r
 970 \r
 971 \r
 972 \r
 973 let IN_ORBIT_IMP_ORBIT_SUBSET = prove_by_refinement(\r
 974 `! x (y:A) f. x IN orbit_map f y ==> orbit_map f x SUBSET orbit_map f y `,\r
 975 [REPEAT GEN_TAC;\r
 976 REWRITE_TAC[orbit_map; IN_ELIM_THM; SUBSET; POWER_TO_ITER];\r
 977 REPEAT STRIP_TAC;\r
 978 ASM_SIMP_TAC[];\r
 979 REWRITE_TAC[ITER_ADD];\r
 980 EXISTS_TAC `n' + (n:num) `;\r
 981 REWRITE_TAC[ARITH_RULE ` a >= 0 `]]);;\r
 982 \r
 983 \r
 984 \r
 985 \r
 986 \r
 987 \r
 988 let IN_FACE_IMP_SUBSET_FACE = prove(\r
 989 `! (x:A). x IN face H y ==> face H x SUBSET face H y `,\r
 990 REWRITE_TAC[face] THEN \r
 991 NHANH IN_ORBIT_IMP_ORBIT_SUBSET THEN \r
 992 SIMP_TAC[]);;\r
 993 \r
 994 \r
 995 \r
 996 \r
 997 \r
 998 \r
 999 let HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT = prove_by_refinement(\r
1000 ` (f:A -> A) has_orders k /\ x IN orbit_map f y /\ ~( k = 0 ) ==>\r
1001 orbit_map f x = orbit_map f y `,\r
1002 [NHANH IN_ORBIT_IMP_ORBIT_SUBSET;\r
1003 SIMP_TAC[SET_RULE[]` a = b <=> a SUBSET b /\ b SUBSET a `];\r
1004 STRIP_TAC;\r
1005 ASSUME_TAC2 HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW;\r
1006 UNDISCH_TAC `(x:A) IN orbit_map f y`;\r
1007 ASM_REWRITE_TAC[];\r
1008 REWRITE_TAC[SUBSET; IN_ELIM_THM];\r
1009 REPEAT STRIP_TAC;\r
1010 ASM_REWRITE_TAC[ITER_ADD];\r
1011 ASM_CASES_TAC ` (n:num) <= n' `;\r
1012 EXISTS_TAC ` n' - (n:num) `;\r
1013 ASM_SIMP_TAC[ARITH_RULE` n <= (n': num) ==> n' - n + n = n' `];\r
1014 ASM_ARITH_TAC;\r
1015 EXISTS_TAC ` (k: num) - n + n' `;\r
1016 ASM_SIMP_TAC[ARITH_RULE` n < k ==> (k - n + n') + n = n' + (k:num) `];\r
1017 UNDISCH_TAC `(f: A -> A) has_orders k `;\r
1018 SIMP_TAC[has_orders; GSYM ITER_ADD; I_THM];\r
1019 REMOVE_TAC THEN ASM_ARITH_TAC]);;\r
1020 \r
1021 \r
1022 \r
1023 \r
1024 \r
1025 \r
1026 \r
1027 \r
1028 \r
1029 \r
1030 let LOCAL_FAN_IMP_FF_SUBSET_DARTS = prove_by_refinement(\r
1031 ` local_fan ((V:real^3 -> bool),E,FF) ==> FF SUBSET darts_of_hyp E V`,\r
1032 [REWRITE_TAC[local_fan];\r
1033 LET_TAC;\r
1034 STRIP_TAC;\r
1035 DOWN_TAC;\r
1036 NHANH lemma_face_subset;\r
1037 STRIP_TAC;\r
1038 UNDISCH_TAC ` face H (x:real^3#real^3) SUBSET dart H`;\r
1039 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` HYP_LEMMA);\r
1040 REWRITE_TAC[dart];\r
1041 EXPAND_TAC "H";\r
1042 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);\r
1043 ASM_REWRITE_TAC[HYP]]);;\r
1044 \r
1045 \r
1046 \r
1047 \r
1048 \r
1049 \r
1050 let LOCAL_IMP_FINITE_DARTS = prove_by_refinement(\r
1051 ` local_fan ((V:real^3 -> bool),E,FF) ==> FINITE (darts_of_hyp E V) `,\r
1052 [REWRITE_TAC[local_fan] THEN LET_TAC;\r
1053 EXPAND_TAC "H";\r
1054 NHANH HYP_LEMMA;\r
1055 REWRITE_TAC[dart];\r
1056 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
1057 SIMP_TAC[]]);;\r
1058 \r
1059 \r
1060 \r
1061 \r
1062 let LOCAL_FAN_FINITE_FF = prove_by_refinement(\r
1063 ` local_fan ((V:real^3 -> bool),E,FF) ==> FINITE FF `,\r
1064 [NHANH LOCAL_FAN_IMP_FF_SUBSET_DARTS;\r
1065 NHANH LOCAL_IMP_FINITE_DARTS;\r
1066 PHA THEN IMP_TAC THEN REMOVE_TAC;\r
1067 REWRITE_TAC[FINITE_SUBSET]]);;\r
1068 \r
1069 \r
1070 \r
1071 \r
1072 \r
1073 \r
1074 \r
1075 \r
1076 \r
1077 let DIH_IMP_EVERY_NODE_INTER_FACE = prove_by_refinement\r
1078 (` dih2k (H:(A) hypermap) k \r
1079 ==> (! x y. {x,y} SUBSET dart H ==> ? d. d IN node H x /\ d IN face H y ) `,\r
1080 [REWRITE_TAC[dih2k; INSERT_SUBSET];\r
1081 REPEAT STRIP_TAC;\r
1082 UNDISCH_TAC `(y:A) IN dart H `;\r
1083 FIRST_X_ASSUM NHANH;\r
1084 REWRITE_TAC[let_CONV` let S = face H (y:A) in dart H = S UNION IMAGE (node_map H) S`];\r
1085 STRIP_TAC;\r
1086 UNDISCH_TAC `(x:A) IN dart H`;\r
1087 ASM_REWRITE_TAC[IN_UNION];\r
1088 STRIP_TAC;\r
1089 EXISTS_TAC `x:A`;\r
1090 ASM_SIMP_TAC[node_refl];\r
1091 DOWN;\r
1092 REWRITE_TAC[IN_IMAGE];\r
1093 STRIP_TAC;\r
1094 EXISTS_TAC `x':A`;\r
1095 ASM_REWRITE_TAC[node; orbit_map; IN_ELIM_THM];\r
1096 EXISTS_TAC `1 `;\r
1097 REWRITE_TAC[ARITH_RULE` 1 >= 0 `; POWER_1];\r
1098 REWRITE_TAC[ARITH_RULE` 1 >= 0 `; POWER_1];\r
1099 UNDISCH_TAC `node_map (H:(A) hypermap ) has_orders 2`;\r
1100 REWRITE_TAC[has_orders; FUN_EQ_THM; ITER; ARITH_RULE`2 = SUC 1 `; ITER1; I_THM];\r
1101 SIMP_TAC[EQ_SYM_EQ]]);;\r
1102 \r
1103 \r
1104 \r
1105 \r
1106 \r
1107 \r
1108 \r
1109 \r
1110 \r
1111 \r
1112 let LOCAL_FAN_IMP_BIJ_FF_NODES = prove_by_refinement(\r
1113 `local_fan ((V:real^3 -> bool),E,FF) /\\r
1114    f = (\y. node (hypermap (HYP (vec 0,V,E))) y ) ==> \r
1115 BIJ f FF {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V} `,\r
1116 [REWRITE_TAC[local_fan];\r
1117 LET_TAC;\r
1118 REWRITE_TAC[dih2k];\r
1119 STRIP_TAC;\r
1120 ASM_REWRITE_TAC[BIJ; INJ; SURJ];\r
1121 PHA;\r
1122 CONJ_TAC;\r
1123 (* SUB 1 *)\r
1124 GEN_TAC;\r
1125 ASSUME_TAC2 (ISPEC `(vec 0): real^3 ` HYP_LEMMA);\r
1126 DOWN;\r
1127 REWRITE_TAC[GSYM hypermap_tybij; HYP];\r
1128 ASSUME_TAC2 (ISPECL [`H: (real^3 # real^3)hypermap `;\r
1129 `x:real^3 # real^3 `] lemma_face_subset);\r
1130 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
1131 PHA THEN STRIP_TAC;\r
1132 UNDISCH_TAC `face H (x:real^3 # real^3) SUBSET dart H`;\r
1133 DOWN;\r
1134 DOWN_TAC THEN STRIP_TAC;\r
1135 EXPAND_TAC "H";\r
1136 USE_FIRST `dart (hypermap (HYP (vec 0,V,E))) = darts_of_hyp E (V:real^3 -> bool) `\r
1137   ( fun x -> REWRITE_TAC[GSYM x]);\r
1138 REPLICATE_TAC 3 DOWN;\r
1139 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1140 ASM_REWRITE_TAC[IN_ELIM_THM; SUBSET];\r
1141 MESON_TAC[];\r
1142 (* SUB 2.1 *)\r
1143 CONJ_TAC;\r
1144 (* sub 2.1.1 *)\r
1145 REPEAT STRIP_TAC;\r
1146 MP_TAC LOCAL_FAN_FINITE_FF;\r
1147 ANTS_TAC THENL [\r
1148 REWRITE_TAC[local_fan; dih2k] THEN \r
1149 LET_TAC THEN ASM_SIMP_TAC[] THEN \r
1150 ASM_MESON_TAC[];\r
1151 ASM_CASES_TAC ` CARD (FF:real^3 # real^3 -> bool) = 0`];\r
1152 (* sub I *)\r
1153 DOWN THEN PHA;\r
1154 NHANH (MESON[CARD_EQ_0]` CARD FF = 0 /\ FINITE FF ==> FF = {} `);\r
1155 STRIP_TAC;\r
1156 MP_TAC (ISPECL [`H: (real^3#real^3) hypermap `;` x: real^3 # real^3 `] face_refl);\r
1157 DOWN;\r
1158 ASM_SIMP_TAC[NOT_IN_EMPTY];\r
1159 (* SUB II *)\r
1160 MP_TAC (ISPECL [` CARD (FF: (real^3 # real^3 ) -> bool) `;` y: real^3 # real^3 `;\r
1161   `face_map (H:(real^3 # real^3) hypermap) `;` x: real^3 # real^3 `] \r
1162 (GEN_ALL HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT));\r
1163 ANTS_TAC THENL [\r
1164 ASM_REWRITE_TAC[GSYM face];\r
1165 REWRITE_TAC[GSYM face]];\r
1166 DISCH_TAC;\r
1167 MP_TAC (ISPECL [` CARD (FF: (real^3 # real^3 ) -> bool) `;` x': real^3 # real^3 `;\r
1168   `face_map (H:(real^3 # real^3) hypermap) `;` x: real^3 # real^3 `] \r
1169 (GEN_ALL HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT));\r
1170 ANTS_TAC THENL [\r
1171 ASM_REWRITE_TAC[GSYM face];\r
1172 ASM_REWRITE_TAC[GSYM face]];\r
1173 REPEAT STRIP_TAC;\r
1174 MP_TAC (ISPECL [`CARD (FF: real^3 # real^3 -> bool) `;\r
1175 ` H: (real^3 # real^3) hypermap `] (GEN_ALL DIH2K_IMP_SIMPLE_HYPERMAP));\r
1176 ANTS_TAC;\r
1177 (* SUB GOAL *)\r
1178 \r
1179 \r
1180 ASM_SIMP_TAC[dih2k];\r
1181 EXPAND_TAC "H";\r
1182 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^ 3 ` ELMS_OF_HYPERMAP_HYP));\r
1183 MP_TAC (REWRITE_RULE[local_fan] LOCAL_IMP_FINITE_DARTS);\r
1184 ANTS_TAC THENL [\r
1185 LET_TAC THEN \r
1186 REWRITE_TAC[dih2k] THEN \r
1187 ASM_MESON_TAC[];\r
1188 ASM_REWRITE_TAC[]];\r
1189 \r
1190 (* =============== *)\r
1191 (* SUB             *)\r
1192 NHANH lemma_simple_hypermap;\r
1193 STRIP_TAC;\r
1194 FIRST_ASSUM (MP_TAC o (SPEC `y: real^3 # real^3 `));\r
1195 UNDISCH_TAC `node H x' = node H (y: real^3 # real^3 ) `;\r
1196 DISCH_THEN (fun x -> REWRITE_TAC[SYM x]);\r
1197 ASM_REWRITE_TAC[];\r
1198 UNDISCH_TAC `face H x' = face H (x: real^3 # real^3 ) `;\r
1199 DISCH_THEN (fun x -> REWRITE_TAC[SYM x]);\r
1200 ASM_REWRITE_TAC[];\r
1201 SET_TAC[];\r
1202 \r
1203 \r
1204 (* ---------------------------------- *)\r
1205 ASSUME_TAC2 (SPEC `(vec 0): real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
1206 DOWN;\r
1207 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1208 ASM_SIMP_TAC[];\r
1209 STRIP_TAC;\r
1210 ASSUME_TAC2 (ISPEC `H:(real^3 # real^3 ) hypermap ` lemma_face_subset);\r
1211 CONJ_TAC;\r
1212 STRIP_TAC THEN DOWN THEN PHA;\r
1213 SET_TAC[];\r
1214 REWRITE_TAC[IN_ELIM_THM];\r
1215 REPEAT STRIP_TAC;\r
1216 MP_TAC (ISPECL [`CARD (FF: real^3#real^3->bool) `;` H : (real^3#real^3)hypermap`]\r
1217   ( GEN_ALL DIH_IMP_EVERY_NODE_INTER_FACE));\r
1218 ANTS_TAC THENL [\r
1219 REWRITE_TAC[dih2k] THEN \r
1220 ASM_SIMP_TAC[];\r
1221 DISCH_THEN (MP_TAC o (SPECL [`y:real^3 # real^3 `;`x:real^3# real^3`]))];\r
1222 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];\r
1223 DISCH_THEN ASSUME_TAC2;\r
1224 FIRST_X_ASSUM CHOOSE_TAC;\r
1225 EXISTS_TAC `d: real^3 # real^3 `;\r
1226 FIRST_X_ASSUM MP_TAC THEN NHANH lemma_node_identity;\r
1227 ASM_SIMP_TAC[]]);;\r
1228 \r
1229 \r
1230 \r
1231 \r
1232 \r
1233 (*  local_fan (V,E,FF) /\ f = (\y. node (hypermap (HYP (vec 0,V,E))) y)\r
1234      ==> BIJ f FF\r
1235          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}\r
1236 *)\r
1237 \r
1238 REWRITE_RULE[MESON[]` (! h. a /\ h = f ==> BIJ h S C ) <=> ( a ==> BIJ f S C ) `]\r
1239   (GEN `f: real^3#real^3->real^3#real^3->bool ` LOCAL_FAN_IMP_BIJ_FF_NODES);;\r
1240 \r
1241 \r
1242 (*\r
1243 val it : thm =\r
1244   |- local_fan (V,E,FF)\r
1245      ==> BIJ (\y. node (hypermap (HYP (vec 0,V,E))) y) FF\r
1246          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}\r
1247 \r
1248 *)\r
1249 \r
1250 REWRITE_RULE[MESON[]` (! h. a /\ h = f ==> BIJ h S C ) <=> ( a ==> BIJ f S C ) `]\r
1251   (GEN `f: real^3->real^3#real^3->bool` FAN_IMP_BIJ_V_NODE_OF_HYP);;\r
1252 \r
1253 FAN_IMP_BIJ_V_NODE_OF_HYP ;;\r
1254 (*   val it : thm =\r
1255   |- FAN (x,V,E) /\\r
1256      f =\r
1257      (\u. if u IN V\r
1258           then node (hypermap (HYP (x,V,E))) (u,choose_nd_point u E V)\r
1259           else {})\r
1260      ==> BIJ f V\r
1261          {node (hypermap (HYP (x,V,E))) y | y | y IN darts_of_hyp E V}\r
1262 \r
1263 *)\r
1264 \r
1265 \r
1266 \r
1267 \r
1268 let F_INVERSE_F = prove(` (? y. f y = x ) ==> f ( (inverse f) x ) = x`,\r
1269 REWRITE_TAC[FUN_EQ_THM; I_THM; o_THM; inverse; IN_IMAGE]\r
1270 THEN ASM_MESON_TAC[]);;\r
1271 \r
1272 let F_INVERSE_F_F = MESON[F_INVERSE_F]` f ( inverse f (f x)) = f x `;;\r
1273 \r
1274 let INJ_IMP_INVERSE_FF = MESON[F_INVERSE_F_F]`(!y. f y = f x ==> y = x ) ==> inverse f ( f x ) = x `;;\r
1275 \r
1276 let BIJ_AND_BIJ_INVERSE = prove(` BIJ f S1 S2 /\ (! x. f x IN S2 ==> x IN S1 )\r
1277 ==> BIJ (inverse f) S2 S1 `,\r
1278 REWRITE_TAC[BIJ; INJ; SURJ] THEN \r
1279 ASM_MESON_TAC[F_INVERSE_F ]);;\r
1280 \r
1281 \r
1282 \r
1283 \r
1284 \r
1285 \r
1286 \r
1287 \r
1288 let INVERSE_FUNCTION_OF_BIJ = prove_by_refinement(\r
1289 `BIJ (f:A -> B) S1 S2 /\ g = (\x. if x IN S2 then (@t. t IN S1 /\ f t = x ) else tt )\r
1290 ==> BIJ g S2 S1 `,\r
1291 [REWRITE_TAC[BIJ; INJ; SURJ];\r
1292 STRIP_TAC;\r
1293 SUBGOAL_THEN `(!x. (x:B) IN S2 ==> g x IN (S1: A -> bool) /\ f ( g x ) = x )` ASSUME_TAC;\r
1294 ASM_REWRITE_TAC[];\r
1295 FIRST_X_ASSUM NHANH;\r
1296 SIMP_TAC[];\r
1297 MESON_TAC[];\r
1298 (* ================= *)\r
1299 CONJ_TAC;\r
1300 ASM_MESON_TAC[];\r
1301 CONJ_TAC;\r
1302 FIRST_X_ASSUM NHANH;\r
1303 SIMP_TAC[];\r
1304 REPEAT STRIP_TAC;\r
1305 EXISTS_TAC `(f:A -> B) x `;\r
1306 ASM_MESON_TAC[]]);;\r
1307 \r
1308 \r
1309 \r
1310 \r
1311 \r
1312 let TOW_BIJS_IMP_BIJ_BETWEEN_FIRST = prove_by_refinement(\r
1313 ` BIJ (f:B -> A ) S1 V /\ BIJ (g:C -> A) S2 V /\\r
1314 ff = (\x. if x IN S1 then (@a. a IN S2 /\ f x = g a) else aa) \r
1315 ==> BIJ ff S1 S2 `,\r
1316 [REWRITE_TAC[BIJ; INJ; SURJ];\r
1317 STRIP_TAC;\r
1318 SUBGOAL_THEN ` (!x. (x:B) IN S1 ==> ff x IN (S2: C -> bool) /\ (f:B -> A) x = g ( ff x )) ` ASSUME_TAC;\r
1319 ASM_REWRITE_TAC[];\r
1320 SIMP_TAC[];\r
1321 ASM_MESON_TAC[];\r
1322 ASM_MESON_TAC[]]);;\r
1323 \r
1324 \r
1325 \r
1326 \r
1327 \r
1328 \r
1329 \r
1330 let INDENT_IN_S1_IMP_BIJ = \r
1331 prove(` BIJ (f: A -> B) S1 S2 /\ (! x. x IN S1 ==> f x = g x )\r
1332 ==> BIJ g S1 S2 `,\r
1333 REWRITE_TAC[BIJ; INJ; SURJ] THEN \r
1334 MESON_TAC[]);;\r
1335 \r
1336 \r
1337 \r
1338 \r
1339 \r
1340 \r
1341 let IN_NODE_IMP_FIRST_EQ = prove_by_refinement(\r
1342 ` FAN (x,V,E) /\ a IN ( node (hypermap (HYP (x,V,E))) b )\r
1343   ==> FST a = FST b `,\r
1344 [REWRITE_TAC[node];\r
1345 NHANH ELMS_OF_HYPERMAP_HYP;\r
1346 IMP_TAC;\r
1347 SIMP_TAC[];\r
1348 STRIP_TAC;\r
1349 REWRITE_TAC[IN_ELIM_THM; orbit_map];\r
1350 STRIP_TAC;\r
1351 DOWN;\r
1352 PAT_ONCE_REWRITE_TAC `\x. a = P x ==> y ` [GSYM PAIR];\r
1353 REWRITE_TAC[N_HYP_TO_AZIM_CYCLE_LEM];\r
1354 PAT_ONCE_REWRITE_TAC `\x. x = a ==> y ` [GSYM PAIR];\r
1355 REWRITE_TAC[PAIR_EQ];\r
1356 SIMP_TAC[]]);;\r
1357 \r
1358 \r
1359 \r
1360 let LOCAL_FAN_IMP_FAN = prove(` local_fan (V,E,FF) ==> FAN ( vec 0, V,E) `,\r
1361 REWRITE_TAC[local_fan] THEN \r
1362 LET_TAC THEN SIMP_TAC[]);;\r
1363 \r
1364 \r
1365 \r
1366 \r
1367 \r
1368 \r
1369 let BIJ_BETWEEN_FF_AND_V = prove_by_refinement(\r
1370 `local_fan (V,E,FF) /\ k = (\x. FST x )\r
1371 ==> BIJ k FF V `,\r
1372 [ABBREV_TAC ` f =\r
1373      (\u. if (u:real^3) IN V\r
1374           then node (hypermap (HYP (vec 0,V,E))) (u,choose_nd_point u E V)\r
1375           else {}) `;\r
1376 ABBREV_TAC `h = (\y. node (hypermap (HYP (vec 0,V,E))) y) ` ;\r
1377 DOWN_TAC;\r
1378 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1379 STRIP_TAC;\r
1380 ASSUME_TAC2 (\r
1381 prove(` local_fan (V,E,FF) /\\r
1382      f =\r
1383      (\u. if (u:real^3) IN V\r
1384           then node (hypermap (HYP (vec 0,V,E))) (u,choose_nd_point u E V)\r
1385           else {}) /\\r
1386  h = (\y. node (hypermap (HYP (vec 0,V,E))) y)\r
1387      ==> BIJ h FF\r
1388          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V} /\\r
1389    BIJ f V\r
1390          {node (hypermap (HYP (vec 0,V,E))) y | y | y IN darts_of_hyp E V}`,\r
1391 SIMP_TAC[FAN_IMP_BIJ_V_NODE_OF_HYP ; LOCAL_FAN_IMP_BIJ_FF_NODES] THEN \r
1392 REWRITE_TAC[local_fan] THEN LET_TAC THEN \r
1393 EXPAND_TAC "H" THEN \r
1394 SIMP_TAC[FAN_IMP_BIJ_V_NODE_OF_HYP]));\r
1395 DOWN;\r
1396 NHANH (REWRITE_RULE[RIGHT_FORALL_IMP_THM]\r
1397   (GEN `ff: B -> C ` (REWRITE_RULE[TAUT` a/\b/\c ==> d <=>\r
1398  a /\ b ==> c ==> d `] TOW_BIJS_IMP_BIJ_BETWEEN_FIRST)));\r
1399 REWRITE_TAC[MESON[]` (! x. x = a ==> P x ) <=> P a `];\r
1400 ABBREV_TAC ` ff = (\x. if x IN FF then @a. a IN V /\ \r
1401 (h:real^3#real^3->real^3#real^3->bool) x = f (a:real^3) else aa) `;\r
1402 STRIP_TAC;\r
1403 SUBGOAL_THEN `(!x. x IN FF ==> (ff: real^3#real^3->real^3)\r
1404  x = k x ) ` ASSUME_TAC;\r
1405 SUBGOAL_THEN ` (! x. (x:real^3 # real^3) IN FF ==> ff x IN (V:real^3 -> bool) /\\r
1406   (h:real^3#real^3->real^3#real^3->bool) x = f ( ff x )) ` ASSUME_TAC;\r
1407 \r
1408 (* SUBGOAL 1 *)\r
1409 EXPAND_TAC "ff";\r
1410 SIMP_TAC[];\r
1411 STRIP_TAC THEN STRIP_TAC;\r
1412 CONV_TAC SELECT_CONV;\r
1413 DOWN_TAC;\r
1414 REWRITE_TAC[BIJ; INJ; SURJ];\r
1415 MESON_TAC[];\r
1416 (* end 1 *)\r
1417 \r
1418 (* sub 2 *)\r
1419 FIRST_X_ASSUM NHANH;\r
1420 STRIP_TAC;\r
1421 STRIP_TAC;\r
1422 DOWN;\r
1423 ASM_REWRITE_TAC[];\r
1424 STRIP_TAC;\r
1425 MP_TAC (ISPECL [` hypermap (HYP (vec 0,V,E)) `;` x: real^3 # real^3 `] node_refl);\r
1426 ASM_REWRITE_TAC[];\r
1427 ASSUME_TAC2 LOCAL_FAN_IMP_FAN;\r
1428 DOWN THEN PHA;\r
1429 NHANH IN_NODE_IMP_FIRST_EQ;\r
1430 EXPAND_TAC "k";\r
1431 SIMP_TAC[EQ_SYM_EQ];\r
1432 (* subgoal -------------------------- *)\r
1433 (* oooooooooooooooooooooooooooooooooo *)\r
1434 \r
1435 DOWN THEN DOWN;\r
1436 PHA;\r
1437 REWRITE_TAC[INDENT_IN_S1_IMP_BIJ ]]);;\r
1438 \r
1439 \r
1440 \r
1441 \r
1442 \r
1443 \r
1444 let IN_ORBIT_MAP_IMP_F_Y = prove(` (y:A) IN orbit_map f x ==> f y IN orbit_map f x `,\r
1445 REWRITE_TAC[orbit_map; IN_ELIM_THM] THEN \r
1446 STRIP_TAC THEN \r
1447 EXISTS_TAC ` n + 1 ` THEN \r
1448 ASM_REWRITE_TAC[ARITH_RULE ` a >= 0 /\ \r
1449 n + 1 = SUC n`; COM_POWER; I_THM; o_THM]);;\r
1450 \r
1451 \r
1452 \r
1453 \r
1454 \r
1455 \r
1456 \r
1457 \r
1458 \r
1459 \r
1460 \r
1461 \r
1462 let SURJ_IMP_S2_EQ_IMAGE_S1 = prove(` SURJ (f:A ->B) S1 S2 ==> IMAGE f S1 = S2 `,\r
1463 REWRITE_TAC[IMAGE; SURJ] THEN SET_TAC[]);;\r
1464 \r
1465 \r
1466 \r
1467 \r
1468 \r
1469 \r
1470 \r
1471 let WRGCVDR = prove_by_refinement(\r
1472 `local_fan (V,E,FF) /\ k = (\x. FST x)\r
1473  ==> BIJ k FF V /\\r
1474      ((!x. x IN V ==> x,hro x IN FF) /\\r
1475       (!x. x IN FF ==> x = FST x,hro (FST x))\r
1476       ==> (!x. x IN V ==> V = orbit_map hro x))`,\r
1477 [STRIP_TAC;\r
1478 ASSUME_TAC2 BIJ_BETWEEN_FF_AND_V;\r
1479 ASM_REWRITE_TAC[];\r
1480 REPEAT STRIP_TAC;\r
1481 DOWN_TAC;\r
1482 REWRITE_TAC[local_fan; dih2k];\r
1483 LET_TAC;\r
1484 STRIP_TAC;\r
1485 SUBGOAL_THEN ` (x:real^3), (hro:real^3 -> real^3) x IN FF ` ASSUME_TAC;\r
1486 FIRST_X_ASSUM MATCH_MP_TAC;\r
1487 ASM_SIMP_TAC[];\r
1488 DOWN;\r
1489 UNDISCH_TAC ` FF = face H (x':real^3 # real^3 ) `;\r
1490 SIMP_TAC[] THEN STRIP_TAC;\r
1491 NHANH lemma_face_identity;\r
1492 DOWN_TAC THEN REWRITE_TAC[BIJ];\r
1493 NHANH (prove(` SURJ (f:A ->B) S1 S2 ==> IMAGE f S1 = S2 `,\r
1494 REWRITE_TAC[IMAGE; SURJ] THEN SET_TAC[]));\r
1495 STRIP_TAC;\r
1496 EXPAND_TAC "V";\r
1497 REPLICATE_TAC 3 DOWN THEN PHA;\r
1498 SIMP_TAC[];\r
1499 STRIP_TAC;\r
1500 REWRITE_TAC[face; IMAGE; orbit_map; IN_ELIM_THM];\r
1501 SUBGOAL_THEN ` (! n. (face_map H POWER n) (x,(hro:real^3 -> real^3 ) x) = \r
1502 ((hro POWER n) x, (hro POWER ( n + 1 )) x )) `  ASSUME_TAC;\r
1503 INDUCT_TAC;\r
1504 REWRITE_TAC[POWER; I_THM; ARITH_RULE` 0 + 1 = 1`; POWER_1];\r
1505 ASM_REWRITE_TAC[COM_POWER; o_THM];\r
1506 DOWN THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1507 NHANH in_orbit_lemma;\r
1508 ASSUME_TAC2 (SPEC `(vec 0):real^3 ` (GEN `x:real^3 ` ELMS_OF_HYPERMAP_HYP));\r
1509 DOWN;\r
1510 ASM_SIMP_TAC[FUN_EQ_THM];\r
1511 STRIP_TAC;\r
1512 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1513 STRIP_TAC;\r
1514 SUBGOAL_THEN `f_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
1515   ASSUME_TAC;\r
1516 ASM_SIMP_TAC[];\r
1517 DOWN;\r
1518 NHANH IN_ORBIT_MAP_IMP_F_Y;\r
1519 REWRITE_TAC[GSYM face];\r
1520 ASM_SIMP_TAC[];\r
1521 (* gggggggggggggggggggg *)\r
1522 DOWN;\r
1523 ASM_REWRITE_TAC[f_of_hyp];\r
1524 DOWN_TAC;\r
1525 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1526 STRIP_TAC;\r
1527 DOWN;\r
1528 UNDISCH_TAC `face H (x,(hro: real^3 -> real^3) x) = face H x' `;\r
1529 SIMP_TAC[];\r
1530 DISCH_TAC;\r
1531 UNDISCH_TAC `face H (x':real^3 # real^3 ) = FF`;\r
1532 SIMP_TAC[];\r
1533 FIRST_ASSUM NHANH;\r
1534 REWRITE_TAC[PAIR_EQ];\r
1535 SIMP_TAC[GSYM ADD1; COM_POWER; o_THM];\r
1536 (* iiiiiiiiiiiiiiiiiiiiiiii *)\r
1537 REWRITE_TAC[FUN_EQ_THM];\r
1538 GEN_TAC THEN EQ_TAC;\r
1539 REWRITE_TAC[IN_ELIM_THM];\r
1540 STRIP_TAC;\r
1541 DOWN;\r
1542 ASM_SIMP_TAC[];\r
1543 STRIP_TAC;\r
1544 EXISTS_TAC `n: num `;\r
1545 ASM_SIMP_TAC[];\r
1546 (* ::::::::::::::::::: *)\r
1547 REWRITE_TAC[IN_ELIM_THM];\r
1548 STRIP_TAC;\r
1549 EXISTS_TAC `(hro POWER n) (x: real^3 ), (hro POWER (n + 1)) x `;\r
1550 ASM_REWRITE_TAC[];\r
1551 EXISTS_TAC `n:num `;\r
1552 ASM_REWRITE_TAC[]]);;\r
1553 \r
1554 \r
1555 \r
1556 \r
1557 \r
1558 \r
1559 let SET_TAC =\r
1560 let basicthms =\r
1561 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
1562 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
1563 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
1564 [IN_ELIM_THM; IN] in\r
1565 let PRESET_TAC =\r
1566 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
1567 REPEAT COND_CASES_TAC THEN\r
1568 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
1569 REWRITE_TAC allthms in\r
1570 fun ths ->\r
1571 PRESET_TAC THEN\r
1572 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
1573 MESON_TAC[];;\r
1574 \r
1575 let SET_RULE tm = prove(tm,SET_TAC[]);; \r
1576 \r
1577 \r
1578 (* ====================================== *)\r
1579 \r
1580 (* ============ MFMPCVM ================  *)\r
1581 \r
1582 (* =====================================  *)\r
1583 let rho_fan = new_specification ["rho_fan"]\r
1584 (MATCH_MP \r
1585 (MESON[]`(! a b c d e. P a b c d e) ==> ? e. ! a b c d. P a b c d e `)\r
1586 (GEN_ALL WRGCVDR));;\r
1587 \r
1588 rho_fan;;\r
1589 (* ================================= *)\r
1590 (*              PJRIMCV              *)\r
1591 (* ================================= *)\r
1592 let interior_angle = new_definition \r
1593 ` interior_angle v E = azim_in_fan (v, rho_fan v) E `;;\r
1594 \r
1595 \r
1596 let wedge_fan_gt = new_definition\r
1597 ` wedge_fan_gt v E = wedge_in_fan_gt (v, rho_fan v) E `;;\r
1598 \r
1599 \r
1600 let wedge_fan_ge = new_definition\r
1601 `wedge_fan_ge v E = wedge_in_fan_ge (v, rho_fan v) E`;;\r
1602 \r
1603 \r
1604 \r
1605 (* ============================= *)\r
1606 (*          localization         *)\r
1607 (*            BIFQATK            *)\r
1608 (* ============================= *)\r
1609 \r
1610 let v_prime = new_definition `v_prime V FF = {v| v IN V /\\r
1611  (?w. (v,w) IN FF )} `;;\r
1612 \r
1613 let e_prime = new_definition ` e_prime E FF = {{v,w} | {v,w} IN E /\ \r
1614 (v,w) IN FF } `;;\r
1615 \r
1616 \r
1617 let IMP_FAN_V_PRIME_E_PRIME = prove_by_refinement\r
1618 (`FAN (v, V, E) /\ (?x. x IN dart (hypermap (HYP (v,V,E))) /\\r
1619 FF = face ( hypermap (HYP (v, V, E))) x)\r
1620 ==> FAN (v, v_prime V FF , e_prime E FF ) `,\r
1621 [REWRITE_TAC[FAN; v_prime; e_prime];\r
1622 STRIP_TAC;\r
1623 CONJ_TAC;\r
1624 REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM];\r
1625 REPEAT STRIP_TAC;\r
1626 DOWN THEN SIMP_TAC[];\r
1627 DOWN;\r
1628 MP_TAC (SPEC `v: real^3 ` (GEN `x: real^3 ` ELMS_OF_HYPERMAP_HYP));\r
1629 ANTS_TAC THENL [\r
1630 ASM_REWRITE_TAC[FAN];\r
1631 DOWN THEN DOWN];\r
1632 REWRITE_TAC[face];\r
1633 SIMP_TAC[];\r
1634 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC;\r
1635 NHANH_PAT `\x. x ==> y ` IN_ORBIT_MAP_IMP_F_Y;\r
1636 REWRITE_TAC[f_of_hyp];\r
1637 UNDISCH_TAC ` {v', (w:real^3) } IN E `;\r
1638 UNDISCH_TAC ` UNIONS E SUBSET (V: real^3 -> bool) `;\r
1639 REWRITE_TAC[UNIONS_SUBSET];\r
1640 DISCH_THEN NHANH;\r
1641 SET_TAC[];\r
1642 \r
1643 \r
1644 \r
1645 UNDISCH_TAC ` graph (E:(real^3 -> bool) -> bool) `;\r
1646 REWRITE_TAC[graph];\r
1647 DISCH_TAC;\r
1648 CONJ_TAC;\r
1649 DOWN THEN SET_TAC[];\r
1650 \r
1651 REWRITE_TAC[fan1; fan2; fan6; fan7];\r
1652 \r
1653 \r
1654 CONJ_TAC;\r
1655 DOWN_TAC;\r
1656 REWRITE_TAC[fan1];\r
1657 STRIP_TAC;\r
1658 CONJ_TAC;\r
1659 UNDISCH_TAC `FINITE (V:real^3 -> bool) `;\r
1660 MATCH_MP_TAC (REWRITE_RULE[TAUT` a /\ b ==> c <=> \r
1661 b ==> a ==> c `] FINITE_SUBSET);\r
1662 SET_TAC[];\r
1663 \r
1664 \r
1665 DOWN THEN DOWN;\r
1666 NHANH (MESON[face_refl]` FF = face H x ==> x IN FF `);\r
1667 REPEAT STRIP_TAC;\r
1668 MP_TAC (SPEC `v:real^3 ` (GEN `x:real^3 ` ELMS_OF_HYPERMAP_HYP));\r
1669 ANTS_TAC THENL [\r
1670 ASM_REWRITE_TAC[FAN; graph; fan1];\r
1671 STRIP_TAC];\r
1672 UNDISCH_TAC `x IN dart (hypermap (HYP (v,V,E)))`;\r
1673 ASM_REWRITE_TAC[];\r
1674 STRIP_TAC;\r
1675 ASSUME_TAC2 (\r
1676 ISPEC `x:real^3#real^3 ` (GEN `y:A#A ` IN_DARTS_HYP_IMP_FST_SND_IN_V));\r
1677 UNDISCH_TAC `(x:real^3 # real^3 ) IN FF `;\r
1678 REWRITE_TAC[];\r
1679 ONCE_REWRITE_TAC[GSYM PAIR];\r
1680 ABBREV_TAC ` fx = FST (x:real^3 # real^3) `;\r
1681 ASM SET_TAC[];\r
1682 (* ---------------------------------------------------------------- *)\r
1683 \r
1684 \r
1685 \r
1686 DOWN_TAC THEN REWRITE_TAC[fan1; fan2];\r
1687 STRIP_TAC;\r
1688 CONJ_TAC;\r
1689 ASM SET_TAC[];\r
1690 \r
1691 DOWN_TAC THEN REWRITE_TAC[fan6; fan7];\r
1692 SET_TAC[]]);;\r
1693 \r
1694 let E_PRIME_SUBSET_E = prove(` e_prime E FF SUBSET E `,\r
1695 REWRITE_TAC[e_prime; SUBSET; IN_ELIM_THM] THEN \r
1696 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;\r
1697 \r
1698 let SUBSET_IMP_SO_DO_EE =\r
1699 prove(` W1 SUBSET W2 ==> EE v W1 SUBSET EE v W2 `,\r
1700 REWRITE_TAC[EE] THEN SET_TAC[]);;\r
1701 \r
1702 \r
1703 \r
1704 \r
1705 let FST_SND_X_IN_EE_E_PRIME =prove(` \r
1706 (x:A #A) IN FF /\ {FST x, SND x} IN E \r
1707 ==> FST x IN EE (SND x) (e_prime E FF ) /\\r
1708 SND x IN EE (FST x) (e_prime E FF) `,\r
1709 PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [GSYM PAIR] THEN \r
1710 ABBREV_TAC ` ax = FST (x:A#A) ` THEN \r
1711 REWRITE_TAC[EE; IN_ELIM_THM; e_prime] THEN \r
1712 STRIP_TAC THEN \r
1713 CONJ_TAC THENL [\r
1714 EXISTS_TAC `ax: A ` THEN \r
1715 EXISTS_TAC `SND (x:A#A) ` THEN \r
1716 ASM_SIMP_TAC[INSERT_COMM] ;\r
1717 EXISTS_TAC `ax:A` THEN \r
1718 EXISTS_TAC `SND (x:A#A) ` THEN \r
1719 ASM_REWRITE_TAC[]]);;\r
1720 \r
1721 \r
1722 \r
1723 \r
1724 let W_SUBSET_SINGLETON_IMP_IDE =\r
1725 prove(` W SUBSET {p} ==> azim_cycle W v w p = p `,\r
1726 SIMP_TAC[azim_cycle]);;\r
1727 \r
1728 \r
1729 \r
1730 \r
1731 let CYCLIC_MAP_IMP_CIRCLE_ITSELF =\r
1732 prove_by_refinement(`\r
1733 (!(x:A). x IN W ==> W = orbit_map f x ) /\ y IN W\r
1734 ==> (?x. x IN W /\ y = f x )`, [\r
1735 IMP_TAC THEN DISCH_TAC;\r
1736 FIRST_ASSUM (NHANH_PAT `\x. x ==> l`);\r
1737 STRIP_TAC;\r
1738 UNDISCH_TAC `y:A IN W `;\r
1739 FIRST_ASSUM (fun x -> PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [x]);\r
1740 NHANH IN_ORBIT_MAP_IMP_F_Y;\r
1741 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1742 FIRST_ASSUM (NHANH_PAT `\x. x ==> y `);\r
1743 STRIP_TAC;\r
1744 UNDISCH_TAC `y:A IN W `;\r
1745 FIRST_ASSUM (fun x -> PAT_REWRITE_TAC`\x. x ==> y `[x]);\r
1746 REWRITE_TAC[orbit_map; IN_ELIM_THM; POWER_FUNCTION; GSYM COM_POWER_FUNCTION];\r
1747 STRIP_TAC;\r
1748 EXISTS_TAC `(f POWER n) (y:A) `;\r
1749 CONJ_TAC;\r
1750 ASM_REWRITE_TAC[lemma_in_orbit];\r
1751 FIRST_X_ASSUM ACCEPT_TAC]);;\r
1752 \r
1753 \r
1754 \r
1755 \r
1756 \r
1757 \r
1758 \r
1759 \r
1760 \r
1761 \r
1762 \r
1763 \r
1764 \r
1765 \r
1766 \r
1767 \r
1768 (* ================================= *)\r
1769 (*   definition 7.8   RTPRRJS        *)\r
1770 (*   chapter: Local Fan              *)\r
1771 (* ================================= *)\r
1772 \r
1773 \r
1774 let generic = new_definition` generic V E <=>\r
1775 (! v w u. {v,w} IN E /\ u IN V ==> aff_ge { vec 0 } {v,w} INTER \r
1776 aff_lt {vec 0} {u} = {} )`;;\r
1777 \r
1778 \r
1779 let circular = new_definition ` circular V E <=> \r
1780 (? v w u. {v,w} IN E /\ u IN V /\ ~(aff_gt { vec 0 } {v,w} INTER \r
1781 aff_lt {vec 0} {u} = {}) )`;;\r
1782 \r
1783 \r
1784 let lunar = new_definition\r
1785 ` lunar (v,w) V E <=> ~(circular V E) /\ {v,w} SUBSET V /\\r
1786 ~( v = w ) /\ collinear {vec 0, v, w } `;;\r
1787 \r
1788 open Aff_sgn_tac;;\r
1789 let AFF_SGN_TRULE tm = prove (tm, AFF_SGN_TAC);;\r
1790 \r
1791 \r
1792 let DIH2K_IMP_NODE_MAP_X_DIFF_X =\r
1793 prove(`FINITE (dart H) /\ dih2k H k /\ ~(k = 0) ==> \r
1794 (!x. x IN dart H ==> ~((node_map H) x = x )) `,\r
1795 NHANH DIH2K_IMP_PRE_SIMPLE_HYP THEN \r
1796 STRIP_TAC THEN FIRST_ASSUM NHANH THEN \r
1797 MESON_TAC[face_refl]);;\r
1798 \r
1799 \r
1800 \r
1801 \r
1802 let FAN_IMP_FINITE_DARTS = \r
1803 prove(` FAN ((x:real^3),V,E) ==> FINITE (darts_of_hyp E V) `,\r
1804 NHANH HYP_LEMMA THEN \r
1805 SIMP_TAC[GSYM hypermap_tybij; HYP]);;\r
1806 \r
1807 \r
1808 \r
1809 let FAN_IMP_NOT_EMPTY_DARTS =\r
1810 prove(` FAN ((x:real^N),V,E) ==> ~(darts_of_hyp E V = {} ) `,\r
1811 REWRITE_TAC[darts_of_hyp; FAN; fan1; ord_pairs; self_pairs; EE]\r
1812 THEN SET_TAC[]);;\r
1813 \r
1814 \r
1815 \r
1816 \r
1817 \r
1818 \r
1819 \r
1820 let FAN7_SIMPLE =\r
1821 prove(`!x. fan7 ((x:real^N),V,E) ==> (!a b. a IN V /\ b IN V \r
1822 ==> aff_ge {x} {a} INTER aff_ge {x} {b} =\r
1823 aff_ge {x} ({a} INTER {b})) `,\r
1824 REWRITE_TAC[fan7] THEN SET_TAC[]);;\r
1825 \r
1826 \r
1827 \r
1828 \r
1829 \r
1830 let FAN_IMP_DIFF =\r
1831 prove(`FAN (x,V,E) ==> (!v. v IN V \/ v IN UNIONS E ==> ~( v = x )) `,\r
1832 REWRITE_TAC[FAN; fan2] THEN SET_TAC[]);;\r
1833 \r
1834 \r
1835 \r
1836 let AFF_GE_TO_AFF_GT2_GE1 = prove_by_refinement(\r
1837 ` ~( u = x ) /\ ~( v = x ) ==>\r
1838 aff_ge {x} {u,v} = aff_gt {x} {u,v} UNION aff_ge {x} {u} \r
1839 UNION aff_ge {x} {v} `,\r
1840 [SIMP_TAC[\r
1841 AFF_SGN_TRULE` ~( u = x ) /\ ~( v = x ) ==>\r
1842 aff_ge {x} {u,v} = {w| ? tx tu tv. &0 <= tu /\ &0 <= tv /\\r
1843 tx + tu + tv = &1 /\ w = tx % x + tu % u + tv % v } `];\r
1844 SIMP_TAC[\r
1845 AFF_SGN_TRULE` ~( u = x ) /\ ~( v = x ) ==>\r
1846 aff_gt {x} {u,v} = {w| ? tx tu tv. &0 < tu /\ &0 < tv /\\r
1847 tx + tu + tv = &1 /\ w = tx % x + tu % u + tv % v } `];\r
1848 SIMP_TAC[\r
1849 AFF_SGN_TRULE` ~( u = x ) ==>\r
1850 aff_ge {x} {u} = {w| ? tx tu . &0 <= tu /\ \r
1851 tx + tu  = &1 /\ w = tx % x + tu % u} `];\r
1852 REWRITE_TAC[SET_RULE` a = b <=> (!x. x IN a <=> x IN b) `; IN_ELIM_THM; IN_UNION];\r
1853 REPEAT STRIP_TAC;\r
1854 EQ_TAC;\r
1855 STRIP_TAC;\r
1856 ASM_CASES_TAC ` tu = &0 `;\r
1857 DISJ2_TAC THEN DISJ2_TAC;\r
1858 EXISTS_TAC ` tx: real `;\r
1859 EXISTS_TAC `tv:real`;\r
1860 ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];\r
1861 ASM_REAL_ARITH_TAC;\r
1862 (* ========= *)\r
1863 ASM_CASES_TAC ` tv = &0 `;\r
1864 DISJ2_TAC THEN DISJ1_TAC;\r
1865 EXISTS_TAC `tx:real`;\r
1866 EXISTS_TAC `tu:real`;\r
1867 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];\r
1868 ASM_REAL_ARITH_TAC;\r
1869 DISJ1_TAC;\r
1870 ASM_MESON_TAC[REAL_ARITH` &0 <= a /\ ~(a = &0 ) <=> &0 < a `];\r
1871 (* _______________ *)\r
1872 STRIP_TAC;\r
1873 ASM_MESON_TAC[REAL_ARITH` &0 <= a /\ ~(a = &0 ) <=> &0 < a `];\r
1874 (* iiiii *)\r
1875 EXISTS_TAC `tx:real`;\r
1876 EXISTS_TAC `tu:real `;\r
1877 EXISTS_TAC ` &0 `;\r
1878 ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_ADD_RID];\r
1879 REAL_ARITH_TAC;\r
1880 (* yyyyyyyyyyyy *)\r
1881 EXISTS_TAC ` tx:real `;\r
1882 EXISTS_TAC ` &0 `;\r
1883 EXISTS_TAC `tu:real`;\r
1884 ASM_SIMP_TAC[REAL_ADD_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID];\r
1885 REAL_ARITH_TAC]);;\r
1886 \r
1887 \r
1888 \r
1889 \r
1890 \r
1891 \r
1892 \r
1893 let AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL = \r
1894 prove_by_refinement(`~((v:real^3) = vec 0)/\\r
1895 ~( u = vec 0 ) /\\r
1896 ~(aff_ge {vec 0} {v} INTER aff_lt {vec 0} {u} = {}) \r
1897 ==> ~ (u = v ) /\ collinear {vec 0, u, v } `,\r
1898 [ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1899 STRIP_TAC THEN DOWN;\r
1900 ASM_SIMP_TAC[AFF_GE_1_1; \r
1901 REWRITE_RULE[SET_RULE` DISJOINT {a} {b} <=> ~( a = b ) `]\r
1902 AFF_LT_1_1; SET_RULE` ~( {} = a INTER b ) <=> ?x. x IN a /\ x IN b `];\r
1903 REWRITE_TAC[IN_ELIM_THM];\r
1904 STRIP_TAC;\r
1905 CONJ_TAC;\r
1906 STRIP_TAC;\r
1907 UNDISCH_TAC` x = t1' % vec 0 + t2' % (u:real^3) `;\r
1908 ASM_SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
1909 REWRITE_TAC[VECTOR_ARITH` a % x = b % x <=> (a - b ) % x = vec 0 `];\r
1910 REWRITE_TAC[VECTOR_MUL_EQ_0];\r
1911 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1912 ASM_SIMP_TAC[DE_MORGAN_THM];\r
1913 ASM_REAL_ARITH_TAC;\r
1914 (* hhhhhhhhhh *)\r
1915 ASM_REWRITE_TAC[COLLINEAR_LEMMA];\r
1916 EXISTS_TAC ` t2' / (t2:real) `;\r
1917 DOWN;\r
1918 ASM_SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
1919 \r
1920 ASM_CASES_TAC ` t2 = &0 `;\r
1921 ASM_SIMP_TAC[VECTOR_ARITH` &0 % x = c <=> c = vec 0`;VECTOR_MUL_EQ_0];\r
1922 ASM_REAL_ARITH_TAC;\r
1923 ASSUME_TAC2 (REAL_FIELD` ~( t2 = &0) ==> t2' = t2 * (t2' / t2 ) `);\r
1924 FIRST_ASSUM SUBST1_TAC;\r
1925 REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; VECTOR_MUL_LCANCEL];\r
1926 DOWN THEN ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1927 SIMP_TAC[];\r
1928 REPEAT STRIP_TAC;\r
1929 ASM_REAL_ARITH_TAC]);;\r
1930 \r
1931 \r
1932 \r
1933 \r
1934 \r
1935 \r
1936 \r
1937 \r
1938 let CIZMRRH = prove_by_refinement\r
1939 (`local_fan (V,E,FF) ==>\r
1940 generic V E /\ ~(circular V E \/ (? v w. lunar (v,w) V E )) \/ \r
1941 circular V E /\ ~(generic V E \/ (? v w. lunar (v,w) V E )) \/ \r
1942 (? v w. lunar (v,w) V E ) /\ ~( generic V E \/ circular V E )  `,\r
1943 [ASM_CASES_TAC `(!v w u.\r
1944               {(v:real^3), w} IN E /\ u IN V\r
1945               ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})`;\r
1946 REWRITE_TAC[convex_local_fan; generic];\r
1947 STRIP_TAC;\r
1948 DISJ1_TAC;\r
1949 ASM_REWRITE_TAC[circular; lunar; DE_MORGAN_THM];\r
1950 CONJ_TAC;\r
1951 REWRITE_TAC[NOT_EXISTS_THM;\r
1952 TAUT` ~( a /\ b /\ c) <=> a /\ b ==> ~c `];\r
1953 ASM_MESON_TAC[\r
1954 SET_RULE` a INTER b = {} /\ aa SUBSET a ==> aa INTER b = {} `;\r
1955 AFF_GT_SUBSET_AFF_GE];\r
1956 REWRITE_TAC[GSYM circular; NOT_EXISTS_THM; DE_MORGAN_THM];\r
1957 REPEAT GEN_TAC THEN DISJ2_TAC;\r
1958 ASM_CASES_TAC `{v:real^3, w} SUBSET V `;\r
1959 DISJ2_TAC;\r
1960 REWRITE_TAC[GSYM (TAUT` ~ a ==> b <=> a \/ b `)];\r
1961 \r
1962 DOWN_TAC;\r
1963 REWRITE_TAC[local_fan];\r
1964 LET_TAC;\r
1965 NHANH FAN_IMP_NOT_EMPTY_DARTS;\r
1966 NHANH ELMS_OF_HYPERMAP_HYP;\r
1967 ASM_SIMP_TAC[];\r
1968 IMP_TAC;\r
1969 REWRITE_TAC[TAUT`(a/\b)/\c <=> a/\b/\c`];\r
1970 IMP_TAC;\r
1971 IMP_TAC;\r
1972 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1973 SIMP_TAC[];\r
1974 NHANH (MESON[dih2k]` dih2k H d ==> CARD (dart H) = 2 * d `);\r
1975 MP_TAC (ISPEC `H: (real^3#real^3)hypermap ` hypermap_lemma);\r
1976 REPEAT STRIP_TAC;\r
1977 ASSUME_TAC2 (ISPEC `dart (H:(real^3#real^3)hypermap)` CARD_EQ_0);\r
1978 UNDISCH_TAC` ~( {} = dart (H:(real^3#real^3)hypermap)) `;\r
1979 REWRITE_TAC[];\r
1980 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
1981 FIRST_X_ASSUM (SUBST1_TAC o SYM);\r
1982 DOWN;\r
1983 ASM_REWRITE_TAC[ARITH_RULE`2 * k = 0 <=> k = 0 `];\r
1984 ONCE_REWRITE_TAC[TAUT` a ==> b <=> ~ b ==> ~ a `];\r
1985 STRIP_TAC;\r
1986 ASSUME_TAC2 (\r
1987 ISPECL [`CARD (FF:real^3#real^3 -> bool) `;`H:(real^3#real^3) hypermap `] \r
1988 (GEN_ALL DIH2K_IMP_NODE_MAP_X_DIFF_X));\r
1989 DOWN_TAC;\r
1990 REWRITE_TAC[FAN; INSERT_SUBSET; EMPTY_SUBSET];\r
1991 STRIP_TAC;\r
1992 ASSUME_TAC2 (SPEC `v:real^3 ` IN_V_OF_FAN_EXISTS_DART);\r
1993 DOWN;\r
1994 ASM_REWRITE_TAC[];\r
1995 FIRST_X_ASSUM NHANH;\r
1996 STRIP_TAC;\r
1997 DOWN THEN DOWN;\r
1998 UNDISCH_TAC` darts_of_hyp E (V:real^3 -> bool) = dart H `;\r
1999 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2000 SIMP_TAC[];\r
2001 STRIP_TAC;\r
2002 REWRITE_TAC[darts_of_hyp; IN_UNION; self_pairs; IN_ELIM_THM];\r
2003 ONCE_REWRITE_TAC[TAUT`a\/b <=> b\/a`];\r
2004 DISCH_THEN DISJ_CASES_TAC;\r
2005 DOWN THEN STRIP_TAC;\r
2006 UNDISCH_TAC `n_of_hyp (vec 0,(V:real^3 -> bool),E) = node_map H`;\r
2007 ONCE_REWRITE_TAC[EQ_SYM_EQ];\r
2008 SIMP_TAC[];\r
2009 STRIP_TAC;\r
2010 REWRITE_TAC[n_of_hyp];\r
2011 UNDISCH_TAC` EE (v'':real^3) E = {} `;\r
2012 DOWN THEN DOWN;\r
2013 SIMP_TAC[PAIR_EQ; EMPTY_SUBSET; W_SUBSET_SINGLETON_IMP_IDE];\r
2014 (* --------------------------------------------------- *)\r
2015 DOWN;\r
2016 REWRITE_TAC[ord_pairs; IN_ELIM_THM; PAIR_EQ];\r
2017 STRIP_TAC;\r
2018 ASM_REWRITE_TAC[];\r
2019 STRIP_TAC;\r
2020 UNDISCH_TAC` (w:real^3) IN V `;\r
2021 UNDISCH_TAC ` {(a:real^3),b} IN E `;\r
2022 PHA;\r
2023 UNDISCH_TAC `!v w u.\r
2024           {(v:real^3), w} IN E /\ u IN V\r
2025           ==> {} = aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u}`;\r
2026 DISCH_TAC;\r
2027 FIRST_ASSUM NHANH;\r
2028 DOWN_TAC;\r
2029 REWRITE_TAC[fan2];\r
2030 REWRITE_TAC[SET_RULE` ~( x IN s) <=> (!a. a IN s ==> ~(a = x )) `];\r
2031 REPLICATE_TAC 10 (IMP_TAC THEN DISCH_TAC);\r
2032 FIRST_X_ASSUM NHANH;\r
2033 STRIP_TAC;\r
2034 REWRITE_TAC[COLLINEAR_LEMMA; DE_MORGAN_THM];\r
2035 CONJ_TAC THENL [\r
2036 EXPAND_TAC "a" THEN \r
2037 FIRST_ASSUM ACCEPT_TAC;\r
2038 CONJ_TAC THENL [\r
2039 FIRST_ASSUM ACCEPT_TAC;\r
2040 REWRITE_TAC[]]];\r
2041 \r
2042 ASSUME_TAC2 (ISPEC `vec 0:real^3 ` FAN7_SIMPLE);\r
2043 DOWN THEN PHA THEN STRIP_TAC;\r
2044 STRIP_TAC;\r
2045 ASM_CASES_TAC `c = &0 ` THENL [\r
2046 UNDISCH_TAC `w = c % (a:real^3)` THEN \r
2047 ASM_REWRITE_TAC[VECTOR_MUL_LZERO];\r
2048 ASM_CASES_TAC ` c = &1 `] THENL [\r
2049 UNDISCH_TAC `w = c % (a:real^3) ` THEN \r
2050 ASM_SIMP_TAC[VECTOR_MUL_LID] THEN \r
2051 EXPAND_TAC "a" THEN \r
2052 FIRST_X_ASSUM ACCEPT_TAC;\r
2053 ASM_CASES_TAC ` &0 < c `];\r
2054 (* ---------- sub 1    ---------- *)\r
2055 UNDISCH_TAC` w IN (V:real^3 -> bool) `;\r
2056 UNDISCH_TAC` v IN (V:real^3 -> bool) `;\r
2057 PHA;\r
2058 FIRST_ASSUM NHANH;\r
2059 UNDISCH_TAC`~(w = (v:real^3)) `;\r
2060 SIMP_TAC[SET_RULE`~(a = b) <=> {a} INTER {b} = {} `; INTER_COMM];\r
2061 REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];\r
2062 ASSUME_TAC2 (AFF_SGN_TRULE`!v. ~((v:real^3) = vec 0) ==>\r
2063 aff_ge {vec 0} {v} = { x| ?t0 tv. &0 <= tv /\ t0 + tv = &1 /\\r
2064 x = t0 % (vec 0) + tv % v } `);\r
2065 ASSUME_TAC2 (SPEC `w:real^3` (AFF_SGN_TRULE`!v. ~((v:real^3) = vec 0) ==>\r
2066 aff_ge {vec 0} {v} = { x| ?t0 tv. &0 <= tv /\ t0 + tv = &1 /\\r
2067 x = t0 % (vec 0) + tv % v } `));\r
2068 DOWN THEN DOWN THEN PHA THEN SIMP_TAC[];\r
2069 REPEAT STRIP_TAC;\r
2070 DOWN;\r
2071 UNDISCH_TAC ` ~((w:real^3) = vec 0) `;\r
2072 PHA;\r
2073 MATCH_MP_TAC (SET_RULE` a IN S ==> ~(~(a = x ) /\ S = {x}) `);\r
2074 REWRITE_TAC[IN_INTER; IN_ELIM_THM];\r
2075 CONJ_TAC;\r
2076 EXISTS_TAC` &1 - c `;\r
2077 EXISTS_TAC `c:real`;\r
2078 UNDISCH_TAC `&0 < c `;\r
2079 SIMP_TAC[REAL_ARITH` &0 < a ==> &0 <= a `;\r
2080 REAL_ARITH` &1 - c + c = &1 `; VECTOR_MUL_RZERO;\r
2081 VECTOR_ADD_LID];\r
2082 ASM_REWRITE_TAC[];\r
2083 (* ============================ *)\r
2084 EXISTS_TAC `&0 `;\r
2085 EXISTS_TAC `&1 `;\r
2086 \r
2087 SIMP_TAC[VECTOR_MUL_LID; VECTOR_MUL_RZERO;\r
2088 VECTOR_ADD_LID];\r
2089 REAL_ARITH_TAC;\r
2090 UNDISCH_TAC ` ~(c = &0 ) `;\r
2091 DOWN;\r
2092 PHA;\r
2093 REWRITE_TAC[REAL_ARITH` ~(&0 < c) /\ ~(c = &0) <=> c < &0 `];\r
2094 STRIP_TAC;\r
2095 UNDISCH_TAC` {} = aff_ge {vec 0} {a, b} INTER aff_lt {vec 0} {(w:real^3)}`;\r
2096 EXPAND_TAC "a";\r
2097 EXPAND_TAC "b";\r
2098 ASSUME_TAC2 (AFF_SGN_TRULE` ~((w:real^3) = vec 0) ==>\r
2099 aff_lt {vec 0} {w} = {x | ? t0 tw . tw < &0 /\ t0 + tw = &1 /\\r
2100 x = t0 % (vec 0) + tw % w }`);\r
2101 ASSUME_TAC2 (\r
2102 AFF_SGN_TRULE` ~((v:real^3) = vec 0) /\ ~( v' = vec 0) ==>\r
2103 aff_ge {vec 0} {v,v'} = {x | ? t0 tv tv' . &0 <= tv /\ \r
2104 &0 <= tv' /\ t0 + tv + tv' = &1 /\\r
2105 x = t0 % (vec 0) + tv % v + tv' % v'  }`);\r
2106 MATCH_MP_TAC (\r
2107 SET_RULE` -- (w:real^3) IN S ==> {} = S ==> F `);\r
2108 DOWN THEN DOWN THEN PHA THEN SIMP_TAC[];\r
2109 REMOVE_TAC;\r
2110 REWRITE_TAC[IN_INTER; IN_ELIM_THM];\r
2111 CONJ_TAC;\r
2112 EXISTS_TAC` &1 + c `;\r
2113 EXISTS_TAC ` -- (c:real) `;\r
2114 EXISTS_TAC `&0 `;\r
2115 ASM_REWRITE_TAC[VECTOR_MUL_LNEG; VECTOR_MUL_RZERO; VECTOR_MUL_LZERO; \r
2116 VECTOR_ADD_RID; VECTOR_ADD_LID];\r
2117 DOWN THEN REAL_ARITH_TAC;\r
2118 (* =================== *)\r
2119 EXISTS_TAC `&2 `;\r
2120 EXISTS_TAC ` -- &1 `;\r
2121 REWRITE_TAC[VECTOR_MUL_LNEG; VECTOR_MUL_LID; VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
2122 REAL_ARITH_TAC;\r
2123 (* +++++++++++++++++++++++++++++++++++++++++++++++++ *)\r
2124 (* ================================================= *)\r
2125 ASM_SIMP_TAC[];\r
2126 (* ************************************************* *)\r
2127 (* ================================================= *)\r
2128 DOWN;\r
2129 REWRITE_TAC[NOT_FORALL_THM; TAUT` ~( a ==> b) <=> a /\ ~ b `;\r
2130 local_fan];\r
2131 LET_TAC;\r
2132 REPEAT STRIP_TAC;\r
2133 DOWN_TAC;\r
2134 NHANH FAN_IMP_DIFF;\r
2135 STRIP_TAC;\r
2136 SUBGOAL_THEN ` (v:real^3) IN UNIONS E /\ w IN UNIONS E ` ASSUME_TAC\r
2137 THENL [REWRITE_TAC[IN_UNIONS] THEN \r
2138 ASM_MESON_TAC[SET_RULE` a IN {a,b} /\ b IN {a,b} `];\r
2139 DOWN_TAC];\r
2140 REWRITE_TAC[MESON[]`(!x. P x \/ Q x ==> R x) <=>\r
2141 (! x. P x ==> R x ) /\ (!x. Q x ==> R x ) `];\r
2142 STRIP_TAC;\r
2143 DOWN THEN DOWN;\r
2144 FIRST_X_ASSUM NHANH;\r
2145 UNDISCH_TAC `(u:real^3) IN V `;\r
2146 FIRST_ASSUM NHANH;\r
2147 REPEAT STRIP_TAC;\r
2148 ASSUME_TAC2 (\r
2149 AFF_SGN_TRULE` ~((v:real^3) = vec 0 ) /\ ~(w = vec 0 ) ==>\r
2150 aff_ge {vec 0} {v, w} = {x | ? t0 tv tw. &0 <= tv /\ &0 <= tw /\\r
2151 t0 + tv + tw = &1 /\ x = t0 % (vec 0) + tv % v + tw % w } `);\r
2152 ASSUME_TAC2 (\r
2153 ISPECL [`(vec 0):real^3 `;`u:real^3`] (REWRITE_RULE[DISJOINT; \r
2154 SET_RULE` {a} INTER {b} = {} <=> ~( b = a )`] AFF_LT_1_1));\r
2155 SUBGOAL_THEN` ~ (generic (V:real^3 -> bool) E )` ASSUME_TAC\r
2156 THENL [REWRITE_TAC[generic] THEN \r
2157 ASM_MESON_TAC[];\r
2158 UNDISCH_TAC `~(aff_ge {vec 0} {(v:real^3), w} INTER \r
2159 aff_lt {vec 0} {u} = {})`];\r
2160 ASSUME_TAC2 (\r
2161 ISPECL [` v:real^3 `;` (vec 0): real^3 `;` w:real^3 `] \r
2162 (GEN_ALL AFF_GE_TO_AFF_GT2_GE1));\r
2163 DOWN THEN SIMP_TAC[];\r
2164 STRIP_TAC;\r
2165 REWRITE_TAC[SET_RULE`( a UNION b ) INTER c = {} <=> a INTER c = {} /\\r
2166 b INTER c = {} `];\r
2167 STRIP_TAC;\r
2168 ASM_SIMP_TAC[];\r
2169 DOWN THEN REWRITE_TAC[DE_MORGAN_THM];\r
2170 DISCH_TAC;\r
2171 ASM_CASES_TAC ` circular (V:real^3 -> bool) E ` THENL [\r
2172 ASM_SIMP_TAC[lunar];\r
2173 DISJ2_TAC];\r
2174 ASM_SIMP_TAC[lunar];\r
2175 DOWN THEN DOWN THEN STRIP_TAC;\r
2176 (* there are three subgoal here *)\r
2177 (* -------- sub 1  -------------- *)\r
2178 REWRITE_TAC[circular];\r
2179 ASM_MESON_TAC[];\r
2180 (* --------- sub 2 --------------  *)\r
2181 DISCH_TAC;\r
2182 EXISTS_TAC `v:real^3`;\r
2183 EXISTS_TAC `u:real^3 `;\r
2184 ASSUME_TAC2 AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL;\r
2185 DOWN;\r
2186 ASM_SIMP_TAC[INSERT_COMM; INSERT_SUBSET; EMPTY_SUBSET];\r
2187 DISCH_TAC;\r
2188 MATCH_MP_TAC (SET_RULE`v IN UNIONS E /\ UNIONS E SUBSET V ==> v IN V `);\r
2189 DOWN_TAC;\r
2190 SIMP_TAC[FAN];\r
2191 (* -------------- sub 3 ------------- *)\r
2192 DISCH_TAC;\r
2193 EXISTS_TAC `u:real^3 `;\r
2194 EXISTS_TAC `w:real^3 `;\r
2195 ASSUME_TAC2 (\r
2196 SPEC `w:real^3 ` (GEN `v:real^3 ` AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL));\r
2197 ASM_SIMP_TAC[];\r
2198 ASM_SIMP_TAC[INSERT_COMM; INSERT_SUBSET; EMPTY_SUBSET];\r
2199 MATCH_MP_TAC (SET_RULE`v IN UNIONS E /\ UNIONS E SUBSET V ==> v IN V `);\r
2200 DOWN_TAC;\r
2201 SIMP_TAC[FAN]]);;\r
2202 \r
2203 end;;\r