legacy/oldpacking/ky_packing/EMNWUUS.hl

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