text_formalization/packing/EMNWUUS.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma:  EMNWUUS                                                 *)
   6 (*      Chaper    : Packing (Marchal Cells)                                  *)
   7 (*      Date      : October 3, 2010                                          *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10 (*
  11 #use "/usr/programs/hollight/hollight-svn75/hol.ml";;
  12 loads "Multivariate/flyspeck.ml";;
  13 #use "/home/ky/flyspeck/working/boot.hl";;
  14 flyspeck_needs "trigonometry/trig1.hl";;
  15 flyspeck_needs "trigonometry/trig2.hl";;
  16 flyspeck_needs "trigonometry/trigonometry.hl";;
  17
  18 (* =================  Loaded files   ======================================== *)
  19
  20 flyspeck_needs "leg/collect_geom.hl";;
  21 flyspeck_needs "fan/fan_defs.hl";;
  22 flyspeck_needs "fan/introduction.hl";;
  23 flyspeck_needs "fan/topology.hl";;
  24 flyspeck_needs "fan/fan_misc.hl";;
  25 flyspeck_needs "fan/HypermapAndFan.hl";;
  26 flyspeck_needs "packing/pack_defs.hl";;
  27 flyspeck_needs "packing/pack_concl.hl";;
  28 flyspeck_needs "packing/pack1.hl";;
  29 flyspeck_needs "packing/pack2.hl";;
  30 flyspeck_needs "packing/pack3.hl";;
  31 flyspeck_needs "packing/Rogers.hl";;
  32 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  33 *)
  34 (* ====================== Open appropriate files ============================ *)
  35 flyspeck_needs "packing/marchal_cells.hl";;
  36
  37 module Emnwuus = struct
  38
  39 open Rogers;;
  40 open Prove_by_refinement;;
  41 open Vukhacky_tactics;;
  42 open Pack_defs;;
  43 open Pack_concl;;
  44 open Pack1;;
  45 open Sphere;;
  46 open Marchal_cells;;
  47
  48 let seans_fn () =
  49 let (tms,tm) = top_goal () in
  50 let vss = map frees (tm::tms) in
  51 let vs = setify (flat vss) in
  52 map dest_var vs;;
  53
  54 (* ======================= Begin working ==================================== *)
  55 (* ========================================================================= *)
  56
  57 let EMNWUUS1 = prove_by_refinement ( EMNWUUS1_concl,
  58 [ (REWRITE_TAC[mcell4] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN COND_CASES_TAC);
  59  (REPEAT STRIP_TAC);
  60  (NEW_GOAL `set_of_list (ul:(real^3)list) = {}`);
  61  (ASM_MESON_TAC[CONVEX_HULL_EQ_EMPTY]);
  62  (NEW_GOAL `ul:(real^3)list = []`);
  63  (NEW_GOAL `~(?h t. ul:(real^3)list = CONS h t)`);
  64  STRIP_TAC;
  65  (NEW_GOAL `(h:real^3) IN set_of_list ul`);
  66  (REWRITE_TAC [ASSUME `ul = CONS (h:real^3) t`; IN_SET_OF_LIST;MEM]);
  67  (ASM_SET_TAC[]);
  68  (ASM_MESON_TAC[list_CASES]);
  69  (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
  70  (REWRITE_TAC[BARV]);
  71  STRIP_TAC;
  72  (NEW_GOAL `LENGTH (ul:(real^3)list) = 0`);
  73  (ASM_MESON_TAC[ASSUME `ul:(real^3)list =[]`;LENGTH]);
  74  (ASM_ARITH_TAC);
  75  (MESON_TAC[]);
  76  (MESON_TAC[]);
  77  (MESON_TAC[]) ]);;
  78
  79
  80 (* ========================================================================= *)
  81
  82 let EMNWUUS2 = prove_by_refinement (EMNWUUS2_concl,
  83 [ (REPEAT GEN_TAC THEN STRIP_TAC);
  84 (EQ_TAC);
  85
  86 (REPEAT STRIP_TAC);
  87 (* Break into 4 cases *)
  88
  89 (* =============== Case 1 ================================ *)
  90
  91 (REWRITE_TAC[mcell0]);
  92 (REWRITE_TAC[SET_RULE `x DIFF y = {} <=> (!a. a IN x ==> a IN y)`]);
  93 (REWRITE_TAC[ROGERS;IMAGE;IN;ball;SUBSET;IN_ELIM_THM]);
  94  GEN_TAC;
  95 (MATCH_MP_TAC BALL_CONVEX_HULL_LEMMA);
  96
  97 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]);
  98 (STRIP_TAC);
  99
 100  (* New_subgoal 1.1 *)
 101 (NEW_GOAL `hl (truncate_simplex x' (ul:(real^3)list))
 102           <= hl (truncate_simplex (LENGTH ul - 1) ul)`);
 103 (ASM_CASES_TAC `x' < LENGTH (ul:(real^3)list) - 1`);
 104 (MATCH_MP_TAC (REAL_ARITH `a < b ==> a <= b`));
 105 (NEW_GOAL `x' < (LENGTH (ul:(real^3)list) - 1) /\ LENGTH ul - 1 <= 3`);
 106 (ASM_REWRITE_TAC[] THEN UNDISCH_TAC `barV V 3 ul`);
 107 (REWRITE_TAC[BARV] THEN ARITH_TAC);
 108 (UP_ASM_TAC);
 109 (NEW_GOAL `ul IN barV V 3`);
 110 (ASM_MESON_TAC[IN]);
 111 (ASM_MESON_TAC[XNHPWAB4; ARITH_RULE `3 <= 3`]);
 112 (MATCH_MP_TAC (REAL_ARITH `a = b ==> a <= b`));
 113 (REWRITE_WITH `LENGTH (ul:(real^3)list) - 1 = x'`);
 114 (ASM_ARITH_TAC);
 115   (* End subgoal 1.1 *)
 116
 117   (* New subgoal 1.2 *)
 118 (NEW_GOAL `hl (truncate_simplex (LENGTH ul - 1) ul) = hl (ul:(real^3)list)`);
 119 (AP_TERM_TAC);
 120 (REWRITE_TAC[TRUNCATE_SIMPLEX]);
 121 (MATCH_MP_TAC SELECT_UNIQUE);
 122 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;INITIAL_SUBLIST] THEN EQ_TAC);
 123 STRIP_TAC;
 124 (NEW_GOAL `LENGTH (ul:(real^3)list) =
 125              LENGTH (y:(real^3)list) + LENGTH (yl:(real^3)list)`);
 126 (ASM_MESON_TAC[LENGTH_APPEND]);
 127 (NEW_GOAL `LENGTH (yl:(real^3)list) = 0`);
 128 (ASM_ARITH_TAC);
 129 (NEW_GOAL `(yl:(real^3)list) = []`);
 130 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 131 (ASM_MESON_TAC[APPEND_NIL]);
 132 (REPEAT STRIP_TAC);
 133 (ASM_REWRITE_TAC[]);
 134 (ASM_ARITH_TAC);
 135 (EXISTS_TAC `[]:(real^3)list`);
 136 (ASM_MESON_TAC[APPEND_NIL]);
 137   (* End subgoal 1.2 *)
 138
 139   (* New subgoal 1.3 *)
 140
 141 (NEW_GOAL `?u0 u1 u2 u3:real^3. ul = [u0;u1;u2;u3]`);
 142 (ASM_MESON_TAC[BARV_3_EXPLICIT]);
 143 (REPEAT (FIRST_X_ASSUM CHOOSE_TAC));
 144 (REWRITE_TAC[ASSUME `ul = [u0:real^3; u1; u2; u3]`; HD]);
 145
 146   (* ---------------------------------------------- *)
 147   (* Consider case x' = 0 *)
 148
 149 (ASM_CASES_TAC `x' = 0`);
 150 (REWRITE_WITH `x:real^3 = u0`);
 151 (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));
 152 (ASM_MESON_TAC[OMEGA_LIST_0_EXPLICIT; GSYM IN]);
 153 (ASM_REWRITE_TAC[DIST_REFL]);
 154 (MESON_TAC[SQRT_LT_0;REAL_ARITH `&0 <= &2 /\ &0 < &2`]);
 155
 156   (* ---------------------------------------------- *)
 157   (* Consider case x' = 1 *)
 158
 159 (ASM_CASES_TAC `x' = 1`);
 160 (REWRITE_WITH `x:real^3 = circumcenter {u0, u1}`);
 161 (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));
 162 (ASM_MESON_TAC[OMEGA_LIST_1_EXPLICIT; GSYM IN]);
 163 (ONCE_REWRITE_TAC[DIST_SYM]);
 164 (REWRITE_WITH `dist (circumcenter {u0:real^3, u1},u0)
 165                = hl (truncate_simplex x' (ul:(real^3)list))`);
 166 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;HL;radV]);
 167 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 168 (MATCH_MP_TAC SELECT_UNIQUE);
 169 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list]
 170    `set_of_list [u0:real^3;u1] = {u0, u1}`] THEN EQ_TAC);
 171 (DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC));
 172 (SUBGOAL_THEN `(u0:real^3) IN {u0, u1}` ASSUME_TAC);
 173 (SET_TAC[]);
 174 (ASM_MESON_TAC[IN]);
 175 (REPEAT STRIP_TAC);
 176 (NEW_GOAL `w IN {u0,u1:real^3}`);
 177 (UP_ASM_TAC THEN MESON_TAC[IN]);
 178 (NEW_GOAL
 179  `(!w. w IN {u0,u1:real^3} ==> radV {u0,u1} = dist (circumcenter {u0,u1},w))`);
 180 (MATCH_MP_TAC OAPVION2);
 181 (REWRITE_TAC[AFFINE_INDEPENDENT_2]);
 182 (ASM_REWRITE_TAC[]);
 183 (NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},w))`);
 184 (ASM_SIMP_TAC[]);
 185 (NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},u0))`);
 186 (FIRST_ASSUM MATCH_MP_TAC);
 187 (SET_TAC[]);
 188 (ASM_MESON_TAC[]);
 189 (ASM_REAL_ARITH_TAC);
 190
 191   (* ---------------------------------------------- *)
 192   (* Consider case x' = 2 *)
 193
 194 (ASM_CASES_TAC `x' = 2`);
 195 (REWRITE_WITH `x:real^3 = circumcenter {u0, u1, u2}`);
 196 (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));
 197 (ASM_MESON_TAC[OMEGA_LIST_2_EXPLICIT; GSYM IN]);
 198 (ONCE_REWRITE_TAC[DIST_SYM]);
 199 (REWRITE_WITH `dist (circumcenter {u0:real^3, u1, u2},u0)
 200                = hl (truncate_simplex x' (ul:(real^3)list))`);
 201 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;HL;radV]);
 202 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 203 (MATCH_MP_TAC SELECT_UNIQUE);
 204 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list]
 205    `set_of_list [u0:real^3;u1;u2] = {u0, u1, u2}`] THEN EQ_TAC);
 206 (DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC));
 207 (SUBGOAL_THEN `(u0:real^3) IN {u0, u1, u2}` ASSUME_TAC);
 208 (SET_TAC[]);
 209 (ASM_MESON_TAC[IN]);
 210 (REPEAT STRIP_TAC);
 211 (NEW_GOAL `w IN {u0,u1:real^3,u2}`);
 212 (UP_ASM_TAC THEN MESON_TAC[IN]);
 213 (NEW_GOAL `(!w. w IN {u0,u1:real^3, u2} ==>
 214              radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w))`);
 215 (MATCH_MP_TAC OAPVION2);
 216 (MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET);
 217 (EXISTS_TAC `{u0, u1, u2, u3:real^3}`);
 218 (REWRITE_TAC[SET_RULE `{a, b:A, c} SUBSET {a, b , c, d:A}`]);
 219 (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);
 220 STRIP_TAC;
 221 (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list]
 222    `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);
 223 (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);
 224 (REWRITE_TAC[MESON[set_of_list]
 225    `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);
 226 (MATCH_MP_TAC MHFTTZN1);
 227 (EXISTS_TAC `V:real^3->bool`);
 228 (ASM_MESON_TAC[ARITH_RULE `3 <= 3`]);
 229 (ONCE_ASM_REWRITE_TAC[]);
 230 (NEW_GOAL `FINITE {u1, u2, u3:real^3}`);
 231 (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list]
 232    `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]);
 233 (MATCH_MP_TAC (ARITH_RULE
 234   `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`));
 235 (MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`));
 236 (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} =
 237             (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}
 238              else SUC (CARD {u1, u2, u3} ))`);
 239 (UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]);
 240 (UP_ASM_TAC THEN COND_CASES_TAC);
 241 (DISCH_TAC);
 242 (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`);
 243 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`);
 244 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 245 (NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=>
 246             {u1, u2, u3:real^3} = {u0, u1, u2, u3}`);
 247 (MATCH_MP_TAC SUBSET_CARD_EQ);
 248 (STRIP_TAC);
 249 (REWRITE_TAC[MESON[set_of_list]
 250  `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 251 (SET_TAC[]);
 252 (ASM_MESON_TAC[]);
 253
 254 (REWRITE_TAC[MESON[set_of_list]
 255   `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]);
 256 (MATCH_MP_TAC AFF_DIM_LE_LENGTH);
 257 (REWRITE_TAC[LENGTH]);
 258 (ARITH_TAC);
 259 (NEW_GOAL `F`);
 260 (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]);
 261 (ASM_MESON_TAC[]);
 262  STRIP_TAC;
 263 (NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`);
 264 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 265 (MATCH_MP_TAC (ARITH_RULE
 266  `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`));
 267  STRIP_TAC;
 268 (REWRITE_TAC[MESON[set_of_list]
 269  `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]);
 270 (REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 271 (ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`);
 272 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`);
 273 (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} =
 274   (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`);
 275 (NEW_GOAL `FINITE {u1,u2,u3:real^3}`);
 276 (REWRITE_TAC[MESON[set_of_list]
 277  `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]);
 278 (ASM_REWRITE_TAC[CARD_CLAUSES]);
 279 (UP_ASM_TAC THEN COND_CASES_TAC);
 280 (ASM_ARITH_TAC);
 281 (ASM_ARITH_TAC);
 282 (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);
 283
 284
 285 (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3}
 286            < int_of_num (CARD {u0, u1, u2, u3})`);
 287 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`);
 288 (EXPAND_TAC "xl");
 289 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 290 (MATCH_MP_TAC SET_OF_LIST_OF_SET);
 291 (REWRITE_TAC[MESON[set_of_list]
 292  `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 293 (MATCH_MP_TAC AFF_DIM_LE_LENGTH);
 294 (REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`);
 295 (EXPAND_TAC "xl");
 296 (MATCH_MP_TAC SET_OF_LIST_OF_SET);
 297 (REWRITE_TAC[MESON[set_of_list]
 298  `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 299 (EXPAND_TAC "xl");
 300 (MATCH_MP_TAC LENGTH_LIST_OF_SET);
 301 (REWRITE_TAC[MESON[set_of_list]
 302  `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 303 (NEW_GOAL `F`);
 304 (ASM_ARITH_TAC);
 305 (ASM_MESON_TAC[]);
 306 (ASM_ARITH_TAC);
 307  ASM_ARITH_TAC;
 308 (MATCH_MP_TAC (REAL_ARITH
 309   `radV {u0,u1,u2:real^3} = a /\ radV {u0,u1,u2} = b ==> a = b`));
 310  STRIP_TAC;
 311 (ASM_REWRITE_TAC[]);
 312 (FIRST_ASSUM MATCH_MP_TAC);
 313 (SET_TAC[]);
 314 (FIRST_ASSUM MATCH_MP_TAC);
 315 (ASM_REWRITE_TAC[]);
 316 (ASM_REAL_ARITH_TAC);
 317
 318   (* ---------------------------------------------- *)
 319   (* Consider case x' = 3 *)
 320
 321 (ASM_CASES_TAC `x' = 3`);
 322 (REWRITE_WITH `x = circumcenter {u0,u1,u2,u3:real^3}`);
 323 (ASM_REWRITE_TAC[]);
 324 (MATCH_MP_TAC OMEGA_LIST_3_EXPLICIT);
 325 (ASM_MESON_TAC[GSYM IN]);
 326 (NEW_GOAL `dist (u0,circumcenter {u0:real^3, u1, u2, u3})
 327            = hl (ul:(real^3)list)`);
 328 (ASM_REWRITE_TAC[HL]);
 329 (REWRITE_WITH `set_of_list [u0:real^3; u1; u2; u3] = {u0,u1,u2,u3}`);
 330 (MESON_TAC[set_of_list]);
 331
 332 (NEW_GOAL `(!w. w IN {u0,u1:real^3, u2,u3} ==>
 333              radV {u0,u1,u2,u3} = dist (circumcenter {u0,u1,u2,u3},w))`);
 334 (MATCH_MP_TAC OAPVION2);
 335 (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);
 336  STRIP_TAC;
 337 (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list]
 338    `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);
 339 (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);
 340 (REWRITE_TAC[MESON[set_of_list]
 341    `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);
 342 (MATCH_MP_TAC MHFTTZN1);
 343 (EXISTS_TAC `V:real^3->bool`);
 344 (ASM_MESON_TAC[ARITH_RULE `3 <= 3`]);
 345 (ONCE_ASM_REWRITE_TAC[]);
 346 (MATCH_MP_TAC (ARITH_RULE
 347   `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`));
 348 (MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`));
 349
 350 (NEW_GOAL `FINITE {u1, u2, u3:real^3}`);
 351 (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list]
 352    `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]);
 353 (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} =
 354             (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}
 355              else SUC (CARD {u1, u2, u3} ))`);
 356 (UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]);
 357 (UP_ASM_TAC THEN COND_CASES_TAC);
 358 (DISCH_TAC);
 359 (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`);
 360 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`);
 361 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 362 (NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=>
 363             {u1, u2, u3:real^3} = {u0, u1, u2, u3}`);
 364 (MATCH_MP_TAC SUBSET_CARD_EQ);
 365 (STRIP_TAC);
 366 (REWRITE_TAC[MESON[set_of_list]
 367  `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 368 (SET_TAC[]); (* check *)
 369 (ASM_MESON_TAC[]);
 370
 371 (REWRITE_TAC[MESON[set_of_list]
 372   `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]);
 373 (MATCH_MP_TAC AFF_DIM_LE_LENGTH);
 374 (REWRITE_TAC[LENGTH]);
 375 (ARITH_TAC);
 376 (NEW_GOAL `F`);
 377 (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]);
 378 (ASM_MESON_TAC[]);
 379  STRIP_TAC;
 380 (NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`);
 381 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
 382 (MATCH_MP_TAC (ARITH_RULE
 383  `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`));
 384  STRIP_TAC;
 385 (REWRITE_TAC[MESON[set_of_list]
 386  `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]);
 387 (REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 388 (ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`);
 389 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`);
 390 (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} =
 391   (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`);
 392 (NEW_GOAL `FINITE {u1,u2,u3:real^3}`);
 393 (REWRITE_TAC[MESON[set_of_list]
 394  `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]);
 395 (ASM_REWRITE_TAC[CARD_CLAUSES]);
 396 (UP_ASM_TAC THEN COND_CASES_TAC);
 397 (ASM_ARITH_TAC);
 398 (ASM_ARITH_TAC);
 399 (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);
 400
 401
 402 (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3}
 403            < int_of_num (CARD {u0, u1, u2, u3})`);
 404 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`);
 405 (EXPAND_TAC "xl");
 406 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 407 (MATCH_MP_TAC SET_OF_LIST_OF_SET);
 408 (REWRITE_TAC[MESON[set_of_list]
 409  `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 410 (MATCH_MP_TAC AFF_DIM_LE_LENGTH);
 411 (REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`);
 412 (EXPAND_TAC "xl");
 413 (MATCH_MP_TAC SET_OF_LIST_OF_SET);
 414 (REWRITE_TAC[MESON[set_of_list]
 415  `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 416 (EXPAND_TAC "xl");
 417 (MATCH_MP_TAC LENGTH_LIST_OF_SET);
 418 (REWRITE_TAC[MESON[set_of_list]
 419  `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);
 420 (NEW_GOAL `F`);
 421 (ASM_ARITH_TAC);
 422 (ASM_MESON_TAC[]);
 423 (ASM_ARITH_TAC);
 424  ASM_ARITH_TAC;
 425 (MATCH_MP_TAC (REAL_ARITH
 426   `radV {u0,u1,u2:real^3,u3} = a /\ radV {u0,u1,u2,u3} = b ==> a = b`));
 427  STRIP_TAC;
 428 (ONCE_REWRITE_TAC[DIST_SYM] THEN FIRST_ASSUM MATCH_MP_TAC);
 429 (SET_TAC[]);
 430 (MESON_TAC[]);
 431
 432 (ASM_MESON_TAC[]);
 433
 434 (* --------------------------------------------- *)
 435
 436 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
 437 (REWRITE_TAC[BARV]);
 438 (STRIP_TAC);
 439 (NEW_GOAL `F`);
 440 (ASM_ARITH_TAC);
 441 (ASM_MESON_TAC[]);
 442
 443 (*
 444 Here we have finished the first part `mcell0 V ul = {}`;there are 3 parts left:
 445 mcell1 V ul = {}
 446 mcell2 V ul = {}
 447 mcell3 V ul = {}
 448 *)
 449
 450 (* =============== Case 2 =================================== *)
 451
 452 (REWRITE_TAC[mcell1]);
 453 (COND_CASES_TAC);
 454 (NEW_GOAL `F`);
 455 (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);
 456 (UP_ASM_TAC THEN MESON_TAC[]);
 457 (REWRITE_TAC[]);
 458
 459 (* =============== Case 3 =================================== *)
 460 (REWRITE_TAC[mcell2]);
 461 (COND_CASES_TAC);
 462 (NEW_GOAL `F`);
 463 (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);
 464 (UP_ASM_TAC THEN MESON_TAC[]);
 465 (REWRITE_TAC[]);
 466
 467 (* =============== Case 4 =================================== *)
 468
 469 (REWRITE_TAC[mcell3]);
 470 (COND_CASES_TAC);
 471 (NEW_GOAL `F`);
 472 (ASM_REAL_ARITH_TAC);
 473 (ASM_MESON_TAC[]);
 474 (MESON_TAC[]);
 475
 476
 477 (* =============== Reverse part =============================== *)
 478
 479 (REPEAT STRIP_TAC);
 480 (ASM_CASES_TAC `hl (ul:(real^3)list) >= sqrt (&2)`);
 481 (NEW_GOAL `omega_list V (ul:(real^3)list) IN mcell0 V ul`);
 482 (REWRITE_TAC[mcell0; IN_DIFF;ROGERS]);
 483 (STRIP_TAC);
 484 (NEW_GOAL`LENGTH (ul:(real^3)list) = 4`);
 485 (NEW_GOAL `?u0 u1 u2 u3:real^3. ul = [u0; u1; u2; u3]`);
 486 (MATCH_MP_TAC BARV_3_EXPLICIT);
 487 (EXISTS_TAC `V:real^3->bool`);
 488 (ASM_REWRITE_TAC[]);
 489 (FIRST_X_ASSUM CHOOSE_TAC);
 490 (FIRST_X_ASSUM CHOOSE_TAC);
 491 (FIRST_X_ASSUM CHOOSE_TAC);
 492 (FIRST_X_ASSUM CHOOSE_TAC);
 493 (ASM_REWRITE_TAC[LENGTH]);
 494 (ARITH_TAC);
 495 (ASM_REWRITE_TAC[OMEGA_LIST; ARITH_RULE `4 - 1 = 3`]);
 496 (REWRITE_TAC[IMAGE; CONVEX_HULL_EXPLICIT; IN; IN_ELIM_THM]);
 497 (EXISTS_TAC `{omega_list_n V (ul:(real^3)list) 3}`);
 498 (ABBREV_TAC `u = (\x:real^3. &1 )`);
 499
 500 (EXISTS_TAC `(\x:real^3. &1)`);
 501 (REPEAT STRIP_TAC);
 502 (MESON_TAC[FINITE_SING]);
 503 (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM; Geomdetail.IN_ACT_SING]);
 504 (GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);
 505 (EXISTS_TAC `3`);
 506 (ASM_REWRITE_TAC[ARITH_RULE `3 < 4`]);
 507 (REWRITE_TAC[BETA_THM]);
 508 (REAL_ARITH_TAC);
 509 (REWRITE_TAC[SUM_SING]);
 510 (REWRITE_TAC[VSUM_SING]);
 511 (VECTOR_ARITH_TAC);
 512 (REWRITE_TAC[IN; ball; IN_ELIM_THM]);
 513 (ONCE_REWRITE_TAC[DIST_SYM]);
 514 (MATCH_MP_TAC (REAL_ARITH `x <= y ==> ~(y < x)`));
 515 (MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) >= x /\ hl ul <= z ==> x <= z`));
 516 (ASM_REWRITE_TAC[]);
 517 (MATCH_MP_TAC WAUFCHE1);
 518 (EXISTS_TAC `3`);
 519 (ASM_REWRITE_TAC[IN]);
 520 (NEW_GOAL `F`);
 521 (UP_ASM_TAC THEN UNDISCH_TAC `mcell0 V (ul:(real^3)list) = {}`);
 522 (SET_TAC[]);
 523 (UP_ASM_TAC THEN MESON_TAC[]);
 524 (UP_ASM_TAC THEN REAL_ARITH_TAC)]);;
 525
 526 end;;