text_formalization/tame/FATUGPD.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALISATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: FATUGPD                                                             *)
   5 (* Chapter: Tame                                                              *)
   6 (* Author: Vuong Anh Quyen                                                    *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 flyspeck_needs "hypermap/hypermap.hl";;
  12 flyspeck_needs "fan/fan_defs.hl";;
  13 flyspeck_needs "fan/planarity.hl";;
  14 flyspeck_needs "leg/geomdetail.hl";;
  15 flyspeck_needs "packing/pack2.hl";; (* for KIUMVTC  *)
  16 flyspeck_needs "packing/pack_defs.hl";; (* for h0 def and others *)
  17 flyspeck_needs "trigonometry/trig1.hl";;
  18 flyspeck_needs "general/prove_by_refinement.hl";;
  19 flyspeck_needs "tame/tame_concl.hl";;
  20 flyspeck_needs "tame/tame_defs.hl";;  (* was commented out *)
  21
  22 module Fatugpd = struct
  23
  24 open Hypermap;;
  25 open Fan_defs;;
  26 open Fan;;
  27 open Planarity;;
  28 open Pack_defs;;
  29 open Pack1;;
  30 open Pack2;;
  31 open Tame_defs;;
  32 open Trigonometry1;;
  33 open Tame_defs;;
  34 open Prove_by_refinement;;
  35
  36 let JBDNJJB = Planarity.JBDNJJB;;
  37
  38 (* my assumptions *)
  39
  40   let UBHDEUU2_concl =  Tame_concl.UBHDEUU2_concl;;
  41
  42   let UBHDEUU2_hypothesis = new_definition (mk_eq(`UBHDEUU2_hypothesis:bool`,UBHDEUU2_concl));;
  43
  44   let UBHDEUU2_quasi = UNDISCH(MATCH_MP (TAUT `(x = y) ==> (x ==> y)`) UBHDEUU2_hypothesis);;
  45
  46
  47  (* my tatics *)
  48
  49 let Q_LABEL_TAC term phr = UNDISCH_THEN term (LABEL_TAC phr);;
  50
  51 let Q_ABBREV_TAC term str = (ABBREV_TAC term) THEN
  52    FIRST_X_ASSUM (LABEL_TAC str);;
  53
  54 let Q_EXPAND_TAC str = (USE_THEN str (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));;
  55
  56 (* some of my lemmas that may help others *)
  57 let NOT_EMPTY_IMAGE = prove
  58 ( ` !(S:A -> bool) (f:A->B). ~( S = {}) ==> ~( IMAGE f S = {})`, SET_TAC[]);;
  59
  60 (* lemma about sup of function on finite set *)
  61 let finite_num_func_attain_max =
  62 prove_by_refinement(
  63 `! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {})
  64      ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`,
  65 [
  66   (REPEAT STRIP_TAC);
  67
  68 (* subgoal 1 *)
  69   (SUBGOAL_THEN
  70 ` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})`
  71 ASSUME_TAC);
  72   CONJ_TAC;
  73 (* subgoal 1.1 *)
  74   (ASM_SIMP_TAC[FINITE_IMAGE]);
  75 (* subgoal 2.1 *)
  76   (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
  77
  78   (FIRST_ASSUM(MP_TAC o (MATCH_MP SUP_FINITE)));
  79   (CONV_TAC(PAT_CONV `\k. _ IN k /\ _ ==> _` (REWRITE_CONV[IMAGE])));
  80   (PURE_REWRITE_TAC[IN_ELIM_THM]);
  81   STRIP_TAC;
  82   (EXISTS_TAC `x:A`);
  83   (ASM_SIMP_TAC[]);
  84   (REPEAT STRIP_TAC);
  85   (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`));
  86
  87 (* subgoal 2 *)
  88   (SUBGOAL_THEN ` (& o (f:A->num)) y IN IMAGE (& o f) S` ASSUME_TAC);
  89   (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
  90   (EXISTS_TAC `y:A` THEN ASM_SIMP_TAC[]);
  91
  92     (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]);
  93 ]);;
  94
  95
  96 (* lemma about property of sup *)
  97 let sup_property1 = prove_by_refinement(
  98 `! (S:real->bool). ~(S = {}) /\(?b. !x. x IN S ==> x <= b) ==>
  99       (! epsilon. epsilon > &0 ==> ?x. x IN S /\ x > sup S - epsilon)`,
 100 [
 101 (GEN_TAC THEN DISCH_THEN  (MP_TAC o (MATCH_MP SUP)));
 102 (STRIP_TAC THEN GEN_TAC);
 103 (DISCH_THEN (ASSUME_TAC o (MATCH_MP (ARITH_RULE
 104 ` epsilon > &0 ==> ~ ( sup (S:real->bool) <= sup S - epsilon)`))));
 105 (MATCH_MP_TAC (MESON[]
 106 `! (P:A->bool) (Q:A->bool). ~(!(x:A). P x ==> ~ (Q x))
 107               ==> (?(x:A). P x /\ Q x)`));
 108 (PURE_REWRITE_TAC[ARITH_RULE
 109 `~(x > sup S - epsilon) <=> x <= sup S - epsilon`]);
 110 (ASM_MESON_TAC[]);]);;
 111
 112
 113 (* lemma about maximal of num bounded function *)
 114
 115 let bdd_num_func_attain_max = prove_by_refinement(
 116 `! (S:A ->bool) (f:A-> num). ~(S = {})/\(?m. !x. x IN S ==> f x <= m)
 117       ==> (?x. x IN S /\ (!y. y IN S ==> f y  <= f x))`,
 118 [
 119 (REPEAT STRIP_TAC);
 120 (* subgoal 1 *)
 121 (SUBGOAL_THEN `~( IMAGE (& o (f:A->num)) (S:A->bool) = {})
 122   /\ (? b. ! y. y IN (IMAGE (& o f) S) ==> y <= b)` ASSUME_TAC);
 123 (CONJ_TAC);
 124
 125 (* subgoal 1.1 *)
 126 (ASM_SET_TAC[]);
 127
 128 (* subgoal 1.2 *)
 129 (EXISTS_TAC `& (m:num)`);
 130 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM]);
 131 (REPEAT STRIP_TAC);
 132 (ONCE_ASM_REWRITE_TAC[]);
 133 (ASM_SIMP_TAC[REAL_OF_NUM_LE]);
 134
 135 (FIRST_ASSUM (MP_TAC o MATCH_MP SUP));
 136 (ABBREV_TAC `p = sup (IMAGE (& o (f:A->num)) (S:A->bool))` THEN STRIP_TAC);
 137 (* subgoal 2 *)
 138 (SUBGOAL_THEN
 139 `?z. z IN (IMAGE (& o (f:A->num)) (S:A->bool)) /\ z > p - &1` MP_TAC);
 140 (EXPAND_TAC "p");
 141 (FIRST_ASSUM (MP_TAC o (SPEC `&1`) o (MATCH_MP sup_property1)));
 142 (SIMP_TAC[ARITH_RULE `&1 > &0`]);
 143
 144 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM] THEN STRIP_TAC );
 145 (EXISTS_TAC `x:A`);
 146 (ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);
 147 (MATCH_MP_TAC (ARITH_RULE ` n < (m:num) + 1 ==> n <= m`));
 148 (* subgoal 3 *)
 149 (SUBGOAL_THEN
 150 `&((f:A->num) y) IN (IMAGE (& o f) (S:A->bool))` ASSUME_TAC);
 151 (ASM_SIMP_TAC[IN_ELIM_THM;o_THM;IMAGE]);
 152 (EXISTS_TAC `y:A`);
 153 (ASM_SIMP_TAC[]);
 154
 155 (* subgoal 4 *)
 156 (SUBGOAL_THEN `&((f:A->num) y) <= p` ASSUME_TAC);
 157 (ASM_SIMP_TAC[]);
 158
 159 (MATCH_MP_TAC
 160   (fst(EQ_IMP_RULE (SPECL [`(f:A->num) y`;`f x + 1`] REAL_OF_NUM_LT))));
 161 (PURE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD]);
 162 (ASM_ARITH_TAC);
 163 ]);;
 164
 165
 166 let BIJ_CARD_EQ = prove
 167 ( `! (V:A->bool) (U:B->bool) (f:A->B). FINITE V /\ BIJ f V U
 168             ==> CARD U = CARD V`,
 169 REPEAT GEN_TAC THEN REWRITE_TAC[BIJ;INJ;SURJ] THEN STRIP_TAC THEN
 170 MATCH_MP_TAC CARD_EQ_CARD_IMP THEN ASM_SIMP_TAC[] THEN
 171 ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c]
 172 THEN EXISTS_TAC `f:A->B` THEN ASM_MESON_TAC[]);;
 173
 174
 175 (* another property of sup *)
 176 let SUP_lt = prove_by_refinement(
 177 `! (S:real -> bool) (b:real).
 178 ~(S = {}) /\ FINITE S /\ (!x. x IN S ==> x < b)   ==> sup S < b`,
 179 [
 180 (REPEAT STRIP_TAC);
 181 (FIRST_ASSUM (fun thm -> (MATCH_MP_TAC thm)));
 182 (ASM_SIMP_TAC[SUP_FINITE]);
 183 ]);;
 184
 185
 186 (* epsilon lemma *)
 187 let epsilon_lemma = prove_by_refinement(
 188  `! (a:real) b. a < b ==> ? epsilon. epsilon > &0 /\ b > a + epsilon`,
 189 [
 190 (REPEAT STRIP_TAC);
 191 (EXISTS_TAC `(b - a) / &2`);
 192 ASM_ARITH_TAC;
 193 ]);;
 194
 195 let normalize = new_definition `!(v:real^N). normalize v = inv (norm v) % v`;;
 196
 197 let norm_normalize = prove_by_refinement(
 198  `! (v:real^3). ~(v = vec 0) ==> norm (normalize v) = &1 `,
 199 [
 200 (GEN_TAC THEN STRIP_TAC);
 201 (PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]);
 202 (MATCH_MP_TAC REAL_MUL_LINV);
 203 (ASM_MESON_TAC[NORM_EQ_0]);
 204 ]);;
 205
 206
 207 let normalize_vec_0 = prove_by_refinement(
 208  `normalize (vec 0:real^N) = (vec 0:real^N)`,
 209 [(PURE_REWRITE_TAC[normalize;REAL_INV_0;NORM_0;VECTOR_MUL_LZERO]);
 210 VECTOR_ARITH_TAC;]);;
 211
 212
 213 let norm_mul_normalize = prove_by_refinement(
 214 `! (v:real^3).(norm v) % (normalize v) = v`,
 215 [
 216 (GEN_TAC);
 217 (ASM_CASES_TAC `v:real^3 = vec 0`);
 218
 219 (* subgoal 1 *)
 220 (ASM_SIMP_TAC[normalize_vec_0; VECTOR_MUL_RZERO]);
 221
 222 (* subgoal 2 *)
 223 (PURE_REWRITE_TAC[normalize;VECTOR_MUL_ASSOC]);
 224 (SUBGOAL_THEN `~(norm (v:real^3) = &0)` (ASSUME_TAC o MATCH_MP REAL_MUL_RINV));
 225 (ASM_MESON_TAC[NORM_EQ_0]);
 226 (ASM_SIMP_TAC[VECTOR_MUL_LID]);]);;
 227
 228
 229 let dot_normalize = prove_by_refinement(
 230  `! v:real^3. v dot (normalize v) = norm v`,
 231 [
 232 (GEN_TAC);
 233 (ASM_CASES_TAC `v:real^3 = vec 0`);
 234
 235 (* subgoal 1 *)
 236 (ASM_SIMP_TAC[NORM_0;DOT_LZERO]);
 237
 238 (* subgoal 2 *)
 239 (SUBGOAL_THEN ` norm (v:real^3) * (v dot normalize v) = norm v pow 2` MP_TAC);
 240 (ONCE_REWRITE_TAC[GSYM DOT_RMUL]);
 241 (ASM_SIMP_TAC[norm_mul_normalize;DOT_SQUARE_NORM]);
 242
 243 (ONCE_REWRITE_TAC[REAL_POW_2]);
 244 (MATCH_MP_TAC (REWRITE_RULE [TAUT `A /\ B ==> C <=> A ==> (B ==> C)`] REAL_EQ_LCANCEL_IMP));
 245 (ASM_SIMP_TAC[NORM_EQ_0]);]);;
 246
 247
 248 let fourier = prove_by_refinement(
 249  ` ! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3
 250 ==> v = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`,
 251 [
 252 (REPEAT STRIP_TAC);
 253 (FIRST_ASSUM  (ASSUME_TAC o (MATCH_MP ORTHONORMAL_IMP_SPANNING)));
 254 (UNDISCH_TAC `orthonormal (e1:real^3) e2 e3`);
 255 (ONCE_REWRITE_TAC[orthonormal]);
 256 (REPEAT STRIP_TAC);
 257 (ABBREV_TAC `(u:real^3) = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`);
 258 (* subgoal 1 *)
 259 (SUBGOAL_THEN ` (v:real^3) dot e1 =  u dot e1 `  ASSUME_TAC);
 260 (EXPAND_TAC "u");
 261 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
 262 REAL_ADD_RID;REAL_MUL_RID]);
 263
 264 (* subgoal 2 *)
 265 (SUBGOAL_THEN ` (v:real^3) dot e2 =  u dot e2 `  ASSUME_TAC);
 266 (EXPAND_TAC "u");
 267 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
 268 REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);
 269
 270 (* subgoal 3 *)
 271 (SUBGOAL_THEN ` (v:real^3) dot e3 =  u dot e3 `  ASSUME_TAC);
 272 (EXPAND_TAC "u");
 273 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
 274 REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);
 275
 276 (* subgoal 4 *)
 277 (SUBGOAL_THEN `(v:real^3) - u IN span {e1:real^3, e2, e3}` MP_TAC);
 278 (ASM_SET_TAC[]);
 279
 280 (SIMP_TAC[SPAN_3;IN_ELIM_THM;IN_UNIV]);
 281 (STRIP_TAC);
 282
 283 (* subgoal 5 *)
 284 (SUBGOAL_THEN `((v:real^3) - u) dot (v - u) = &0` MP_TAC);
 285 (PURE_REWRITE_TAC[DOT_LSUB]);
 286 (ASM_SIMP_TAC[DOT_RMUL;DOT_RADD;REAL_SUB_REFL]);
 287
 288 (ASM_SIMP_TAC[DOT_EQ_0;VECTOR_SUB_EQ]);]);;
 289
 290
 291 let norm_lemma1 = prove_by_refinement(
 292 `! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3 ==>
 293   norm v = sqrt ((v dot e1) pow 2 + (v dot e2) pow 2 + (v dot e3) pow 2)`,
 294 [
 295 (REPEAT STRIP_TAC);
 296 (PURE_REWRITE_TAC[vector_norm]);
 297 (FIRST_ASSUM (ASSUME_TAC o MATCH_MP fourier));
 298 (FIRST_ASSUM (fun thm -> CONV_TAC (PAT_CONV `\x. sqrt (x dot x) = _` (ONCE_REWRITE_CONV[thm]))));
 299 (PURE_REWRITE_TAC[DOT_RADD;DOT_LADD;DOT_RMUL;DOT_LMUL;
 300 REAL_ADD_RDISTRIB;REAL_ADD_LDISTRIB]);
 301 (ONCE_REWRITE_TAC[REAL_MUL_ASSOC]);
 302 (ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
 303 (FIRST_ASSUM (MP_TAC o MATCH_MP
 304 (fst (EQ_IMP_RULE (SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`] orthonormal)))));
 305 STRIP_TAC;
 306 (ASM_SIMP_TAC[DOT_SYM;REAL_MUL_RZERO;REAL_ADD_RID;
 307 REAL_ADD_LID;REAL_MUL_RID]);]);;
 308
 309
 310 let coordinates_lemma = prove_by_refinement(
 311  `! (v:real^3) (e1:real^3) e2 e3 (x:real) y z. orthonormal e1 e2 e3 /\
 312   v = x % e1 + y % e2 + z % e3 ==>
 313      x = v dot e1 /\ y = v dot e2 /\ z = v dot e3`,
 314 [
 315 (REPEAT GEN_TAC);
 316 (STRIP_TAC);
 317 (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` (MATCH_MP fourier thm))));
 318 (ASM_MESON_TAC[ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT]);]);;
 319
 320
 321 let dot_coordinates = prove_by_refinement(
 322  `! v:real^3 u e1 e2 e3. orthonormal e1 e2 e3
 323    ==> v dot u = (v dot e1) * (u dot e1) + (v dot e2) * (u dot e2)
 324                 + (v dot e3) * (u dot e3)`,
 325 [
 326 (REPEAT STRIP_TAC);
 327 (FIRST_ASSUM((LABEL_TAC "a") o (MATCH_MP (SPEC `u:real^3` fourier))));
 328 (USE_THEN "a" (fun thm -> (CONV_TAC (PAT_CONV `\x. A dot x = B`
 329     (ONCE_REWRITE_CONV[thm])))));
 330 (ONCE_REWRITE_TAC[VECTOR_ARITH `(v:real^3) dot (a % e1 + b % e2 + c % e3) =
 331    (v dot e1) * a + (v dot e2 ) * b + (v dot e3) * c`]);
 332 (SIMP_TAC[]);]);;
 333
 334
 335 let dot_coordinates_2 = prove_by_refinement(
 336  `! (v:real^3) u e1 e2 e3 x y z a b c. orthonormal e1 e2 e3 /\
 337    v = x % e1 + y % e2 + z % e3 /\ u = a % e1 + b % e2 + c % e3
 338  ==> v dot u = x * a + y * b + z * c`,
 339 [(ONCE_REWRITE_TAC[orthonormal]);
 340 (REPEAT STRIP_TAC);
 341 (ONCE_ASM_REWRITE_TAC[]);
 342 (ASM_SIMP_TAC[DOT_SYM;DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL]);
 343 ARITH_TAC;]);;
 344
 345
 346 let norm_lemma2 = prove_by_refinement(
 347  `! (v:real^3) e1 e2 e3 x y z. orthonormal e1 e2 e3 /\
 348    v = x % e1 + y % e2 + z % e3 ==>
 349    norm v = sqrt (x pow 2 + y pow 2 + z pow 2)`,
 350 [
 351 (REPEAT GEN_TAC);
 352 (DISCH_TAC);
 353 (FIRST_ASSUM (fun thm -> ONCE_REWRITE_TAC [ MATCH_MP norm_lemma1 (CONJUNCT1 thm)]));
 354 (FIRST_ASSUM (fun thm -> SIMP_TAC[ MATCH_MP coordinates_lemma thm]));]);;
 355
 356
 357 let dot_gt_0 = prove_by_refinement(
 358  `! v:real^3 u. &0 < v dot u <=> &0 < v dot normalize u `,
 359 [
 360 (REPEAT GEN_TAC);
 361 (ASM_CASES_TAC `u:real^3 = vec 0`);
 362
 363 (* subgoal 1 *)
 364 (ASM_SIMP_TAC[normalize_vec_0]);
 365
 366 (* subgoal 2 *)
 367 ( CONV_TAC(PAT_CONV `\x. &0 < A dot x <=> B`(ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
 368 (PURE_REWRITE_TAC[DOT_RMUL]);
 369 (MATCH_MP_TAC (CONJUNCT1 REAL_LT_MUL_EQ));
 370 (MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < x`));
 371 (ASM_SIMP_TAC[NORM_POS_LE;NORM_EQ_0]);]);;
 372
 373
 374 let dot_eq_0 = prove_by_refinement(
 375 `! v:real^3 u. v dot u = &0 <=> (normalize v) dot u = &0`,
 376 [
 377 (REPEAT GEN_TAC);
 378 (ASM_CASES_TAC `v:real^3 = vec 0`);
 379
 380 (* subgoal 1 *)
 381 (ASM_SIMP_TAC[normalize_vec_0]);
 382
 383 (* subgoal 2 *)
 384 (CONV_TAC(PAT_CONV `\x. x dot y = &0 <=> A`
 385 (ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
 386 (ONCE_REWRITE_TAC[DOT_LMUL]);
 387 (CONV_TAC(PAT_CONV `\x. x <=> A` (ONCE_REWRITE_CONV
 388 [ARITH_RULE `&0 = norm (v:real^3) * &0`])));
 389 (ONCE_REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);
 390 (ASM_SIMP_TAC[NORM_EQ_0]);]);;
 391
 392
 393 let azim_ge_azim_dart = prove_by_refinement(
 394  `! (V:real^3->bool) E w u v. FAN (vec 0, V, E) /\ w IN V /\
 395 u IN set_of_edge w V E /\ v IN set_of_edge w V E /\ ~(w = u) /\ ~(v = u)
 396    ==> azim (vec 0) w u v >= azim_dart (V,E) (w,u)`,
 397 [
 398 (REPEAT STRIP_TAC);
 399 (ASM_SIMP_TAC[azim_dart]);
 400 (PURE_REWRITE_TAC[azim_fan]);
 401
 402 (* subgoal 1 *)
 403 (SUBGOAL_THEN `CARD (set_of_edge (w:real^3) V E) > 1` ASSUME_TAC);
 404 (MP_TAC (SPECL [`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;
 405 `u:real^3`;`w:real^3`] Fan.remark1_fan));
 406 (ASM_SIMP_TAC[]);
 407 (STRIP_TAC);
 408 (MP_TAC(ISPECL [`v:real^3`;`u:real^3`] Hypermap.CARD_TWO_ELEMENTS));
 409 (ASM_SIMP_TAC[]);
 410 (MATCH_MP_TAC (ARITH_RULE `(a:num) <= b ==> a = 2 ==> b > 1`));
 411 (MATCH_MP_TAC CARD_SUBSET);
 412 (ASM_SET_TAC[]);
 413
 414 (ASM_SIMP_TAC[]);
 415 (* subgoal 2 *)
 416 (SUBGOAL_THEN `~(set_of_edge (w:real^3) V E = {u})` ASSUME_TAC);
 417 (ONCE_REWRITE_TAC[TAUT ` ~A <=> A ==> F`]);
 418 (DISCH_THEN (MP_TAC o (AP_TERM `(\(S:real^3->bool). CARD S)`)));
 419 (SIMP_TAC[BETA_THM;Geomdetail.CARD_SING]);
 420 (ASM_ARITH_TAC);
 421 (MP_TAC (SPECL [`vec 0 :real^3`;`V:real^3 -> bool`;
 422 `E:(real^3->bool)->bool`;`w:real^3`;`u:real^3`] Fan.SIGMA_FAN));
 423 (ASM_SIMP_TAC[]);
 424 STRIP_TAC;
 425 (ASM_SIMP_TAC[ARITH_RULE `a >= b <=> b <= a`]);]);;
 426
 427
 428 (* FATUGPD *)
 429
 430 (* definitions in the proof *)
 431
 432 let set_of_iso = new_definition
 433 ` set_of_iso W = {w| w IN W /\ set_of_edge w W (ECTC W) = {}}`;;
 434
 435
 436 (* lemmas prepared for the proof *)
 437 let lemma1 = prove_by_refinement(
 438  `! (S:real^3->bool). packing S /\ S SUBSET ball_annulus ==> FINITE S`,
 439 [
 440 (REPEAT STRIP_TAC);
 441
 442 (* subgoal 1 *)
 443 (SUBGOAL_THEN ` (S:real^3->bool) = S INTER ball (vec 0,&3 * h0)` ASSUME_TAC);
 444
 445 (MATCH_MP_TAC (SET_RULE `! U V. U SUBSET ball_annulus /\ ball_annulus SUBSET V ==> (U = U INTER V)`));
 446 (ASM_SIMP_TAC[ball_annulus;ball;cball;IN_DIFF;SUBSET;IN_ELIM_THM;h0]);
 447 (REPEAT STRIP_TAC );
 448 (MATCH_MP_TAC (ARITH_RULE ` u <= &2 * #1.26 ==> u < &3 * #1.26`));
 449 (ASM_SIMP_TAC[]);
 450
 451 (ONCE_ASM_REWRITE_TAC[]);
 452 (ASM_SIMP_TAC[KIUMVTC]);]);;
 453
 454
 455 let lemma2 = prove_by_refinement(
 456  `! (V:real^3 -> bool) v. packing V /\ FINITE V /\ v IN V
 457 ==> ? epsilon. epsilon > &0 /\
 458   (! w. w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))
 459           ==> dist (v,w) > &2 + epsilon )`,
 460 [
 461 (REPEAT STRIP_TAC);
 462 (ABBREV_TAC `(S:real^3->bool) = {w|w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))}`);
 463
 464 (ASM_CASES_TAC `(S:real^3 ->bool) = {}`);
 465
 466 (* subgoal 1 *)
 467 (EXISTS_TAC `&1`);
 468 (SIMP_TAC[ARITH_RULE `&1 > &0`]);
 469 (REPEAT STRIP_TAC);
 470 (* subgoal 1.1 *)
 471 (SUBGOAL_THEN `~((S:real^3->bool) = {})` ASSUME_TAC);
 472 (ASM_SET_TAC[]);
 473
 474 (ASM_MESON_TAC[]);
 475
 476 (* subgoal 2 *)
 477
 478 (* subgoal 2.1 *)
 479 (SUBGOAL_THEN `FINITE (S:real^3 -> bool)` ASSUME_TAC);
 480 (MATCH_MP_TAC
 481   (ISPECL [`(S:real^3-> bool)`;`(V:real^3 ->bool)`] FINITE_SUBSET));
 482 (ASM_SET_TAC[]);
 483
 484 (ABBREV_TAC `(f:real^3 -> real) = (\w. dist (v,w))`);
 485 (* subgoal 2.2 *)
 486 (SUBGOAL_THEN `&2 < inf (IMAGE (f:real^3 -> real) (S:real^3 ->bool))`         ASSUME_TAC);
 487 (* subgoal 2.2.1 *)
 488 (SUBGOAL_THEN
 489   `FINITE (IMAGE (f:real^3 ->real) S) /\ ~ (IMAGE f S = {})` ASSUME_TAC);
 490 (ASM_SIMP_TAC[FINITE_IMAGE;NOT_EMPTY_IMAGE]);
 491
 492 (ASM_SIMP_TAC[REAL_LT_INF_FINITE]);
 493 (EXPAND_TAC "S");
 494 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
 495 (REPEAT STRIP_TAC);
 496 (ONCE_ASM_REWRITE_TAC[]);
 497 (EXPAND_TAC "f");
 498 (MATCH_MP_TAC (ARITH_RULE `! (a:real). &2 <= a /\ ~(&2 = a) ==> &2 < a`));
 499 CONJ_TAC;
 500 (* subgoal 2.2.3 *)
 501 (UNDISCH_TAC `packing (V:real^3 -> bool)`);
 502 (PURE_REWRITE_TAC[packing]);
 503 (DISCH_THEN (fun thm -> MATCH_MP_TAC (ISPECL [`x':real^3`;`v:real^3`] thm)));
 504 (ASM_MESON_TAC[IN]);
 505
 506 (* subgoal 2.2.4 *)
 507 (SUBGOAL_THEN `&2 = dist (v,x') ==> (x' IN set_of_edge v V (ECTC V))` ASSUME_TAC);
 508 (STRIP_TAC);
 509 (PURE_REWRITE_TAC[set_of_edge]);
 510 (ASM_SIMP_TAC[ECTC;IN_ELIM_THM]);
 511 (EXISTS_TAC `v:real^3`);
 512 (EXISTS_TAC `x':real^3`);
 513 (ASM_SIMP_TAC[]);
 514
 515 (ASM_MESON_TAC[]);
 516
 517 (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP epsilon_lemma)));
 518 (FIRST_X_ASSUM CHOOSE_TAC);
 519 (EXISTS_TAC `epsilon:real`);
 520 (ASM_SIMP_TAC[]);
 521 (REPEAT STRIP_TAC);
 522 (MATCH_MP_TAC (ARITH_RULE `! u:real v w. u >= v /\ v > w ==> u > w`));
 523 (EXISTS_TAC `inf (IMAGE (f:real^3 -> real) (S:real^3 -> bool))`);
 524 (ASM_SIMP_TAC[]);
 525
 526 (* subgoal 2.3 *)
 527 (SUBGOAL_THEN `dist (v,w:real^3) IN (IMAGE (f:real^3 -> real) S)` ASSUME_TAC);
 528 (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
 529 (EXISTS_TAC `w:real^3`);
 530 (CONJ_TAC);
 531
 532 (* subgoal 2.3.1 *)
 533 (EXPAND_TAC "S");
 534 (ASM_SIMP_TAC[IN_ELIM_THM]);
 535
 536 (* subgoal 2.3.2 *)
 537 (EXPAND_TAC "f");
 538 (SIMP_TAC[]);
 539
 540 (* subgoal 2.3.3 *)
 541 (SUBGOAL_THEN `~(IMAGE (f:real^3 -> real) S = {})
 542   /\ (? b:real. !x. x IN (IMAGE f S) ==> b <= x )` ASSUME_TAC);
 543 (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
 544 (EXISTS_TAC `&2`);
 545 STRIP_TAC;
 546 (EXPAND_TAC "f");
 547 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
 548 (REPEAT STRIP_TAC);
 549 (ONCE_ASM_REWRITE_TAC[]);
 550 (SIMP_TAC[]);
 551 (UNDISCH_TAC `packing (V:real^3 -> bool)`);
 552 (PURE_REWRITE_TAC[packing]);
 553 (DISCH_THEN (fun thm -> MP_TAC  (ISPECL [`v:real^3`;`x':real^3`] thm)));
 554 (MATCH_MP_TAC (TAUT `U ==> ((U ==> V)==> V) `));
 555
 556 (CONV_TAC (PAT_CONV `\x y. x /\ y /\ _ ` (ONCE_REWRITE_CONV[GSYM IN])));
 557 (ASM_SIMP_TAC[]);
 558 (UNDISCH_TAC `(x':real^3) IN S`);
 559 (EXPAND_TAC "S");
 560 (PURE_REWRITE_TAC[IN_ELIM_THM]);
 561 (SIMP_TAC[]);
 562
 563 (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP INF)));
 564 (ONCE_REWRITE_TAC[ARITH_RULE `a >= b <=> b <= a`]);
 565 (FIRST_X_ASSUM (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
 566 (ASM_SIMP_TAC[]); ]);;
 567
 568
 569 let lemma3 = prove_by_refinement(
 570  `! (w:real^3) (W:real^3 -> bool). packing W /\ w IN W /\
 571 ~(set_of_edge w W (ECTC W) = {}) /\ ~(surrounded_node (W,(ECTC W)) w)
 572 ==> ?u. (u IN set_of_edge w W (ECTC W)) /\ (azim_dart (W, (ECTC W)) (w,u) >= pi)`,
 573 [
 574 (PURE_REWRITE_TAC[surrounded_node]);
 575 (PURE_REWRITE_TAC[GSYM EXISTS_NOT_THM]);
 576 (PURE_REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`]);
 577 (PURE_REWRITE_TAC[ARITH_RULE `~ (a < pi) <=> a >= pi`]);
 578 (PURE_REWRITE_TAC[dart_of_fan]);
 579 (PURE_REWRITE_TAC[SET_RULE `x IN A UNION B <=> x IN A \/ x IN B`]);
 580 (SIMP_TAC[IN_ELIM_THM]);
 581 (REPEAT STRIP_TAC);
 582
 583 (* subgoal 1 *)
 584 (SUBGOAL_THEN `set_of_edge (w:real^3) (W:real^3 ->bool) (ECTC W) = {}` ASSUME_TAC);
 585 (FIRST_X_ASSUM (fun thm -> ALL_TAC));
 586 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
 587 (ASM_SIMP_TAC[]);
 588 (ASM_MESON_TAC[]);
 589
 590 (* subgoal 2 *)
 591 (EXISTS_TAC `SND (x:real^3 # real^3)`);
 592 (Q_LABEL_TAC `FST (x:real^3 # real^3) = w` "a");
 593 (USE_THEN "a" (fun thm -> SIMP_TAC[PAIR; GSYM thm]));
 594 (ASM_SIMP_TAC[]);
 595 (PURE_REWRITE_TAC[IN_ELIM_THM;set_of_edge]);
 596
 597 (* subgoal 2.1 *)
 598 (SUBGOAL_THEN `w:real^3 = v` (LABEL_TAC "b"));
 599 (REMOVE_THEN "a" (fun thm -> PURE_REWRITE_TAC[GSYM thm]));
 600 (ASM_SIMP_TAC[]);
 601 (ASM_SIMP_TAC[]);
 602 (UNDISCH_TAC `{v:real^3,w':real^3} IN ECTC (W:real^3 -> bool)`);
 603 (REWRITE_TAC[ECTC;IN_ELIM_THM;Geomdetail.PAIR_EQ_EXPAND]);
 604 (STRIP_TAC);
 605
 606 (* subgoal 2.2 *)
 607 (ASM_SIMP_TAC[]);
 608
 609 (* subgoal 2.3 *)
 610 (ASM_SIMP_TAC[]);]);;
 611
 612
 613
 614 let lemma4 = prove_by_refinement(
 615  `! w:real^3 u v.
 616          ~collinear {vec 0, w, u} /\ ~collinear {vec 0, w, v} /\
 617          azim (vec 0) w u v >= pi
 618   ==> (w cross u) dot v <= &0`,
 619 [
 620 (REPEAT STRIP_TAC);
 621 (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] JBDNJJB));
 622 (ASM_SIMP_TAC[]);
 623 STRIP_TAC;
 624 (ABBREV_TAC `(a:real) = ((w:real^3) cross u) dot v`);
 625 (MATCH_MP_TAC (SPECL [`t:real`;`a:real`;`&0`] REAL_LE_LCANCEL_IMP));
 626 (ASM_SIMP_TAC[]);
 627 (Q_LABEL_TAC `sin (azim (vec 0) w u v ) = t * a` "b");
 628 (USE_THEN "b" (fun thm -> (ONCE_REWRITE_TAC[GSYM thm; REAL_MUL_RZERO])));
 629
 630 (* subgoal 1 *)
 631 (SUBGOAL_THEN `azim (vec 0 :real^3) w u v < &2 * pi` ASSUME_TAC);
 632 (SIMP_TAC[SPECL [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`] azim]);
 633
 634 (ABBREV_TAC `b:real = azim (vec 0:real^3) w u v`);
 635 (ONCE_REWRITE_TAC[ARITH_RULE `m <= &0 <=> &0 <= -- m `]);
 636 (ONCE_REWRITE_TAC[GSYM SIN_NEG]);
 637 (ONCE_REWRITE_TAC[GSYM SIN_PERIODIC]);
 638
 639 (* subgoal 2 *)
 640 (SUBGOAL_THEN `-- pi < --b + &2 * pi /\ --b + &2 * pi <= pi` ASSUME_TAC);
 641 ASM_ARITH_TAC;
 642
 643 (ABBREV_TAC `c:real = --b + &2 * pi`);
 644 (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP SIN_NEGPOS_PI)));
 645 (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= x <=> x = &0 \/ &0 < x`]);
 646 (ONCE_ASM_REWRITE_TAC[]);
 647 (MATCH_MP_TAC (ARITH_RULE ` (&0 <= c /\ c <= pi) ==> ((c = &0 \/ c = pi) \/ &0 <  c /\ c < pi)`));
 648 (ASM_SIMP_TAC[]);
 649 (EXPAND_TAC "c");
 650 (MATCH_MP_TAC (ARITH_RULE `b < a ==> &0 <= --b + a`));
 651 (ASM_SIMP_TAC[]);]);;
 652
 653
 654 let lemma5 = prove_by_refinement(
 655  `! (V:real^3 -> bool) v. packing V /\ V SUBSET ball_annulus /\ v IN V
 656   ==> ! u. (u IN set_of_edge v V (ECTC V)) ==> v dot u > &0`,
 657 [
 658 (REPEAT STRIP_TAC);
 659 (* subgoal 1 *)
 660 (SUBGOAL_THEN `!(w:real^3). w IN V ==> w dot w >= &4` (LABEL_TAC "a"));
 661 (REPEAT STRIP_TAC);
 662 (MP_TAC (SET_RULE `(w:real^3) IN V /\ V SUBSET ball_annulus ==> w IN ball_annulus`));
 663 (ASM_SIMP_TAC[]);
 664 (PURE_REWRITE_TAC[ball_annulus]);
 665 (PURE_REWRITE_TAC[DIFF;ball;IN_ELIM_THM]);
 666 (PURE_REWRITE_TAC[REAL_ARITH `~(a < &2) <=> a >= &2`]);
 667 (PURE_REWRITE_TAC[dist; DIST_SYM;VECTOR_SUB_RZERO]);
 668 (PURE_REWRITE_TAC[NORM_GE_SQUARE]);
 669
 670 (SIMP_TAC[ARITH_RULE `~(&2 <= &0) /\ &2 pow 2 = &4`]);
 671 (MATCH_MP_TAC (ARITH_RULE `&2 * a > &0 ==> a > &0`));
 672 (ONCE_REWRITE_TAC[VECTOR_ARITH `&2 * (v dot u) = v dot v + u dot u - (v - u) dot (v - u)`]);
 673
 674 (* subgoal 2 *)
 675 (SUBGOAL_THEN `(v:real^3 - u) dot (v - u) = &4 /\ u IN V` MP_TAC);
 676 (UNDISCH_TAC `u:real^3 IN set_of_edge v V (ECTC V)`);
 677 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
 678 STRIP_TAC;
 679 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
 680 (ONCE_REWRITE_TAC[GSYM dist]);
 681 (FIRST_ASSUM (MP_TAC o (MATCH_MP (fst (EQ_IMP_RULE Geomdetail.PAIR_EQ_EXPAND)))));
 682 (REPEAT STRIP_TAC);
 683
 684 (* subgoal 2.1 *)
 685 (ASM_SIMP_TAC[]);
 686 ARITH_TAC;
 687 (* subgoal 2.2 *)
 688 (ONCE_REWRITE_TAC[DIST_SYM]);
 689 (ASM_SIMP_TAC[]);
 690 ARITH_TAC;
 691
 692 (STRIP_TAC);
 693 (ASM_SIMP_TAC[]);
 694 (MATCH_MP_TAC (ARITH_RULE `a >= &4 /\ b >= &4 ==> a + b - &4 > &0`));
 695 (USE_THEN "a" (fun thm -> MP_TAC( SPEC `v:real^3` thm)));
 696 (USE_THEN "a" (fun thm -> MP_TAC( SPEC `u:real^3` thm)));
 697 (ASM_SIMP_TAC[]);]);;
 698
 699
 700 let lemma6 = prove_by_refinement(
 701  `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\
 702  orthonormal e1 e2 e3 /\
 703  u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
 704 ==> norm u = norm v`,
 705 [
 706 (REPEAT STRIP_TAC);
 707 (* subgoal 1 *)
 708 (SUBGOAL_THEN `orthonormal e1 e2 e3 /\
 709  u:real^3 = (cos (phi:real) * norm (v:real^3)) % e1 + (sin phi * norm v) % e2 + &0 % e3` ASSUME_TAC);
 710 (ASM_SIMP_TAC[]);
 711 VECTOR_ARITH_TAC;
 712
 713 (FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP (SPECL [`u:real^3`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
 714 ` cos (phi:real) * norm (v:real^3)`;`sin (phi:real) * norm (v:real^3)`;`&0`]
 715 norm_lemma2)));
 716 (ONCE_ASM_REWRITE_TAC[]);
 717 (ONCE_REWRITE_TAC[ARITH_RULE `( a * m) pow 2 + (b * m) pow 2 + &0 pow 2
 718 = (b pow 2 + a pow 2) * m pow 2`]);
 719 (SIMP_TAC[SIN_CIRCLE;REAL_MUL_LID]);
 720 (MATCH_MP_TAC POW_2_SQRT);
 721 (SIMP_TAC[NORM_POS_LE]);]);;
 722
 723
 724 let lemma7 = prove_by_refinement(
 725  `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\
 726  orthonormal e1 e2 e3 /\ &0 < phi /\ phi < pi /\ &0 < norm v  /\
 727  u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
 728 ==> (! w:real^3. &0 < w dot e1  /\ w dot e2 <= &0
 729      ==> dist (v,w) < dist (u,w))`,
 730 [
 731 (REPEAT STRIP_TAC);
 732 (PURE_REWRITE_TAC[dist;NORM_LT]);
 733 (ONCE_REWRITE_TAC[ARITH_RULE `a < b <=> &0 < b - a `]);
 734 (ONCE_REWRITE_TAC[VECTOR_ARITH `(u - w) dot (u - w) - (v - w) dot (v - w) =
 735  u dot u - v dot v - &2 * ((u - v) dot w )`]);
 736 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
 737
 738 (* subgoal 1 *)
 739 (SUBGOAL_THEN `norm (u:real^3) = norm (v:real^3)` ASSUME_TAC);
 740 (MATCH_MP_TAC (SPECL [`v:real^3`;`u:real^3`;`phi:real`; `e1:real^3`;
 741 `e2:real^3`;`e3:real^3`] lemma6));
 742 (ASM_SIMP_TAC[]);
 743
 744 (FIRST_ASSUM (fun thm -> SIMP_TAC[thm; ARITH_RULE `a - a - b = --b`]));
 745 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < --(&2 * a) <=> a < &0`]);
 746
 747 (* subgoal 2 *)
 748 (SUBGOAL_THEN `v:real^3 = (norm v) % e1` (LABEL_TAC "v_coordinate"));
 749 (ASM_SIMP_TAC[norm_mul_normalize]);
 750
 751 (Q_LABEL_TAC `orthonormal e1 e2 e3` "base");
 752 (USE_THEN "base" (ASSUME_TAC o MATCH_MP (SPECL [`(u - v):real^3`;`w:real^3`;
 753 `e1:real^3`;`e2:real^3`;`e3:real^3`] dot_coordinates)));
 754 (ONCE_ASM_REWRITE_TAC[]);
 755
 756 (* subgoal 3 *)
 757 (SUBGOAL_THEN `(u:real^3 - v) dot e1 = (cos phi - &1) * norm v /\
 758 (u - v) dot e2 = sin phi * norm v /\ (u - v) dot e3 = &0` MP_TAC);
 759 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 760 (MATCH_MP_TAC (SPECL [`u:real^3 - v`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
 761 `(cos phi - &1) * norm v`;`sin phi * norm v`;`&0`] coordinates_lemma));
 762 (USE_THEN "base" (fun thm -> SIMP_TAC[thm]));
 763 (USE_THEN "v_coordinate" (fun thm -> CONV_TAC( PAT_CONV
 764 `\x. U - x = _` (ONCE_REWRITE_CONV[thm]))));
 765 (Q_LABEL_TAC `u:real^3 = (cos phi * norm (v:real^3)) % e1 + (sin phi * norm v) % e2` "u");
 766 (USE_THEN "u" (fun thm -> ONCE_REWRITE_TAC[thm]));
 767 (VECTOR_ARITH_TAC);
 768 (DISCH_THEN (LABEL_TAC "c"));
 769 (USE_THEN "c" (fun thm -> ONCE_REWRITE_TAC[thm]));
 770 (PURE_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_RID]);
 771 (MATCH_MP_TAC (REAL_ARITH `a < &0 /\ b <= &0 ==> a + b < &0`));
 772 CONJ_TAC;
 773
 774 (* subgoal 4 *)
 775 (ONCE_REWRITE_TAC[REAL_ARITH
 776 `((a - &1) * b) * c < &0 <=> &0 < ((&1 - a) * b) * c`]);
 777 (MATCH_MP_TAC REAL_LT_MUL);
 778 (ASM_SIMP_TAC[]);
 779 (MATCH_MP_TAC REAL_LT_MUL);
 780 (ASM_SIMP_TAC[]);
 781 (ONCE_REWRITE_TAC[REAL_ARITH
 782 `&0 < &1 - a <=> (a <= &1 /\ ~(a = &1))`]);
 783 (SIMP_TAC[COS_BOUNDS;COS_ONE_2PI]);
 784 (ONCE_REWRITE_TAC[ TAUT `~(A \/ B) <=> ~A /\ ~B`]);
 785 (STRIP_TAC);
 786
 787 (* subgoal 4.1 *)
 788 (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
 789 (STRIP_TAC);
 790 (FIRST_X_ASSUM(LABEL_TAC "phi"));
 791
 792
 793 (* subgoal 4.1.1 *)
 794 (SUBGOAL_THEN `0 < n:num` ASSUME_TAC);
 795 (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
 796 (MATCH_MP_TAC (SPECL [`&0`;`&(n:num)`;`&2 * pi`]
 797 REAL_LT_RCANCEL_IMP));
 798 (SIMP_TAC[ARITH_RULE `&0 * &2 * pi = &0`;
 799 ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
 800 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
 801 (ASM_SIMP_TAC[PI_POS]);
 802
 803 (* subgoal 4.1.2 *)
 804 (SUBGOAL_THEN `n:num < 1` ASSUME_TAC);
 805 (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
 806 (MATCH_MP_TAC (SPECL [`&(n:num)`;`&1`;`&2 * pi`]
 807 REAL_LT_RCANCEL_IMP));
 808 (SIMP_TAC[ARITH_RULE `&1 * &2 * pi = &2 * pi`;
 809 ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
 810 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
 811 (SIMP_TAC[PI_POS]);
 812 (MATCH_MP_TAC(ARITH_RULE `a < pi /\ pi < b ==> a < b`));
 813 (ASM_SIMP_TAC[]);
 814 (MATCH_MP_TAC(ARITH_RULE `&0 < a ==> a < &2 * a`));
 815 (SIMP_TAC[PI_POS]);
 816 (ASM_MESON_TAC[ARITH_RULE `~(0 < n:num /\ n < 1)`]);
 817
 818 (* subgoal 4.2 *)
 819 (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
 820 (STRIP_TAC);
 821 (FIRST_X_ASSUM(LABEL_TAC "phi"));
 822 (* subgoal 4.2.1 *)
 823 (SUBGOAL_THEN `~(&0 < phi:real)` ASSUME_TAC);
 824 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[thm]));
 825 (ONCE_REWRITE_TAC[ARITH_RULE `~(&0 < -- a) <=> &0 <= a`]);
 826 (MATCH_MP_TAC REAL_LE_MUL);
 827 (SIMP_TAC[REAL_POS]);
 828 (MATCH_MP_TAC (ARITH_RULE `&0 < a ==> &0 <= a`));
 829 (MATCH_MP_TAC REAL_LT_MUL);
 830 (SIMP_TAC[PI_POS]);
 831 ARITH_TAC;
 832 (ASM_MESON_TAC[]);
 833
 834 (* subgoal 5 *)
 835 (ONCE_REWRITE_TAC[ARITH_RULE `a * b <= &0 <=> &0 <= a * (--b)`]);
 836 (MATCH_MP_TAC REAL_LE_MUL);
 837 (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= -- a <=> a <= &0`]);
 838 (ASM_SIMP_TAC[]);
 839 (MATCH_MP_TAC REAL_LE_MUL);
 840 (SIMP_TAC[NORM_POS_LE]);
 841 (MATCH_MP_TAC SIN_POS_PI_LE);
 842 (ASM_ARITH_TAC);]);;
 843
 844
 845 let lemma8 = prove_by_refinement(
 846 `! w:real^3 W:real^3->bool. w IN W
 847 ==> set_of_edge w W (ECTC W) = {v| v IN W /\ dist (w,v) = &2}`,
 848 [
 849 (REPEAT STRIP_TAC);
 850 (MATCH_MP_TAC SUBSET_ANTISYM);
 851 CONJ_TAC;
 852
 853 (* subgoal 1 *)
 854 (PURE_REWRITE_TAC[SUBSET]);
 855 (GEN_TAC);
 856 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
 857 (STRIP_TAC);
 858 (SUBGOAL_THEN `dist (w:real^3,x) = dist (v:real^3,w'')` ASSUME_TAC);
 859 (MATCH_MP_TAC Geomdetail.DIST_PAIR_LEMMA);
 860 (ASM_SIMP_TAC[]);
 861 (ASM_ARITH_TAC);
 862
 863 (* subgoal 2 *)
 864 (PURE_REWRITE_TAC[SUBSET]);
 865 (GEN_TAC);
 866 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
 867 (STRIP_TAC);
 868 (EXISTS_TAC `w:real^3`);
 869 (EXISTS_TAC `x:real^3`);
 870 (ASM_SIMP_TAC[]);
 871 (ONCE_REWRITE_TAC[DIST_NZ]);
 872 (ASM_ARITH_TAC);]);;
 873
 874
 875 (* main proof *)
 876
 877 let FATUGPD_quasi =  prove_by_refinement( ` UBHDEUU2_hypothesis ==> (!V. packing V /\ V SUBSET ball_annulus
 878 ==> (?W phi.  BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\
 879         (!w. w IN W ==>  (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w))))`,
 880 [
 881 DISCH_TAC;
 882 GEN_TAC;
 883 STRIP_TAC;
 884 (ABBREV_TAC
 885    `S = {(U:real^3->bool)| FINITE U /\ packing U /\
 886          (?phi. BIJ phi (V:real^3->bool) U /\
 887                    (! v. v IN V ==> norm v = norm (phi v)))}`);
 888 (ABBREV_TAC
 889    `(f:(real^3 ->bool)->num) =
 890      (\U. CARD (set_of_iso U))`);
 891
 892 (* subgoal 1 *)
 893 (SUBGOAL_THEN `FINITE (V:real^3->bool)` (LABEL_TAC "finite_v"));
 894 (ASM_SIMP_TAC[lemma1]);
 895
 896 (* subgoal 2 *)
 897 (SUBGOAL_THEN `! (U:real^3 ->bool). U IN S ==> FINITE U` (LABEL_TAC "finite_u"));
 898 (EXPAND_TAC "S");
 899 (SIMP_TAC[IN_ELIM_THM]);
 900
 901 (* subgoal 3 *)
 902 (SUBGOAL_THEN
 903  `~ ((S:(real^3->bool)->bool) = {}) /\
 904     (?m. !U. U IN S ==> (f:(real^3->bool)->num) U <= m)` (LABEL_TAC "asm1"));
 905 CONJ_TAC;
 906
 907 (* subgoal 3.1 *)
 908 (PURE_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]);
 909 (EXISTS_TAC `V:real^3->bool`);
 910 (EXPAND_TAC "S");
 911 (ASM_SIMP_TAC[IN_ELIM_THM]);
 912 (EXISTS_TAC `(I:real^3->real^3)`);
 913 CONJ_TAC;
 914
 915 (* subgoal 3.1.1 *)
 916 (SIMP_TAC[BIJ;INJ;SURJ;I_THM]);
 917 (SET_TAC[]);
 918
 919 (* subgoal 3.1.2 *)
 920 (SIMP_TAC[I_THM]);
 921
 922 (* subgoal 3.2 *)
 923 (EXISTS_TAC `CARD (V:real^3->bool)`);
 924 (GEN_TAC);
 925
 926 (* subgoal 3.2.1 *)
 927 (SUBGOAL_THEN `! (U:real^3->bool). U IN S ==> CARD U = CARD (V:real^3->bool)` MP_TAC);
 928 (GEN_TAC);
 929 (EXPAND_TAC "S");
 930 (PURE_REWRITE_TAC[IN_ELIM_THM]);
 931 STRIP_TAC;
 932 (MATCH_MP_TAC BIJ_CARD_EQ);
 933 (EXISTS_TAC `phi:real^3->real^3`);
 934 (ASM_SIMP_TAC[]);
 935
 936 (DISCH_THEN (MP_TAC o (fun thm -> (SPEC `U:real^3 ->bool` thm))));
 937 (MATCH_MP_TAC (TAUT ` (p ==> (q ==> r)) ==> ((p ==> q) ==> (p ==> r))`));
 938 (REPEAT STRIP_TAC);
 939
 940 (* subgoal 3.2.2 *)
 941 (SUBGOAL_THEN  `(f:(real^3->bool) -> num) U <= CARD U` ASSUME_TAC);
 942 (EXPAND_TAC "f");
 943 (MATCH_MP_TAC CARD_SUBSET);
 944 CONJ_TAC;
 945
 946 (* subgoal 3.2.2.1 *)
 947 (SET_TAC[set_of_iso]);
 948
 949 (* subgoal 3.2.2.2 *)
 950 (UNDISCH_TAC `(U:real^3->bool) IN (S:(real^3->bool)->bool)`);
 951 (ASM_SIMP_TAC[]);
 952
 953 ASM_ARITH_TAC;
 954
 955 (REMOVE_THEN "asm1" (ASSUME_TAC o (MATCH_MP bdd_num_func_attain_max)));
 956 (FIRST_X_ASSUM CHOOSE_TAC);
 957 (EXISTS_TAC `U:real^3->bool`);
 958
 959 (FIRST_X_ASSUM MP_TAC);
 960 (STRIP_TAC);
 961 (UNDISCH_TAC `U:real^3 -> bool IN S`);
 962 (EXPAND_TAC "S");
 963 (SIMP_TAC[IN_ELIM_THM]);
 964 (REPEAT STRIP_TAC);
 965 (EXISTS_TAC `phi:real^3 ->real^3`);
 966 (ASM_SIMP_TAC[]);
 967 (REPEAT STRIP_TAC);
 968
 969 (* subgoal 4 *)
 970 (SUBGOAL_THEN `! v:real^3. v IN U ==> norm v <= &2 * h0 /\ ~(norm v < &2)`
 971 (LABEL_TAC "norm_bdd"));
 972 GEN_TAC;
 973 (UNDISCH_TAC `BIJ phi (V:real^3->bool) (U:real^3->bool)`);
 974 (PURE_REWRITE_TAC[BIJ;SURJ]);
 975 ( STRIP_TAC);
 976 (STRIP_TAC);
 977 (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` thm)));
 978 (FIRST_ASSUM (fun thm -> SIMP_TAC[thm]));
 979 STRIP_TAC;
 980 (UNDISCH_TAC `! v:real^3. v IN V ==> norm v = norm ((phi:real^3 -> real^3) v)`);
 981 (DISCH_THEN (fun thm -> MP_TAC (SPEC `y:real^3` thm)));
 982 (ASM_SIMP_TAC[]);
 983 (MATCH_MP_TAC (ARITH_RULE
 984 `a <= &2 * h0 /\ ~(a < &2) ==> a = b ==> b <= &2 * h0 /\ ~(b < &2)`));
 985
 986 (* subgoal 4.1 *)
 987 (SUBGOAL_THEN `y:real^3 IN ball_annulus` MP_TAC);
 988 (MATCH_MP_TAC (SET_RULE `y:real^3 IN V /\ V SUBSET ball_annulus ==> y IN ball_annulus`));
 989 (ASM_SIMP_TAC[]);
 990
 991 (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
 992 (SIMP_TAC[DIST_0]);
 993
 994 (* subgoal 5 *)
 995 (SUBGOAL_THEN `(U:real^3 -> bool) SUBSET ball_annulus` (LABEL_TAC "u_annu"));
 996 (PURE_REWRITE_TAC[SUBSET]);
 997 GEN_TAC;
 998 STRIP_TAC;
 999 (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
1000 (SIMP_TAC[DIST_0]);
1001 (ASM_SIMP_TAC[]);
1002
1003 (* subgoal 6 *)
1004 (SUBGOAL_THEN `! v:real^3. v IN U ==> ~(v = vec 0)` (LABEL_TAC "not_0"));
1005 (GEN_TAC);
1006 STRIP_TAC;
1007 (ONCE_REWRITE_TAC[GSYM NORM_POS_LT]);
1008 (MATCH_MP_TAC (ARITH_RULE `~(norm (v:real^3) < &2) ==> &0 < norm v`));
1009 (ASM_SIMP_TAC[]);
1010
1011 (* subgoal 7 *)
1012 (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U)
1013   ==> ~(collinear {vec 0, w, v})` (LABEL_TAC "not_li"));
1014 (GEN_TAC);
1015 (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1016 (ASM_SIMP_TAC[]);
1017 (SIMP_TAC[IN_ELIM_THM;ECTC]);
1018 (MATCH_MP_TAC (TAUT `(B ==> C) ==> (A ==> B ==> C)`));
1019 STRIP_TAC;
1020 (ONCE_REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);
1021 (ONCE_REWRITE_TAC[TAUT `~(A \/ B \/ C) <=> ~A /\ ~B /\ ~C`]);
1022 (ONCE_REWRITE_TAC[between]);
1023 (ONCE_REWRITE_TAC[DIST_0]);
1024 (CONV_TAC (PAT_CONV `\x. A /\ ~( _ = x + _ ) /\ ~( _ = _ + x)`
1025 (ONCE_REWRITE_CONV[DIST_SYM])));
1026 (ASM_SIMP_TAC[]);
1027 (MATCH_MP_TAC (ARITH_RULE
1028 `(a <= &2 * #1.26) /\ ~(a < &2) /\ (b <= &2 * #1.26) /\ ~(b < &2)
1029 ==> ~(&2 = a + b) /\ ~(b = &2 + a) /\ ~(a = b + &2)`));
1030 (ONCE_REWRITE_TAC[GSYM h0]);
1031 (ASM_SIMP_TAC[]);
1032
1033 (ASM_CASES_TAC `~(set_of_edge (w:real^3) (U:real^3->bool) (ECTC U) = {}) /\
1034   ~(surrounded_node (U,ECTC U) w)`);
1035
1036 (ABBREV_TAC `result:bool = (set_of_edge w U (ECTC U) = {} \/ surrounded_node (U,ECTC U) w)`);
1037 (MP_TAC (SPECL [`U:real^3 -> bool`;`w:real^3`] lemma2));
1038 (ASM_SIMP_TAC[]);
1039 (STRIP_TAC);
1040 (MP_TAC (SPECL[`w:real^3`;`U:real^3->bool`] lemma3));
1041 (ASM_SIMP_TAC[]);
1042 (STRIP_TAC);
1043 (Q_ABBREV_TAC `e1:real^3 = normalize w` "e1");
1044 (Q_ABBREV_TAC `y:real^3 = w cross u` "y_axis");
1045 (Q_ABBREV_TAC `e2:real^3 = normalize y` "e2");
1046 (Q_ABBREV_TAC `e3:real^3 = e1 cross e2` "e3");
1047
1048 (* subgoal 8 *)
1049 (SUBGOAL_THEN `orthonormal (e1:real^3) e2 e3` ASSUME_TAC);
1050 (PURE_REWRITE_TAC[orthonormal]);
1051 (ONCE_REWRITE_TAC[GSYM NORM_EQ_1]);
1052 (* subgoal 8.1 *)
1053 (SUBGOAL_THEN `norm (e1:real^3) = &1` ASSUME_TAC);
1054 (Q_EXPAND_TAC "e1");
1055 (MATCH_MP_TAC norm_normalize);
1056 (ASM_SIMP_TAC[]);
1057
1058 (* subgoal 8.2 *)
1059 (SUBGOAL_THEN `norm (e2:real^3) = &1` ASSUME_TAC);
1060 (Q_EXPAND_TAC "e2");
1061 (MATCH_MP_TAC norm_normalize);
1062 (Q_EXPAND_TAC "y_axis");
1063 (ONCE_REWRITE_TAC[CROSS_EQ_0]);
1064 (ASM_SIMP_TAC[]);
1065
1066 (* subgoal 8.3 *)
1067 (SUBGOAL_THEN `(e1:real^3) dot e2 = &0` ASSUME_TAC);
1068 (Q_EXPAND_TAC "e1");
1069 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1070 (Q_EXPAND_TAC "e2");
1071 (ONCE_REWRITE_TAC[DOT_SYM]);
1072 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1073 (Q_EXPAND_TAC "y_axis");
1074 (SIMP_TAC[DOT_CROSS_SELF]);
1075
1076 (* subgoal 8.4 *)
1077 (SUBGOAL_THEN `(e1:real^3) dot e3 = &0 /\ e2 dot e3 = &0` ASSUME_TAC);
1078 (Q_EXPAND_TAC "e3");
1079 (SIMP_TAC[DOT_CROSS_SELF]);
1080
1081 (* subgoal 8.5 *)
1082 (SUBGOAL_THEN `norm (e3:real^3) = &1` ASSUME_TAC);
1083 (Q_EXPAND_TAC "e3");
1084 (MP_TAC(ISPECL [`e1:real^3`;`e2:real^3`] NORM_CROSS_DOT));
1085 (ASM_SIMP_TAC[REAL_POW_2;REAL_MUL_RZERO;REAL_ADD_RID;REAL_MUL_RID]);
1086 (ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
1087 (STRIP_TAC);
1088 (MP_TAC(SPECL [`norm (e3:real^3)`;`2`] REAL_POW_EQ_1_IMP));
1089 (ASM_SIMP_TAC[ARITH_RULE `~(2 = 0)`]);
1090 (STRIP_TAC);
1091 (MATCH_MP_TAC (ARITH_RULE `abs x = &1 /\ &0 <= x  ==> x = &1`));
1092 (ASM_SIMP_TAC[NORM_POS_LE]);
1093
1094 (ASM_SIMP_TAC[]);
1095 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
1096 (ASM_SIMP_TAC[REAL_POW_2]);
1097 ARITH_TAC;
1098
1099 (* subgoal 9 *)
1100 (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U)
1101   ==> v dot e2 <= &0` ASSUME_TAC);
1102 (GEN_TAC);
1103 (STRIP_TAC);
1104 (ONCE_REWRITE_TAC[DOT_SYM]);
1105 (ONCE_REWRITE_TAC[ARITH_RULE `a <= &0 <=> &0 < --a \/ a = &0`]);
1106 (ONCE_REWRITE_TAC[VECTOR_ARITH `--((e2:real^3) dot v) = (--v) dot e2`]);
1107 (Q_EXPAND_TAC "e2");
1108 (ONCE_REWRITE_TAC[GSYM dot_gt_0]);
1109 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1110 (ONCE_REWRITE_TAC[VECTOR_ARITH ` --(v:real^3) dot y = -- (y dot v)`]);
1111 (ONCE_REWRITE_TAC[ARITH_RULE ` (&0 < --a \/ a = &0 )<=> a <= &0`]);
1112 (Q_EXPAND_TAC "y_axis");
1113 (ASM_CASES_TAC `v:real^3 = u`);
1114
1115 (* subgoal 9.1 *)
1116 (FIRST_ASSUM(fun thm -> SIMP_TAC[thm;DOT_CROSS_SELF]));
1117  ARITH_TAC;
1118
1119 (* subgoal 9.2 *)
1120 (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] lemma4));
1121 (ASM_SIMP_TAC[]);
1122 (MATCH_MP_TAC (TAUT `A ==> (A ==>B) ==> B`));
1123 (MP_TAC (SPEC `U:real^3 -> bool` UBHDEUU2_quasi));
1124 (ASM_SIMP_TAC[]);
1125 (DISCH_TAC);
1126 (MP_TAC (SPECL [`U:real^3->bool`;`(ECTC U):(real^3->bool)->bool`;`w:real^3`;
1127 `u:real^3`;`v:real^3`] azim_ge_azim_dart));
1128 (ASM_SIMP_TAC[]);
1129
1130 (* subgoal 9.2.1 *)
1131 (SUBGOAL_THEN `~(w:real^3 = u)` ASSUME_TAC);
1132 (UNDISCH_TAC `u:real^3 IN set_of_edge w U (ECTC U)`);
1133 (MP_TAC(SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1134 (ASM_SIMP_TAC[IN_ELIM_THM]);
1135 (STRIP_TAC);
1136 (STRIP_TAC);
1137 (ONCE_REWRITE_TAC[GSYM DIST_EQ_0]);
1138 (ASM_ARITH_TAC);
1139
1140 (ASM_SIMP_TAC[]);
1141 (ASM_ARITH_TAC);
1142
1143 (* subgoal 10 *)
1144 (SUBGOAL_THEN `?(a:real). &0 < a /\ a < pi /\
1145  (&2 - &2 * cos a ) * ( norm (w:real^3) pow 2) < epsilon pow 2` ASSUME_TAC);
1146 (MP_TAC (SPEC `&0` REAL_CONTINUOUS_AT_COS));
1147 (ONCE_REWRITE_TAC[real_continuous_atreal]);
1148 (DISCH_THEN (MP_TAC o (SPEC
1149 `epsilon pow 2 / (&2 * norm(w:real^3) pow 2)`)));
1150
1151 (* subgoal 10.1 *)
1152 (SUBGOAL_THEN
1153 `&0 < epsilon pow 2/ (&2 * norm (w:real^3) pow 2)` ASSUME_TAC);
1154 (MATCH_MP_TAC REAL_LT_DIV);
1155 (CONJ_TAC);
1156
1157 (* subgoal 10.1.1 *)
1158 (MATCH_MP_TAC REAL_POW_LT);
1159 (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1160
1161 (* subgoal 10.1.2 *)
1162 (MATCH_MP_TAC (ARITH_RULE ` &0 < a ==> &0 < &2 * a`));
1163 (MATCH_MP_TAC REAL_POW_LT);
1164 (ASM_SIMP_TAC[NORM_POS_LT]);
1165
1166 (ASM_SIMP_TAC[COS_0;REAL_MUL_RID;REAL_SUB_RZERO]);
1167 (DISCH_THEN CHOOSE_TAC);
1168 (FIRST_X_ASSUM MP_TAC);
1169 STRIP_TAC;
1170 (Q_ABBREV_TAC `m:real = min (d / &2) (pi / &2)` "phi");
1171 (EXISTS_TAC `m:real`);
1172  (* subgoal 10.2 *)
1173 (SUBGOAL_THEN `&0 < m:real` ASSUME_TAC);
1174 (Q_EXPAND_TAC "phi");
1175 (SIMP_TAC[REAL_LT_MIN;PI2_BOUNDS]);
1176 (MATCH_MP_TAC REAL_LT_DIV);
1177 (ASM_ARITH_TAC);
1178
1179 (* subgoal 10.3 *)
1180 (SUBGOAL_THEN `m < pi` ASSUME_TAC);
1181 (Q_EXPAND_TAC "phi");
1182 (ONCE_REWRITE_TAC[REAL_MIN_LT]);
1183 (DISJ2_TAC);
1184 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> a / &2 < a`));
1185 (SIMP_TAC[PI_POS]);
1186
1187 (ASM_SIMP_TAC[]);
1188 (ONCE_REWRITE_TAC [REAL_ARITH `(&2 - &2 * a) * b = (&1 - a) * (&2 * b)`]);
1189 (MP_TAC (SPECL [`&1 - cos (m:real)`;`epsilon:real pow 2`;
1190 `&2 * norm (w:real^3) pow 2`] REAL_LT_RDIV_EQ));
1191
1192 (* subgoal 10.4 *)
1193 (SUBGOAL_THEN `&0 < &2 * norm (w:real^3) pow 2` ASSUME_TAC);
1194 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
1195 (MATCH_MP_TAC REAL_POW_LT);
1196 (ASM_SIMP_TAC[NORM_POS_LT]);
1197
1198 (ASM_SIMP_TAC[]);
1199 (MATCH_MP_TAC (TAUT `A ==> (A <=> B ) ==> B`));
1200 (MATCH_MP_TAC (REAL_ARITH `abs a < b ==> a < b`));
1201 (ONCE_REWRITE_TAC[REAL_ARITH `abs (a - b) = abs (b - a)`]);
1202 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1203
1204 (* subgoal 10.5 *)
1205 (SUBGOAL_THEN `abs (m:real) = m` ASSUME_TAC);
1206 (ONCE_REWRITE_TAC[REAL_ABS_REFL]);
1207 (ASM_ARITH_TAC);
1208 (ASM_SIMP_TAC[]);
1209 (Q_EXPAND_TAC "phi");
1210 (ONCE_REWRITE_TAC[REAL_MIN_LT]);
1211 (DISJ1_TAC);
1212  ASM_ARITH_TAC;
1213
1214 (FIRST_X_ASSUM CHOOSE_TAC);
1215 (Q_ABBREV_TAC `s:real^3 =
1216   (cos a * norm (w:real^3)) % e1 + (sin a * norm w) % e2` "subs_point");
1217 (Q_ABBREV_TAC `U':real^3 -> bool = s INSERT (U DELETE w)` "new_set");
1218
1219 (* subgoal 11 *)
1220 (SUBGOAL_THEN `!(v:real^3). v IN U /\ ~(v = w) ==> &2 < dist (s,v)`
1221 (LABEL_TAC "dist_gt_2"));
1222 (GEN_TAC);
1223 (STRIP_TAC);
1224 (ASM_CASES_TAC  `(v:real^3) IN set_of_edge w U (ECTC U)`);
1225
1226 (* subgoal 11.1 *)
1227 (SUBGOAL_THEN `dist ((w:real^3),v) = &2` ASSUME_TAC);
1228 (FIRST_X_ASSUM MP_TAC);
1229 (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1230 (ASM_SIMP_TAC[]);
1231 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1232 (SIMP_TAC[IN_ELIM_THM]);
1233
1234 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1235 (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
1236 `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma7));
1237 (ASM_SIMP_TAC[NORM_POS_LT]);
1238 (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPEC `v:real^3` thm)));
1239 (ASM_SIMP_TAC[]);
1240 (Q_EXPAND_TAC "e1");
1241 (ONCE_REWRITE_TAC[GSYM dot_gt_0]);
1242 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1243 (ONCE_REWRITE_TAC[DOT_SYM]);
1244 (MP_TAC (SPECL [`U:real^3->bool`;`w:real^3`] lemma5));
1245 (ASM_SIMP_TAC[]);
1246
1247 (* subgoal 11.2 *)
1248 (ONCE_REWRITE_TAC[DIST_SYM]);
1249 (MATCH_MP_TAC (REAL_ARITH `&2 < dist (v:real^3,w) - dist (s,w) /\
1250 dist (v,w) - dist (s,w) <= a ==> &2 < a`));
1251 (SIMP_TAC[Pack1.real_sub_norm]);
1252 (MATCH_MP_TAC (REAL_ARITH
1253 `a > &2 + (epsilon:real) /\ b < epsilon ==>  &2 < a - b`));
1254 (ONCE_REWRITE_TAC[DIST_SYM]);
1255 (ASM_SIMP_TAC[]);
1256 (ONCE_REWRITE_TAC[DIST_SYM]);
1257 (PURE_REWRITE_TAC[dist]);
1258 (ONCE_REWRITE_TAC[NORM_LT_SQUARE]);
1259 (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1260
1261 (* subgoal 11.2.1 *)
1262 (SUBGOAL_THEN `s:real^3 - w = ((cos (a:real) - &1) * norm (w:real^3)) % e1 +
1263 (sin a * norm w) % e2 + &0 % e3` ASSUME_TAC);
1264 (* subgoal 11.2.1.1 *)
1265 (SUBGOAL_THEN `w:real^3 = norm w % e1` ASSUME_TAC);
1266 (Q_EXPAND_TAC "e1");
1267 (SIMP_TAC[norm_mul_normalize]);
1268
1269 (FIRST_X_ASSUM(fun thm -> CONV_TAC(PAT_CONV `\x. s - x = A`
1270 (ONCE_REWRITE_CONV[thm]))));
1271 (Q_EXPAND_TAC "subs_point");
1272 (SIMP_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_RID]);
1273 (ONCE_REWRITE_TAC[VECTOR_ARITH
1274 `(a % (e1:real^3) + b % e2) - c % e1 = (a - c) % e1 + b % e2`]);
1275 (SIMP_TAC[ARITH_RULE `a * b - b = (a - &1) * b`]);
1276 (MP_TAC (SPECL
1277 [`s:real^3 - w`;`s:real^3 - w`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
1278 `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
1279 `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`]
1280 dot_coordinates_2));
1281 (ASM_SIMP_TAC[]);
1282 (MATCH_MP_TAC (TAUT `B ==> A ==> B`));
1283 (ONCE_REWRITE_TAC [REAL_ARITH
1284 `(a * b) * a * b + (c * b) * c * b + &0 * &0 = (a * a + c * c) * b pow 2`]);
1285 (ONCE_REWRITE_TAC [REAL_ARITH
1286 `(a - &1) * (a - &1) + b * b = &1 - &2 * a + b pow 2 + a pow 2`]);
1287 (SIMP_TAC[SIN_CIRCLE]);
1288 (ASM_SIMP_TAC[REAL_ARITH `&1 - b + &1 = &2 - b`]);
1289
1290 (* subgoal 12 *)
1291 (SUBGOAL_THEN `!(v:real^3). v IN U' /\ ~(v = s) ==> &2 < dist (s,v)`
1292 (LABEL_TAC "iso"));
1293 (GEN_TAC);
1294 (Q_EXPAND_TAC "new_set");
1295 (SIMP_TAC[IN_INSERT; TAUT ` ((A \/ B) /\ ~A) <=> (~A /\ B)`]);
1296 (SIMP_TAC[IN_DELETE]);
1297 (ASM_SIMP_TAC[]);
1298
1299 (* subgoal 13 *)
1300 (SUBGOAL_THEN `~(s:real^3 IN U)` ASSUME_TAC);
1301 (ONCE_REWRITE_TAC[SET_RULE `~(x IN S) <=> (!y. y IN S ==> ~(x = y))`]);
1302 GEN_TAC;
1303 STRIP_TAC;
1304 (ASM_CASES_TAC `y':real^3 = w`);
1305
1306 (* subgoal 13.1 *)
1307 (ASM_SIMP_TAC[]);
1308 (* subgoal 13.1.1 *)
1309 (SUBGOAL_THEN `w:real^3 = norm w % e1 + &0 % e2 + &0 % e3` ASSUME_TAC);
1310 (SIMP_TAC[ VECTOR_ARITH `a % e1 + &0 % e2 + &0 % e3 = a % e1`]);
1311 (Q_EXPAND_TAC "e1");
1312 (SIMP_TAC[norm_mul_normalize]);
1313
1314 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[thm]));
1315 (USE_THEN "subs_point" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1316 (CONV_TAC(PAT_CONV `\x. ~(x = A)` (ONCE_REWRITE_CONV[
1317 VECTOR_ARITH `a % e1 + b % e2 = a % e1 + b % e2 + &0 % e3`])));
1318 (MP_TAC ( SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`;
1319 `cos a * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
1320 `norm (w:real^3)`;`&0`;`&0`] ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT ));
1321 (MATCH_MP_TAC(TAUT `(A /\ ~C) ==> ((A ==> ( B <=> C)) ==> ~B) `));
1322 (ASM_SIMP_TAC[]);
1323 (MATCH_MP_TAC (TAUT `~B ==> ~ (A /\ B)`));
1324 (SIMP_TAC[REAL_ENTIRE]);
1325 (SIMP_TAC[TAUT `~(A \/ B) <=> ~A /\ ~B`]);
1326 CONJ_TAC;
1327
1328 (* subgoal 13.1.2 *)
1329 (ASM_SIMP_TAC[PI_WORKS]);
1330 (* subgoal 13.1.3 *)
1331 (MATCH_MP_TAC(ARITH_RULE `&0 < x ==> ~(x = &0)`));
1332 (ASM_SIMP_TAC[NORM_POS_LT]);
1333
1334 (* subgoal 13.2 *)
1335 (ONCE_REWRITE_TAC[DIST_NZ]);
1336 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &0 < a`));
1337 (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
1338 (ASM_SIMP_TAC[]);
1339
1340
1341 (* subgoal 14 *)
1342 (SUBGOAL_THEN `U':real^3 -> bool IN S` ASSUME_TAC);
1343 (EXPAND_TAC "S");
1344 (SIMP_TAC[IN_ELIM_THM]);
1345
1346 (* subgoal 14.1 *)
1347 (SUBGOAL_THEN `norm (s:real^3) = norm (w:real^3)` ASSUME_TAC);
1348 (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
1349 `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma6));
1350 (ASM_SIMP_TAC[]);
1351
1352 (* subgoal 14.2 *)
1353 (SUBGOAL_THEN `FINITE (U':real^3->bool)` ASSUME_TAC);
1354 (Q_EXPAND_TAC "new_set");
1355 (ONCE_REWRITE_TAC[FINITE_INSERT]);
1356 (ASM_SIMP_TAC[FINITE_DELETE]);
1357
1358 (* subgoal 14.3 *)
1359 (SUBGOAL_THEN `packing (U':real^3 -> bool)` ASSUME_TAC);
1360 (PURE_REWRITE_TAC[packing]);
1361 (REPEAT GEN_TAC);
1362 (CONV_TAC(PAT_CONV `\x. x /\ x /\ A ==> B`
1363 (ONCE_REWRITE_CONV[GSYM IN])));
1364 (STRIP_TAC);
1365 (ASM_CASES_TAC `u':real^3 = s`);
1366
1367 (* subgoal 14.3.1 *)
1368 (ASM_SIMP_TAC[]);
1369 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
1370 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1371 (ASM_SIMP_TAC[]);
1372 (FIRST_X_ASSUM(fun thm-> ONCE_REWRITE_TAC[GSYM thm]));
1373 (ASM_SIMP_TAC[EQ_SYM_EQ]);
1374
1375 (ASM_CASES_TAC `v:real^3 = s`);
1376
1377 (* subgoal 14.3.2.1 *)
1378 (ASM_SIMP_TAC[]);
1379 (ONCE_REWRITE_TAC[DIST_SYM]);
1380 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
1381 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1382 (ASM_SIMP_TAC[]);
1383
1384 (* subgoal 14.3.2.2 *)
1385 (UNDISCH_TAC `u':real^3 IN U'`);
1386 (Q_EXPAND_TAC "new_set");
1387 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1388 (STRIP_TAC);
1389 (UNDISCH_TAC `v:real^3 IN U'`);
1390 (Q_EXPAND_TAC "new_set");
1391 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1392 (STRIP_TAC);
1393 (UNDISCH_TAC `packing (U:real^3->bool)`);
1394 (PURE_REWRITE_TAC[packing]);
1395 (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPECL [`u':real^3`;`v:real^3`] thm)));
1396 (CONV_TAC(PAT_CONV `\x. x /\ x /\ A` (ONCE_REWRITE_CONV[GSYM IN])));
1397 (ASM_SIMP_TAC[]);
1398
1399 (ASM_SIMP_TAC[]);
1400 (Q_ABBREV_TAC `(h:real^3->real^3) = (\v. if  v = w then s else v)` "h");
1401 (EXISTS_TAC `(h:real^3->real^3) o (phi:real^3->real^3)`);
1402 (CONJ_TAC);
1403
1404 (* subgoal 14.4 *)
1405 (MATCH_MP_TAC Hypermap.COMPOSE_BIJ);
1406 (EXISTS_TAC `U:real^3->bool`);
1407 (ASM_SIMP_TAC[]);
1408 (* subgoal 14.4.1 *)
1409 (SUBGOAL_THEN `!v:real^3. v IN U ==> (h:real^3->real^3) v IN U'` ASSUME_TAC);
1410 (REPEAT STRIP_TAC);
1411 (Q_EXPAND_TAC "h");
1412 (SIMP_TAC[BETA_THM]);
1413 (COND_CASES_TAC);
1414 (* subgoal 14.4.1.1 *)
1415 (Q_EXPAND_TAC "new_set");
1416 (SET_TAC[]);
1417 (* subgoal 14.5.1.2 *)
1418 (Q_EXPAND_TAC "new_set");
1419 (SIMP_TAC[IN_INSERT]);
1420 (DISJ2_TAC);
1421 (ASM_SIMP_TAC[IN_DELETE]);
1422
1423 (ASM_SIMP_TAC[BIJ;INJ;SURJ]);
1424 (CONJ_TAC);
1425
1426 (* subgoal 14.5.2 *)
1427 (REPEAT STRIP_TAC);
1428 (UNDISCH_TAC `(h:real^3->real^3) x = h y'`);
1429 (Q_EXPAND_TAC "h");
1430 (SIMP_TAC[BETA_THM]);
1431 (COND_CASES_TAC);
1432
1433 (* subgoal 14.5.2.1 *)
1434 (COND_CASES_TAC);
1435 (* subgoal 14.5.2.1.1 *)
1436 (ASM_SIMP_TAC[]);
1437 (* subgoal 14.5.2.1.2 *)
1438 (ASM_MESON_TAC[]);
1439
1440 (* subgoal 14.5.2.2 *)
1441 (COND_CASES_TAC);
1442
1443 (* subgoal 14.5.2.2.1 *)
1444 (ASM_MESON_TAC[]);
1445
1446 (* subgoal 14.5.2.2.2 *)
1447 (SIMP_TAC []);
1448
1449 (* subgoal 14.5.3 *)
1450 (REPEAT STRIP_TAC);
1451 (ASM_CASES_TAC `x:real^3 = s`);
1452
1453 (* subgoal 14.5.3.1 *)
1454 (EXISTS_TAC `w:real^3`);
1455 (ASM_SIMP_TAC[]);
1456 (Q_EXPAND_TAC "h");
1457 (SIMP_TAC[BETA_THM]);
1458
1459 (* subgoal 14.5.3.2 *)
1460 (EXISTS_TAC `x:real^3`);
1461 (UNDISCH_TAC `x:real^3 IN U'`);
1462 (Q_EXPAND_TAC "new_set");
1463 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1464 (STRIP_TAC);
1465 (Q_EXPAND_TAC "h");
1466 (ASM_SIMP_TAC[BETA_THM]);
1467
1468 (REPEAT STRIP_TAC);
1469 (SIMP_TAC[o_THM]);
1470
1471 (* subgoal 14.6 *)
1472 (SUBGOAL_THEN `! x:real^3. x IN U ==> norm x = norm ((h:real^3->real^3) x)` MATCH_MP_TAC);
1473 (REPEAT STRIP_TAC);
1474 (Q_EXPAND_TAC "h");
1475 (SIMP_TAC[BETA_THM]);
1476 (COND_CASES_TAC);
1477 (* subgoal 14.6.1 *)
1478 (ASM_SIMP_TAC[]);
1479
1480 (* subgoal 14.6.2 *)
1481 (SIMP_TAC[]);
1482
1483 (UNDISCH_TAC `BIJ (phi:real^3->real^3) V U`);
1484 (SIMP_TAC[BIJ]);
1485 (DISCH_THEN (fun thm -> MP_TAC (CONJUNCT1 thm)));
1486 (SIMP_TAC[INJ]);
1487 (DISCH_THEN (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
1488 (ASM_SIMP_TAC[]);
1489
1490 (* subgoal 15 *)
1491 (SUBGOAL_THEN `~((f:(real^3->bool)->num) U' <= f U)` ASSUME_TAC);
1492 (ONCE_REWRITE_TAC[ ARITH_RULE `~((a:num) <= b) <=> (b < a)`]);
1493 (EXPAND_TAC "f");
1494 (MATCH_MP_TAC CARD_PSUBSET);
1495 (CONJ_TAC);
1496
1497 (* subgoal 15.1 *)
1498 (ONCE_REWRITE_TAC[PSUBSET_ALT]);
1499 (CONJ_TAC);
1500
1501 (* subgoal 15.1.1 *)
1502 (ONCE_REWRITE_TAC[SUBSET]);
1503 GEN_TAC;
1504 (ONCE_REWRITE_TAC[set_of_iso]);
1505 (SIMP_TAC[IN_ELIM_THM]);
1506 (STRIP_TAC);
1507
1508 (* subgoal 15.1.1.1 *)
1509 (SUBGOAL_THEN `x:real^3 IN U'` ASSUME_TAC);
1510 (Q_EXPAND_TAC "new_set");
1511 (SIMP_TAC[IN_INSERT]);
1512 DISJ2_TAC;
1513 (SIMP_TAC[IN_DELETE]);
1514 (ASM_SIMP_TAC[]);
1515 (ASM_MESON_TAC[]);
1516
1517 (ASM_SIMP_TAC[]);
1518 (ONCE_REWRITE_TAC[GSYM SUBSET_EMPTY]);
1519 (UNDISCH_TAC `set_of_edge x U (ECTC U) = {}`);
1520 (DISCH_THEN(fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1521 (MP_TAC (SPECL [`x:real^3`;`U:real^3->bool`] lemma8));
1522 (ASM_SIMP_TAC[]);
1523 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1524 (MP_TAC (SPECL [`x:real^3`;`U':real^3->bool`] lemma8));
1525 (ASM_SIMP_TAC[]);
1526 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1527 (SIMP_TAC[SUBSET;IN_ELIM_THM]);
1528 GEN_TAC;
1529 (Q_EXPAND_TAC "new_set");
1530 (SIMP_TAC[IN_INSERT;IN_DELETE]);
1531 (MATCH_MP_TAC (TAUT `(D ==> ~A) ==> (A \/ B /\ C) /\ D ==> B`));
1532 (MATCH_MP_TAC (TAUT `(B ==> ~A) ==> (A ==> ~B)`));
1533 STRIP_TAC;
1534 (ASM_SIMP_TAC[]);
1535 (ONCE_REWRITE_TAC[DIST_SYM]);
1536 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~(a = &2)`));
1537 (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
1538 (ASM_SIMP_TAC[]);
1539 (ASM_SET_TAC[]);
1540
1541 (* subgoal 15.2 *)
1542 (EXISTS_TAC `s:real^3`);
1543 (CONJ_TAC);
1544 (* subgoal 15.2.1 *)
1545 (SIMP_TAC[set_of_iso;IN_ELIM_THM]);
1546 (* subgoal 15.2.1.1 *)
1547 (SUBGOAL_THEN `s:real^3 IN U'` ASSUME_TAC);
1548 (Q_EXPAND_TAC "new_set");
1549 (SET_TAC[]);
1550
1551 (ASM_SIMP_TAC[]);
1552 (MP_TAC (SPECL [`s:real^3`;`U':real^3->bool`] lemma8));
1553 (ASM_SIMP_TAC[]);
1554 (MATCH_MP_TAC (TAUT ` B ==> A ==> B`));
1555 (ONCE_REWRITE_TAC[SET_RULE `{x| P x} = {} <=> !x. ~(P x)`]);
1556 (GEN_TAC);
1557 (MATCH_MP_TAC (TAUT ` (A ==> ~B) ==> ~(A /\ B)`));
1558 (STRIP_TAC);
1559 (ASM_CASES_TAC `v:real^3 = s`);
1560
1561 (* subgoal 15.2.1.2 *)
1562 (ASM_SIMP_TAC[DIST_REFL]);
1563 ARITH_TAC;
1564 (* subgoal 15.2.1.3 *)
1565 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~ (a = &2)`));
1566 (USE_THEN "iso" (fun thm -> MATCH_MP_TAC thm));
1567 (ASM_SIMP_TAC[]);
1568
1569 (* subgoal 15.2.2 *)
1570 (ASM_SIMP_TAC[set_of_iso;IN_ELIM_THM]);
1571 (MATCH_MP_TAC ( ISPECL [`set_of_iso (U':real^3->bool)`;
1572 `U':real^3->bool`] FINITE_SUBSET));
1573 (ASM_SIMP_TAC[set_of_iso]);
1574 (SET_TAC[]);
1575
1576 (ASM_MESON_TAC[]);
1577 (ASM_MESON_TAC[]);
1578 ]);;
1579
1580 end;;