2 (* ========================================================================= *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Authour : VU KHAC KY *)
6 (* Book lemma: EMNWUUS *)
7 (* Chaper : Packing (Marchal Cells) *)
8 (* Date : October 3, 2010 *)
10 (* ========================================================================= *)
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 :
19 ! `mcell0 V ul = {} /\ mcell1 V ul = {} /\ mcell2 V ul = {} /\ mcell3 V ul = {}
20 ! ==> hl ul < sqrt (&2)`
23 (* ========================================================================= *)
24 (* FILES NEED TO BE LOADED *)
25 (* ========================================================================= *)
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";;
32 module EMNWUUS = struct
34 (* dmtcp: needs "flyspeck_load.hl";; *)
40 open Vukhacky_tactics;;
43 needs "marchal_cells.hl";;
45 (* ============== Axioms in previous parts ===================================*)
47 let XNHPWAB1 = new_axiom XNHPWAB1_concl;;
49 let XNHPWAB4 = new_axiom XNHPWAB4_concl;;
51 let WAUFCHE1 = new_axiom WAUFCHE1_concl;;
53 let WAUFCHE2 = new_axiom WAUFCHE2_concl;;
55 let OAPVION2 = new_axiom OAPVION2_concl;;
57 let MHFTTZN1 = new_axiom MHFTTZN1_concl;;
59 let MHFTTZN4 = new_axiom MHFTTZN4_concl;;
61 (* ========================================================================= *)
63 let EMNWUUS1 = prove_by_refinement ( EMNWUUS1_concl,
64 [ (REWRITE_TAC[mcell4] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN COND_CASES_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)`);
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]);
74 (ASM_MESON_TAC[list_CASES]);
75 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
78 (NEW_GOAL `LENGTH (ul:(real^3)list) = 0`);
79 (ASM_MESON_TAC[ASSUME `ul:(real^3)list =[]`;LENGTH]);
86 (* ========================================================================= *)
89 e (REPEAT GEN_TAC THEN STRIP_TAC);;
90 (* ! Note: The inverse part of this lemma has not been Done *)
94 e (REPEAT STRIP_TAC);;
95 (* Break into 4 cases *)
97 (* =============== Case 1 ================================ *) (* OK *)
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]);;
103 e (MATCH_MP_TAC BALL_CONVEX_HULL_LEMMA);;
105 e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
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);;
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'`);;
123 (* End subgoal 1.1 *)
125 (* New subgoal 1.2 *)
126 e (NEW_GOAL `hl (truncate_simplex (LENGTH ul - 1) ul) = hl (ul:(real^3)list)`);;
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);;
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`);;
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[]);;
143 e (EXISTS_TAC `[]:(real^3)list`);;
144 e (ASM_MESON_TAC[APPEND_NIL]);;
145 (* End subgoal 1.2 *)
147 (* New subgoal 1.3 *)
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]);;
154 (* ---------------------------------------------- *)
155 (* Consider case x' = 0 *)
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`]);;
164 (* ---------------------------------------------- *)
165 (* Consider case x' = 1 *)
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));;
181 e (REPEAT STRIP_TAC);;
182 e (NEW_GOAL `w IN {u0,u1:real^3}`);;
183 e (UP_ASM_TAC THEN SET_TAC[]);;
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))`);;
191 e (NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},u0))`);;
192 e (FIRST_ASSUM MATCH_MP_TAC);;
194 e (ASM_MESON_TAC[]);;
195 e (ASM_REAL_ARITH_TAC);;
197 (* ---------------------------------------------- *)
198 (* Consider case x' = 2 *)
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));;
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]);;
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);;
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);;
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]);;
256 e (ASM_MESON_TAC[]);;
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]);;
264 e (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a < int_of_num 3 ==> F`]);;
265 e (ASM_MESON_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`));;
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);;
286 e (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);;
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]);;
309 e (ASM_MESON_TAC[]);;
312 e (MATCH_MP_TAC (REAL_ARITH
313 `radV {u0,u1,u2:real^3} = a /\ radV {u0,u1,u2} = b ==> a = b`));;
315 e (ASM_REWRITE_TAC[]);;
316 e (FIRST_ASSUM MATCH_MP_TAC);;
318 e (FIRST_ASSUM MATCH_MP_TAC);;
319 e (ASM_REWRITE_TAC[]);;
320 e (ASM_REAL_ARITH_TAC);;
322 (* ---------------------------------------------- *)
323 (* Consider case x' = 3 *)
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]);;
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]);;
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`));;
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);;
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);;
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]);;
376 e (ASM_MESON_TAC[]);;
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]);;
384 e (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a < int_of_num 3 ==> F`]);;
385 e (ASM_MESON_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`));;
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);;
406 e (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);;
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]);;
429 e (ASM_MESON_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`));;
435 e (ONCE_REWRITE_TAC[DIST_SYM] THEN FIRST_ASSUM MATCH_MP_TAC);;
439 e (ASM_MESON_TAC[]);;
441 (* --------------------------------------------- *)
443 e (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);;
444 e (REWRITE_TAC[BARV]);;
448 e (ASM_MESON_TAC[]);;
451 Here we have finished the first part `mcell0 V ul = {}`;there are 3 parts left:
457 (* =============== Case 2 =================================== *) ( Finished *)
459 e (REWRITE_TAC[mcell1]);;
462 e (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);;
463 e (UP_ASM_TAC THEN MESON_TAC[]);;
466 (* =============== Case 3 =================================== *) (* Finished *)
468 e (REWRITE_TAC[mcell2]);;
471 e (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);;
472 e (UP_ASM_TAC THEN MESON_TAC[]);;
475 (* =============== Case 4 =================================== *) ( Finished *)
477 e (REWRITE_TAC[mcell3]);;
480 e (ASM_REAL_ARITH_TAC);;
481 e (ASM_MESON_TAC[]);;
485 (* =============== Reverse part =============================== *)
487 (* .............................................................*)
490 (* ! Need to be done later ...................................... *)